hints with variable names

server/leanserver/GameServer/Commands.lean

@@ -132,54 +132,50 @@ end metadata
 
 open Lean Meta Elab Command Term
 
-declare_syntax_cat mydecl
-syntax "(" ident ":" term ")" : mydecl
-
-def getIdent : TSyntax `mydecl → Ident
-| `(mydecl| ($n:ident : $_t:term)) => n
-| _ => default
-
-def getType : TSyntax `mydecl → Term
-| `(mydecl| ($_n:ident : $t:term)) => t
-| _ => default
-
 /-- From a term `s` and a list of pairs `(i, t) ; Ident × Term`, create the syntax
 where `s` is preceded with universal quantifiers `∀ i : t`. -/
 def mkGoalSyntax (s : Term) : List (Ident × Term) → MacroM Term
 | (n, t)::tail => do return (← `(∀ $n : $t, $(← mkGoalSyntax s tail)))
 | [] => return s
 
-/-- Declare a hint. This version doesn't prevent the unused linter variable from running. -/
-local elab "Hint'" decls:mydecl* ":" goal:term "=>" msg:str : command => do
-  let g ← liftMacroM $ mkGoalSyntax goal (decls.map (λ decl => (getIdent decl, getType decl))).toList
-  let g ← liftTermElabM do (return ← elabTermAndSynthesize g none)
+def elabHint (hidden : Bool) (binders : TSyntaxArray `Lean.Parser.Term.bracketedBinder)
+  (goal : TSyntax `term) (msg : TSyntax `interpolatedStrKind) :=
+liftTermElabM do withOptions (fun options => options.setBool `linter.unusedVariables false) do
+  let (g, decls) ← elabBinders binders fun xs => do
+    let g ← mkForallFVars xs $ ← elabTermAndSynthesize goal none
+    return (g, ← xs.mapM (fun x => x.fvarId!.getDecl))
+  let varsName := `vars
+  let msg ← withLocalDeclD varsName (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) fun vars => do
+    let mut msg ← `(m! $msg)
+    for i in [:decls.size] do
+      msg ← `(let $(mkIdent decls[i]!.userName) := $(mkIdent varsName)[$(quote i)]!; $msg)
+    return ← mkLambdaFVars #[vars] $ ← elabTermAndSynthesize msg none
   modifyCurLevel fun level => pure {level with hints := level.hints.push {
     goal := g,
     intros := decls.size,
-    text := msg.getString }}
+    hidden := hidden,
+    text := msg }}
+
+/-- Declare a hint. This version doesn't prevent the unused linter variable from running. -/
+local elab "Hint'" binders:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command =>
+  elabHint false binders goal msg
 
 /--
 Declare a hint. This version doesn't prevent the unused linter variable from running.
 A hidden hint is only displayed if explicitly requested by the user.
 -/
-local elab "HiddenHint'" decls:mydecl* ":" goal:term "=>" msg:str : command => do
-  let g ← liftMacroM $ mkGoalSyntax goal (decls.map (λ decl => (getIdent decl, getType decl))).toList
-  let g ← liftTermElabM do (return ← elabTermAndSynthesize g none)
-  modifyCurLevel fun level => pure {level with hints := level.hints.push {
-    goal := g,
-    intros := decls.size,
-    hidden := true,
-    text := msg.getString }}
-
+local elab "HiddenHint'" binders:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command => do
+  elabHint true binders goal msg
 
 /-- Declare a hint in reaction to a given tactic state in the current level. -/
-macro "Hint" decls:mydecl* ":" goal:term "=>" msg:str : command => do
+macro "Hint" decls:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command => do
   `(set_option linter.unusedVariables false in Hint' $decls* : $goal => $msg)
 
 /-- Declare a hidden hint in reaction to a given tactic state in the current level. -/
-macro "HiddenHint" decls:mydecl* ":" goal:term "=>" msg:str : command => do
+macro "HiddenHint" decls:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command => do
   `(set_option linter.unusedVariables false in HiddenHint' $decls* : $goal => $msg)
 
+
 /-! ## Inventory -/
 
 /-- Throw an error if inventory doc does not exist -/

server/leanserver/GameServer/EnvExtensions.lean

@@ -14,15 +14,14 @@ open Lean
 
 /--
 A hint to help the user with a specific goal state
-
-Fields
-  (TODO)
-  hidden: If true, then hint should be hidden by default
 -/
 structure GoalHintEntry where
   goal : Expr
+  /-- Number of variables to intro in the beginning of goal -/
   intros : Nat
-  text : String
+  /-- Text of the hint as an expression of type `Array Expr → MessageData` -/
+  text : Expr
+  /--  If true, then hint should be hidden by default -/
   hidden : Bool := false
   deriving Repr
 

server/leanserver/GameServer/RpcHandlers.lean

@@ -47,6 +47,14 @@ def matchDecls (declMvars : Array Expr) (declFvars : Array Expr) : MetaM Bool :=
     if ¬ found then return false
   return true
 
+unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) :=
+  evalExpr (Array Expr → MessageData)
+    (.forallE default (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr))
+      (mkConst ``MessageData) .default)
+
+@[implemented_by evalHintMessageUnsafe]
+def evalHintMessage : Expr → MetaM (Array Expr → MessageData) := fun _ => pure (fun _ => "")
+
 open Meta in
 /-- Find all hints whose trigger matches the current goal -/
 def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array GameHint) := do
@@ -61,7 +69,10 @@ def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array
         let lctx ← getLCtx -- Local context of the `goal`
         if ← matchDecls declMvars lctx.getFVars
         then
-          return some { text := hint.text, hidden := hint.hidden }
+          let text := (← evalHintMessage hint.text) declMvars
+          let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
+          let text ← (MessageData.withContext ctx text).toString
+          return some { text := text, hidden := hint.hidden }
         else return none
       else return none
     return hints