From 649a5d2dfb01934b0222cd1dd4731bd35c357291 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 12 Dec 2022 12:19:21 +0100 Subject: [PATCH] Add hints. --- client/src/components/TacticState.tsx | 1 + server/leanserver/GameServer/Commands.lean | 20 +++++-- .../leanserver/GameServer/EnvExtensions.lean | 8 +++ server/leanserver/GameServer/RpcHandlers.lean | 55 +++++++++++++------ 4 files changed, 64 insertions(+), 20 deletions(-) diff --git a/client/src/components/TacticState.tsx b/client/src/components/TacticState.tsx index 6eb9dee..fd96a47 100644 --- a/client/src/components/TacticState.tsx +++ b/client/src/components/TacticState.tsx @@ -35,6 +35,7 @@ function Goal({ goal }) { Prove: {goal.goal} {goal.messages.map((message) => {message})} + {goal.hints.map((message) => {message})} ) } diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean index af2e930..efb4fa1 100644 --- a/server/leanserver/GameServer/Commands.lean +++ b/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 -/ diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean index 67c452c..a437ee6 100644 --- a/server/leanserver/GameServer/EnvExtensions.lean +++ b/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 -/ diff --git a/server/leanserver/GameServer/RpcHandlers.lean b/server/leanserver/GameServer/RpcHandlers.lean index a231b0a..97b7f74 100644 --- a/server/leanserver/GameServer/RpcHandlers.lean +++ b/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