Merge pull request 'feat: Update `CoreM` options from parsed header' (#177) from frontend/env-init into dev

Reviewed-on: #177

Main.lean

@@ -43,7 +43,7 @@ partial def loop : MainM Unit := do repeat do
         | false => ret.compress
       IO.println str
     catch e =>
-      let message ← e.toMessageData.toString
+      let message := e.toString
       let error  := Lean.toJson ({ error := "main", desc := message }: InteractionError)
       IO.println error.compress
 
@@ -60,11 +60,10 @@ unsafe def main (args: List String): IO Unit := do
   let (options, imports) := args.partition (·.startsWith "--")
   let coreContext ← options.map (·.drop 2) |>.toArray |> Pantograph.createCoreContext
   let coreState ← Pantograph.createCoreState imports.toArray
-  let context: Context := {}
   try
-    let coreM := loop.run context |>.run' {}
+    let mainM := loop.run { coreContext } |>.run' { env := coreState.env }
     IO.println "ready."
-    discard <| coreM.toIO coreContext coreState
+    mainM
   catch ex =>
     let message := ex.toString
     let error  := Lean.toJson ({ error := "io", desc := message }: InteractionError)

Pantograph/Goal.lean

@@ -85,12 +85,19 @@ protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n]
 
 private def GoalState.mvars (state: GoalState): SSet MVarId :=
   state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
-protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
+-- Restore the name generator and macro scopes of the core state
+protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit := do
+  let savedCore := state.coreState
+  modifyGetThe Core.State (fun st => ((),
+    { st with nextMacroScope := savedCore.nextMacroScope, ngen := savedCore.ngen }))
+protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit := do
+  state.restoreCoreMExtra
   state.savedState.term.meta.restore
-protected def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
+protected def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit := do
+  state.restoreCoreMExtra
   state.savedState.term.restore
 private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do
-  state.savedState.restore
+  state.restoreElabM
   Elab.Tactic.setGoals [goal]
 
 @[export pantograph_goal_state_focus]
@@ -215,7 +222,7 @@ protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Ta
   goal.checkNotAssigned `GoalState.step
   let (_, { goals }) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
   let nextElabState ← MonadBacktrack.saveState
-  Elab.Term.synthesizeSyntheticMVarsNoPostponing
+  --Elab.Term.synthesizeSyntheticMVarsNoPostponing
 
   let goals ← if guardMVarErrors then
       pure $ mergeMVarLists goals (← collectAllErroredMVars goal)
@@ -280,6 +287,7 @@ protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: Str
     (fileName := ← getFileName) with
     | .ok stx => pure $ stx
     | .error error => return .parseError error
+  assert! ¬ (← goal.isAssigned)
   state.tryTacticM goal (Elab.Tactic.evalTactic tactic) true
 
 protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String):

Pantograph/Protocol.lean

@@ -103,7 +103,7 @@ structure StatResult where
 -- Return the type of an expression
 structure ExprEcho where
   expr: String
-  type?: Option String
+  type?: Option String := .none
   -- universe levels
   levels: Option (Array String) := .none
   deriving Lean.FromJson
@@ -217,14 +217,14 @@ structure EnvSaveLoadResult where
 
 /-- Set options; See `Options` struct above for meanings -/
 structure OptionsSet where
-  printJsonPretty?: Option Bool
+  printJsonPretty?: Option Bool := .none
-  printExprPretty?: Option Bool
+  printExprPretty?: Option Bool := .none
-  printExprAST?: Option Bool
+  printExprAST?: Option Bool := .none
-  printDependentMVars?: Option Bool
+  printDependentMVars?: Option Bool := .none
-  noRepeat?: Option Bool
+  noRepeat?: Option Bool := .none
-  printAuxDecls?: Option Bool
+  printAuxDecls?: Option Bool := .none
-  printImplementationDetailHyps?: Option Bool
+  printImplementationDetailHyps?: Option Bool := .none
-  automaticMode?: Option Bool
+  automaticMode?: Option Bool := .none
   deriving Lean.FromJson
 structure OptionsSetResult where
   deriving Lean.ToJson
@@ -236,7 +236,7 @@ structure GoalStart where
   expr: Option String     -- Directly parse in an expression
   -- universe levels
   levels: Option (Array String) := .none
-  copyFrom: Option String -- Copy the type from a theorem in the environment
+  copyFrom: Option String := .none -- Copy the type from a theorem in the environment
   deriving Lean.FromJson
 structure GoalStartResult where
   stateId: Nat := 0

Repl.lean

@@ -6,18 +6,28 @@ namespace Pantograph.Repl
 open Lean
 
 structure Context where
+  coreContext : Core.Context
 
 /-- Stores state of the REPL -/
 structure State where
-  options: Protocol.Options := {}
+  options : Protocol.Options := {}
-  nextId: Nat := 0
+  nextId : Nat := 0
-  goalStates: Std.HashMap Nat GoalState := Std.HashMap.empty
+  goalStates : Std.HashMap Nat GoalState := Std.HashMap.empty
+
+  env : Environment
+  -- Parser state
+  scope : Elab.Command.Scope := { header := "" }
 
 /-- Main state monad for executing commands -/
-abbrev MainM := ReaderT Context $ StateRefT State CoreM
+abbrev MainM := ReaderT Context $ StateRefT State IO
+def getMainState : MainM State := get
 /-- Fallible subroutine return type -/
 abbrev CR α := Except Protocol.InteractionError α
 
+instance : MonadEnv MainM where
+  getEnv := return (← get).env
+  modifyEnv f := modify fun s => { s with env := f s.env  }
+
 def newGoalState (goalState: GoalState) : MainM Nat := do
   let state ← get
   let stateId := state.nextId
@@ -27,11 +37,25 @@ def newGoalState (goalState: GoalState) : MainM Nat := do
   }
   return stateId
 
+def runCoreM { α } (coreM : CoreM α) : MainM α := do
+  let scope := (← get).scope
+  let coreCtx : Core.Context := {
+    (← read).coreContext with
+    currNamespace      := scope.currNamespace
+    openDecls          := scope.openDecls
+    options            := scope.opts
+  }
+  let coreState : Core.State := {
+    env := (← get).env
+  }
+  let (result, state') ← coreM.toIO coreCtx coreState
+  modifyEnv λ _ => state'.env
+  return result
 
-def runMetaInMainM { α } (metaM: MetaM α): MainM α :=
+def liftMetaM { α } (metaM : MetaM α): MainM α :=
-  metaM.run'
+  runCoreM metaM.run'
-def runTermElabInMainM { α } (termElabM: Elab.TermElabM α) : MainM α :=
+def liftTermElabM { α } (termElabM: Elab.TermElabM α) : MainM α :=
-  termElabM.run' (ctx := defaultElabContext) |>.run'
+  runCoreM $ termElabM.run' (ctx := defaultElabContext) |>.run'
 
 section Frontend
 
@@ -45,7 +69,7 @@ structure CompilationUnit where
   newConstants : List Name
 
 def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
-  let options := (← get).options
+  let options := (← getMainState).options
   let (fileName, file) ← match args.fileName?, args.file? with
     | .some fileName, .none => do
       let file ← IO.FS.readFile fileName
@@ -85,6 +109,9 @@ def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.
   let (li, state') ← frontendM.run context |>.run state
   if args.inheritEnv then
     setEnv state'.commandState.env
+    if let .some scope := state'.commandState.scopes.head? then
+      -- modify the scope
+      set { ← getMainState with scope }
   let units ← li.mapM λ step => withEnv step.env do
     let newConstants? := if args.newConstants then
         .some $ step.newConstants.toArray.map λ name => name.toString
@@ -93,9 +120,11 @@ def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.
     let (goalStateId?, goals?, goalSrcBoundaries?) ← if step.sorrys.isEmpty then do
         pure (.none, .none, .none)
       else do
-        let { state, srcBoundaries } ← runMetaInMainM $ Frontend.sorrysToGoalState step.sorrys
+        let ({ state, srcBoundaries }, goals) ← liftMetaM do
+          let result@{state, .. } ← Frontend.sorrysToGoalState step.sorrys
+          let goals ← goalSerialize state options
+          pure (result, goals)
         let stateId ← newGoalState state
-        let goals ← goalSerialize state options
         let srcBoundaries := srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx))
         pure (.some stateId, .some goals, .some srcBoundaries)
     let invocations? := if args.invocations then .some step.invocations else .none
@@ -121,63 +150,58 @@ def execute (command: Protocol.Command): MainM Json := do
       | .ok result =>  return toJson result
       | .error ierror => return toJson ierror
     | .error error => return toJson $ errorCommand s!"Unable to parse json: {error}"
-  try
+  match command.cmd with
-    match command.cmd with
+  | "reset"         => run reset
-    | "reset"         => run reset
+  | "stat"          => run stat
-    | "stat"          => run stat
+  | "expr.echo"     => run expr_echo
-    | "expr.echo"     => run expr_echo
+  | "env.describe"  => run env_describe
-    | "env.describe"  => run env_describe
+  | "env.module_read" => run env_module_read
-    | "env.module_read" => run env_module_read
+  | "env.catalog"   => run env_catalog
-    | "env.catalog"   => run env_catalog
+  | "env.inspect"   => run env_inspect
-    | "env.inspect"   => run env_inspect
+  | "env.add"       => run env_add
-    | "env.add"       => run env_add
+  | "env.save"      => run env_save
-    | "env.save"      => run env_save
+  | "env.load"      => run env_load
-    | "env.load"      => run env_load
+  | "options.set"   => run options_set
-    | "options.set"   => run options_set
+  | "options.print" => run options_print
-    | "options.print" => run options_print
+  | "goal.start"    => run goal_start
-    | "goal.start"    => run goal_start
+  | "goal.tactic"   => run goal_tactic
-    | "goal.tactic"   => run goal_tactic
+  | "goal.continue" => run goal_continue
-    | "goal.continue" => run goal_continue
+  | "goal.delete"   => run goal_delete
-    | "goal.delete"   => run goal_delete
+  | "goal.print"    => run goal_print
-    | "goal.print"    => run goal_print
+  | "goal.save"     => run goal_save
-    | "goal.save"     => run goal_save
+  | "goal.load"     => run goal_load
-    | "goal.load"     => run goal_load
+  | "frontend.process" => run frontend_process
-    | "frontend.process" => run frontend_process
+  | cmd =>
-    | cmd =>
+    let error: Protocol.InteractionError :=
-      let error: Protocol.InteractionError :=
+      errorCommand s!"Unknown command {cmd}"
-        errorCommand s!"Unknown command {cmd}"
+    return toJson error
-      return toJson error
-  catch ex => do
-    let error ← ex.toMessageData.toString
-    return toJson $ errorIO error
   where
   errorCommand := errorI "command"
   errorIndex := errorI "index"
   errorIO := errorI "io"
   -- Command Functions
   reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
-    let state ← get
+    let state ← getMainState
     let nGoals := state.goalStates.size
     set { state with nextId := 0, goalStates := .empty }
-    Core.resetMessageLog
     return .ok { nGoals }
   stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
-    let state ← get
+    let state ← getMainState
     let nGoals := state.goalStates.size
     return .ok { nGoals }
   env_describe (args: Protocol.EnvDescribe): MainM (CR Protocol.EnvDescribeResult) := do
-    let result ← Environment.describe args
+    let result ← runCoreM $ Environment.describe args
     return .ok result
   env_module_read (args: Protocol.EnvModuleRead): MainM (CR Protocol.EnvModuleReadResult) := do
-    Environment.moduleRead args
+    runCoreM $ Environment.moduleRead args
   env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
-    let result ← Environment.catalog args
+    let result ← runCoreM $ Environment.catalog args
     return .ok result
   env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do
-    let state ← get
+    let state ← getMainState
-    Environment.inspect args state.options
+    runCoreM $ Environment.inspect args state.options
   env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
-    Environment.addDecl args
+    runCoreM $ Environment.addDecl args
   env_save (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
     let env ← MonadEnv.getEnv
     environmentPickle env args.path
@@ -187,10 +211,10 @@ def execute (command: Protocol.Command): MainM Json := do
     setEnv env
     return .ok {}
   expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
-    let state ← get
+    let state ← getMainState
-    exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
+    runCoreM $ exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
   options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
-    let state ← get
+    let state ← getMainState
     let options := state.options
     set { state with
       options := {
@@ -207,13 +231,12 @@ def execute (command: Protocol.Command): MainM Json := do
     }
     return .ok {  }
   options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do
-    return .ok (← get).options
+    return .ok (← getMainState).options
   goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
-    let env ← MonadEnv.getEnv
+    let expr?: Except _ GoalState ← liftTermElabM (match args.expr, args.copyFrom with
-    let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with
       | .some expr, .none => goalStartExpr expr (args.levels.getD #[])
-      | .none, .some copyFrom =>
+      | .none, .some copyFrom => do
-        (match env.find? <| copyFrom.toName with
+        (match (← getEnv).find? <| copyFrom.toName with
         | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
         | .some cInfo => return .ok (← GoalState.create cInfo.type))
       | _, _ =>
@@ -224,12 +247,12 @@ def execute (command: Protocol.Command): MainM Json := do
       let stateId ← newGoalState goalState
       return .ok { stateId, root := goalState.root.name.toString }
   goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
-    let state ← get
+    let state ← getMainState
     let .some goalState := state.goalStates[args.stateId]? |
       return .error $ errorIndex s!"Invalid state index {args.stateId}"
     let .some goal := goalState.goals.get? args.goalId |
       return .error $ errorIndex s!"Invalid goal index {args.goalId}"
-    let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do
+    let nextGoalState?: Except _ TacticResult ← liftTermElabM do
       -- NOTE: Should probably use a macro to handle this...
       match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv?, args.draft?  with
       | .some tactic, .none, .none, .none, .none, .none, .none => do
@@ -251,26 +274,26 @@ def execute (command: Protocol.Command): MainM Json := do
       | .none, .none, .none, .none, .none, .none, .some draft => do
         pure <| Except.ok <| ← goalState.tryDraft goal draft
       | _, _, _, _, _, _, _ =>
-        let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied"
+        let error := errorI "arguments" "Exactly one of {tactic, expr, have, let, calc, conv, draft} must be supplied"
-        pure $ Except.error $ error
+        pure $ .error error
     match nextGoalState? with
     | .error error => return .error error
     | .ok (.success nextGoalState) => do
       let nextGoalState ← match state.options.automaticMode, args.conv? with
         | true, .none => do
           let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) |
-            throwError "Resuming known goals"
+            return .error $ errorIO "Resuming known goals"
           pure result
         | true, .some true => pure nextGoalState
         | true, .some false => do
           let .some (_, _, dormantGoals) := goalState.convMVar? |
-            throwError "If conv exit succeeded this should not fail"
+            return .error $ errorIO "If conv exit succeeded this should not fail"
           let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) |
-            throwError "Resuming known goals"
+            return .error $ errorIO "Resuming known goals"
           pure result
         | false, _ => pure nextGoalState
       let nextStateId ← newGoalState nextGoalState
-      let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
+      let goals ← runCoreM $ nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
       return .ok {
         nextStateId? := .some nextStateId,
         goals? := .some goals,
@@ -282,7 +305,7 @@ def execute (command: Protocol.Command): MainM Json := do
     | .ok (.failure messages) =>
       return .ok { tacticErrors? := .some messages }
   goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
-    let state ← get
+    let state ← getMainState
     let .some target := state.goalStates[args.target]? |
       return .error $ errorIndex s!"Invalid state index {args.target}"
     let nextState? ← match args.branch?, args.goals? with
@@ -297,21 +320,21 @@ def execute (command: Protocol.Command): MainM Json := do
     | .error error => return .error <| errorI "structure" error
     | .ok nextGoalState =>
       let nextStateId ← newGoalState nextGoalState
-      let goals ← goalSerialize nextGoalState (options := state.options)
+      let goals ← liftMetaM $ goalSerialize nextGoalState (options := state.options)
       return .ok {
         nextStateId,
         goals,
       }
   goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
-    let state ← get
+    let state ← getMainState
     let goalStates := args.stateIds.foldl (λ map id => map.erase id) state.goalStates
     set { state with goalStates }
     return .ok {}
   goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
-    let state ← get
+    let state ← getMainState
     let .some goalState := state.goalStates[args.stateId]? |
       return .error $ errorIndex s!"Invalid state index {args.stateId}"
-    let result ← runMetaInMainM <| goalPrint
+    let result ← liftMetaM <| goalPrint
         goalState
         (rootExpr := args.rootExpr?.getD False)
         (parentExpr := args.parentExpr?.getD False)
@@ -320,7 +343,7 @@ def execute (command: Protocol.Command): MainM Json := do
         (options := state.options)
     return .ok result
   goal_save (args: Protocol.GoalSave): MainM (CR Protocol.GoalSaveResult) := do
-    let state ← get
+    let state ← getMainState
     let .some goalState := state.goalStates[args.id]? |
       return .error $ errorIndex s!"Invalid state index {args.id}"
     goalStatePickle goalState args.path
@@ -333,6 +356,6 @@ def execute (command: Protocol.Command): MainM Json := do
     try
       frontend_process_inner args
     catch e =>
-      return .error $ errorI "frontend" (← e.toMessageData.toString)
+      return .error $ errorI "frontend" e.toString
 
 end Pantograph.Repl

Test/Integration.lean

@@ -8,23 +8,33 @@ import Test.Common
 namespace Pantograph.Test.Integration
 open Pantograph.Repl
 
-def step { α } [Lean.ToJson α] (cmd: String) (payload: List (String × Lean.Json))
+deriving instance Lean.ToJson for Protocol.EnvInspect
-    (expected: α) (name? : Option String := .none): MainM LSpec.TestSeq := do
+deriving instance Lean.ToJson for Protocol.EnvAdd
-  let payload := Lean.Json.mkObj payload
+deriving instance Lean.ToJson for Protocol.ExprEcho
+deriving instance Lean.ToJson for Protocol.OptionsSet
+deriving instance Lean.ToJson for Protocol.OptionsPrint
+deriving instance Lean.ToJson for Protocol.GoalStart
+deriving instance Lean.ToJson for Protocol.GoalPrint
+deriving instance Lean.ToJson for Protocol.GoalTactic
+deriving instance Lean.ToJson for Protocol.FrontendProcess
+
+def step { α β } [Lean.ToJson α] [Lean.ToJson β] (cmd: String) (payload: α)
+    (expected: β) (name? : Option String := .none): MainM LSpec.TestSeq := do
+  let payload := Lean.toJson payload
   let name := name?.getD s!"{cmd} {payload.compress}"
   let result ← Repl.execute { cmd, payload }
-  return LSpec.test name (toString result = toString (Lean.toJson expected))
+  return LSpec.test name (result.pretty = (Lean.toJson expected).pretty)
 
 abbrev Test := List (MainM LSpec.TestSeq)
 
-def test_elab : Test :=
+def test_expr_echo : Test :=
   [
     step "expr.echo"
-      [("expr", .str "λ {α : Sort (u + 1)} => List α"), ("levels", .arr #["u"])]
+     ({ expr := "λ {α : Sort (u + 1)} => List α", levels := .some #["u"]}: Protocol.ExprEcho)
-     (Lean.toJson ({
+     ({
        type := { pp? := .some "{α : Type u} → Type u" },
        expr := { pp? := .some "fun {α} => List α" }
-     }: Protocol.ExprEchoResult)),
+     }: Protocol.ExprEchoResult),
   ]
 
 def test_option_modify : Test :=
@@ -33,49 +43,53 @@ def test_option_modify : Test :=
   let module? := Option.some "Init.Data.Nat.Basic"
   let options: Protocol.Options := {}
   [
-    step "env.inspect" [("name", .str "Nat.add_one")]
+    step "env.inspect" ({ name := "Nat.add_one" } : Protocol.EnvInspect)
      ({ type := { pp? }, module? }: Protocol.EnvInspectResult),
-    step "options.set" [("printExprAST", .bool true)]
+    step "options.set" ({ printExprAST? := .some true } : Protocol.OptionsSet)
      ({ }: Protocol.OptionsSetResult),
-    step "env.inspect" [("name", .str "Nat.add_one")]
+    step "env.inspect" ({ name := "Nat.add_one" } : Protocol.EnvInspect)
      ({ type := { pp?, sexp? }, module? }: Protocol.EnvInspectResult),
-    step "options.print" []
+    step "options.print" ({} : Protocol.OptionsPrint)
      ({ options with printExprAST := true }: Protocol.Options),
   ]
 def test_malformed_command : Test :=
   let invalid := "invalid"
   [
-    step invalid [("name", .str "Nat.add_one")]
+    step invalid ({ name := "Nat.add_one" }: Protocol.EnvInspect)
      ({ error := "command", desc := s!"Unknown command {invalid}" }: Protocol.InteractionError)
      (name? := .some "Invalid Command"),
-    step "expr.echo" [(invalid, .str "Random garbage data")]
+    step "expr.echo" (Lean.Json.mkObj [(invalid, .str "Random garbage data")])
      ({ error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected" }:
       Protocol.InteractionError)
     (name? := .some "JSON Deserialization")
   ]
 def test_tactic : Test :=
+  let varX := { name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }}
   let goal1: Protocol.Goal := {
     name := "_uniq.11",
     target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
-    vars := #[{ name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }}],
+    vars := #[varX],
   }
   let goal2: Protocol.Goal := {
-    name := "_uniq.17",
+    name := "_uniq.14",
     target := { pp? := .some "x ∨ y → y ∨ x" },
     vars := #[
-      { name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }},
+      varX,
-      { name := "_uniq.16", userName := "y", type? := .some { pp? := .some "Prop" }}
+      { name := "_uniq.13", userName := "y", type? := .some { pp? := .some "Prop" }}
     ],
   }
   [
-    step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
+    step "goal.start" ({ expr := "∀ (p q: Prop), p ∨ q → q ∨ p" }: Protocol.GoalStart)
      ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
-    step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
+    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro x" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
-    step "goal.print" [("stateId", .num 1), ("parentExpr", .bool true), ("rootExpr", .bool true)]
+    step "goal.print" ({ stateId := 1, parentExpr? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
      ({ parent? := .some { pp? := .some "fun x => ?m.11" }, }: Protocol.GoalPrintResult),
-    step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
+    step "goal.tactic" ({ stateId := 1, tactic? := .some "intro y" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
+    step "goal.tactic" ({ stateId := 1, tactic? := .some "apply Nat.le_of_succ_le" }: Protocol.GoalTactic)
+     ({ tacticErrors? := .some #["tactic 'apply' failed, failed to unify\n  ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith\n  ∀ (q : Prop), x ∨ q → q ∨ x\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }:
+      Protocol.GoalTacticResult)
   ]
 def test_automatic_mode (automatic: Bool): Test :=
   let varsPQ := #[
@@ -114,16 +128,16 @@ def test_automatic_mode (automatic: Bool): Test :=
     ],
   }
   [
-    step "options.set" [("automaticMode", .bool automatic)]
+    step "options.set" ({automaticMode? := .some automatic}: Protocol.OptionsSet)
      ({}: Protocol.OptionsSetResult),
-    step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
+    step "goal.start" ({ expr := "∀ (p q: Prop), p ∨ q → q ∨ p"} : Protocol.GoalStart)
      ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
-    step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro p q h")]
+    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro p q h" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
-    step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "cases h")]
+    step "goal.tactic" ({ stateId := 1, tactic? := .some "cases h" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 2, goals? := #[goal2l, goal2r], }: Protocol.GoalTacticResult),
     let goals? := if automatic then #[goal3l, goal2r] else #[goal3l]
-    step "goal.tactic" [("stateId", .num 2), ("goalId", .num 0), ("tactic", .str "apply Or.inr")]
+    step "goal.tactic" ({ stateId := 2, tactic? := .some "apply Or.inr" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 3, goals?, }: Protocol.GoalTacticResult),
   ]
 
@@ -132,28 +146,28 @@ def test_env_add_inspect : Test :=
   let name2 := "Pantograph.mystery2"
   [
     step "env.add"
-      [
+      ({
-        ("name", .str name1),
+        name := name1,
-        ("type", .str "Prop → Prop → Prop"),
+        type := "Prop → Prop → Prop",
-        ("value", .str "λ (a b: Prop) => Or a b"),
+        value := "λ (a b: Prop) => Or a b",
-        ("isTheorem", .bool false)
+        isTheorem := false
-      ]
+      }: Protocol.EnvAdd)
      ({}: Protocol.EnvAddResult),
-    step "env.inspect" [("name", .str name1)]
+    step "env.inspect" ({name := name1, value? := .some true} : Protocol.EnvInspect)
      ({
        value? := .some { pp? := .some "fun a b => a ∨ b" },
        type := { pp? := .some "Prop → Prop → Prop" },
      }:
       Protocol.EnvInspectResult),
     step "env.add"
-      [
+      ({
-        ("name", .str name2),
+        name := name2,
-        ("type", .str "Nat → Int"),
+        type := "Nat → Int",
-        ("value", .str "λ (a: Nat) => a + 1"),
+        value := "λ (a: Nat) => a + 1",
-        ("isTheorem", .bool false)
+        isTheorem := false
-      ]
+      }: Protocol.EnvAdd)
      ({}: Protocol.EnvAddResult),
-    step "env.inspect" [("name", .str name2)]
+    step "env.inspect" ({name := name2, value? := .some true} : Protocol.EnvInspect)
      ({
        value? := .some { pp? := .some "fun a => ↑a + 1" },
        type := { pp? := .some "Nat → Int" },
@@ -166,19 +180,14 @@ example : ∀ (p: Prop), p → p := by
   exact h
 
 def test_frontend_process : Test :=
+  let file := "example : ∀ (p q: Prop), p → p ∨ q := by\n  intro p q h\n  exact Or.inl h"
+  let goal1 := "p q : Prop\nh : p\n⊢ p ∨ q"
   [
-    let file := "example : ∀ (p q: Prop), p → p ∨ q := by\n  intro p q h\n  exact Or.inl h"
-    let goal1 := "p q : Prop\nh : p\n⊢ p ∨ q"
     step "frontend.process"
-      [
+      ({
-        ("file",              .str file),
+        file? := .some file,
-        ("invocations",       .bool true),
+        invocations := true,
-        ("readHeader",        .bool false),
+      }: Protocol.FrontendProcess)
-        ("inheritEnv",        .bool false),
-        ("sorrys",            .bool false),
-        ("typeErrorsAsGoals", .bool false),
-        ("newConstants",      .bool false),
-      ]
      ({
        units := [{
          boundary := (0, file.utf8ByteSize),
@@ -214,15 +223,10 @@ def test_frontend_process_sorry : Test :=
       vars := #[{ name := "_uniq.4", userName := "p", type? := .some { pp? := .some "Prop" }}],
     }
     step "frontend.process"
-      [
+      ({
-        ("file", .str file),
+        file? := .some file,
-        ("readHeader",        .bool false),
+        sorrys := true,
-        ("inheritEnv",        .bool false),
+      }: Protocol.FrontendProcess)
-        ("invocations", .bool false),
-        ("sorrys", .bool true),
-        ("typeErrorsAsGoals", .bool false),
-        ("newConstants", .bool false),
-      ]
      ({
        units := [{
          boundary := (0, solved.utf8ByteSize),
@@ -233,23 +237,46 @@ def test_frontend_process_sorry : Test :=
          goalSrcBoundaries? := .some #[(57, 62)],
          messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
        }],
-    }: Protocol.FrontendProcessResult),
+     }: Protocol.FrontendProcessResult),
   ]
 
+def test_import_open : Test :=
+  let header := "import Init\nopen Nat"
+  let goal1: Protocol.Goal := {
+    name := "_uniq.67",
+    target := { pp? := .some "n + 1 = n.succ" },
+    vars := #[{ name := "_uniq.66", userName := "n", type? := .some { pp? := .some "Nat" }}],
+  }
+  [
+    step "frontend.process"
+      ({
+        file? := .some header,
+        readHeader := true,
+        inheritEnv := true,
+      }: Protocol.FrontendProcess)
+     ({
+       units := [{
+         boundary := (12, header.utf8ByteSize),
+       }],
+     }: Protocol.FrontendProcessResult),
+    step "goal.start" ({ expr := "∀ (n : Nat), n + 1 = Nat.succ n"} : Protocol.GoalStart)
+     ({ stateId := 0, root := "_uniq.65" }: Protocol.GoalStartResult),
+    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro n" }: Protocol.GoalTactic)
+     ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
+    step "goal.tactic" ({ stateId := 1, tactic? := .some "apply add_one" }: Protocol.GoalTactic)
+     ({ nextStateId? := .some 2, goals? := .some #[], }: Protocol.GoalTacticResult),
+  ]
 
 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
   -- Setup the environment for execution
-  let context: Context := {}
+  let coreContext ← createCoreContext #[]
-  let commands: MainM LSpec.TestSeq :=
+  let mainM : MainM LSpec.TestSeq :=
-    steps.foldlM (λ suite step => do
+    steps.foldlM (λ suite step => do return suite ++ (← step)) LSpec.TestSeq.done
-      let result ← step
+  mainM.run { coreContext } |>.run' { env }
-      return suite ++ result) LSpec.TestSeq.done
-  runCoreMSeq env <| commands.run context |>.run' {}
-
 
 def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
-    ("expr.echo", test_elab),
+    ("expr.echo", test_expr_echo),
     ("options.set options.print", test_option_modify),
     ("Malformed command", test_malformed_command),
     ("Tactic", test_tactic),
@@ -258,6 +285,7 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
     ("env.add env.inspect", test_env_add_inspect),
     ("frontend.process invocation", test_frontend_process),
     ("frontend.process sorry", test_frontend_process_sorry),
+    ("frontend.process import", test_import_open),
   ]
   tests.map (fun (name, test) => (name, runTest env test))
 

Test/Tactic/Prograde.lean

@@ -87,7 +87,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
         { userName := "q", type? := .some { pp? := .some "Prop" } },
         { userName := "h", type? := .some { pp? := .some "p" } },
         { userName := "y",
-          type? := .some { pp? := .some "p ∨ ?m.25" },
+          type? := .some { pp? := .some "p ∨ ?m.19" },
           value? := .some { pp? := .some "Or.inl h" },
         }
       ]