From 25a7025c254102da74ad89343801719769bc62b4 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 23 Jun 2024 15:01:51 -0700 Subject: [PATCH 01/19] feat: Evaluation tactic --- Pantograph/Goal.lean | 12 ++++++++++++ Pantograph/Tactic.lean | 2 +- Pantograph/Tactic/Prograde.lean | 22 ++++++++++++++++++++++ 3 files changed, 35 insertions(+), 1 deletion(-) create mode 100644 Pantograph/Tactic/Prograde.lean diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 46888e7..ebe29fb 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -302,6 +302,7 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St Meta.withNewLocalInstances #[fvar] 0 do let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous) + -- FIXME: May be redundant? let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream goal.assign expr pure mvarUpstream @@ -537,5 +538,16 @@ protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: Strin | .ok syn => pure syn | .error error => return .parseError error state.execute goalId (tacticM := Tactic.noConfuse recursor) +protected def GoalState.tryEval (state: GoalState) (goalId: Nat) (binderName: Name) (expr: String) : + Elab.TermElabM TacticResult := do + state.restoreElabM + let expr ← match Parser.runParserCategory + (env := state.env) + (catName := `term) + (input := expr) + (fileName := filename) with + | .ok syn => pure syn + | .error error => return .parseError error + state.execute goalId (tacticM := Tactic.tacticEval binderName expr) end Pantograph diff --git a/Pantograph/Tactic.lean b/Pantograph/Tactic.lean index 225ad31..094d1f8 100644 --- a/Pantograph/Tactic.lean +++ b/Pantograph/Tactic.lean @@ -1,4 +1,4 @@ - import Pantograph.Tactic.Congruence import Pantograph.Tactic.MotivatedApply import Pantograph.Tactic.NoConfuse +import Pantograph.Tactic.Prograde diff --git a/Pantograph/Tactic/Prograde.lean b/Pantograph/Tactic/Prograde.lean new file mode 100644 index 0000000..f37a1e5 --- /dev/null +++ b/Pantograph/Tactic/Prograde.lean @@ -0,0 +1,22 @@ +/- Prograde (forward) reasoning tactics -/ + +import Lean +open Lean + +namespace Pantograph.Tactic + +def tacticEval (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do + let goal ← Elab.Tactic.getMainGoal + let nextGoals ← goal.withContext do + let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none) + let type ← Meta.inferType expr + + let mvarUpstream ← Meta.withLetDecl binderName type expr λ _ => do + let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) + (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous) + goal.assign mvarUpstream + pure mvarUpstream + pure [mvarUpstream.mvarId!] + Elab.Tactic.setGoals nextGoals + +end Pantograph.Tactic From e282d9f7815e8ea616da07185ae55062527831b4 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 25 Jun 2024 11:03:08 -0400 Subject: [PATCH 02/19] test: Evaluation tactic --- Pantograph/Goal.lean | 2 +- Pantograph/Serial.lean | 2 +- Pantograph/Tactic/Prograde.lean | 2 +- Test/Common.lean | 11 +++++++++ Test/Main.lean | 1 + Test/Tactic.lean | 1 + Test/Tactic/Prograde.lean | 42 +++++++++++++++++++++++++++++++++ 7 files changed, 58 insertions(+), 3 deletions(-) create mode 100644 Test/Tactic/Prograde.lean diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index ebe29fb..db73a48 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -548,6 +548,6 @@ protected def GoalState.tryEval (state: GoalState) (goalId: Nat) (binderName: Na (fileName := filename) with | .ok syn => pure syn | .error error => return .parseError error - state.execute goalId (tacticM := Tactic.tacticEval binderName expr) + state.execute goalId (tacticM := Tactic.evaluate binderName expr) end Pantograph diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 159b78e..5f08186 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -202,7 +202,7 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol. } /-- Adapted from ppGoal -/ -def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl) +def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none) : MetaM Protocol.Goal := do -- Options for printing; See Meta.ppGoal for details let showLetValues := true diff --git a/Pantograph/Tactic/Prograde.lean b/Pantograph/Tactic/Prograde.lean index f37a1e5..81dd28c 100644 --- a/Pantograph/Tactic/Prograde.lean +++ b/Pantograph/Tactic/Prograde.lean @@ -5,7 +5,7 @@ open Lean namespace Pantograph.Tactic -def tacticEval (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do +def evaluate (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do let goal ← Elab.Tactic.getMainGoal let nextGoals ← goal.withContext do let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none) diff --git a/Test/Common.lean b/Test/Common.lean index c656309..e4e1d4c 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -8,6 +8,17 @@ open Lean namespace Pantograph +deriving instance Repr for Expr +-- Use strict equality check for expressions +--instance : BEq Expr := ⟨Expr.equal⟩ +instance (priority := 80) (x y : Expr) : LSpec.Testable (x.equal y) := + if h : Expr.equal x y then + .isTrue h + else + .isFalse h $ s!"Expected to be equalaaa: '{x.dbgToString}' and '{y.dbgToString}'" + +def uniq (n: Nat): Name := .num (.str .anonymous "_uniq") n + -- Auxiliary functions namespace Protocol def Goal.devolatilizeVars (goal: Goal): Goal := diff --git a/Test/Main.lean b/Test/Main.lean index 31042c5..89c757a 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -52,6 +52,7 @@ def main (args: List String) := do ("Tactic/Congruence", Tactic.Congruence.suite env_default), ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default), ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default), + ("Tactic/Prograde", Tactic.Prograde.suite env_default), ] let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) [] LSpec.lspecIO (← runTestGroup name_filter tests) diff --git a/Test/Tactic.lean b/Test/Tactic.lean index 5863ec0..3cb0e40 100644 --- a/Test/Tactic.lean +++ b/Test/Tactic.lean @@ -1,3 +1,4 @@ import Test.Tactic.Congruence import Test.Tactic.MotivatedApply import Test.Tactic.NoConfuse +import Test.Tactic.Prograde diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean new file mode 100644 index 0000000..863aca5 --- /dev/null +++ b/Test/Tactic/Prograde.lean @@ -0,0 +1,42 @@ +import LSpec +import Lean +import Test.Common + +open Lean +open Pantograph + +namespace Pantograph.Test.Tactic.Prograde + +def test_eval (env: Environment): IO LSpec.TestSeq := + let expr := "forall (p q : Prop) (h: p), And (Or p q) (Or p q)" + runMetaMSeq env do + let expr ← parseSentence expr + Meta.forallTelescope expr $ λ _ body => do + let e ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := "Or.inl h") + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + let mut tests := LSpec.TestSeq.done + -- Apply the tactic + let goal ← Meta.mkFreshExprSyntheticOpaqueMVar body + let target: Expr := mkAnd + (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩)) + (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩)) + let test := LSpec.test "goals before" ((← goal.mvarId!.getType) == target) + tests := tests ++ test + let tactic := Tactic.evaluate `h2 e + let test ← runTermElabMInMeta do + let newGoals ← runTacticOnMVar tactic goal.mvarId! + pure $ LSpec.test "goals after" ((← newGoals.head!.getType) == target) + tests := tests ++ test + return tests + +def suite (env: Environment): List (String × IO LSpec.TestSeq) := + [ + ("eval", test_eval env), + ] + +end Pantograph.Test.Tactic.Prograde From 58f9d72288d9f2870d5fdecb8afc84d974427cd9 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 25 Jun 2024 16:18:31 -0400 Subject: [PATCH 03/19] test: Evaluate tactic context --- Test/Common.lean | 27 +++++++++++++++++++++------ Test/Tactic/Prograde.lean | 27 ++++++++++++++++++++++++--- 2 files changed, 45 insertions(+), 9 deletions(-) diff --git a/Test/Common.lean b/Test/Common.lean index e4e1d4c..df0edcd 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -1,6 +1,7 @@ import Pantograph.Goal import Pantograph.Library import Pantograph.Protocol +import Pantograph.Condensed import Lean import LSpec @@ -10,12 +11,7 @@ namespace Pantograph deriving instance Repr for Expr -- Use strict equality check for expressions ---instance : BEq Expr := ⟨Expr.equal⟩ -instance (priority := 80) (x y : Expr) : LSpec.Testable (x.equal y) := - if h : Expr.equal x y then - .isTrue h - else - .isFalse h $ s!"Expected to be equalaaa: '{x.dbgToString}' and '{y.dbgToString}'" +instance : BEq Expr := ⟨Expr.equal⟩ def uniq (n: Nat): Name := .num (.str .anonymous "_uniq") n @@ -25,6 +21,7 @@ def Goal.devolatilizeVars (goal: Goal): Goal := { goal with vars := goal.vars.map removeInternalAux, + } where removeInternalAux (v: Variable): Variable := { @@ -47,6 +44,24 @@ deriving instance DecidableEq, Repr for InteractionError deriving instance DecidableEq, Repr for Option end Protocol +namespace Condensed + +deriving instance BEq, Repr for LocalDecl +deriving instance BEq, Repr for Goal + +protected def LocalDecl.devolatilize (decl: LocalDecl): LocalDecl := + { + decl with fvarId := { name := .anonymous } + } +protected def Goal.devolatilize (goal: Goal): Goal := + { + goal with + mvarId := { name := .anonymous }, + context := goal.context.map LocalDecl.devolatilize + } + +end Condensed + def TacticResult.toString : TacticResult → String | .success state => s!".success ({state.goals.length} goals)" | .failure messages => diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean index 863aca5..d959f4f 100644 --- a/Test/Tactic/Prograde.lean +++ b/Test/Tactic/Prograde.lean @@ -25,12 +25,33 @@ def test_eval (env: Environment): IO LSpec.TestSeq := let target: Expr := mkAnd (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩)) (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩)) - let test := LSpec.test "goals before" ((← goal.mvarId!.getType) == target) + let h := .fvar ⟨uniq 8⟩ + let test := LSpec.test "goals before" ((← toCondensedGoal goal.mvarId!).devolatilize == { + context := #[ + { userName := `p, type := .sort 0 }, + { userName := `q, type := .sort 0 }, + { userName := `h, type := h} + ], + target, + }) tests := tests ++ test let tactic := Tactic.evaluate `h2 e + let m := .mvar ⟨uniq 13⟩ let test ← runTermElabMInMeta do - let newGoals ← runTacticOnMVar tactic goal.mvarId! - pure $ LSpec.test "goals after" ((← newGoals.head!.getType) == target) + let [goal] ← runTacticOnMVar tactic goal.mvarId! | panic! "Incorrect goal number" + pure $ LSpec.test "goals after" ((← toCondensedGoal goal).devolatilize == { + context := #[ + { userName := `p, type := .sort 0 }, + { userName := `q, type := .sort 0 }, + { userName := `h, type := h}, + { + userName := `h2, + type := mkOr h m, + value? := .some $ mkApp3 (mkConst `Or.inl) h m (.fvar ⟨uniq 10⟩) + } + ], + target, + }) tests := tests ++ test return tests From 7acf1ffdf1de629141129a077c5f10405407a81f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 25 Jun 2024 16:58:35 -0400 Subject: [PATCH 04/19] refactor: Move `have` to prograde tactic --- Pantograph.lean | 2 +- Pantograph/Compile.lean | 2 +- Pantograph/Compile/Parse.lean | 14 +++++++ Pantograph/Goal.lean | 72 +++------------------------------ Pantograph/Library.lean | 9 ++++- Pantograph/Tactic/Prograde.lean | 25 ++++++++++++ 6 files changed, 53 insertions(+), 71 deletions(-) create mode 100644 Pantograph/Compile/Parse.lean diff --git a/Pantograph.lean b/Pantograph.lean index 097651f..35ab117 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -125,7 +125,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do pure ( Except.ok (← goalAssign goalState args.goalId expr)) | .none, .none, .some type, .none, .none => do let binderName := args.binderName?.getD "" - pure ( Except.ok (← goalHave goalState args.goalId binderName type)) + pure ( Except.ok (← goalState.tryHave args.goalId binderName type)) | .none, .none, .none, .some pred, .none => do pure ( Except.ok (← goalCalc goalState args.goalId pred)) | .none, .none, .none, .none, .some true => do diff --git a/Pantograph/Compile.lean b/Pantograph/Compile.lean index 15081d9..83b463f 100644 --- a/Pantograph/Compile.lean +++ b/Pantograph/Compile.lean @@ -2,7 +2,7 @@ import Pantograph.Protocol import Pantograph.Compile.Frontend import Pantograph.Compile.Elab - +import Pantograph.Compile.Parse open Lean diff --git a/Pantograph/Compile/Parse.lean b/Pantograph/Compile/Parse.lean new file mode 100644 index 0000000..72eb620 --- /dev/null +++ b/Pantograph/Compile/Parse.lean @@ -0,0 +1,14 @@ +import Lean + +open Lean + +namespace Pantograph.Compile + +def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do + return Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := s) + (fileName := "") + +end Pantograph.Compile diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index b2f6f53..60a28d6 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -5,6 +5,7 @@ All the functions starting with `try` resume their inner monadic state. -/ import Pantograph.Protocol import Pantograph.Tactic +import Pantograph.Compile.Parse import Lean def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog := @@ -277,57 +278,6 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String -- Specialized Tactics -protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): - Elab.TermElabM TacticResult := do - state.restoreElabM - let goal ← match state.savedState.tactic.goals.get? goalId with - | .some goal => pure goal - | .none => return .indexError goalId - goal.checkNotAssigned `GoalState.tryHave - let type ← match Parser.runParserCategory - (env := state.env) - (catName := `term) - (input := type) - (fileName := filename) with - | .ok syn => pure syn - | .error error => return .parseError error - let binderName := binderName.toName - try - -- Implemented similarly to the intro tactic - let nextGoals: List MVarId ← goal.withContext do - let type ← Elab.Term.elabType (stx := type) - let lctx ← MonadLCtx.getLCtx - - -- The branch goal inherits the same context, but with a different type - let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type - - -- Create the context for the `upstream` goal - let fvarId ← mkFreshFVarId - let lctxUpstream := lctx.mkLocalDecl fvarId binderName type - let fvar := mkFVar fvarId - let mvarUpstream ← - withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do - Meta.withNewLocalInstances #[fvar] 0 do - let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) - (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous) - -- FIXME: May be redundant? - let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream - goal.assign expr - pure mvarUpstream - - pure [mvarBranch.mvarId!, mvarUpstream.mvarId!] - return .success { - root := state.root, - savedState := { - term := ← MonadBacktrack.saveState, - tactic := { goals := nextGoals } - }, - newMVars := nextGoals.toSSet, - parentMVar? := .some goal, - calcPrevRhs? := .none - } - catch exception => - return .failure #[← exception.toMessageData.toString] protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Elab.TermElabM TacticResult := do state.restoreElabM @@ -527,33 +477,21 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Elab.TermElabM TacticResult := do state.restoreElabM - let recursor ← match Parser.runParserCategory - (env := state.env) - (catName := `term) - (input := recursor) - (fileName := filename) with + let recursor ← match (← Compile.parseTermM recursor) with | .ok syn => pure syn | .error error => return .parseError error state.execute goalId (tacticM := Tactic.motivatedApply recursor) protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Elab.TermElabM TacticResult := do state.restoreElabM - let recursor ← match Parser.runParserCategory - (env := state.env) - (catName := `term) - (input := eq) - (fileName := filename) with + let eq ← match (← Compile.parseTermM eq) with | .ok syn => pure syn | .error error => return .parseError error - state.execute goalId (tacticM := Tactic.noConfuse recursor) + state.execute goalId (tacticM := Tactic.noConfuse eq) protected def GoalState.tryEval (state: GoalState) (goalId: Nat) (binderName: Name) (expr: String) : Elab.TermElabM TacticResult := do state.restoreElabM - let expr ← match Parser.runParserCategory - (env := state.env) - (catName := `term) - (input := expr) - (fileName := filename) with + let expr ← match (← Compile.parseTermM expr) with | .ok syn => pure syn | .error error => return .parseError error state.execute goalId (tacticM := Tactic.evaluate binderName expr) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 8036103..aa8bcbc 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -180,8 +180,13 @@ def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticRe def goalAssign (state: GoalState) (goalId: Nat) (expr: String): CoreM TacticResult := runTermElabM <| state.tryAssign goalId expr @[export pantograph_goal_have_m] -def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := - runTermElabM <| state.tryHave goalId binderName type +protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := do + let type ← match (← Compile.parseTermM type) with + | .ok syn => pure syn + | .error error => return .parseError error + runTermElabM do + state.restoreElabM + state.execute goalId (Tactic.have_t binderName.toName type) @[export pantograph_goal_let_m] def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := runTermElabM <| state.tryLet goalId binderName type diff --git a/Pantograph/Tactic/Prograde.lean b/Pantograph/Tactic/Prograde.lean index 81dd28c..4c525c2 100644 --- a/Pantograph/Tactic/Prograde.lean +++ b/Pantograph/Tactic/Prograde.lean @@ -19,4 +19,29 @@ def evaluate (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do pure [mvarUpstream.mvarId!] Elab.Tactic.setGoals nextGoals +def have_t (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do + let goal ← Elab.Tactic.getMainGoal + let nextGoals: List MVarId ← goal.withContext do + let type ← Elab.Term.elabType (stx := type) + let lctx ← MonadLCtx.getLCtx + + -- The branch goal inherits the same context, but with a different type + let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type + + -- Create the context for the `upstream` goal + let fvarId ← mkFreshFVarId + let lctxUpstream := lctx.mkLocalDecl fvarId binderName type + let fvar := mkFVar fvarId + let mvarUpstream ← + withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do + Meta.withNewLocalInstances #[fvar] 0 do + let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) + (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous) + --let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream + goal.assign mvarUpstream + pure mvarUpstream + + pure [mvarBranch.mvarId!, mvarUpstream.mvarId!] + Elab.Tactic.setGoals nextGoals + end Pantograph.Tactic From 2d2ff24017151bca6f1e466e7a4cf565fc055291 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 25 Jun 2024 17:01:49 -0400 Subject: [PATCH 05/19] feat: FFI interface for `evaluate` tactic --- Pantograph/Library.lean | 10 +++++++++- Pantograph/Tactic/Prograde.lean | 2 +- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index aa8bcbc..71dcdfe 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -186,7 +186,15 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St | .error error => return .parseError error runTermElabM do state.restoreElabM - state.execute goalId (Tactic.have_t binderName.toName type) + state.execute goalId (Tactic.«have» binderName.toName type) +@[export pantograph_goal_evaluate_m] +protected def GoalState.tryEvaluate (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := do + let type ← match (← Compile.parseTermM type) with + | .ok syn => pure syn + | .error error => return .parseError error + runTermElabM do + state.restoreElabM + state.execute goalId (Tactic.evaluate binderName.toName type) @[export pantograph_goal_let_m] def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := runTermElabM <| state.tryLet goalId binderName type diff --git a/Pantograph/Tactic/Prograde.lean b/Pantograph/Tactic/Prograde.lean index 4c525c2..59acaf1 100644 --- a/Pantograph/Tactic/Prograde.lean +++ b/Pantograph/Tactic/Prograde.lean @@ -19,7 +19,7 @@ def evaluate (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do pure [mvarUpstream.mvarId!] Elab.Tactic.setGoals nextGoals -def have_t (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do +def «have» (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do let goal ← Elab.Tactic.getMainGoal let nextGoals: List MVarId ← goal.withContext do let type ← Elab.Term.elabType (stx := type) From fc0d872343d1290c8e6e3e6b63116157abb1d359 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 27 Jun 2024 14:34:21 -0400 Subject: [PATCH 06/19] refactor: Simplify proof test infrastructure --- Test/Common.lean | 36 +++++- Test/Proofs.lean | 64 ----------- Test/Tactic/Congruence.lean | 161 ++++++++++++--------------- Test/Tactic/MotivatedApply.lean | 191 +++++++++++++++----------------- Test/Tactic/NoConfuse.lean | 123 +++++++++----------- Test/Tactic/Prograde.lean | 152 +++++++++++++++++-------- 6 files changed, 349 insertions(+), 378 deletions(-) diff --git a/Test/Common.lean b/Test/Common.lean index df0edcd..41025f5 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -89,10 +89,12 @@ def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSe runCoreMSeq env metaM.run' def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α := termElabM.run' (ctx := Pantograph.defaultTermElabMContext) +def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq): IO LSpec.TestSeq := + runMetaMSeq env $ termElabM.run' (ctx := Pantograph.defaultTermElabMContext) def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e -def parseSentence (s: String): MetaM Expr := do +def parseSentence (s: String): Elab.TermElabM Expr := do let recursor ← match Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `term) @@ -100,7 +102,7 @@ def parseSentence (s: String): MetaM Expr := do (fileName := filename) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" - runTermElabMInMeta $ Elab.Term.elabTerm (stx := recursor) .none + Elab.Term.elabTerm (stx := recursor) .none def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] } @@ -110,6 +112,36 @@ def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do let t ← exprToStr (← mvarId.getType) return (name, t) + +-- Monadic testing + +abbrev TestT := StateT LSpec.TestSeq + +def addTest [Monad m] (test: LSpec.TestSeq): TestT m Unit := do + set $ (← get) ++ test + +def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq := + Prod.snd <$> t.run LSpec.TestSeq.done + +def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit): + IO LSpec.TestSeq := + runTermElabMSeq env $ runTest t + +def cdeclOf (userName: Name) (type: Expr): Condensed.LocalDecl := + { userName, type } + +def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): + Protocol.Goal := + { + userName?, + target := { pp? := .some target}, + vars := (nameType.map fun x => ({ + userName := x.fst, + type? := .some { pp? := .some x.snd }, + isInaccessible? := .some false + })).toArray + } + end Test end Pantograph diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 9c45138..0603571 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -357,69 +357,6 @@ def test_or_comm: TestM Unit := do ] } -def test_have: TestM Unit := do - let state? ← startProof (.expr "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))") - let state0 ← match state? with - | .some state => pure state - | .none => do - addTest $ assertUnreachable "Goal could not parse" - return () - let tactic := "intro p q h" - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = - #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"]) - - let expr := "Or.inl (Or.inl h)" - let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = - #[]) - - let haveBind := "y" - let haveType := "p ∨ q" - let state2 ← match ← state1.tryHave (goalId := 0) (binderName := haveBind) (type := haveType) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check s!"have {haveBind}: {haveType}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = - #[ - buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "p ∨ q", - buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p"), ("y", "p ∨ q")] "(p ∨ q) ∨ p ∨ q" - ]) - - let expr := "Or.inl h" - let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) = - #[]) - - let state2b ← match state3.continue state2 with - | .ok state => pure state - | .error e => do - addTest $ assertUnreachable e - return () - let expr := "Or.inl y" - let state4 ← match ← state2b.tryAssign (goalId := 0) (expr := expr) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) = - #[]) - - addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome - example : ∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2 := by intro a b c1 c2 h conv => @@ -856,7 +793,6 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("Nat.add_comm delta", test_delta_variable), ("arithmetic", test_arith), ("Or.comm", test_or_comm), - ("have", test_have), ("conv", test_conv), ("calc", test_calc), ("let via assign", test_let false), diff --git a/Test/Tactic/Congruence.lean b/Test/Tactic/Congruence.lean index 6e8f547..38c94f3 100644 --- a/Test/Tactic/Congruence.lean +++ b/Test/Tactic/Congruence.lean @@ -7,103 +7,82 @@ open Pantograph namespace Pantograph.Test.Tactic.Congruence -def test_congr_arg_list (env: Environment): IO LSpec.TestSeq := +def test_congr_arg_list : TestT Elab.TermElabM Unit := do let expr := "λ {α} (l1 l2 : List α) (h: l1 = l2) => l1.reverse = l2.reverse" - runMetaMSeq env do - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let mut tests := LSpec.TestSeq.done - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let (newGoals, test) ← runTermElabMInMeta do - let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId! - let test := LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = - [ - (`α, "Sort ?u.30"), - (`a₁, "?α"), - (`a₂, "?α"), - (`f, "?α → List α"), - (`h, "?a₁ = ?a₂"), - (`conduit, "(?f ?a₁ = ?f ?a₂) = (l1.reverse = l2.reverse)"), - ]) - return (newGoals, test) - tests := tests ++ test - let f := newGoals.get! 3 - let h := newGoals.get! 4 - let c := newGoals.get! 5 - let results ← f.apply (← parseSentence "List.reverse") - tests := tests ++ (LSpec.check "apply" (results.length = 0)) - tests := tests ++ (LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂")) - tests := tests ++ (LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)")) - return tests -def test_congr_arg (env: Environment): IO LSpec.TestSeq := + let expr ← parseSentence expr + Meta.lambdaTelescope expr $ λ _ body => do + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId! + addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = + [ + (`α, "Sort ?u.30"), + (`a₁, "?α"), + (`a₂, "?α"), + (`f, "?α → List α"), + (`h, "?a₁ = ?a₂"), + (`conduit, "(?f ?a₁ = ?f ?a₂) = (l1.reverse = l2.reverse)"), + ]) + let f := newGoals.get! 3 + let h := newGoals.get! 4 + let c := newGoals.get! 5 + let results ← f.apply (← parseSentence "List.reverse") + addTest $ LSpec.check "apply" (results.length = 0) + addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂") + addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)") +def test_congr_arg : TestT Elab.TermElabM Unit := do let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m" - runMetaMSeq env do - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let mut tests := LSpec.TestSeq.done - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let test ← runTermElabMInMeta do - let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId! - pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = - [ - (`α, "Sort ?u.70"), - (`a₁, "?α"), - (`a₂, "?α"), - (`f, "?α → Nat"), - (`h, "?a₁ = ?a₂"), - (`conduit, "(?f ?a₁ = ?f ?a₂) = (n * n = m * m)"), - ]) - tests := tests ++ test - return tests -def test_congr_fun (env: Environment): IO LSpec.TestSeq := + let expr ← parseSentence expr + Meta.lambdaTelescope expr $ λ _ body => do + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId! + addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = + [ + (`α, "Sort ?u.70"), + (`a₁, "?α"), + (`a₂, "?α"), + (`f, "?α → Nat"), + (`h, "?a₁ = ?a₂"), + (`conduit, "(?f ?a₁ = ?f ?a₂) = (n * n = m * m)"), + ]) +def test_congr_fun : TestT Elab.TermElabM Unit := do let expr := "λ (n m: Nat) => (n + m) + (n + m) = (n + m) * 2" - runMetaMSeq env do - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let mut tests := LSpec.TestSeq.done - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let test ← runTermElabMInMeta do - let newGoals ← runTacticOnMVar Tactic.congruenceFun target.mvarId! - pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = - [ - (`α, "Sort ?u.159"), - (`f₁, "?α → Nat"), - (`f₂, "?α → Nat"), - (`h, "?f₁ = ?f₂"), - (`a, "?α"), - (`conduit, "(?f₁ ?a = ?f₂ ?a) = (n + m + (n + m) = (n + m) * 2)"), - ]) - tests := tests ++ test - return tests -def test_congr (env: Environment): IO LSpec.TestSeq := + let expr ← parseSentence expr + Meta.lambdaTelescope expr $ λ _ body => do + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let newGoals ← runTacticOnMVar Tactic.congruenceFun target.mvarId! + addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = + [ + (`α, "Sort ?u.159"), + (`f₁, "?α → Nat"), + (`f₂, "?α → Nat"), + (`h, "?f₁ = ?f₂"), + (`a, "?α"), + (`conduit, "(?f₁ ?a = ?f₂ ?a) = (n + m + (n + m) = (n + m) * 2)"), + ]) +def test_congr : TestT Elab.TermElabM Unit := do let expr := "λ (a b: Nat) => a = b" - runMetaMSeq env do - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let mut tests := LSpec.TestSeq.done - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let test ← runTermElabMInMeta do - let newGoals ← runTacticOnMVar Tactic.congruence target.mvarId! - pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = - [ - (`α, "Sort ?u.10"), - (`f₁, "?α → Nat"), - (`f₂, "?α → Nat"), - (`a₁, "?α"), - (`a₂, "?α"), - (`h₁, "?f₁ = ?f₂"), - (`h₂, "?a₁ = ?a₂"), - (`conduit, "(?f₁ ?a₁ = ?f₂ ?a₂) = (a = b)"), - ]) - tests := tests ++ test - return tests + let expr ← parseSentence expr + Meta.lambdaTelescope expr $ λ _ body => do + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let newGoals ← runTacticOnMVar Tactic.congruence target.mvarId! + addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = + [ + (`α, "Sort ?u.10"), + (`f₁, "?α → Nat"), + (`f₂, "?α → Nat"), + (`a₁, "?α"), + (`a₂, "?α"), + (`h₁, "?f₁ = ?f₂"), + (`h₂, "?a₁ = ?a₂"), + (`conduit, "(?f₁ ?a₁ = ?f₂ ?a₂) = (a = b)"), + ]) def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ - ("congrArg List.reverse", test_congr_arg_list env), - ("congrArg", test_congr_arg env), - ("congrFun", test_congr_fun env), - ("congr", test_congr env), - ] + ("congrArg List.reverse", test_congr_arg_list), + ("congrArg", test_congr_arg), + ("congrFun", test_congr_fun), + ("congr", test_congr), + ] |>.map (λ (name, t) => (name, runTestTermElabM env t)) end Pantograph.Test.Tactic.Congruence diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean index 154e34c..091e309 100644 --- a/Test/Tactic/MotivatedApply.lean +++ b/Test/Tactic/MotivatedApply.lean @@ -7,82 +7,23 @@ open Pantograph namespace Pantograph.Test.Tactic.MotivatedApply -def test_type_extract (env: Environment): IO LSpec.TestSeq := - runMetaMSeq env do - let mut tests := LSpec.TestSeq.done - let recursor ← parseSentence "@Nat.brecOn" - let recursorType ← Meta.inferType recursor - tests := tests ++ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" = - (← exprToStr recursorType)) - let info ← match Tactic.getRecursorInformation recursorType with - | .some info => pure info - | .none => throwError "Failed to extract recursor info" - tests := tests ++ LSpec.check "iMotive" (info.iMotive = 2) - let motiveType := info.getMotiveType - tests := tests ++ LSpec.check "motiveType" ("Nat → Sort ?u.1" = - (← exprToStr motiveType)) - return tests +def test_type_extract : TestT Elab.TermElabM Unit := do + let recursor ← parseSentence "@Nat.brecOn" + let recursorType ← Meta.inferType recursor + addTest $ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" = + (← exprToStr recursorType)) + let info ← match Tactic.getRecursorInformation recursorType with + | .some info => pure info + | .none => throwError "Failed to extract recursor info" + addTest $ LSpec.check "iMotive" (info.iMotive = 2) + let motiveType := info.getMotiveType + addTest $ LSpec.check "motiveType" ("Nat → Sort ?u.1" = + (← exprToStr motiveType)) -def test_nat_brec_on (env: Environment): IO LSpec.TestSeq := +def test_nat_brec_on : TestT Elab.TermElabM Unit := do let expr := "λ (n t: Nat) => n + 0 = n" - runMetaMSeq env do - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let recursor ← match Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `term) - (input := "@Nat.brecOn") - (fileName := filename) with - | .ok syn => pure syn - | .error error => throwError "Failed to parse: {error}" - let mut tests := LSpec.TestSeq.done - -- Apply the tactic - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let tactic := Tactic.motivatedApply recursor - let test ← runTermElabMInMeta do - let newGoals ← runTacticOnMVar tactic target.mvarId! - pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = - [ - "Nat → Prop", - "Nat", - "∀ (t : Nat), Nat.below t → ?motive t", - "?motive ?m.67 = (n + 0 = n)", - ]) - tests := tests ++ test - return tests - -def test_list_brec_on (env: Environment): IO LSpec.TestSeq := - let expr := "λ {α : Type} (l: List α) => l ++ [] = [] ++ l" - runMetaMSeq env do - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let recursor ← match Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `term) - (input := "@List.brecOn") - (fileName := filename) with - | .ok syn => pure syn - | .error error => throwError "Failed to parse: {error}" - let mut tests := LSpec.TestSeq.done - -- Apply the tactic - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let tactic := Tactic.motivatedApply recursor - let test ← runTermElabMInMeta do - let newGoals ← runTacticOnMVar tactic target.mvarId! - pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = - [ - "Type ?u.90", - "List ?m.92 → Prop", - "List ?m.92", - "∀ (t : List ?m.92), List.below t → ?motive t", - "?motive ?m.94 = (l ++ [] = [] ++ l)", - ]) - tests := tests ++ test - return tests - -def test_partial_motive_instantiation (env: Environment): IO LSpec.TestSeq := do - let expr := "λ (n t: Nat) => n + 0 = n" - runMetaMSeq env $ runTermElabMInMeta do + let expr ← parseSentence expr + Meta.lambdaTelescope expr $ λ _ body => do let recursor ← match Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `term) @@ -90,41 +31,83 @@ def test_partial_motive_instantiation (env: Environment): IO LSpec.TestSeq := do (fileName := filename) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let mut tests := LSpec.TestSeq.done - -- Apply the tactic - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let tactic := Tactic.motivatedApply recursor - let newGoals ← runTacticOnMVar tactic target.mvarId! - let majorId := 67 - tests := tests ++ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = - [ - "Nat → Prop", - "Nat", - "∀ (t : Nat), Nat.below t → ?motive t", - s!"?motive ?m.{majorId} = (n + 0 = n)", - ])) - let [motive, major, step, conduit] := newGoals | panic! "Incorrect goal number" - tests := tests ++ (LSpec.check "goal name" (major.name.toString = s!"_uniq.{majorId}")) + -- Apply the tactic + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let tactic := Tactic.motivatedApply recursor + let newGoals ← runTacticOnMVar tactic target.mvarId! + let test := LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = + [ + "Nat → Prop", + "Nat", + "∀ (t : Nat), Nat.below t → ?motive t", + "?motive ?m.67 = (n + 0 = n)", + ]) + addTest test - -- Assign motive to `λ x => x + _` - let motive_assign ← parseSentence "λ (x: Nat) => @Nat.add x + 0 = _" - motive.assign motive_assign +def test_list_brec_on : TestT Elab.TermElabM Unit := do + let expr := "λ {α : Type} (l: List α) => l ++ [] = [] ++ l" + let expr ← parseSentence expr + Meta.lambdaTelescope expr $ λ _ body => do + let recursor ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := "@List.brecOn") + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + -- Apply the tactic + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let tactic := Tactic.motivatedApply recursor + let newGoals ← runTacticOnMVar tactic target.mvarId! + addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = + [ + "Type ?u.90", + "List ?m.92 → Prop", + "List ?m.92", + "∀ (t : List ?m.92), List.below t → ?motive t", + "?motive ?m.94 = (l ++ [] = [] ++ l)", + ]) - let test ← conduit.withContext do - let t := toString (← Meta.ppExpr $ ← conduit.getType) - return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)") - tests := tests ++ test +def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do + let expr := "λ (n t: Nat) => n + 0 = n" + let recursor ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := "@Nat.brecOn") + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + let expr ← parseSentence expr + Meta.lambdaTelescope expr $ λ _ body => do + -- Apply the tactic + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let tactic := Tactic.motivatedApply recursor + let newGoals ← runTacticOnMVar tactic target.mvarId! + let majorId := 67 + addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = + [ + "Nat → Prop", + "Nat", + "∀ (t : Nat), Nat.below t → ?motive t", + s!"?motive ?m.{majorId} = (n + 0 = n)", + ])) + let [motive, major, step, conduit] := newGoals | panic! "Incorrect goal number" + addTest $ (LSpec.check "goal name" (major.name.toString = s!"_uniq.{majorId}")) - return tests + -- Assign motive to `λ x => x + _` + let motive_assign ← parseSentence "λ (x: Nat) => @Nat.add x + 0 = _" + motive.assign motive_assign + + addTest $ ← conduit.withContext do + let t := toString (← Meta.ppExpr $ ← conduit.getType) + return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)") def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ - ("type_extract", test_type_extract env), - ("Nat.brecOn", test_nat_brec_on env), - ("List.brecOn", test_list_brec_on env), - ("Nat.brecOn partial motive instantiation", test_partial_motive_instantiation env), - ] + ("type_extract", test_type_extract), + ("Nat.brecOn", test_nat_brec_on), + ("List.brecOn", test_list_brec_on), + ("Nat.brecOn partial motive instantiation", test_partial_motive_instantiation), + ] |>.map (λ (name, t) => (name, runTestTermElabM env t)) end Pantograph.Test.Tactic.MotivatedApply diff --git a/Test/Tactic/NoConfuse.lean b/Test/Tactic/NoConfuse.lean index c672a0b..cc15198 100644 --- a/Test/Tactic/NoConfuse.lean +++ b/Test/Tactic/NoConfuse.lean @@ -7,81 +7,66 @@ open Pantograph namespace Pantograph.Test.Tactic.NoConfuse -def test_nat (env: Environment): IO LSpec.TestSeq := +def test_nat : TestT Elab.TermElabM Unit := do let expr := "λ (n: Nat) (h: 0 = n + 1) => False" - runMetaMSeq env do - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let recursor ← match Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `term) - (input := "h") - (fileName := filename) with - | .ok syn => pure syn - | .error error => throwError "Failed to parse: {error}" - let mut tests := LSpec.TestSeq.done - -- Apply the tactic - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let tactic := Tactic.noConfuse recursor - let test ← runTermElabMInMeta do - let newGoals ← runTacticOnMVar tactic target.mvarId! - pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = - []) - tests := tests ++ test - return tests + let expr ← parseSentence expr + Meta.lambdaTelescope expr $ λ _ body => do + let recursor ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := "h") + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + -- Apply the tactic + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let tactic := Tactic.noConfuse recursor + let newGoals ← runTacticOnMVar tactic target.mvarId! + addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = []) -def test_nat_fail (env: Environment): IO LSpec.TestSeq := +def test_nat_fail : TestT Elab.TermElabM Unit := do let expr := "λ (n: Nat) (h: n = n) => False" - runMetaMSeq env do - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let recursor ← match Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `term) - (input := "h") - (fileName := filename) with - | .ok syn => pure syn - | .error error => throwError "Failed to parse: {error}" - let mut tests := LSpec.TestSeq.done - -- Apply the tactic - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - try - let tactic := Tactic.noConfuse recursor - let _ ← runTermElabMInMeta $ runTacticOnMVar tactic target.mvarId! - tests := tests ++ assertUnreachable "Tactic should fail" - catch _ => - tests := tests ++ LSpec.check "Tactic should fail" true - return tests - return tests - -def test_list (env: Environment): IO LSpec.TestSeq := - let expr := "λ (l: List Nat) (h: [] = 1 :: l) => False" - runMetaMSeq env do - let expr ← parseSentence expr - Meta.lambdaTelescope expr $ λ _ body => do - let recursor ← match Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `term) - (input := "h") - (fileName := filename) with - | .ok syn => pure syn - | .error error => throwError "Failed to parse: {error}" - let mut tests := LSpec.TestSeq.done - -- Apply the tactic - let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let expr ← parseSentence expr + Meta.lambdaTelescope expr $ λ _ body => do + let recursor ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := "h") + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + -- Apply the tactic + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + try let tactic := Tactic.noConfuse recursor - let test ← runTermElabMInMeta do - let newGoals ← runTacticOnMVar tactic target.mvarId! - pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = - []) - tests := tests ++ test - return tests + let _ ← runTacticOnMVar tactic target.mvarId! + addTest $ assertUnreachable "Tactic should fail" + catch _ => + addTest $ LSpec.check "Tactic should fail" true + +def test_list : TestT Elab.TermElabM Unit := do + let expr := "λ (l: List Nat) (h: [] = 1 :: l) => False" + let expr ← parseSentence expr + Meta.lambdaTelescope expr $ λ _ body => do + let recursor ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := "h") + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + -- Apply the tactic + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let tactic := Tactic.noConfuse recursor + let newGoals ← runTacticOnMVar tactic target.mvarId! + addTest $ LSpec.check "goals" + ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = []) def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ - ("Nat", test_nat env), - ("Nat fail", test_nat_fail env), - ("List", test_list env), - ] + ("Nat", test_nat), + ("Nat fail", test_nat_fail), + ("List", test_list), + ] |>.map (λ (name, t) => (name, runTestTermElabM env t)) end Pantograph.Test.Tactic.NoConfuse diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean index d959f4f..5b4da2b 100644 --- a/Test/Tactic/Prograde.lean +++ b/Test/Tactic/Prograde.lean @@ -7,57 +7,113 @@ open Pantograph namespace Pantograph.Test.Tactic.Prograde -def test_eval (env: Environment): IO LSpec.TestSeq := +def test_eval : TestT Elab.TermElabM Unit := do let expr := "forall (p q : Prop) (h: p), And (Or p q) (Or p q)" - runMetaMSeq env do - let expr ← parseSentence expr - Meta.forallTelescope expr $ λ _ body => do - let e ← match Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `term) - (input := "Or.inl h") - (fileName := filename) with - | .ok syn => pure syn - | .error error => throwError "Failed to parse: {error}" - let mut tests := LSpec.TestSeq.done - -- Apply the tactic - let goal ← Meta.mkFreshExprSyntheticOpaqueMVar body - let target: Expr := mkAnd - (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩)) - (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩)) - let h := .fvar ⟨uniq 8⟩ - let test := LSpec.test "goals before" ((← toCondensedGoal goal.mvarId!).devolatilize == { - context := #[ - { userName := `p, type := .sort 0 }, - { userName := `q, type := .sort 0 }, - { userName := `h, type := h} - ], - target, - }) - tests := tests ++ test - let tactic := Tactic.evaluate `h2 e - let m := .mvar ⟨uniq 13⟩ - let test ← runTermElabMInMeta do - let [goal] ← runTacticOnMVar tactic goal.mvarId! | panic! "Incorrect goal number" - pure $ LSpec.test "goals after" ((← toCondensedGoal goal).devolatilize == { - context := #[ - { userName := `p, type := .sort 0 }, - { userName := `q, type := .sort 0 }, - { userName := `h, type := h}, - { - userName := `h2, - type := mkOr h m, - value? := .some $ mkApp3 (mkConst `Or.inl) h m (.fvar ⟨uniq 10⟩) - } - ], - target, - }) - tests := tests ++ test - return tests + let expr ← parseSentence expr + Meta.forallTelescope expr $ λ _ body => do + let e ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := "Or.inl h") + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + -- Apply the tactic + let goal ← Meta.mkFreshExprSyntheticOpaqueMVar body + let target: Expr := mkAnd + (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩)) + (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩)) + let h := .fvar ⟨uniq 8⟩ + addTest $ LSpec.test "goals before" ((← toCondensedGoal goal.mvarId!).devolatilize == { + context := #[ + cdeclOf `p (.sort 0), + cdeclOf `q (.sort 0), + cdeclOf `h h + ], + target, + }) + let tactic := Tactic.evaluate `h2 e + let m := .mvar ⟨uniq 13⟩ + let [newGoal] ← runTacticOnMVar tactic goal.mvarId! | panic! "Incorrect goal number" + addTest $ LSpec.test "goals after" ((← toCondensedGoal newGoal).devolatilize == { + context := #[ + cdeclOf `p (.sort 0), + cdeclOf `q (.sort 0), + cdeclOf `h h, + { + userName := `h2, + type := mkOr h m, + value? := .some $ mkApp3 (mkConst `Or.inl) h m (.fvar ⟨uniq 10⟩) + } + ], + target, + }) + addTest $ LSpec.test "assign" ((← getExprMVarAssignment? goal.mvarId!) == .some (.mvar newGoal)) + +def test_have : TestT Elab.TermElabM Unit := do + let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))" + let state0 ← GoalState.create rootExpr + let tactic := "intro p q h" + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) = + #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"]) + + let expr := "Or.inl (Or.inl h)" + let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals).map (·.devolatilize) = + #[]) + + let haveBind := "y" + let haveType := "p ∨ q" + let state2 ← match ← state1.tryHave (goalId := 0) (binderName := haveBind) (type := haveType) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!"have {haveBind}: {haveType}" ((← state2.serializeGoals).map (·.devolatilize) = + #[ + buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "p ∨ q", + buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p"), ("y", "p ∨ q")] "(p ∨ q) ∨ p ∨ q" + ]) + + let expr := "Or.inl h" + let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals).map (·.devolatilize) = + #[]) + + let state2b ← match state3.continue state2 with + | .ok state => pure state + | .error e => do + addTest $ assertUnreachable e + return () + let expr := "Or.inl y" + let state4 ← match ← state2b.tryAssign (goalId := 0) (expr := expr) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals).map (·.devolatilize) = + #[]) + + addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome + def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ - ("eval", test_eval env), - ] + ("eval", test_eval), + ("have", test_have), + ] |>.map (λ (name, t) => (name, runTestTermElabM env t)) end Pantograph.Test.Tactic.Prograde From 6ddde2963d484176225fc4c35ddc77fdf7a621a1 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 27 Jun 2024 14:51:16 -0400 Subject: [PATCH 07/19] test: Eval instantiate --- Pantograph/Goal.lean | 7 ----- Pantograph/Library.lean | 6 ++-- Test/Tactic/Prograde.lean | 58 +++++++++++++++++++++++++++++++++++++-- 3 files changed, 59 insertions(+), 12 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 60a28d6..68b2aa9 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -488,12 +488,5 @@ protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: Strin | .ok syn => pure syn | .error error => return .parseError error state.execute goalId (tacticM := Tactic.noConfuse eq) -protected def GoalState.tryEval (state: GoalState) (goalId: Nat) (binderName: Name) (expr: String) : - Elab.TermElabM TacticResult := do - state.restoreElabM - let expr ← match (← Compile.parseTermM expr) with - | .ok syn => pure syn - | .error error => return .parseError error - state.execute goalId (tacticM := Tactic.evaluate binderName expr) end Pantograph diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 71dcdfe..e83dcc2 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -188,13 +188,13 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St state.restoreElabM state.execute goalId (Tactic.«have» binderName.toName type) @[export pantograph_goal_evaluate_m] -protected def GoalState.tryEvaluate (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := do - let type ← match (← Compile.parseTermM type) with +protected def GoalState.tryEvaluate (state: GoalState) (goalId: Nat) (binderName: String) (expr: String): CoreM TacticResult := do + let expr ← match (← Compile.parseTermM expr) with | .ok syn => pure syn | .error error => return .parseError error runTermElabM do state.restoreElabM - state.execute goalId (Tactic.evaluate binderName.toName type) + state.execute goalId (Tactic.evaluate binderName.toName expr) @[export pantograph_goal_let_m] def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := runTermElabM <| state.tryLet goalId binderName type diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean index 5b4da2b..15da63e 100644 --- a/Test/Tactic/Prograde.lean +++ b/Test/Tactic/Prograde.lean @@ -50,7 +50,60 @@ def test_eval : TestT Elab.TermElabM Unit := do }) addTest $ LSpec.test "assign" ((← getExprMVarAssignment? goal.mvarId!) == .some (.mvar newGoal)) -def test_have : TestT Elab.TermElabM Unit := do +def test_proof_eval : TestT Elab.TermElabM Unit := do + let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))" + let state0 ← GoalState.create rootExpr + let tactic := "intro p q h" + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) = + #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"]) + + let expr := "Or.inl (Or.inl h)" + let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals).map (·.devolatilize) = + #[]) + + let evalBind := "y" + let evalExpr := "Or.inl h" + let state2 ← match ← state1.tryEvaluate (goalId := 0) (binderName := evalBind) (expr := evalExpr) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!"eval {evalBind} := {evalExpr}" ((← state2.serializeGoals).map (·.devolatilize) = + #[{ + target := { pp? := .some "(p ∨ q) ∨ p ∨ q"}, + vars := #[ + { userName := "p", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false }, + { userName := "q", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false }, + { userName := "h", type? := .some { pp? := .some "p" }, isInaccessible? := .some false }, + { userName := "y", + type? := .some { pp? := .some "p ∨ ?m.25" }, + value? := .some { pp? := .some "Or.inl h" }, + isInaccessible? := .some false } + ] + }]) + + let expr := "Or.inl y" + let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals).map (·.devolatilize) = + #[]) + + addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome + +def test_proof_have : TestT Elab.TermElabM Unit := do let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))" let state0 ← GoalState.create rootExpr let tactic := "intro p q h" @@ -113,7 +166,8 @@ def test_have : TestT Elab.TermElabM Unit := do def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ ("eval", test_eval), - ("have", test_have), + ("Proof eval", test_proof_eval), + ("Proof have", test_proof_have), ] |>.map (λ (name, t) => (name, runTestTermElabM env t)) end Pantograph.Test.Tactic.Prograde From 7968072097912d26bee25e35637e52f663425d10 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 15 Aug 2024 22:53:42 -0700 Subject: [PATCH 08/19] refactor: Remove the newMVarSet mechanism This field has ambiguous purpose and does not account for different types of mvars --- Pantograph/Goal.lean | 56 ++++++++++++++------------------------------ 1 file changed, 18 insertions(+), 38 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 0d58fb5..cd29d2a 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -22,8 +22,6 @@ structure GoalState where -- The root hole which is the search target root: MVarId - -- New metavariables acquired in this state - newMVars: SSet MVarId -- Parent state metavariable source parentMVar?: Option MVarId @@ -48,7 +46,6 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do return { root, savedState, - newMVars := SSet.insert .empty root, parentMVar? := .none, } protected def GoalState.isConv (state: GoalState): Bool := @@ -89,15 +86,6 @@ private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tac Elab.Tactic.setGoals [goal] -private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext): SSet MVarId := - mctxNew.decls.foldl (fun acc mvarId mvarDecl => - if let .some prevMVarDecl := mctxOld.decls.find? mvarId then - assert! prevMVarDecl.type == mvarDecl.type - acc - else - acc.insert mvarId - ) SSet.empty - protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do let goal ← state.savedState.tactic.goals.get? goalId return { @@ -166,6 +154,21 @@ protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvar: MVarId) --- Tactic execution functions --- +protected def GoalState.step (state: GoalState) (mvarId: MVarId) (tacticM: Elab.Tactic.TacticM Unit) + : Elab.TermElabM GoalState := do + state.restoreElabM + unless (← getMCtx).decls.contains mvarId do + throwError s!"MVarId is not in context: {mvarId.name}" + mvarId.checkNotAssigned `GoalState.step + let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [mvarId] } + let nextElabState ← MonadBacktrack.saveState + return { + state with + savedState := { term := nextElabState, tactic := newGoals }, + parentMVar? := .some mvarId, + calcPrevRhs? := .none, + } + /-- Response for executing a tactic -/ inductive TacticResult where -- Goes to next state @@ -182,27 +185,12 @@ inductive TacticResult where /-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/ protected def GoalState.tryTacticM (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit): Elab.TermElabM TacticResult := do - state.restoreElabM - let goal ← match state.savedState.tactic.goals.get? goalId with + let mvarId ← match state.savedState.tactic.goals.get? goalId with | .some goal => pure $ goal | .none => return .indexError goalId - goal.checkNotAssigned `GoalState.tryTacticM try - let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] } - if (← getThe Core.State).messages.hasErrors then - let messages := (← getThe Core.State).messages.toArray - let errors ← (messages.map (·.data)).mapM fun md => md.toString - return .failure errors - let nextElabState ← MonadBacktrack.saveState - let nextMCtx := nextElabState.meta.meta.mctx - let prevMCtx := state.mctx - return .success { - state with - savedState := { term := nextElabState, tactic := newGoals }, - newMVars := newMVarSet prevMCtx nextMCtx, - parentMVar? := .some goal, - calcPrevRhs? := .none, - } + let nextState ← state.step mvarId tacticM + return .success nextState catch exception => return .failure #[← exception.toMessageData.toString] @@ -269,7 +257,6 @@ protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: Str term := ← MonadBacktrack.saveState, tactic := { goals := nextGoals } }, - newMVars := nextGoals.toSSet, parentMVar? := .some goal, calcPrevRhs? := .none } @@ -296,12 +283,9 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat): return (← MonadBacktrack.saveState, convMVar) try let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic - let prevMCtx := state.mctx - let nextMCtx := nextSavedState.term.meta.meta.mctx return .success { root := state.root, savedState := nextSavedState - newMVars := newMVarSet prevMCtx nextMCtx, parentMVar? := .some goal, convMVar? := .some (convRhs, goal), calcPrevRhs? := .none @@ -335,12 +319,9 @@ protected def GoalState.convExit (state: GoalState): MonadBacktrack.saveState try let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic - let nextMCtx := nextSavedState.term.meta.meta.mctx - let prevMCtx := state.savedState.term.meta.meta.mctx return .success { root := state.root, savedState := nextSavedState - newMVars := newMVarSet prevMCtx nextMCtx, parentMVar? := .some convGoal, convMVar? := .none calcPrevRhs? := .none @@ -420,7 +401,6 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): term := ← MonadBacktrack.saveState, tactic := { goals }, }, - newMVars := goals.toSSet, parentMVar? := .some goal, calcPrevRhs? } From 9b0456a5e0026ac5d8087a78fe3e3d5ff4f9b594 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 15 Aug 2024 23:17:15 -0700 Subject: [PATCH 09/19] refactor: MetaM form of have and let --- Pantograph/Goal.lean | 37 ++-------------- Pantograph/Library.lean | 2 +- Pantograph/Tactic/Prograde.lean | 76 ++++++++++++++++++++++++--------- 3 files changed, 60 insertions(+), 55 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index cd29d2a..b54c5f7 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -156,7 +156,6 @@ protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvar: MVarId) protected def GoalState.step (state: GoalState) (mvarId: MVarId) (tacticM: Elab.Tactic.TacticM Unit) : Elab.TermElabM GoalState := do - state.restoreElabM unless (← getMCtx).decls.contains mvarId do throwError s!"MVarId is not in context: {mvarId.name}" mvarId.checkNotAssigned `GoalState.step @@ -197,6 +196,7 @@ protected def GoalState.tryTacticM (state: GoalState) (goalId: Nat) (tacticM: El /-- Execute a string tactic on given state -/ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String): Elab.TermElabM TacticResult := do + state.restoreElabM let tactic ← match Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := if state.isConv then `conv else `tactic) @@ -223,45 +223,14 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Elab.TermElabM TacticResult := do state.restoreElabM - let goal ← match state.savedState.tactic.goals.get? goalId with - | .some goal => pure goal - | .none => return .indexError goalId - goal.checkNotAssigned `GoalState.tryLet let type ← match Parser.runParserCategory - (env := state.env) + (env := ← MonadEnv.getEnv) (catName := `term) (input := type) (fileName := filename) with | .ok syn => pure syn | .error error => return .parseError error - let binderName := binderName.toName - try - -- Implemented similarly to the intro tactic - let nextGoals: List MVarId ← goal.withContext do - let type ← Elab.Term.elabType (stx := type) - let lctx ← MonadLCtx.getLCtx - - -- The branch goal inherits the same context, but with a different type - let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type - - let upstreamType := .letE binderName type mvarBranch (← goal.getType) false - let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) - upstreamType (kind := MetavarKind.synthetic) (userName := (← goal.getTag)) - - goal.assign mvarUpstream - - pure [mvarBranch.mvarId!, mvarUpstream.mvarId!] - return .success { - root := state.root, - savedState := { - term := ← MonadBacktrack.saveState, - tactic := { goals := nextGoals } - }, - parentMVar? := .some goal, - calcPrevRhs? := .none - } - catch exception => - return .failure #[← exception.toMessageData.toString] + state.tryTacticM goalId $ Tactic.evalLet binderName.toName type /-- Enter conv tactic mode -/ protected def GoalState.conv (state: GoalState) (goalId: Nat): diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 4b8cc9d..da2ae5c 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -168,7 +168,7 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St | .error error => return .parseError error runTermElabM do state.restoreElabM - state.tryTacticM goalId (Tactic.«have» binderName.toName type) + state.tryTacticM goalId $ Tactic.evalHave binderName.toName type @[export pantograph_goal_evaluate_m] protected def GoalState.tryEvaluate (state: GoalState) (goalId: Nat) (binderName: String) (expr: String): CoreM TacticResult := do let expr ← match (← Compile.parseTermM expr) with diff --git a/Pantograph/Tactic/Prograde.lean b/Pantograph/Tactic/Prograde.lean index 59acaf1..d6abb16 100644 --- a/Pantograph/Tactic/Prograde.lean +++ b/Pantograph/Tactic/Prograde.lean @@ -19,29 +19,65 @@ def evaluate (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do pure [mvarUpstream.mvarId!] Elab.Tactic.setGoals nextGoals -def «have» (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do +structure BranchResult where + fvarId?: Option FVarId := .none + main: MVarId + branch: MVarId + +def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do + mvarId.checkNotAssigned `Pantograph.Tactic.have + let lctx ← MonadLCtx.getLCtx + -- The branch goal inherits the same context, but with a different type + let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type + + -- Create the context for the `upstream` goal + let fvarId ← mkFreshFVarId + let lctxUpstream := lctx.mkLocalDecl fvarId binderName type + let mvarUpstream ← + withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do + Meta.withNewLocalInstances #[.fvar fvarId] 0 do + let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) + (← mvarId.getType) (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag) + --let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream + mvarId.assign mvarUpstream + pure mvarUpstream + + return { + fvarId? := .some fvarId, + main := mvarUpstream.mvarId!, + branch := mvarBranch.mvarId!, + } + +def evalHave (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do let goal ← Elab.Tactic.getMainGoal let nextGoals: List MVarId ← goal.withContext do let type ← Elab.Term.elabType (stx := type) - let lctx ← MonadLCtx.getLCtx - - -- The branch goal inherits the same context, but with a different type - let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type - - -- Create the context for the `upstream` goal - let fvarId ← mkFreshFVarId - let lctxUpstream := lctx.mkLocalDecl fvarId binderName type - let fvar := mkFVar fvarId - let mvarUpstream ← - withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do - Meta.withNewLocalInstances #[fvar] 0 do - let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) - (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous) - --let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream - goal.assign mvarUpstream - pure mvarUpstream - - pure [mvarBranch.mvarId!, mvarUpstream.mvarId!] + let result ← «have» goal binderName type + pure [result.branch, result.main] Elab.Tactic.setGoals nextGoals +def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do + mvarId.checkNotAssigned `Pantograph.Tactic.let + let lctx ← MonadLCtx.getLCtx + + -- The branch goal inherits the same context, but with a different type + let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type + + assert! ¬ type.hasLooseBVars + let upstreamType := .letE binderName type mvarBranch (← mvarId.getType) false + let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) + upstreamType (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag) + mvarId.assign mvarUpstream + + return { + main := mvarUpstream.mvarId!, + branch := mvarBranch.mvarId!, + } + +def evalLet (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do + let goal ← Elab.Tactic.getMainGoal + let type ← goal.withContext $ Elab.Term.elabType (stx := type) + let result ← «let» goal binderName type + Elab.Tactic.setGoals [result.branch, result.main] + end Pantograph.Tactic From 1e7a186bb1d423585630d0370bec8612d6fc73be Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 15 Aug 2024 23:23:17 -0700 Subject: [PATCH 10/19] refactor: MetaM form of define (evaluate) --- Pantograph/Library.lean | 6 +++--- Pantograph/Tactic/Prograde.lean | 27 +++++++++++++++------------ Test/Tactic/Prograde.lean | 4 ++-- 3 files changed, 20 insertions(+), 17 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index da2ae5c..6fff21e 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -169,14 +169,14 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St runTermElabM do state.restoreElabM state.tryTacticM goalId $ Tactic.evalHave binderName.toName type -@[export pantograph_goal_evaluate_m] -protected def GoalState.tryEvaluate (state: GoalState) (goalId: Nat) (binderName: String) (expr: String): CoreM TacticResult := do +@[export pantograph_goal_try_define_m] +protected def GoalState.tryDefine (state: GoalState) (goalId: Nat) (binderName: String) (expr: String): CoreM TacticResult := do let expr ← match (← Compile.parseTermM expr) with | .ok syn => pure syn | .error error => return .parseError error runTermElabM do state.restoreElabM - state.tryTacticM goalId (Tactic.evaluate binderName.toName expr) + state.tryTacticM goalId (Tactic.evalDefine binderName.toName expr) @[export pantograph_goal_let_m] def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := runTermElabM <| state.tryLet goalId binderName type diff --git a/Pantograph/Tactic/Prograde.lean b/Pantograph/Tactic/Prograde.lean index d6abb16..dd34684 100644 --- a/Pantograph/Tactic/Prograde.lean +++ b/Pantograph/Tactic/Prograde.lean @@ -5,19 +5,22 @@ open Lean namespace Pantograph.Tactic -def evaluate (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do - let goal ← Elab.Tactic.getMainGoal - let nextGoals ← goal.withContext do - let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none) - let type ← Meta.inferType expr +/-- Introduces a fvar to the current mvar -/ +def define (mvarId: MVarId) (binderName: Name) (expr: Expr): MetaM (FVarId × MVarId) := mvarId.withContext do + mvarId.checkNotAssigned `Pantograph.Tactic.define + let type ← Meta.inferType expr - let mvarUpstream ← Meta.withLetDecl binderName type expr λ _ => do - let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) - (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous) - goal.assign mvarUpstream - pure mvarUpstream - pure [mvarUpstream.mvarId!] - Elab.Tactic.setGoals nextGoals + Meta.withLetDecl binderName type expr λ fvar => do + let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) + (← mvarId.getType) (kind := MetavarKind.synthetic) (userName := .anonymous) + mvarId.assign mvarUpstream + pure (fvar.fvarId!, mvarUpstream.mvarId!) + +def evalDefine (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do + let goal ← Elab.Tactic.getMainGoal + let expr ← goal.withContext $ Elab.Term.elabTerm (stx := expr) (expectedType? := .none) + let (_, mvarId) ← define goal binderName expr + Elab.Tactic.setGoals [mvarId] structure BranchResult where fvarId?: Option FVarId := .none diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean index 15da63e..6b7cd44 100644 --- a/Test/Tactic/Prograde.lean +++ b/Test/Tactic/Prograde.lean @@ -32,7 +32,7 @@ def test_eval : TestT Elab.TermElabM Unit := do ], target, }) - let tactic := Tactic.evaluate `h2 e + let tactic := Tactic.evalDefine `h2 e let m := .mvar ⟨uniq 13⟩ let [newGoal] ← runTacticOnMVar tactic goal.mvarId! | panic! "Incorrect goal number" addTest $ LSpec.test "goals after" ((← toCondensedGoal newGoal).devolatilize == { @@ -73,7 +73,7 @@ def test_proof_eval : TestT Elab.TermElabM Unit := do let evalBind := "y" let evalExpr := "Or.inl h" - let state2 ← match ← state1.tryEvaluate (goalId := 0) (binderName := evalBind) (expr := evalExpr) with + let state2 ← match ← state1.tryDefine (goalId := 0) (binderName := evalBind) (expr := evalExpr) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString From 5b4f8a37ebbbbd435b400af11ce65ec9c96ec428 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 15 Aug 2024 23:41:17 -0700 Subject: [PATCH 11/19] refactor: All Tactic/ tactics into MetaM form --- Pantograph/Goal.lean | 4 +- Pantograph/Library.lean | 6 - Pantograph/Tactic/Congruence.lean | 153 ++++++++++++++------------ Pantograph/Tactic/MotivatedApply.lean | 68 ++++++------ Pantograph/Tactic/NoConfuse.lean | 20 ++-- Test/Tactic/Congruence.lean | 8 +- Test/Tactic/MotivatedApply.lean | 6 +- Test/Tactic/NoConfuse.lean | 6 +- 8 files changed, 141 insertions(+), 130 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index b54c5f7..9be5164 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -383,13 +383,13 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu let recursor ← match (← Compile.parseTermM recursor) with | .ok syn => pure syn | .error error => return .parseError error - state.tryTacticM goalId (tacticM := Tactic.motivatedApply recursor) + state.tryTacticM goalId (tacticM := Tactic.evalMotivatedApply recursor) protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Elab.TermElabM TacticResult := do state.restoreElabM let eq ← match (← Compile.parseTermM eq) with | .ok syn => pure syn | .error error => return .parseError error - state.tryTacticM goalId (tacticM := Tactic.noConfuse eq) + state.tryTacticM goalId (tacticM := Tactic.evalNoConfuse eq) end Pantograph diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 6fff21e..c4ce4ff 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -192,11 +192,5 @@ def goalCalc (state: GoalState) (goalId: Nat) (pred: String): CoreM TacticResult @[export pantograph_goal_focus] def goalFocus (state: GoalState) (goalId: Nat): Option GoalState := state.focus goalId -@[export pantograph_goal_motivated_apply_m] -def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): CoreM TacticResult := - runTermElabM <| state.tryMotivatedApply goalId recursor -@[export pantograph_goal_no_confuse_m] -def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): CoreM TacticResult := - runTermElabM <| state.tryNoConfuse goalId eq end Pantograph diff --git a/Pantograph/Tactic/Congruence.lean b/Pantograph/Tactic/Congruence.lean index bbb9d75..2ff23d2 100644 --- a/Pantograph/Tactic/Congruence.lean +++ b/Pantograph/Tactic/Congruence.lean @@ -4,82 +4,95 @@ open Lean namespace Pantograph.Tactic -def congruenceArg: Elab.Tactic.TacticM Unit := do +def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do + mvarId.checkNotAssigned `Pantograph.Tactic.congruenceArg + let target ← mvarId.getType + let .some (β, _, _) := target.eq? | throwError "Goal is not an Eq" + let userName := (← mvarId.getDecl).userName + + let u ← Meta.mkFreshLevelMVar + let α ← Meta.mkFreshExprMVar (.some $ mkSort u) + .natural (userName := userName ++ `α) + let f ← Meta.mkFreshExprMVar (.some <| .forallE .anonymous α β .default) + .synthetic (userName := userName ++ `f) + let a₁ ← Meta.mkFreshExprMVar (.some α) + .synthetic (userName := userName ++ `a₁) + let a₂ ← Meta.mkFreshExprMVar (.some α) + .synthetic (userName := userName ++ `a₂) + let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂) + .synthetic (userName := userName ++ `h) + let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) target + let conduit ← Meta.mkFreshExprMVar conduitType + .synthetic (userName := userName ++ `conduit) + mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h) + let result := [α, a₁, a₂, f, h, conduit] + return result.map (·.mvarId!) + +def evalCongruenceArg: Elab.Tactic.TacticM Unit := do let goal ← Elab.Tactic.getMainGoal - let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq" - let userName := (← goal.getDecl).userName + let nextGoals ← congruenceArg goal + Elab.Tactic.setGoals nextGoals - let nextGoals ← goal.withContext do - let u ← Meta.mkFreshLevelMVar - let α ← Meta.mkFreshExprMVar (.some $ mkSort u) - .natural (userName := userName ++ `α) - let f ← Meta.mkFreshExprMVar (.some <| .forallE .anonymous α β .default) - .synthetic (userName := userName ++ `f) - let a₁ ← Meta.mkFreshExprMVar (.some α) - .synthetic (userName := userName ++ `a₁) - let a₂ ← Meta.mkFreshExprMVar (.some α) - .synthetic (userName := userName ++ `a₂) - let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂) - .synthetic (userName := userName ++ `h) - let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) (← goal.getType) - let conduit ← Meta.mkFreshExprMVar conduitType - .synthetic (userName := userName ++ `conduit) - goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h) - return [α, a₁, a₂, f, h, conduit] - Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!) +def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do + mvarId.checkNotAssigned `Pantograph.Tactic.congruenceFun + let target ← mvarId.getType + let .some (β, _, _) := target.eq? | throwError "Goal is not an Eq" + let userName := (← mvarId.getDecl).userName + let u ← Meta.mkFreshLevelMVar + let α ← Meta.mkFreshExprMVar (.some $ mkSort u) + .natural (userName := userName ++ `α) + let fType := .forallE .anonymous α β .default + let f₁ ← Meta.mkFreshExprMVar (.some fType) + .synthetic (userName := userName ++ `f₁) + let f₂ ← Meta.mkFreshExprMVar (.some fType) + .synthetic (userName := userName ++ `f₂) + let a ← Meta.mkFreshExprMVar (.some α) + .synthetic (userName := userName ++ `a) + let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂) + .synthetic (userName := userName ++ `h) + let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) target + let conduit ← Meta.mkFreshExprMVar conduitType + .synthetic (userName := userName ++ `conduit) + mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a) + let result := [α, f₁, f₂, h, a, conduit] + return result.map (·.mvarId!) -def congruenceFun: Elab.Tactic.TacticM Unit := do +def evalCongruenceFun: Elab.Tactic.TacticM Unit := do let goal ← Elab.Tactic.getMainGoal - let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq" - let userName := (← goal.getDecl).userName + let nextGoals ← congruenceFun goal + Elab.Tactic.setGoals nextGoals - let nextGoals ← goal.withContext do - let u ← Meta.mkFreshLevelMVar - let α ← Meta.mkFreshExprMVar (.some $ mkSort u) - .natural (userName := userName ++ `α) - let fType := .forallE .anonymous α β .default - let f₁ ← Meta.mkFreshExprMVar (.some fType) - .synthetic (userName := userName ++ `f₁) - let f₂ ← Meta.mkFreshExprMVar (.some fType) - .synthetic (userName := userName ++ `f₂) - let a ← Meta.mkFreshExprMVar (.some α) - .synthetic (userName := userName ++ `a) - let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂) - .synthetic (userName := userName ++ `h) - let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) (← goal.getType) - let conduit ← Meta.mkFreshExprMVar conduitType - .synthetic (userName := userName ++ `conduit) - goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a) - return [α, f₁, f₂, h, a, conduit] - Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!) +def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do + mvarId.checkNotAssigned `Pantograph.Tactic.congruence + let target ← mvarId.getType + let .some (β, _, _) := target.eq? | throwError "Goal is not an Eq" + let userName := (← mvarId.getDecl).userName + let u ← Meta.mkFreshLevelMVar + let α ← Meta.mkFreshExprMVar (.some $ mkSort u) + .natural (userName := userName ++ `α) + let fType := .forallE .anonymous α β .default + let f₁ ← Meta.mkFreshExprMVar (.some fType) + .synthetic (userName := userName ++ `f₁) + let f₂ ← Meta.mkFreshExprMVar (.some fType) + .synthetic (userName := userName ++ `f₂) + let a₁ ← Meta.mkFreshExprMVar (.some α) + .synthetic (userName := userName ++ `a₁) + let a₂ ← Meta.mkFreshExprMVar (.some α) + .synthetic (userName := userName ++ `a₂) + let h₁ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂) + .synthetic (userName := userName ++ `h₁) + let h₂ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂) + .synthetic (userName := userName ++ `h₂) + let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) target + let conduit ← Meta.mkFreshExprMVar conduitType + .synthetic (userName := userName ++ `conduit) + mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂) + let result := [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit] + return result.map (·.mvarId!) -def congruence: Elab.Tactic.TacticM Unit := do +def evalCongruence: Elab.Tactic.TacticM Unit := do let goal ← Elab.Tactic.getMainGoal - let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq" - let userName := (← goal.getDecl).userName - - let nextGoals ← goal.withContext do - let u ← Meta.mkFreshLevelMVar - let α ← Meta.mkFreshExprMVar (.some $ mkSort u) - .natural (userName := userName ++ `α) - let fType := .forallE .anonymous α β .default - let f₁ ← Meta.mkFreshExprMVar (.some fType) - .synthetic (userName := userName ++ `f₁) - let f₂ ← Meta.mkFreshExprMVar (.some fType) - .synthetic (userName := userName ++ `f₂) - let a₁ ← Meta.mkFreshExprMVar (.some α) - .synthetic (userName := userName ++ `a₁) - let a₂ ← Meta.mkFreshExprMVar (.some α) - .synthetic (userName := userName ++ `a₂) - let h₁ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂) - .synthetic (userName := userName ++ `h₁) - let h₂ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂) - .synthetic (userName := userName ++ `h₂) - let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) (← goal.getType) - let conduit ← Meta.mkFreshExprMVar conduitType - .synthetic (userName := userName ++ `conduit) - goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂) - return [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit] - Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!) + let nextGoals ← congruence goal + Elab.Tactic.setGoals nextGoals end Pantograph.Tactic diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean index f570560..37d0099 100644 --- a/Pantograph/Tactic/MotivatedApply.lean +++ b/Pantograph/Tactic/MotivatedApply.lean @@ -62,44 +62,44 @@ def collectMotiveArguments (forallBody: Expr): SSet Nat := | _ => SSet.empty /-- Applies a symbol of the type `∀ (motive: α → Sort u) (a: α)..., (motive α)` -/ -def motivatedApply: Elab.Tactic.Tactic := λ stx => do - let goal ← Elab.Tactic.getMainGoal - let nextGoals: List MVarId ← goal.withContext do - let recursor ← Elab.Term.elabTerm (stx := stx) .none - let recursorType ← Meta.inferType recursor +def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (List Meta.InductionSubgoal) := mvarId.withContext do + mvarId.checkNotAssigned `Pantograph.Tactic.motivatedApply + let recursorType ← Meta.inferType recursor + let resultant ← mvarId.getType - let resultant ← goal.getType + let info ← match getRecursorInformation recursorType with + | .some info => pure info + | .none => throwError "Recursor return type does not correspond with the invocation of a motive: {← Meta.ppExpr recursorType}" - let info ← match getRecursorInformation recursorType with - | .some info => pure info - | .none => throwError "Recursor return type does not correspond with the invocation of a motive: {← Meta.ppExpr recursorType}" + let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do + if i ≥ info.nArgs then + return prev + else + let argType := info.args.get! i + -- If `argType` has motive references, its goal needs to be placed in it + let argType := argType.instantiateRev prev + let bvarIndex := info.nArgs - i - 1 + let argGoal ← if bvarIndex = info.iMotive then + let surrogateMotiveType ← info.surrogateMotiveType prev resultant + Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive) + else + Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous) + let prev := prev ++ [argGoal] + go (i + 1) prev + termination_by info.nArgs - i + let mut newMVars ← go 0 #[] - let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do - if i ≥ info.nArgs then - return prev - else - let argType := info.args.get! i - -- If `argType` has motive references, its goal needs to be placed in it - let argType := argType.instantiateRev prev - let bvarIndex := info.nArgs - i - 1 - let argGoal ← if bvarIndex = info.iMotive then - let surrogateMotiveType ← info.surrogateMotiveType prev resultant - Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive) - else - Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous) - let prev := prev ++ [argGoal] - go (i + 1) prev - termination_by info.nArgs - i - let mut newMVars ← go 0 #[] + -- Create the conduit type which proves the result of the motive is equal to the goal + let conduitType ← info.conduitType newMVars resultant + let goalConduit ← Meta.mkFreshExprMVar conduitType .natural (userName := `conduit) + mvarId.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars) + newMVars := newMVars ++ [goalConduit] - -- Create the conduit type which proves the result of the motive is equal to the goal - let conduitType ← info.conduitType newMVars resultant - let goalConduit ← Meta.mkFreshExprMVar conduitType .natural (userName := `conduit) - goal.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars) - newMVars := newMVars ++ [goalConduit] + return newMVars.toList.map (λ mvar => { mvarId := mvar.mvarId!}) - let nextGoals := newMVars.toList.map (·.mvarId!) - pure nextGoals - Elab.Tactic.setGoals nextGoals +def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do + let recursor ← Elab.Term.elabTerm (stx := stx) .none + let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor + Elab.Tactic.setGoals $ nextGoals.map (·.mvarId) end Pantograph.Tactic diff --git a/Pantograph/Tactic/NoConfuse.lean b/Pantograph/Tactic/NoConfuse.lean index b8bc84e..f4ce78f 100644 --- a/Pantograph/Tactic/NoConfuse.lean +++ b/Pantograph/Tactic/NoConfuse.lean @@ -4,15 +4,19 @@ open Lean namespace Pantograph.Tactic -def noConfuse: Elab.Tactic.Tactic := λ stx => do - let goal ← Elab.Tactic.getMainGoal - goal.withContext do - let absurd ← Elab.Term.elabTerm (stx := stx) .none - let noConfusion ← Meta.mkNoConfusion (target := ← goal.getType) (h := absurd) +def noConfuse (mvarId: MVarId) (h: Expr): MetaM Unit := mvarId.withContext do + mvarId.checkNotAssigned `Pantograph.Tactic.noConfuse + let target ← mvarId.getType + let noConfusion ← Meta.mkNoConfusion (target := target) (h := h) - unless ← Meta.isDefEq (← Meta.inferType noConfusion) (← goal.getType) do - throwError "invalid noConfuse call: The resultant type {← Meta.ppExpr $ ← Meta.inferType noConfusion} cannot be unified with {← Meta.ppExpr $ ← goal.getType}" - goal.assign noConfusion + unless ← Meta.isDefEq (← Meta.inferType noConfusion) target do + throwError "invalid noConfuse call: The resultant type {← Meta.ppExpr $ ← Meta.inferType noConfusion} cannot be unified with {← Meta.ppExpr target}" + mvarId.assign noConfusion + +def evalNoConfuse: Elab.Tactic.Tactic := λ stx => do + let goal ← Elab.Tactic.getMainGoal + let h ← goal.withContext $ Elab.Term.elabTerm (stx := stx) .none + noConfuse goal h Elab.Tactic.setGoals [] end Pantograph.Tactic diff --git a/Test/Tactic/Congruence.lean b/Test/Tactic/Congruence.lean index 38c94f3..836041c 100644 --- a/Test/Tactic/Congruence.lean +++ b/Test/Tactic/Congruence.lean @@ -12,7 +12,7 @@ def test_congr_arg_list : TestT Elab.TermElabM Unit := do let expr ← parseSentence expr Meta.lambdaTelescope expr $ λ _ body => do let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId! + let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId! addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = [ (`α, "Sort ?u.30"), @@ -34,7 +34,7 @@ def test_congr_arg : TestT Elab.TermElabM Unit := do let expr ← parseSentence expr Meta.lambdaTelescope expr $ λ _ body => do let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId! + let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId! addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = [ (`α, "Sort ?u.70"), @@ -49,7 +49,7 @@ def test_congr_fun : TestT Elab.TermElabM Unit := do let expr ← parseSentence expr Meta.lambdaTelescope expr $ λ _ body => do let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let newGoals ← runTacticOnMVar Tactic.congruenceFun target.mvarId! + let newGoals ← runTacticOnMVar Tactic.evalCongruenceFun target.mvarId! addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = [ (`α, "Sort ?u.159"), @@ -64,7 +64,7 @@ def test_congr : TestT Elab.TermElabM Unit := do let expr ← parseSentence expr Meta.lambdaTelescope expr $ λ _ body => do let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let newGoals ← runTacticOnMVar Tactic.congruence target.mvarId! + let newGoals ← runTacticOnMVar Tactic.evalCongruence target.mvarId! addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = [ (`α, "Sort ?u.10"), diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean index 091e309..4fb05e3 100644 --- a/Test/Tactic/MotivatedApply.lean +++ b/Test/Tactic/MotivatedApply.lean @@ -33,7 +33,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do | .error error => throwError "Failed to parse: {error}" -- Apply the tactic let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let tactic := Tactic.motivatedApply recursor + let tactic := Tactic.evalMotivatedApply recursor let newGoals ← runTacticOnMVar tactic target.mvarId! let test := LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [ @@ -57,7 +57,7 @@ def test_list_brec_on : TestT Elab.TermElabM Unit := do | .error error => throwError "Failed to parse: {error}" -- Apply the tactic let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let tactic := Tactic.motivatedApply recursor + let tactic := Tactic.evalMotivatedApply recursor let newGoals ← runTacticOnMVar tactic target.mvarId! addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [ @@ -81,7 +81,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do Meta.lambdaTelescope expr $ λ _ body => do -- Apply the tactic let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let tactic := Tactic.motivatedApply recursor + let tactic := Tactic.evalMotivatedApply recursor let newGoals ← runTacticOnMVar tactic target.mvarId! let majorId := 67 addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = diff --git a/Test/Tactic/NoConfuse.lean b/Test/Tactic/NoConfuse.lean index cc15198..ac277e2 100644 --- a/Test/Tactic/NoConfuse.lean +++ b/Test/Tactic/NoConfuse.lean @@ -20,7 +20,7 @@ def test_nat : TestT Elab.TermElabM Unit := do | .error error => throwError "Failed to parse: {error}" -- Apply the tactic let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let tactic := Tactic.noConfuse recursor + let tactic := Tactic.evalNoConfuse recursor let newGoals ← runTacticOnMVar tactic target.mvarId! addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = []) @@ -38,7 +38,7 @@ def test_nat_fail : TestT Elab.TermElabM Unit := do -- Apply the tactic let target ← Meta.mkFreshExprSyntheticOpaqueMVar body try - let tactic := Tactic.noConfuse recursor + let tactic := Tactic.evalNoConfuse recursor let _ ← runTacticOnMVar tactic target.mvarId! addTest $ assertUnreachable "Tactic should fail" catch _ => @@ -57,7 +57,7 @@ def test_list : TestT Elab.TermElabM Unit := do | .error error => throwError "Failed to parse: {error}" -- Apply the tactic let target ← Meta.mkFreshExprSyntheticOpaqueMVar body - let tactic := Tactic.noConfuse recursor + let tactic := Tactic.evalNoConfuse recursor let newGoals ← runTacticOnMVar tactic target.mvarId! addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = []) From d17b21e282f9f23ac9105d2241e805a1553fde2b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 16 Aug 2024 00:32:34 -0700 Subject: [PATCH 12/19] fix: Use `getMVarsNoDelayed` --- Pantograph/Tactic/Assign.lean | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) diff --git a/Pantograph/Tactic/Assign.lean b/Pantograph/Tactic/Assign.lean index cd9281f..af76bfd 100644 --- a/Pantograph/Tactic/Assign.lean +++ b/Pantograph/Tactic/Assign.lean @@ -4,14 +4,6 @@ open Lean namespace Pantograph.Tactic -private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext): SSet MVarId := - mctxNew.decls.foldl (fun acc mvarId mvarDecl => - if let .some prevMVarDecl := mctxOld.decls.find? mvarId then - assert! prevMVarDecl.type == mvarDecl.type - acc - else - acc.insert mvarId - ) SSet.empty def assign (goal: MVarId) (expr: Expr): MetaM (List MVarId) := do goal.checkNotAssigned `Pantograph.Tactic.assign @@ -21,7 +13,8 @@ def assign (goal: MVarId) (expr: Expr): MetaM (List MVarId) := do unless ← Meta.isDefEq goalType exprType do throwError s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} ≠ {← Meta.ppExpr goalType}" - let nextGoals ← Meta.getMVars expr + -- FIXME: Use `withCollectingNewGoalsFrom`. Think about how this interacts with elaboration ... + let nextGoals ← Meta.getMVarsNoDelayed expr goal.assign expr nextGoals.toList.filterM (not <$> ·.isAssigned) From e1b7eaab12084371bf27d9ae68da0431de8d37b7 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 17 Aug 2024 00:47:12 -0700 Subject: [PATCH 13/19] fix: Let tactic not bringing binder into scope --- Pantograph/Protocol.lean | 2 +- Pantograph/Serial.lean | 2 + Pantograph/Tactic/Assign.lean | 9 ++-- Pantograph/Tactic/Prograde.lean | 11 ++-- Test/Metavar.lean | 7 +-- Test/Proofs.lean | 81 +--------------------------- Test/Tactic/Prograde.lean | 93 +++++++++++++++++++++++++++++++++ 7 files changed, 113 insertions(+), 92 deletions(-) diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 1e4bc06..f954f0d 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -51,7 +51,7 @@ structure Variable where /-- The name displayed to the user -/ userName: String /-- Does the name contain a dagger -/ - isInaccessible?: Option Bool := .none + isInaccessible?: Option Bool := .some false type?: Option Expression := .none value?: Option Expression := .none deriving Lean.ToJson diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index b353785..9f54bbb 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -215,11 +215,13 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava return { name := ofName fvarId.name, userName:= ofName userName.simpMacroScopes, + isInaccessible? := .some userName.isInaccessibleUserName } | .ldecl _ fvarId userName _ _ _ _ => do return { name := ofName fvarId.name, userName := toString userName.simpMacroScopes, + isInaccessible? := .some userName.isInaccessibleUserName } let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do match localDecl with diff --git a/Pantograph/Tactic/Assign.lean b/Pantograph/Tactic/Assign.lean index af76bfd..ea08c48 100644 --- a/Pantograph/Tactic/Assign.lean +++ b/Pantograph/Tactic/Assign.lean @@ -19,9 +19,12 @@ def assign (goal: MVarId) (expr: Expr): MetaM (List MVarId) := do nextGoals.toList.filterM (not <$> ·.isAssigned) def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do - let goalType ← Elab.Tactic.getMainTarget - let expr ← Elab.Term.elabTermAndSynthesize (stx := stx) (expectedType? := .some goalType) - let nextGoals ← assign (← Elab.Tactic.getMainGoal) expr + let target ← Elab.Tactic.getMainTarget + let (expr, nextGoals) ← Elab.Tactic.elabTermWithHoles stx + (expectedType? := .some target) + (tagSuffix := .anonymous ) + (allowNaturalHoles := true) + (← Elab.Tactic.getMainGoal).assign expr Elab.Tactic.setGoals nextGoals diff --git a/Pantograph/Tactic/Prograde.lean b/Pantograph/Tactic/Prograde.lean index dd34684..c67102c 100644 --- a/Pantograph/Tactic/Prograde.lean +++ b/Pantograph/Tactic/Prograde.lean @@ -64,13 +64,14 @@ def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult let lctx ← MonadLCtx.getLCtx -- The branch goal inherits the same context, but with a different type - let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type + let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type (userName := binderName) assert! ¬ type.hasLooseBVars - let upstreamType := .letE binderName type mvarBranch (← mvarId.getType) false - let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) - upstreamType (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag) - mvarId.assign mvarUpstream + let mvarUpstream ← Meta.withLetDecl binderName type mvarBranch $ λ fvar => do + let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) + (type := ← mvarId.getType) (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag) + mvarId.assign $ .letE binderName type fvar mvarUpstream (nonDep := false) + pure mvarUpstream return { main := mvarUpstream.mvarId!, diff --git a/Test/Metavar.lean b/Test/Metavar.lean index 3849b44..65e43a3 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -198,15 +198,16 @@ def test_proposition_generation: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) = - #[.some "∀ (x : Nat), ?m.29 x"]) + #[.some "?m.29 x"]) addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone - let state3 ← match ← state2.tryAssign (goalId := 0) (expr := "fun x => Eq.refl x") with + let assign := "Eq.refl x" + let state3 ← match ← state2.tryAssign (goalId := 0) (expr := assign) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) = + addTest $ LSpec.check s!":= {assign}" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) = #[]) addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 8e0f78d..d138e4c 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -175,7 +175,7 @@ def test_delta_variable: TestM Unit := do vars := (nameType.map fun x => ({ userName := x.fst, type? := x.snd.map (λ type => { pp? := type }), - isInaccessible? := x.snd.map (λ _ => false) + isInaccessible? := .some false, })).toArray } @@ -544,83 +544,6 @@ def test_calc: TestM Unit := do ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free buildGoal free target userName? -def test_let (specialized: Bool): TestM Unit := do - let state? ← startProof (.expr "∀ (a: Nat) (p: Prop), p → p ∨ ¬p") - let state0 ← match state? with - | .some state => pure state - | .none => do - addTest $ assertUnreachable "Goal could not parse" - return () - let tactic := "intro a p h" - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = - #[interiorGoal [] "p ∨ ¬p"]) - - - let letType := "Nat" - let expr := s!"let b: {letType} := _; _" - let result2 ← match specialized with - | true => state1.tryLet (goalId := 0) (binderName := "b") (type := letType) - | false => state1.tryAssign (goalId := 0) (expr := expr) - let state2 ← match result2 with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - let serializedState2 ← state2.serializeGoals (options := ← read) - addTest $ LSpec.check expr (serializedState2.map (·.devolatilize) = - #[ - interiorGoal [] letType, - interiorGoal [] "let b := ?m.20;\np ∨ ¬p" - ]) - -- Check that the goal mvar ids match up - addTest $ LSpec.check "(mvarId)" ((serializedState2.map (·.name) |>.get! 0) = "_uniq.20") - - let tactic := "exact a" - let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check tactic ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) = #[]) - - let state3r ← match state3.continue state2 with - | .error msg => do - addTest $ assertUnreachable $ msg - return () - | .ok state => pure state - addTest $ LSpec.check "(continue)" ((← state3r.serializeGoals (options := ← read)).map (·.devolatilize) = - #[interiorGoal [] "let b := a;\np ∨ ¬p"]) - - let tactic := "exact h" - match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with - | .failure #[message] => - addTest $ LSpec.check tactic (message = "type mismatch\n h\nhas type\n p : Prop\nbut is expected to have type\n let b := a;\n p ∨ ¬p : Prop") - | other => do - addTest $ assertUnreachable $ other.toString - - let tactic := "intro b" - let state4 ← match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - let tactic := "exact Or.inl h" - let state5 ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.test "(5 root)" state5.rootExpr?.isSome - where - interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) := - let free := [("a", "Nat"), ("p", "Prop"), ("h", "p")] ++ free - buildGoal free target userName? - def test_nat_zero_add: TestM Unit := do let state? ← startProof (.expr "∀ (n: Nat), n + 0 = n") let state0 ← match state? with @@ -795,8 +718,6 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("Or.comm", test_or_comm), ("conv", test_conv), ("calc", test_calc), - ("let via assign", test_let false), - ("let via tryLet", test_let true), ("Nat.zero_add", test_nat_zero_add), ("Nat.zero_add alt", test_nat_zero_add_alt), ] diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean index 6b7cd44..5b20011 100644 --- a/Test/Tactic/Prograde.lean +++ b/Test/Tactic/Prograde.lean @@ -162,12 +162,105 @@ def test_proof_have : TestT Elab.TermElabM Unit := do addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome +def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do + let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))" + let state0 ← GoalState.create rootExpr + let tactic := "intro a p h" + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) = + #[{ + target := { pp? := .some mainTarget }, + vars := interiorVars, + }]) + + let letType := "Nat" + let expr := s!"let b: {letType} := _; _" + let result2 ← match specialized with + | true => state1.tryLet (goalId := 0) (binderName := "b") (type := letType) + | false => state1.tryAssign (goalId := 0) (expr := expr) + let state2 ← match result2 with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + let serializedState2 ← state2.serializeGoals + let letBindName := if specialized then "b" else "_1" + addTest $ LSpec.check expr (serializedState2.map (·.devolatilize) = + #[{ + target := { pp? := .some letType }, + vars := interiorVars, + userName? := .some letBindName + }, + { + target := { pp? := .some mainTarget }, + vars := interiorVars ++ #[{ + userName := "b", + type? := .some { pp? := .some letType }, + value? := .some { pp? := .some s!"?{letBindName}" }, + }], + userName? := if specialized then .none else .some "_2", + } + ]) + + let tactic := "exact 1" + let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← state3.serializeGoals).map (·.devolatilize) = #[]) + + let state3r ← match state3.continue state2 with + | .error msg => do + addTest $ assertUnreachable $ msg + return () + | .ok state => pure state + addTest $ LSpec.check "(continue)" ((← state3r.serializeGoals).map (·.devolatilize) = + #[ + { + target := { pp? := .some mainTarget }, + vars := interiorVars ++ #[{ + userName := "b", + type? := .some { pp? := .some "Nat" }, + value? := .some { pp? := .some "1" }, + }], + userName? := if specialized then .none else .some "_2", + } + ]) + + let tactic := "exact h" + match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with + | .failure #[message] => + addTest $ LSpec.check tactic (message = s!"type mismatch\n h\nhas type\n a : Prop\nbut is expected to have type\n {mainTarget} : Prop") + | other => do + addTest $ assertUnreachable $ other.toString + + let tactic := "exact Or.inl (Or.inl h)" + let state4 ← match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.test "(4 root)" state4.rootExpr?.isSome + where + mainTarget := "(a ∨ p) ∨ a ∨ p" + interiorVars: Array Protocol.Variable := #[ + { userName := "a", type? := .some { pp? := .some "Prop" }, }, + { userName := "p", type? := .some { pp? := .some "Prop" }, }, + { userName := "h", type? := .some { pp? := .some "a" }, } + ] def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ ("eval", test_eval), ("Proof eval", test_proof_eval), ("Proof have", test_proof_have), + ("let via assign", test_let false), + ("let via tryLet", test_let true), ] |>.map (λ (name, t) => (name, runTestTermElabM env t)) end Pantograph.Test.Tactic.Prograde From 0c469027c6ccb84f14c2c097dbc96c2e152cdbc6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 17 Aug 2024 00:50:02 -0700 Subject: [PATCH 14/19] fix: Refactor mvar collection in assign tactic --- Pantograph/Tactic/Assign.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Pantograph/Tactic/Assign.lean b/Pantograph/Tactic/Assign.lean index ea08c48..acf5d16 100644 --- a/Pantograph/Tactic/Assign.lean +++ b/Pantograph/Tactic/Assign.lean @@ -4,7 +4,8 @@ open Lean namespace Pantograph.Tactic -def assign (goal: MVarId) (expr: Expr): MetaM (List MVarId) := do +/-- WARNING: This should be used with a function like `elabTermWithHoles` that properly collects the mvar information from `expr`. -/ +def assign (goal: MVarId) (expr: Expr) (nextGoals: List MVarId): MetaM (List MVarId) := do goal.checkNotAssigned `Pantograph.Tactic.assign -- This run of the unifier is critical in resolving mvars in passing @@ -12,19 +13,18 @@ def assign (goal: MVarId) (expr: Expr): MetaM (List MVarId) := do let goalType ← goal.getType unless ← Meta.isDefEq goalType exprType do throwError s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} ≠ {← Meta.ppExpr goalType}" - - -- FIXME: Use `withCollectingNewGoalsFrom`. Think about how this interacts with elaboration ... - let nextGoals ← Meta.getMVarsNoDelayed expr goal.assign expr - nextGoals.toList.filterM (not <$> ·.isAssigned) + nextGoals.filterM (not <$> ·.isAssigned) def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do let target ← Elab.Tactic.getMainTarget + let goal ← Elab.Tactic.getMainGoal + goal.checkNotAssigned `Pantograph.Tactic.evalAssign let (expr, nextGoals) ← Elab.Tactic.elabTermWithHoles stx (expectedType? := .some target) (tagSuffix := .anonymous ) (allowNaturalHoles := true) - (← Elab.Tactic.getMainGoal).assign expr + goal.assign expr Elab.Tactic.setGoals nextGoals From 43e11f1ba3176c94c7a0a8f78a36da6d70aa0be2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 17 Aug 2024 00:53:38 -0700 Subject: [PATCH 15/19] refactor: Always display isInaccessible --- Pantograph/Protocol.lean | 2 +- Pantograph/Serial.lean | 8 ++++---- Test/Common.lean | 1 - Test/Integration.lean | 6 +++--- Test/Metavar.lean | 1 - Test/Proofs.lean | 16 ++++++---------- Test/Tactic/Prograde.lean | 8 ++++---- 7 files changed, 18 insertions(+), 24 deletions(-) diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index f954f0d..1a52c8a 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -51,7 +51,7 @@ structure Variable where /-- The name displayed to the user -/ userName: String /-- Does the name contain a dagger -/ - isInaccessible?: Option Bool := .some false + isInaccessible: Bool := false type?: Option Expression := .none value?: Option Expression := .none deriving Lean.ToJson diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 9f54bbb..c788be2 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -215,13 +215,13 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava return { name := ofName fvarId.name, userName:= ofName userName.simpMacroScopes, - isInaccessible? := .some userName.isInaccessibleUserName + isInaccessible := userName.isInaccessibleUserName } | .ldecl _ fvarId userName _ _ _ _ => do return { name := ofName fvarId.name, userName := toString userName.simpMacroScopes, - isInaccessible? := .some userName.isInaccessibleUserName + isInaccessible := userName.isInaccessibleUserName } let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do match localDecl with @@ -231,7 +231,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava return { name := ofName fvarId.name, userName:= ofName userName, - isInaccessible? := .some userName.isInaccessibleUserName + isInaccessible := userName.isInaccessibleUserName type? := .some (← serializeExpression options type) } | .ldecl _ fvarId userName type val _ _ => do @@ -245,7 +245,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava return { name := ofName fvarId.name, userName:= ofName userName, - isInaccessible? := .some userName.isInaccessibleUserName + isInaccessible := userName.isInaccessibleUserName type? := .some (← serializeExpression options type) value? := value? } diff --git a/Test/Common.lean b/Test/Common.lean index 813e1b3..e572b72 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -138,7 +138,6 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O vars := (nameType.map fun x => ({ userName := x.fst, type? := .some { pp? := .some x.snd }, - isInaccessible? := .some false })).toArray } diff --git a/Test/Integration.lean b/Test/Integration.lean index 9f7ad92..931c9f2 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -85,14 +85,14 @@ def test_tactic : IO LSpec.TestSeq := let goal1: Protocol.Goal := { name := "_uniq.11", target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" }, - vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}], + vars := #[{ name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }}], } let goal2: Protocol.Goal := { name := "_uniq.17", target := { pp? := .some "x ∨ y → y ∨ x" }, vars := #[ - { name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}, - { name := "_uniq.16", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }} + { name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }}, + { name := "_uniq.16", userName := "y", type? := .some { pp? := .some "Prop" }} ], } subroutine_runner [ diff --git a/Test/Metavar.lean b/Test/Metavar.lean index 65e43a3..2fcab28 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -60,7 +60,6 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O vars := (nameType.map fun x => ({ userName := x.fst, type? := .some { pp? := .some x.snd }, - isInaccessible? := .some false })).toArray } def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do diff --git a/Test/Proofs.lean b/Test/Proofs.lean index d138e4c..ba97ad7 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -58,7 +58,6 @@ def buildNamedGoal (name: String) (nameType: List (String × String)) (target: S vars := (nameType.map fun x => ({ userName := x.fst, type? := .some { pp? := .some x.snd }, - isInaccessible? := .some false })).toArray } def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): @@ -69,7 +68,6 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O vars := (nameType.map fun x => ({ userName := x.fst, type? := .some { pp? := .some x.snd }, - isInaccessible? := .some false })).toArray } def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do @@ -175,7 +173,6 @@ def test_delta_variable: TestM Unit := do vars := (nameType.map fun x => ({ userName := x.fst, type? := x.snd.map (λ type => { pp? := type }), - isInaccessible? := .some false, })).toArray } @@ -256,9 +253,9 @@ def test_or_comm: TestM Unit := do name := state1g0, target := { pp? := .some "q ∨ p" }, vars := #[ - { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false }, - { name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false }, - { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" }, isInaccessible? := .some false } + { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" } }, + { name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" } }, + { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" } } ] }]) addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome @@ -351,9 +348,9 @@ def test_or_comm: TestM Unit := do userName? := .some caseName, target := { pp? := .some "q ∨ p" }, vars := #[ - { userName := "p", type? := .some typeProp, isInaccessible? := .some false }, - { userName := "q", type? := .some typeProp, isInaccessible? := .some false }, - { userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible? := .some true } + { userName := "p", type? := .some typeProp }, + { userName := "q", type? := .some typeProp }, + { userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible := true } ] } @@ -703,7 +700,6 @@ def test_nat_zero_add_alt: TestM Unit := do name := fvN, userName := "n", type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" }, - isInaccessible? := .some false }], } ]) diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean index 5b20011..dd194e7 100644 --- a/Test/Tactic/Prograde.lean +++ b/Test/Tactic/Prograde.lean @@ -82,13 +82,13 @@ def test_proof_eval : TestT Elab.TermElabM Unit := do #[{ target := { pp? := .some "(p ∨ q) ∨ p ∨ q"}, vars := #[ - { userName := "p", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false }, - { userName := "q", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false }, - { userName := "h", type? := .some { pp? := .some "p" }, isInaccessible? := .some false }, + { userName := "p", type? := .some { pp? := .some "Prop" } }, + { userName := "q", type? := .some { pp? := .some "Prop" } }, + { userName := "h", type? := .some { pp? := .some "p" } }, { userName := "y", type? := .some { pp? := .some "p ∨ ?m.25" }, value? := .some { pp? := .some "Or.inl h" }, - isInaccessible? := .some false } + } ] }]) From f87eed817fb28ae72bf0fba863747ad5ff5750e7 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 17 Aug 2024 01:59:48 -0700 Subject: [PATCH 16/19] build: Move non-package output to legacyPackages --- flake.nix | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/flake.nix b/flake.nix index 54a139f..e062e54 100644 --- a/flake.nix +++ b/flake.nix @@ -63,9 +63,11 @@ packages = { inherit (leanPkgs) lean lean-all; inherit (project) sharedLib executable; - inherit project leanPkgs; default = project.executable; }; + legacyPackages = { + inherit project leanPkgs; + }; checks = { test = pkgs.runCommand "test" { buildInputs = [ test.executable leanPkgs.lean-all ]; From 5d43068ec3170c02d4405f2d10762cfc69641671 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 17 Aug 2024 02:07:17 -0700 Subject: [PATCH 17/19] fix: Flake check failure --- flake.lock | 8 ++++---- flake.nix | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/flake.lock b/flake.lock index c803f65..e9b7a7b 100644 --- a/flake.lock +++ b/flake.lock @@ -91,16 +91,16 @@ "lspec": { "flake": false, "locked": { - "lastModified": 1701971219, - "narHash": "sha256-HYDRzkT2UaLDrqKNWesh9C4LJNt0JpW0u68wYVj4Byw=", + "lastModified": 1722857503, + "narHash": "sha256-F9uaymiw1wTCLrJm4n1Bpk3J8jW6poedQzvnnQlZ6Kw=", "owner": "lurk-lab", "repo": "LSpec", - "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114", + "rev": "8a51034d049c6a229d88dd62f490778a377eec06", "type": "github" }, "original": { "owner": "lurk-lab", - "ref": "3388be5a1d1390594a74ec469fd54a5d84ff6114", + "ref": "8a51034d049c6a229d88dd62f490778a377eec06", "repo": "LSpec", "type": "github" } diff --git a/flake.nix b/flake.nix index e062e54..088f306 100644 --- a/flake.nix +++ b/flake.nix @@ -9,7 +9,7 @@ url = "github:leanprover/lean4?ref=v4.10.0-rc1"; }; lspec = { - url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114"; + url = "github:lurk-lab/LSpec?ref=8a51034d049c6a229d88dd62f490778a377eec06"; flake = false; }; }; From 3733c10a4e303ead385b05c968bf3e296480d744 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 17 Aug 2024 16:47:21 -0700 Subject: [PATCH 18/19] refactor: Unify call convention Induction like tactics should return `Array InductionSubgoal`. Branching tactics should return their branch first. --- Pantograph/Tactic/MotivatedApply.lean | 6 +++--- Pantograph/Tactic/Prograde.lean | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean index 37d0099..99e499d 100644 --- a/Pantograph/Tactic/MotivatedApply.lean +++ b/Pantograph/Tactic/MotivatedApply.lean @@ -62,7 +62,7 @@ def collectMotiveArguments (forallBody: Expr): SSet Nat := | _ => SSet.empty /-- Applies a symbol of the type `∀ (motive: α → Sort u) (a: α)..., (motive α)` -/ -def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (List Meta.InductionSubgoal) := mvarId.withContext do +def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.InductionSubgoal) := mvarId.withContext do mvarId.checkNotAssigned `Pantograph.Tactic.motivatedApply let recursorType ← Meta.inferType recursor let resultant ← mvarId.getType @@ -95,11 +95,11 @@ def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (List Meta.Inductio mvarId.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars) newMVars := newMVars ++ [goalConduit] - return newMVars.toList.map (λ mvar => { mvarId := mvar.mvarId!}) + return newMVars.map (λ mvar => { mvarId := mvar.mvarId!}) def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do let recursor ← Elab.Term.elabTerm (stx := stx) .none let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor - Elab.Tactic.setGoals $ nextGoals.map (·.mvarId) + Elab.Tactic.setGoals $ nextGoals.toList.map (·.mvarId) end Pantograph.Tactic diff --git a/Pantograph/Tactic/Prograde.lean b/Pantograph/Tactic/Prograde.lean index c67102c..58c6050 100644 --- a/Pantograph/Tactic/Prograde.lean +++ b/Pantograph/Tactic/Prograde.lean @@ -24,8 +24,8 @@ def evalDefine (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do structure BranchResult where fvarId?: Option FVarId := .none - main: MVarId branch: MVarId + main: MVarId def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do mvarId.checkNotAssigned `Pantograph.Tactic.have @@ -47,8 +47,8 @@ def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResul return { fvarId? := .some fvarId, - main := mvarUpstream.mvarId!, branch := mvarBranch.mvarId!, + main := mvarUpstream.mvarId!, } def evalHave (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do @@ -74,8 +74,8 @@ def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult pure mvarUpstream return { - main := mvarUpstream.mvarId!, branch := mvarBranch.mvarId!, + main := mvarUpstream.mvarId!, } def evalLet (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do From edec0f5733207bba278701ce9a13ed127742bc5b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 26 Aug 2024 13:42:14 -0400 Subject: [PATCH 19/19] feat: Use CoreM for diag monad --- Pantograph/Serial.lean | 48 ++++++++++++++++++++++-------------------- 1 file changed, 25 insertions(+), 23 deletions(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index c788be2..93dfb95 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -289,29 +289,31 @@ protected def GoalState.serializeGoals /-- Print the metavariables in a readable format -/ @[export pantograph_goal_state_diag_m] -protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): MetaM String := do - goalState.restoreMetaM - let savedState := goalState.savedState - let goals := savedState.tactic.goals - let mctx ← getMCtx - let root := goalState.root - -- Print the root - let result: String ← match mctx.decls.find? root with - | .some decl => printMVar ">" root decl - | .none => pure s!">{root.name}: ??" - let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId => - match mctx.decls.find? mvarId with - | .some decl => printMVar "⊢" mvarId decl - | .none => pure s!"⊢{mvarId.name}: ??" - ) - let goals := goals.toSSet - let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) => - !(goals.contains mvarId || mvarId == root) && options.printAll) - |>.mapM (fun (mvarId, decl) => do - let pref := if parentHasMVar mvarId then " " else "~" - printMVar pref mvarId decl - ) - pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join) +protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): CoreM String := do + let metaM: MetaM String := do + goalState.restoreMetaM + let savedState := goalState.savedState + let goals := savedState.tactic.goals + let mctx ← getMCtx + let root := goalState.root + -- Print the root + let result: String ← match mctx.decls.find? root with + | .some decl => printMVar ">" root decl + | .none => pure s!">{root.name}: ??" + let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId => + match mctx.decls.find? mvarId with + | .some decl => printMVar "⊢" mvarId decl + | .none => pure s!"⊢{mvarId.name}: ??" + ) + let goals := goals.toSSet + let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) => + !(goals.contains mvarId || mvarId == root) && options.printAll) + |>.mapM (fun (mvarId, decl) => do + let pref := if parentHasMVar mvarId then " " else "~" + printMVar pref mvarId decl + ) + pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join) + metaM.run' {} where printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do let resultFVars: List String ←