From edec0f5733207bba278701ce9a13ed127742bc5b Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 26 Aug 2024 13:42:14 -0400
Subject: [PATCH] feat: Use CoreM for diag monad

---
 Pantograph/Serial.lean | 48 ++++++++++++++++++++++--------------------
 1 file changed, 25 insertions(+), 23 deletions(-)

diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index c788be2..93dfb95 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -289,29 +289,31 @@ protected def GoalState.serializeGoals
 
 /-- Print the metavariables in a readable format -/
 @[export pantograph_goal_state_diag_m]
-protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): MetaM String := do
-  goalState.restoreMetaM
-  let savedState := goalState.savedState
-  let goals := savedState.tactic.goals
-  let mctx ← getMCtx
-  let root := goalState.root
-  -- Print the root
-  let result: String ← match mctx.decls.find? root with
-    | .some decl => printMVar ">" root decl
-    | .none => pure s!">{root.name}: ??"
-  let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId =>
-    match mctx.decls.find? mvarId with
-    | .some decl => printMVar "⊢" mvarId decl
-    | .none => pure s!"⊢{mvarId.name}: ??"
-  )
-  let goals := goals.toSSet
-  let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
-      !(goals.contains mvarId || mvarId == root) && options.printAll)
-      |>.mapM (fun (mvarId, decl) => do
-        let pref := if parentHasMVar mvarId then " " else "~"
-        printMVar pref mvarId decl
-      )
-  pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
+protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): CoreM String := do
+  let metaM: MetaM String := do
+    goalState.restoreMetaM
+    let savedState := goalState.savedState
+    let goals := savedState.tactic.goals
+    let mctx ← getMCtx
+    let root := goalState.root
+    -- Print the root
+    let result: String ← match mctx.decls.find? root with
+      | .some decl => printMVar ">" root decl
+      | .none => pure s!">{root.name}: ??"
+    let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId =>
+      match mctx.decls.find? mvarId with
+      | .some decl => printMVar "⊢" mvarId decl
+      | .none => pure s!"⊢{mvarId.name}: ??"
+    )
+    let goals := goals.toSSet
+    let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
+        !(goals.contains mvarId || mvarId == root) && options.printAll)
+        |>.mapM (fun (mvarId, decl) => do
+          let pref := if parentHasMVar mvarId then " " else "~"
+          printMVar pref mvarId decl
+        )
+    pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
+  metaM.run' {}
   where
     printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
       let resultFVars: List String ←