cleanup; including using doc comment syntax for documentation like TacticDoc

2023-12-11 19:38:58 +01:00
8 changed files with 460 additions and 383 deletions
@@ -1,23 +1,12 @@
-import GameServer.EnvExtensions
+import GameServer.Helpers
 import GameServer.Inventory
 import GameServer.Options
 import GameServer.SaveData
 open Lean Meta Elab Command
 set_option autoImplicit false
 /-- Let `MakeGame` print the reasons why the worlds depend on each other. -/
 register_option lean4game.showDependencyReasons : Bool := {
  defValue := false
  descr := "show reasons for calculated world dependencies."
 }
 /-- Let `MakeGame` print the reasons why the worlds depend on each other.
 Note: currently unused in favour of setting `set_option trace.debug true`. -/
 register_option lean4game.verbose : Bool := {
  defValue := false
  descr := "display more info messages to help developing the game."
 }
 /-! # Game metadata -/
 /-- Switch to the specified `Game` (and create it if non-existent). Example: `Game "NNG"` -/
@@ -52,13 +41,15 @@ elab "Title" t:str : command => do
 /-- Define the introduction of the current game/world/level. -/
 elab "Introduction" t:str : command => do
  let intro := t.getString
  match ← getCurLayer with
-  | .Level => modifyCurLevel fun level => pure {level with introduction := t.getString}
+  | .Level => modifyCurLevel fun level => pure {level with introduction := intro}
-  | .World => modifyCurWorld  fun world => pure {world with introduction := t.getString}
+  | .World => modifyCurWorld  fun world => pure {world with introduction := intro}
-  | .Game => modifyCurGame  fun game => pure {game with introduction := t.getString}
+  | .Game => modifyCurGame  fun game => pure {game with introduction := intro}
 /-- Define the info of the current game. Used for e.g. credits -/
 elab "Info" t:str : command => do
  let info:= t.getString
  match ← getCurLayer with
  | .Level =>
    logError "Can't use `Info` in a level!"
@@ -66,7 +57,7 @@ elab "Info" t:str : command => do
  | .World =>
    logError "Can't use `Info` in a world"
    pure ()
-  | .Game => modifyCurGame  fun game => pure {game with info := t.getString}
+  | .Game => modifyCurGame  fun game => pure {game with info := info}
 /-- Provide the location of the image for the current game/world/level.
 Paths are relative to the lean project's root. -/
@@ -90,10 +81,11 @@ elab "Image" t:str : command => do
 /-- Define the conclusion of the current game or current level if some
 building a level. -/
 elab "Conclusion" t:str : command => do
  let conclusion := t.getString
  match ← getCurLayer with
-  | .Level => modifyCurLevel fun level => pure {level with conclusion := t.getString}
+  | .Level => modifyCurLevel fun level => pure {level with conclusion := conclusion}
-  | .World => modifyCurWorld  fun world => pure {world with conclusion := t.getString}
+  | .World => modifyCurWorld  fun world => pure {world with conclusion := conclusion}
-  | .Game => modifyCurGame  fun game => pure {game with conclusion := t.getString}
+  | .Game => modifyCurGame  fun game => pure {game with conclusion := conclusion}
 /-- A list of games that should be played before this one. Example `Prerequisites "NNG" "STG"`. -/
 elab "Prerequisites" t:str* : command => do
@@ -102,13 +94,15 @@ elab "Prerequisites" t:str* : command => do
 /-- Short caption for the game (1 sentence) -/
 elab "CaptionShort" t:str : command => do
  let caption := t.getString
  modifyCurGame fun game => pure {game with
-    tile := {game.tile with short := t.getString}}
+    tile := {game.tile with short := caption}}
 /-- More detailed description what the game is about (2-4 sentences). -/
 elab "CaptionLong" t:str : command => do
  let caption := t.getString
  modifyCurGame fun game => pure {game with
-    tile := {game.tile with long := t.getString}}
+    tile := {game.tile with long := caption}}
 /-- A list of Languages the game is translated to. For example `Languages "German" "English"`.
 NOTE: For the time being, only a single language is supported.
@@ -136,113 +130,6 @@ in the first level and get enabled during the game.
 /-! ## Doc entries -/
 /-- 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 tactic {name}, 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
 /-- 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.
 `ref` is the syntax piece. If `name` is not provided, it will use `ident.getId`.
 I used this workaround, because I needed a new name (with correct namespace etc)
 to be used, and I don't know how to create a new ident with same position but different name.
 -/
 def checkInventoryDoc (type : InventoryType) (ref : Ident) (name : Name := ref.getId)
    (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
  -- Find a key with matching `(type, name)`.
  match (inventoryTemplateExt.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 =>
      let docstring ← match (← getDocstring env name type) with
      | some ds =>
        logInfoAt ref (m!"Missing {type} Documentation. Using existing docstring. " ++
        m!"Add {name}\nAdd `{type}Doc {name}` somewhere above this statement.")
        pure s!"*(lean docstring)*\\\n{ds}"
      | none =>
        logWarningAt ref (m!"Missing {type} Documentation: {name}\nAdd `{type}Doc {name}` " ++
        m!"somewhere above this statement.")
        pure "(missing)"
      -- We just add a dummy entry
      modifyEnv (inventoryTemplateExt.addEntry · {
        type := type
        name := name
        category := if type == .Lemma then s!"{n.getPrefix}" else ""
        content := docstring})
    -- Add the default documentation
    | some s =>
      modifyEnv (inventoryTemplateExt.addEntry · {
        type := type
        name := name
        category := if type == .Lemma then s!"{n.getPrefix}" else ""
        content := s })
      logInfoAt ref (m!"Missing {type} Documentation: {name}, used default (e.g. provided " ++
        m!"docstring) instead. If you want to write a different description, add " ++
        m!"`{type}Doc {name}` somewhere above this statement.")
 /-- Documentation entry of a tactic. Example:
 ```
@@ -252,12 +139,13 @@ TacticDoc rw "`rw` stands for rewrite, etc. "
 * The identifier is the tactics name. Some need to be escaped like `«have»`.
 * The description is a string supporting Markdown.
 -/
-elab "TacticDoc" name:ident content:str : command =>
+elab doc:docComment ? "TacticDoc" name:ident content:str ? : command => do
  let doc ← parseDocCommentLegacy doc content
  modifyEnv (inventoryTemplateExt.addEntry · {
    type := .Tactic
    name := name.getId
    displayName := name.getId.toString
-    content := content.getString })
+    content := doc })
 /-- Documentation entry of a lemma. Example:
@@ -274,13 +162,15 @@ LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
 Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires
 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 =>
+elab doc:docComment ? "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str ? :
    command => do
  let doc ← parseDocCommentLegacy doc content
  modifyEnv (inventoryTemplateExt.addEntry · {
    type := .Lemma
    name := name.getId
    category := category.getString
    displayName := displayName.getString
-    content := content.getString })
+    content := doc })
 -- 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`
@@ -302,33 +192,16 @@ DefinitionDoc Function.Bijective as "Bijective" "defined as `Injective f ∧ Sur
 Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires
 The lemma/definition to have the same fully qualified name as in mathlib.
 -/
-elab "DefinitionDoc" name:ident "as" displayName:str template:str : command =>
+elab doc:docComment ? "DefinitionDoc" name:ident "as" displayName:str template:str ? : command => do
  let doc ← parseDocCommentLegacy doc template
  modifyEnv (inventoryTemplateExt.addEntry · {
    type := .Definition
    name := name.getId,
    displayName := displayName.getString,
-    content := template.getString })
+    content := doc })
 /-! ## Add inventory items -/
 def getStatement (name : Name) : CommandElabM MessageData := do
  return ← addMessageContextPartial (.ofPPFormat { pp := fun
    | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature name
    | 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`.
 Note: A statement like `theorem abc : ∀ x : Nat, x ≥ 0` would be turned into
 `theorem abc (x : Nat) : x ≥ 0` by `PrettyPrinter.ppSignature`. -/
 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
@@ -405,54 +278,12 @@ elab "LemmaTab"  category:str : command =>
 /-! # Exercise Statement -/
 /-- A `attr := ...` option for `Statement`. Add attributes to the defined theorem. -/
 syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
 -- TODO
 -- TODO: Reuse the following code for checking available tactics in user code:
 structure UsedInventory where
 (tactics : HashSet Name := {})
 (definitions : HashSet Name := {})
 (lemmas : HashSet Name := {})
 partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : CommandElabM UsedInventory := do
  match stx with
  | .missing => return acc
  | .node _info kind args =>
    if kind == `GameServer.Tactic.Hint || kind == `GameServer.Tactic.Branch then return acc
    return ← args.foldlM (fun acc arg => collectUsedInventory arg acc) acc
  | .atom _info val =>
    -- ignore syntax elements that do not start with a letter
    -- and ignore some standard keywords
    let allowed := ["with", "fun", "at", "only", "by"]
    if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
      let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
      return {acc with tactics := acc.tactics.insert val}
    else
      return acc
  | .ident _info _rawVal val _preresolved =>
      let ns ←
        try resolveGlobalConst (mkIdent val)
        catch | _ => pure [] -- catch "unknown constant" error
      return ← ns.foldlM (fun acc n => do
        if let some (.thmInfo ..) := (← getEnv).find? n then
          return {acc with lemmas := acc.lemmas.insertMany ns}
        else
          return {acc with definitions := acc.definitions.insertMany ns}
      ) acc
 -- #check expandOptDocComment?
 /-- Define the statement of the current level. -/
 elab doc:docComment ? attrs:Parser.Term.attributes ?
    "Statement" statementName:ident ? sig:declSig val:declVal : command => do
  let lvlIdx ← getCurLevelIdx
-  let docContent : Option String := match doc with
+  let docContent ← parseDocComment doc
  | none => none
  | some s => match s.raw[1] with
    | .atom _ val => val.dropRight 2 |>.trim -- some (val.extract 0 (val.endPos - ⟨2⟩))
    | _           => none --panic "not implemented error message" --throwErrorAt s "unexpected doc string{indentD s.raw[1]}"
  -- Save the messages before evaluation of the proof.
  let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
@@ -553,23 +384,6 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
 /-! # Hints -/
 syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
 /-- Remove any spaces at the beginning of a new line -/
 partial def removeIndentation (s : String) : String :=
  let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
    let c := s.get i
    let i := s.next i
    if s.atEnd i then
      acc.push c
    else if removeSpaces && c == ' ' then
      loop i acc (removeSpaces := true)
    else if c == '\n' then
      loop i (acc.push c) (removeSpaces := true)
    else
      loop i (acc.push c)
  loop ⟨0⟩ ""
 /-- A tactic that can be used inside `Statement`s to indicate in which proof states players should
 see hints. The tactic does not affect the goal state.
 -/
@@ -683,26 +497,6 @@ elab "Template" tacs:tacticSeq : tactic => do
    return {level with template := s!"{template}"}
 open IO.FS System FilePath in
 /-- Copies the folder `images/` to `.lake/gamedata/images/` -/
 def copyImages : IO Unit := do
  let target : FilePath := ".lake" / "gamedata"
  if ← FilePath.pathExists "images" then
    for file in ← walkDir "images" do
      let outFile := target.join file
      -- create the directories
      if ← file.isDir then
        createDirAll outFile
      else
        if let some parent := outFile.parent then
          createDirAll parent
        -- copy file
        let content ← readBinFile file
        writeBinFile outFile content
 -- TODO: Notes for testing if a declaration has the simp attribute
 -- -- Test: From zulip
@@ -721,139 +515,6 @@ def copyImages : IO Unit := do
 /-! # Make Game -/
 #eval IO.FS.createDirAll ".lake/gamedata/"
 -- TODO: register all of this as ToJson instance?
 def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : CommandElabM Unit := do
  let game ← getCurGame
  let env ← getEnv
  let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata"
  if ← path.isDir then
    IO.FS.removeDirAll path
  IO.FS.createDirAll path
  -- copy the images folder
  copyImages
  for (worldId, world) in game.worlds.nodes.toArray do
    for (levelId, level) in world.levels.toArray do
      IO.FS.writeFile (path / s!"level__{worldId}__{levelId}.json") (toString (toJson (level.toInfo env)))
  IO.FS.writeFile (path / s!"game.json") (toString (getGameJson game))
  for inventoryType in [InventoryType.Lemma, .Tactic, .Definition] do
    for name in allItemsByType.findD inventoryType {} do
      let some item ← getInventoryItem? name inventoryType
        | throwError "Expected item to exist: {name}"
      IO.FS.writeFile (path / s!"doc__{inventoryType}__{name}.json") (toString (toJson item))
  let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do
    (allItemsByType.findD type {}).toArray.mapM (fun name => do
      let some item ← getInventoryItem? name type
        | throwError "Expected item to exist: {name}"
      return item.toTile)
  let inventory : InventoryOverview := {
    lemmas := ← getTiles .Lemma
    tactics := ← getTiles .Tactic
    definitions := ← getTiles .Definition
    lemmaTab := none
  }
  IO.FS.writeFile (path / s!"inventory.json") (toString (toJson inventory))
 def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo
 | .Tactic => level.tactics
 | .Definition => level.definitions
 | .Lemma => level.lemmas
 def GameLevel.setComputedInventory (level : GameLevel) :
    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}}
 partial def removeTransitiveAux (id : Name) (arrows : HashMap Name (HashSet Name))
      (newArrows : HashMap Name (HashSet Name)) (decendants : HashMap Name (HashSet Name)) :
    HashMap Name (HashSet Name) × HashMap Name (HashSet Name) := Id.run do
  match (newArrows.find? id, decendants.find? id) with
  | (some _, some _) => return (newArrows, decendants)
  | _ =>
    let mut newArr := newArrows
    let mut desc := decendants
    desc := desc.insert id {} -- mark as worked in case of loops
    newArr := newArr.insert id {} -- mark as worked in case of loops
    let children := arrows.findD id {}
    let mut trimmedChildren := children
    let mut theseDescs := children
    for child in children do
      (newArr, desc) := removeTransitiveAux child arrows newArr desc
      let childDescs := desc.findD child {}
      theseDescs := theseDescs.insertMany childDescs
      for d in childDescs do
        trimmedChildren := trimmedChildren.erase d
    desc := desc.insert id theseDescs
    newArr := newArr.insert id trimmedChildren
    return (newArr, desc)
 def removeTransitive (arrows : HashMap Name (HashSet Name)) : CommandElabM (HashMap Name (HashSet Name)) := do
  let mut newArr := {}
  let mut desc := {}
  for id in arrows.toArray.map Prod.fst do
    (newArr, desc) := removeTransitiveAux id arrows newArr desc
    if (desc.findD id {}).contains id then
      logError <| m!"Loop at {id}. " ++
        m!"This should not happen and probably means that `findLoops` has a bug."
      -- DEBUG:
      -- for ⟨x, hx⟩ in desc.toList do
      --   m := m ++ m!"{x}: {hx.toList}\n"
      -- logError m
  return newArr
 /-- The recursive part of `findLoops`. Finds loops that appear as successors of `node`.
 For performance reason it returns a HashSet of visited
 nodes as well. This is filled with all nodes ever looked at as they cannot be
 part of a loop anymore. -/
 partial def findLoopsAux (arrows : HashMap Name (HashSet Name)) (node : Name)
    (path : Array Name := #[]) (visited : HashSet Name := {}) :
    Array Name × HashSet Name := Id.run do
  let mut visited := visited
  match path.getIdx? node with
  | some i =>
    -- Found a loop: `node` is already the iᵗʰ element of the path
    return (path.extract i path.size, visited.insert node)
  | none =>
    for successor in arrows.findD node {} do
      -- If we already visited the successor, it cannot be part of a loop anymore
      if visited.contains successor then
        continue
      -- Find any loop involving `successor`
      let (loop, _) := findLoopsAux arrows successor (path.push node) visited
      visited := visited.insert successor
      -- No loop found in the dependants of `successor`
      if loop.isEmpty then
        continue
      -- Found a loop, return it
      return (loop, visited)
  return (#[], visited.insert node)
 /-- Find a loop in the graph and return it. Returns `[]` if there are no loops. -/
 partial def findLoops (arrows : HashMap Name (HashSet Name)) : List Name := Id.run do
  let mut visited : HashSet Name := {}
  for node in arrows.toArray.map (·.1) do
    -- Skip a node if it was already visited
    if visited.contains node then
      continue
    -- `findLoopsAux` returns a loop or `[]` together with a set of nodes it visited on its
    -- search starting from `node`
    let (loop, moreVisited) := (findLoopsAux arrows node (visited := visited))
    visited := moreVisited
    if !loop.isEmpty then
      return loop.toList
  return []
 /-- The worlds of a game are joint by dependencies. These are
 automatically computed but can also be defined with the syntax
 `Dependency World₁ → World₂ → World₃`. -/
@@ -1191,17 +852,3 @@ elab "MakeGame" : command => do
    allItemsByType := allItemsByType.insert inventoryType allItems
  saveGameData allItemsByType
 /-! # Debugging tools -/
 -- /-- Print current game for debugging purposes. -/
 -- elab "PrintCurGame" : command => do
 --   logInfo (toJson (← getCurGame))
 /-- Print current level for debugging purposes. -/
 elab "PrintCurLevel" : command => do
  logInfo (repr (← getCurLevel))
 /-- Print levels for debugging purposes. -/
 elab "PrintLevels" : command => do
  logInfo $ repr $ (← getCurWorld).levels.toArray
@@ -148,6 +148,12 @@ structure InventoryOverview where
  lemmaTab : Option String
 deriving ToJson, FromJson
 -- TODO: Reuse the following code for checking available tactics in user code:
 structure UsedInventory where
 (tactics : HashSet Name := {})
 (definitions : HashSet Name := {})
 (lemmas : HashSet Name := {})
 /-! ## Environment extensions for game specification -/
 /-- Register a (non-persistent) environment extension to hold the current level -/
@@ -0,0 +1,190 @@
 import Lean
 /-! This document contains various things which cluttered `Commands.lean`. -/
 open Lean Meta Elab Command
 syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
 /-! ## Doc Comment Parsing -/
 /-- Read a doc comment and get its content. Return `""` if no doc comment available. -/
 def parseDocComment! (doc: Option (TSyntax `Lean.Parser.Command.docComment)) :
    CommandElabM String := do
  match doc with
  | none =>
    logWarning "Add a text to this command with `/-- yada yada -/ MyCommand`!"
    pure ""
  | some s => match s.raw[1] with
    | .atom _ val => pure <| val.dropRight 2 |>.trim -- some (val.extract 0 (val.endPos - ⟨2⟩))
    | _           => pure "" --panic "not implemented error message" --throwErrorAt s "unexpected doc string{indentD s.raw[1]}"
 /-- Read a doc comment and get its content. Return `none` if no doc comment available. -/
 def parseDocComment (doc: Option (TSyntax `Lean.Parser.Command.docComment)) :
    CommandElabM <| Option String := do
  match doc with
  | none => pure none
  | some _ => parseDocComment! doc
 /-- TODO: This is only used to provide some backwards compatibility and you can
 replace `parseDocCommentLegacy` with `parseDocComment` in the future. -/
 def parseDocCommentLegacy (doc: Option (TSyntax `Lean.Parser.Command.docComment))
    (t : Option (TSyntax `str)) : CommandElabM <| String := do
  match doc with
  | none =>
    match t with
    | none =>
      pure <| ← parseDocComment! doc
    | some t =>
      logWarningAt t "You should use the new Syntax:
      /-- yada yada -/
      YourCommand
      instead of
      YourCommand \"yada yada\"
      "
      pure t.getString
  | some _ =>
    match t with
      | none =>
        pure <| ← parseDocComment! doc
      | some t =>
        logErrorAt t "You must not provide both, a docstring and a string following the command!
        Only use
        /-- yada yada -/
        YourCommand
        and remove the string following it!"
        pure <| ← parseDocComment! doc
 /-! ## Statement string -/
 def getStatement (name : Name) : CommandElabM MessageData := do
  return ← addMessageContextPartial (.ofPPFormat { pp := fun
    | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature name
    | 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`.
 Note: A statement like `theorem abc : ∀ x : Nat, x ≥ 0` would be turned into
 `theorem abc (x : Nat) : x ≥ 0` by `PrettyPrinter.ppSignature`. -/
 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.
 /-- A `attr := ...` option for `Statement`. Add attributes to the defined theorem. -/
 syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
 -- TODO
 /-- Remove any spaces at the beginning of a new line -/
 partial def removeIndentation (s : String) : String :=
  let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
    let c := s.get i
    let i := s.next i
    if s.atEnd i then
      acc.push c
    else if removeSpaces && c == ' ' then
      loop i acc (removeSpaces := true)
    else if c == '\n' then
      loop i (acc.push c) (removeSpaces := true)
    else
      loop i (acc.push c)
  loop ⟨0⟩ ""
 /-! ## Loops in Graph-like construct
 TODO: Why are we not using graphs here but our own construct `HashMap Name (HashSet Name)`?
 -/
 partial def removeTransitiveAux (id : Name) (arrows : HashMap Name (HashSet Name))
      (newArrows : HashMap Name (HashSet Name)) (decendants : HashMap Name (HashSet Name)) :
    HashMap Name (HashSet Name) × HashMap Name (HashSet Name) := Id.run do
  match (newArrows.find? id, decendants.find? id) with
  | (some _, some _) => return (newArrows, decendants)
  | _ =>
    let mut newArr := newArrows
    let mut desc := decendants
    desc := desc.insert id {} -- mark as worked in case of loops
    newArr := newArr.insert id {} -- mark as worked in case of loops
    let children := arrows.findD id {}
    let mut trimmedChildren := children
    let mut theseDescs := children
    for child in children do
      (newArr, desc) := removeTransitiveAux child arrows newArr desc
      let childDescs := desc.findD child {}
      theseDescs := theseDescs.insertMany childDescs
      for d in childDescs do
        trimmedChildren := trimmedChildren.erase d
    desc := desc.insert id theseDescs
    newArr := newArr.insert id trimmedChildren
    return (newArr, desc)
 def removeTransitive (arrows : HashMap Name (HashSet Name)) : CommandElabM (HashMap Name (HashSet Name)) := do
  let mut newArr := {}
  let mut desc := {}
  for id in arrows.toArray.map Prod.fst do
    (newArr, desc) := removeTransitiveAux id arrows newArr desc
    if (desc.findD id {}).contains id then
      logError <| m!"Loop at {id}. " ++
        m!"This should not happen and probably means that `findLoops` has a bug."
      -- DEBUG:
      -- for ⟨x, hx⟩ in desc.toList do
      --   m := m ++ m!"{x}: {hx.toList}\n"
      -- logError m
  return newArr
 /-- The recursive part of `findLoops`. Finds loops that appear as successors of `node`.
 For performance reason it returns a HashSet of visited
 nodes as well. This is filled with all nodes ever looked at as they cannot be
 part of a loop anymore. -/
 partial def findLoopsAux (arrows : HashMap Name (HashSet Name)) (node : Name)
    (path : Array Name := #[]) (visited : HashSet Name := {}) :
    Array Name × HashSet Name := Id.run do
  let mut visited := visited
  match path.getIdx? node with
  | some i =>
    -- Found a loop: `node` is already the iᵗʰ element of the path
    return (path.extract i path.size, visited.insert node)
  | none =>
    for successor in arrows.findD node {} do
      -- If we already visited the successor, it cannot be part of a loop anymore
      if visited.contains successor then
        continue
      -- Find any loop involving `successor`
      let (loop, _) := findLoopsAux arrows successor (path.push node) visited
      visited := visited.insert successor
      -- No loop found in the dependants of `successor`
      if loop.isEmpty then
        continue
      -- Found a loop, return it
      return (loop, visited)
  return (#[], visited.insert node)
 /-- Find a loop in the graph and return it. Returns `[]` if there are no loops. -/
 partial def findLoops (arrows : HashMap Name (HashSet Name)) : List Name := Id.run do
  let mut visited : HashSet Name := {}
  for node in arrows.toArray.map (·.1) do
    -- Skip a node if it was already visited
    if visited.contains node then
      continue
    -- `findLoopsAux` returns a loop or `[]` together with a set of nodes it visited on its
    -- search starting from `node`
    let (loop, moreVisited) := (findLoopsAux arrows node (visited := visited))
    visited := moreVisited
    if !loop.isEmpty then
      return loop.toList
  return []
@@ -0,0 +1,152 @@
 import Lean
 import GameServer.EnvExtensions
 open Lean Elab Command
 /-- 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
 /-! ## Doc entries -/
 /-- 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 tactic {name}, 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
 /-- 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.
 `ref` is the syntax piece. If `name` is not provided, it will use `ident.getId`.
 I used this workaround, because I needed a new name (with correct namespace etc)
 to be used, and I don't know how to create a new ident with same position but different name.
 -/
 def checkInventoryDoc (type : InventoryType) (ref : Ident) (name : Name := ref.getId)
    (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
  -- Find a key with matching `(type, name)`.
  match (inventoryTemplateExt.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 =>
      let docstring ← match (← getDocstring env name type) with
      | some ds =>
        logInfoAt ref (m!"Missing {type} Documentation. Using existing docstring. " ++
        m!"Add {name}\nAdd `{type}Doc {name}` somewhere above this statement.")
        pure s!"*(lean docstring)*\\\n{ds}"
      | none =>
        logWarningAt ref (m!"Missing {type} Documentation: {name}\nAdd `{type}Doc {name}` " ++
        m!"somewhere above this statement.")
        pure "(missing)"
      -- We just add a dummy entry
      modifyEnv (inventoryTemplateExt.addEntry · {
        type := type
        name := name
        category := if type == .Lemma then s!"{n.getPrefix}" else ""
        content := docstring})
    -- Add the default documentation
    | some s =>
      modifyEnv (inventoryTemplateExt.addEntry · {
        type := type
        name := name
        category := if type == .Lemma then s!"{n.getPrefix}" else ""
        content := s })
      logInfoAt ref (m!"Missing {type} Documentation: {name}, used default (e.g. provided " ++
        m!"docstring) instead. If you want to write a different description, add " ++
        m!"`{type}Doc {name}` somewhere above this statement.")
 partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : CommandElabM UsedInventory := do
  match stx with
  | .missing => return acc
  | .node _info kind args =>
    if kind == `GameServer.Tactic.Hint || kind == `GameServer.Tactic.Branch then return acc
    return ← args.foldlM (fun acc arg => collectUsedInventory arg acc) acc
  | .atom _info val =>
    -- ignore syntax elements that do not start with a letter
    -- and ignore some standard keywords
    let allowed := ["with", "fun", "at", "only", "by"]
    if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
      let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
      return {acc with tactics := acc.tactics.insert val}
    else
      return acc
  | .ident _info _rawVal val _preresolved =>
      let ns ←
        try resolveGlobalConst (mkIdent val)
        catch | _ => pure [] -- catch "unknown constant" error
      return ← ns.foldlM (fun acc n => do
        if let some (.thmInfo ..) := (← getEnv).find? n then
          return {acc with lemmas := acc.lemmas.insertMany ns}
        else
          return {acc with definitions := acc.definitions.insertMany ns}
      ) acc
 -- #check expandOptDocComment?
 def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo
 | .Tactic => level.tactics
 | .Definition => level.definitions
 | .Lemma => level.lemmas
 def GameLevel.setComputedInventory (level : GameLevel) :
    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}}
@@ -0,0 +1,17 @@
 import Lean
 /-! This document contains custom options available in the game. -/
 /-- Let `MakeGame` print the reasons why the worlds depend on each other. -/
 register_option lean4game.showDependencyReasons : Bool := {
  defValue := false
  descr := "show reasons for calculated world dependencies."
 }
 /-- Let `MakeGame` print the reasons why the worlds depend on each other.
 Note: currently unused in favour of setting `set_option trace.debug true`. -/
 register_option lean4game.verbose : Bool := {
  defValue := false
  descr := "display more info messages to help developing the game."
 }
@@ -0,0 +1,65 @@
 import GameServer.EnvExtensions
 open Lean Meta Elab Command
 /-! ## Copy images -/
 open IO.FS System FilePath in
 /-- Copies the folder `images/` to `.lake/gamedata/images/` -/
 def copyImages : IO Unit := do
  let target : FilePath := ".lake" / "gamedata"
  if ← FilePath.pathExists "images" then
    for file in ← walkDir "images" do
      let outFile := target.join file
      -- create the directories
      if ← file.isDir then
        createDirAll outFile
      else
        if let some parent := outFile.parent then
          createDirAll parent
        -- copy file
        let content ← readBinFile file
        writeBinFile outFile content
 -- TODO: I'm not sure this should be happening here...
 #eval IO.FS.createDirAll ".lake/gamedata/"
 -- TODO: register all of this as ToJson instance?
 def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : CommandElabM Unit := do
  let game ← getCurGame
  let env ← getEnv
  let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata"
  if ← path.isDir then
    IO.FS.removeDirAll path
  IO.FS.createDirAll path
  -- copy the images folder
  copyImages
  for (worldId, world) in game.worlds.nodes.toArray do
    for (levelId, level) in world.levels.toArray do
      IO.FS.writeFile (path / s!"level__{worldId}__{levelId}.json") (toString (toJson (level.toInfo env)))
  IO.FS.writeFile (path / s!"game.json") (toString (getGameJson game))
  for inventoryType in [InventoryType.Lemma, .Tactic, .Definition] do
    for name in allItemsByType.findD inventoryType {} do
      let some item ← getInventoryItem? name inventoryType
        | throwError "Expected item to exist: {name}"
      IO.FS.writeFile (path / s!"doc__{inventoryType}__{name}.json") (toString (toJson item))
  let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do
    (allItemsByType.findD type {}).toArray.mapM (fun name => do
      let some item ← getInventoryItem? name type
        | throwError "Expected item to exist: {name}"
      return item.toTile)
  let inventory : InventoryOverview := {
    lemmas := ← getTiles .Lemma
    tactics := ← getTiles .Tactic
    definitions := ← getTiles .Definition
    lemmaTab := none
  }
  IO.FS.writeFile (path / s!"inventory.json") (toString (toJson inventory))
@@ -12,7 +12,7 @@ lean_lib GameServer
@[default_target]
 lean_exe gameserver {
-  root := `Main
+  root := `GameServer
  supportInterpreter := true
 }