|
|
|
@ -46,7 +46,9 @@ elab "Title" t:str : command => do
|
|
|
|
match ← getCurLayer with
|
|
|
|
match ← getCurLayer with
|
|
|
|
| .Level => modifyCurLevel fun level => pure {level with title := t.getString}
|
|
|
|
| .Level => modifyCurLevel fun level => pure {level with title := t.getString}
|
|
|
|
| .World => modifyCurWorld fun world => pure {world with title := t.getString}
|
|
|
|
| .World => modifyCurWorld fun world => pure {world with title := t.getString}
|
|
|
|
| .Game => modifyCurGame fun game => pure {game with title := t.getString}
|
|
|
|
| .Game => modifyCurGame fun game => pure {game with
|
|
|
|
|
|
|
|
title := t.getString
|
|
|
|
|
|
|
|
tile := {game.tile with title := t.getString}}
|
|
|
|
|
|
|
|
|
|
|
|
/-- Define the introduction of the current game/world/level. -/
|
|
|
|
/-- Define the introduction of the current game/world/level. -/
|
|
|
|
elab "Introduction" t:str : command => do
|
|
|
|
elab "Introduction" t:str : command => do
|
|
|
|
@ -58,10 +60,32 @@ elab "Introduction" t:str : command => do
|
|
|
|
/-- Define the info of the current game. Used for e.g. credits -/
|
|
|
|
/-- Define the info of the current game. Used for e.g. credits -/
|
|
|
|
elab "Info" t:str : command => do
|
|
|
|
elab "Info" t:str : command => do
|
|
|
|
match ← getCurLayer with
|
|
|
|
match ← getCurLayer with
|
|
|
|
| .Level => pure ()
|
|
|
|
| .Level =>
|
|
|
|
| .World => pure ()
|
|
|
|
logError "Can't use `Info` in a level!"
|
|
|
|
|
|
|
|
pure ()
|
|
|
|
|
|
|
|
| .World =>
|
|
|
|
|
|
|
|
logError "Can't use `Info` in a world"
|
|
|
|
|
|
|
|
pure ()
|
|
|
|
| .Game => modifyCurGame fun game => pure {game with info := t.getString}
|
|
|
|
| .Game => modifyCurGame fun game => pure {game with info := t.getString}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
/-- Provide the location of the image for the current game/world/level.
|
|
|
|
|
|
|
|
Paths are relative to the lean project's root. -/
|
|
|
|
|
|
|
|
elab "Image" t:str : command => do
|
|
|
|
|
|
|
|
let file := t.getString
|
|
|
|
|
|
|
|
if not <| ← System.FilePath.pathExists file then
|
|
|
|
|
|
|
|
logWarningAt t s!"Make sure the cover image '{file}' exists."
|
|
|
|
|
|
|
|
if not <| file.startsWith "images/" then
|
|
|
|
|
|
|
|
logWarningAt t s!"The file name should start with `images/`. Make sure all images are in that folder."
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
match ← getCurLayer with
|
|
|
|
|
|
|
|
| .Level =>
|
|
|
|
|
|
|
|
logWarning "Level-images not implemented yet" -- TODO
|
|
|
|
|
|
|
|
modifyCurLevel fun level => pure {level with image := file}
|
|
|
|
|
|
|
|
| .World =>
|
|
|
|
|
|
|
|
modifyCurWorld fun world => pure {world with image := file}
|
|
|
|
|
|
|
|
| .Game =>
|
|
|
|
|
|
|
|
logWarning "Main image of the game not implemented yet" -- TODO
|
|
|
|
|
|
|
|
modifyCurGame fun game => pure {game with image := file}
|
|
|
|
|
|
|
|
|
|
|
|
/-- Define the conclusion of the current game or current level if some
|
|
|
|
/-- Define the conclusion of the current game or current level if some
|
|
|
|
building a level. -/
|
|
|
|
building a level. -/
|
|
|
|
@ -71,6 +95,38 @@ elab "Conclusion" t:str : command => do
|
|
|
|
| .World => modifyCurWorld fun world => pure {world with conclusion := t.getString}
|
|
|
|
| .World => modifyCurWorld fun world => pure {world with conclusion := t.getString}
|
|
|
|
| .Game => modifyCurGame fun game => pure {game with conclusion := t.getString}
|
|
|
|
| .Game => modifyCurGame fun game => pure {game with conclusion := t.getString}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
/-- A list of games that should be played before this one. Example `Prerequisites "NNG" "STG"`. -/
|
|
|
|
|
|
|
|
elab "Prerequisites" t:str* : command => do
|
|
|
|
|
|
|
|
modifyCurGame fun game => pure {game with
|
|
|
|
|
|
|
|
tile := {game.tile with prerequisites := t.map (·.getString) |>.toList}}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
/-- Short caption for the game (1 sentence) -/
|
|
|
|
|
|
|
|
elab "CaptionShort" t:str : command => do
|
|
|
|
|
|
|
|
modifyCurGame fun game => pure {game with
|
|
|
|
|
|
|
|
tile := {game.tile with short := t.getString}}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
/-- More detailed description what the game is about (2-4 sentences). -/
|
|
|
|
|
|
|
|
elab "CaptionLong" t:str : command => do
|
|
|
|
|
|
|
|
modifyCurGame fun game => pure {game with
|
|
|
|
|
|
|
|
tile := {game.tile with long := t.getString}}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
/-- A list of Languages the game is translated to. For example `Languages "German" "English"`.
|
|
|
|
|
|
|
|
NOTE: For the time being, only a single language is supported.
|
|
|
|
|
|
|
|
-/
|
|
|
|
|
|
|
|
elab "Languages" t:str* : command => do
|
|
|
|
|
|
|
|
modifyCurGame fun game => pure {game with
|
|
|
|
|
|
|
|
tile := {game.tile with languages := t.map (·.getString) |>.toList}}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
/-- The Image of the game (optional). TODO: Not impementeds -/
|
|
|
|
|
|
|
|
elab "CoverImage" t:str : command => do
|
|
|
|
|
|
|
|
let file := t.getString
|
|
|
|
|
|
|
|
if not <| ← System.FilePath.pathExists file then
|
|
|
|
|
|
|
|
logWarningAt t s!"Make sure the cover image '{file}' exists."
|
|
|
|
|
|
|
|
if not <| file.startsWith "images/" then
|
|
|
|
|
|
|
|
logWarningAt t s!"The file name should start with `images/`. Make sure all images are in that folder."
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
modifyCurGame fun game => pure {game with
|
|
|
|
|
|
|
|
tile := {game.tile with image := file}}
|
|
|
|
|
|
|
|
|
|
|
|
/-! # Inventory
|
|
|
|
/-! # Inventory
|
|
|
|
|
|
|
|
|
|
|
|
@ -626,6 +682,27 @@ elab "Template" tacs:tacticSeq : tactic => do
|
|
|
|
modifyLevel (←getCurLevelId) fun level => do
|
|
|
|
modifyLevel (←getCurLevelId) fun level => do
|
|
|
|
return {level with template := s!"{template}"}
|
|
|
|
return {level with template := s!"{template}"}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
open IO.FS System FilePath in
|
|
|
|
|
|
|
|
/-- Copies the folder `images/` to `.lake/gamedata/images/` -/
|
|
|
|
|
|
|
|
def copyImages : IO Unit := do
|
|
|
|
|
|
|
|
let target : FilePath := ".lake" / "gamedata"
|
|
|
|
|
|
|
|
if ← FilePath.pathExists "images" then
|
|
|
|
|
|
|
|
for file in ← walkDir "images" do
|
|
|
|
|
|
|
|
let outFile := target.join file
|
|
|
|
|
|
|
|
-- create the directories
|
|
|
|
|
|
|
|
if ← file.isDir then
|
|
|
|
|
|
|
|
createDirAll outFile
|
|
|
|
|
|
|
|
else
|
|
|
|
|
|
|
|
if let some parent := outFile.parent then
|
|
|
|
|
|
|
|
createDirAll parent
|
|
|
|
|
|
|
|
-- copy file
|
|
|
|
|
|
|
|
let content ← readBinFile file
|
|
|
|
|
|
|
|
writeBinFile outFile content
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
-- TODO: Notes for testing if a declaration has the simp attribute
|
|
|
|
-- TODO: Notes for testing if a declaration has the simp attribute
|
|
|
|
|
|
|
|
|
|
|
|
-- -- Test: From zulip
|
|
|
|
-- -- Test: From zulip
|
|
|
|
@ -647,7 +724,7 @@ elab "Template" tacs:tacticSeq : tactic => do
|
|
|
|
#eval IO.FS.createDirAll ".lake/gamedata/"
|
|
|
|
#eval IO.FS.createDirAll ".lake/gamedata/"
|
|
|
|
|
|
|
|
|
|
|
|
-- TODO: register all of this as ToJson instance?
|
|
|
|
-- TODO: register all of this as ToJson instance?
|
|
|
|
def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : CommandElabM Unit:= do
|
|
|
|
def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : CommandElabM Unit := do
|
|
|
|
let game ← getCurGame
|
|
|
|
let game ← getCurGame
|
|
|
|
let env ← getEnv
|
|
|
|
let env ← getEnv
|
|
|
|
let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata"
|
|
|
|
let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata"
|
|
|
|
@ -656,6 +733,9 @@ def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : Comma
|
|
|
|
IO.FS.removeDirAll path
|
|
|
|
IO.FS.removeDirAll path
|
|
|
|
IO.FS.createDirAll path
|
|
|
|
IO.FS.createDirAll path
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
-- copy the images folder
|
|
|
|
|
|
|
|
copyImages
|
|
|
|
|
|
|
|
|
|
|
|
for (worldId, world) in game.worlds.nodes.toArray do
|
|
|
|
for (worldId, world) in game.worlds.nodes.toArray do
|
|
|
|
for (levelId, level) in world.levels.toArray do
|
|
|
|
for (levelId, level) in world.levels.toArray do
|
|
|
|
IO.FS.writeFile (path / s!"level__{worldId}__{levelId}.json") (toString (toJson (level.toInfo env)))
|
|
|
|
IO.FS.writeFile (path / s!"level__{worldId}__{levelId}.json") (toString (toJson (level.toInfo env)))
|
|
|
|
@ -848,8 +928,12 @@ elab "MakeGame" : command => do
|
|
|
|
-- Items that should not be displayed in inventory
|
|
|
|
-- Items that should not be displayed in inventory
|
|
|
|
let mut hiddenItems : HashSet Name := {}
|
|
|
|
let mut hiddenItems : HashSet Name := {}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let allWorlds := game.worlds.nodes.toArray
|
|
|
|
|
|
|
|
let nrWorlds := allWorlds.size
|
|
|
|
|
|
|
|
let mut nrLevels := 0
|
|
|
|
|
|
|
|
|
|
|
|
-- Calculate which "items" are used/new in which world
|
|
|
|
-- Calculate which "items" are used/new in which world
|
|
|
|
for (worldId, world) in game.worlds.nodes.toArray do
|
|
|
|
for (worldId, world) in allWorlds do
|
|
|
|
let mut usedItems : HashSet Name := {}
|
|
|
|
let mut usedItems : HashSet Name := {}
|
|
|
|
let mut newItems : HashSet Name := {}
|
|
|
|
let mut newItems : HashSet Name := {}
|
|
|
|
for inventoryType in #[.Tactic, .Definition, .Lemma] do
|
|
|
|
for inventoryType in #[.Tactic, .Definition, .Lemma] do
|
|
|
|
@ -888,9 +972,12 @@ elab "MakeGame" : command => do
|
|
|
|
-- logInfo m!"{worldId} uses: {usedItems.toList}"
|
|
|
|
-- logInfo m!"{worldId} uses: {usedItems.toList}"
|
|
|
|
-- logInfo m!"{worldId} introduces: {newItems.toList}"
|
|
|
|
-- logInfo m!"{worldId} introduces: {newItems.toList}"
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
-- Moreover, count the number of levels in the game
|
|
|
|
|
|
|
|
nrLevels := nrLevels + world.levels.toArray.size
|
|
|
|
|
|
|
|
|
|
|
|
/- for each "item" this is a HashSet of `worldId`s that introduce this item -/
|
|
|
|
/- for each "item" this is a HashSet of `worldId`s that introduce this item -/
|
|
|
|
let mut worldsWithNewItem : HashMap Name (HashSet Name) := {}
|
|
|
|
let mut worldsWithNewItem : HashMap Name (HashSet Name) := {}
|
|
|
|
for (worldId, _world) in game.worlds.nodes.toArray do
|
|
|
|
for (worldId, _world) in allWorlds do
|
|
|
|
for newItem in newItemsInWorld.findD worldId {} do
|
|
|
|
for newItem in newItemsInWorld.findD worldId {} do
|
|
|
|
worldsWithNewItem := worldsWithNewItem.insert newItem $
|
|
|
|
worldsWithNewItem := worldsWithNewItem.insert newItem $
|
|
|
|
(worldsWithNewItem.findD newItem {}).insert worldId
|
|
|
|
(worldsWithNewItem.findD newItem {}).insert worldId
|
|
|
|
@ -902,7 +989,7 @@ elab "MakeGame" : command => do
|
|
|
|
let mut dependencyReasons : HashMap (Name × Name) (HashSet Name) := {}
|
|
|
|
let mut dependencyReasons : HashMap (Name × Name) (HashSet Name) := {}
|
|
|
|
|
|
|
|
|
|
|
|
-- Calculate world dependency graph `game.worlds`
|
|
|
|
-- Calculate world dependency graph `game.worlds`
|
|
|
|
for (dependentWorldId, _dependentWorld) in game.worlds.nodes.toArray do
|
|
|
|
for (dependentWorldId, _dependentWorld) in allWorlds do
|
|
|
|
let mut dependsOnWorlds : HashSet Name := {}
|
|
|
|
let mut dependsOnWorlds : HashSet Name := {}
|
|
|
|
-- Adding manual dependencies that were specified via the `Dependency` command.
|
|
|
|
-- Adding manual dependencies that were specified via the `Dependency` command.
|
|
|
|
for (sourceId, targetId) in game.worlds.edges do
|
|
|
|
for (sourceId, targetId) in game.worlds.edges do
|
|
|
|
@ -953,11 +1040,21 @@ elab "MakeGame" : command => do
|
|
|
|
logError m!"{w1} depends on {w2} because of {items.toList}."
|
|
|
|
logError m!"{w1} depends on {w2} because of {items.toList}."
|
|
|
|
else
|
|
|
|
else
|
|
|
|
worldDependsOnWorlds ← removeTransitive worldDependsOnWorlds
|
|
|
|
worldDependsOnWorlds ← removeTransitive worldDependsOnWorlds
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
-- need to delete all existing edges as they are already present in `worldDependsOnWorlds`.
|
|
|
|
|
|
|
|
modifyCurGame fun game =>
|
|
|
|
|
|
|
|
pure {game with worlds := {game.worlds with edges := Array.empty}}
|
|
|
|
|
|
|
|
|
|
|
|
for (dependentWorldId, worldIds) in worldDependsOnWorlds.toArray do
|
|
|
|
for (dependentWorldId, worldIds) in worldDependsOnWorlds.toArray do
|
|
|
|
modifyCurGame fun game =>
|
|
|
|
modifyCurGame fun game =>
|
|
|
|
pure {game with worlds := {game.worlds with
|
|
|
|
pure {game with worlds := {game.worlds with
|
|
|
|
edges := game.worlds.edges.append (worldIds.toArray.map fun wid => (wid, dependentWorldId))}}
|
|
|
|
edges := game.worlds.edges.append (worldIds.toArray.map fun wid => (wid, dependentWorldId))}}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
-- Add the number of levels and worlds to the tile for the landing page
|
|
|
|
|
|
|
|
modifyCurGame fun game => pure {game with tile := {game.tile with
|
|
|
|
|
|
|
|
levels := nrLevels
|
|
|
|
|
|
|
|
worlds := nrWorlds }}
|
|
|
|
|
|
|
|
|
|
|
|
-- Apparently we need to reload `game` to get the changes to `game.worlds` we just made
|
|
|
|
-- Apparently we need to reload `game` to get the changes to `game.worlds` we just made
|
|
|
|
let game ← getCurGame
|
|
|
|
let game ← getCurGame
|
|
|
|
|
|
|
|
|
|
|
|
|
Jon Eugster
3 years ago
