diff --git a/server/Main.lean b/server/GameServer.lean similarity index 100% rename from server/Main.lean rename to server/GameServer.lean diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index a7fafc8..5b15847 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -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} - | .World => modifyCurWorld fun world => pure {world with introduction := t.getString} - | .Game => modifyCurGame fun game => pure {game with introduction := t.getString} + | .Level => modifyCurLevel fun level => pure {level with introduction := intro} + | .World => modifyCurWorld fun world => pure {world with introduction := intro} + | .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} - | .World => modifyCurWorld fun world => pure {world with conclusion := t.getString} - | .Game => modifyCurGame fun game => pure {game with conclusion := t.getString} + | .Level => modifyCurLevel fun level => pure {level with conclusion := conclusion} + | .World => modifyCurWorld fun world => pure {world with conclusion := conclusion} + | .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 - | 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]}" + let docContent ← parseDocComment doc -- 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 diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean index a1e15f3..fdbd351 100644 --- a/server/GameServer/EnvExtensions.lean +++ b/server/GameServer/EnvExtensions.lean @@ -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 -/ diff --git a/server/GameServer/Helpers.lean b/server/GameServer/Helpers.lean new file mode 100644 index 0000000..4a59e75 --- /dev/null +++ b/server/GameServer/Helpers.lean @@ -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 [] diff --git a/server/GameServer/Inventory.lean b/server/GameServer/Inventory.lean new file mode 100644 index 0000000..bff10d4 --- /dev/null +++ b/server/GameServer/Inventory.lean @@ -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}} diff --git a/server/GameServer/Options.lean b/server/GameServer/Options.lean new file mode 100644 index 0000000..f467876 --- /dev/null +++ b/server/GameServer/Options.lean @@ -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." +} diff --git a/server/GameServer/SaveData.lean b/server/GameServer/SaveData.lean new file mode 100644 index 0000000..4718717 --- /dev/null +++ b/server/GameServer/SaveData.lean @@ -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)) diff --git a/server/lakefile.lean b/server/lakefile.lean index dc2f526..fc337ce 100644 --- a/server/lakefile.lean +++ b/server/lakefile.lean @@ -12,7 +12,7 @@ lean_lib GameServer @[default_target] lean_exe gameserver { - root := `Main + root := `GameServer supportInterpreter := true }