add worlds

client/src/components/Level.tsx

@@ -114,7 +114,7 @@ function Level({ leanClient, nbLevels, level, setCurLevel, setLevelTitle, setFin
       // setInfoProvider(infoProvider)
       // setInfoviewApi(infoviewApi)
 
-      leanClient.sendRequest("loadLevel", {number: level}).then((res) => {
+      leanClient.sendRequest("loadLevel", {world: "TestWorld", level}).then((res) => {
         setLevelTitle("Level " + res["index"] + ": " + res["title"])
         setIndex(parseInt(res["index"]))
         setTacticDocs(res["tactics"])

client/src/components/Welcome.tsx

@@ -34,7 +34,8 @@ function Welcome({ leanClient, setNbLevels, setTitle, startGame, setConclusion }
 
     const getInfo = async () => {
       await leanClient.start() // TODO: need a way to wait for start without restarting
-      leanClient.sendRequest("info", "hello").then((res: infoResultType) =>{
+      leanClient.sendRequest("info", {}).then((res: infoResultType) =>{
+        console.log(res)
         setLeanData(res)
         setNbLevels(res.nb_levels)
         setTitle(res.title)

server/leanserver/GameServer/Commands.lean

@@ -15,64 +15,64 @@ open Lean Meta Elab Command Term
 
 /-- Create a game with the given identifier as name. -/
 elab "Game" n:str : command => do
-  gameExt.set {name := n.getString}
+  let name := n.getString
+  setCurGameId name
+  if (← getGame? name).isNone then
+    insertGame name {name}
+
+/-- Create a World -/
+elab "World" n:str : command => do
+  let name := n.getString
+  setCurWorldId name
+  if ¬ (← getCurGame).worlds.nodes.contains name then
+    addWorld {name}
 
 /-- Define the current level number. -/
-elab "Level" n:num : command => do
-  let idx := n.getNat
-  setCurLevelIdx idx
-  levelsExt.insert idx {index := idx}
+elab "Level" level:num : command => do
+  let level := level.getNat
+  setCurLevelIdx level
+  addLevel {index := level}
 
-/-- Define the title of the current game or current level if some
-building a level. -/
+/-- Define the title of the current game/world/level. -/
 elab "Title" t:str : command => do
-  let lvlIdx ← getCurLevelIdx
-  if lvlIdx > 0 then
-    let some lvl := (← levelsExt.find? lvlIdx) | throwError "Unable to find level"
-    levelsExt.update lvlIdx {lvl with title := t.getString}
-  else
-    gameExt.set {← gameExt.get with title := t.getString}
+  match ← getCurLayer with
+  | .Level => modifyCurLevel fun level => pure {level with title := t.getString}
+  | .World => modifyCurWorld  fun world => pure {world with title := t.getString}
+  | .Game => modifyCurGame  fun game => pure {game with title := t.getString}
 
-/-- Define the introduction of the current game or current level if some
-building a level. -/
+/-- Define the introduction of the current game/world/level. -/
 elab "Introduction" t:str : command => do
-  let lvlIdx ← getCurLevelIdx
-  if lvlIdx > 0 then
-    let some lvl := (← levelsExt.find? lvlIdx) | throwError "Unable to find level"
-    levelsExt.update lvlIdx {lvl with introduction := t.getString}
-  else
-    gameExt.set {← gameExt.get with introduction := t.getString}
+  match ← getCurLayer with
+  | .Level => modifyCurLevel fun level => pure {level with introduction := t.getString}
+  | .World => modifyCurWorld  fun world => pure {world with introduction := t.getString}
+  | .Game => modifyCurGame  fun game => pure {game with introduction := t.getString}
 
 /-- Define the statement of the current level. -/
 elab "Statement" sig:declSig val:declVal : command => do
   let lvlIdx ← getCurLevelIdx
-  let declName : Name := (← gameExt.get).name ++ ("level" ++ toString lvlIdx : String)
+  let declName : Name := (← getCurGame).name ++ (← getCurWorld).name ++ ("level" ++ toString lvlIdx : String)
   elabCommand (← `(theorem $(mkIdent declName) $sig $val))
-  levelsExt.update lvlIdx {← getCurLevel with goal := sig}
-  
+  modifyCurLevel fun level => pure {level with goal := sig}
+
 /-- Define the conclusion of the current game or current level if some
 building a level. -/
 elab "Conclusion" t:str : command => do
-  let lvlIdx ← getCurLevelIdx
-  if lvlIdx > 0 then
-    let some lvl := (← levelsExt.find? lvlIdx) | throwError "Unable to find level"
-    levelsExt.update lvlIdx {lvl with conclusion := t.getString}
-  else
-    gameExt.set {← gameExt.get with conclusion := t.getString}
+  match ← getCurLayer with
+  | .Level => modifyCurLevel fun level => pure {level with conclusion := t.getString}
+  | .World => modifyCurWorld  fun world => pure {world with conclusion := t.getString}
+  | .Game => modifyCurGame  fun game => pure {game with conclusion := t.getString}
 
-/-- Print current game for debugging purposes. -/
-elab "PrintCurGame" : command => do
-  logInfo (repr (← gameExt.get))
+-- /-- Print current game for debugging purposes. -/
+-- elab "PrintCurGame" : command => do
+--   logInfo (toJson (← getCurGame))
 
 /-- Print current level for debugging purposes. -/
 elab "PrintCurLevel" : command => do
-  match ← levelsExt.find? (← getCurLevelIdx) with
-  | some lvl => logInfo (repr lvl)
-  | none => logInfo "Could not find level"
+  logInfo (repr (← getCurLevel))
 
-/-- Print levels for debugging purposes. -/
+-- /-- Print levels for debugging purposes. -/
 elab "PrintLevels" : command => do
-  logInfo $ repr $ (levelsExt.getState (← getEnv)).toList.map (·.fst)
+  logInfo $ repr $ (← getCurWorld).levels.toArray
 
 end metadata
 
@@ -93,7 +93,7 @@ def getType : TSyntax `mydecl → Term
 
 /-- From a term `s` and a list of pairs `(i, t) ; Ident × Term`, create the syntax
 where `s` is preceded with universal quantifiers `∀ i : t`. -/
-def mkGoalSyntax (s : Term) : List (Ident × Term) → MacroM Term 
+def mkGoalSyntax (s : Term) : List (Ident × Term) → MacroM Term
 | (n, t)::tail => do return (← `(∀ $n : $t, $(← mkGoalSyntax s tail)))
 | [] => return s
 
@@ -103,12 +103,10 @@ local elab "Message'" decls:mydecl* ":" goal:term "=>" msg:str : command => do
   let g ← liftTermElabM do (return ← instantiateMVars (← elabTerm g none))
   let (ctx_size, normalized_goal) ← liftTermElabM do
     let msg_mvar ← mkFreshExprMVar g MetavarKind.syntheticOpaque
-    msg_mvar.mvarId!.withContext do 
+    msg_mvar.mvarId!.withContext do
       let (_, msg_mvar) ← msg_mvar.mvarId!.introNP decls.size
       return ((← msg_mvar.getDecl).lctx.size,  (← normalizedRevertExpr msg_mvar))
-  let lvlIdx ← getCurLevelIdx
-  let lvl ← getCurLevel
-  levelsExt.update lvlIdx {lvl with messages := lvl.messages.push {
+  modifyCurLevel fun level => pure {level with messages := level.messages.push {
     ctx_size := ctx_size,
     normalized_goal := normalized_goal,
     intro_nb := decls.size,
@@ -123,12 +121,12 @@ macro "Message" decls:mydecl* ":" goal:term "=>" msg:str : command => do
 
 /-- Declare a documentation entry for some tactic.
 Expect an identifier and then a string literal. -/
-elab "TacticDoc" name:ident content:str : command => 
+elab "TacticDoc" name:ident content:str : command =>
   modifyEnv (tacticDocExt.addEntry · {
-    name := name.getId, 
+    name := name.getId,
     content := content.getString })
 
-/-- Declare a set of tactic documentation entries. 
+/-- Declare a set of tactic documentation entries.
 Expect an identifier used as the set name then `:=` and a
 space separated list of identifiers.
 -/
@@ -141,13 +139,13 @@ elab "TacticSet" name:ident ":=" args:ident* : command => do
     | some doc => entries := entries.push doc
     | none => throwError "Documentation for tactic {name} wasn't found."
   modifyEnv (tacticSetExt.addEntry · {
-    name := name.getId, 
+    name := name.getId,
     tactics := entries })
 
 instance : Quote TacticDocEntry `term :=
 ⟨λ entry => Syntax.mkCApp ``TacticDocEntry.mk #[quote entry.name, quote entry.content]⟩
 
-/-- Declare the list of tactics that will be displayed in the current level. 
+/-- Declare the list of tactics that will be displayed in the current level.
 Expects a space separated list of identifiers that refer to either a tactic doc
 entry or a tactic doc set. -/
 elab "Tactics" args:ident* : command => do
@@ -162,12 +160,7 @@ elab "Tactics" args:ident* : command => do
     | none => match sets.find? (·.name = name) with
               | some entry => tactics := tactics ++ entry.tactics
               | none => throwError "Tactic doc or tactic set {name} wasn't found."
-  let lvlIdx ← getCurLevelIdx
-  if lvlIdx > 0 then
-    let some lvl := (← levelsExt.find? lvlIdx) | throwError "Unable to find level"
-    levelsExt.update lvlIdx {lvl with tactics := tactics}
-  else
-    throwError "This command can be used only while building a level."
+  modifyCurLevel fun level => pure {level with tactics := tactics}
 
 /-! ## Lemmas -/
 
@@ -175,14 +168,14 @@ elab "Tactics" args:ident* : command => do
 Expect two identifiers and then a string literal. The first identifier is meant
 as the real name of the lemma while the second is the displayed name. Currently
 the real name isn't used. -/
-elab "LemmaDoc" name:ident "as" userName:ident "in" category:str content:str : command => 
+elab "LemmaDoc" name:ident "as" userName:ident "in" category:str content:str : command =>
   modifyEnv (lemmaDocExt.addEntry · {
-    name := name.getId, 
+    name := name.getId,
     userName := userName.getId,
     category := category.getString,
     content := content.getString })
 
-/-- Declare a set of lemma documentation entries. 
+/-- Declare a set of lemma documentation entries.
 Expect an identifier used as the set name then `:=` and a
 space separated list of identifiers. -/
 elab "LemmaSet" name:ident ":" title:str ":=" args:ident* : command => do
@@ -201,7 +194,7 @@ elab "LemmaSet" name:ident ":" title:str ":=" args:ident* : command => do
 instance : Quote LemmaDocEntry `term :=
 ⟨λ entry => Syntax.mkCApp ``LemmaDocEntry.mk #[quote entry.name, quote entry.userName, quote entry.category, quote entry.content]⟩
 
-/-- Declare the list of lemmas that will be displayed in the current level. 
+/-- Declare the list of lemmas that will be displayed in the current level.
 Expects a space separated list of identifiers that refer to either a lemma doc
 entry or a lemma doc set. -/
 elab "Lemmas" args:ident* : command => do
@@ -216,9 +209,4 @@ elab "Lemmas" args:ident* : command => do
     | none => match sets.find? (·.name = name) with
               | some entry => lemmas := lemmas ++ entry.lemmas
               | none => throwError "Lemma doc or lemma set {name} wasn't found."
-  let lvlIdx ← getCurLevelIdx
-  if lvlIdx > 0 then
-    let some lvl := (← levelsExt.find? lvlIdx) | throwError "Unable to find level"
-    levelsExt.update lvlIdx {lvl with lemmas := lemmas}
-  else
-    throwError "This command can be used only while building a level."
+  modifyCurLevel fun level => pure {level with lemmas := lemmas}

server/leanserver/GameServer/Communication.lean

@@ -1,98 +0,0 @@
-/- Inspired by `Lean/Data/Lsp/Communication.lean` -/
-import Lean.Data.JsonRpc
-
-/-! Reading/writing Game Server Protocol messages from/to IO handles. -/
-
-namespace IO.FS.Stream
-
-open Lean
-open Lean.JsonRpc
-
-section
-
-def readJsonLine (h : FS.Stream) : IO Json := do
-  let s ← h.getLine
-  ofExcept (Json.parse s)
-
-def readGspMessage (h : FS.Stream) : IO Message := do
-  let j ← h.readJsonLine
-  match fromJson? j with
-  | Except.ok m => pure m
-  | Except.error inner =>
-    throw $
-      userError s!"JSON '{j.compress}' did not have the format of a JSON-RPC message.\n{inner}"
-
-def readGspRequestAs (h : FS.Stream) (expectedMethod : String) (α) [FromJson α]
-    : IO (Request α) := do
-  let m ← h.readGspMessage
-  match m with
-  | Message.request id method params? =>
-    if method = expectedMethod then
-      let j := toJson params?
-      match fromJson? j with
-      | Except.ok v => pure ⟨id, expectedMethod, v⟩
-      | Except.error inner =>
-        throw $
-          userError s!"Unexpected param '{j.compress}' for method '{expectedMethod}'\n{inner}"
-    else
-      throw $ userError s!"Expected method '{expectedMethod}', got method '{method}'"
-  | _ => throw $ userError s!"Expected JSON-RPC request, got: '{(toJson m).compress}'"
-
-def readGspNotificationAs
-    (h : FS.Stream) (nBytes : Nat) (expectedMethod : String) (α) [FromJson α]
-    : IO (Notification α) := do
-  let m ← h.readMessage nBytes
-  match m with
-  | Message.notification method params? =>
-    if method = expectedMethod then
-      let j := toJson params?
-      match fromJson? j with
-      | Except.ok v => pure ⟨expectedMethod, v⟩
-      | Except.error inner =>
-        throw $
-          userError s!"Unexpected param '{j.compress}' for method '{expectedMethod}'\n{inner}"
-    else
-      throw $ userError s!"Expected method '{expectedMethod}', got method '{method}'"
-  | _ => throw $ userError s!"Expected JSON-RPC notification, got: '{(toJson m).compress}'"
-
-def readGspResponseAs
-    (h : FS.Stream) (nBytes : Nat) (expectedID : RequestID) (α) [FromJson α]
-    : IO (Response α) := do
-  let m ← h.readMessage nBytes
-  match m with
-  | Message.response id result =>
-    if id == expectedID then
-      match fromJson? result with
-      | Except.ok v => pure ⟨expectedID, v⟩
-      | Except.error inner => throw $ userError s!"Unexpected result '{result.compress}'\n{inner}"
-    else
-      throw $ userError s!"Expected id {expectedID}, got id {id}"
-  | Message.notification .. => readResponseAs h nBytes expectedID α
-  | _ => throw $ userError s!"Expected JSON-RPC response, got: '{(toJson m).compress}'"
-
-end
-
-section
-  variable [ToJson α]
-
-  def writeGspMessage (h : FS.Stream) (m : Message) : IO Unit := do
-    h.putStr ((toJson m).compress ++ "\n")
-    h.flush
-
-  def writeGspRequest (h : FS.Stream) (r : Request α) : IO Unit :=
-    h.writeGspMessage r
-
-  def writeGspNotification (h : FS.Stream) (n : Notification α) : IO Unit :=
-    h.writeGspMessage n
-
-  def writeGspResponse (h : FS.Stream) (r : Response α) : IO Unit :=
-    h.writeGspMessage r
-
-  def writeGspResponseError (h : FS.Stream) (e : ResponseError Unit) : IO Unit :=
-    h.writeGspMessage (Message.responseError e.id e.code e.message none)
-
-  def writeGspResponseErrorWithData (h : FS.Stream) (e : ResponseError α) : IO Unit :=
-    h.writeGspMessage e
-end
-
-end IO.FS.Stream

server/leanserver/GameServer/EnvExtensions.lean

@@ -1,11 +1,8 @@
-import GameServer.HashMapExtension
-import GameServer.SingleValPersistentEnvExtension
-
+import Lean
 /-! # Environment extensions
 
 The game framework stores almost all its game building data in environment extensions
-defined in this file. MAyn of them are `SimplePersistentEnvExtension` but we also
-use `HashMapExtension` and `SingleValPersistentEnvExtension`
+defined in this file.
 -/
 
 
@@ -103,31 +100,80 @@ elab "#print_lemma_set" : command => do
   for entry in lemmaSetExt.getState (← getEnv) do
     dbg_trace "{entry.name} : {entry.lemmas.map LemmaDocEntry.name}"
 
-/-! ## Game -/
+/-! ## Graph -/
 
-structure Game where
-  name : Name
-  title : String := ""
-  introduction : String := ""
-  conclusion : String := ""
-  authors : List String := []
-  nb_levels : Nat := 0
-  deriving Repr, Inhabited, ToJson
+structure Graph (α β : Type) [inst : BEq α] [inst : Hashable α] where
+  nodes: HashMap α β := {}
+  edges: Array (α × α) := {}
+deriving Inhabited
 
-initialize gameExt : SingleValPersistentEnvExtension Game ← registerSingleValPersistentEnvExtension `gameExt Game
+instance [inst : BEq α] [inst : Hashable α] [ToJson α] : ToJson (Graph α β) := {
+  toJson := fun graph => Json.mkObj [
+    ("nodes", toJson (graph.nodes.toArray.map Prod.fst)),
+    ("edges", toJson graph.edges)
+  ]
+}
 
-/-! ## Levels -/
+instance [inst : BEq α] [inst : Hashable α] : EmptyCollection (Graph α β) := ⟨default⟩
+
+def Graph.insertNode [inst : BEq α] [inst : Hashable α] (g : Graph α β) (a : α) (b : β) :=
+  {g with nodes := g.nodes.insert a b}
 
-/- Register a (non-persistent) environment extension to hold the current level number. -/
-initialize curLevelExt : EnvExtension Nat ← registerEnvExtension (pure 0)
+/-! ## Environment extensions for game specification-/
+
+/-- Register a (non-persistent) environment extension to hold the current level -/
+initialize curGameExt : EnvExtension (Option Name) ← registerEnvExtension (pure none)
+/-- Register a (non-persistent) environment extension to hold the current level -/
+initialize curWorldExt : EnvExtension (Option Name) ← registerEnvExtension (pure none)
+/-- Register a (non-persistent) environment extension to hold the current level -/
+initialize curLevelExt : EnvExtension (Option Nat) ← registerEnvExtension (pure none)
+
+inductive Layer :=
+| Game | World | Level
 
 variable {m: Type → Type} [Monad m] [MonadEnv m]
 
-def setCurLevelIdx (lvl : Nat) :  m Unit :=
-  modifyEnv (curLevelExt.setState · lvl)
+def setCurGameId (game : Name) : m Unit :=
+  modifyEnv (curGameExt.setState · (some game))
+
+def setCurWorldId (world : Name) : m Unit :=
+  modifyEnv (curWorldExt.setState · (some world))
 
-def getCurLevelIdx :  m Nat := do
-  return curLevelExt.getState (← getEnv)
+def setCurLevelIdx (level : Nat) : m Unit :=
+  modifyEnv (curLevelExt.setState · (some level))
+
+def getCurLayer [MonadError m] : m Layer := do
+  match curGameExt.getState (← getEnv), curWorldExt.getState (← getEnv), curLevelExt.getState (← getEnv) with
+  | some _, some _, some _ => return Layer.Level
+  | some _, some _, none => return Layer.World
+  | some _, none, none => return Layer.Game
+  | _, _, _ => throwError "Invalid Layer"
+
+def getCurGameId [MonadError m] : m Name := do
+  match curGameExt.getState (← getEnv) with
+  | some game => return game
+  | none => throwError "Current game not set"
+
+def getCurWorldId [MonadError m] : m Name := do
+  match curWorldExt.getState (← getEnv) with
+  | some world => return world
+  | none => throwError "Current world not set"
+
+def getCurLevelIdx [MonadError m] : m Nat := do
+  match curLevelExt.getState (← getEnv) with
+  | some level => return level
+  | none => throwError "Current level not set"
+
+/-! ## Levels -/
+
+structure LevelId where
+  game : Name
+  world : Name
+  level : Nat
+deriving Inhabited
+
+def getCurLevelId [MonadError m] : m LevelId := do
+  return { game := ← getCurGameId, world := ← getCurWorldId, level := ← getCurLevelIdx}
 
 structure GameLevel where
   index: Nat
@@ -140,10 +186,117 @@ structure GameLevel where
   goal : TSyntax `Lean.Parser.Command.declSig := default
   deriving Inhabited, Repr
 
-initialize levelsExt : HashMapExtension Nat GameLevel ← mkHashMapExtension `levels Nat GameLevel
+/-! ## World -/
 
-def getCurLevel [MonadError m] :  m GameLevel := do
-  let idx ← getCurLevelIdx
-  match (← levelsExt.find? idx) with
-  | some level => return level
-  | none => throwError "Couldn't find level {idx}"
+structure World where
+  name: Name
+  title: String := ""
+  introduction: String := ""
+  conclusion : String := ""
+  levels: HashMap Nat GameLevel := {}
+deriving Inhabited
+
+/-! ## Game -/
+
+structure Game where
+  name : Name
+  title : String := ""
+  introduction : String := ""
+  conclusion : String := ""
+  authors : List String := []
+  worlds : Graph Name World := {}
+deriving Inhabited, ToJson
+
+/-! ## Game environment extension -/
+
+def HashMap.merge [BEq α] [Hashable α] (old : HashMap α β) (new : HashMap α β) (merge : β → β → β) :
+  HashMap α β :=
+new.fold (fun acc a b =>
+  if let some bOld := acc.find? a
+  then acc.insert a (merge bOld b)
+  else acc.insert a b) old
+
+def GameLevel.merge (old : GameLevel) (new : GameLevel) : GameLevel :=
+  new
+
+def World.merge (old : World) (new : World) : World :=
+{ new with
+  levels := HashMap.merge old.levels new.levels GameLevel.merge}
+
+def Game.merge (old : Game) (new : Game) : Game :=
+{ new with
+  worlds := {
+    nodes := HashMap.merge old.worlds.nodes new.worlds.nodes World.merge
+    edges := old.worlds.edges ++ new.worlds.edges
+  } }
+
+initialize gameExt : PersistentEnvExtension (Name × Game) (Name × Game) (HashMap Name Game) ←
+  do registerPersistentEnvExtension {
+    name          := `gameExt,
+    mkInitial     := pure {},
+    addImportedFn := fun ess => do
+      let mut games := {}
+      for es in ess do
+        for (name, game) in es do
+          match games.find? name with
+          | some oldgame =>
+            games := games.insert name (Game.merge oldgame game)
+          | none =>
+            games := games.insert name game
+      return games
+    addEntryFn    := (λ s n => s.insert n.1 n.2),
+    exportEntriesFn := HashMap.toArray,
+    statsFn := fun s => format "number of local entries: " ++ format s.size
+}
+
+def getGame? (n : Name) : m (Option Game) := do
+  return (gameExt.getState (← getEnv)).find? n
+
+def insertGame (n : Name) (g : Game) : m Unit := do
+  modifyEnv (gameExt.addEntry · (n, g))
+
+def getLevel? (levelId : LevelId) : m (Option GameLevel) := do
+  let some game ← getGame? levelId.game
+    | return none
+  let some world := game.worlds.nodes.find? levelId.world
+    | return none
+  let some level := world.levels.find? levelId.level
+    | return none
+  return level
+
+def getCurGame [MonadError m] : m Game := do
+  let some game ← getGame? (← getCurGameId)
+    | throwError m!"Game {← getCurGameId} does not exist"
+  return game
+
+def modifyCurGame (fn : Game → m Game) [MonadError m] : m Unit := do
+  let game ← getCurGame
+  insertGame game.name (← fn game)
+
+def addWorld (world : World) [MonadError m] : m Unit := do
+  modifyCurGame fun game => do
+    return {game with worlds := game.worlds.insertNode world.name world}
+
+def getCurWorld [MonadError m] : m World := do
+  let some world := (← getCurGame).worlds.nodes.find? (← getCurWorldId)
+    | throwError m!"World {← getCurWorldId} does not exist"
+  return world
+
+def modifyCurWorld (fn : World → m World) [MonadError m] : m Unit := do
+  modifyCurGame fun game => do
+    let world ← getCurWorld
+    return {game with worlds := {game.worlds with nodes := game.worlds.nodes.insert world.name (← fn world) }}
+
+def addLevel (level : GameLevel) [MonadError m] : m Unit := do
+  modifyCurWorld fun world => do
+    return {world with levels := world.levels.insert level.index level}
+
+def getCurLevel [MonadError m] : m GameLevel := do
+  let some level := (← getCurWorld).levels.find? (← getCurLevelIdx)
+    | throwError m!"Level {← getCurLevelIdx} does not exist"
+  return level
+
+def modifyCurLevel (fn : GameLevel → m GameLevel) [MonadError m] : m Unit := do
+  modifyCurWorld fun world => do
+    let level ← getCurLevel
+    return {world with levels := world.levels.insert level.index (← fn level)}

server/leanserver/GameServer/FileWorker.lean

@@ -96,12 +96,14 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
     let (output, _) ← IO.FS.withIsolatedStreams (isolateStderr := server.stderrAsMessages.get scope.opts) <| liftM (m := BaseIO) do
       Elab.Command.catchExceptions
         (getResetInfoTrees *> do
-          let levels := levelsExt.getState (← getEnv)
           let levelId ← levelIdFromFileName inputCtx.fileName
+          -- TODO: make world and game configurable
+          let some level ← getLevel? {game := `TestGame, world := `TestWorld, level := levelId}
+            | throwServerError "Level not found"
           let done := Syntax.node (.synthetic cmdParserState.pos cmdParserState.pos) ``Lean.Parser.Tactic.done #[]
           let tacticStx := (tacticStx.getArgs.push done).map (⟨.⟩)
           let tacticStx := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*)
-          let cmdStx ← `(command| theorem mythm $(levels[levelId].get!.goal) := by {$(⟨tacticStx⟩)} )
+          let cmdStx ← `(command| theorem my_theorem $(level.goal) := by {$(⟨tacticStx⟩)} )
           Elab.Command.elabCommandTopLevel cmdStx)
         cmdCtx cmdStateRef
     let postNew := (← tacticCacheNew.get).post

server/leanserver/GameServer/Game.lean

@@ -6,6 +6,7 @@ open Lean
 
 structure GameServerState :=
 (env : Lean.Environment)
+(game : Name)
 
 abbrev GameServerM := StateT GameServerState Server.Watchdog.ServerM
 
@@ -23,6 +24,11 @@ open Lsp
 open JsonRpc
 open IO
 
+def getGame (game : Name): GameServerM Game := do
+  let some game ← getGame? game
+    | throwServerError "Game not found"
+  return game
+
 structure LevelInfo where
   index : Nat
   title : String
@@ -32,7 +38,8 @@ structure LevelInfo where
 deriving ToJson
 
 structure LoadLevelParams where
-  number : Nat
+  world : Name
+  level : Nat
   deriving ToJson, FromJson
 
 partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
@@ -42,17 +49,14 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
     | Message.request id "info" _ =>
       let s ← get
       let c ← read
-      let levels := levelsExt.getState s.env
-      let game := {← gameExt.get with nb_levels := levels.size }
-      c.hOut.writeLspResponse ⟨id, game⟩
+      c.hOut.writeLspResponse ⟨id, (← getGame s.game)⟩
       return true
     | Message.request id "loadLevel" params =>
       let p ← parseParams LoadLevelParams (toJson params)
-      let idx := p.number
       let s ← get
       let c ← read
-      let levels := levelsExt.getState s.env
-      let some lvl := levels.find? idx | throwServerError s!"Cannot find level {idx}"
+      let some lvl ← getLevel? {game := s.game, world := p.world, level := p.level}
+        | throwServerError s!"Level not found {(← getGame s.game).name} {p.world} {p.level}"
       let levelInfo : LevelInfo :=
           { index := lvl.index,
             title := lvl.title,

server/leanserver/GameServer/HashMapExtension.lean

@@ -1,31 +0,0 @@
-import Lean
-
-open Lean Std
-
-def HashMapExtension (α β : Type) [BEq α] [Hashable α] := SimplePersistentEnvExtension (α × β) (HashMap α β)
-
-instance (α β : Type) [BEq α] [Hashable α] : Inhabited (HashMapExtension α β) :=
-  inferInstanceAs (Inhabited (SimplePersistentEnvExtension (α × β) (HashMap α β)))
-
-def mkHashMapExtension (name : Name) (α β : Type) [BEq α] [Hashable α]  : IO (HashMapExtension α β) :=
-  registerSimplePersistentEnvExtension {
-    name          := name,
-    addImportedFn := mkStateFromImportedEntries (λ s n => s.insert n.1 n.2) {},
-    addEntryFn    := (λ s n => s.insert n.1 n.2),
-    toArrayFn     := fun es => es.toArray
-  }
-
-namespace HashMapExtension
-
-variable {α β : Type} [BEq α] [Hashable α] {m: Type → Type} [Monad m] [MonadEnv m]
-
-def find? (ext : HashMapExtension α β) (a : α) : m $ Option β := do
-  return (ext.getState (← getEnv)).find? a
-
-def insert (ext : HashMapExtension α β) (a : α) (b : β) : m Unit :=
-  modifyEnv (ext.addEntry · (a, b))
-
-def update (ext : HashMapExtension α β) (a : α) (b : β) : m Unit :=
-  modifyEnv (ext.addEntry · (a, b))
-
-end HashMapExtension

server/leanserver/GameServer/SingleValPersistentEnvExtension.lean

@@ -1,26 +0,0 @@
-import Lean
-
-open Lean
-
-/-- A persistent environment extension that is meant to hold a single (mutable) value. -/
-def SingleValPersistentEnvExtension (α : Type) := PersistentEnvExtension α α α 
-
-instance {α} [Inhabited α] : Inhabited (SingleValPersistentEnvExtension α) :=
-  inferInstanceAs <| Inhabited  <| PersistentEnvExtension α α α
-
-def registerSingleValPersistentEnvExtension (name : Name) (α : Type) [Inhabited α] : IO (SingleValPersistentEnvExtension α) := 
-  registerPersistentEnvExtension {
-    name            := name,
-    mkInitial       := pure default,
-    addImportedFn   := mkStateFromImportedEntries (fun _ b => return b) (return default),
-    addEntryFn      := (λ _ b => b),
-    exportEntriesFn := λ x => #[x]
-  }
-
-variable {m: Type → Type} [Monad m] [MonadEnv m] {α : Type} [Inhabited α] 
-
-def SingleValPersistentEnvExtension.get (ext : SingleValPersistentEnvExtension α) : m α :=
-  return ext.getState (← getEnv)
-
-def SingleValPersistentEnvExtension.set (ext : SingleValPersistentEnvExtension α) (a : α) : m Unit := do
-  modifyEnv (ext.modifyState · (λ _ => a))

server/leanserver/GameServer/Watchdog.lean

@@ -148,7 +148,7 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
       : InitializeResult
     }
   }
-  let state := {env := ← createEnv}
+  let state := {env := ← createEnv, game := `TestGame}
   let context : ServerContext := {
     hIn            := i
     hOut           := o

server/testgame/TestGame.lean

@@ -3,5 +3,4 @@ import TestGame.Levels.Level1
 import TestGame.Levels.Level2
 import TestGame.Levels.Level3
 import TestGame.Levels.Level4
-import TestGame.Levels.Level5
-
+import TestGame.Levels.Level5

server/testgame/TestGame/Levels/Level1.lean

@@ -1,5 +1,7 @@
 import TestGame.Metadata
 
+Game "TestGame"
+World "TestWorld"
 Level 1
 
 Title "The reflexivity spell"
@@ -23,4 +25,4 @@ rfl
 
 Conclusion "Congratulations for completing your first level! You can now click on the *Go to next level* button."
 
-Tactics rfl
+Tactics rfl

server/testgame/TestGame/Levels/Level2.lean

@@ -1,5 +1,7 @@
 import TestGame.Metadata
 
+Game "TestGame"
+World "TestWorld"
 Level 2
 
 Title "The rewriting spell"

server/testgame/TestGame/Levels/Level3.lean

@@ -1,5 +1,7 @@
 import TestGame.Metadata
 
+Game "TestGame"
+World "TestWorld"
 Level 3
 
 Title "Peano's axioms"

server/testgame/TestGame/Levels/Level4.lean

@@ -1,5 +1,7 @@
 import TestGame.Metadata
 
+Game "TestGame"
+World "TestWorld"
 Level 4
 
 Title "Addition"

server/testgame/TestGame/Levels/Level5.lean

@@ -1,6 +1,8 @@
 import TestGame.Metadata
 import TestGame.Tactics
 
+Game "TestGame"
+World "TestWorld"
 Level 5
 
 Title "The induction_on spell"