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

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

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

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

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