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 := {}):
+def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options := {}):
-    Protocol.FallibleT CoreM Protocol.ExprEchoResult := do
+    Protocol.FallibleT Elab.TermElabM Protocol.ExprEchoResult := do
-  let e : Except Protocol.InteractionError _ ← runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
+  let expr ← parseElabExpr expr expectedType?
-    let expr ← match ← parseElabExpr expr expectedType? |>.run with
+  try
-      | .error e => return Except.error e
+    let type ← unfoldAuxLemmas (← Meta.inferType expr)
-      | .ok expr => pure expr
+    return {
-    try
+        type := (← serializeExpression options type),
-      let type ← unfoldAuxLemmas (← Meta.inferType expr)
+        expr := (← serializeExpression options expr),
-      return .ok $ .ok ({
+    }
-          type := (← serializeExpression options type),
+  catch exception =>
-          expr := (← serializeExpression options expr),
+    Protocol.throw $ errorI "typing" (← exception.toMessageData.toString)
-      }: Protocol.ExprEchoResult)
-    catch exception =>
-      return Except.error $ errorI "typing" (← exception.toMessageData.toString)
-  liftExcept e
 
 @[export pantograph_goal_start_expr_m]
 def goalStartExpr (expr: String) : Protocol.FallibleT Elab.TermElabM GoalState := do

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

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",