From ab1b309c7267e6557ce319311f62c71e6d89bf70 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 12 Dec 2023 18:39:02 -0800
Subject: [PATCH] feat: Use CoreM as the main interaction monad

---
 Main.lean             |  3 +--
 Pantograph.lean       | 22 ++++++++++++----------
 Test/Integration.lean |  3 +--
 3 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/Main.lean b/Main.lean
index e833649..68d1a3e 100644
--- a/Main.lean
+++ b/Main.lean
@@ -102,8 +102,7 @@ unsafe def main (args: List String): IO Unit := do
     options := options
   }
   try
-    let metaM := loop.run context |>.run' {}
-    let coreM := metaM.run'
+    let coreM := loop.run context |>.run' {}
     IO.println "ready."
     discard <| coreM.toIO coreContext { env := env }
   catch ex =>
diff --git a/Pantograph.lean b/Pantograph.lean
index a5a181b..1e3dbe3 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -16,16 +16,18 @@ structure State where
   goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty
 
 /-- Main state monad for executing commands -/
-abbrev MainM := ReaderT Context (StateT State Lean.MetaM)
+abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
 -- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
 -- certain monadic features in `MainM`
 abbrev CR α := Except Protocol.InteractionError α
 
-def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
+def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α :=
+  metaM.run'
+def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α :=
   termElabM.run' (ctx := {
     declName? := .none,
     errToSorry := false,
-  })
+  }) |>.run'
 
 def execute (command: Protocol.Command): MainM Lean.Json := do
   let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
@@ -89,8 +91,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         | .none, .defnInfo _ => info.value?
         | .none, _ => .none
       return .ok {
-        type := ← serialize_expression state.options info.type,
-        value? := ← value?.mapM (λ v => serialize_expression state.options v),
+        type := ← (serialize_expression state.options info.type).run',
+        value? := ← value?.mapM (λ v => serialize_expression state.options v |>.run'),
         publicName? := Lean.privateToUserName? name |>.map (·.toString),
         -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
         typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none,
@@ -102,8 +104,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let env ← Lean.MonadEnv.getEnv
     match syntax_from_str env args.expr with
     | .error str => return .error $ errorI "parsing" str
-    | .ok syn => do
-      match ← runTermElabM <| syntax_to_expr syn with
+    | .ok syn => runTermElabM do
+      match ← syntax_to_expr syn with
       | .error str => return .error $ errorI "elab" str
       | .ok expr => do
         try
@@ -176,7 +178,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           goalStates := state.goalStates.insert state.nextId nextGoalState,
           nextId := state.nextId + 1,
         }
-        let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options)
+        let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
         return .ok {
           nextStateId? := .some nextStateId,
           goals? := .some goals,
@@ -209,7 +211,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           goalStates := state.goalStates.insert nextStateId nextGoalState,
           nextId := state.nextId + 1
         }
-        let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options)
+        let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options) |>.run'
         return .ok {
           nextStateId,
           goals,
@@ -223,7 +225,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let state ← get
     match state.goalStates.find? args.stateId with
     | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
-    | .some goalState => do
+    | .some goalState => runMetaM <| do
       goalState.restoreMetaM
       let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr)
       return .ok {
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 50ee740..5aad1e7 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -33,8 +33,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d
       let result ← step
       return suite ++ result) LSpec.TestSeq.done
   try
-    let metaM := commands.run context |>.run' {}
-    let coreM := metaM.run'
+    let coreM := commands.run context |>.run' {}
     return Prod.fst $ (← coreM.toIO coreContext { env := env })
   catch ex =>
     return LSpec.check s!"Uncaught IO exception: {ex.toString}" false