Pantograph/Library.lean

@@ -127,7 +127,7 @@ def exprEcho (expr: String) (options: @&Protocol.Options):
       | .error e => return .error e
       | .ok expr => pure expr
     try
-      let type ← Lean.Meta.inferType expr
+      let type ← instantiateAll (← Lean.Meta.inferType expr)
       return .ok {
           type := (← serialize_expression options type),
           expr := (← serialize_expression options expr)
@@ -171,9 +171,9 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto
     state.restoreMetaM
     return {
       root? := ← state.rootExpr?.mapM (λ expr => do
-        serialize_expression options (← unfoldAuxLemmas expr)),
+        serialize_expression options (← instantiateAll expr)),
       parent? := ← state.parentExpr?.mapM (λ expr => do
-        serialize_expression options (← unfoldAuxLemmas expr)),
+        serialize_expression options (← instantiateAll expr)),
     }
   runMetaM metaM
 

Pantograph/Serial.lean

@@ -18,6 +18,10 @@ namespace Pantograph
 def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do
   Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
 
+def instantiateAll (e: Lean.Expr) : Lean.MetaM Lean.Expr := do
+  let e ← unfoldAuxLemmas e
+  instantiateMVars (← Lean.Meta.whnf e)
+
 --- Input Functions ---
 
 /-- Read syntax object from string -/

Test/Metavar.lean

@@ -13,6 +13,27 @@ abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M)
 def addTest (test: LSpec.TestSeq): TestM Unit := do
   set $ (← get) ++ test
 
+-- Tests that all delay assigned mvars are instantiated
+def test_instantiate_mvar: TestM Unit := do
+  let env ← Lean.MonadEnv.getEnv
+  let value := "@Nat.le_trans 2 2 5 (@of_eq_true (@LE.le Nat instLENat 2 2) (@eq_true (@LE.le Nat instLENat 2 2) (@Nat.le_refl 2))) (@of_eq_true (@LE.le Nat instLENat 2 5) (@eq_true_of_decide (@LE.le Nat instLENat 2 5) (@Nat.decLe 2 5) (@Eq.refl Bool Bool.true)))"
+  let syn ← match syntax_from_str env value with
+    | .ok s => pure $ s
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let expr ← match ← syntax_to_expr syn with
+    | .ok expr => pure $ expr
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let t ← Lean.Meta.inferType expr
+  addTest $ LSpec.check "typing" ((toString (← serialize_expression_ast t)) =
+    "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))")
+  return ()
+
+
+
 def startProof (expr: String): TestM (Option GoalState) := do
   let env ← Lean.MonadEnv.getEnv
   let syn? := syntax_from_str env expr
@@ -140,8 +161,9 @@ def test_m_couple_simp: TestM Unit := do
       return ()
   let rootStr: String := toString (← Lean.Meta.ppExpr root)
   addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (Init.Data.Nat.Basic._auxLemma.4 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
-  let rootStr: String := toString (← Lean.Meta.ppExpr (← unfoldAuxLemmas root))
-  addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
+  let unfoldedRoot ←  unfoldAuxLemmas root
+  addTest $ LSpec.check "(5 root)" ((toString (← Lean.Meta.ppExpr unfoldedRoot)) =
+    "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
   return ()
 
 def test_proposition_generation: TestM Unit := do
@@ -252,6 +274,7 @@ def suite: IO LSpec.TestSeq := do
     (opts := {})
     (trustLevel := 1)
   let tests := [
+    ("Instantiate", test_instantiate_mvar),
     ("2 < 5", test_m_couple),
     ("2 < 5", test_m_couple_simp),
     ("Proposition Generation", test_proposition_generation),