From d753d1d87382c88adcd98b861e48ab501ec78ae8 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 19 May 2023 13:01:58 +0200
Subject: [PATCH 1/5] docstrings

---
 server/GameServer/EnvExtensions.lean | 30 +++++++++++++++++++---------
 1 file changed, 21 insertions(+), 9 deletions(-)

diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean
index 65b8a33..c4174cc 100644
--- a/server/GameServer/EnvExtensions.lean
+++ b/server/GameServer/EnvExtensions.lean
@@ -11,17 +11,15 @@ open Lean
 
 -- Note: When changing these, one also needs to change them in `index.mjs`
 
-/-! The default game name if `Game "MyGame"` is not used. -/
+/-- The default game name if `Game "MyGame"` is not used. -/
 def defaultGameName: String := "MyGame"
 
-/-! The default game module name. -/
+/-- The default game module name. -/
 def defaultGameModule: String := "Game"
 
 /-! ## Hints -/
 
-/--
-A hint to help the user with a specific goal state
--/
+/-- A hint to help the user with a specific goal state -/
 structure GoalHintEntry where
   goal : AbstractCtxResult
   /-- Text of the hint as an expression of type `Array Expr → MessageData` -/
@@ -37,6 +35,7 @@ instance : Repr GoalHintEntry := {
 
 /-! ## Tactic/Definition/Lemma documentation -/
 
+/-- The game knows three different inventory types that contain slightly different information -/
 inductive InventoryType := | Tactic | Lemma | Definition
 deriving ToJson, FromJson, Repr, BEq, Hashable, Inhabited
 
@@ -66,6 +65,7 @@ structure InventoryDocEntry where
   content : String
   deriving ToJson, Repr, Inhabited
 
+/-- Another reduced version of `InventoryDocEntry` which is used for the tiles in the doc -/
 structure ComputedInventoryItem where
   /--
   The name of the item. The restrictions are:
@@ -115,20 +115,29 @@ initialize curWorldExt : EnvExtension (Option Name) ← registerEnvExtension (pu
 /-- Register a (non-persistent) environment extension to hold the current level -/
 initialize curLevelExt : EnvExtension (Option Nat) ← registerEnvExtension (pure none)
 
+/--
+A game has three layers: Game, World, Levels. These are set with the commands
+`Game`, `World`, and `Level`.
+Commands like `Introduction` depend on the current level.
+-/
 inductive Layer :=
 | Game | World | Level
 
 variable {m: Type → Type} [Monad m] [MonadEnv m]
 
+/-- Set the current game -/
 def setCurGameId (game : Name) : m Unit :=
   modifyEnv (curGameExt.setState · (some game))
 
+/-- Set the current world -/
 def setCurWorldId (world : Name) : m Unit :=
   modifyEnv (curWorldExt.setState · (some world))
 
+/-- Set the current level -/
 def setCurLevelIdx (level : Nat) : m Unit :=
   modifyEnv (curLevelExt.setState · (some level))
 
+/-- Get the current layer. -/
 def getCurLayer [MonadError m] : m Layer := do
   match curGameExt.getState (← getEnv), curWorldExt.getState (← getEnv), curLevelExt.getState (← getEnv) with
   | _, some _, some _ => return Layer.Level
@@ -136,16 +145,19 @@ def getCurLayer [MonadError m] : m Layer := do
   | _, none, none => return Layer.Game
   | _, _, _ => throwError "Invalid Layer"
 
+/-- Get the current game, or default if none is specified -/
 def getCurGameId [Monad m] : m Name := do
   match curGameExt.getState (← getEnv) with
   | some game => return game
   | none => return defaultGameName
 
+/-- Get the current world -/
 def getCurWorldId [MonadError m] : m Name := do
   match curWorldExt.getState (← getEnv) with
   | some world => return world
   | none => throwError "Current world not set"
 
+/-- Get the current level -/
 def getCurLevelIdx [MonadError m] : m Nat := do
   match curLevelExt.getState (← getEnv) with
   | some level => return level
@@ -160,13 +172,13 @@ structure LevelId where
 deriving Inhabited
 
 structure InventoryInfo where
-  -- new inventory items introduced by this level:
+  /-- new inventory items introduced by this level -/
   new : Array Name
-  -- inventory items exceptionally forbidden in this level:
+  /-- inventory items exceptionally forbidden in this level -/
   disabled : Array Name
-  -- only these inventory items are allowed in this level (ignored if empty):
+  /-- only these inventory items are allowed in this level (ignored if empty) -/
   only : Array Name
-  -- inventory items in this level (computed by `MakeGame`):
+  /-- inventory items in this level (computed by `MakeGame`) -/
   computed : Array ComputedInventoryItem
 deriving ToJson, FromJson, Repr, Inhabited
 

From 60876b4a7764b79c0f8b2ebef30df1f3ef538ece Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 19 May 2023 13:03:23 +0200
Subject: [PATCH 2/5] move Doc class

---
 server/GameServer/EnvExtensions.lean | 7 +++++++
 server/GameServer/Game.lean          | 6 ------
 2 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean
index c4174cc..6e54609 100644
--- a/server/GameServer/EnvExtensions.lean
+++ b/server/GameServer/EnvExtensions.lean
@@ -65,6 +65,13 @@ structure InventoryDocEntry where
   content : String
   deriving ToJson, Repr, Inhabited
 
+/-- The reduced version of `InventoryDocEntry` which is sent to the client -/
+structure Doc where
+  name: String
+  displayName: String
+  text: String -- TODO: rename to `content`
+deriving ToJson
+
 /-- Another reduced version of `InventoryDocEntry` which is used for the tiles in the doc -/
 structure ComputedInventoryItem where
   /--
diff --git a/server/GameServer/Game.lean b/server/GameServer/Game.lean
index 230f818..f418d22 100644
--- a/server/GameServer/Game.lean
+++ b/server/GameServer/Game.lean
@@ -65,12 +65,6 @@ structure DidOpenLevelParams where
   definitions : Array ComputedInventoryItem
   deriving ToJson, FromJson
 
-structure Doc where
-  name: String
-  displayName: String
-  text: String
-deriving ToJson
-
 structure LoadDocParams where
   name : Name
   type : InventoryType

From fbf0f55968eb41ff51fcad05785d43416a362530 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Mon, 22 May 2023 20:30:58 +0200
Subject: [PATCH 3/5] reorganisational draft

---
 client/src/components/Inventory.tsx  |   5 +-
 client/src/components/Level.tsx      |   1 +
 client/src/state/api.ts              |   5 +-
 server/GameServer/Commands.lean      | 220 +++++++++++++++------------
 server/GameServer/EnvExtensions.lean | 160 ++++++++++++++-----
 server/GameServer/Game.lean          |  15 +-
 6 files changed, 261 insertions(+), 145 deletions(-)

diff --git a/client/src/components/Inventory.tsx b/client/src/components/Inventory.tsx
index 87efaa1..5b44995 100644
--- a/client/src/components/Inventory.tsx
+++ b/client/src/components/Inventory.tsx
@@ -13,6 +13,7 @@ export function Inventory({levelInfo, setInventoryDoc } :
     setInventoryDoc: (inventoryDoc: {name: string, type: string}) => void,
   }) {
 
+  // TODO: This seems like a useless wrapper to me
   function openDoc(name, type) {
     setInventoryDoc({name, type})
   }
@@ -103,6 +104,8 @@ export function Documentation({name, type}) {
 
   return <>
     <h2 className="doc">{doc.data?.displayName}</h2>
-    <Markdown>{doc.data?.text}</Markdown>
+    <p><code>{doc.data?.statement}</code></p>
+    {/* <code>docstring: {doc.data?.docstring}</code> */}
+    <Markdown>{doc.data?.content}</Markdown>
   </>
 }
diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index 7fae3d8..7c9cea0 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -171,6 +171,7 @@ function PlayableLevel({worldId, levelId}) {
     }
   }, [editor, commandLineMode])
 
+  // if this is set to a pair `(name, type)` then the according doc will be open.
   const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null)
 
   const levelTitle = <>{levelId && `Level ${levelId}`}{level?.data?.title && `: ${level?.data?.title}`}</>
diff --git a/client/src/state/api.ts b/client/src/state/api.ts
index 151af3b..1a47cf4 100644
--- a/client/src/state/api.ts
+++ b/client/src/state/api.ts
@@ -36,7 +36,10 @@ export interface LevelInfo {
 interface Doc {
   name: string,
   displayName: string,
-  text: string
+  content: string,
+  statement: string,
+  type: string, // TODO: can I remove these?
+  category: string,
 }
 
 
diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
index 9a1da1f..49bdf45 100644
--- a/server/GameServer/Commands.lean
+++ b/server/GameServer/Commands.lean
@@ -78,33 +78,40 @@ in the first level and get enabled during the game.
 
 /-! ## Doc entries -/
 
-/-- Throw a warning if inventory doc does not exist. If `(default := _)` is provided,
-it will create a new inverntory entry with the specified default description. -/
-def checkInventoryDoc (type : InventoryType) (name : Syntax)
-    (default : Option (String) := none) : CommandElabM Unit := do
-  let some _ := (inventoryDocExt.getState (← getEnv)).find?
-      (fun x => x.name == name.getId && x.type == type)
-    | match default with
-      | some _ =>
-        logInfoAt name (m!"Missing {type} Documentation: {name}, used provided default (e.g. " ++
-        m!"statement description) instead. If you want to write your own description, add " ++
-        m!"`{type}Doc {name}` somewhere above this statement.")
-      | none =>
-        logWarningAt name (m!"Missing {type} Documentation: {name}\nAdd `{type}Doc {name}` " ++
+/-- Checks if `inventoryKeyExt` contains an entry with `(type, name)` and yields
+a warning otherwise. If `template` is provided, it will add such an entry instead of yielding a
+warning. -/
+def checkInventoryDoc (type : InventoryType) (name : Ident)
+    (template : Option String := none) : CommandElabM Unit := do
+  -- note: `name` is an `Ident` (instead of `Name`) for the log messages.
+  let env ← getEnv
+  let n := name.getId
+  -- Find a key with matching `(type, name)`.
+  match (inventoryKeyExt.getState env).findIdx?
+    (fun x => x.name == n && x.type == type) with
+  -- Nothing to do if the entry exists
+  | some _ => pure ()
+  | none =>
+    match template with
+    -- Warn about missing documentation
+    | none =>
+      -- We just add a dummy entry
+      modifyEnv (inventoryKeyExt.addEntry · {
+        type := type
+        name := name.getId
+        category := if type == .Lemma then s!"{n.getPrefix}" else "" })
+      logWarningAt name (m!"Missing {type} Documentation: {name}\nAdd `{type}Doc {name}` " ++
         m!"somewhere above this statement.")
-
-      let default₀ := match default with
-      | some d => d
-      | none => "missing"
-
-      -- Create a default inventory entry
-      let n := name.getId
-      modifyEnv (inventoryDocExt.addEntry · {
-        name := n
+    -- Add the default documentation
+    | some s =>
+      modifyEnv (inventoryKeyExt.addEntry · {
         type := type
-        displayName :=  s!"{n}" -- TODO: for lemmas, only take the last part of the name
+        name := name.getId
         category := if type == .Lemma then s!"{n.getPrefix}" else ""
-        content := default₀ })
+        content := s })
+      logInfoAt name (m!"Missing {type} Documentation: {name}, used provided default (e.g. " ++
+      m!"statement description) instead. If you want to write your own description, add " ++
+      m!"`{type}Doc {name}` somewhere above this statement.")
 
 /-- Documentation entry of a tactic. Example:
 
@@ -116,8 +123,7 @@ TacticDoc rw "`rw` stands for rewrite, etc. "
 * The description is a string supporting Markdown.
  -/
 elab "TacticDoc" name:ident content:str : command =>
-  modifyEnv (inventoryDocExt.addEntry · {
-    category := default
+  modifyEnv (inventoryKeyExt.addEntry · {
     type := .Tactic
     name := name.getId
     displayName := name.getId.toString
@@ -136,12 +142,18 @@ LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
 * The description is a string supporting Markdown.
  -/
 elab "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str : command =>
-  modifyEnv (inventoryDocExt.addEntry · {
-    name := name.getId,
+  modifyEnv (inventoryKeyExt.addEntry · {
     type := .Lemma
-    displayName := displayName.getString,
-    category := category.getString,
+    name := name.getId
+    category := category.getString
+    displayName := displayName.getString
     content := content.getString })
+-- TODO: Catch the following behaviour.
+-- 1. if `LemmaDoc` appears in the same file as `Statement`, it will silently use
+-- it but display the info that it wasn't found in `Statement`
+-- 2. if it appears in a later file, however, it will silently not do anything and keep
+-- the first one.
+
 
 /-- Documentation entry of a definition. Example:
 
@@ -154,31 +166,63 @@ DefinitionDoc Function.Bijective as "Bijective" "defined as `Injective f ∧ Sur
 * The string following `as` is the displayed name (in the Inventory).
 * The description is a string supporting Markdown.
  -/
-elab "DefinitionDoc" name:ident "as" displayName:str content:str : command =>
-  modifyEnv (inventoryDocExt.addEntry · {
-    category := default
+elab "DefinitionDoc" name:ident "as" displayName:str template:str : command =>
+  modifyEnv (inventoryKeyExt.addEntry · {
     type := .Definition
     name := name.getId,
     displayName := displayName.getString,
-    content := content.getString })
+    content := template.getString })
 
 /-! ## Add inventory items -/
 
+-- namespace Lean.PrettyPrinter
+-- def ppSignature' (c : Name) : MetaM String := do
+--   let decl ← getConstInfo c
+--   let e := .const c (decl.levelParams.map mkLevelParam)
+--   let (stx, _) ← delabCore e (delab := Delaborator.delabConstWithSignature)
+--   let f ← ppTerm stx
+--   return toString f
+-- end Lean.PrettyPrinter
+
+def getStatement (name : Name) : CommandElabM MessageData := do
+  -- let c := name.getId
+
+  let decl ← getConstInfo name
+  -- -- TODO: How to go between CommandElabM and MetaM
+
+  -- addCompletionInfo <| .id name c (danglingDot := false) {} none
+  return ← addMessageContextPartial (.ofPPFormat { pp := fun
+    | some ctx => ctx.runMetaM <| ppExpr decl.type
+    -- PrettyPrinter.ppSignature' c
+    -- PrettyPrinter.ppSignature c
+    | none     => return "that's a bug." })
+
+-- Note: We use `String` because we can't send `MessageData` as json, but
+-- `MessageData` might be better for interactive highlighting.
+/-- Get a string of the form `my_lemma (n : ℕ) : n + n = 2 * n`. -/
+def getStatementString (name : Name) : CommandElabM String := do
+  try
+    return ← (← getStatement name).toString
+  catch
+  | _ => throwError m!"Could not find {name} in context."
+  -- TODO: I think it would be nicer to unresolve Namespaces as much as possible.
+
 /-- Declare tactics that are introduced by this level. -/
 elab "NewTactic" args:ident* : command => do
-  for name in ↑args do checkInventoryDoc .Tactic name
+  for name in ↑args do checkInventoryDoc .Tactic name -- TODO: Add (template := "[docstring]")
   modifyCurLevel fun level => pure {level with
     tactics := {level.tactics with new := args.map (·.getId)}}
 
 /-- Declare lemmas that are introduced by this level. -/
 elab "NewLemma" args:ident* : command => do
-  for name in ↑args do checkInventoryDoc .Lemma name
+  for name in ↑args do
+    checkInventoryDoc .Lemma name -- TODO: Add (template := "[mathlib]")
   modifyCurLevel fun level => pure {level with
     lemmas := {level.lemmas with new := args.map (·.getId)}}
 
 /-- Declare definitions that are introduced by this level. -/
 elab "NewDefinition" args:ident* : command => do
-  for name in ↑args do checkInventoryDoc .Definition name
+  for name in ↑args do checkInventoryDoc .Definition name -- TODO: Add (template := "[mathlib]")
   modifyCurLevel fun level => pure {level with
     definitions := {level.definitions with new := args.map (·.getId)}}
 
@@ -228,22 +272,6 @@ elab "LemmaTab"  category:str : command =>
 
 /-! # Exercise Statement -/
 
--- TODO: Instead of this, it would be nice to have a proper syntax parser that enables
--- us highlighting on the client side.
-partial def reprintCore : Syntax → Option Format
-  | Syntax.missing => none
-  | Syntax.atom _ val => val.trim
-  | Syntax.ident _ rawVal _ _ => rawVal.toString
-  | Syntax.node _ _ args =>
-    match args.toList.filterMap reprintCore with
-    | [] => none
-    | [arg] => arg
-    | args => Format.group <| Format.nest 2 <| Format.joinSep args " "
-
-/-- `reprint` is used to display the Lean-statement to the user-/
-def reprint (stx : Syntax) : Format :=
-  reprintCore stx |>.getD ""
-
 /-- A `attr := ...` option for `Statement`. Add attributes to the defined theorem. -/
 syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
 -- TODO
@@ -259,14 +287,9 @@ elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : com
   -- Save the messages before evaluation of the proof.
   let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
 
-  -- Check that statement has a docs entry.
-  match statementName with
-  | some name => checkInventoryDoc .Lemma name (default := descr)
-  | none => pure ()
-
   -- The default name of the statement is `[Game].[World].level[no.]`, e.g. `NNG.Addition.level1`
   -- However, this should not be used when designing the game.
-  let defaultDeclName : Name := (← getCurGame).name ++ (← getCurWorld).name ++
+  let defaultDeclName : Ident := mkIdent <| (← getCurGame).name ++ (← getCurWorld).name ++
     ("level" ++ toString lvlIdx : String)
 
   -- Add theorem to context.
@@ -277,35 +300,21 @@ elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : com
       let origType := (env.constants.map₁.find! name.getId).type
       -- TODO: Check if `origType` agrees with `sig` and output `logInfo` instead of `logWarning`
       -- in that case.
-      logWarningAt name m!"Environment already contains {name.getId}!
-Only the existing statement will be available in later levels:
-
-{origType}"
-      -- let (binders, typeStx) := expandDeclSig sig
-      -- --let type ← Term.elabType typeStx
-      -- runTermElabM (fun vars =>
-      --   Term.elabBinders binders.getArgs (fun xs => do
-      --   let type ← Term.elabType typeStx
-      --   --Term.synthesizeSyntheticMVarsNoPostponing
-      --   --let type ← instantiateMVars type
-      --   --let type ← mkForallFVars xs type
-      -- ))
-      --let newType := Term.elabTerm sig.raw
-      --dbg_trace newType
-      --logInfo origType
-      -- dbg_trace sig
-      -- dbg_trace origType
-      --dbg_trace (env.constants.map₁.find! name.getId).value! -- that's the proof
-      --let newType := Lean.Elab.Term.elabTerm sig none
-
-      let thmStatement ← `(theorem $(mkIdent defaultDeclName) $sig $val)
+      logWarningAt name (m!"Environment already contains {name.getId}! Only the existing " ++
+      m!"statement will be available in later levels:\n\n{origType}")
+      let thmStatement ← `(theorem $defaultDeclName $sig $val)
       elabCommand thmStatement
+      -- Check that statement has a docs entry.
+      checkInventoryDoc .Lemma name (template := descr)
+
     else
-      -- logInfo attr
-      let thmStatement ← `( theorem $(mkIdent name.getId) $sig $val)
+      let thmStatement ← `( theorem $name $sig $val)
       elabCommand thmStatement
+      -- Check that statement has a docs entry.
+      checkInventoryDoc .Lemma name (template := descr)
+
   | none =>
-    let thmStatement ← `(theorem $(mkIdent defaultDeclName) $sig $val)
+    let thmStatement ← `(theorem $defaultDeclName $sig $val)
     elabCommand thmStatement
 
   let msgs := (← get).messages
@@ -339,7 +348,15 @@ Only the existing statement will be available in later levels:
   let scope ← getScope
   let env ← getEnv
 
-  modifyCurLevel fun level => pure {level with
+  let st ← match statementName with
+  | some name => getStatementString name.getId
+  | none =>  getStatementString defaultDeclName.getId -- TODO: We dont want the internal lemma name here
+
+  let head := match statementName with
+  | some name => Format.join ["theorem ", name.getId.toString]
+  | none => "example"
+
+  modifyCurLevel fun level => pure { level with
     module := env.header.mainModule
     goal := sig,
     scope := scope,
@@ -347,13 +364,8 @@ Only the existing statement will be available in later levels:
     statementName := match statementName with
     | none => default
     | some name => name.getId
-    descrFormat := match statementName with
-    | none => "example " ++ (toString <| reprint sig.raw) ++ " := by"
-    | some name => (Format.join ["theorem ", reprint name.raw, " ", reprint sig.raw, " := by"]).pretty 10  -- "lemma "  ++ (toString <| reprint name.raw) ++ " " ++ (Format.pretty (reprint sig.raw) 40) ++ " := by"
-    hints := hints
-  } -- Format.pretty <| format thmStatement.raw }
-
-
+    descrFormat := (Format.join [head, " ", st, " := by"]).pretty 10
+    hints := hints }
 
 /-! # Hints -/
 
@@ -500,6 +512,21 @@ elab "MakeGame" : command => do
   if game.worlds.hasLoops then
     throwError "World graph must not contain loops! Check your `Path` declarations."
 
+  -- Now create The doc entries from the templates
+  for item in inventoryKeyExt.getState (← getEnv) do
+    -- TODO: Add information about inventory items
+    let name := item.name
+    match item.type with
+    | .Lemma =>
+      modifyEnv (inventoryExt.addEntry · { item with
+        -- Add the lemma statement to the doc.
+        statement := (← getStatementString name)
+      })
+    | _ =>
+      modifyEnv (inventoryExt.addEntry · {
+        item with
+      })
+
   -- Compute which inventory items are available in which level:
   for inventoryType in #[.Tactic, .Definition, .Lemma] do
     let mut newItemsInWorld : HashMap Name (HashSet Name) := {}
@@ -543,7 +570,8 @@ elab "MakeGame" : command => do
     let Availability₀ : HashMap Name ComputedInventoryItem :=
       HashMap.ofList $
         ← allItems.toList.mapM fun item => do
-          let data := (← getInventoryDoc? item inventoryType).get!
+          let data := (← getInventoryItem? item inventoryType).get!
+          -- TODO: BUG, panic at `get!` in vscode
           return (item, {
             name := item
             displayName := data.displayName
@@ -557,7 +585,7 @@ elab "MakeGame" : command => do
       let predecessors := game.worlds.predecessors worldId
       for predWorldId in predecessors do
         for item in newItemsInWorld.find! predWorldId do
-          let data := (← getInventoryDoc? item inventoryType).get!
+          let data := (← getInventoryItem? item inventoryType).get!
           items := items.insert item {
             name := item
             displayName := data.displayName
@@ -575,7 +603,7 @@ elab "MakeGame" : command => do
 
         -- unlock items that are unlocked in this level
         for item in levelInfo.new do
-          let data := (← getInventoryDoc? item inventoryType).get!
+          let data := (← getInventoryItem? item inventoryType).get!
           items := items.insert item {
             name := item
             displayName := data.displayName
@@ -588,7 +616,7 @@ elab "MakeGame" : command => do
           match lemmaStatements.find? (worldId, levelId) with
           | none => pure ()
           | some name =>
-            let data := (← getInventoryDoc? name inventoryType).get!
+            let data := (← getInventoryItem? name inventoryType).get!
             items := items.insert name {
               name := name
               displayName := data.displayName
diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean
index 6e54609..748ccd2 100644
--- a/server/GameServer/EnvExtensions.lean
+++ b/server/GameServer/EnvExtensions.lean
@@ -1,22 +1,23 @@
 import GameServer.AbstractCtx
 import GameServer.Graph
 
-/-! # Environment extensions
-
-The game framework stores almost all its game building data in environment extensions
-defined in this file.
--/
-
-open Lean
 
--- Note: When changing these, one also needs to change them in `index.mjs`
 
 /-- The default game name if `Game "MyGame"` is not used. -/
 def defaultGameName: String := "MyGame"
+-- Note: When changing any of these default names, one also needs to change them in `index.mjs`
 
 /-- The default game module name. -/
 def defaultGameModule: String := "Game"
 
+/-! # Environment extensions
+
+The game framework stores almost all its game building data in environment extensions
+defined in this file.
+-/
+
+open Lean
+
 /-! ## Hints -/
 
 /-- A hint to help the user with a specific goal state -/
@@ -33,17 +34,88 @@ instance : Repr GoalHintEntry := {
   reprPrec := fun a n => reprPrec a.text n
 }
 
-/-! ## Tactic/Definition/Lemma documentation -/
+/-! ## Tactic/Definition/Lemma documentation
+
+There are three inventory types: Lemma, Tactic, Definition. They vary about in the information
+they carry.
+
+The commands `LemmaDoc`, `TacticDoc`, and `DefinitionDoc` add keys and templates to an
+env. extension called `InventoryKeyExt`. Commands like `NewLemma`, etc. as well as
+`Statement` check if there is a key registered in this extension and might add a default or
+print a warning if not.
+
+Then, `MakeGame` takes the templates from `InventoryKeyExt` and creates the documentation entries
+that are sent to the client. This allows us to modify them like adding information from
+mathlib or from parsing the lemma in question.
+-/
 
 /-- The game knows three different inventory types that contain slightly different information -/
 inductive InventoryType := | Tactic | Lemma | Definition
 deriving ToJson, FromJson, Repr, BEq, Hashable, Inhabited
 
+-- TODO: golf this?
 instance : ToString InventoryType := ⟨fun t => match t with
 | .Tactic => "Tactic"
 | .Lemma => "Lemma"
-| .Definition => "Definition"
-⟩
+| .Definition => "Definition"⟩
+
+/-- The keys/templates of the inventory items, stored in `InventoryKeyExt`. -/
+structure InventoryKey where
+  /-- Lemma, Tactic, or Definition -/
+  type: InventoryType
+  /-- Depends on the type:
+  * Tactic: the tactic's name
+  * Lemma: fully qualified lemma name
+  * Definition: no restrictions (preferrably the definions fully qualified name)
+  -/
+  name: Name
+  /-- Only for Lemmas. To sort them into tabs -/
+  category: String := default
+  /-- Free-text short name -/
+  displayName: String := name.toString
+  /-- Template documentation. Allows for special tags to insert mathlib info [TODO!] -/
+  content: String := "(missing)"
+  deriving ToJson, Repr, Inhabited
+
+/-- A inventory item as it gets sent to the client. The command `MakeGame` creates these
+from the `InventoryKey`s and modifies them. -/
+structure InventoryItem extends InventoryKey where -- TODO: can I remove the field `template`? Probably not...
+  statement: String := ""
+  deriving ToJson, Repr, Inhabited
+
+/-- The extension that stores the doc templates. Note that you can only add, but never modify
+entries! -/
+initialize inventoryKeyExt : SimplePersistentEnvExtension InventoryKey (Array InventoryKey) ←
+  registerSimplePersistentEnvExtension {
+    name := `inventory_keys
+    addEntryFn := Array.push
+    addImportedFn := Array.concatMap id }
+
+def getInventoryKey? [Monad m] [MonadEnv m] (n : Name) (type : InventoryType) :
+    m (Option InventoryKey) := do
+  return (inventoryKeyExt.getState (← getEnv)).find? (fun x => x.name == n && x.type == type)
+
+/-- The extension that contains the inventory content after it has been processed.
+`MakeGame` is the only command adding items here. -/
+initialize inventoryExt : SimplePersistentEnvExtension InventoryItem (Array InventoryItem) ←
+  registerSimplePersistentEnvExtension {
+    name := `inventory_doc
+    addEntryFn := Array.push
+    addImportedFn := Array.concatMap id }
+
+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)
+
+
+
+
+
+
+
+
+
+
 
 /-- An inventory item represents the documentation of a tactic/lemma/definitions. -/
 structure InventoryDocEntry where
@@ -63,14 +135,20 @@ structure InventoryDocEntry where
   category : String
   /-- The description (doc) of the item. (free-text) -/
   content : String
+  /-- For definitions and statements this is the statement -/
+  statement : String := ""
+  /-- The docstring if one exists -/
+  docstring : String := ""
   deriving ToJson, Repr, Inhabited
 
-/-- The reduced version of `InventoryDocEntry` which is sent to the client -/
-structure Doc where
-  name: String
-  displayName: String
-  text: String -- TODO: rename to `content`
-deriving ToJson
+-- /-- The reduced version of `InventoryDocEntry` which is sent to the client -/
+-- structure Doc where
+--   name: String
+--   displayName: String
+--   content: String
+--   statement : String
+--   docstring : String
+-- deriving ToJson
 
 /-- Another reduced version of `InventoryDocEntry` which is used for the tiles in the doc -/
 structure ComputedInventoryItem where
@@ -94,23 +172,23 @@ structure ComputedInventoryItem where
   new := false
 deriving ToJson, FromJson, Repr, Inhabited
 
-/-- Environment extension for inventory documentation. -/
-initialize inventoryDocExt : SimplePersistentEnvExtension InventoryDocEntry (Array InventoryDocEntry) ←
-  registerSimplePersistentEnvExtension {
-    name := `inventory_doc
-    addEntryFn := Array.push
-    addImportedFn := Array.concatMap id
-  }
+-- /-- This extension only keeps track of all doc entries that will need to be gener. -/
+-- initialize inventoryDocExt : SimplePersistentEnvExtension InventoryDocEntry (Array InventoryDocEntry) ←
+--   registerSimplePersistentEnvExtension {
+--     name := `inventory_doc_old
+--     addEntryFn := Array.push
+--     addImportedFn := Array.concatMap id
+--   }
 
-def getInventoryDoc? {m : Type → Type} [Monad m] [MonadEnv m] (n : Name) (type : InventoryType) :
-    m (Option InventoryDocEntry) := do
-  return (inventoryDocExt.getState (← getEnv)).find? (fun x => x.name == n && x.type == type)
+-- def getInventoryDoc? {m : Type → Type} [Monad m] [MonadEnv m] (n : Name) (type : InventoryType) :
+--     m (Option InventoryDocEntry) := do
+--   return (inventoryDocExt.getState (← getEnv)).find? (fun x => x.name == n && x.type == type)
 
-open Elab Command in
-/-- Print a registered tactic doc for debugging purposes. -/
-elab "#print_doc" : command => do
-  for entry in inventoryDocExt.getState (← getEnv) do
-    dbg_trace "[{entry.type}] {entry.name} : {entry.content}"
+-- open Elab Command in
+-- /-- Print a registered tactic doc for debugging purposes. -/
+-- elab "#print_doc" : command => do
+--   for entry in inventoryDocExt.getState (← getEnv) do
+--     dbg_trace "[{entry.type}] {entry.name} : {entry.content}"
 
 
 /-! ## Environment extensions for game specification-/
@@ -134,23 +212,25 @@ variable {m: Type → Type} [Monad m] [MonadEnv m]
 
 /-- Set the current game -/
 def setCurGameId (game : Name) : m Unit :=
-  modifyEnv (curGameExt.setState · (some game))
+  modifyEnv (curGameExt.setState · game)
 
 /-- Set the current world -/
 def setCurWorldId (world : Name) : m Unit :=
-  modifyEnv (curWorldExt.setState · (some world))
+  modifyEnv (curWorldExt.setState · world)
 
 /-- Set the current level -/
 def setCurLevelIdx (level : Nat) : m Unit :=
-  modifyEnv (curLevelExt.setState · (some level))
+  modifyEnv (curLevelExt.setState · level)
 
 /-- Get the current layer. -/
 def getCurLayer [MonadError m] : m Layer := do
-  match curGameExt.getState (← getEnv), curWorldExt.getState (← getEnv), curLevelExt.getState (← getEnv) with
-  | _, some _, some _ => return Layer.Level
-  | _, some _, none => return Layer.World
-  | _, none, none => return Layer.Game
-  | _, _, _ => throwError "Invalid Layer"
+  -- previously, we also had `curGameExt.getState (← getEnv), ` in here, which got removed
+  -- when we made the `Game` command optional
+  match curWorldExt.getState (← getEnv), curLevelExt.getState (← getEnv) with
+  | some _, some _ => return Layer.Level
+  | some _, none => return Layer.World
+  | none, none => return Layer.Game
+  | _, _ => throwError "Invalid Layer"
 
 /-- Get the current game, or default if none is specified -/
 def getCurGameId [Monad m] : m Name := do
diff --git a/server/GameServer/Game.lean b/server/GameServer/Game.lean
index f418d22..057c795 100644
--- a/server/GameServer/Game.lean
+++ b/server/GameServer/Game.lean
@@ -130,7 +130,7 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
             lemmaTab := lvl.lemmaTab
             statementName := match lvl.statementName with
               | .anonymous => none
-              | name => match (inventoryDocExt.getState env).find?
+              | name => match (inventoryExt.getState env).find?
                   (fun x => x.name == name && x.type == .Lemma) with
                 | some n => n.displayName
                 | none => name.toString
@@ -143,14 +143,15 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
       let p ← parseParams LoadDocParams (toJson params)
       -- let s ← get
       let c ← read
-      let some doc ← getInventoryDoc? p.name p.type
+      let some doc ← getInventoryItem? p.name p.type
         | do
-            c.hOut.writeLspResponseError ⟨id, .invalidParams, s!"Documentation not found: {p.name}", none⟩
+            c.hOut.writeLspResponseError ⟨id, .invalidParams,
+              s!"Documentation not found: {p.name}", none⟩
             return true
-      let doc : Doc :=
-          { name := doc.name.toString
-            displayName := doc.displayName
-            text := doc.content }
+      -- 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
     | _ => return false

From 3bf5c5e5e8939e6be10da8b42f6bb9268c8db73c Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Mon, 22 May 2023 21:20:24 +0200
Subject: [PATCH 4/5] rename and tidy up

---
 client/src/components/Inventory.tsx  |   4 +-
 client/src/state/api.ts              |   8 +-
 server/GameServer/Commands.lean      |  28 +++---
 server/GameServer/EnvExtensions.lean | 135 ++++++++-------------------
 server/GameServer/Game.lean          |  24 ++---
 5 files changed, 71 insertions(+), 128 deletions(-)

diff --git a/client/src/components/Inventory.tsx b/client/src/components/Inventory.tsx
index 5b44995..c987b7b 100644
--- a/client/src/components/Inventory.tsx
+++ b/client/src/components/Inventory.tsx
@@ -4,7 +4,7 @@ import './inventory.css'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faLock, faLockOpen, faBook, faHammer, faBan } from '@fortawesome/free-solid-svg-icons'
 import Markdown from './Markdown';
-import { useLoadDocQuery, ComputedInventoryItem, LevelInfo } from '../state/api';
+import { useLoadDocQuery, InventoryTile, LevelInfo } from '../state/api';
 import { GameIdContext } from '../App';
 
 export function Inventory({levelInfo, setInventoryDoc } :
@@ -37,7 +37,7 @@ export function Inventory({levelInfo, setInventoryDoc } :
 
 function InventoryList({items, docType, openDoc, defaultTab=null, level=undefined} :
   {
-    items: ComputedInventoryItem[],
+    items: InventoryTile[],
     docType: string,
     openDoc(name: string, type: string): void,
     defaultTab? : string,
diff --git a/client/src/state/api.ts b/client/src/state/api.ts
index 1a47cf4..349b905 100644
--- a/client/src/state/api.ts
+++ b/client/src/state/api.ts
@@ -10,7 +10,7 @@ interface GameInfo {
   conclusion: null|string,
 }
 
-export interface ComputedInventoryItem {
+export interface InventoryTile {
   name: string,
   displayName: string,
   category: string,
@@ -24,9 +24,9 @@ export interface LevelInfo {
   introduction: null|string,
   conclusion: null|string,
   index: number,
-  tactics: ComputedInventoryItem[],
-  lemmas: ComputedInventoryItem[],
-  definitions: ComputedInventoryItem[],
+  tactics: InventoryTile[],
+  lemmas: InventoryTile[],
+  definitions: InventoryTile[],
   descrText: null|string,
   descrFormat: null|string,
   lemmaTab: null|string,
diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
index 49bdf45..bed4d07 100644
--- a/server/GameServer/Commands.lean
+++ b/server/GameServer/Commands.lean
@@ -78,7 +78,7 @@ in the first level and get enabled during the game.
 
 /-! ## Doc entries -/
 
-/-- Checks if `inventoryKeyExt` contains an entry with `(type, name)` and yields
+/-- Checks if `inventoryTemplateExt` contains an entry with `(type, name)` and yields
 a warning otherwise. If `template` is provided, it will add such an entry instead of yielding a
 warning. -/
 def checkInventoryDoc (type : InventoryType) (name : Ident)
@@ -87,7 +87,7 @@ def checkInventoryDoc (type : InventoryType) (name : Ident)
   let env ← getEnv
   let n := name.getId
   -- Find a key with matching `(type, name)`.
-  match (inventoryKeyExt.getState env).findIdx?
+  match (inventoryTemplateExt.getState env).findIdx?
     (fun x => x.name == n && x.type == type) with
   -- Nothing to do if the entry exists
   | some _ => pure ()
@@ -96,7 +96,7 @@ def checkInventoryDoc (type : InventoryType) (name : Ident)
     -- Warn about missing documentation
     | none =>
       -- We just add a dummy entry
-      modifyEnv (inventoryKeyExt.addEntry · {
+      modifyEnv (inventoryTemplateExt.addEntry · {
         type := type
         name := name.getId
         category := if type == .Lemma then s!"{n.getPrefix}" else "" })
@@ -104,7 +104,7 @@ def checkInventoryDoc (type : InventoryType) (name : Ident)
         m!"somewhere above this statement.")
     -- Add the default documentation
     | some s =>
-      modifyEnv (inventoryKeyExt.addEntry · {
+      modifyEnv (inventoryTemplateExt.addEntry · {
         type := type
         name := name.getId
         category := if type == .Lemma then s!"{n.getPrefix}" else ""
@@ -123,7 +123,7 @@ TacticDoc rw "`rw` stands for rewrite, etc. "
 * The description is a string supporting Markdown.
  -/
 elab "TacticDoc" name:ident content:str : command =>
-  modifyEnv (inventoryKeyExt.addEntry · {
+  modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Tactic
     name := name.getId
     displayName := name.getId.toString
@@ -142,7 +142,7 @@ LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
 * The description is a string supporting Markdown.
  -/
 elab "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str : command =>
-  modifyEnv (inventoryKeyExt.addEntry · {
+  modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Lemma
     name := name.getId
     category := category.getString
@@ -167,7 +167,7 @@ DefinitionDoc Function.Bijective as "Bijective" "defined as `Injective f ∧ Sur
 * The description is a string supporting Markdown.
  -/
 elab "DefinitionDoc" name:ident "as" displayName:str template:str : command =>
-  modifyEnv (inventoryKeyExt.addEntry · {
+  modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Definition
     name := name.getId,
     displayName := displayName.getString,
@@ -498,10 +498,10 @@ def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo
 | .Lemma => level.lemmas
 
 def GameLevel.setComputedInventory (level : GameLevel) :
-    InventoryType → Array ComputedInventoryItem → GameLevel
-| .Tactic, v =>     {level with tactics     := {level.tactics     with computed := v}}
-| .Definition, v => {level with definitions := {level.definitions with computed := v}}
-| .Lemma, v =>      {level with lemmas      := {level.lemmas      with computed := v}}
+    InventoryType → Array InventoryTile → GameLevel
+| .Tactic, v =>     {level with tactics     := {level.tactics     with tiles := v}}
+| .Definition, v => {level with definitions := {level.definitions with tiles := v}}
+| .Lemma, v =>      {level with lemmas      := {level.lemmas      with tiles := v}}
 
 /-- Build the game. This command will precompute various things about the game, such as which
 tactics are available in each level etc. -/
@@ -513,7 +513,7 @@ elab "MakeGame" : command => do
     throwError "World graph must not contain loops! Check your `Path` declarations."
 
   -- Now create The doc entries from the templates
-  for item in inventoryKeyExt.getState (← getEnv) do
+  for item in inventoryTemplateExt.getState (← getEnv) do
     -- TODO: Add information about inventory items
     let name := item.name
     match item.type with
@@ -567,7 +567,7 @@ elab "MakeGame" : command => do
       newItemsInWorld := newItemsInWorld.insert worldId newItems
 
     -- Basic inventory item availability: all locked.
-    let Availability₀ : HashMap Name ComputedInventoryItem :=
+    let Availability₀ : HashMap Name InventoryTile :=
       HashMap.ofList $
         ← allItems.toList.mapM fun item => do
           let data := (← getInventoryItem? item inventoryType).get!
@@ -578,7 +578,7 @@ elab "MakeGame" : command => do
             category := data.category })
 
     -- Availability after a given world
-    let mut itemsInWorld : HashMap Name (HashMap Name ComputedInventoryItem) := {}
+    let mut itemsInWorld : HashMap Name (HashMap Name InventoryTile) := {}
     for (worldId, _) in game.worlds.nodes.toArray do
       -- Unlock all items from previous worlds
       let mut items := Availability₀
diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean
index 748ccd2..90d1f5d 100644
--- a/server/GameServer/EnvExtensions.lean
+++ b/server/GameServer/EnvExtensions.lean
@@ -34,17 +34,18 @@ instance : Repr GoalHintEntry := {
   reprPrec := fun a n => reprPrec a.text n
 }
 
-/-! ## Tactic/Definition/Lemma documentation
+/-! ## Inventory (documentation)
 
+The inventory contains documentation that the user can access.
 There are three inventory types: Lemma, Tactic, Definition. They vary about in the information
 they carry.
 
 The commands `LemmaDoc`, `TacticDoc`, and `DefinitionDoc` add keys and templates to an
-env. extension called `InventoryKeyExt`. Commands like `NewLemma`, etc. as well as
+env. extension called `InventoryTemplateExt`. Commands like `NewLemma`, etc. as well as
 `Statement` check if there is a key registered in this extension and might add a default or
 print a warning if not.
 
-Then, `MakeGame` takes the templates from `InventoryKeyExt` and creates the documentation entries
+Then, `MakeGame` takes the templates from `InventoryTemplateExt` and creates the documentation entries
 that are sent to the client. This allows us to modify them like adding information from
 mathlib or from parsing the lemma in question.
 -/
@@ -59,8 +60,8 @@ instance : ToString InventoryType := ⟨fun t => match t with
 | .Lemma => "Lemma"
 | .Definition => "Definition"⟩
 
-/-- The keys/templates of the inventory items, stored in `InventoryKeyExt`. -/
-structure InventoryKey where
+/-- The keys/templates of the inventory items, stored in `InventoryTemplateExt`. -/
+structure InventoryTemplate where
   /-- Lemma, Tactic, or Definition -/
   type: InventoryType
   /-- Depends on the type:
@@ -77,81 +78,14 @@ structure InventoryKey where
   content: String := "(missing)"
   deriving ToJson, Repr, Inhabited
 
-/-- A inventory item as it gets sent to the client. The command `MakeGame` creates these
-from the `InventoryKey`s and modifies them. -/
-structure InventoryItem extends InventoryKey where -- TODO: can I remove the field `template`? Probably not...
+/-- A full inventory item including the processing by `MakeGame`, which creates these
+from the `InventoryTemplate`s and modifies them. -/
+structure InventoryItem extends InventoryTemplate where
   statement: String := ""
   deriving ToJson, Repr, Inhabited
 
-/-- The extension that stores the doc templates. Note that you can only add, but never modify
-entries! -/
-initialize inventoryKeyExt : SimplePersistentEnvExtension InventoryKey (Array InventoryKey) ←
-  registerSimplePersistentEnvExtension {
-    name := `inventory_keys
-    addEntryFn := Array.push
-    addImportedFn := Array.concatMap id }
-
-def getInventoryKey? [Monad m] [MonadEnv m] (n : Name) (type : InventoryType) :
-    m (Option InventoryKey) := do
-  return (inventoryKeyExt.getState (← getEnv)).find? (fun x => x.name == n && x.type == type)
-
-/-- The extension that contains the inventory content after it has been processed.
-`MakeGame` is the only command adding items here. -/
-initialize inventoryExt : SimplePersistentEnvExtension InventoryItem (Array InventoryItem) ←
-  registerSimplePersistentEnvExtension {
-    name := `inventory_doc
-    addEntryFn := Array.push
-    addImportedFn := Array.concatMap id }
-
-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)
-
-
-
-
-
-
-
-
-
-
-
-/-- An inventory item represents the documentation of a tactic/lemma/definitions. -/
-structure InventoryDocEntry where
-  /--
-  The name of the item. The restrictions are:
-
-  * for Tactics: The name of the tactic.
-  * for Lemmas: *Fully qualified* lemma name.
-  * for Definitions: no restrictions.
-  -/
-  name : Name
-  /-- One of `Tactic`, `Lemma` and `Definition`. -/
-  type : InventoryType
-  /-- The display name shown in the inventory. This can be free-text. -/
-  displayName : String
-  /-- Category to group inventory items by. (currently only used for lemmas) -/
-  category : String
-  /-- The description (doc) of the item. (free-text) -/
-  content : String
-  /-- For definitions and statements this is the statement -/
-  statement : String := ""
-  /-- The docstring if one exists -/
-  docstring : String := ""
-  deriving ToJson, Repr, Inhabited
-
--- /-- The reduced version of `InventoryDocEntry` which is sent to the client -/
--- structure Doc where
---   name: String
---   displayName: String
---   content: String
---   statement : String
---   docstring : String
--- deriving ToJson
-
-/-- Another reduced version of `InventoryDocEntry` which is used for the tiles in the doc -/
-structure ComputedInventoryItem where
+/-- A reduced variant of `InventoryItem` which is used for the tiles in the doc -/
+structure InventoryTile where
   /--
   The name of the item. The restrictions are:
 
@@ -172,26 +106,36 @@ structure ComputedInventoryItem where
   new := false
 deriving ToJson, FromJson, Repr, Inhabited
 
--- /-- This extension only keeps track of all doc entries that will need to be gener. -/
--- initialize inventoryDocExt : SimplePersistentEnvExtension InventoryDocEntry (Array InventoryDocEntry) ←
---   registerSimplePersistentEnvExtension {
---     name := `inventory_doc_old
---     addEntryFn := Array.push
---     addImportedFn := Array.concatMap id
---   }
+/-- The extension that stores the doc templates. Note that you can only add, but never modify
+entries! -/
+initialize inventoryTemplateExt :
+    SimplePersistentEnvExtension InventoryTemplate (Array InventoryTemplate) ←
+  registerSimplePersistentEnvExtension {
+    name := `inventory_keys
+    addEntryFn := Array.push
+    addImportedFn := Array.concatMap id }
+
+/-- Receive the template with that matches `(name, type)` -/
+def getInventoryTemplate? [Monad m] [MonadEnv m] (n : Name) (type : InventoryType) :
+    m (Option InventoryTemplate) := do
+  return (inventoryTemplateExt.getState (← getEnv)).find? (fun x => x.name == n && x.type == type)
 
--- def getInventoryDoc? {m : Type → Type} [Monad m] [MonadEnv m] (n : Name) (type : InventoryType) :
---     m (Option InventoryDocEntry) := do
---   return (inventoryDocExt.getState (← getEnv)).find? (fun x => x.name == n && x.type == type)
+/-- The extension that contains the inventory content after it has been processed.
+`MakeGame` is the only command adding items here. -/
+initialize inventoryExt : SimplePersistentEnvExtension InventoryItem (Array InventoryItem) ←
+  registerSimplePersistentEnvExtension {
+    name := `inventory_doc
+    addEntryFn := Array.push
+    addImportedFn := Array.concatMap id }
+
+/-- Receive the item with that matches `(name, type)` -/
+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)
 
--- open Elab Command in
--- /-- Print a registered tactic doc for debugging purposes. -/
--- elab "#print_doc" : command => do
---   for entry in inventoryDocExt.getState (← getEnv) do
---     dbg_trace "[{entry.type}] {entry.name} : {entry.content}"
 
 
-/-! ## Environment extensions for game specification-/
+/-! ## Environment extensions for game specification -/
 
 /-- Register a (non-persistent) environment extension to hold the current level -/
 initialize curGameExt : EnvExtension (Option Name) ← registerEnvExtension (pure none)
@@ -202,8 +146,7 @@ initialize curLevelExt : EnvExtension (Option Nat) ← registerEnvExtension (pur
 
 /--
 A game has three layers: Game, World, Levels. These are set with the commands
-`Game`, `World`, and `Level`.
-Commands like `Introduction` depend on the current level.
+`Game`, `World`, and `Level`. Commands like `Introduction` depend on the current level.
 -/
 inductive Layer :=
 | Game | World | Level
@@ -266,7 +209,7 @@ structure InventoryInfo where
   /-- only these inventory items are allowed in this level (ignored if empty) -/
   only : Array Name
   /-- inventory items in this level (computed by `MakeGame`) -/
-  computed : Array ComputedInventoryItem
+  tiles : Array InventoryTile
 deriving ToJson, FromJson, Repr, Inhabited
 
 def getCurLevelId [MonadError m] : m LevelId := do
diff --git a/server/GameServer/Game.lean b/server/GameServer/Game.lean
index 057c795..8183d15 100644
--- a/server/GameServer/Game.lean
+++ b/server/GameServer/Game.lean
@@ -40,9 +40,9 @@ Fields:
 structure LevelInfo where
   index : Nat
   title : String
-  tactics : Array ComputedInventoryItem
-  lemmas : Array ComputedInventoryItem
-  definitions : Array ComputedInventoryItem
+  tactics : Array InventoryTile
+  lemmas : Array InventoryTile
+  definitions : Array InventoryTile
   introduction : String
   conclusion : String
   descrText : Option String := none
@@ -60,9 +60,9 @@ structure DidOpenLevelParams where
   uri : String
   gameDir : String
   levelModule : Name
-  tactics : Array ComputedInventoryItem
-  lemmas : Array ComputedInventoryItem
-  definitions : Array ComputedInventoryItem
+  tactics : Array InventoryTile
+  lemmas : Array InventoryTile
+  definitions : Array InventoryTile
   deriving ToJson, FromJson
 
 structure LoadDocParams where
@@ -89,9 +89,9 @@ def handleDidOpenLevel (params : Json) : GameServerM Unit := do
       uri := m.uri
       gameDir := (← get).gameDir
       levelModule := lvl.module
-      tactics := lvl.tactics.computed
-      lemmas := lvl.lemmas.computed
-      definitions := lvl.definitions.computed
+      tactics := lvl.tactics.tiles
+      lemmas := lvl.lemmas.tiles
+      definitions := lvl.definitions.tiles
       : DidOpenLevelParams
     }
   }
@@ -120,9 +120,9 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
       let levelInfo : LevelInfo :=
           { index := lvl.index,
             title := lvl.title,
-            tactics := lvl.tactics.computed,
-            lemmas := lvl.lemmas.computed,
-            definitions := lvl.definitions.computed,
+            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

From 047d75e74d27e88efb4570e859e92b40c36e9905 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Wed, 24 May 2023 15:25:55 +0200
Subject: [PATCH 5/5] add function to retrieve tactic docstring

---
 server/GameServer/Commands.lean      | 103 +++++++++++++++++++++++++--
 server/GameServer/EnvExtensions.lean |   2 +-
 2 files changed, 99 insertions(+), 6 deletions(-)

diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
index bed4d07..2a7d02b 100644
--- a/server/GameServer/Commands.lean
+++ b/server/GameServer/Commands.lean
@@ -140,6 +140,9 @@ LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
 * The string following `as` is the displayed name (in the Inventory).
 * The identifier after `in` is the category to group lemmas by (in the Inventory).
 * The description is a string supporting Markdown.
+
+Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requries
+The lemma/definition to have the same fully qualified name as in mathlib.
  -/
 elab "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str : command =>
   modifyEnv (inventoryTemplateExt.addEntry · {
@@ -165,6 +168,9 @@ DefinitionDoc Function.Bijective as "Bijective" "defined as `Injective f ∧ Sur
   It is preferably the true name of the definition. However, this is not required.
 * The string following `as` is the displayed name (in the Inventory).
 * The description is a string supporting Markdown.
+
+Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requries
+The lemma/definition to have the same fully qualified name as in mathlib.
  -/
 elab "DefinitionDoc" name:ident "as" displayName:str template:str : command =>
   modifyEnv (inventoryTemplateExt.addEntry · {
@@ -487,8 +493,21 @@ elab "Hole" t:tacticSeq : tactic => do
   Tactic.evalTactic t
 
 
+-- TODO: Notes for testing if a declaration has the simp attribute
+
+-- -- Test: From zulip
+-- section test
 
+-- open Lean Meta Elab Command Tactic Simp
 
+-- def Lean.Meta.SimpTheorems.hasAttribute (d : SimpTheorems) (decl : Name) :=
+--   d.isLemma (.decl decl) || d.isDeclToUnfold decl
+
+-- def isInSimpset (simpAttr decl: Name) : CoreM Bool := do
+--   let .some simpDecl ←getSimpExtension? simpAttr | return false
+--   return (← simpDecl.getTheorems).hasAttribute decl
+
+-- end test
 
 /-! # Make Game -/
 
@@ -503,6 +522,64 @@ def GameLevel.setComputedInventory (level : GameLevel) :
 | .Definition, v => {level with definitions := {level.definitions with tiles := v}}
 | .Lemma, v =>      {level with lemmas      := {level.lemmas      with tiles := v}}
 
+/-- Copied from `Mathlib.Tactic.HelpCmd`.
+
+Gets the initial string token in a parser description. For example, for a declaration like
+`syntax "bla" "baz" term : tactic`, it returns `some "bla"`. Returns `none` for syntax declarations
+that don't start with a string constant. -/
+partial def getHeadTk (e : Expr) : Option String :=
+  match (Expr.withApp e λ e a => (e.constName?.getD Name.anonymous, a)) with
+  | (``ParserDescr.node, #[_, _, p]) => getHeadTk p
+  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getHeadTk p
+  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getHeadTk p
+  | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getHeadTk p
+  | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk
+  | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => some tk
+  | (``Parser.withAntiquot, #[_, p]) => getHeadTk p
+  | (``Parser.leadingNode, #[_, _, p]) => getHeadTk p
+  | (``HAndThen.hAndThen, #[_, _, _, _, p, _]) => getHeadTk p
+  | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk
+  | (``Parser.symbol, #[.lit (.strVal tk)]) => some tk
+  | _ => none
+
+/-- Modified from `#help` in `Mathlib.Tactic.HelpCmd` -/
+def getTacticDocstring (env : Environment) (name: Name) : CommandElabM (Option String) := do
+  let name := name.toString (escape := false)
+  let mut decls : Lean.RBMap String (Array SyntaxNodeKind) compare := {}
+
+  let catName : Name := `tactic
+  let catStx : Ident := mkIdent catName -- TODO
+  let some cat := (Parser.parserExtension.getState env).categories.find? catName
+    | throwErrorAt catStx "{catStx} is not a syntax category"
+  liftTermElabM <| Term.addCategoryInfo catStx catName
+  for (k, _) in cat.kinds do
+    let mut used := false
+    if let some tk := do getHeadTk (← (← env.find? k).value?) then
+      let tk := tk.trim
+      if name ≠ tk then -- was `!name.isPrefixOf tk`
+        continue
+      used := true
+      decls := decls.insert tk ((decls.findD tk #[]).push k)
+  for (_name, ks) in decls do
+    for k in ks do
+      if let some doc ← findDocString? env k then
+        return doc
+
+  logWarning <| m!"Could not find a docstring for this tactic, consider adding one " ++
+    m!"using `TacticDoc {name} \"some doc\"`"
+  return none
+
+/-- Retrieve the docstring associated to an inventory item. For Tactics, this
+is not guaranteed to work. -/
+def getDocstring (env : Environment) (name : Name) (type : InventoryType) :
+    CommandElabM (Option String) :=
+  match type with
+  -- for tactics it's a lookup following mathlib's `#help`. not guaranteed to be the correct one.
+  | .Tactic => getTacticDocstring env name
+  | .Lemma => findDocString? env name
+  -- TODO: for definitions not implemented yet, does it work?
+  | .Definition => findDocString? env name
+
 /-- Build the game. This command will precompute various things about the game, such as which
 tactics are available in each level etc. -/
 elab "MakeGame" : command => do
@@ -512,19 +589,35 @@ elab "MakeGame" : command => do
   if game.worlds.hasLoops then
     throwError "World graph must not contain loops! Check your `Path` declarations."
 
+  let env ← getEnv
+
   -- Now create The doc entries from the templates
-  for item in inventoryTemplateExt.getState (← getEnv) do
-    -- TODO: Add information about inventory items
+  for item in inventoryTemplateExt.getState env do
     let name := item.name
+
+    let docstring ← getDocstring env name item.type
+    let content : String := match item.content with
+    | "" =>
+      -- If documentation is missing, try using the docstring instead.
+      match docstring with
+      | some ds => s!"*(lean docstring)*\\\n{ds}" -- TODO `\n` does not work in markdown
+      | none => "(missing)"
+    | template =>
+      -- TODO: Process content template.
+      -- TODO: Add information about inventory items
+      template.replace "[[mathlib_doc]]"
+        s!"[mathlib doc](https://leanprover-community.github.io/mathlib4_docs/find/?pattern={name}#doc)"
+
     match item.type with
     | .Lemma =>
       modifyEnv (inventoryExt.addEntry · { item with
-        -- Add the lemma statement to the doc.
+        content := content
+        -- Add the lemma statement to the doc
         statement := (← getStatementString name)
       })
     | _ =>
-      modifyEnv (inventoryExt.addEntry · {
-        item with
+      modifyEnv (inventoryExt.addEntry · { item with
+        content := content
       })
 
   -- Compute which inventory items are available in which level:
diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean
index 90d1f5d..dd50dd9 100644
--- a/server/GameServer/EnvExtensions.lean
+++ b/server/GameServer/EnvExtensions.lean
@@ -75,7 +75,7 @@ structure InventoryTemplate where
   /-- Free-text short name -/
   displayName: String := name.toString
   /-- Template documentation. Allows for special tags to insert mathlib info [TODO!] -/
-  content: String := "(missing)"
+  content: String := ""
   deriving ToJson, Repr, Inhabited
 
 /-- A full inventory item including the processing by `MakeGame`, which creates these