From bc09f4a29df6e32a1b016b6b563d58b9a26f2411 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 13 May 2024 13:58:50 -0700
Subject: [PATCH] refactor: Expr related functions to Expr.lean

---
 Pantograph/Expr.lean    | 52 +++++++++++++++++++++++++++++++++++++++++
 Pantograph/Library.lean |  4 ++++
 Pantograph/Serial.lean  | 43 +---------------------------------
 3 files changed, 57 insertions(+), 42 deletions(-)
 create mode 100644 Pantograph/Expr.lean

diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean
new file mode 100644
index 0000000..14d063e
--- /dev/null
+++ b/Pantograph/Expr.lean
@@ -0,0 +1,52 @@
+import Lean
+
+open Lean
+
+namespace Pantograph
+
+def _root_.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 : Expr) : CoreM Expr := do
+  Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
+
+def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do
+  Meta.transform e
+    (pre := fun e => e.withApp fun f args => do
+      if let .mvar mvarId := f then
+        if let some decl ← getDelayedMVarAssignment? mvarId then
+          if args.size ≥ decl.fvars.size then
+            let pending ← instantiateMVars (.mvar decl.mvarIdPending)
+            if !pending.isMVar then
+              return .visit <| (← Meta.mkLambdaFVars decl.fvars pending).beta args
+      return .continue)
+
+@[export pantograph_instantiate_all_meta_m]
+def instantiateAll (e: Expr): MetaM Expr := do
+  let e ← instantiateMVars e
+  let e ← unfoldAuxLemmas e
+  --let e ← instantiatePartialDelayedMVars e
+  return e
+
+structure DelayedMVarInvocation where
+  mvarIdPending: MVarId
+  args: Array (FVarId × Expr)
+  tail: Array Expr
+
+@[export pantograph_to_delayed_mvar_invocation_meta_m]
+def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do
+  let .mvar mvarId := e.getAppFn | return .none
+  let .some decl ← getDelayedMVarAssignment? mvarId | return .none
+  let mvarIdPending := decl.mvarIdPending
+  -- Print the function application e. See Lean's `withOverApp`
+  let args := e.getAppArgs
+
+  assert! args.size >= decl.fvars.size
+
+  return .some {
+    mvarIdPending,
+    args := decl.fvars.map (·.fvarId!) |>.zip args,
+    tail := args.toList.drop decl.fvars.size |>.toArray,
+  }
+
+end Pantograph
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 59d7adc..9c64b69 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -78,6 +78,10 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do
     (trustLevel := 1)
   return { env := env }
 
+@[export pantograph_create_meta_context]
+def createMetaContext: IO Lean.Meta.Context := do
+  return {}
+
 @[export pantograph_env_catalog_m]
 def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
   Environment.catalog ({}: Protocol.EnvCatalog)
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index a95180e..58d4ea7 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -2,6 +2,7 @@
 All serialisation functions
 -/
 import Lean
+import Pantograph.Expr
 
 import Pantograph.Protocol
 import Pantograph.Goal
@@ -10,30 +11,8 @@ open Lean
 
 -- Symbol processing functions --
 
-def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
-
 namespace Pantograph
 
-/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
-def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
-  Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
-
-def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do
-  Meta.transform e
-    (pre := fun e => e.withApp fun f args => do
-      if let .mvar mvarId := f then
-        if let some decl ← getDelayedMVarAssignment? mvarId then
-          if args.size ≥ decl.fvars.size then
-            let pending ← instantiateMVars (.mvar decl.mvarIdPending)
-            if !pending.isMVar then
-              return .visit <| (← Meta.mkLambdaFVars decl.fvars pending).beta args
-      return .continue)
-
-def instantiateAll (e: Expr): MetaM Expr := do
-  let e ← instantiateMVars e
-  let e ← unfoldAuxLemmas e
-  --let e ← instantiatePartialDelayedMVars e
-  return e
 
 --- Input Functions ---
 
@@ -101,26 +80,6 @@ partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
   | _, .zero => s!"{k}"
   | _, _ => s!"(+ {u_str} {k})"
 
-structure DelayedMVarInvocation where
-  mvarIdPending: MVarId
-  args: Array (FVarId × Expr)
-  tail: Array Expr
-
-def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do
-  let .mvar mvarId := e.getAppFn | return .none
-  let .some decl ← getDelayedMVarAssignment? mvarId | return .none
-  let mvarIdPending := decl.mvarIdPending
-  -- Print the function application e. See Lean's `withOverApp`
-  let args := e.getAppArgs
-
-  assert! args.size >= decl.fvars.size
-
-  return .some {
-    mvarIdPending,
-    args := decl.fvars.map (·.fvarId!) |>.zip args,
-    tail := args.toList.drop decl.fvars.size |>.toArray,
-  }
-
 
 /--
  Completely serializes an expression tree. Json not used due to compactness