json api

server/GameServer/Commands.lean

@@ -644,6 +644,44 @@ elab "Template" tacs:tacticSeq : tactic => do
 
 /-! # Make Game -/
 
+#eval IO.FS.createDirAll ".lake/gamedata/"
+
+-- TODO: register all of this as ToJson instance?
+def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : CommandElabM Unit:= do
+  let game ← getCurGame
+  let env ← getEnv
+  let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata"
+
+  if ← path.isDir then
+    IO.FS.removeDirAll path
+  IO.FS.createDirAll path
+
+  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 / s!"game.json") (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))
+
+  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 / s!"inventory.json") (toString (toJson inventory))
+
+
 def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo
 | .Tactic => level.tactics
 | .Definition => level.definitions
@@ -923,6 +961,7 @@ elab "MakeGame" : command => do
   -- Apparently we need to reload `game` to get the changes to `game.worlds` we just made
   let game ← getCurGame
 
+  let mut allItemsByType : HashMap InventoryType (HashSet Name) := {}
   -- Compute which inventory items are available in which level:
   for inventoryType in #[.Tactic, .Definition, .Lemma] do
 
@@ -1052,6 +1091,9 @@ elab "MakeGame" : command => do
 
         modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
           return level.setComputedInventory inventoryType itemsArray
+    allItemsByType := allItemsByType.insert inventoryType allItems
+
+  saveGameData allItemsByType
 
 /-! # Debugging tools -/
 

server/GameServer/EnvExtensions.lean

@@ -108,6 +108,12 @@ structure InventoryTile where
   hidden := false
 deriving ToJson, FromJson, Repr, Inhabited
 
+def InventoryItem.toTile (item : InventoryItem) : InventoryTile := {
+      name := item.name,
+      displayName := item.displayName
+      category := item.category
+}
+
 /-- The extension that stores the doc templates. Note that you can only add, but never modify
 entries! -/
 initialize inventoryTemplateExt :
@@ -135,7 +141,12 @@ def getInventoryItem? [Monad m] [MonadEnv m] (n : Name) (type : InventoryType) :
     m (Option InventoryItem) := do
   return (inventoryExt.getState (← getEnv)).find? (fun x => x.name == n && x.type == type)
 
-
+structure InventoryOverview where
+  tactics : Array InventoryTile
+  lemmas : Array InventoryTile
+  definitions : Array InventoryTile
+  lemmaTab : Option String
+deriving ToJson, FromJson
 
 /-! ## Environment extensions for game specification -/
 
@@ -256,6 +267,55 @@ structure GameLevel where
   template: Option String := none
   deriving Inhabited, Repr
 
+/-- Json-encodable version of `GameLevel`
+Fields:
+- description: Lemma in mathematical language.
+- descriptionGoal: Lemma printed as Lean-Code.
+-/
+structure LevelInfo where
+  index : Nat
+  title : String
+  tactics : Array InventoryTile
+  lemmas : Array InventoryTile
+  definitions : Array InventoryTile
+  introduction : String
+  conclusion : String
+  descrText : Option String := none
+  descrFormat : String := ""
+  lemmaTab : Option String
+  displayName : Option String
+  statementName : Option String
+  template : Option String
+deriving ToJson, FromJson
+
+def GameLevel.toInfo (lvl : GameLevel) (env : Environment) : LevelInfo :=
+  { index := lvl.index,
+    title := lvl.title,
+    tactics := lvl.tactics.tiles,
+    lemmas := lvl.lemmas.tiles,
+    definitions := lvl.definitions.tiles,
+    descrText := lvl.descrText,
+    descrFormat := lvl.descrFormat --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO
+    introduction := lvl.introduction
+    conclusion := lvl.conclusion
+    lemmaTab := match lvl.lemmaTab with
+    | some tab => tab
+    | none =>
+      -- Try to set the lemma tab to the category of the first added lemma
+      match lvl.lemmas.tiles.find? (·.new) with
+      | some tile => tile.category
+      | none => none
+    statementName := lvl.statementName.toString
+    displayName := match lvl.statementName with
+      | .anonymous => none
+      | name => match (inventoryExt.getState env).find?
+          (fun x => x.name == name && x.type == .Lemma) with
+        | some n => n.displayName
+        | none => name.toString
+        -- Note: we could call `.find!` because we check in `Statement` that the
+        -- lemma doc must exist.
+    template := lvl.template
+  }
 
 /-! ## World -/
 
@@ -298,6 +358,13 @@ structure Game where
   worlds : Graph Name World := default
 deriving Inhabited, ToJson
 
+def getGameJson (game : «Game») : Json := Id.run do
+  let gameJson : Json := toJson game
+  -- Add world sizes to Json object
+  let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size))
+  let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)])
+  return gameJson
+
 /-! ## Game environment extension -/
 
 def HashMap.merge [BEq α] [Hashable α] (old : HashMap α β) (new : HashMap α β) (merge : β → β → β) :

server/GameServer/Game.lean

@@ -25,53 +25,6 @@ open Lsp
 open JsonRpc
 open IO
 
-def getGame (game : Name): GameServerM Json := do
-  let some game ← getGame? game
-    | throwServerError "Game not found"
-  let gameJson : Json := toJson game
-  -- Add world sizes to Json object
-  let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size))
-  let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)])
-  return gameJson
-
-/--
-Fields:
-- description: Lemma in mathematical language.
-- descriptionGoal: Lemma printed as Lean-Code.
--/
-structure LevelInfo where
-  index : Nat
-  title : String
-  tactics : Array InventoryTile
-  lemmas : Array InventoryTile
-  definitions : Array InventoryTile
-  introduction : String
-  conclusion : String
-  descrText : Option String := none
-  descrFormat : String := ""
-  lemmaTab : Option String
-  displayName : Option String
-  statementName : Option String
-  template : Option String
-deriving ToJson, FromJson
-
-structure InventoryOverview where
-  tactics : Array InventoryTile
-  lemmas : Array InventoryTile
-  definitions : Array InventoryTile
-  lemmaTab : Option String
-deriving ToJson, FromJson
-
-structure LoadLevelParams where
-  world : Name
-  level : Nat
-  deriving ToJson, FromJson
-
--- structure LoadTemplateParams where
---   world : Name
---   level : Nat
---   deriving ToJson, FromJson
-
 structure DidOpenLevelParams where
   uri : String
   gameDir : String
@@ -91,11 +44,6 @@ structure DidOpenLevelParams where
   statementName : Name
   deriving ToJson, FromJson
 
-structure LoadDocParams where
-  name : Name
-  type : InventoryType
-deriving ToJson, FromJson
-
 structure SetInventoryParams where
   inventory : Array String
   difficulty : Nat
@@ -131,86 +79,10 @@ def handleDidOpenLevel (params : Json) : GameServerM Unit := do
     }
   }
 
-
 partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
   match ev with
   | ServerEvent.clientMsg msg =>
     match msg with
-    | Message.request id "info" _ =>
-      let s ← get
-      let c ← read
-      c.hOut.writeLspResponse ⟨id, (← getGame s.game)⟩
-      return true
-    | Message.request id "loadLevel" params =>
-      let p ← parseParams LoadLevelParams (toJson params)
-      let s ← get
-      let c ← read
-      let some lvl ← getLevel? {game := s.game, world := p.world, level := p.level}
-        | do
-          c.hOut.writeLspResponseError ⟨id, .invalidParams, s!"Level not found: world {p.world}, level {p.level}", none⟩
-          return true
-
-      let env ← getEnv
-
-      let levelInfo : LevelInfo :=
-          { index := lvl.index,
-            title := lvl.title,
-            tactics := lvl.tactics.tiles,
-            lemmas := lvl.lemmas.tiles,
-            definitions := lvl.definitions.tiles,
-            descrText := lvl.descrText,
-            descrFormat := lvl.descrFormat --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO
-            introduction := lvl.introduction
-            conclusion := lvl.conclusion
-            lemmaTab := match lvl.lemmaTab with
-            | some tab => tab
-            | none =>
-              -- Try to set the lemma tab to the category of the first added lemma
-              match lvl.lemmas.tiles.find? (·.new) with
-              | some tile => tile.category
-              | none => none
-            statementName := lvl.statementName.toString
-            displayName := match lvl.statementName with
-              | .anonymous => none
-              | name => match (inventoryExt.getState env).find?
-                  (fun x => x.name == name && x.type == .Lemma) with
-                | some n => n.displayName
-                | none => name.toString
-                -- Note: we could call `.find!` because we check in `Statement` that the
-                -- lemma doc must exist.
-            template := lvl.template
-            }
-      c.hOut.writeLspResponse ⟨id, ToJson.toJson levelInfo⟩
-      return true
-    -- | Message.request id "loadTemplate" params =>
-    --   let p ← parseParams LoadTemplateParams (toJson params)
-    --   let s ← get
-    --   let c ← read
-
-    --   let some game ← getGame? s.game
-    --     | throwServerError "Game not found"
-    --   let some world := game.worlds.nodes.find? p.world
-    --     | throwServerError "World not found"
-
-    --   let mut templates : Array <| Option String := #[]
-    --   for (_, level) in world.levels.toArray do
-    --     templates := templates.push level.template
-    --   c.hOut.writeLspResponse ⟨id, ToJson.toJson templates⟩
-    --   return true
-    | Message.request id "loadDoc" params =>
-      let p ← parseParams LoadDocParams (toJson params)
-      let c ← read
-      let some doc ← getInventoryItem? p.name p.type
-        | do
-            c.hOut.writeLspResponseError ⟨id, .invalidParams,
-              s!"Documentation not found: {p.name}", none⟩
-            return true
-      -- TODO: not necessary at all?
-      -- Here we only need to convert the fields that were not `String` in the `InventoryDocEntry`
-      -- let doc : InventoryItem := { doc with
-      --   name := doc.name.toString }
-      c.hOut.writeLspResponse ⟨id, ToJson.toJson doc⟩
-      return true
     | Message.notification "$/game/setInventory" params =>
       let p := (← parseParams SetInventoryParams (toJson params))
       let s ← get
@@ -221,30 +93,6 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
         fw.stdin.writeLspMessage msg
 
       return true
-    | Message.request id "loadInventoryOverview" _ =>
-      let s ← get
-      let some game ← getGame? s.game
-        | return false
-      -- All Levels have the same tiles, so we just load them from level 1 of an arbitrary world
-      -- and reset `new`, `disabled` and `unlocked`.
-      -- Note: as we allow worlds without any levels (for developing), we might need
-      -- to try until we find the first world with levels.
-      for ⟨worldId, _⟩ in game.worlds.nodes.toList do
-        let some lvl ← getLevel? {game := s.game, world := worldId, level := 1}
-          | do continue
-        let inventory : InventoryOverview := {
-          tactics := lvl.tactics.tiles.map
-            ({ · with locked := true, disabled := false, new := false }),
-          lemmas := lvl.lemmas.tiles.map
-            ({ · with locked := true, disabled := false, new := false }),
-          definitions := lvl.definitions.tiles.map
-            ({ · with locked := true, disabled := false, new := false }),
-          lemmaTab := none
-        }
-        let c ← read
-        c.hOut.writeLspResponse ⟨id, ToJson.toJson inventory⟩
-        return true
-      return false
     | _ => return false
   | _ => return false
 

server/index.mjs

@@ -34,6 +34,32 @@ var router = express.Router();
 router.get('/import/status/:owner/:repo', importStatus)
 router.get('/import/trigger/:owner/:repo', importTrigger)
 
+function loadJson(req, filename) {
+  const owner = req.params.owner;
+  const repo = req.params.repo
+  return JSON.parse(fs.readFileSync(path.join(getGameDir(owner,repo),".lake","gamedata",filename)))
+}
+
+router.get("/api/g/:owner/:repo/game", (req, res) => {
+  res.send(loadJson(req, `game.json`));
+});
+
+router.get("/api/g/:owner/:repo/inventory", (req, res) => {
+  res.send(loadJson(req, `inventory.json`));
+});
+
+router.get("/api/g/:owner/:repo/level/:world/:level", (req, res) => {
+  const world = req.params.world;
+  const level = req.params.level;
+  res.send(loadJson(req, `level__${world}__${level}.json`));
+});
+
+router.get("/api/g/:owner/:repo/doc/:type/:name", (req, res) => {
+  const type = req.params.type;
+  const name = req.params.name;
+  res.send(loadJson(req, `doc__${type}__${name}.json`));
+});
+
 const server = app
   .use(express.static(path.join(__dirname, '../client/dist/')))
   .use('/', router)
@@ -53,7 +79,7 @@ function getTag(owner, repo) {
   return `g/${owner.toLowerCase()}/${repo.toLowerCase()}`
 }
 
-function startServerProcess(owner, repo) {
+function getGameDir(owner, repo) {
   owner = owner.toLowerCase()
   if (owner == 'local') {
     if(!isDevelopment) {
@@ -77,6 +103,14 @@ function startServerProcess(owner, repo) {
     return
   }
 
+  return game_dir;
+}
+
+function startServerProcess(owner, repo) {
+
+  let game_dir = getGameDir(owner, repo)
+  if (!game_dir) return;
+
   let serverProcess
   if (isDevelopment) {
     let args = ["--server", game_dir]