6 changed files with 36 additions and 34 deletions
--- a/Main.lean
+++ b/Main.lean
@ -102,12 +102,7 @@ unsafe def main (args: List String): IO Unit := do
    options := options
  }
  try
-    let termElabM := loop.run context |>.run' {}
-    let metaM := termElabM.run' (ctx := {
-      declName? := some "_pantograph",
-      errToSorry := false
-    })
-    let coreM := metaM.run'
+    let coreM := loop.run context |>.run' {}
    IO.println "ready."
    discard <| coreM.toIO coreContext { env := env }
  catch ex =>
--- a/Pantograph.lean
+++ b/Pantograph.lean
@ -16,11 +16,19 @@ structure State where
  goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty

 /-- Main state monad for executing commands -/
-abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM)
+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 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 :=
    match Lean.fromJson? command.payload with
@ -83,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,
@ -96,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 (← 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
@ -128,24 +136,23 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
  goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
    let state ← get
    let env ← Lean.MonadEnv.getEnv
-    let expr?: Except _ Lean.Expr ← (match args.expr, args.copyFrom with
+    let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
      | .some expr, .none =>
        (match syntax_from_str env expr with
        | .error str => return .error <| errorI "parsing" str
        | .ok syn => do
-          (match (← syntax_to_expr syn) with
+          (match ← syntax_to_expr syn with
          | .error str => return .error <| errorI "elab" str
-          | .ok expr => return .ok expr))
+          | .ok expr => return .ok (← GoalState.create expr)))
      | .none, .some copyFrom =>
        (match env.find? <| copyFrom.toName with
        | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
-        | .some cInfo => return .ok cInfo.type)
+        | .some cInfo => return .ok (← GoalState.create cInfo.type))
      | _, _ =>
        return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
    match expr? with
    | .error error => return .error error
-    | .ok expr =>
-      let goalState ← GoalState.create expr
+    | .ok goalState =>
      let stateId := state.nextId
      set { state with
        goalStates := state.goalStates.insert stateId goalState,
@ -159,9 +166,9 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
    | .some goalState => do
      let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
        | .some tactic, .none => do
-          pure ( Except.ok (← GoalState.execute goalState args.goalId tactic))
+          pure ( Except.ok (← runTermElabM <| GoalState.execute goalState args.goalId tactic))
        | .none, .some expr => do
-          pure ( Except.ok (← GoalState.tryAssign goalState args.goalId expr))
+          pure ( Except.ok (← runTermElabM <| GoalState.tryAssign goalState args.goalId expr))
        | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied")
      match nextGoalState? with
      | .error error => return .error error
@ -171,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,
@ -204,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,
@ -218,7 +225,8 @@ 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 {
        root?,
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@ -51,6 +51,10 @@ protected def GoalState.env (state: GoalState): Environment :=
  state.savedState.term.meta.core.env
 private def GoalState.mvars (state: GoalState): SSet MVarId :=
  state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
+private def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
+  state.savedState.term.restore
+def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
+  state.savedState.term.meta.restore

 /-- Inner function for executing tactic on goal state -/
 def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) :
@ -84,6 +88,7 @@ inductive TacticResult where
 /-- Execute tactic on given state -/
 protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String):
    M TacticResult := do
+  state.restoreElabM
  let goal ← match state.savedState.tactic.goals.get? goalId with
    | .some goal => pure $ goal
    | .none => return .indexError goalId
@ -118,6 +123,7 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String
    }

 protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do
+  state.restoreElabM
  let goal ← match state.savedState.tactic.goals.get? goalId with
    | .some goal => pure goal
    | .none => return .indexError goalId
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@ -26,6 +26,7 @@ def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
    (fileName := "<stdin>")


+/-- Parse a syntax object. May generate additional metavariables! -/
 def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do
  try
    let expr ← Elab.Term.elabType syn
@ -242,8 +243,8 @@ def serialize_goal (options: Protocol.Options) (goal: MVarId) (mvarDecl: Metavar
  of_name (n: Name) := name_to_ast n (sanitize := false)

 protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalState := .none) (options: Protocol.Options := {}): MetaM (Array Protocol.Goal):= do
+  state.restoreMetaM
  let goals := state.goals.toArray
-  state.savedState.term.meta.restore
  let parentDecl? := parent.bind (λ parentState =>
    let parentGoal := parentState.goals.get! state.parentGoalId
    parentState.mctx.findDecl? parentGoal)
@ -256,8 +257,8 @@ protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalSt

 /-- Print the metavariables in a readable format -/
 protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do
+  goalState.restoreMetaM
  let savedState := goalState.savedState
-  savedState.term.meta.restore
  let goals := savedState.tactic.goals
  let mctx ← getMCtx
  let root := goalState.root
--- a/Test/Catalog.lean
+++ b/Test/Catalog.lean
@ -10,8 +10,7 @@ open Lean
 def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do
  let entries: List (Name × Bool) := [
    ("Nat.add_comm".toName, false),
-    ("Lean.Name".toName, true),
-    ("_private.Init.0.Lean.Name".toName, true)
+    ("Lean.Name".toName, true)
  ]
  let suite := entries.foldl (λ suites (symbol, target) =>
    let constant := env.constants.find! symbol
@ -19,8 +18,6 @@ def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do
    LSpec.TestSeq.append suites test) LSpec.TestSeq.done
  return suite

-
-
 def suite: IO LSpec.TestSeq := do
  let env: Environment ← importModules
    (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@ -33,12 +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 termElabM := commands.run context |>.run' {}
-    let metaM := termElabM.run' (ctx := {
-      declName? := some "_pantograph",
-      errToSorry := false
-    })
-    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