From 2682ce5b7b5a7e494d166b20b17852e88bea448a Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 23 Jul 2024 11:57:12 -0700
Subject: [PATCH] refactor: Move condensed functions to condensed

---
 Pantograph/Condensed.lean | 58 +++++++++++++++++++++++++++++++++++++--
 Pantograph/Serial.lean    | 48 --------------------------------
 2 files changed, 56 insertions(+), 50 deletions(-)

diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
index ac41133..90fc050 100644
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@@ -1,9 +1,13 @@
 /- structures for FFI based interface -/
 import Lean
+import Pantograph.Goal
+import Pantograph.Expr
+import Pantograph.Protocol
 
 open Lean
 
-namespace Pantograph.Condensed
+namespace Pantograph
+namespace Condensed
 
 /-
 These two functions are for user defiend names. For internal names such as
@@ -58,5 +62,55 @@ def elabState (levelNames: Array Name): Elab.Term.State := {
     levelNames := levelNames.toList,
   }
 
+end Condensed
 
-end Pantograph.Condensed
+@[export pantograph_to_condensed_goal_m]
+def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
+  let options : Protocol.Options := {}
+  let ppAuxDecls       := options.printAuxDecls
+  let ppImplDetailHyps := options.printImplementationDetailHyps
+  let mvarDecl ← mvarId.getDecl
+  let lctx     := mvarDecl.lctx
+  let lctx     := lctx.sanitizeNames.run' { options := (← getOptions) }
+  Meta.withLCtx lctx mvarDecl.localInstances do
+    let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do
+      match localDecl with
+      | .cdecl _ fvarId userName type _ _ =>
+        let type ← instantiate type
+        return { fvarId, userName, type }
+      | .ldecl _ fvarId userName type value _ _ => do
+        let userName := userName.simpMacroScopes
+        let type ← instantiate type
+        let value ← instantiate value
+        return { fvarId, userName, type, value? := .some value }
+    let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
+      let skip := !ppAuxDecls && localDecl.isAuxDecl ||
+        !ppImplDetailHyps && localDecl.isImplementationDetail
+      if skip then
+        return acc
+      else
+        let var ← ppVar localDecl
+        return var::acc
+    return {
+        mvarId,
+        userName := mvarDecl.userName,
+        context := vars.reverse.toArray,
+        target := ← instantiate mvarDecl.type
+    }
+  where
+  instantiate := instantiateAll
+
+@[export pantograph_goal_state_to_condensed_m]
+protected def GoalState.toCondensed (state: GoalState):
+    CoreM (Array Condensed.Goal):= do
+  let metaM := do
+    let goals := state.goals.toArray
+    goals.mapM fun goal => do
+      match state.mctx.findDecl? goal with
+      | .some _ =>
+        let serializedGoal ← toCondensedGoal goal
+        pure serializedGoal
+      | .none => throwError s!"Metavariable does not exist in context {goal.name}"
+  metaM.run' (s := state.savedState.term.meta.meta)
+
+end Pantograph
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 2cdf3d6..87353e2 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -201,54 +201,6 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.
     dependentMVars?,
   }
 
-@[export pantograph_to_condensed_goal]
-def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
-  let options: Protocol.Options := {}
-  let ppAuxDecls       := options.printAuxDecls
-  let ppImplDetailHyps := options.printImplementationDetailHyps
-  let mvarDecl ← mvarId.getDecl
-  let lctx     := mvarDecl.lctx
-  let lctx     := lctx.sanitizeNames.run' { options := (← getOptions) }
-  Meta.withLCtx lctx mvarDecl.localInstances do
-    let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do
-      match localDecl with
-      | .cdecl _ fvarId userName type _ _ =>
-        let type ← instantiate type
-        return { fvarId, userName, type }
-      | .ldecl _ fvarId userName type value _ _ => do
-        let userName := userName.simpMacroScopes
-        let type ← instantiate type
-        let value ← instantiate value
-        return { fvarId, userName, type, value? := .some value }
-    let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
-      let skip := !ppAuxDecls && localDecl.isAuxDecl ||
-        !ppImplDetailHyps && localDecl.isImplementationDetail
-      if skip then
-        return acc
-      else
-        let var ← ppVar localDecl
-        return var::acc
-    return {
-        mvarId,
-        userName := mvarDecl.userName,
-        context := vars.reverse.toArray,
-        target := ← instantiate mvarDecl.type
-    }
-  where
-  instantiate := instantiateAll
-
-@[export pantograph_goal_state_to_condensed]
-protected def GoalState.toCondensed (state: GoalState):
-    CoreM (Array Condensed.Goal):= do
-  let metaM := do
-    let goals := state.goals.toArray
-    goals.mapM fun goal => do
-      match state.mctx.findDecl? goal with
-      | .some _ =>
-        let serializedGoal ← toCondensedGoal goal
-        pure serializedGoal
-      | .none => throwError s!"Metavariable does not exist in context {goal.name}"
-  metaM.run' (s := state.savedState.term.meta.meta)
 
 /-- Adapted from ppGoal -/
 def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)