rename and tidy up

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,

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[],
+  tactics: InventoryTile[],
-  lemmas: ComputedInventoryItem[],
+  lemmas: InventoryTile[],
-  definitions: ComputedInventoryItem[],
+  definitions: InventoryTile[],
   descrText: null|string,
   descrFormat: null|string,
   lemmaTab: null|string,

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
+    InventoryType → Array InventoryTile → GameLevel
-| .Tactic, v =>     {level with tactics     := {level.tactics     with computed := v}}
+| .Tactic, v =>     {level with tactics     := {level.tactics     with tiles := v}}
-| .Definition, v => {level with definitions := {level.definitions with computed := v}}
+| .Definition, v => {level with definitions := {level.definitions with tiles := v}}
-| .Lemma, v =>      {level with lemmas      := {level.lemmas      with computed := 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₀

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`. -/
+/-- The keys/templates of the inventory items, stored in `InventoryTemplateExt`. -/
-structure InventoryKey where
+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
+/-- A full inventory item including the processing by `MakeGame`, which creates these
-from the `InventoryKey`s and modifies them. -/
+from the `InventoryTemplate`s and modifies them. -/
-structure InventoryItem extends InventoryKey where -- TODO: can I remove the field `template`? Probably not...
+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
+/-- A reduced variant of `InventoryItem` which is used for the tiles in the doc -/
-entries! -/
+structure InventoryTile where
-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
   /--
   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. -/
+/-- The extension that stores the doc templates. Note that you can only add, but never modify
--- initialize inventoryDocExt : SimplePersistentEnvExtension InventoryDocEntry (Array InventoryDocEntry) ←
+entries! -/
---   registerSimplePersistentEnvExtension {
+initialize inventoryTemplateExt :
---     name := `inventory_doc_old
+    SimplePersistentEnvExtension InventoryTemplate (Array InventoryTemplate) ←
---     addEntryFn := Array.push
+  registerSimplePersistentEnvExtension {
---     addImportedFn := Array.concatMap id
+    name := `inventory_keys
---   }
+    addEntryFn := Array.push
+    addImportedFn := Array.concatMap id }
 
--- def getInventoryDoc? {m : Type → Type} [Monad m] [MonadEnv m] (n : Name) (type : InventoryType) :
+/-- Receive the template with that matches `(name, type)` -/
---     m (Option InventoryDocEntry) := do
+def getInventoryTemplate? [Monad m] [MonadEnv m] (n : Name) (type : InventoryType) :
---   return (inventoryDocExt.getState (← getEnv)).find? (fun x => x.name == n && x.type == type)
+    m (Option InventoryTemplate) := do
+  return (inventoryTemplateExt.getState (← getEnv)).find? (fun x => x.name == n && x.type == type)
 
--- open Elab Command in
+/-- The extension that contains the inventory content after it has been processed.
--- /-- Print a registered tactic doc for debugging purposes. -/
+`MakeGame` is the only command adding items here. -/
--- elab "#print_doc" : command => do
+initialize inventoryExt : SimplePersistentEnvExtension InventoryItem (Array InventoryItem) ←
---   for entry in inventoryDocExt.getState (← getEnv) do
+  registerSimplePersistentEnvExtension {
---     dbg_trace "[{entry.type}] {entry.name} : {entry.content}"
+    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)
 
 
-/-! ## 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`.
+`Game`, `World`, and `Level`. Commands like `Introduction` depend on the current 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

server/GameServer/Game.lean

@@ -40,9 +40,9 @@ Fields:
 structure LevelInfo where
   index : Nat
   title : String
-  tactics : Array ComputedInventoryItem
+  tactics : Array InventoryTile
-  lemmas : Array ComputedInventoryItem
+  lemmas : Array InventoryTile
-  definitions : Array ComputedInventoryItem
+  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
+  tactics : Array InventoryTile
-  lemmas : Array ComputedInventoryItem
+  lemmas : Array InventoryTile
-  definitions : Array ComputedInventoryItem
+  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
+      tactics := lvl.tactics.tiles
-      lemmas := lvl.lemmas.computed
+      lemmas := lvl.lemmas.tiles
-      definitions := lvl.definitions.computed
+      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,
+            tactics := lvl.tactics.tiles,
-            lemmas := lvl.lemmas.computed,
+            lemmas := lvl.lemmas.tiles,
-            definitions := lvl.definitions.computed,
+            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