From efa956464d8fd3f6fd635090f70d701b0e078217 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 16 Jan 2024 16:44:54 -0800
Subject: [PATCH] test: Option controlled mvar instantiation

---
 Pantograph/Protocol.lean |  1 +
 Pantograph/Serial.lean   | 13 ++++++++-----
 2 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index c0204d0..8db30ad 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -219,6 +219,7 @@ structure GoalDiag where
   printNewMVars: Bool := false
   -- Print all mvars
   printAll: Bool := false
+  instantiate: Bool := true
 
 
 end Pantograph.Protocol
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 072872b..38d1f14 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -276,9 +276,6 @@ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag
   mctx.decls.forM (fun mvarId decl => do
     if goals.contains mvarId || mvarId == root then
       pure ()
-    -- Always print the root goal
-    else if mvarId == goalState.root then
-      printMVar (pref := ">") mvarId decl
     -- Print the remainig ones that users don't see in Lean
     else if options.printAll then
       let pref := if goalState.newMVars.contains mvarId then "~" else " "
@@ -291,11 +288,17 @@ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag
     printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do
       if options.printContext then
         decl.lctx.fvarIdToDecl.forM printFVar
-      let type_sexp ← serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false)
+      let type ← if options.instantiate
+        then instantiateMVars decl.type
+        else pure $ decl.type
+      let type_sexp ← serialize_expression_ast type (sanitize := false)
       IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
       if options.printValue then
         if let Option.some value := (← getMCtx).eAssignment.find? mvarId then
-          IO.println s!"  = {← Meta.ppExpr value}"
+          let value ← if options.instantiate
+            then instantiateMVars value
+            else pure $ value
+          IO.println s!" := {← Meta.ppExpr value}"
     printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM Unit := do
       IO.println s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
     userNameToString : Name → String