From 9a5ee49778395409d99af04d6970c4f97b082194 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 24 Jan 2024 18:19:04 -0800 Subject: [PATCH 1/5] feat: Print parent expression assignment --- Pantograph.lean | 2 ++ Pantograph/Environment.lean | 8 +++----- Pantograph/Goal.lean | 17 +++++++++++++++-- Pantograph/Protocol.lean | 5 ++++- Test/Proofs.lean | 4 ++++ 5 files changed, 28 insertions(+), 8 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index 9d9399d..46729fc 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -206,8 +206,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | .some goalState => runMetaM <| do goalState.restoreMetaM let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr) + let parent? ← goalState.parentExpr?.mapM (λ expr => serialize_expression state.options expr) return .ok { root?, + parent?, } end Pantograph diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index 18e4445..b823e8f 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -7,8 +7,6 @@ open Pantograph namespace Pantograph.Environment -abbrev CR α := Except Protocol.InteractionError α - def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool := isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ info.isUnsafe where @@ -32,14 +30,14 @@ def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String : if is_symbol_unsafe_or_internal n info then Option.none else Option.some <| to_compact_symbol_name n info -def catalog (_: Protocol.EnvCatalog): CoreM (CR Protocol.EnvCatalogResult) := do +def catalog (_: Protocol.EnvCatalog): CoreM (Protocol.CR Protocol.EnvCatalogResult) := do let env ← Lean.MonadEnv.getEnv let names := env.constants.fold (init := #[]) (λ acc name info => match to_filtered_symbol name info with | .some x => acc.push x | .none => acc) return .ok { symbols := names } -def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (CR Protocol.EnvInspectResult) := do +def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do let env ← Lean.MonadEnv.getEnv let name := args.name.toName let info? := env.find? name @@ -90,7 +88,7 @@ def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (CR P } } | _ => core return .ok result -def addDecl (args: Protocol.EnvAdd): CoreM (CR Protocol.EnvAddResult) := do +def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do let env ← Lean.MonadEnv.getEnv let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do let type ← match syntax_from_str env args.type with diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 9b68319..bd28944 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -1,3 +1,4 @@ +import Pantograph.Protocol import Lean def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog := @@ -20,6 +21,9 @@ structure GoalState where -- The id of the goal in the parent parentGoalId: Nat := 0 + -- Parent state metavariable source + parentMVar: Option MVarId + abbrev M := Elab.TermElabM protected def GoalState.create (expr: Expr): M GoalState := do @@ -36,6 +40,7 @@ protected def GoalState.create (expr: Expr): M GoalState := do savedState, root, newMVars := SSet.insert .empty root, + parentMVar := .none, } protected def GoalState.goals (state: GoalState): List MVarId := state.savedState.tactic.goals @@ -114,10 +119,11 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String return acc.insert mvarId ) SSet.empty return .success { - state with + root := state.root, savedState := nextSavedState newMVars, parentGoalId := goalId, + parentMVar := .some goal, } protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do @@ -164,10 +170,11 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String Elab.Tactic.setGoals (← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned))) let nextSavedState ← MonadBacktrack.saveState return .success { - state with + root := state.root, savedState := nextSavedState, newMVars := newMVars.toSSet, parentGoalId := goalId, + parentMVar := .some goal, } catch exception => return .failure #[← exception.toMessageData.toString] @@ -213,5 +220,11 @@ protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := else assert! goalState.goals.isEmpty .some expr +protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do + let parent ← goalState.parentMVar + let expr := goalState.mctx.eAssignment.find! parent + let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) + return expr + end Pantograph diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 6869bdc..fcc253f 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -240,7 +240,9 @@ structure GoalPrint where deriving Lean.FromJson structure GoalPrintResult where -- The root expression - root?: Option Expression + root?: Option Expression := .none + -- How is this goal filled in relation to its children? + parent?: Option Expression := .none deriving Lean.ToJson -- Diagnostic Options, not available in REPL @@ -252,5 +254,6 @@ structure GoalDiag where printAll: Bool := false instantiate: Bool := true +abbrev CR α := Except InteractionError α end Pantograph.Protocol diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 8992697..224bb22 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -231,6 +231,8 @@ def proof_or_comm: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () + let state3_1parent ← serialize_expression_ast state3_1.parentExpr?.get! (sanitize := false) + addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.83))") addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1) let state4_1 ← match ← state3_1.execute (goalId := 0) (tactic := "assumption") with | .success state => pure state @@ -238,6 +240,8 @@ def proof_or_comm: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check " assumption" state4_1.goals.isEmpty + let state4_1parent ← serialize_expression_ast state4_1.parentExpr?.get! (sanitize := false) + addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.49)") addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone let state3_2 ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with | .success state => pure state From 6d22841a276e36de88ce5eed5ec2efb6e7af45a3 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 30 Jan 2024 16:37:35 -0800 Subject: [PATCH 2/5] doc: Correct comment about parent filling expr --- Pantograph/Protocol.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index fcc253f..84e0cc2 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -241,7 +241,7 @@ structure GoalPrint where structure GoalPrintResult where -- The root expression root?: Option Expression := .none - -- How is this goal filled in relation to its children? + -- The filling expression of the parent goal parent?: Option Expression := .none deriving Lean.ToJson From 5720c725154cb54b3db6b8a6e6a6a1d6e0082192 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 30 Jan 2024 17:22:20 -0800 Subject: [PATCH 3/5] feat: Prevent crash during rootExpr call --- Pantograph/Goal.lean | 6 +++--- Test/Proofs.lean | 6 ++++++ 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index bd28944..630637d 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -210,8 +210,8 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except else target.resume (goals := branch.goals) -protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := - let expr := goalState.mctx.eAssignment.find! goalState.root +protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do + let expr ← goalState.mctx.eAssignment.find? goalState.root let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) if expr.hasMVar then -- Must not assert that the goal state is empty here. We could be in a branch goal. @@ -219,7 +219,7 @@ protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := .none else assert! goalState.goals.isEmpty - .some expr + return expr protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do let parent ← goalState.parentMVar let expr := goalState.mctx.eAssignment.find! parent diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 224bb22..07e4cea 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -210,6 +210,8 @@ def proof_or_comm: TestM Unit := do | .none => do addTest $ assertUnreachable "Goal could not parse" return () + addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone + addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") with | .success state => pure state @@ -218,6 +220,8 @@ def proof_or_comm: TestM Unit := do return () addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"]) + addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome + addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone let state2 ← match ← state1.execute (goalId := 0) (tactic := "cases h") with | .success state => pure state | other => do @@ -225,6 +229,8 @@ def proof_or_comm: TestM Unit := do return () addTest $ LSpec.check "cases h" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = #[branchGoal "inl" "p", branchGoal "inr" "q"]) + addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome + addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with | .success state => pure state From 4a98b902895f3f77ff1781038bd0b96892c1f614 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 30 Jan 2024 17:45:32 -0800 Subject: [PATCH 4/5] chore: Version bump to 0.2.12-alpha --- Pantograph/Version.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean index 67cbb8f..7bf12f9 100644 --- a/Pantograph/Version.lean +++ b/Pantograph/Version.lean @@ -1,5 +1,5 @@ namespace Pantograph -def version := "0.2.10-alpha" +def version := "0.2.12-alpha" end Pantograph From d57612ec71e9f0416d1e42dc01f030522abbc901 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 15 Feb 2024 14:47:09 -0800 Subject: [PATCH 5/5] test: Delayed metavariable assignment --- Test/Proofs.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 07e4cea..85ba66d 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -232,6 +232,11 @@ def proof_or_comm: TestM Unit := do addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone + let state2parent ← serialize_expression_ast state2.parentExpr?.get! (sanitize := false) + -- This is due to delayed assignment + addTest $ LSpec.test "(2 parent)" (state2parent == + "((:mv _uniq.45) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))") + let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with | .success state => pure state | other => do