From 0725d865de5dbe0195c6cafa8e81b42f9e967fc5 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 10 Dec 2024 12:40:00 -0800
Subject: [PATCH] feat: Print value of arbitrary mvar in goal state

---
 Pantograph/Library.lean  | 16 +++++++++++-----
 Pantograph/Protocol.lean |  4 ++++
 Repl.lean                |  3 ++-
 3 files changed, 17 insertions(+), 6 deletions(-)

diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 20c7c9b..ee17fa5 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -138,16 +138,22 @@ def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array
   runMetaM <| state.serializeGoals (parent := .none) options
 
 @[export pantograph_goal_print_m]
-def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult :=
+def goalPrint (state: GoalState) (extraMVars : Array String) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult :=
   runMetaM do
     state.restoreMetaM
     return {
-      root? := ← state.rootExpr?.mapM (λ expr =>
+      root? := ← state.rootExpr?.mapM λ expr =>
         state.withRootContext do
-          serializeExpression options (← instantiateAll expr)),
-      parent? := ← state.parentExpr?.mapM (λ expr =>
+          serializeExpression options (← instantiateAll expr),
+      parent? := ← state.parentExpr?.mapM λ expr =>
         state.withParentContext do
-          serializeExpression options (← instantiateAll expr)),
+          serializeExpression options (← instantiateAll expr),
+      extraMVars := ← extraMVars.mapM λ mvarId => do
+        let mvarId: MVarId := { name := mvarId.toName }
+        let .some _ ← mvarId.findDecl? | return {}
+        state.withContext mvarId do
+          let .some expr ← getExprMVarAssignment? mvarId | return {}
+          serializeExpression options (← instantiateAll expr),
     }
 
 @[export pantograph_goal_tactic_m]
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 0cb6cac..9b00dfe 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -271,12 +271,16 @@ structure GoalDeleteResult where
 
 structure GoalPrint where
   stateId: Nat
+  -- Print values of extra mvars
+  extraMVars?: Option (Array String) := .none
   deriving Lean.FromJson
 structure GoalPrintResult where
   -- The root expression
   root?: Option Expression := .none
   -- The filling expression of the parent goal
   parent?: Option Expression
+
+  extraMVars: Array Expression := #[]
   deriving Lean.ToJson
 
 -- Diagnostic Options, not available in REPL
diff --git a/Repl.lean b/Repl.lean
index 3f8a3c6..0dd92d2 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -222,7 +222,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let state ← get
     let .some goalState := state.goalStates[args.stateId]? |
       return .error $ errorIndex s!"Invalid state index {args.stateId}"
-    let result ← runMetaInMainM <| goalPrint goalState state.options
+    let extraMVars := args.extraMVars?.getD #[]
+    let result ← runMetaInMainM <| goalPrint goalState extraMVars state.options
     return .ok result
   goal_save (args: Protocol.GoalSave): MainM (CR Protocol.GoalSaveResult) := do
     let state ← get