From 5df3d2bee19b0ecb2db28ef8995077fbd663a82d Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 7 Apr 2025 20:17:58 -0700
Subject: [PATCH] refactor: Remove `runTermElabM` from library

---
 Pantograph/Library.lean | 28 +++++++++++-----------------
 Repl.lean               |  4 +++-
 Test/Library.lean       |  7 +++++--
 3 files changed, 19 insertions(+), 20 deletions(-)

diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index b62a63b..e26b4ff 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -41,8 +41,6 @@ namespace Pantograph
 
 def runMetaM { α } (metaM: MetaM α): CoreM α :=
   metaM.run'
-def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α :=
-  termElabM.run' (ctx := defaultElabContext) |>.run'
 
 def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
 
@@ -99,21 +97,17 @@ def parseElabExpr (expr: String) (expectedType?: Option String := .none): Protoc
   | .ok expr => return (← instantiateMVars expr)
 
 @[export pantograph_expr_echo_m]
-def exprEcho (expr: String) (expectedType?: Option String := .none) (levels: Array String := #[])  (options: @&Protocol.Options := {}):
-    Protocol.FallibleT CoreM Protocol.ExprEchoResult := do
-  let e : Except Protocol.InteractionError _ ← runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
-    let expr ← match ← parseElabExpr expr expectedType? |>.run with
-      | .error e => return Except.error e
-      | .ok expr => pure expr
-    try
-      let type ← unfoldAuxLemmas (← Meta.inferType expr)
-      return .ok $ .ok ({
-          type := (← serializeExpression options type),
-          expr := (← serializeExpression options expr),
-      }: Protocol.ExprEchoResult)
-    catch exception =>
-      return Except.error $ errorI "typing" (← exception.toMessageData.toString)
-  liftExcept e
+def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options := {}):
+    Protocol.FallibleT Elab.TermElabM Protocol.ExprEchoResult := do
+  let expr ← parseElabExpr expr expectedType?
+  try
+    let type ← unfoldAuxLemmas (← Meta.inferType expr)
+    return {
+        type := (← serializeExpression options type),
+        expr := (← serializeExpression options expr),
+    }
+  catch exception =>
+    Protocol.throw $ errorI "typing" (← exception.toMessageData.toString)
 
 @[export pantograph_goal_start_expr_m]
 def goalStartExpr (expr: String) : Protocol.FallibleT Elab.TermElabM GoalState := do
diff --git a/Repl.lean b/Repl.lean
index 1971431..bcbe8f9 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -247,7 +247,9 @@ def execute (command: Protocol.Command): MainM Json := do
     return {}
   expr_echo (args: Protocol.ExprEcho): EMainM Protocol.ExprEchoResult := do
     let state ← getMainState
-    runCoreM' $ exprEcho args.expr (expectedType? := args.type?) (levels := args.levels?.getD #[]) (options := state.options)
+    let levelNames := (args.levels?.getD #[]).toList.map (·.toName)
+    liftExcept $ ← liftTermElabM (levelNames := levelNames) do
+      (exprEcho args.expr (expectedType? := args.type?) (options := state.options)).run
   options_set (args: Protocol.OptionsSet): EMainM Protocol.OptionsSetResult := do
     let state ← getMainState
     let options := state.options
diff --git a/Test/Library.lean b/Test/Library.lean
index df1ba4d..8763672 100644
--- a/Test/Library.lean
+++ b/Test/Library.lean
@@ -8,15 +8,18 @@ open Pantograph
 
 namespace Pantograph.Test.Library
 
+def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α :=
+  termElabM.run' (ctx := defaultElabContext) |>.run'
+
 def test_expr_echo (env: Environment): IO LSpec.TestSeq := do
   let inner: CoreM LSpec.TestSeq := do
     let prop_and_proof := "⟨∀ (x: Prop), x → x, λ (x: Prop) (h: x) => h⟩"
     let tests := LSpec.TestSeq.done
-    let echoResult ← exprEcho prop_and_proof (options := {})
+    let echoResult ← runTermElabM $ exprEcho prop_and_proof (options := {})
     let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
       type := { pp? := "?m.2" }, expr := { pp? := "?m.3" }
     }))
-    let echoResult ← exprEcho prop_and_proof (expectedType? := .some "Σ' p:Prop, p") (options := { printExprAST := true })
+    let echoResult ← runTermElabM $ exprEcho prop_and_proof (expectedType? := .some "Σ' p:Prop, p") (options := { printExprAST := true })
     let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
       type := {
         pp? := "(p : Prop) ×' p",