compute which tactics are available in which level

server/leanserver/GameServer/Commands.lean

@@ -190,16 +190,8 @@ instance : Quote TacticDocEntry `term :=
 /-- 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
-  let env ← getEnv
-  let docs := tacticDocExt.getState env
-  let mut tactics : Array TacticDocEntry := #[]
-  for arg in args do
-    let name := arg.getId
-    match docs.find? (·.name = name) with
-    | some entry => tactics := tactics.push entry
-    | none => throwError "Tactic doc {name} wasn't found."
-  modifyCurLevel fun level => pure {level with tactics := tactics}
+elab "NewTactics" args:ident* : command => do
+  modifyCurLevel fun level => pure {level with newTactics := args.map (·.getId)}
 
 /-! ## Lemmas -/
 
@@ -219,11 +211,11 @@ 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
   let docs := lemmaDocExt.getState (← getEnv)
-  let mut entries : Array LemmaDocEntry := #[]
+  let mut entries : Array Name := #[]
   for arg in args do
     let name := arg.getId
     match docs.find? (·.userName = name) with
-    | some doc => entries := entries.push doc
+    | some doc => entries := entries.push name
     | none => throwError "Lemma doc {name} wasn't found."
   modifyEnv (lemmaSetExt.addEntry · {
     name := name.getId,
@@ -236,16 +228,60 @@ instance : Quote LemmaDocEntry `term :=
 /-- 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
+elab "NewLemmas" args:ident* : command => do
   let env ← getEnv
   let docs := lemmaDocExt.getState env
   let sets := lemmaSetExt.getState env
-  let mut lemmas : Array LemmaDocEntry := #[]
+  let mut lemmas : Array Name := #[]
   for arg in args do
     let name := arg.getId
     match docs.find? (·.userName = name) with
-    | some entry => lemmas := lemmas.push entry
+    | some entry => lemmas := lemmas.push name
     | none => match sets.find? (·.name = name) with
               | some entry => lemmas := lemmas ++ entry.lemmas
               | none => throwError "Lemma doc or lemma set {name} wasn't found."
-  modifyCurLevel fun level => pure {level with lemmas := lemmas}
+  modifyCurLevel fun level => pure {level with newLemmas := lemmas}
+
+/-! ## Make Game -/
+
+def getTacticDoc! (tac : Name) : CommandElabM TacticDocEntry := do
+  match (tacticDocExt.getState (← getEnv)).find? (·.name = tac) with
+  | some doc => return doc
+  | none => throwError "Tactic documentation not found: {tac}"
+
+/-- Make the final Game. This command will precompute various things about the game, such as which
+tactics are available in each level etc. -/
+elab "MakeGame" : command => do
+  let game ← getCurGame
+
+  -- Check for loops in world graph
+  if game.worlds.hasLoops then
+    throwError "World graph has loops!"
+
+  -- Compute which tactics are available in which level:
+  let mut newTacticsInWorld : HashMap Name (HashSet Name) := {}
+  for (worldId, world) in game.worlds.nodes.toArray do
+    let mut newTactics : HashSet Name:= {}
+    for (_, level) in world.levels.toArray do
+      newTactics := newTactics.insertMany level.newTactics
+    newTacticsInWorld := newTacticsInWorld.insert worldId newTactics
+
+  let mut tacticsInWorld : HashMap Name (HashSet Name) := {}
+  for (worldId, _) in game.worlds.nodes.toArray do
+    let mut tactics : HashSet Name:= {}
+    let predecessors := game.worlds.predecessors worldId
+    for predWorldId in predecessors do
+      tactics := tactics.insertMany (newTacticsInWorld.find! predWorldId)
+    tacticsInWorld := tacticsInWorld.insert worldId tactics
+
+  for (worldId, world) in game.worlds.nodes.toArray do
+    let mut tactics := tacticsInWorld.find! worldId
+    logInfo m!"{tactics.toArray}"
+
+    let levels := world.levels.toArray.insertionSort fun a b => a.1 < b.1
+
+    for (levelId, level) in levels do
+      tactics := tactics.insertMany level.newTactics
+
+      modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
+        return {level with tactics := ← tactics.toArray.mapM getTacticDoc!}

server/leanserver/GameServer/EnvExtensions.lean

@@ -1,4 +1,6 @@
 import Lean
+import GameServer.Graph
+
 /-! # Environment extensions
 
 The game framework stores almost all its game building data in environment extensions
@@ -71,7 +73,7 @@ elab "#print_lemma_doc" : command => do
 structure LemmaSetEntry where
   name : Name
   title : String
-  lemmas : Array LemmaDocEntry
+  lemmas : Array Name
   deriving ToJson, Repr
 
 /-- Environment extension for lemma sets. -/
@@ -86,26 +88,8 @@ open Elab Command in
 /-- Print all registered lemma sets for debugging purposes. -/
 elab "#print_lemma_set" : command => do
   for entry in lemmaSetExt.getState (← getEnv) do
-    dbg_trace "{entry.name} : {entry.lemmas.map LemmaDocEntry.name}"
+    dbg_trace "{entry.name} : {entry.lemmas}"
 
-/-! ## Graph -/
-
-structure Graph (α β : Type) [inst : BEq α] [inst : Hashable α] where
-  nodes: HashMap α β := {}
-  edges: Array (α × α) := {}
-deriving Inhabited
-
-instance [ToJson β] : ToJson (Graph Name β) := {
-  toJson := fun graph => Json.mkObj [
-    ("nodes", Json.mkObj (graph.nodes.toList.map fun (a,b) => (a.toString, toJson b))),
-    ("edges", toJson graph.edges)
-  ]
-}
-
-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}
 
 /-! ## Environment extensions for game specification-/
 
@@ -179,7 +163,21 @@ structure GameLevel where
   introduction: String := default
   description: String := default
   conclusion: String := default
+  -- new tactics introduces by this level:
+  newTactics: Array Name := default
+  -- tactics exceptionally forbidden in this level:
+  disabledTactics: Array Name := default
+  -- only these tactics are allowed in this level (ignore if empty):
+  onlyTactics: Array Name := default
+  -- tactics in this level (computed by `MakeGame`):
   tactics: Array TacticDocEntry := default
+  -- new lemmas introduces by this level:
+  newLemmas: Array Name := default
+  -- lemmas exceptionally forbidden in this level:
+  disabledLemmas: Array Name := default
+  -- 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
   hints: Array GoalHintEntry := default
   goal : TSyntax `Lean.Parser.Command.declSig := default
@@ -310,3 +308,15 @@ def modifyCurLevel (fn : GameLevel → m GameLevel) [MonadError m] : m Unit := d
   modifyCurWorld fun world => do
     let level ← getCurLevel
     return {world with levels := world.levels.insert level.index (← fn level)}
+
+def modifyLevel (levelId : LevelId) (fn : GameLevel → m GameLevel) [MonadError m] : m Unit := do
+  let some game ← getGame? levelId.game
+    | throwError m!"Game {levelId.game} does not exist"
+  let some world := (← getCurGame).worlds.nodes.find? levelId.world
+    | throwError m!"World {levelId.world} does not exist"
+  let some level := world.levels.find? levelId.level
+    | throwError m!"Level {levelId.level} does not exist"
+  let level' ← fn level
+  let world' := {world with levels := world.levels.insert levelId.level level'}
+  let game' := {game with worlds := game.worlds.insertNode levelId.world world'}
+  insertGame levelId.game game'