unify hints and messages

client/src/components/TacticState.tsx

@@ -23,7 +23,9 @@ function Goal({ goal }) {
 
   const hasObject = typeof goal.objects === "object" && goal.objects.length > 0
   const hasAssumption = typeof goal.assumptions === "object" && goal.assumptions.length > 0
-  const hasHints = typeof goal.hints === "object" && goal.hints.length > 0
+  const openMessages = typeof goal.messages === "object" ? goal.messages.filter((msg) => ! msg.spoiler) : []
+  const hints = typeof goal.messages === "object" ? goal.messages.filter((msg) => msg.spoiler) : []
+  const hasHints = hints.length > 0
   return (
     <Box sx={{ pl: 2 }}>
       {hasObject && <Box><Typography>Objects</Typography>
@@ -41,13 +43,13 @@ function Goal({ goal }) {
         </List></Box>}
       <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>)}
+      {openMessages.map((message) => <Alert severity="info" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{message.message}</ReactMarkdown></MathJax></Alert>)}
       {hasHints &&
         <FormControlLabel
           control={<Switch checked={showHints} onChange={handleHintsChange} />}
           label="Help"
         />}
-        {goal.hints.map((hint) => <Collapse in={showHints}><Alert severity="warning" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{hint}</ReactMarkdown></MathJax></Alert></Collapse>)}
+        {hints.map((hint) => <Collapse in={showHints}><Alert severity="warning" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{hint.message}</ReactMarkdown></MathJax></Alert></Collapse>)}
     </Box>)
 }
 

server/leanserver/GameServer/RpcHandlers.lean

@@ -15,17 +15,20 @@ structure GameLocalDecl where
   type : String
 deriving FromJson, ToJson
 
+structure GameMessage where
+  message : String
+  spoiler : Bool
+deriving FromJson, ToJson
+
 structure GameGoal where
   objects : List GameLocalDecl
   assumptions : List GameLocalDecl
   goal : String
-  messages : Array String
+  messages : Array GameMessage
-  hints : Array String
 deriving FromJson, ToJson
 
 
-def Lean.MVarId.toGameGoal (goal : MVarId)
+def Lean.MVarId.toGameGoal (goal : MVarId) (messages : Array GameMessage) : MetaM GameGoal := do
-    (messages : Array String) (hints : Array String) : MetaM GameGoal := do
 match (← getMCtx).findDecl? goal with
 | none          => throwError "unknown goal"
 | some mvarDecl => do
@@ -48,7 +51,7 @@ 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, hints }
+    return {objects := objects, assumptions := assumptions, goal := toString (← Meta.ppExpr mvarDecl.type), messages }
 
 namespace GameServer
 
@@ -97,46 +100,23 @@ def matchDecls (declMvars : Array Expr) (declFvars : Array Expr) : MetaM Bool :=
 
 open Meta in
 /-- Find all messages whose trigger matches the current goal -/
-def findMessages (goal : MVarId) (doc : FileWorker.EditableDocument) (hLog : IO.FS.Stream) : MetaM (Array String) := do
+def findMessages (goal : MVarId) (doc : FileWorker.EditableDocument) (hLog : IO.FS.Stream) : MetaM (Array GameMessage) := do
   goal.withContext do
     let level ← getLevelByFileName doc.meta.mkInputContext.fileName
     let messages ← level.messages.filterMapM fun message => do
-      if message.spoiler then
+      let (declMvars, binderInfo, messageGoal) ← forallMetaBoundedTelescope message.goal message.intros
-        return none
+      -- TODO: Protext mvars in the type of `goal` to be instantiated?
-      else
+      if ← isDefEq messageGoal (← inferType $ mkMVar goal) -- TODO: also check assumptions
-        let (declMvars, binderInfo, messageGoal) ← forallMetaBoundedTelescope message.goal message.intros
+      then
-        -- TODO: Protext mvars in the type of `goal` to be instantiated?
+        let lctx ← getLCtx -- Local context of the `goal`
-        if ← isDefEq messageGoal (← inferType $ mkMVar goal) -- TODO: also check assumptions
+        hLog.putStr s!"{← declMvars.mapM inferType} =?= {← lctx.getFVars.mapM inferType}"
+        if ← matchDecls declMvars lctx.getFVars
         then
-          let lctx ← getLCtx -- Local context of the `goal`
+          return some { message := message.message, spoiler := message.spoiler }
-          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
-    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
+    return messages
+
 
 /-- Get goals and messages at a given position -/
 def getGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option PlainGoal)) := do
@@ -154,8 +134,7 @@ 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
-            let hints ← findHints goal doc hLog
+            return ← goal.toGameGoal messages
-            return ← goal.toGameGoal messages hints
           return goals
         return some { goals := goals.foldl (· ++ ·) ∅ }
       else