feat: Print parent expression assignment

This commit is contained in:
Leni Aniva 2024-01-24 18:19:04 -08:00
parent a811decf84
commit 9a5ee49778
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
5 changed files with 28 additions and 8 deletions

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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