From 1d7facd8dd340ed060f59a3b1fc5c1651bb22c03 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Thu, 9 Mar 2023 15:34:15 +0100 Subject: [PATCH] use fvars instead of mvars for hints --- server/leanserver/GameServer/AbstractCtx.lean | 24 ++++ server/leanserver/GameServer/Commands.lean | 77 +++++----- .../leanserver/GameServer/EnvExtensions.lean | 9 +- server/leanserver/GameServer/RpcHandlers.lean | 133 ++++++++++-------- 4 files changed, 141 insertions(+), 102 deletions(-) create mode 100644 server/leanserver/GameServer/AbstractCtx.lean diff --git a/server/leanserver/GameServer/AbstractCtx.lean b/server/leanserver/GameServer/AbstractCtx.lean new file mode 100644 index 0000000..eaf683e --- /dev/null +++ b/server/leanserver/GameServer/AbstractCtx.lean @@ -0,0 +1,24 @@ +import Lean + +section AbstractCtx +open Lean +open Meta + +structure AbstractCtxResult := + (abstractMVarsResult : AbstractMVarsResult) + +/-- Abstract LCtx and MCtx to transport an expression into different contexts -/ +def abstractCtx (goal : MVarId) : MetaM AbstractCtxResult := do + let goalDecl ← goal.getDecl + let fvars := goalDecl.lctx.decls.toArray.filterMap id |> Array.map (mkFVar ·.fvarId) + let goal ← mkLambdaFVars (usedLetOnly := false) fvars goalDecl.type + let goal ← abstractMVars goal + return { + abstractMVarsResult := goal + } + +def openAbstractCtxResult (res : AbstractCtxResult) (k : Array Expr → Expr → MetaM α) : MetaM α := do + let (mvars, binderInfo, expr) ← openAbstractMVarsResult res.abstractMVarsResult + lambdaLetTelescope (← instantiateMVars expr) k + +end AbstractCtx diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean index a9d72ac..3b630db 100644 --- a/server/leanserver/GameServer/Commands.lean +++ b/server/leanserver/GameServer/Commands.lean @@ -65,17 +65,18 @@ def reprint (stx : Syntax) : Format := elab "Hint" msg:interpolatedStr(term) : tactic => do let goal ← Tactic.getMainGoal - let varsName := `vars - let text ← withLocalDeclD varsName (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) fun vars => do - let mut text ← `(m! $msg) - let goalDecl ← goal.getDecl - let decls := goalDecl.lctx.decls.toArray.filterMap id - for i in [:decls.size] do - text ← `(let $(mkIdent decls[i]!.userName) := $(mkIdent varsName)[$(quote i)]!; $text) - return ← mkLambdaFVars #[vars] $ ← elabTermAndSynthesize text none - let mvar ← mkFreshExprMVar none - guard $ ← isDefEq mvar text - logInfo (.compose (.ofGoal mvar.mvarId!) (.ofGoal goal)) + goal.withContext do + let varsName := `vars + let text ← withLocalDeclD varsName (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) fun vars => do + let mut text ← `(m! $msg) + let goalDecl ← goal.getDecl + let decls := goalDecl.lctx.decls.toArray.filterMap id + for i in [:decls.size] do + text ← `(let $(mkIdent decls[i]!.userName) := $(mkIdent varsName)[$(quote i)]!; $text) + return ← mkLambdaFVars #[vars] $ ← elabTermAndSynthesize text none + let mvar ← mkFreshExprMVar none + guard $ ← isDefEq mvar text + logInfo (.compose (.ofGoal mvar.mvarId!) (.ofGoal goal)) /-- Define the statement of the current level. @@ -105,12 +106,8 @@ elab "Statement" statementName:ident ? descr:str sig:declSig val:declVal : comma if let (MessageData.withNamingContext nctx (MessageData.withContext ctx (.compose (.ofGoal text) (.ofGoal goal)))) := msg.data then let hint ← liftTermElabM $ withMCtx ctx.mctx $ withLCtx ctx.lctx #[] $ withEnv ctx.env do - let goalDecl ← goal.getDecl - let fvars := goalDecl.lctx.decls.toArray.filterMap id |> Array.map (mkFVar ·.fvarId) - let goal ← mkForallFVars fvars goalDecl.type return { - goal := goal - intros := fvars.size + goal := ← abstractCtx goal text := ← instantiateMVars (mkMVar text) } hints := hints.push hint @@ -178,38 +175,40 @@ def mkGoalSyntax (s : Term) : List (Ident × Term) → MacroM Term | (n, t)::tail => do return (← `(∀ $n : $t, $(← mkGoalSyntax s tail))) | [] => return s -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 - synthesizeSyntheticMVarsNoPostponing false - return (← instantiateMVars 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 - - if g.hasMVar then throwError m!"Goal contains metavariables: {g}" - - modifyCurLevel fun level => pure {level with hints := level.hints.push { - goal := g, - intros := decls.size, - hidden := hidden, - text := msg }} +-- 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 +-- synthesizeSyntheticMVarsNoPostponing false +-- return (← instantiateMVars 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 + +-- if g.hasMVar then throwError m!"Goal contains metavariables: {g}" + + -- modifyCurLevel fun level => pure {level with hints := level.hints.push { + -- goal := g, + -- intros := decls.size, + -- 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 + -- elabHint false binders goal msg + pure () /-- 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'" binders:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command => do - elabHint true binders goal msg + -- elabHint true binders goal msg + pure () /-- Declare a hint in reaction to a given tactic state in the current level. -/ macro "Hint" decls:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command => do diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean index 71500af..d2c95cc 100644 --- a/server/leanserver/GameServer/EnvExtensions.lean +++ b/server/leanserver/GameServer/EnvExtensions.lean @@ -1,5 +1,6 @@ import Lean import GameServer.Graph +import GameServer.AbstractCtx /-! # Environment extensions @@ -16,15 +17,15 @@ open Lean A hint to help the user with a specific goal state -/ structure GoalHintEntry where - goal : Expr - /-- Number of variables to intro in the beginning of goal -/ - intros : Nat + goal : AbstractCtxResult /-- 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 +instance : Repr GoalHintEntry := { + reprPrec := fun a n => reprPrec a.text n +} /-! ## Tactic/Definition/Lemma documentation -/ diff --git a/server/leanserver/GameServer/RpcHandlers.lean b/server/leanserver/GameServer/RpcHandlers.lean index f82f24c..852cfc5 100644 --- a/server/leanserver/GameServer/RpcHandlers.lean +++ b/server/leanserver/GameServer/RpcHandlers.lean @@ -25,67 +25,82 @@ def getLevelByFileName? [Monad m] [MonadEnv m] (fileName : String) : m (Option G | return none return ← getLevel? levelId +structure FVarBijection := + (forward : HashMap FVarId FVarId) + (backward : HashMap FVarId FVarId) -/-- Checks if `pattern` and `e` are equal up to mvars in `pattern` that may be assigned to fvars in `e`. -/ -partial def matchExprAux (pattern : Expr) (e : Expr) : MetaM Bool := do +instance : EmptyCollection FVarBijection := ⟨{},{}⟩ + +def FVarBijection.insert (bij : FVarBijection) (a b : FVarId) : FVarBijection := + ⟨bij.forward.insert a b, bij.backward.insert b a⟩ + +def FVarBijection.insert? (bij : FVarBijection) (a b : FVarId) : Option FVarBijection := + let a' := bij.forward.find? a + let b' := bij.forward.find? b + if (a' == none || a' == some b) && (b' == none || b' == some a) + then some $ bij.insert a b + else none + +/-- Checks if `pattern` and `e` are equal up to FVar identities. -/ +partial def matchExpr (pattern : Expr) (e : Expr) (bij : FVarBijection := {}) : Option FVarBijection := match pattern, e with - | .bvar i1, .bvar i2 => return i1 == i2 - | .fvar i1, .fvar i2 => return i1 == i2 - | .mvar _, .mvar _ => return true - | .sort u1, .sort u2 => Meta.isLevelDefEq u1 u2 + | .bvar i1, .bvar i2 => if i1 == i2 then bij else none + | .fvar i1, .fvar i2 => bij.insert? i1 i2 + | .mvar _, .mvar _ => bij + | .sort u1, .sort u2 => bij -- TODO? | .const n1 ls1, .const n2 ls2 => - return n1 == n2 && (← (ls1.zip ls2).allM fun (l1, l2) => Meta.isLevelDefEq l1 l2) + if n1 == n2 then bij else none -- && (← (ls1.zip ls2).allM fun (l1, l2) => Meta.isLevelDefEq l1 l2) | .app f1 a1, .app f2 a2 => - return (← matchExprAux f1 f2) && (← matchExprAux a1 a2) + some bij + |> (Option.bind · (fun bij => matchExpr f1 f2 bij)) + |> (Option.bind · (fun bij => matchExpr a1 a2 bij)) | .lam _ t1 b1 _, .lam _ t2 b2 _ => - return (← matchExprAux t1 t2) && (← matchExprAux b1 b2) + some bij + |> (Option.bind · (fun bij => matchExpr t1 t2 bij)) + |> (Option.bind · (fun bij => matchExpr b1 b2 bij)) | .forallE _ t1 b1 _, .forallE _ t2 b2 _ => - return (← matchExprAux t1 t2) && (← matchExprAux b1 b2) + some bij + |> (Option.bind · (fun bij => matchExpr t1 t2 bij)) + |> (Option.bind · (fun bij => matchExpr b1 b2 bij)) | .letE _ t1 v1 b1 _, .letE _ t2 v2 b2 _ => - return (← matchExprAux t1 t2) && (← matchExprAux v1 v2) && (← matchExprAux b1 b2) + some bij + |> (Option.bind · (fun bij => matchExpr t1 t2 bij)) + |> (Option.bind · (fun bij => matchExpr v1 v2 bij)) + |> (Option.bind · (fun bij => matchExpr b1 b2 bij)) | .lit l1, .lit l2 => - return l1 == l2 + if l1 == l2 then bij else none | .proj i1 n1 e1, .proj i2 n2 e2 => - return i1 == i2 && n1 == n2 && (← matchExprAux e1 e2) + if i1 == i2 && n1 == n2 then matchExpr e1 e2 bij else none -- ignore mdata: | .mdata _ pattern', _ => - return ← matchExprAux pattern' e + matchExpr pattern' e bij | _, .mdata _ e' => - return ← matchExprAux pattern e' - -- assign fvars to mvars: - | .mvar i1, .fvar _ => - match ← getExprMVarAssignment? i1 with - | some pattern' => matchExprAux pattern' e - | none => - i1.assign e - return true - | _, _ => return false - -def matchExpr (pattern : Expr) (e : Expr) : MetaM Bool := do - checkpointDefEq (mayPostpone := true) do - matchExprAux pattern e - -/-- Check if each meta variable in `declMvars` has a matching fvar in `declFvars` -/ -def matchDecls (declMvars : Array Expr) (declFvars : Array Expr) : MetaM Bool := do + matchExpr pattern e' bij + | _, _ => none + +/-- Check if each fvar in `patterns` has a matching fvar in `fvars` -/ +def matchDecls (patterns : Array Expr) (fvars : Array Expr) : Bool := -- We iterate through the array backwards hoping that this will find us faster results -- TODO: implement backtracking - let mut usedFvars := (List.replicate declFvars.size false).toArray - -- `usedFvars` keeps track of the fvars that were already used to match an mvar. - for i in [:declMvars.size] do - let declMvar := declMvars[declMvars.size - i - 1]! - let mut found := false - for j in [:declFvars.size] do - let declFvar := declFvars[declFvars.size - j - 1]! - let usedFvar := usedFvars[declFvars.size - j - 1]! - if ¬ usedFvar then - if ← matchExpr declMvar declFvar then - usedFvars := usedFvars.set! (declFvars.size - j - 1) true - found := true - break - else - continue - if ¬ found then return false - return true + -- TODO: reimplement this + patterns.size = fvars.size + -- let mut usedFvars := (List.replicate declFvars.size false).toArray + -- -- `usedFvars` keeps track of the fvars that were already used to match an mvar. + -- for i in [:declMvars.size] do + -- let declMvar := declMvars[declMvars.size - i - 1]! + -- let mut found := false + -- for j in [:declFvars.size] do + -- let declFvar := declFvars[declFvars.size - j - 1]! + -- let usedFvar := usedFvars[declFvars.size - j - 1]! + -- if ¬ usedFvar then + -- if let some _ := matchExpr declMvar declFvar then + -- usedFvars := usedFvars.set! (declFvars.size - j - 1) true + -- found := true + -- break + -- else + -- continue + -- if ¬ found then return false + -- return true unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) := evalExpr (Array Expr → MessageData) @@ -102,19 +117,19 @@ def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array let some level ← getLevelByFileName? doc.meta.mkInputContext.fileName | throwError "Level not found: {doc.meta.mkInputContext.fileName}" let hints ← level.hints.filterMapM fun hint => do - let (declMvars, binderInfo, hintGoal) ← forallMetaBoundedTelescope hint.goal hint.intros - -- TODO: Protect mvars in the type of `goal` to be instantiated? - if ← matchExpr hintGoal (← inferType $ mkMVar goal) - then - let lctx ← getLCtx -- Local context of the `goal` - if ← matchDecls declMvars lctx.getFVars + openAbstractCtxResult hint.goal fun hintFVars hintGoal => do + if let some _ := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal) then - 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 + let lctx := (← goal.getDecl).lctx + if matchDecls hintFVars lctx.getFVars + then + let text := (← evalHintMessage hint.text) hintFVars + 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