From 9a5ee49778395409d99af04d6970c4f97b082194 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 24 Jan 2024 18:19:04 -0800 Subject: [PATCH] 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