lemma inventory

server/leanserver/GameServer/Commands.lean

@@ -264,32 +264,50 @@ elab "MakeGame" : command => do
   if game.worlds.hasLoops then
     throwError "World graph has loops!"
 
-  -- Compute which tactics are available in which level:
+  -- Compute which tactics/lemmas are available in which level:
   let mut newTacticsInWorld : HashMap Name (HashSet Name) := {}
   let mut allTactics : HashSet Name := {}
+  let mut newLemmasInWorld : HashMap Name (HashSet Name) := {}
+  let mut allLemmas : HashSet Name := {}
   for (worldId, world) in game.worlds.nodes.toArray do
     let mut newTactics : HashSet Name:= {}
+    let mut newLemmas : HashSet Name:= {}
     for (_, level) in world.levels.toArray do
       newTactics := newTactics.insertMany level.newTactics
       allTactics := allTactics.insertMany level.newTactics
+      newLemmas := newLemmas.insertMany level.newLemmas
+      allLemmas := allLemmas.insertMany level.newLemmas
     newTacticsInWorld := newTacticsInWorld.insert worldId newTactics
+    newLemmasInWorld := newLemmasInWorld.insert worldId newLemmas
 
-  let tacticAvailability₀ : HashMap Name TacticAvailability :=
+  -- Basic tactic/lemma availability: all locked, none disabled.
+  let Availability₀ : HashMap Name Availability :=
     HashMap.ofList $
       allTactics.toList.map fun name =>
         (name, {name, locked := true, disabled := false})
+  let lemmaAvailability₀ : HashMap Name Availability :=
+    HashMap.ofList $
+      allLemmas.toList.map fun name =>
+        (name, {name, locked := true, disabled := false})
 
-  let mut tacticsInWorld : HashMap Name (HashMap Name TacticAvailability) := {}
+  -- Availability after a given world
+  let mut tacticsInWorld : HashMap Name (HashMap Name Availability) := {}
+  let mut lemmasInWorld : HashMap Name (HashMap Name Availability) := {}
   for (worldId, _) in game.worlds.nodes.toArray do
-    let mut tactics : HashMap Name TacticAvailability := tacticAvailability₀
+    let mut tactics := Availability₀
+    let mut lemmas := lemmaAvailability₀
     let predecessors := game.worlds.predecessors worldId
     for predWorldId in predecessors do
       for tac in newTacticsInWorld.find! predWorldId do
         tactics := tactics.insert tac {name := tac, locked := false, disabled := false}
+      for lem in newLemmasInWorld.find! predWorldId do
+        lemmas := lemmas.insert lem {name := lem, locked := false, disabled := false}
     tacticsInWorld := tacticsInWorld.insert worldId tactics
+    lemmasInWorld := lemmasInWorld.insert worldId lemmas
 
   for (worldId, world) in game.worlds.nodes.toArray do
     let mut tactics := tacticsInWorld.find! worldId
+    let mut lemmas := lemmasInWorld.find! worldId
 
     let levels := world.levels.toArray.insertionSort fun a b => a.1 < b.1
 
@@ -298,9 +316,20 @@ elab "MakeGame" : command => do
         tactics := tactics.insert tac {name := tac, locked := false, disabled := false}
       for tac in level.disabledTactics do
         tactics := tactics.insert tac {name := tac, locked := false, disabled := true}
+      for lem in level.newLemmas do
+        lemmas := lemmas.insert lem {name := lem, locked := false, disabled := false}
+      for lem in level.disabledLemmas do
+        lemmas := lemmas.insert lem {name := lem, locked := false, disabled := true}
 
       let tacticArray := tactics.toArray
         |>.insertionSort (fun a b => a.1.toString < b.1.toString)
         |>.map (·.2)
+
+      let lemmaArray := lemmas.toArray
+        |>.insertionSort (fun a b => a.1.toString < b.1.toString)
+        |>.map (·.2)
+
       modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
-        return {level with tactics := tacticArray}
+        return {level with
+          tactics := tacticArray
+          lemmas := lemmaArray}

server/leanserver/GameServer/EnvExtensions.lean

@@ -144,7 +144,7 @@ structure LevelId where
   level : Nat
 deriving Inhabited
 
-structure TacticAvailability where
+structure Availability where
   name : Name
   locked : Bool
   disabled : Bool
@@ -176,7 +176,7 @@ structure GameLevel where
   -- only these tactics are allowed in this level (ignore if empty):
   onlyTactics: Array Name := default
   -- tactics in this level (computed by `MakeGame`):
-  tactics: Array TacticAvailability := default
+  tactics: Array Availability := default
   -- new lemmas introduces by this level:
   newLemmas: Array Name := default
   -- lemmas exceptionally forbidden in this level:
@@ -184,7 +184,7 @@ structure GameLevel where
   -- only these lemmas are allowed in this level (ignore if empty):
   onlyLemmas: Array Name := default
   -- lemmas in this level (computed by `MakeGame`):
-  lemmas: Array LemmaDocEntry := default
+  lemmas: Array Availability := default
   hints: Array GoalHintEntry := default
   goal : TSyntax `Lean.Parser.Command.declSig := default
   descrText: String := default

server/leanserver/GameServer/Game.lean

@@ -41,8 +41,8 @@ Fields:
 structure LevelInfo where
   index : Nat
   title : String
-  tactics: Array TacticAvailability
-  lemmas: Array LemmaDocEntry
+  tactics: Array Availability
+  lemmas: Array Availability
   introduction : String
   descrText : String := ""
   descrFormat : String := ""