diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean index d2fa975..b7e532c 100644 --- a/server/GameServer/EnvExtensions.lean +++ b/server/GameServer/EnvExtensions.lean @@ -381,7 +381,7 @@ structure GameTile where TODO: What's the format? -/ image: String := default -deriving Inhabited, ToJson +deriving Inhabited, ToJson, FromJson structure Game where /-- Internal name of the game. -/ @@ -401,7 +401,7 @@ structure Game where tile : GameTile := default /-- The path to the background image of the world. -/ image : String := default -deriving Inhabited, ToJson +deriving Inhabited, ToJson, FromJson def getGameJson (game : «Game») : Json := Id.run do let gameJson : Json := toJson game diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index d1b9ad9..d8faead 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -2,6 +2,7 @@ import Lean.Server.FileWorker import GameServer.Game import GameServer.ImportModules +import GameServer.SaveData namespace MyModule open Lean @@ -461,8 +462,9 @@ section Initialization def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options) (gameDir : String) : IO (WorkerContext × WorkerState) := do + let game ← loadGameData gameDir -- TODO: We misuse the `rootUri` field to the gameName - let rootUri? := some "MyGame" + let rootUri? : Option String := some (toString game.name) let initParams := {initParams with rootUri?} let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets) diff --git a/server/GameServer/Graph.lean b/server/GameServer/Graph.lean index 0cd5f63..30adc16 100644 --- a/server/GameServer/Graph.lean +++ b/server/GameServer/Graph.lean @@ -18,6 +18,14 @@ instance [ToJson β] : ToJson (Graph Name β) := { ] } +-- Just a dummy implementation for now: +instance : FromJson (Graph Name β) := { + fromJson? := fun _ => .ok { + nodes := {} + edges := {} + } +} + instance : EmptyCollection (Graph α β) := ⟨default⟩ def Graph.insertNode (g : Graph α β) (a : α) (b : β) := diff --git a/server/GameServer/SaveData.lean b/server/GameServer/SaveData.lean index 4aa17fc..be50bd7 100644 --- a/server/GameServer/SaveData.lean +++ b/server/GameServer/SaveData.lean @@ -22,17 +22,21 @@ def copyImages : IO Unit := do let content ← readBinFile file writeBinFile outFile content +namespace GameData + def gameDataPath : System.FilePath := ".lake" / "gamedata" + def gameFileName := s!"game.json" + def docFileName := fun (inventoryType : InventoryType) (name : Name) => s!"doc__{inventoryType}__{name}.json" + def levelFileName := fun (worldId : Name) (levelId : Nat) => s!"level__{worldId}__{levelId}.json" + def inventoryFileName := s!"inventory.json" +end GameData --- TODO: I'm not sure this should be happening here... -#eval IO.FS.createDirAll ".lake/gamedata/" - +open GameData in -- TODO: register all of this as ToJson instance? def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) (inventory : InventoryOverview): CommandElabM Unit := do let game ← getCurGame let env ← getEnv - let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata" - + let path := (← IO.currentDir) / gameDataPath if ← path.isDir then IO.FS.removeDirAll path IO.FS.createDirAll path @@ -42,14 +46,37 @@ def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) for (worldId, world) in game.worlds.nodes.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 / levelFileName worldId levelId) (toString (toJson (level.toInfo env))) - IO.FS.writeFile (path / s!"game.json") (toString (getGameJson game)) + IO.FS.writeFile (path / gameFileName) (toString (getGameJson game)) for inventoryType in [InventoryType.Lemma, .Tactic, .Definition] do for name in allItemsByType.findD inventoryType {} do let some item ← getInventoryItem? name inventoryType | throwError "Expected item to exist: {name}" - IO.FS.writeFile (path / s!"doc__{inventoryType}__{name}.json") (toString (toJson item)) + IO.FS.writeFile (path / docFileName inventoryType name) (toString (toJson item)) + + let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do + (allItemsByType.findD type {}).toArray.mapM (fun name => do + let some item ← getInventoryItem? name type + | throwError "Expected item to exist: {name}" + return item.toTile) + let inventory : InventoryOverview := { + lemmas := ← getTiles .Lemma + tactics := ← getTiles .Tactic + definitions := ← getTiles .Definition + lemmaTab := none + } + IO.FS.writeFile (path / inventoryFileName) (toString (toJson inventory)) - IO.FS.writeFile (path / s!"inventory.json") (toString (toJson inventory)) +open GameData in +def loadGameData (gameDir : System.FilePath) : IO Game := do + let path := gameDir / gameDataPath + let str ← IO.FS.readFile (path / gameFileName) + let json ← match Json.parse str with + | .ok v => pure v + | .error e => throw (IO.userError e) + let data ← match fromJson? json with + | .ok v => pure v + | .error e => throw (IO.userError e) + return data