From 01a23b338a66d255126cd3cfb85f429b136b7648 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 28 Mar 2024 18:56:42 -0700
Subject: [PATCH] feat: Unfold aux lemmas when printing root expr

---
 Pantograph/Library.lean           | 12 ++++++++++--
 Test/Common.lean                  |  3 +++
 Test/Environment.lean             |  3 ++-
 Test/Main.lean                    |  4 ++--
 Test/{Holes.lean => Metavar.lean} |  6 +++---
 Test/Serial.lean                  |  3 ++-
 6 files changed, 22 insertions(+), 9 deletions(-)
 rename Test/{Holes.lean => Metavar.lean} (98%)

diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 078ca0f..c40322a 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -165,13 +165,21 @@ def goalResume (target: GoalState) (goals: Array String): Except String GoalStat
 def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) :=
   runMetaM <| state.serializeGoals (parent := .none) options
 
+def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
+
+/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
+def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do
+  Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
+
 @[export pantograph_goal_print_m]
 def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := do
   let metaM := do
     state.restoreMetaM
     return {
-      root? := ← state.rootExpr?.mapM (λ expr => serialize_expression options expr),
-      parent? := ← state.parentExpr?.mapM (λ expr => serialize_expression options expr),
+      root? := ← state.rootExpr?.mapM (λ expr => do
+        serialize_expression options (← unfoldAuxLemmas expr)),
+      parent? := ← state.parentExpr?.mapM (λ expr => do
+        serialize_expression options (← unfoldAuxLemmas expr)),
     }
   runMetaM metaM
 
diff --git a/Test/Common.lean b/Test/Common.lean
index 7c5b6e5..2e7149d 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -1,8 +1,11 @@
 import Pantograph.Goal
 import Pantograph.Library
 import Pantograph.Protocol
+import Lean
 import LSpec
 
+open Lean
+
 namespace Pantograph
 
 namespace Protocol
diff --git a/Test/Environment.lean b/Test/Environment.lean
index 9e3bd70..ba99380 100644
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@@ -2,11 +2,12 @@ import LSpec
 import Pantograph.Serial
 import Pantograph.Environment
 import Test.Common
+import Lean
 
+open Lean
 namespace Pantograph.Test.Environment
 
 open Pantograph
-open Lean
 
 deriving instance DecidableEq, Repr for Protocol.InductInfo
 deriving instance DecidableEq, Repr for Protocol.ConstructorInfo
diff --git a/Test/Main.lean b/Test/Main.lean
index 4a8ab1f..d24f45f 100644
--- a/Test/Main.lean
+++ b/Test/Main.lean
@@ -1,6 +1,6 @@
 import LSpec
 import Test.Environment
-import Test.Holes
+import Test.Metavar
 import Test.Integration
 import Test.Proofs
 import Test.Serial
@@ -11,7 +11,7 @@ def main := do
   Lean.initSearchPath (← Lean.findSysroot)
 
   let suites := [
-    Holes.suite,
+    Metavar.suite,
     Integration.suite,
     Proofs.suite,
     Serial.suite,
diff --git a/Test/Holes.lean b/Test/Metavar.lean
similarity index 98%
rename from Test/Holes.lean
rename to Test/Metavar.lean
index af322e9..cbbfc81 100644
--- a/Test/Holes.lean
+++ b/Test/Metavar.lean
@@ -3,7 +3,7 @@ import Pantograph.Goal
 import Pantograph.Serial
 import Test.Common
 
-namespace Pantograph.Test.Holes
+namespace Pantograph.Test.Metavar
 open Pantograph
 open Lean
 
@@ -204,6 +204,6 @@ def suite: IO LSpec.TestSeq := do
     let tests ← proofRunner env tests
     return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
 
-  return LSpec.group "Holes" tests
+  return LSpec.group "Metavar" tests
 
-end Pantograph.Test.Holes
+end Pantograph.Test.Metavar
diff --git a/Test/Serial.lean b/Test/Serial.lean
index 490b538..c2810c8 100644
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@@ -1,11 +1,12 @@
 import LSpec
 import Pantograph.Serial
 import Test.Common
+import Lean
 
+open Lean
 namespace Pantograph.Test.Serial
 
 open Pantograph
-open Lean
 
 deriving instance Repr, DecidableEq for Protocol.BoundExpression