From 6f85c262cff99d31400bb731693e594f44f1ecd7 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 31 Mar 2024 17:09:24 -0700
Subject: [PATCH] feat: Instantiate mvars during echo

---
 Pantograph/Library.lean |  4 ++--
 Test/Library.lean       | 11 +++++++++--
 2 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index e2cf3f1..d36866a 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -116,7 +116,7 @@ def parseElabType (type: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) :=
     | .ok syn => pure syn
   match ← elabType syn with
   | .error str => return .error $ errorI "elab" str
-  | .ok expr => return .ok expr
+  | .ok expr => return .ok (← Lean.instantiateMVars expr)
 
 /-- This must be a TermElabM since the parsed expr contains extra information -/
 def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
@@ -130,7 +130,7 @@ def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.E
     | .ok syn => pure syn
   match ← elabTerm syn expectedType? with
   | .error str => return .error $ errorI "elab" str
-  | .ok expr => return .ok expr
+  | .ok expr => return .ok (← Lean.instantiateMVars expr)
 
 @[export pantograph_expr_echo_m]
 def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options):
diff --git a/Test/Library.lean b/Test/Library.lean
index 265335a..8c935ee 100644
--- a/Test/Library.lean
+++ b/Test/Library.lean
@@ -20,9 +20,16 @@ def test_expr_echo: IO LSpec.TestSeq := do
     let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
       type := { pp? := "?m.2" }, expr := { pp? := "?m.3" }
     }))
-    let echoResult ← exprEcho prop_and_proof (expectedType? := .some "Σ' p:Prop, p") (options := {})
+    let echoResult ← exprEcho prop_and_proof (expectedType? := .some "Σ' p:Prop, p") (options := { printExprAST := true })
     let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
-      type := { pp? := "(p : Prop) ×' p" }, expr := { pp? := "⟨∀ (x : Prop), x → x, fun x h => h⟩" }
+      type := {
+        pp? := "(p : Prop) ×' p",
+        sexp? := "((:c PSigma) (:sort 0) (:lambda p (:sort 0) 0))",
+      },
+      expr := {
+        pp? := "⟨∀ (x : Prop), x → x, fun x h => h⟩",
+        sexp? := "((:c PSigma.mk) (:sort 0) (:lambda p (:sort 0) 0) (:forall x (:sort 0) (:forall _ 0 1)) (:lambda x (:sort 0) (:lambda h 0 0)))",
+      }
     }))
     return tests
   runCoreMSeq env (options := #["pp.proofs.threshold=100"]) inner