add Template server-side

server/GameServer/Commands.lean

@@ -283,7 +283,7 @@ partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : Co
   match stx with
   | .missing => return acc
   | .node _info kind args =>
-    if kind == `tacticHint__ || kind == `tacticBranch_ then return acc
+    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
@@ -439,7 +439,7 @@ partial def removeIndentation (s : String) : String :=
 /-- 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.
 -/
-elab "Hint" args:hintArg* msg:interpolatedStr(term) : tactic => do
+elab (name := GameServer.Tactic.Hint) "Hint" args:hintArg* msg:interpolatedStr(term) : tactic => do
   let mut strict := false
   let mut hidden := false
 
@@ -490,7 +490,7 @@ elab "Hint" args:hintArg* msg:interpolatedStr(term) : tactic => do
 
 /-- This tactic allows us to execute an alternative sequence of tactics, but without affecting the
 proof state. We use it to define Hints for alternative proof methods or dead ends. -/
-elab "Branch" t:tacticSeq : tactic => do
+elab (name := GameServer.Tactic.Branch) "Branch" t:tacticSeq : tactic => do
   let b ← saveState
   Tactic.evalTactic t
 
@@ -505,40 +505,48 @@ elab "Branch" t:tacticSeq : tactic => do
   b.restore
   Core.setMessageLog msgs
 
+/-- A hole inside a template proof that will be replaced by `sorry`. -/
+elab (name := GameServer.Tactic.Hole) "Hole" t:tacticSeq : tactic => do
+  Tactic.evalTactic t
 
+/--
+Iterate recursively through the Syntax, replace `Hole` with `sorry` and remove all
+`Hint`/`Branch` occurences.
+-/
+def replaceHoles (tacs : Syntax) : Syntax :=
+  match tacs with
+  | Syntax.node info kind ⟨args⟩ =>
+    let newArgs := filterArgs args
+    Syntax.node info kind ⟨newArgs⟩
+  | other => other
+where filterArgs (args : List Syntax) : List Syntax :=
+  match args with
+    | [] => []
+    -- replace `Hole` with `sorry`.
+    | Syntax.node info `GameServer.Tactic.Hole _ :: r =>
+      Syntax.node info `Lean.Parser.Tactic.tacticSorry #[Syntax.atom info "sorry"] :: filterArgs r
+    -- delete all `Hint` and `Branch` occurences in the middle.
+    | Syntax.node _ `GameServer.Tactic.Hint _ :: _ :: r
+    | Syntax.node _ `GameServer.Tactic.Branch _ :: _ :: r =>
+      filterArgs r
+    -- delete `Hint` and `Branch` occurence at the end of the tactic sequence.
+    | Syntax.node _ `GameServer.Tactic.Hint _ :: []
+    | Syntax.node _ `GameServer.Tactic.Branch _ :: [] =>
+        []
+    -- Recurse on all other Syntax.
+    | a :: rest =>
+      replaceHoles a :: filterArgs rest
 
 /-- The tactic block inside `Template` will be copied into the users editor.
 Use `Hole` inside the template for a part of the proof that should be replaced
 with `sorry`. -/
 elab "Template" tacs:tacticSeq : tactic => do
-  --let b ← saveState
   Tactic.evalTactic tacs
-
-  logInfo m!"{tacs.raw.getArgs}"
-
-  pure ()
-  -- -- Not correct
-  -- let gs ← Tactic.getUnsolvedGoals
-  -- if ¬ gs.isEmpty then
-  --   logWarning "To work as intended, `Template` should contain the entire proof"
-
-
-  -- -- Show an info whether the branch proofs all remaining goals.
-  -- let gs ← Tactic.getUnsolvedGoals
-  -- if gs.isEmpty then
-  --   logInfo "This branch finishes the proof."
-  -- else
-  --   logInfo "This branch leaves open goals."
-
-  -- let msgs ← Core.getMessageLog
-  -- b.restore
-  -- Core.setMessageLog msgs
-
-
-/-- A hole inside a template proof that will be replaced by `sorry`. -/
-elab "Hole" t:tacticSeq : tactic => do
-  Tactic.evalTactic t
-
+  let newTacs : TSyntax `Lean.Parser.Tactic.tacticSeq := ⟨replaceHoles tacs.raw⟩
+  let template ← PrettyPrinter.ppCategory `Lean.Parser.Tactic.tacticSeq newTacs
+  logInfo s!"Template:\n{template}"
+  modifyLevel (←getCurLevelId) fun level => do
+    return {level with template := s!"{template}"}
 
 -- TODO: Notes for testing if a declaration has the simp attribute
 

server/GameServer/EnvExtensions.lean

@@ -201,6 +201,9 @@ structure LevelId where
   level : Nat
 deriving Inhabited
 
+instance : ToString LevelId := ⟨fun id =>
+  s!"{id.game}:{id.world}:{id.level}"⟩
+
 structure InventoryInfo where
   /-- inventory items used by the main sample solution of this level -/
   used : Array Name
@@ -245,6 +248,8 @@ structure GameLevel where
   tactics: InventoryInfo := default
   definitions: InventoryInfo := default
   lemmas: InventoryInfo := default
+  /-- A proof template that is printed in an empty editor. -/
+  template: Option String := none
   deriving Inhabited, Repr
 
 

server/GameServer/Game.lean

@@ -51,6 +51,7 @@ structure LevelInfo where
   descrFormat : String := ""
   lemmaTab : Option String
   statementName : Option String
+  template : Option String
 deriving ToJson, FromJson
 
 structure InventoryOverview where
@@ -65,6 +66,11 @@ structure LoadLevelParams where
   level : Nat
   deriving ToJson, FromJson
 
+-- structure LoadTemplateParams where
+--   world : Name
+--   level : Nat
+--   deriving ToJson, FromJson
+
 structure DidOpenLevelParams where
   uri : String
   gameDir : String
@@ -156,9 +162,25 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
                 | none => name.toString
                 -- Note: we could call `.find!` because we check in `Statement` that the
                 -- lemma doc must exist.
+            template := lvl.template
             }
       c.hOut.writeLspResponse ⟨id, ToJson.toJson levelInfo⟩
       return true
+    -- | Message.request id "loadTemplate" params =>
+    --   let p ← parseParams LoadTemplateParams (toJson params)
+    --   let s ← get
+    --   let c ← read
+
+    --   let some game ← getGame? s.game
+    --     | throwServerError "Game not found"
+    --   let some world := game.worlds.nodes.find? p.world
+    --     | throwServerError "World not found"
+
+    --   let mut templates : Array <| Option String := #[]
+    --   for (_, level) in world.levels.toArray do
+    --     templates := templates.push level.template
+    --   c.hOut.writeLspResponse ⟨id, ToJson.toJson templates⟩
+    --   return true
     | Message.request id "loadDoc" params =>
       let p ← parseParams LoadDocParams (toJson params)
       let s ← get

server/GameServer/TacticDocstringTest.lean

@@ -0,0 +1,63 @@
+/- Modified from Mathlib.Tactic.HelpCmd -/
+import Lean
+
+open Lean Meta Elab Tactic Command Expr
+
+/-- 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 (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
+
+def getTacticDocstring (name: Name) : CommandElabM String := do
+  let name := name.toString (escape := false)
+  let mut decls : Lean.RBMap String (Array SyntaxNodeKind) compare := {}
+
+  let env ← getEnv
+
+  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 ""
+
+#eval (getTacticDocstring `simp)
+
+
+    -- TODO: Things we want:
+    -- 1) Getting docstring this way is a problem if we want to "reprove" a mathlib lemma because
+    -- either it would not be imported from mathlib or have a different name in `Statement`
+    -- 3) is the lemma a simp lemma? (are there other attributes on it? --> hard/impossible)
+    -- 4) which mathlib file is it imported from?
+    -- 5) namespace
+    -- 6) tactics: are there alternative variations like `ext`, `ext?`, `ext1?`, …
+    -- 7) definition: is it reducible?
+    -- .) …

server/test/test_statement.lean

@@ -45,9 +45,15 @@ Statement add_zero (n : Nat) : n + 0 = n := by
 Statement (n : Nat) : 0 + n = n := by
   Template
     induction n
+    Hint ""
     Hole
       simp
-    simp
+    Branch
+      skip
+      Hint ""
+    Hint ""
+  simp
+
 
 NewLemma add_zero