phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Revert "fix variables in hints"

Browse Source 
This reverts commit 8851cd8b1f.
This commit is contained in:
joneugster
2023-11-30 12:16:06 +01:00
parent 8851cd8b1f
commit 44f7b6703e
1 changed files with 18 additions and 17 deletions
Download Patch File Download Diff File Expand all files Collapse all files
server/GameServer/RpcHandlers.lean
+18 -17
View File
@@ -114,24 +114,25 @@ def evalHintMessage : Expr → MetaM (Array Expr → MessageData) := fun _ => pu
open Meta in
/-- Find all hints whose trigger matches the current goal -/
def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
let some level ← getLevelByFileName? initParams doc.meta.mkInputContext.fileName
| throwError "Level not found: {doc.meta.mkInputContext.fileName}"
let hints ← level.hints.filterMapM fun hint => do
openAbstractCtxResult hint.goal fun hintFVars hintGoal => goal.withContext do
if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
then
let lctx := (← goal.getDecl).lctx
if let some bij ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
goal.withContext do
let some level ← getLevelByFileName? initParams doc.meta.mkInputContext.fileName
| throwError "Level not found: {doc.meta.mkInputContext.fileName}"
let hints ← level.hints.filterMapM fun hint => do
openAbstractCtxResult hint.goal fun hintFVars hintGoal => do
if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
then
let userFVars := hintFVars.map fun v => bij.forward.findD v.fvarId! v.fvarId!
let text := (← evalHintMessage hint.text) (userFVars.map Expr.fvar)
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
let lctx := (← goal.getDecl).lctx
if let some bij ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
then
let userFVars := hintFVars.map fun v => bij.forward.findD v.fvarId! v.fvarId!
let text := (← evalHintMessage hint.text) (userFVars.map Expr.fvar)
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
open RequestM in
def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option InteractiveGoals)) := do