Add hints.

client/src/components/TacticState.tsx

@@ -35,6 +35,7 @@ function Goal({ goal }) {
       <Typography>Prove:</Typography>
       <Typography color="primary" sx={{ ml: 2 }}>{goal.goal}</Typography>
       {goal.messages.map((message) => <Alert severity="info" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{message}</ReactMarkdown></MathJax></Alert>)}
+      {goal.hints.map((message) => <Alert severity="warning" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{message}</ReactMarkdown></MathJax></Alert>)}
     </Box>)
 }
 

server/leanserver/GameServer/Commands.lean

@@ -70,8 +70,6 @@ elab "Conclusion" t:str : command => do
 elab "PrintCurLevel" : command => do
   logInfo (repr (← getCurLevel))
 
-#check Syntax.SepArray
-
 -- /-- Print levels for debugging purposes. -/
 elab "PrintLevels" : command => do
   logInfo $ repr $ (← getCurWorld).levels.toArray
@@ -121,14 +119,28 @@ local elab "Message'" decls:mydecl* ":" goal:term "=>" msg:str : command => do
     intros := decls.size,
     message := msg.getString }}
 
+/--
+Declare a hint. This version doesn't prevent the unused linter variable from running.
+The difference between hints/messages is that hints should be hidden by default, while
+messages are visible.
+-/
+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)
+  modifyCurLevel fun level => pure {level with messages := level.messages.push {
+    goal := g,
+    intros := decls.size,
+    spoiler := true,
+    message := msg.getString }}
+
+
 /-- Declare a message in reaction to a given tactic state in the current level. -/
 macro "Message" decls:mydecl* ":" goal:term "=>" msg:str : command => do
   `(set_option linter.unusedVariables false in Message' $decls* : $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
-  `(set_option linter.unusedVariables false in Message' $decls* : $goal => $msg)
-  -- TODO: implement me?
+  `(set_option linter.unusedVariables false in Hint' $decls* : $goal => $msg)
 
 /-! ## Tactics -/
 

server/leanserver/GameServer/EnvExtensions.lean

@@ -10,10 +10,18 @@ open Lean
 
 /-! ## Messages -/
 
+/--
+A message to be displayed to the user as instruction/hint.
+
+Fields
+  (TODO)
+  spoiler: If true, then message should be hidden by default
+-/
 structure GoalMessageEntry where
   goal : Expr
   intros : Nat
   message : String
+  spoiler : Bool := false
   deriving Repr
 
 /-! ## Tactic documentation -/

server/leanserver/GameServer/RpcHandlers.lean

@@ -20,10 +20,12 @@ structure GameGoal where
   assumptions : List GameLocalDecl
   goal : String
   messages : Array String
+  hints : Array String
 deriving FromJson, ToJson
 
 
-def Lean.MVarId.toGameGoal (goal : MVarId) (messages : Array String) : MetaM GameGoal := do
+def Lean.MVarId.toGameGoal (goal : MVarId) (messages : Array String)
+    (hints : Array String) : MetaM GameGoal := do
 match (← getMCtx).findDecl? goal with
 | none          => throwError "unknown goal"
 | some mvarDecl => do
@@ -46,20 +48,16 @@ match (← getMCtx).findDecl? goal with
       return { userName := decl.userName, type := toString (← Meta.ppExpr decl.type) }
     let assumptions ← assumptions.mapM fun decl => do
       return { userName := decl.userName, type := toString (← Meta.ppExpr decl.type) }
-    return {objects := objects, assumptions := assumptions, goal := toString (← Meta.ppExpr mvarDecl.type), messages }
-
+    return {objects := objects, assumptions := assumptions, goal := toString (← Meta.ppExpr mvarDecl.type), messages, hints }
 
 namespace GameServer
 
-
 /-- `Game.getGoals` client<-server reply. -/
 structure PlainGoal where
   /-- The pretty-printed goals, empty if all accomplished. -/
   goals : Array GameGoal
   deriving FromJson, ToJson
 
-#check String.split
-
 -- TODO: Find a better way to pass on the file name?
 def levelIdFromFileName [Monad m] [MonadError m] [MonadEnv m] (fileName : String) : m LevelId := do
   let fileParts := fileName.splitOn "/"
@@ -103,19 +101,43 @@ def findMessages (goal : MVarId) (doc : FileWorker.EditableDocument) (hLog : IO.
   goal.withContext do
     let level ← getLevelByFileName doc.meta.mkInputContext.fileName
     let messages ← level.messages.filterMapM fun message => do
-      let (declMvars, binderInfo, messageGoal) ← forallMetaBoundedTelescope message.goal message.intros
-      -- TODO: Protext mvars in the type of `goal` to be instantiated?
-      if ← isDefEq messageGoal (← inferType $ mkMVar goal) -- TODO: also check assumptions
-      then
-        let lctx ← getLCtx -- Local context of the `goal`
-        hLog.putStr s!"{← declMvars.mapM inferType} =?= {← lctx.getFVars.mapM inferType}"
-        if ← matchDecls declMvars lctx.getFVars
+      if message.spoiler then
+        return none
+      else
+        let (declMvars, binderInfo, messageGoal) ← forallMetaBoundedTelescope message.goal message.intros
+        -- TODO: Protext mvars in the type of `goal` to be instantiated?
+        if ← isDefEq messageGoal (← inferType $ mkMVar goal) -- TODO: also check assumptions
         then
-          return some message.message
+          let lctx ← getLCtx -- Local context of the `goal`
+          hLog.putStr s!"{← declMvars.mapM inferType} =?= {← lctx.getFVars.mapM inferType}"
+          if ← matchDecls declMvars lctx.getFVars
+          then
+            return some message.message
+          else return none
         else return none
-      else return none
     return messages
 
+open Meta in
+/-- Find all hints whose trigger matches the current goal -/
+def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) (hLog : IO.FS.Stream) : MetaM (Array String) := do
+  goal.withContext do
+    let level ← getLevelByFileName doc.meta.mkInputContext.fileName
+    let hints ← level.messages.filterMapM fun message => do
+      if message.spoiler then
+        let (declMvars, binderInfo, messageGoal) ← forallMetaBoundedTelescope message.goal message.intros
+        -- TODO: Protext mvars in the type of `goal` to be instantiated?
+        if ← isDefEq messageGoal (← inferType $ mkMVar goal) -- TODO: also check assumptions
+        then
+          let lctx ← getLCtx -- Local context of the `goal`
+          hLog.putStr s!"{← declMvars.mapM inferType} =?= {← lctx.getFVars.mapM inferType}"
+          if ← matchDecls declMvars lctx.getFVars
+          then
+            return some message.message
+          else return none
+        else return none
+      else return none
+    return hints
+
 /-- Get goals and messages at a given position -/
 def getGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option PlainGoal)) := do
   let doc ← readDoc
@@ -132,7 +154,8 @@ def getGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option PlainGoal
           let goals := List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
           let goals ← ci.runMetaM {} $ goals.mapM fun goal => do
             let messages ← findMessages goal doc hLog
-            return ← goal.toGameGoal messages
+            let hints ← findHints goal doc hLog
+            return ← goal.toGameGoal messages hints
           return goals
         return some { goals := goals.foldl (· ++ ·) ∅ }
       else