Main.lean

@@ -8,12 +8,6 @@ import Repl
 open Pantograph.Repl
 open Pantograph.Protocol
 
-/-- Print a string to stdout without buffering -/
-def printImmediate (s : String) : IO Unit := do
-  let stdout ← IO.getStdout
-  stdout.putStr (s ++ "\n")
-  stdout.flush
-
 /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
 def parseCommand (s: String): Except String Command := do
   match s.trim.get? 0 with
@@ -40,36 +34,37 @@ partial def loop : MainM Unit := do repeat do
   | .error error =>
     let error  := Lean.toJson ({ error := "command", desc := error }: InteractionError)
     -- Using `Lean.Json.compress` here to prevent newline
-    printImmediate error.compress
+    IO.println error.compress
   | .ok command =>
     try
       let ret ← execute command
       let str := match state.options.printJsonPretty with
         | true => ret.pretty
         | false => ret.compress
-      printImmediate str
+      IO.println str
     catch e =>
-      let message := e.toString
+      let message ← e.toMessageData.toString
       let error  := Lean.toJson ({ error := "main", desc := message }: InteractionError)
-      printImmediate error.compress
+      IO.println error.compress
 
-def main (args: List String): IO Unit := do
+
+unsafe def main (args: List String): IO Unit := do
   -- NOTE: A more sophisticated scheme of command line argument handling is needed.
   if args == ["--version"] then do
     IO.println s!"{Pantograph.version}"
     return
 
-  unsafe do
   Pantograph.initSearch ""
 
   -- Separate imports and options
   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 mainM := loop.run { coreContext } |>.run' { env := coreState.env }
+    let coreM := loop.run context |>.run' {}
-    printImmediate "ready."
+    IO.println "ready."
-    mainM
+    discard <| coreM.toIO coreContext coreState
   catch ex =>
     let message := ex.toString
     let error  := Lean.toJson ({ error := "io", desc := message }: InteractionError)

Pantograph/Delate.lean

@@ -26,7 +26,7 @@ def analyzeProjection (env: Environment) (e: Expr): Projection :=
     | _ => panic! "Argument must be proj"
   if (getStructureInfo? env typeName).isSome then
     let ctor := getStructureCtor env typeName
-    let fieldName := (getStructureFields env typeName)[idx]!
+    let fieldName := getStructureFields env typeName |>.get! idx
     let projector := getProjFnForField? env typeName fieldName |>.get!
     .field projector ctor.numParams
   else
@@ -37,7 +37,7 @@ def analyzeProjection (env: Environment) (e: Expr): Projection :=
 def anonymousLevel : Level := .mvar ⟨.anonymous⟩
 
 @[export pantograph_expr_proj_to_app]
-def exprProjToApp (env : Environment) (e : Expr) : Expr :=
+def exprProjToApp (env: Environment) (e: Expr): Expr :=
   let anon : Expr := .mvar ⟨.anonymous⟩
   match analyzeProjection env e with
   | .field projector numParams =>
@@ -66,18 +66,9 @@ def exprProjToApp (env : Environment) (e : Expr) : Expr :=
 def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
 
 /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
-@[export pantograph_unfold_aux_lemmas_m]
+@[export pantograph_unfold_aux_lemmas]
-def unfoldAuxLemmas : Expr → CoreM Expr :=
+def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
-  (Meta.deltaExpand · Lean.Name.isAuxLemma)
+  Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
-/-- Unfold all matcher applications -/
-@[export pantograph_unfold_matchers_m]
-def unfoldMatchers (expr : Expr) : CoreM Expr :=
-  Core.transform expr λ e => do
-    let .some mapp ← Meta.matchMatcherApp? e | return .continue e
-    let .some matcherInfo := (← getEnv).find? mapp.matcherName | panic! "Matcher must exist"
-    let f ← Meta.instantiateValueLevelParams matcherInfo mapp.matcherLevels.toList
-    let mdata := KVMap.empty.insert `matcher (DataValue.ofName mapp.matcherName)
-    return .visit $ .mdata mdata (f.betaRev e.getAppRevArgs (useZeta := true))
 
 /--
 Force the instantiation of delayed metavariables even if they cannot be fully
@@ -94,12 +85,13 @@ This function ensures any metavariable in the result is either
 1. Delayed assigned with its pending mvar not assigned in any form
 2. Not assigned (delay or not)
  -/
-partial def instantiateDelayedMVars (expr : Expr) : MetaM Expr :=
+partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
-  withTraceNode `Pantograph.Delate (λ _ex => return m!":= {← Meta.ppExpr expr}") do
+  --let padding := String.join $ List.replicate level "│ "
-  let mut result ← Meta.transform (← instantiateMVars expr)
+  --IO.println s!"{padding}Starting {toString eOrig}"
-    λ e => e.withApp fun f args => do
+  let mut result ← Meta.transform (← instantiateMVars eOrig)
+    (pre := fun e => e.withApp fun f args => do
       let .mvar mvarId := f | return .continue
-    trace[Pantograph.Delate] "V {e}"
+      --IO.println s!"{padding}├V {e}"
       let mvarDecl ← mvarId.getDecl
 
       -- This is critical to maintaining the interdependency of metavariables.
@@ -117,70 +109,67 @@ partial def instantiateDelayedMVars (expr : Expr) : MetaM Expr :=
           panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}"
 
         if let .some assign ← getExprMVarAssignment? mvarId then
-        trace[Pantograph.Delate] "A ?{mvarId.name}"
+          --IO.println s!"{padding}├A ?{mvarId.name}"
           assert! !(← mvarId.isDelayedAssigned)
           return .visit (mkAppN assign args)
         else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
-        if ← isTracingEnabledFor `Pantograph.Delate then
+          --let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
-          let substTableStr := ",".intercalate $
+          --IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
-            Array.zipWith (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") fvars args |>.toList
-          trace[Pantograph.Delate]"MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
 
           if args.size < fvars.size then
-          throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString expr}"
+            throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
-        if !args.isEmpty then
+          --if !args.isEmpty then
-          trace[Pantograph.Delate] "─ Arguments Begin"
+            --IO.println s!"{padding}├── Arguments Begin"
           let args ← args.mapM self
-        if !args.isEmpty then
+          --if !args.isEmpty then
-          trace[Pantograph.Delate] "─ Arguments End"
+            --IO.println s!"{padding}├── Arguments End"
           if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
-          trace[Pantograph.Delate] "T1"
+            --IO.println s!"{padding}├T1"
             let result := mkAppN f args
             return .done result
 
           let pending ← mvarIdPending.withContext do
-          let inner ← instantiateDelayedMVars (.mvar mvarIdPending)
+            let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
-          trace[Pantograph.Delate] "Pre: {inner}"
+            --IO.println s!"{padding}├Pre: {inner}"
             pure <| (← inner.abstractM fvars).instantiateRev args
 
           -- Tail arguments
           let result := mkAppRange pending fvars.size args.size args
-        trace[Pantograph.Delate] "MD {result}"
+          --IO.println s!"{padding}├MD {result}"
           return .done result
         else
           assert! !(← mvarId.isAssigned)
           assert! !(← mvarId.isDelayedAssigned)
-        if !args.isEmpty then
+          --if !args.isEmpty then
-          trace[Pantograph.Delate] "─ Arguments Begin"
+          --  IO.println s!"{padding}├── Arguments Begin"
           let args ← args.mapM self
-        if !args.isEmpty then
+          --if !args.isEmpty then
-          trace[Pantograph.Delate] "─ Arguments End"
+          --  IO.println s!"{padding}├── Arguments End"
 
-        trace[Pantograph.Delate] "M ?{mvarId.name}"
+          --IO.println s!"{padding}├M ?{mvarId.name}"
-        return .done (mkAppN f args)
+          return .done (mkAppN f args))
-  trace[Pantoraph.Delate] "Result {result}"
+  --IO.println s!"{padding}└Result {result}"
   return result
   where
-  self e := instantiateDelayedMVars e
+  self e := instantiateDelayedMVars e --(level := level + 1)
 
 /--
-Convert an expression to an equivalent form with
+Convert an expression to an equiavlent form with
 1. No nested delayed assigned mvars
-2. No aux lemmas or matchers
+2. No aux lemmas
 3. No assigned mvars
  -/
 @[export pantograph_instantiate_all_m]
-def instantiateAll (e : Expr) : MetaM Expr := do
+def instantiateAll (e: Expr): MetaM Expr := do
   let e ← instantiateDelayedMVars e
   let e ← unfoldAuxLemmas e
-  let e ← unfoldMatchers e
   return e
 
 structure DelayedMVarInvocation where
-  mvarIdPending : MVarId
+  mvarIdPending: MVarId
-  args : Array (FVarId × (Option Expr))
+  args: Array (FVarId × (Option Expr))
   -- Extra arguments applied to the result of this substitution
-  tail : Array Expr
+  tail: Array Expr
 
 -- The pending mvar of any delayed assigned mvar must not be assigned in any way.
 @[export pantograph_to_delayed_mvar_invocation_m]
@@ -605,7 +594,4 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState :
       | other => s!"[{other}]"
     parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
 
-initialize
-  registerTraceClass `Pantograph.Delate
-
 end Pantograph

Pantograph/Elab.lean

@@ -6,8 +6,7 @@ namespace Pantograph
 -- Functions for creating contexts and states
 @[export pantograph_default_elab_context]
 def defaultElabContext: Elab.Term.Context := {
-    declName? := .some `mystery,
+    errToSorry := false
-    errToSorry := false,
   }
 
 /-- Read syntax object from string -/

Pantograph/Environment.lean

@@ -25,10 +25,7 @@ def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[
 @[export pantograph_environment_module_of_name]
 def module_of_name (env: Environment) (name: Name): Option Name := do
   let moduleId ←  env.getModuleIdxFor? name
-  if h : moduleId.toNat < env.allImportedModuleNames.size then
+  return env.allImportedModuleNames.get! moduleId.toNat
-    return env.allImportedModuleNames[moduleId.toNat]
-  else
-    .none
 
 def toCompactSymbolName (n: Name) (info: ConstantInfo): String :=
   let pref := match info with
@@ -52,12 +49,12 @@ def describe (_: Protocol.EnvDescribe): CoreM Protocol.EnvDescribeResult := do
     imports := env.header.imports.map toString,
     modules := env.header.moduleNames.map (·.toString),
   }
-def moduleRead (args: Protocol.EnvModuleRead): CoreM Protocol.EnvModuleReadResult := do
+def moduleRead (args: Protocol.EnvModuleRead): CoreM (Protocol.CR Protocol.EnvModuleReadResult) := do
   let env ← Lean.MonadEnv.getEnv
   let .some i := env.header.moduleNames.findIdx? (· == args.module.toName) |
-    throwError s!"Module not found {args.module}"
+    return .error $ Protocol.errorIndex s!"Module not found {args.module}"
   let data := env.header.moduleData[i]!
-  return {
+  return .ok {
     imports := data.imports.map toString,
     constNames := data.constNames.map (·.toString),
     extraConstNames := data.extraConstNames.map (·.toString),
@@ -69,13 +66,15 @@ def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do
     | .some x => acc.push x
     | .none => acc)
   return { symbols := names }
-def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol.FallibleT CoreM Protocol.EnvInspectResult := do
+def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do
   let env ← Lean.MonadEnv.getEnv
   let name :=  args.name.toName
   let info? := env.find? name
-  let .some info := info? | Protocol.throw $ Protocol.errorIndex s!"Symbol not found {args.name}"
+  let info ← match info? with
+    | none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}"
+    | some info => pure info
   let module? := env.getModuleIdxFor? name >>=
-    (λ idx => env.allImportedModuleNames[idx.toNat]?)
+    (λ idx => env.allImportedModuleNames.get? idx.toNat)
   let value? := match args.value?, info with
     | .some true, _ => info.value?
     | .some false, _ => .none
@@ -89,6 +88,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol.
     isUnsafe := info.isUnsafe,
     value? := ← value?.mapM (λ v => serializeExpression 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 <| type.getUsedConstants.map (λ n => serializeName n)
       else .none,
@@ -143,56 +143,44 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol.
       }
     else
       .pure result
-  return result
+  return .ok result
-/-- Elaborates and adds a declaration to the `CoreM` environment. -/
+def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
-@[export pantograph_env_add_m]
-def addDecl (name: String) (levels: Array String := #[]) (type?: Option String) (value: String) (isTheorem: Bool)
-    : Protocol.FallibleT CoreM Protocol.EnvAddResult := do
   let env ← Lean.MonadEnv.getEnv
-  let levelParams := levels.toList.map (·.toName)
+  let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do
-  let tvM: Elab.TermElabM (Except String (Expr × Expr)) :=
+    let type ← match parseTerm env args.type with
-    Elab.Term.withLevelNames levelParams do do
+      | .ok syn => do
-    let expectedType?? : Except String (Option Expr) ← ExceptT.run $ type?.mapM λ type => do
+        match ← elabTerm syn with
-      match parseTerm env type with
-      | .ok syn => elabTerm syn
-      | .error e => MonadExceptOf.throw e
-    let expectedType? ← match expectedType?? with
-      | .ok t? => pure t?
         | .error e => return .error e
-    let value ← match parseTerm env value with
+        | .ok expr => pure expr
+      | .error e => return .error e
+    let value ← match parseTerm env args.value with
       | .ok syn => do
         try
-          let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := expectedType?)
+          let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .some type)
           Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing
           let expr ← instantiateMVars expr
           pure $ expr
         catch ex => return .error (← ex.toMessageData.toString)
       | .error e => return .error e
-    Elab.Term.synthesizeSyntheticMVarsNoPostponing
+    pure $ .ok (type, value)
-    let type ← match expectedType? with
-      | .some t => pure t
-      | .none => Meta.inferType value
-    pure $ .ok (← instantiateMVars type, ← instantiateMVars value)
   let (type, value) ← match ← tvM.run' (ctx := {}) |>.run' with
     | .ok t => pure t
-    | .error e => Protocol.throw $ Protocol.errorExpr e
+    | .error e => return .error $ Protocol.errorExpr e
-  let decl := if isTheorem then
+  let constant := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx
-    Lean.Declaration.thmDecl <| Lean.mkTheoremValEx
+    (name := args.name.toName)
-      (name := name.toName)
+    (levelParams := [])
-      (levelParams := levelParams)
-      (type := type)
-      (value := value)
-      (all := [])
-  else
-    Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx
-      (name := name.toName)
-      (levelParams := levelParams)
     (type := type)
     (value := value)
     (hints := Lean.mkReducibilityHintsRegularEx 1)
     (safety := Lean.DefinitionSafety.safe)
     (all := [])
-  Lean.addDecl decl
+  let env' ← match env.addDecl (← getOptions) constant with
-  return {}
+    | .error e => do
+      let options ← Lean.MonadOptions.getOptions
+      let desc ← (e.toMessageData options).toString
+      return .error $ { error := "kernel", desc }
+    | .ok env' => pure env'
+  Lean.MonadEnv.modifyEnv (λ _ => env')
+  return .ok {}
 
 end Pantograph.Environment

Pantograph/Frontend/Basic.lean

@@ -40,7 +40,6 @@ def stxByteRange (stx : Syntax) : String.Pos × String.Pos :=
 abbrev FrontendM := Elab.Frontend.FrontendM
 
 structure CompilationStep where
-  scope : Elab.Command.Scope
   fileName : String
   fileMap : FileMap
   src : Substring
@@ -75,7 +74,7 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do
   let msgs := s'.messages.toList.drop s.messages.toList.length
   let trees := s'.infoState.trees.drop s.infoState.trees.size
   let ⟨_, fileName, fileMap⟩  := (← read).inputCtx
-  return ({ scope := s.scopes.head!, fileName, fileMap, src, stx, before, after, msgs, trees }, done)
+  return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done)
 
 partial def mapCompilationSteps { α } (f: CompilationStep → IO α) : FrontendM (List α) := do
   let (cmd, done) ← processOneCommand

Pantograph/Frontend/Elab.lean

@@ -154,7 +154,9 @@ the draft tactic instead.
 -/
 @[export pantograph_frontend_sorrys_to_goal_state_m]
 def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState := do
+  let env := sorrys.head? >>= (·.context?) |>.map (·.env) |>.getD (← getEnv)
   assert! !sorrys.isEmpty
+  withEnv env do
     let goalsM := sorrys.mapM λ i => do
       match i.info with
       | .ofTermInfo termInfo  => do

Pantograph/Frontend/InfoTree.lean

@@ -25,9 +25,9 @@ protected def Info.stx? : Info → Option Syntax
   | .ofCustomInfo         info => info.stx
   | .ofFVarAliasInfo      _    => none
   | .ofFieldRedeclInfo    info => info.stx
+  | .ofOmissionInfo       info => info.stx
   | .ofChoiceInfo         info => info.stx
   | .ofPartialTermInfo    info => info.stx
-  | .ofDelabTermInfo      info => info.stx
 /-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
 protected def Info.isOriginal (i : Info) : Bool :=
   match i.stx? with
@@ -142,9 +142,9 @@ partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .
       | .ofCustomInfo _ => pure "[custom]"
       | .ofFVarAliasInfo _ => pure "[fvar]"
       | .ofFieldRedeclInfo _ => pure "[field_redecl]"
+      | .ofOmissionInfo _ => pure "[omission]"
       | .ofChoiceInfo _ => pure "[choice]"
       | .ofPartialTermInfo  _ => pure "[partial_term]"
-      | .ofDelabTermInfo _ => pure "[delab_term]"
       let children := "\n".intercalate (← children.toList.mapM λ t' => do pure $ indent $ ← t'.toString ctx)
       return s!"{node}\n{children}"
     else throw <| IO.userError "No `ContextInfo` available."

Pantograph/Frontend/MetaTranslate.lean

@@ -62,7 +62,7 @@ private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
   let sourceMCtx ← getSourceMCtx
   -- We want to create as few mvars as possible
   let (srcExpr, _) := instantiateMVarsCore (mctx := sourceMCtx) srcExpr
-  trace[Pantograph.Frontend.MetaTranslate] "Transform src: {srcExpr}"
+  --IO.println s!"Transform src: {srcExpr}"
   let result ← Core.transform srcExpr λ e => do
     let state ← get
     match e with
@@ -100,10 +100,10 @@ partial def translateLocalDecl (srcLocalDecl: LocalDecl) : MetaTranslateM LocalD
   addTranslatedFVar srcLocalDecl.fvarId fvarId
   match srcLocalDecl with
   | .cdecl index _ userName type bi kind => do
-    trace[Pantograph.Frontend.MetaTranslate] "[CD] {userName} {toString type}"
+    --IO.println s!"[CD] {userName} {toString type}"
     return .cdecl index fvarId userName (← translateExpr type) bi kind
   | .ldecl index _ userName type value nonDep kind => do
-    trace[Pantograph.Frontend.MetaTranslate] "[LD] {toString type} := {toString value}"
+    --IO.println s!"[LD] {toString type} := {toString value}"
     return .ldecl index fvarId userName (← translateExpr type) (← translateExpr value) nonDep kind
 
 partial def translateLCtx : MetaTranslateM LocalContext := do
@@ -118,7 +118,6 @@ partial def translateLCtx : MetaTranslateM LocalContext := do
 
 partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
   if let .some mvarId' := (← get).mvarMap[srcMVarId]? then
-    trace[Pantograph.Frontend.MetaTranslate] "Existing mvar id {srcMVarId.name} → {mvarId'.name}"
     return mvarId'
   let mvarId' ← Meta.withLCtx .empty #[] do
     let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get!
@@ -135,7 +134,6 @@ partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
           let fvars' ← mvarIdPending'.withContext $ fvars.mapM translateExpr
           assignDelayedMVar mvarId' fvars' mvarIdPending'
         pure mvarId'
-  trace[Pantograph.Frontend.MetaTranslate] "Translated {srcMVarId.name} → {mvarId'.name}"
   addTranslatedMVar srcMVarId mvarId'
   return mvarId'
 end
@@ -150,7 +148,6 @@ def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab
     let lctx' ← translateLCtx
     let mvar ← Meta.withLCtx lctx' #[] do
       let type' ← translateExpr type
-      trace[Pantograph.Frontend.MetaTranslate] "Translating from term info {← Meta.ppExpr type'}"
       Meta.mkFreshExprSyntheticOpaqueMVar type'
     return mvar.mvarId!
 
@@ -165,7 +162,4 @@ end MetaTranslate
 
 export MetaTranslate (MetaTranslateM)
 
-initialize
-  registerTraceClass `Pantograph.Frontend.MetaTranslate
-
 end Pantograph.Frontend

Pantograph/Goal.lean

@@ -74,35 +74,27 @@ protected def GoalState.metaState (state: GoalState): Meta.State :=
 protected def GoalState.coreState (state: GoalState): Core.SavedState :=
   state.savedState.term.meta.core
 
-protected def GoalState.withContext' (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
+protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
   mvarId.withContext m |>.run' (← read) state.metaState
-protected def GoalState.withContext { m } [MonadControlT MetaM m] [Monad m] (state: GoalState) (mvarId: MVarId) : m α → m α :=
+
-  Meta.mapMetaM <| state.withContext' mvarId
 protected def GoalState.withParentContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
-  Meta.mapMetaM <| state.withContext' state.parentMVar?.get!
+  Meta.mapMetaM <| state.withContext state.parentMVar?.get!
 protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
-  Meta.mapMetaM <| state.withContext' state.root
+  Meta.mapMetaM <| state.withContext state.root
 
 private def GoalState.mvars (state: GoalState): SSet MVarId :=
   state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
--- Restore the name generator and macro scopes of the core state
+protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
-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 := do
+protected def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
-  state.restoreCoreMExtra
   state.savedState.term.restore
 private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do
-  state.restoreElabM
+  state.savedState.restore
   Elab.Tactic.setGoals [goal]
 
 @[export pantograph_goal_state_focus]
 protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do
-  let goal ← state.savedState.tactic.goals[goalId]?
+  let goal ← state.savedState.tactic.goals.get? goalId
   return {
     state with
     savedState := {
@@ -113,14 +105,11 @@ protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState
   }
 
 /-- Immediately bring all parent goals back into scope. Used in automatic mode -/
-@[export pantograph_goal_state_immediate_resume]
+@[export pantograph_goal_state_immediate_resume_parent]
 protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): GoalState :=
   -- Prune parents solved goals
   let mctx := state.mctx
-  let parentGoals := parent.goals.filter λ goal =>
+  let parentGoals := parent.goals.filter $ λ goal => mctx.eAssignment.contains goal
-    let isDuplicate := state.goals.contains goal
-    let isSolved := mctx.eAssignment.contains goal || mctx.dAssignment.contains goal
-    (¬ isDuplicate) && (¬ isSolved)
   {
     state with
     savedState := {
@@ -130,18 +119,19 @@ protected def GoalState.immediateResume (state: GoalState) (parent: GoalState):
   }
 
 /--
-Brings into scope a list of goals. User must ensure `goals` is distinct.
+Brings into scope a list of goals
 -/
 @[export pantograph_goal_state_resume]
-protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState := do
+protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
   if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
     let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString)
     .error s!"Goals {invalid_goals} are not in scope"
+  else
     -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
-  let unassigned := goals.filter λ goal =>
+    let unassigned := goals.filter (λ goal =>
-    let isSolved := state.mctx.eAssignment.contains goal || state.mctx.dAssignment.contains goal
+      let mctx := state.mctx
-    ¬ isSolved
+      ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
-  return {
+    .ok {
       state with
       savedState := {
         term := state.savedState.term,
@@ -161,18 +151,18 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except
     target.resume (goals := branch.goals)
 
 @[export pantograph_goal_state_root_expr]
-protected def GoalState.rootExpr? (goalState : GoalState): Option Expr := do
+protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
   if goalState.root.name == .anonymous then
     .none
   let expr ← goalState.mctx.eAssignment.find? goalState.root
   let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
+  if expr.hasExprMVar then
+    -- Must not assert that the goal state is empty here. We could be in a branch goal.
+    --assert! ¬goalState.goals.isEmpty
+    .none
+  else
+    assert! goalState.goals.isEmpty
     return expr
-@[export pantograph_goal_state_is_solved]
-protected def GoalState.isSolved (goalState : GoalState) : Bool :=
-  let solvedRoot := match goalState.rootExpr? with
-    | .some e => ¬ e.hasExprMVar
-    | .none => true
-  goalState.goals.isEmpty && solvedRoot
 @[export pantograph_goal_state_parent_expr]
 protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
   let parent ← goalState.parentMVar?
@@ -224,7 +214,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)
@@ -240,20 +230,23 @@ protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Ta
 /-- Response for executing a tactic -/
 inductive TacticResult where
   -- Goes to next state
-  | success (state : GoalState) (messages : Array String)
+  | success (state: GoalState)
   -- Tactic failed with messages
-  | failure (messages : Array String)
+  | failure (messages: Array String)
   -- Could not parse tactic
-  | parseError (message : String)
+  | parseError (message: String)
   -- The given action cannot be executed in the state
-  | invalidAction (message : String)
+  | invalidAction (message: String)
 
-private def dumpMessageLog (prevMessageLength : Nat) : CoreM (Bool × Array String) := do
+private def dumpMessageLog (prevMessageLength : Nat) : CoreM (Array String) := do
-  let newMessages := (← Core.getMessageLog).toList.drop prevMessageLength
+  let newMessages ← (← Core.getMessageLog).toList.drop prevMessageLength
-  let hasErrors := newMessages.any (·.severity == .error)
+    |>.filterMapM λ m => do
-  let newMessages ← newMessages.mapM λ m => m.toString
+      if m.severity == .error then
+        return .some $ ← m.toString
+      else
+        return .none
   Core.resetMessageLog
-  return (hasErrors, newMessages.toArray)
+  return newMessages.toArray
 
 /-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
 protected def GoalState.tryTacticM
@@ -265,16 +258,13 @@ protected def GoalState.tryTacticM
     let nextState ← state.step goal tacticM guardMVarErrors
 
     -- Check if error messages have been generated in the core.
-    let (hasError, newMessages) ← dumpMessageLog prevMessageLength
+    let newMessages ← dumpMessageLog prevMessageLength
-    if hasError then
+    if ¬ newMessages.isEmpty then
       return .failure newMessages
-    else
+    return .success nextState
-      return .success nextState newMessages
   catch exception =>
     match exception with
-    | .internal _ =>
+    | .internal _ => return .failure $ ← dumpMessageLog prevMessageLength
-      let (_, messages) ← dumpMessageLog prevMessageLength
-      return .failure messages
     | _ => return .failure #[← exception.toMessageData.toString]
 
 /-- Execute a string tactic on given state. Restores TermElabM -/
@@ -289,7 +279,6 @@ 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):
@@ -343,7 +332,7 @@ protected def GoalState.conv (state: GoalState) (goal: MVarId):
       parentMVar? := .some goal,
       convMVar? := .some (convRhs, goal, otherGoals),
       calcPrevRhs? := .none
-    } #[]
+    }
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
@@ -380,7 +369,7 @@ protected def GoalState.convExit (state: GoalState):
       parentMVar? := .some convGoal,
       convMVar? := .none
       calcPrevRhs? := .none
-    } #[]
+    }
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
@@ -458,7 +447,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String)
       },
       parentMVar? := .some goal,
       calcPrevRhs?
-    } #[]
+    }
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 

Pantograph/Library.lean

@@ -3,7 +3,6 @@ import Pantograph.Goal
 import Pantograph.Protocol
 import Pantograph.Delate
 import Pantograph.Version
-
 import Lean
 
 namespace Lean
@@ -41,6 +40,8 @@ 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 }
 
@@ -74,45 +75,63 @@ def createCoreState (imports: Array String): IO Core.State := do
     (trustLevel := 1)
   return { env := env }
 
+@[export pantograph_env_add_m]
+def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
+    CoreM (Protocol.CR Protocol.EnvAddResult) :=
+  Environment.addDecl { name, type, value, isTheorem }
+
 @[export pantograph_parse_elab_type_m]
-def parseElabType (type: String): Protocol.FallibleT Elab.TermElabM Expr := do
+def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do
   let env ← MonadEnv.getEnv
   let syn ← match parseTerm env type with
-    | .error str => Protocol.throw $ errorI "parsing" str
+    | .error str => return .error $ errorI "parsing" str
     | .ok syn => pure syn
   match ← elabType syn with
-  | .error str => Protocol.throw $ errorI "elab" str
+  | .error str => return .error $ errorI "elab" str
-  | .ok expr => return (← instantiateMVars expr)
+  | .ok expr => return .ok (← instantiateMVars expr)
 
 /-- This must be a TermElabM since the parsed expr contains extra information -/
 @[export pantograph_parse_elab_expr_m]
-def parseElabExpr (expr: String) (expectedType?: Option String := .none): Protocol.FallibleT Elab.TermElabM Expr := do
+def parseElabExpr (expr: String) (expectedType?: Option String := .none): Elab.TermElabM (Protocol.CR Expr) := do
   let env ← MonadEnv.getEnv
-  let expectedType? ← expectedType?.mapM parseElabType
+  let expectedType? ← match ← expectedType?.mapM parseElabType with
+    | .none => pure $ .none
+    | .some (.ok t) => pure $ .some t
+    | .some (.error e) => return .error e
   let syn ← match parseTerm env expr with
-    | .error str => Protocol.throw $ errorI "parsing" str
+    | .error str => return .error $ errorI "parsing" str
     | .ok syn => pure syn
   match ← elabTerm syn expectedType? with
-  | .error str => Protocol.throw $ errorI "elab" str
+  | .error str => return .error $ errorI "elab" str
-  | .ok expr => return (← instantiateMVars expr)
+  | .ok expr => return .ok (← instantiateMVars expr)
 
 @[export pantograph_expr_echo_m]
-def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options := {}):
+def exprEcho (expr: String) (expectedType?: Option String := .none) (levels: Array String := #[])  (options: @&Protocol.Options := {}):
-    Protocol.FallibleT Elab.TermElabM Protocol.ExprEchoResult := do
+    CoreM (Protocol.CR Protocol.ExprEchoResult) :=
-  let expr ← parseElabExpr expr expectedType?
+  runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
+    let expr ← match ← parseElabExpr expr expectedType? with
+      | .error e => return .error e
+      | .ok expr => pure expr
     try
       let type ← unfoldAuxLemmas (← Meta.inferType expr)
-    return {
+      return .ok {
           type := (← serializeExpression options type),
-        expr := (← serializeExpression options expr),
+          expr := (← serializeExpression options expr)
       }
     catch exception =>
-    Protocol.throw $ errorI "typing" (← exception.toMessageData.toString)
+      return .error $ errorI "typing" (← exception.toMessageData.toString)
 
 @[export pantograph_goal_start_expr_m]
-def goalStartExpr (expr: String) : Protocol.FallibleT Elab.TermElabM GoalState := do
+def goalStartExpr (expr: String) (levels: Array String): CoreM (Protocol.CR GoalState) :=
-  let t ← parseElabType expr
+  runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
-  GoalState.create t
+    let expr ← match ← parseElabType expr with
+      | .error e => return .error e
+      | .ok expr => pure $ expr
+    return .ok $ ← GoalState.create expr
+
+@[export pantograph_goal_resume]
+def goalResume (target: GoalState) (goals: Array String): Except String GoalState :=
+  target.resume (goals.map (λ n => { name := n.toName }) |>.toList)
 
 @[export pantograph_goal_serialize_m]
 def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) :=
@@ -123,9 +142,8 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
   : CoreM Protocol.GoalPrintResult := runMetaM do
   state.restoreMetaM
 
-  let rootExpr? := state.rootExpr?
   let root? ← if rootExpr then
-      rootExpr?.mapM λ expr => state.withRootContext do
+      state.rootExpr?.mapM λ expr => state.withRootContext do
         serializeExpression options (← instantiateAll expr)
     else
       pure .none
@@ -144,45 +162,70 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
     state.withContext mvarId do
       let .some expr ← getExprMVarAssignment? mvarId | return {}
       serializeExpression options (← instantiateAll expr)
-  let env ← getEnv
   return {
     root?,
     parent?,
     goals,
     extraMVars,
-    rootHasSorry := rootExpr?.map (·.hasSorry) |>.getD false,
-    rootHasUnsafe := rootExpr?.map (env.hasUnsafe ·) |>.getD false,
-    rootHasMVar := rootExpr?.map (·.hasExprMVar) |>.getD false,
   }
 
+@[export pantograph_goal_tactic_m]
+def goalTactic (state: GoalState) (goal:  MVarId) (tactic: String): CoreM TacticResult :=
+  runTermElabM <| state.tryTactic goal tactic
+@[export pantograph_goal_assign_m]
+def goalAssign (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticResult :=
+  runTermElabM <| state.tryAssign goal expr
 @[export pantograph_goal_have_m]
-protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): Elab.TermElabM TacticResult := do
+protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult := do
   let type ← match (← parseTermM type) with
     | .ok syn => pure syn
     | .error error => return .parseError error
+  runTermElabM do
     state.restoreElabM
     state.tryTacticM goal $ Tactic.evalHave binderName.toName type
 @[export pantograph_goal_try_define_m]
-protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): Elab.TermElabM TacticResult := do
+protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): CoreM TacticResult := do
   let expr ← match (← parseTermM expr) with
     | .ok syn => pure syn
     | .error error => return .parseError error
+  runTermElabM do
     state.restoreElabM
     state.tryTacticM goal (Tactic.evalDefine binderName.toName expr)
+@[export pantograph_goal_try_motivated_apply_m]
+protected def GoalState.tryMotivatedApply (state: GoalState) (goal: MVarId) (recursor: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  let recursor ← match (← parseTermM recursor) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  state.tryTacticM goal (tacticM := Tactic.evalMotivatedApply recursor)
+@[export pantograph_goal_try_no_confuse_m]
+protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  let eq ← match (← parseTermM eq) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq)
 @[export pantograph_goal_try_draft_m]
-protected def GoalState.tryDraft (state: GoalState) (goal: MVarId) (expr: String): Elab.TermElabM TacticResult := do
+protected def GoalState.tryDraft (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticResult := do
   let expr ← match (← parseTermM expr) with
     | .ok syn => pure syn
     | .error error => return .parseError error
+  runTermElabM do
     state.restoreElabM
     state.tryTacticM goal (Tactic.evalDraft expr)
-
+@[export pantograph_goal_let_m]
--- Cancel the token after a timeout.
+def goalLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult :=
-@[export pantograph_run_cancel_token_with_timeout_m]
+  runTermElabM <| state.tryLet goal binderName type
-def runCancelTokenWithTimeout (cancelToken : IO.CancelToken) (timeout : UInt32) : IO Unit := do
+@[export pantograph_goal_conv_m]
-  let _ ← EIO.asTask do
+def goalConv (state: GoalState) (goal: MVarId): CoreM TacticResult :=
-    IO.sleep timeout
+  runTermElabM <| state.conv goal
-    cancelToken.set
+@[export pantograph_goal_conv_exit_m]
-  return ()
+def goalConvExit (state: GoalState): CoreM TacticResult :=
+  runTermElabM <| state.convExit
+@[export pantograph_goal_calc_m]
+def goalCalc (state: GoalState) (goal: MVarId) (pred: String): CoreM TacticResult :=
+  runTermElabM <| state.tryCalc goal pred
 
 end Pantograph

Pantograph/Protocol.lean

@@ -30,8 +30,6 @@ structure Options where
   printImplementationDetailHyps: Bool := false
   -- If this is set to `true`, goals will never go dormant, so you don't have to manage resumption
   automaticMode: Bool := true
-  -- Timeout for tactics and operations that could potentially execute a tactic
-  timeout: Nat := 0
   deriving Lean.ToJson
 
 abbrev OptionsT := ReaderT Options
@@ -105,9 +103,9 @@ structure StatResult where
 -- Return the type of an expression
 structure ExprEcho where
   expr: String
-  type?: Option String := .none
+  type?: Option String
   -- universe levels
-  levels?: Option (Array String) := .none
+  levels: Option (Array String) := .none
   deriving Lean.FromJson
 structure ExprEchoResult where
   expr: Expression
@@ -204,10 +202,9 @@ structure EnvInspectResult where
 
 structure EnvAdd where
   name: String
-  levels?: Option (Array String) := .none
+  type: String
-  type?: Option String := .none
   value: String
-  isTheorem: Bool := false
+  isTheorem: Bool
   deriving Lean.FromJson
 structure EnvAddResult where
   deriving Lean.ToJson
@@ -220,15 +217,14 @@ structure EnvSaveLoadResult where
 
 /-- Set options; See `Options` struct above for meanings -/
 structure OptionsSet where
-  printJsonPretty?: Option Bool := .none
+  printJsonPretty?: Option Bool
-  printExprPretty?: Option Bool := .none
+  printExprPretty?: Option Bool
-  printExprAST?: Option Bool := .none
+  printExprAST?: Option Bool
-  printDependentMVars?: Option Bool := .none
+  printDependentMVars?: Option Bool
-  noRepeat?: Option Bool := .none
+  noRepeat?: Option Bool
-  printAuxDecls?: Option Bool := .none
+  printAuxDecls?: Option Bool
-  printImplementationDetailHyps?: Option Bool := .none
+  printImplementationDetailHyps?: Option Bool
-  automaticMode?: Option Bool := .none
+  automaticMode?: Option Bool
-  timeout?: Option Nat := .none
   deriving Lean.FromJson
 structure OptionsSetResult where
   deriving Lean.ToJson
@@ -239,8 +235,8 @@ structure GoalStart where
   -- Only one of the fields below may be populated.
   expr: Option String     -- Directly parse in an expression
   -- universe levels
-  levels?: Option (Array String) := .none
+  levels: Option (Array String) := .none
-  copyFrom: Option String := .none -- Copy the type from a theorem in the environment
+  copyFrom: Option String -- Copy the type from a theorem in the environment
   deriving Lean.FromJson
 structure GoalStartResult where
   stateId: Nat := 0
@@ -268,17 +264,14 @@ structure GoalTactic where
 structure GoalTacticResult where
   -- The next goal state id. Existence of this field shows success
   nextStateId?: Option Nat          := .none
-  -- If the array is empty, it shows the goals have been fully resolved. If this
+  -- If the array is empty, it shows the goals have been fully resolved.
-  -- is .none, there has been a tactic error.
   goals?: Option (Array Goal)          := .none
 
-  messages? : Option (Array String) := .some #[]
+  -- Existence of this field shows tactic execution failure
+  tacticErrors?: Option (Array String) := .none
 
   -- Existence of this field shows the tactic parsing has failed
-  parseError? : Option String       := .none
+  parseError?: Option String := .none
-
-  hasSorry : Bool := false
-  hasUnsafe : Bool := false
   deriving Lean.ToJson
 structure GoalContinue where
   -- State from which the continuation acquires the context
@@ -322,10 +315,6 @@ structure GoalPrintResult where
   parent?: Option Expression := .none
   goals: Array Goal := #[]
   extraMVars: Array Expression := #[]
-
-  rootHasSorry : Bool := false
-  rootHasUnsafe : Bool := false
-  rootHasMVar : Bool := true
   deriving Lean.ToJson
 
 -- Diagnostic Options, not available in REPL
@@ -357,10 +346,6 @@ structure FrontendProcess where
   -- One of these two must be supplied: Either supply the file name or the content.
   fileName?: Option String := .none
   file?: Option String := .none
-  -- Whether to read the header
-  readHeader : Bool := false
-  -- Alter the REPL environment after the compilation units.
-  inheritEnv : Bool := false
   -- collect tactic invocations
   invocations: Bool := false
   -- collect `sorry`s
@@ -397,9 +382,6 @@ structure FrontendProcessResult where
   units: List CompilationUnit
   deriving Lean.ToJson
 
-abbrev FallibleT := ExceptT InteractionError
+abbrev CR α := Except InteractionError α
-
-abbrev throw {m : Type v → Type w} [MonadExceptOf InteractionError m] {α : Type v} (e : InteractionError) : m α :=
-  throwThe InteractionError e
 
 end Pantograph.Protocol

Pantograph/Tactic.lean

@@ -1,2 +1,5 @@
 import Pantograph.Tactic.Assign
+import Pantograph.Tactic.Congruence
+import Pantograph.Tactic.MotivatedApply
+import Pantograph.Tactic.NoConfuse
 import Pantograph.Tactic.Prograde

Pantograph/Tactic/Assign.lean

@@ -28,16 +28,15 @@ def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
   Elab.Tactic.replaceMainGoal nextGoals
 
 def sorryToHole (src : Expr) : StateRefT (List MVarId) MetaM Expr := do
-  Meta.transform src λ expr =>
+  Meta.transform src λ
-    if expr.isSorry then do
+    | .app (.app (.const ``sorryAx ..) type) .. => do
-      let type ← instantiateMVars (expr.getArg! 0 |>.bindingBody!)
+      let type ← instantiateMVars type
       if type.hasSorry then
         throwError s!"Coupling is not allowed in draft tactic: {← Meta.ppExpr type}"
       let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type
       modify (mvar.mvarId! :: .)
       pure $ .done mvar
-    else
+    | _ => pure .continue
-      pure .continue
 
 -- Given a complete (no holes) expression, extract the sorry's from it and convert them into goals.
 def draft (goal : MVarId) (expr : Expr) : MetaM (List MVarId) := do

Pantograph/Tactic/Congruence.lean

@@ -0,0 +1,98 @@
+import Lean
+
+open Lean
+
+namespace Pantograph.Tactic
+
+def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.congruenceArg
+  let target ← mvarId.getType
+  let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq"
+  let userName := (← mvarId.getDecl).userName
+
+  let u ← Meta.mkFreshLevelMVar
+  let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u)
+    (tag := userName ++ `α)
+  let f ← Meta.mkFreshExprSyntheticOpaqueMVar (.forallE .anonymous α β .default)
+    (tag := userName ++ `f)
+  let a₁ ← Meta.mkFreshExprSyntheticOpaqueMVar α
+    (tag := userName ++ `a₁)
+  let a₂ ← Meta.mkFreshExprSyntheticOpaqueMVar α
+    (tag := userName ++ `a₂)
+  let h ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq a₁ a₂)
+    (tag := userName ++ `h)
+  let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) target
+  let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType
+    (tag := userName ++ `conduit)
+  mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
+  let result := [α, a₁, a₂, f,  h, conduit]
+  return result.map (·.mvarId!)
+
+def evalCongruenceArg: Elab.Tactic.TacticM Unit := do
+  let goal ← Elab.Tactic.getMainGoal
+  let nextGoals ← congruenceArg goal
+  Elab.Tactic.replaceMainGoal nextGoals
+
+def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.congruenceFun
+  let target ← mvarId.getType
+  let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq"
+  let userName := (← mvarId.getDecl).userName
+  let u ← Meta.mkFreshLevelMVar
+  let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u)
+    (tag := userName ++ `α)
+  let fType := .forallE .anonymous α β .default
+  let f₁ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
+    (tag := userName ++ `f₁)
+  let f₂ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
+    (tag := userName ++ `f₂)
+  let a ← Meta.mkFreshExprSyntheticOpaqueMVar α
+    (tag := userName ++ `a)
+  let h ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq f₁ f₂)
+    (tag := userName ++ `h)
+  let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) target
+  let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType
+    (tag := userName ++ `conduit)
+  mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
+  let result := [α, f₁, f₂, h, a, conduit]
+  return result.map (·.mvarId!)
+
+def evalCongruenceFun: Elab.Tactic.TacticM Unit := do
+  let goal ← Elab.Tactic.getMainGoal
+  let nextGoals ← congruenceFun goal
+  Elab.Tactic.replaceMainGoal nextGoals
+
+def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.congruence
+  let target ← mvarId.getType
+  let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq"
+  let userName := (← mvarId.getDecl).userName
+  let u ← Meta.mkFreshLevelMVar
+  let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u)
+    (tag := userName ++ `α)
+  let fType := .forallE .anonymous α β .default
+  let f₁ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
+    (tag := userName ++ `f₁)
+  let f₂ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
+    (tag := userName ++ `f₂)
+  let a₁ ← Meta.mkFreshExprSyntheticOpaqueMVar α
+    (tag := userName ++ `a₁)
+  let a₂ ← Meta.mkFreshExprSyntheticOpaqueMVar α
+    (tag := userName ++ `a₂)
+  let h₁ ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq f₁ f₂)
+    (tag := userName ++ `h₁)
+  let h₂ ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq a₁ a₂)
+    (tag := userName ++ `h₂)
+  let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) target
+  let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType
+    (tag := userName ++ `conduit)
+  mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂)
+  let result := [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
+  return result.map (·.mvarId!)
+
+def evalCongruence: Elab.Tactic.TacticM Unit := do
+  let goal ← Elab.Tactic.getMainGoal
+  let nextGoals ← congruence goal
+  Elab.Tactic.replaceMainGoal nextGoals
+
+end Pantograph.Tactic

Pantograph/Tactic/MotivatedApply.lean

@@ -0,0 +1,106 @@
+import Lean
+
+open Lean
+
+namespace Pantograph.Tactic
+
+def getForallArgsBody: Expr → List Expr × Expr
+  | .forallE _ d b _ =>
+    let (innerArgs, innerBody) := getForallArgsBody b
+    (d :: innerArgs, innerBody)
+  | e => ([], e)
+
+def replaceForallBody: Expr → Expr → Expr
+  | .forallE param domain body binderInfo, target =>
+    let body := replaceForallBody body target
+    .forallE param domain body binderInfo
+  | _, target => target
+
+structure RecursorWithMotive where
+  args: List Expr
+  body: Expr
+
+  -- .bvar index for the motive and major from the body
+  iMotive: Nat
+
+namespace RecursorWithMotive
+
+protected def nArgs (info: RecursorWithMotive): Nat := info.args.length
+
+protected def getMotiveType (info: RecursorWithMotive): Expr :=
+  let level := info.nArgs - info.iMotive - 1
+  let a := info.args.get! level
+  a
+
+protected def surrogateMotiveType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
+  let motiveType := Expr.instantiateRev info.getMotiveType mvars
+  let resultantType ← Meta.inferType resultant
+  return replaceForallBody motiveType resultantType
+
+protected def conduitType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
+  let motiveCall := Expr.instantiateRev info.body mvars
+  Meta.mkEq motiveCall resultant
+
+end RecursorWithMotive
+
+def getRecursorInformation (recursorType: Expr): Option RecursorWithMotive := do
+  let (args, body) := getForallArgsBody recursorType
+  if ¬ body.isApp then
+    .none
+  let iMotive ← match body.getAppFn with
+    | .bvar iMotive => pure iMotive
+    | _ => .none
+  return {
+    args,
+    body,
+    iMotive,
+  }
+
+def collectMotiveArguments (forallBody: Expr): SSet Nat :=
+  match forallBody with
+  | .app (.bvar i) _ => SSet.empty.insert i
+  | _ => SSet.empty
+
+/-- Applies a symbol of the type `∀ (motive: α → Sort u) (a: α)..., (motive α)` -/
+def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.InductionSubgoal) := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.motivatedApply
+  let recursorType ← Meta.inferType recursor
+  let resultant ← mvarId.getType
+  let tag ← mvarId.getTag
+
+  let info ← match getRecursorInformation recursorType with
+    | .some info => pure info
+    | .none => throwError "Recursor return type does not correspond with the invocation of a motive: {← Meta.ppExpr recursorType}"
+
+  let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do
+    if i ≥ info.nArgs then
+      return prev
+    else
+      let argType := info.args.get! i
+      -- If `argType` has motive references, its goal needs to be placed in it
+      let argType := argType.instantiateRev prev
+      let bvarIndex := info.nArgs - i - 1
+      let argGoal ← if bvarIndex = info.iMotive then
+          let surrogateMotiveType ← info.surrogateMotiveType prev resultant
+          Meta.mkFreshExprSyntheticOpaqueMVar surrogateMotiveType (tag := tag ++ `motive)
+        else
+          Meta.mkFreshExprSyntheticOpaqueMVar argType (tag := .anonymous)
+      let prev :=  prev ++ [argGoal]
+      go (i + 1) prev
+    termination_by info.nArgs - i
+  let mut newMVars ← go 0 #[]
+
+  -- Create the conduit type which proves the result of the motive is equal to the goal
+  let conduitType ← info.conduitType newMVars resultant
+  let goalConduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType (tag := `conduit)
+  mvarId.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
+  newMVars := newMVars ++ [goalConduit]
+
+  return newMVars.map (λ mvar => { mvarId := mvar.mvarId!})
+
+def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
+  let recursor ← Elab.Term.elabTerm (stx := stx) .none
+  let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor
+  Elab.Tactic.replaceMainGoal $ nextGoals.toList.map (·.mvarId)
+
+end Pantograph.Tactic

Pantograph/Tactic/NoConfuse.lean

@@ -0,0 +1,22 @@
+import Lean
+
+open Lean
+
+namespace Pantograph.Tactic
+
+def noConfuse (mvarId: MVarId) (h: Expr): MetaM Unit := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.noConfuse
+  let target ← mvarId.getType
+  let noConfusion ← Meta.mkNoConfusion (target := target) (h := h)
+
+  unless ← Meta.isDefEq (← Meta.inferType noConfusion) target do
+    throwError "invalid noConfuse call: The resultant type {← Meta.ppExpr $ ← Meta.inferType noConfusion} cannot be unified with {← Meta.ppExpr target}"
+  mvarId.assign noConfusion
+
+def evalNoConfuse: Elab.Tactic.Tactic := λ stx => do
+  let goal ← Elab.Tactic.getMainGoal
+  let h ← goal.withContext $ Elab.Term.elabTerm (stx := stx) .none
+  noConfuse goal h
+  Elab.Tactic.replaceMainGoal []
+
+end Pantograph.Tactic

Pantograph/Version.lean

@@ -1,6 +1,6 @@
 namespace Pantograph
 
 @[export pantograph_version]
-def version := "0.3.1"
+def version := "0.2.25"
 
 end Pantograph

README.md

@@ -81,7 +81,7 @@ the environment might be setup like this:
 ``` sh
 LIB="../lib"
 LIB_MATHLIB="$LIB/mathlib4/.lake"
-export LEAN_PATH="$LIB_MATHLIB:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
+export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
 
 LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
 ```

Repl.lean

@@ -5,30 +5,18 @@ namespace Pantograph.Repl
 
 open Lean
 
-set_option trace.Pantograph.Frontend.MetaTranslate true
-
 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
+/-- Main state monad for executing commands -/
-  -- Parser state
+abbrev MainM := ReaderT Context $ StateRefT State CoreM
-  scope : Elab.Command.Scope := { header := "" }
+/-- Fallible subroutine return type -/
-
+abbrev CR α := Except Protocol.InteractionError α
-/-- Main monad for executing commands -/
-abbrev MainM := ReaderT Context $ StateRefT State IO
-/-- Main with possible exception -/
-abbrev EMainM := Protocol.FallibleT $ ReaderT Context $ StateRefT State IO
-def getMainState : MainM State := get
-
-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
@@ -39,61 +27,11 @@ def newGoalState (goalState: GoalState) : MainM Nat := do
   }
   return stateId
 
-def runCoreM { α } (coreM : CoreM α) : EMainM α := do
-  let scope := (← get).scope
-  let options :=(← get).options
-  let cancelTk? ← match options.timeout with
-    | 0 => pure .none
-    | _ => .some <$> IO.CancelToken.new
-  let coreCtx : Core.Context := {
-    (← read).coreContext with
-    currNamespace      := scope.currNamespace,
-    openDecls          := scope.openDecls,
-    options            := scope.opts,
-    initHeartbeats     :=  ← IO.getNumHeartbeats,
-    cancelTk?,
-  }
-  let coreState : Core.State := {
-    env := (← get).env
-  }
-  -- Remap the coreM to capture every exception
-  let coreM' : CoreM _ :=
-    try
-      Except.ok <$> coreM
-    catch ex =>
-      let desc ← ex.toMessageData.toString
-      return Except.error $ ({ error := "exception", desc } : Protocol.InteractionError)
-    finally
-      for {msg, ..} in (← getTraceState).traces do
-        IO.eprintln (← msg.format.toIO)
-      resetTraceState
-  if let .some token := cancelTk? then
-    runCancelTokenWithTimeout token (timeout := .ofBitVec options.timeout)
-  let (result, state') ← match ← (coreM'.run coreCtx coreState).toIO' with
-    | Except.error (Exception.error _ msg)   => Protocol.throw $ { error := "core", desc := ← msg.toString }
-    | Except.error (Exception.internal id _) => Protocol.throw $ { error := "internal", desc := (← id.getName).toString }
-    | Except.ok a                            => pure a
-  if result matches .ok _ then
-    modifyEnv λ _ => state'.env
-  liftExcept result
 
-def runCoreM' { α } (coreM : Protocol.FallibleT CoreM α) : EMainM α := do
+def runMetaInMainM { α } (metaM: MetaM α): MainM α :=
-  liftExcept $ ← runCoreM coreM.run
+  metaM.run'
-
+def runTermElabInMainM { α } (termElabM: Elab.TermElabM α) : MainM α :=
-
+  termElabM.run' (ctx := defaultElabContext) |>.run'
-def liftMetaM { α } (metaM : MetaM α): EMainM α :=
-  runCoreM metaM.run'
-def liftTermElabM { α } (termElabM: Elab.TermElabM α) (levelNames : List Name := [])
-    : EMainM α := do
-  let scope := (← get).scope
-  let context := {
-    errToSorry := false,
-    isNoncomputableSection := scope.isNoncomputable,
-  }
-  let state := {
-    levelNames := scope.levelNames ++ levelNames,
-  }
-  runCoreM $ termElabM.run' context state |>.run'
 
 section Frontend
 
@@ -106,19 +44,20 @@ structure CompilationUnit where
   messages : Array String
   newConstants : List Name
 
-def frontend_process_inner (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
+def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
-  let options := (← getMainState).options
+  let options := (← get).options
   let (fileName, file) ← match args.fileName?, args.file? with
     | .some fileName, .none => do
       let file ← IO.FS.readFile fileName
       pure (fileName, file)
     | .none, .some file =>
       pure ("<anonymous>", file)
-    | _, _ => Protocol.throw $ errorI "arguments" "Exactly one of {fileName, file} must be supplied"
+    | _, _ => return .error <| errorI "arguments" "Exactly one of {fileName, file} must be supplied"
-  let env?: Option Environment ← if args.readHeader then
+  let env?: Option Environment ← if args.fileName?.isSome then
       pure .none
     else do
-      .some <$> getEnv
+      let env ← getEnv
+      pure <| .some env
   let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
   let frontendM: Elab.Frontend.FrontendM (List CompilationUnit) :=
     Frontend.mapCompilationSteps λ step => do
@@ -144,25 +83,18 @@ def frontend_process_inner (args: Protocol.FrontendProcess): EMainM Protocol.Fro
       messages,
       newConstants
     }
-  let (li, state') ← frontendM.run context |>.run state
+  let li ← 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
       else
         .none
-    let (goalStateId?, goals?, goalSrcBoundaries?) ← if step.sorrys.isEmpty then
+    let (goalStateId?, goals?, goalSrcBoundaries?) ← if step.sorrys.isEmpty then do
         pure (.none, .none, .none)
       else do
-        let ({ state, srcBoundaries }, goals) ← liftMetaM do
+        let { state, srcBoundaries } ← runMetaInMainM $ Frontend.sorrysToGoalState step.sorrys
-          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
@@ -175,23 +107,20 @@ def frontend_process_inner (args: Protocol.FrontendProcess): EMainM Protocol.Fro
       goalSrcBoundaries?,
       newConstants?,
     }
-  return { units }
+  return .ok { units }
 
 end Frontend
 
 /-- Main loop command of the REPL -/
 def execute (command: Protocol.Command): MainM Json := do
-  let run { α β: Type } [FromJson α] [ToJson β] (comm: α → EMainM β): MainM Json :=
+  let run { α β: Type } [FromJson α] [ToJson β] (comm: α → MainM (CR β)): MainM Json :=
-    try
     match fromJson? command.payload with
     | .ok args => do
-        match (← comm args |>.run) with
+      match (← comm args) with
       | .ok result =>  return toJson result
       | .error ierror => return toJson ierror
     | .error error => return toJson $ errorCommand s!"Unable to parse json: {error}"
-    catch ex : IO.Error =>
+  try
-      let error : Protocol.InteractionError := { error := "io", desc := ex.toString }
-      return toJson error
     match command.cmd with
     | "reset"         => run reset
     | "stat"          => run stat
@@ -217,48 +146,50 @@ def execute (command: Protocol.Command): MainM Json := do
       let error: Protocol.InteractionError :=
         errorCommand s!"Unknown command {cmd}"
       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): EMainM Protocol.StatResult := do
+  reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
-    let state ← getMainState
+    let state ← get
     let nGoals := state.goalStates.size
     set { state with nextId := 0, goalStates := .empty }
-    return { nGoals }
+    Core.resetMessageLog
-  stat (_: Protocol.Stat): EMainM Protocol.StatResult := do
+    return .ok { nGoals }
-    let state ← getMainState
+  stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
+    let state ← get
     let nGoals := state.goalStates.size
-    return { nGoals }
+    return .ok { nGoals }
-  env_describe (args: Protocol.EnvDescribe): EMainM Protocol.EnvDescribeResult := do
+  env_describe (args: Protocol.EnvDescribe): MainM (CR Protocol.EnvDescribeResult) := do
-    let result ← runCoreM $ Environment.describe args
+    let result ← Environment.describe args
-    return result
+    return .ok result
-  env_module_read (args: Protocol.EnvModuleRead): EMainM Protocol.EnvModuleReadResult := do
+  env_module_read (args: Protocol.EnvModuleRead): MainM (CR Protocol.EnvModuleReadResult) := do
-    runCoreM $ Environment.moduleRead args
+    Environment.moduleRead args
-  env_catalog (args: Protocol.EnvCatalog): EMainM Protocol.EnvCatalogResult := do
+  env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
-    let result ← runCoreM $ Environment.catalog args
+    let result ← Environment.catalog args
-    return result
+    return .ok result
-  env_inspect (args: Protocol.EnvInspect): EMainM Protocol.EnvInspectResult := do
+  env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do
-    let state ← getMainState
+    let state ← get
-    runCoreM' $ Environment.inspect args state.options
+    Environment.inspect args state.options
-  env_add (args: Protocol.EnvAdd): EMainM Protocol.EnvAddResult := do
+  env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
-    runCoreM' $ Environment.addDecl args.name (args.levels?.getD #[]) args.type? args.value args.isTheorem
+    Environment.addDecl args
-  env_save (args: Protocol.EnvSaveLoad): EMainM Protocol.EnvSaveLoadResult := do
+  env_save (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
     let env ← MonadEnv.getEnv
     environmentPickle env args.path
-    return {}
+    return .ok {}
-  env_load (args: Protocol.EnvSaveLoad): EMainM Protocol.EnvSaveLoadResult := do
+  env_load (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
     let (env, _) ← environmentUnpickle args.path
     setEnv env
-    return {}
+    return .ok {}
-  expr_echo (args: Protocol.ExprEcho): EMainM Protocol.ExprEchoResult := do
+  expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
-    let state ← getMainState
+    let state ← get
-    let levelNames := (args.levels?.getD #[]).toList.map (·.toName)
+    exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
-    liftExcept $ ← liftTermElabM (levelNames := levelNames) do
+  options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
-      (exprEcho args.expr (expectedType? := args.type?) (options := state.options)).run
+    let state ← get
-  options_set (args: Protocol.OptionsSet): EMainM Protocol.OptionsSetResult := do
-    let state ← getMainState
     let options := state.options
     set { state with
       options := {
@@ -271,35 +202,33 @@ def execute (command: Protocol.Command): MainM Json := do
         printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
         printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
         automaticMode := args.automaticMode?.getD options.automaticMode,
-        timeout := args.timeout?.getD options.timeout,
       }
     }
-    return {  }
+    return .ok {  }
-  options_print (_: Protocol.OptionsPrint): EMainM Protocol.Options := do
+  options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do
-    return (← getMainState).options
+    return .ok (← get).options
-  goal_start (args: Protocol.GoalStart): EMainM Protocol.GoalStartResult := do
+  goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
-    let levelNames := (args.levels?.getD #[]).toList.map (·.toName)
+    let env ← MonadEnv.getEnv
-    let expr?: Except _ GoalState ← liftTermElabM (levelNames := levelNames) do
+    let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with
-      match args.expr, args.copyFrom with
+      | .some expr, .none => goalStartExpr expr (args.levels.getD #[])
-      | .some expr, .none => goalStartExpr expr |>.run
+      | .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))
       | _, _ =>
-        return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied"
+        return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
     match expr? with
-    | .error error => Protocol.throw error
+    | .error error => return .error error
     | .ok goalState =>
       let stateId ← newGoalState goalState
-      return { stateId, root := goalState.root.name.toString }
+      return .ok { stateId, root := goalState.root.name.toString }
-  goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult := do
+  goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
-    let state ← getMainState
+    let state ← get
     let .some goalState := state.goalStates[args.stateId]? |
-      Protocol.throw $ errorIndex s!"Invalid state index {args.stateId}"
+      return .error $ errorIndex s!"Invalid state index {args.stateId}"
-    let .some goal := goalState.goals[args.goalId]? |
+    let .some goal := goalState.goals.get? args.goalId |
-      Protocol.throw $ errorIndex s!"Invalid goal index {args.goalId}"
+      return .error $ errorIndex s!"Invalid goal index {args.goalId}"
-    let nextGoalState?: Except _ TacticResult ← liftTermElabM do
+    let nextGoalState?: Except _ TacticResult ← runTermElabInMainM 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
@@ -321,88 +250,88 @@ 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, let, calc, conv, draft} must be supplied"
+        let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied"
-        pure $ .error error
+        pure $ Except.error $ error
     match nextGoalState? with
-    | .error error => Protocol.throw error
+    | .error error => return .error error
-    | .ok (.success nextGoalState messages) => do
+    | .ok (.success nextGoalState) => do
       let nextGoalState ← match state.options.automaticMode, args.conv? with
         | true, .none => do
-          pure $ nextGoalState.immediateResume goalState
+          let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) |
+            throwError "Resuming known goals"
+          pure result
         | true, .some true => pure nextGoalState
         | true, .some false => do
           let .some (_, _, dormantGoals) := goalState.convMVar? |
-            Protocol.throw $ errorIO "If conv exit succeeded this should not fail"
+            throwError "If conv exit succeeded this should not fail"
           let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) |
-            Protocol.throw $ errorIO "Resuming known goals"
+            throwError "Resuming known goals"
           pure result
         | false, _ => pure nextGoalState
       let nextStateId ← newGoalState nextGoalState
-      let parentExpr := nextGoalState.parentExpr?.get!
+      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 {
-      return {
         nextStateId? := .some nextStateId,
         goals? := .some goals,
-        messages? := .some messages,
-        hasSorry := parentExpr.hasSorry,
-        hasUnsafe := (← getEnv).hasUnsafe parentExpr,
       }
     | .ok (.parseError message) =>
-      return { messages? := .none, parseError? := .some message }
+      return .ok { parseError? := .some message }
     | .ok (.invalidAction message) =>
-      Protocol.throw $ errorI "invalid" message
+      return .error $ errorI "invalid" message
     | .ok (.failure messages) =>
-      return { messages? := .some messages }
+      return .ok { tacticErrors? := .some messages }
-  goal_continue (args: Protocol.GoalContinue): EMainM Protocol.GoalContinueResult := do
+  goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
-    let state ← getMainState
+    let state ← get
     let .some target := state.goalStates[args.target]? |
-      Protocol.throw $ errorIndex s!"Invalid state index {args.target}"
+      return .error $ errorIndex s!"Invalid state index {args.target}"
-    let nextGoalState? : GoalState  ← match args.branch?, args.goals? with
+    let nextState? ← match args.branch?, args.goals? with
       | .some branchId, .none => do
         match state.goalStates[branchId]? with
-        | .none => Protocol.throw $ errorIndex s!"Invalid state index {branchId}"
+        | .none => return .error $ errorIndex s!"Invalid state index {branchId}"
         | .some branch => pure $ target.continue branch
       | .none, .some goals =>
-        let goals := goals.toList.map (λ n => { name := n.toName })
+        pure $ goalResume target goals
-        pure $ target.resume goals
+      | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
-      | _, _ => Protocol.throw $ errorI "arguments" "Exactly one of {branch, goals} must be supplied"
+    match nextState? with
-    match nextGoalState? with
+    | .error error => return .error <| errorI "structure" error
-    | .error error => Protocol.throw $ errorI "structure" error
     | .ok nextGoalState =>
       let nextStateId ← newGoalState nextGoalState
-      let goals ← liftMetaM $ goalSerialize nextGoalState (options := state.options)
+      let goals ← goalSerialize nextGoalState (options := state.options)
-      return {
+      return .ok {
         nextStateId,
         goals,
       }
-  goal_delete (args: Protocol.GoalDelete): EMainM Protocol.GoalDeleteResult := do
+  goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
-    let state ← getMainState
+    let state ← get
     let goalStates := args.stateIds.foldl (λ map id => map.erase id) state.goalStates
     set { state with goalStates }
-    return {}
+    return .ok {}
-  goal_print (args: Protocol.GoalPrint): EMainM Protocol.GoalPrintResult := do
+  goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
-    let state ← getMainState
+    let state ← get
     let .some goalState := state.goalStates[args.stateId]? |
-      Protocol.throw $ errorIndex s!"Invalid state index {args.stateId}"
+      return .error $ errorIndex s!"Invalid state index {args.stateId}"
-    let result ← liftMetaM <| goalPrint
+    let result ← runMetaInMainM <| goalPrint
         goalState
         (rootExpr := args.rootExpr?.getD False)
         (parentExpr := args.parentExpr?.getD False)
         (goals := args.goals?.getD False)
         (extraMVars := args.extraMVars?.getD #[])
         (options := state.options)
-    return result
+    return .ok result
-  goal_save (args: Protocol.GoalSave): EMainM Protocol.GoalSaveResult := do
+  goal_save (args: Protocol.GoalSave): MainM (CR Protocol.GoalSaveResult) := do
-    let state ← getMainState
+    let state ← get
     let .some goalState := state.goalStates[args.id]? |
-      Protocol.throw $ errorIndex s!"Invalid state index {args.id}"
+      return .error $ errorIndex s!"Invalid state index {args.id}"
     goalStatePickle goalState args.path
-    return {}
+    return .ok {}
-  goal_load (args: Protocol.GoalLoad): EMainM Protocol.GoalLoadResult := do
+  goal_load (args: Protocol.GoalLoad): MainM (CR Protocol.GoalLoadResult) := do
     let (goalState, _) ← goalStateUnpickle args.path (← MonadEnv.getEnv)
     let id ← newGoalState goalState
-    return { id }
+    return .ok { id }
-  frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
+  frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
+    try
       frontend_process_inner args
+    catch e =>
+      return .error $ errorI "frontend" (← e.toMessageData.toString)
 
 end Pantograph.Repl

Test/Common.lean

@@ -67,11 +67,11 @@ protected def Goal.devolatilize (goal: Goal): Goal :=
 
 end Condensed
 
-def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals[i]!
+def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals.get! i
-def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.get! goalId) tactic
+def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.goals.get! goalId) tactic
 
 def TacticResult.toString : TacticResult → String
-  | .success state _messages => s!".success ({state.goals.length} goals)"
+  | .success state => s!".success ({state.goals.length} goals)"
   | .failure messages =>
     let messages := "\n".intercalate messages.toList
     s!".failure {messages}"
@@ -108,7 +108,7 @@ def strToTermSyntax (s: String): CoreM Syntax := do
     (input := s)
     (fileName := ← getFileName) | panic! s!"Failed to parse {s}"
   return stx
-def parseSentence (s : String) (expectedType? : Option Expr := .none) : Elab.TermElabM Expr := do
+def parseSentence (s: String): Elab.TermElabM Expr := do
   let stx ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := `term)
@@ -116,7 +116,7 @@ def parseSentence (s : String) (expectedType? : Option Expr := .none) : Elab.Ter
     (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => throwError "Failed to parse: {error}"
-  Elab.Term.elabTerm (stx := stx) expectedType?
+  Elab.Term.elabTerm (stx := stx) .none
 
 def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do
     let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }

Test/Delate.lean

@@ -3,10 +3,11 @@ import Pantograph.Delate
 import Test.Common
 import Lean
 
-open Lean Pantograph
+open Lean
-
 namespace Pantograph.Test.Delate
 
+open Pantograph
+
 deriving instance Repr, DecidableEq for Protocol.BoundExpression
 
 def test_serializeName: LSpec.TestSeq :=
@@ -112,13 +113,6 @@ def test_projection_exists (env: Environment) : IO LSpec.TestSeq:= runTest do
   checkEq "numParams" numParams 2
   checkEq "numFields" numFields 2
 
-def test_matcher : TestT Elab.TermElabM Unit := do
-  let t ← parseSentence "Nat → Nat"
-  let e ← parseSentence "fun (n : Nat) => match n with | 0 => 0 | k => k" (.some t)
-  let .some _ ← Meta.matchMatcherApp? e.bindingBody! | fail "Must be a matcher app"
-  let e' ← instantiateAll e
-  checkTrue "ok" <| ← Meta.isTypeCorrect e'
-
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
     ("serializeName", do pure test_serializeName),
@@ -129,7 +123,6 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("Instance", test_instance env),
     ("Projection Prod", test_projection_prod env),
     ("Projection Exists", test_projection_exists env),
-    ("Matcher", runTestTermElabM env test_matcher),
   ]
 
 end Pantograph.Test.Delate

Test/Environment.lean

@@ -103,31 +103,23 @@ def test_symbol_location : TestT IO Unit := do
     (opts := {})
     (trustLevel := 1)
   addTest $ ← runTestCoreM env do
-    let .ok result ← (Environment.inspect { name := "Nat.le_of_succ_le", source? := .some true } (options := {})).run | fail "Inspect failed"
+    let .ok result ← Environment.inspect { name := "Nat.le_of_succ_le", source? := .some true } (options := {}) | fail "Inspect failed"
     checkEq "module" result.module? <| .some "Init.Data.Nat.Basic"
 
     -- Extraction of source doesn't work for symbols in `Init` for some reason
     checkTrue "file" result.sourceUri?.isNone
     checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0
     checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88
-    let { imports, constNames, .. } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩
+    let .ok { imports, constNames, .. } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩ | fail "Module read failed"
     checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"]
     checkTrue "constNames" $ constNames.contains "Nat.succ_add"
 
-def test_matcher : TestT IO Unit := do
-  let env: Environment ← importModules
-    (imports := #[`Init])
-    (opts := {})
-    (trustLevel := 1)
-  checkTrue "not matcher" $ ¬ Meta.isMatcherCore env `Nat.strongRecOn
-
 def suite: List (String × IO LSpec.TestSeq) :=
   [
     ("Catalog", test_catalog),
     ("Symbol Visibility", test_symbol_visibility),
     ("Inspect", test_inspect),
     ("Symbol Location", runTest test_symbol_location),
-    ("Matcher", runTest test_matcher),
   ]
 
 end Pantograph.Test.Environment

Test/Frontend.lean

@@ -1,28 +1,11 @@
+import LSpec
 import Pantograph
 import Repl
 import Test.Common
 
-import LSpec
-
 open Lean Pantograph
 namespace Pantograph.Test.Frontend
 
-def runFrontend { α } (source: String) (f : Frontend.CompilationStep → IO α) : MetaM (List α) := do
-  let filename := "<anonymous>"
-  let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
-  let m := Frontend.mapCompilationSteps f
-  m.run context |>.run' state
-
-def test_open : TestT MetaM Unit := do
-  let sketch := "
-open Nat
-example : ∀ (n : Nat), n + 1 = Nat.succ n := by
-  intro
-  apply add_one
-  "
-  let errors ← runFrontend sketch λ step => step.msgs.mapM (·.toString)
-  checkEq "errors" errors [[], []]
-
 def collectSorrysFromSource (source: String) (options : Frontend.GoalCollectionOptions := {})
     : MetaM (List GoalState) := do
   let filename := "<anonymous>"
@@ -250,7 +233,6 @@ theorem mystery [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get
 
 def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
-    ("open", test_open),
     ("multiple_sorrys_in_proof", test_multiple_sorrys_in_proof),
     ("sorry_in_middle", test_sorry_in_middle),
     ("sorry_in_induction", test_sorry_in_induction),

Test/Integration.lean

@@ -8,33 +8,23 @@ import Test.Common
 namespace Pantograph.Test.Integration
 open Pantograph.Repl
 
-deriving instance Lean.ToJson for Protocol.EnvInspect
+def step { α } [Lean.ToJson α] (cmd: String) (payload: List (String × Lean.Json))
-deriving instance Lean.ToJson for Protocol.EnvAdd
+    (expected: α) (name? : Option String := .none): MainM LSpec.TestSeq := do
-deriving instance Lean.ToJson for Protocol.ExprEcho
+  let payload := Lean.Json.mkObj payload
-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 (result.pretty = (Lean.toJson expected).pretty)
+  return LSpec.test name (toString result = toString (Lean.toJson expected))
 
 abbrev Test := List (MainM LSpec.TestSeq)
 
-def test_expr_echo : Test :=
+def test_elab : Test :=
   [
     step "expr.echo"
-     ({ expr := "λ {α : Sort (u + 1)} => List α", levels? := .some #["u"]}: Protocol.ExprEcho)
+      [("expr", .str "λ {α : Sort (u + 1)} => List α"), ("levels", .arr #["u"])]
-     ({
+     (Lean.toJson ({
        type := { pp? := .some "{α : Type u} → Type u" },
        expr := { pp? := .some "fun {α} => List α" }
-     }: Protocol.ExprEchoResult),
+     }: Protocol.ExprEchoResult)),
   ]
 
 def test_option_modify : Test :=
@@ -43,77 +33,50 @@ def test_option_modify : Test :=
   let module? := Option.some "Init.Data.Nat.Basic"
   let options: Protocol.Options := {}
   [
-    step "env.inspect" ({ name := "Nat.add_one" } : Protocol.EnvInspect)
+    step "env.inspect" [("name", .str "Nat.add_one")]
      ({ type := { pp? }, module? }: Protocol.EnvInspectResult),
-    step "options.set" ({ printExprAST? := .some true } : Protocol.OptionsSet)
+    step "options.set" [("printExprAST", .bool true)]
      ({ }: Protocol.OptionsSetResult),
-    step "env.inspect" ({ name := "Nat.add_one" } : Protocol.EnvInspect)
+    step "env.inspect" [("name", .str "Nat.add_one")]
      ({ type := { pp?, sexp? }, module? }: Protocol.EnvInspectResult),
-    step "options.print" ({} : Protocol.OptionsPrint)
+    step "options.print" []
      ({ options with printExprAST := true }: Protocol.Options),
   ]
 def test_malformed_command : Test :=
   let invalid := "invalid"
   [
-    step invalid ({ name := "Nat.add_one" }: Protocol.EnvInspect)
+    step invalid [("name", .str "Nat.add_one")]
      ({ error := "command", desc := s!"Unknown command {invalid}" }: Protocol.InteractionError)
      (name? := .some "Invalid Command"),
-    step "expr.echo" (Lean.Json.mkObj [(invalid, .str "Random garbage data")])
+    step "expr.echo" [(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 := #[varX],
+    vars := #[{ name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }}],
   }
   let goal2: Protocol.Goal := {
-    name := "_uniq.14",
+    name := "_uniq.17",
     target := { pp? := .some "x ∨ y → y ∨ x" },
     vars := #[
-      varX,
+      { name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }},
-      { name := "_uniq.13", userName := "y", type? := .some { pp? := .some "Prop" }}
+      { name := "_uniq.16", userName := "y", type? := .some { pp? := .some "Prop" }}
     ],
   }
   [
-    step "goal.start" ({ expr := "∀ (p q: Prop), p ∨ q → q ∨ p" }: Protocol.GoalStart)
+    step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
      ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
-    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro x" }: Protocol.GoalTactic)
+    step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
-    step "goal.print" ({ stateId := 1, parentExpr? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
+    step "goal.print" [("stateId", .num 1), ("parentExpr", .bool true), ("rootExpr", .bool true)]
-     ({
+     ({ parent? := .some { pp? := .some "fun x => ?m.11" }, }: Protocol.GoalPrintResult),
-       root? := .some { pp? := "fun x => ?m.11"},
+    step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
-       parent? := .some { pp? := .some "fun x => ?m.11" },
-     }: Protocol.GoalPrintResult),
-    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)
-     ({ messages? := .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),
-    step "goal.tactic" ({ stateId := 0, tactic? := .some "sorry" }: Protocol.GoalTactic)
-     ({ nextStateId? := .some 3, goals? := .some #[], hasSorry := true }: Protocol.GoalTacticResult),
   ]
-example : (1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3 := by
-  simp
-def test_tactic_timeout : Test :=
-  [
-    step "goal.start" ({ expr := "(1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3" }: Protocol.GoalStart)
-     ({ stateId := 0, root := "_uniq.319" }: Protocol.GoalStartResult),
-    -- timeout of 10 milliseconds
-    step "options.set" ({ timeout? := .some 10 } : Protocol.OptionsSet)
-     ({ }: Protocol.OptionsSetResult),
-    step "goal.tactic" ({ stateId := 0, expr? := .some "by\nsleep 1000; simp" }: Protocol.GoalTactic)
-     ({ error := "internal", desc := "interrupt" }: Protocol.InteractionError),
-    -- ensure graceful recovery
-    step "options.set" ({ timeout? := .some 0 } : Protocol.OptionsSet)
-     ({ }: Protocol.OptionsSetResult),
-    step "goal.tactic" ({ stateId := 0, tactic? := .some "simp" }: Protocol.GoalTactic)
-     ({ nextStateId? := .some 1, goals? := .some #[], }: Protocol.GoalTacticResult),
-  ]
-
 def test_automatic_mode (automatic: Bool): Test :=
   let varsPQ := #[
     { name := "_uniq.10", userName := "p", type? := .some { pp? := .some "Prop" }},
@@ -151,65 +114,51 @@ def test_automatic_mode (automatic: Bool): Test :=
     ],
   }
   [
-    step "options.set" ({automaticMode? := .some automatic}: Protocol.OptionsSet)
+    step "options.set" [("automaticMode", .bool automatic)]
      ({}: Protocol.OptionsSetResult),
-    step "goal.start" ({ expr := "∀ (p q: Prop), p ∨ q → q ∨ p"} : Protocol.GoalStart)
+    step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
      ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
-    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro p q h" }: Protocol.GoalTactic)
+    step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro p q h")]
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
-    step "goal.tactic" ({ stateId := 1, tactic? := .some "cases h" }: Protocol.GoalTactic)
+    step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "cases h")]
      ({ nextStateId? := .some 2, goals? := #[goal2l, goal2r], }: Protocol.GoalTacticResult),
     let goals? := if automatic then #[goal3l, goal2r] else #[goal3l]
-    step "goal.tactic" ({ stateId := 2, tactic? := .some "apply Or.inr" }: Protocol.GoalTactic)
+    step "goal.tactic" [("stateId", .num 2), ("goalId", .num 0), ("tactic", .str "apply Or.inr")]
      ({ nextStateId? := .some 3, goals?, }: Protocol.GoalTacticResult),
   ]
 
 def test_env_add_inspect : Test :=
   let name1 := "Pantograph.mystery"
   let name2 := "Pantograph.mystery2"
-  let name3 := "Pantograph.mystery3"
   [
     step "env.add"
-      ({
+      [
-        name := name1,
+        ("name", .str name1),
-        value := "λ (a b: Prop) => Or a b",
+        ("type", .str "Prop → Prop → Prop"),
-        isTheorem := false
+        ("value", .str "λ (a b: Prop) => Or a b"),
-      }: Protocol.EnvAdd)
+        ("isTheorem", .bool false)
+      ]
      ({}: Protocol.EnvAddResult),
-    step "env.inspect" ({name := name1, value? := .some true} : Protocol.EnvInspect)
+    step "env.inspect" [("name", .str name1)]
      ({
        value? := .some { pp? := .some "fun a b => a ∨ b" },
        type := { pp? := .some "Prop → Prop → Prop" },
      }:
       Protocol.EnvInspectResult),
     step "env.add"
-      ({
+      [
-        name := name2,
+        ("name", .str name2),
-        type? := "Nat → Int",
+        ("type", .str "Nat → Int"),
-        value := "λ (a: Nat) => a + 1",
+        ("value", .str "λ (a: Nat) => a + 1"),
-        isTheorem := false
+        ("isTheorem", .bool false)
-      }: Protocol.EnvAdd)
+      ]
      ({}: Protocol.EnvAddResult),
-    step "env.inspect" ({name := name2, value? := .some true} : Protocol.EnvInspect)
+    step "env.inspect" [("name", .str name2)]
      ({
        value? := .some { pp? := .some "fun a => ↑a + 1" },
        type := { pp? := .some "Nat → Int" },
      }:
-      Protocol.EnvInspectResult),
+      Protocol.EnvInspectResult)
-    step "env.add"
-      ({
-        name := name3,
-        levels? := .some #["u"]
-        type? := "(α : Type u) → α → (α × α)",
-        value := "λ (α : Type u) (x : α) => (x, x)",
-        isTheorem := false
-      }: Protocol.EnvAdd)
-     ({}: Protocol.EnvAddResult),
-    step "env.inspect" ({name := name3} : Protocol.EnvInspect)
-     ({
-       type := { pp? := .some "(α : Type u) → α → α × α" },
-     }:
-      Protocol.EnvInspectResult),
   ]
 
 example : ∀ (p: Prop), p → p := by
@@ -217,14 +166,17 @@ 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"
-  [
     step "frontend.process"
-      ({
+      [
-        file? := .some file,
+        ("file",              .str file),
-        invocations := true,
+        ("invocations",       .bool true),
-      }: Protocol.FrontendProcess)
+        ("sorrys",            .bool false),
+        ("typeErrorsAsGoals", .bool false),
+        ("newConstants",      .bool false),
+      ]
      ({
        units := [{
          boundary := (0, file.utf8ByteSize),
@@ -260,10 +212,13 @@ def test_frontend_process_sorry : Test :=
       vars := #[{ name := "_uniq.4", userName := "p", type? := .some { pp? := .some "Prop" }}],
     }
     step "frontend.process"
-      ({
+      [
-        file? := .some file,
+        ("file", .str file),
-        sorrys := true,
+        ("invocations", .bool false),
-      }: Protocol.FrontendProcess)
+        ("sorrys", .bool true),
+        ("typeErrorsAsGoals", .bool false),
+        ("newConstants", .bool false),
+      ]
      ({
        units := [{
          boundary := (0, solved.utf8ByteSize),
@@ -277,85 +232,28 @@ def test_frontend_process_sorry : Test :=
     }: Protocol.FrontendProcessResult),
   ]
 
-def test_import_open : Test :=
-  let header := "import Init\nopen Nat\nuniverse u"
-  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, 21) },
-         { boundary := (21, 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),
-    step "goal.start" ({ expr := "∀ (x : Sort u), Sort (u + 1)"} : Protocol.GoalStart)
-     ({ stateId := 3, root := "_uniq.5" }: Protocol.GoalStartResult),
-  ]
-
-/-- Ensure there cannot be circular references -/
-def test_frontend_process_circular : Test :=
-  let withSorry := "theorem mystery : 1 + 2 = 2 + 3 := sorry"
-  [
-    let goal1: Protocol.Goal := {
-      name := "_uniq.2",
-      target := { pp? := .some "1 + 2 = 2 + 3" },
-      vars := #[],
-    }
-    step "frontend.process"
-      ({
-        file? := .some withSorry,
-        sorrys := true,
-      }: Protocol.FrontendProcess)
-     ({
-       units := [{
-         boundary := (0, withSorry.utf8ByteSize),
-         goalStateId? := .some 0,
-         goals? := .some #[goal1],
-         goalSrcBoundaries? := .some #[(35, 40)],
-         messages := #["<anonymous>:1:8: warning: declaration uses 'sorry'\n"],
-       }],
-     }: Protocol.FrontendProcessResult),
-    step "goal.tactic" ({ stateId := 0, tactic? := .some "exact?" }: Protocol.GoalTactic)
-     ({ messages? := .some #["`exact?` could not close the goal. Try `apply?` to see partial suggestions."] }
-     : Protocol.GoalTacticResult),
-  ]
 
 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
   -- Setup the environment for execution
-  let coreContext ← createCoreContext #[]
+  let context: Context := {}
-  let mainM : MainM LSpec.TestSeq :=
+  let commands: MainM LSpec.TestSeq :=
-    steps.foldlM (λ suite step => do return suite ++ (← step)) LSpec.TestSeq.done
+    steps.foldlM (λ suite step => do
-  mainM.run { coreContext } |>.run' { env }
+      let result ← step
+      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_expr_echo),
+    ("expr.echo", test_elab),
     ("options.set options.print", test_option_modify),
     ("Malformed command", test_malformed_command),
     ("Tactic", test_tactic),
-    ("Tactic Timeout", test_tactic_timeout),
     ("Manual Mode", test_automatic_mode false),
     ("Automatic Mode", test_automatic_mode true),
     ("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),
-    ("frontend.process circular", test_frontend_process_circular),
   ]
   tests.map (fun (name, test) => (name, runTest env test))
 

Test/Library.lean

@@ -8,18 +8,15 @@ 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 ← runTermElabM $ exprEcho prop_and_proof (options := {})
+    let echoResult ← 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 ← runTermElabM $ exprEcho prop_and_proof (expectedType? := .some "Σ' p:Prop, p") (options := { printExprAST := true })
+    let echoResult ← 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",

Test/Main.lean

@@ -17,9 +17,9 @@ def addPrefix (pref: String) (tests: List (String × α)): List (String  × α)
   tests.map (λ (name, x) => (pref ++ "/" ++ name, x))
 
 /-- Runs test in parallel. Filters test name if given -/
-def runTestGroup (nameFilter?: Option String) (tests: List (String × IO LSpec.TestSeq)): IO LSpec.TestSeq := do
+def runTestGroup (filter: Option String) (tests: List (String × IO LSpec.TestSeq)): IO LSpec.TestSeq := do
-  let tests: List (String × IO LSpec.TestSeq) := match nameFilter? with
+  let tests: List (String × IO LSpec.TestSeq) := match filter with
-    | .some nameFilter => tests.filter (λ (name, _) => nameFilter.isPrefixOf name)
+    | .some filter => tests.filter (λ (name, _) => filter.isPrefixOf name)
     | .none => tests
   let tasks: List (String × Task _) ← tests.mapM (λ (name, task) => do
     return (name, ← EIO.asTask task))
@@ -37,7 +37,7 @@ open Pantograph.Test
 
 /-- Main entry of tests; Provide an argument to filter tests by prefix -/
 def main (args: List String) := do
-  let nameFilter? := args.head?
+  let name_filter := args.head?
   Lean.initSearchPath (← Lean.findSysroot)
   let env_default: Lean.Environment ← Lean.importModules
     (imports := #[`Init])
@@ -54,8 +54,10 @@ def main (args: List String) := do
     ("Delate", Delate.suite env_default),
     ("Serial", Serial.suite env_default),
     ("Tactic/Assign", Tactic.Assign.suite env_default),
+    ("Tactic/Congruence", Tactic.Congruence.suite env_default),
+    ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
+    ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),
     ("Tactic/Prograde", Tactic.Prograde.suite env_default),
-    ("Tactic/Special", Tactic.Special.suite env_default),
   ]
   let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
-  LSpec.lspecEachIO [()] (λ () => runTestGroup nameFilter? tests)
+  LSpec.lspecIO (← runTestGroup name_filter tests)

Test/Metavar.lean

@@ -79,20 +79,20 @@ def test_m_couple: TestM Unit := do
       return ()
 
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
-  checkTrue "(1 root)" $ ¬ state1.isSolved
+  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
   -- Set m to 3
   let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 3") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  checkTrue "(1b root)" $ ¬ state2.isSolved
+  addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
   let state1b ← match state2.continue state1 with
     | .error msg => do
       addTest $ assertUnreachable $ msg
@@ -100,7 +100,7 @@ def test_m_couple: TestM Unit := do
     | .ok state => pure state
   addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ 3", .some "3 ≤ 5"])
-  checkTrue "(2 root)" $ ¬ state1b.isSolved
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
 
 def test_m_couple_simp: TestM Unit := do
   let state? ← startProof "(2: Nat) ≤ 5"
@@ -111,7 +111,7 @@ def test_m_couple_simp: TestM Unit := do
       return ()
 
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -122,11 +122,11 @@ def test_m_couple_simp: TestM Unit := do
     #[#["_uniq.38"], #["_uniq.38"], #[]])
 
   let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 2") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  checkTrue "(1b root)" $ ¬ state2.isSolved
+  addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
   let state1b ← match state2.continue state1 with
     | .error msg => do
       addTest $ assertUnreachable $ msg
@@ -134,9 +134,9 @@ def test_m_couple_simp: TestM Unit := do
     | .ok state => pure state
   addTest $ LSpec.check "exact 2" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ 2", .some "2 ≤ 5"])
-  checkTrue "(2 root)" $ ¬ state1b.isSolved
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
   let state3 ← match ← state1b.tacticOn (goalId := 0) (tactic := "simp") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -146,7 +146,7 @@ def test_m_couple_simp: TestM Unit := do
       return ()
     | .ok state => pure state
   let state5 ← match ← state4.tacticOn (goalId := 0) (tactic := "simp") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -173,7 +173,7 @@ def test_proposition_generation: TestM Unit := do
       return ()
 
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply PSigma.mk") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -184,27 +184,27 @@ def test_proposition_generation: TestM Unit := do
       ])
   if let #[goal1, goal2] := ← state1.serializeGoals (options := { (← read) with printExprAST := true }) then
     addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})")
-  checkTrue "(1 root)" $ ¬ state1.isSolved
+  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
 
   let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := "λ (x: Nat) => _") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "?m.30 x"])
+    #[.some "?m.29 x"])
-  checkTrue "(2 root)" $ ¬ state2.isSolved
+  addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
 
   let assign := "Eq.refl x"
   let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := assign) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check s!":= {assign}" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[])
 
-  checkTrue "(3 root)" state3.isSolved
+  addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome
   return ()
 
 def test_partial_continuation: TestM Unit := do
@@ -216,7 +216,7 @@ def test_partial_continuation: TestM Unit := do
       return ()
 
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -224,7 +224,7 @@ def test_partial_continuation: TestM Unit := do
     #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
 
   let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "apply Nat.succ") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -238,23 +238,23 @@ def test_partial_continuation: TestM Unit := do
       addTest $ assertUnreachable $ msg
       return ()
     | .ok state => pure state
-  addTest $ LSpec.check "(continue 1)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
-  checkTrue "(2 root)" state1b.rootExpr?.get!.hasExprMVar
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
 
   -- Roundtrip
   --let coupled_goals := coupled_goals.map (λ g =>
   --  { name := str_to_name $ serializeName g.name (sanitize := false)})
-  let coupled_goals := coupled_goals.map (·.name.toString)
+  let coupled_goals := coupled_goals.map (λ g => serializeName g.name (sanitize := false))
-  let coupled_goals := coupled_goals.map ({ name := ·.toName })
+  let coupled_goals := coupled_goals.map (λ g => { name := g.toName })
   let state1b ← match state2.resume (goals := coupled_goals) with
     | .error msg => do
       addTest $ assertUnreachable $ msg
       return ()
     | .ok state => pure state
-  addTest $ LSpec.check "(continue 2)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
-  checkTrue "(2 root)" state1b.rootExpr?.get!.hasExprMVar
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
 
   -- Continuation should fail if the state does not exist:
   match state0.resume coupled_goals with

Test/Proofs.lean

@@ -89,7 +89,7 @@ def test_identity: TestM Unit := do
 
   let tactic := "intro p h"
   let state1 ← match ← state0.tacticOn 0 tactic with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -116,7 +116,7 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
       return ()
 
   let state1 ← match ← state0.tacticOn 0 "intro n m" with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -130,7 +130,7 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
     addTest $ assertUnreachable $ other.toString
 
   let state2 ← match ← state1.tacticOn 0 "rw [Nat.add_comm]" with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -148,14 +148,14 @@ def test_delta_variable: TestM Unit := do
       return ()
 
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "intro n") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "intro n" ((← state1.serializeGoals (parent := state0) options).map (·.devolatilize) =
     #[buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"])
   let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "intro m") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -187,27 +187,27 @@ def test_arith: TestM Unit := do
 
   let tactic := "intros"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check tactic (state1.goals.length = 1)
-  checkTrue "(1 root)" state1.rootExpr?.get!.hasExprMVar
+  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
   let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "simp ..." (state2.goals.length = 1)
-  checkTrue "(2 root)" state2.rootExpr?.get!.hasExprMVar
+  addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
   let tactic := "assumption"
   let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.test tactic state3.goals.isEmpty
-  checkTrue "(3 root)" $ ¬ state3.rootExpr?.get!.hasExprMVar
+  addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
   return ()
 
 -- Two ways to write the same theorem
@@ -237,7 +237,7 @@ def test_or_comm: TestM Unit := do
 
   let tactic := "intro p q h"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -257,15 +257,15 @@ def test_or_comm: TestM Unit := do
         { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" } }
       ]
     }])
-  checkTrue "(1 parent)" state1.parentExpr?.isSome
+  addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
-  checkTrue "(1 root)" $ ¬ state1.isSolved
+  addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
 
   let state1parent ← state1.withParentContext do
     serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
   addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) 2 1 0))))")
   let tactic := "cases h"
   let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -276,8 +276,8 @@ def test_or_comm: TestM Unit := do
   let (caseL, caseR) := (state2g0.name.toString, state2g1.name.toString)
   addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
     #[caseL, caseR])
-  checkTrue "(2 parent exists)" state2.parentExpr?.isSome
+  addTest $ LSpec.check "(2 parent exists)" state2.parentExpr?.isSome
-  checkTrue "(2 root)" $ ¬ state2.isSolved
+  addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
 
   let state2parent ← state2.withParentContext do
     serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!)
@@ -291,7 +291,7 @@ def test_or_comm: TestM Unit := do
     s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})")
 
   let state3_1 ← match ← state2.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -301,47 +301,47 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv {state3_1goal0}))")
   addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
   let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
   let state4_1parent ← instantiateAll state4_1.parentExpr?.get!
   addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
-  checkTrue "(4_1 root)" $ ¬ state4_1.isSolved
+  addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
   let state3_2 ← match ← state2.tacticOn (goalId := 1) (tactic := "apply Or.inl") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "· apply Or.inl" (state3_2.goals.length = 1)
   let state4_2 ← match ← state3_2.tacticOn (goalId := 0) (tactic := "assumption") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "  assumption" state4_2.goals.isEmpty
-  checkTrue "(4_2 root)" $ ¬ state4_2.isSolved
+  addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr?.isNone
   -- Ensure the proof can continue from `state4_2`.
   let state2b ← match state4_2.continue state2 with
     | .error msg => do
       addTest $ assertUnreachable $ msg
       return ()
     | .ok state => pure state
-  addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals[0]!])
+  addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals.get! 0])
   let state3_1 ← match ← state2b.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
   let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
-  checkTrue "(4_1 root)" $ ¬ state4_1.rootExpr?.get!.hasExprMVar
+  addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isSome
 
   return ()
   where
@@ -375,7 +375,7 @@ def test_conv: TestM Unit := do
 
   let tactic := "intro a b c1 c2 h"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -383,7 +383,7 @@ def test_conv: TestM Unit := do
     #[interiorGoal [] "a + b + c1 = b + a + c2"])
 
   let state2 ← match ← state1.conv (state1.get! 0) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -392,7 +392,7 @@ def test_conv: TestM Unit := do
 
   let convTactic := "rhs"
   let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -401,7 +401,7 @@ def test_conv: TestM Unit := do
 
   let convTactic := "lhs"
   let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -410,7 +410,7 @@ def test_conv: TestM Unit := do
 
   let convTactic := "congr"
   let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -422,7 +422,7 @@ def test_conv: TestM Unit := do
 
   let convTactic := "rw [Nat.add_comm]"
   let state5_1 ← match ← state4.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -431,7 +431,7 @@ def test_conv: TestM Unit := do
 
   let convTactic := "rfl"
   let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -446,7 +446,7 @@ def test_conv: TestM Unit := do
 
   let convTactic := "rfl"
   let state6 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -454,14 +454,14 @@ def test_conv: TestM Unit := do
     #[])
 
   let state1_1 ← match ← state6.convExit with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
 
   let tactic := "exact h"
   let stateF ← match ← state1_1.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -488,7 +488,7 @@ def test_calc: TestM Unit := do
       return ()
   let tactic := "intro a b c d h1 h2"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -496,7 +496,7 @@ def test_calc: TestM Unit := do
     #[interiorGoal [] "a + b = c + d"])
   let pred := "a + b = b + c"
   let state2 ← match ← state1.tryCalc (state1.get! 0) (pred := pred) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -510,7 +510,7 @@ def test_calc: TestM Unit := do
 
   let tactic := "apply h1"
   let state2m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -521,7 +521,7 @@ def test_calc: TestM Unit := do
       return ()
   let pred := "_ = c + d"
   let state4 ← match ← state3.tryCalc (state3.get! 0) (pred := pred) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -532,7 +532,7 @@ def test_calc: TestM Unit := do
   addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? (state4.get! 0) |>.isNone)
   let tactic := "apply h2"
   let state4m ← match ← state4.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -543,6 +543,179 @@ def test_calc: TestM Unit := do
         ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
       buildGoal free target userName?
 
+def test_nat_zero_add: TestM Unit := do
+  let state? ← startProof (.expr "∀ (n: Nat), n + 0 = n")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+  let tactic := "intro n"
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[buildGoal [("n", "Nat")] "n + 0 = n"])
+  let recursor := "@Nat.brecOn"
+  let state2 ← match ← state1.tryMotivatedApply (state1.get! 0) (recursor := recursor) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let [mvarMotive, mvarMajor, mvarInduct, mvarConduit] := state2.goals |
+      fail "Incorrect number of goals"
+  let .num _ major := mvarMajor.name | fail "Incorrect form of mvar id"
+  addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
+    #[
+      buildNamedGoal mvarMotive.name.toString  [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal mvarMajor.name.toString   [("n", "Nat")] "Nat",
+      buildNamedGoal mvarInduct.name.toString  [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal mvarConduit.name.toString [("n", "Nat")] s!"?motive ?m.{major} = (n + 0 = n)" (.some "conduit")
+    ])
+
+  let tactic := "exact n"
+  let state3b ← match ← state2.tacticOn (goalId := 1) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state3b.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[])
+  let state2b ← match state3b.continue state2 with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let tactic := "exact (λ x => x + 0 = x)"
+  let state3c ← match ← state2b.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state3c.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[])
+  let state2c ← match state3c.continue state2b with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let tactic := "intro t h"
+  let state3 ← match ← state2c.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"])
+
+  let tactic := "simp"
+  let state3d ← match ← state3.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let state2d ← match state3d.continue state2c with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let tactic := "rfl"
+  let stateF ← match ← state2d.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← stateF.serializeGoals (options := ← read)) =
+    #[])
+
+  let expr := stateF.mctx.eAssignment.find! stateF.root
+  let (expr, _) := instantiateMVarsCore (mctx := stateF.mctx) (e := expr)
+  addTest $ LSpec.check "(F root)" stateF.rootExpr?.isSome
+
+def test_nat_zero_add_alt: TestM Unit := do
+  let state? ← startProof (.expr "∀ (n: Nat), n + 0 = n")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+  let tactic := "intro n"
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[buildGoal [("n", "Nat")] "n + 0 = n"])
+  let recursor := "@Nat.brecOn"
+  let state2 ← match ← state1.tryMotivatedApply (state1.get! 0) (recursor := recursor) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let [mvarMotive, mvarMajor, mvarInduct, mvarConduit] := state2.goals |
+      fail "Incorrect number of goals"
+  let .num _ major := mvarMajor.name | fail "Incorrect form of mvar id"
+  addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
+    #[
+      buildNamedGoal mvarMotive.name.toString [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal mvarMajor.name.toString [("n", "Nat")] "Nat",
+      buildNamedGoal mvarInduct.name.toString [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal mvarConduit.name.toString [("n", "Nat")] s!"?motive ?m.{major} = (n + 0 = n)" (.some "conduit")
+    ])
+
+  let tactic := "intro x"
+  let state3m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state3m.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[buildGoal [("n", "Nat"), ("x", "Nat")] "Prop" (.some "motive")])
+  let tactic := "apply Eq"
+  let state3m2 ← match ← state3m.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let [eqL, eqR, eqT] := state3m2.goals | fail "Incorrect number of goals"
+  let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
+  let state2b ← match state3m2.resume [conduit] with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+
+  let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))"
+  let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))"
+  let fvN ← state2b.withContext conduit do
+    let lctx ← getLCtx
+    pure $ lctx.getFVarIds.get! 0 |>.name
+  let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))"
+  let substOf (mvarId: MVarId) := s!"(:subst (:mv {mvarId.name}) (:fv {fvN}) (:mv {mvarMajor}))"
+  let .num _ nL := eqL.name | fail "Incorrect form of mvar id"
+  let .num _ nR := eqR.name | fail "Incorrect form of mvar id"
+  let nL' := nL + 4
+  let nR' := nR + 5
+  addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
+    #[
+      {
+        name := mvarConduit.name.toString,
+        userName? := .some "conduit",
+        target := {
+          pp? := .some s!"(?m.{nL'} ?m.{major} = ?m.{nR'} ?m.{major}) = (n + 0 = n)",
+          sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})",
+        },
+        vars := #[{
+          name := fvN.toString,
+          userName := "n",
+          type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" },
+        }],
+      }
+    ])
+
 def test_tactic_failure_unresolved_goals : TestM Unit := do
   let state? ← startProof (.expr "∀ (p : Nat → Prop), ∃ (x : Nat), p (0 + x + 0)")
   let state0 ← match state? with
@@ -553,7 +726,7 @@ def test_tactic_failure_unresolved_goals : TestM Unit := do
 
   let tactic := "intro p"
   let state1 ← match ← state0.tacticOn 0 tactic with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -572,7 +745,7 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do
 
   let tactic := "intro p q r h"
   let state1 ← match ← state0.tacticOn 0 tactic with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -594,25 +767,6 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do
   let message := s!"<Pantograph>:0:31: error: don't know how to synthesize placeholder\ncontext:\np q r : Prop\nh : p → q\n⊢ p ∧ r\n"
   checkEq s!"{tactic} fails" messages #[message]
 
-def test_deconstruct : TestM Unit := do
-  let state? ← startProof (.expr "∀ (p q : Prop) (h : And p q), And q p")
-  let state0 ← match state? with
-    | .some state => pure state
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
-
-  let tactic := "intro p q ⟨hp, hq⟩"
-  let state1 ← match ← state0.tacticOn 0 tactic with
-    | .success state _ => pure state
-    | other => do
-      fail other.toString
-      return ()
-  checkEq tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize))
-    #[
-      buildGoal [("p", "Prop"), ("q", "Prop"), ("hp", "p"), ("hq", "q")] "q ∧ p"
-    ]
-
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
@@ -624,9 +778,10 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("Or.comm", test_or_comm),
     ("conv", test_conv),
     ("calc", test_calc),
+    ("Nat.zero_add", test_nat_zero_add),
+    ("Nat.zero_add alt", test_nat_zero_add_alt),
     ("tactic failure with unresolved goals", test_tactic_failure_unresolved_goals),
     ("tactic failure with synthesize placeholder", test_tactic_failure_synthesize_placeholder),
-    ("deconstruct", test_deconstruct),
   ]
   tests.map (fun (name, test) => (name, proofRunner env test))
 

Test/Serial.lean

@@ -47,8 +47,12 @@ def test_environment_pickling : TestM Unit := do
       (hints := Lean.mkReducibilityHintsRegularEx 1)
       (safety := Lean.DefinitionSafety.safe)
       (all := [])
-    addDecl c
+    let env' ← match (← getEnv).addDecl (← getOptions) c with
-    environmentPickle (← getEnv) envPicklePath
+      | .error e => do
+        let error ← (e.toMessageData (← getOptions)).toString
+        throwError error
+      | .ok env' => pure env'
+    environmentPickle env' envPicklePath
 
   let _ ← runCoreM coreDst do
     let (env', _) ← environmentUnpickle envPicklePath

Test/Tactic.lean

@@ -1,3 +1,5 @@
 import Test.Tactic.Assign
+import Test.Tactic.Congruence
+import Test.Tactic.MotivatedApply
+import Test.Tactic.NoConfuse
 import Test.Tactic.Prograde
-import Test.Tactic.Special

Test/Tactic/Congruence.lean

@@ -0,0 +1,88 @@
+import LSpec
+import Lean
+import Test.Common
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Test.Tactic.Congruence
+
+def test_congr_arg_list : TestT Elab.TermElabM Unit := do
+  let expr := "λ {α} (l1 l2 : List α) (h: l1 = l2) => l1.reverse = l2.reverse"
+  let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
+    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+      [
+        (`α, "Sort ?u.30"),
+        (`a₁, "?α"),
+        (`a₂, "?α"),
+        (`f, "?α → List α"),
+        (`h, "?a₁ = ?a₂"),
+        (`conduit, "(?f ?a₁ = ?f ?a₂) = (l1.reverse = l2.reverse)"),
+      ])
+    let f := newGoals.get! 3
+    let h := newGoals.get! 4
+    let c := newGoals.get! 5
+    let results ← Meta.withAssignableSyntheticOpaque do f.apply (← parseSentence "List.reverse")
+    addTest $ LSpec.check "apply" (results.length = 0)
+    addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂")
+    addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(List.reverse ?a₁ = List.reverse ?a₂) = (l1.reverse = l2.reverse)")
+def test_congr_arg : TestT Elab.TermElabM Unit := do
+  let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
+  let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
+    addTest $  LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+      [
+        (`α, "Sort ?u.73"),
+        (`a₁, "?α"),
+        (`a₂, "?α"),
+        (`f, "?α → Nat"),
+        (`h, "?a₁ = ?a₂"),
+        (`conduit, "(?f ?a₁ = ?f ?a₂) = (n * n = m * m)"),
+      ])
+def test_congr_fun : TestT Elab.TermElabM Unit := do
+  let expr := "λ (n m: Nat) => (n + m) + (n + m) = (n + m) * 2"
+  let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    let newGoals ← runTacticOnMVar Tactic.evalCongruenceFun target.mvarId!
+    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+      [
+        (`α, "Sort ?u.165"),
+        (`f₁, "?α → Nat"),
+        (`f₂, "?α → Nat"),
+        (`h, "?f₁ = ?f₂"),
+        (`a, "?α"),
+        (`conduit, "(?f₁ ?a = ?f₂ ?a) = (n + m + (n + m) = (n + m) * 2)"),
+      ])
+def test_congr : TestT Elab.TermElabM Unit := do
+  let expr := "λ (a b: Nat) => a = b"
+  let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    let newGoals ← runTacticOnMVar Tactic.evalCongruence target.mvarId!
+    addTest $  LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+      [
+        (`α, "Sort ?u.10"),
+        (`f₁, "?α → Nat"),
+        (`f₂, "?α → Nat"),
+        (`a₁, "?α"),
+        (`a₂, "?α"),
+        (`h₁, "?f₁ = ?f₂"),
+        (`h₂, "?a₁ = ?a₂"),
+        (`conduit, "(?f₁ ?a₁ = ?f₂ ?a₂) = (a = b)"),
+      ])
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("congrArg List.reverse", test_congr_arg_list),
+    ("congrArg", test_congr_arg),
+    ("congrFun", test_congr_fun),
+    ("congr", test_congr),
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
+
+end Pantograph.Test.Tactic.Congruence

Test/Tactic/MotivatedApply.lean

@@ -0,0 +1,113 @@
+import LSpec
+import Lean
+import Test.Common
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Test.Tactic.MotivatedApply
+
+def test_type_extract : TestT Elab.TermElabM Unit := do
+  let recursor ← parseSentence "@Nat.brecOn"
+  let recursorType ← Meta.inferType recursor
+  addTest $ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" =
+    (← exprToStr recursorType))
+  let info ← match Tactic.getRecursorInformation recursorType with
+    | .some info => pure info
+    | .none => throwError "Failed to extract recursor info"
+  addTest $ LSpec.check "iMotive" (info.iMotive = 2)
+  let motiveType := info.getMotiveType
+  addTest $ LSpec.check "motiveType" ("Nat → Sort ?u.1" =
+    (← exprToStr motiveType))
+
+def test_nat_brec_on : TestT Elab.TermElabM Unit := do
+  let expr := "λ (n t: Nat) => n + 0 = n"
+  let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
+    let recursor ← match Parser.runParserCategory
+      (env := ← MonadEnv.getEnv)
+      (catName := `term)
+      (input := "@Nat.brecOn")
+      (fileName := ← getFileName) with
+      | .ok syn => pure syn
+      | .error error => throwError "Failed to parse: {error}"
+    -- Apply the tactic
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    let tactic := Tactic.evalMotivatedApply recursor
+    let newGoals ← runTacticOnMVar tactic target.mvarId!
+    let test :=  LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
+      [
+        "Nat → Prop",
+        "Nat",
+        "∀ (t : Nat), Nat.below t → ?motive t",
+        "?motive ?m.74 = (n + 0 = n)",
+      ])
+    addTest test
+
+def test_list_brec_on : TestT Elab.TermElabM Unit := do
+  let expr := "λ {α : Type} (l: List α) => l ++ [] = [] ++ l"
+  let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
+    let recursor ← match Parser.runParserCategory
+      (env := ← MonadEnv.getEnv)
+      (catName := `term)
+      (input := "@List.brecOn")
+      (fileName := ← getFileName) with
+      | .ok syn => pure syn
+      | .error error => throwError "Failed to parse: {error}"
+    -- Apply the tactic
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    let tactic := Tactic.evalMotivatedApply recursor
+    let newGoals ← runTacticOnMVar tactic target.mvarId!
+    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
+      [
+        "Type ?u.90",
+        "List ?m.92 → Prop",
+        "List ?m.92",
+        "∀ (t : List ?m.92), List.below t → ?motive t",
+        "?motive ?m.94 = (l ++ [] = [] ++ l)",
+      ])
+
+def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
+  let expr := "λ (n t: Nat) => n + 0 = n"
+  let recursor ← match Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := `term)
+    (input := "@Nat.brecOn")
+    (fileName := ← getFileName) with
+    | .ok syn => pure syn
+    | .error error => throwError "Failed to parse: {error}"
+  let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
+    -- Apply the tactic
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    let tactic := Tactic.evalMotivatedApply recursor
+    let newGoals ← runTacticOnMVar tactic target.mvarId!
+    let majorId := 74
+    addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
+      [
+        "Nat → Prop",
+        "Nat",
+        "∀ (t : Nat), Nat.below t → ?motive t",
+        s!"?motive ?m.{majorId} = (n + 0 = n)",
+      ]))
+    let [motive, major, step, conduit] := newGoals | panic! "Incorrect goal number"
+    addTest $ (LSpec.check "goal name" (major.name.toString = s!"_uniq.{majorId}"))
+
+    -- Assign motive to `λ x => x + _`
+    let motive_assign ← parseSentence "λ (x: Nat) => @Nat.add x + 0 = _"
+    motive.assign motive_assign
+
+    addTest $ ← conduit.withContext do
+      let t := toString (← Meta.ppExpr $ ← conduit.getType)
+      return LSpec.check "conduit" (t = s!"(Nat.add ?m.{majorId} + 0 = ?m.149 ?m.{majorId}) = (n + 0 = n)")
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("type_extract", test_type_extract),
+    ("Nat.brecOn", test_nat_brec_on),
+    ("List.brecOn", test_list_brec_on),
+    ("Nat.brecOn partial motive instantiation", test_partial_motive_instantiation),
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
+
+end Pantograph.Test.Tactic.MotivatedApply

Test/Tactic/NoConfuse.lean

@@ -0,0 +1,72 @@
+import LSpec
+import Lean
+import Test.Common
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Test.Tactic.NoConfuse
+
+def test_nat : TestT Elab.TermElabM Unit := do
+  let expr := "λ (n: Nat) (h: 0 = n + 1) => False"
+  let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
+    let recursor ← match Parser.runParserCategory
+      (env := ← MonadEnv.getEnv)
+      (catName := `term)
+      (input := "h")
+      (fileName := ← getFileName) with
+      | .ok syn => pure syn
+      | .error error => throwError "Failed to parse: {error}"
+    -- Apply the tactic
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    let tactic := Tactic.evalNoConfuse recursor
+    let newGoals ← runTacticOnMVar tactic target.mvarId!
+    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
+
+def test_nat_fail : TestT Elab.TermElabM Unit := do
+  let expr := "λ (n: Nat) (h: n = n) => False"
+  let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
+    let recursor ← match Parser.runParserCategory
+      (env := ← MonadEnv.getEnv)
+      (catName := `term)
+      (input := "h")
+      (fileName := ← getFileName) with
+      | .ok syn => pure syn
+      | .error error => throwError "Failed to parse: {error}"
+    -- Apply the tactic
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    try
+      let tactic := Tactic.evalNoConfuse recursor
+      let _ ← runTacticOnMVar tactic target.mvarId!
+      addTest $ assertUnreachable "Tactic should fail"
+    catch _ =>
+      addTest $ LSpec.check "Tactic should fail" true
+
+def test_list : TestT Elab.TermElabM Unit := do
+  let expr := "λ (l: List Nat) (h: [] = 1 :: l) => False"
+  let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
+    let recursor ← match Parser.runParserCategory
+      (env := ← MonadEnv.getEnv)
+      (catName := `term)
+      (input := "h")
+      (fileName := ← getFileName) with
+      | .ok syn => pure syn
+      | .error error => throwError "Failed to parse: {error}"
+    -- Apply the tactic
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    let tactic := Tactic.evalNoConfuse recursor
+    let newGoals ← runTacticOnMVar tactic target.mvarId!
+    addTest $ LSpec.check "goals"
+      ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("Nat", test_nat),
+    ("Nat fail", test_nat_fail),
+    ("List", test_list),
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
+
+end Pantograph.Test.Tactic.NoConfuse

Test/Tactic/Prograde.lean

@@ -56,7 +56,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
   let state0 ← GoalState.create rootExpr
   let tactic := "intro p q h"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -65,7 +65,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
 
   let expr := "Or.inl (Or.inl h)"
   let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -75,7 +75,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
   let evalBind := "y"
   let evalExpr := "Or.inl h"
   let state2 ← match ← state1.tryDefine (state1.get! 0) (binderName := evalBind) (expr := evalExpr) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -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.19" },
+          type? := .some { pp? := .some "p ∨ ?m.25" },
           value? := .some { pp? := .some "Or.inl h" },
         }
       ]
@@ -95,7 +95,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
 
   let expr := "Or.inl y"
   let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -112,22 +112,22 @@ def fun_define_root_expr: ∀ (p: Prop), PProd (Nat → p) Unit → p := by
 def test_define_root_expr : TestT Elab.TermElabM Unit := do
   --let rootExpr ← parseSentence "Nat"
   --let state0 ← GoalState.create rootExpr
-  --let .success state1 _ ← state0.tacticOn (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5"
+  --let .success state1 ← state0.tacticOn (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5"
   --let .some rootExpr := state1.rootExpr? | addTest $ assertUnreachable "Root expr"
   --addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "5")
   let rootExpr ← parseSentence "∀ (p: Prop), PProd (Nat → p) Unit → p"
   let state0 ← GoalState.create rootExpr
   let tactic := "intro p x"
-  let .success state1 _ ← state0.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let .success state1 ← state0.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
   let binderName := `binder
   let value := "x.fst"
   let expr ← state1.goals[0]!.withContext $ strToTermSyntax value
   let tacticM := Tactic.evalDefine binderName expr
-  let .success state2 _ ← state1.tryTacticM (state1.get! 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}"
+  let .success state2 ← state1.tryTacticM (state1.get! 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}"
   let tactic := s!"apply {binderName}"
-  let .success state3 _ ← state2.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let .success state3 ← state2.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
   let tactic := s!"exact 5"
-  let .success state4 _ ← state3.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let .success state4 ← state3.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
   let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
   addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n  let binder := x.fst;\n  binder 5")
 
@@ -140,7 +140,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
   let state0 ← GoalState.create rootExpr
   let tactic := "intro p q h"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -149,7 +149,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
 
   let expr := "Or.inl (Or.inl h)"
   let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -159,7 +159,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
   let haveBind := "y"
   let haveType := "p ∨ q"
   let state2 ← match ← state1.tryHave (state1.get! 0) (binderName := haveBind) (type := haveType) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -171,7 +171,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
 
   let expr := "Or.inl h"
   let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -185,7 +185,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
       return ()
   let expr := "Or.inl y"
   let state4 ← match ← state2b.tryAssign (state2b.get! 0) (expr := expr) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -200,7 +200,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
   let state0 ← GoalState.create rootExpr
   let tactic := "intro a p h"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -216,7 +216,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
     | true => state1.tryLet (state1.get! 0) (binderName := "b") (type := letType)
     | false => state1.tryAssign (state1.get! 0) (expr := expr)
   let state2 ← match result2 with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -241,7 +241,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
 
   let tactic := "exact 1"
   let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -274,7 +274,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
 
   let tactic := "exact Or.inl (Or.inl h)"
   let state4 ← match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()

Test/Tactic/Special.lean

@@ -1,23 +0,0 @@
-import LSpec
-import Lean
-import Test.Common
-
-open Lean
-open Pantograph
-
-namespace Pantograph.Test.Tactic.Special
-
-def test_exact_q : TestT Elab.TermElabM Unit := do
-  let rootExpr ← parseSentence "1 + 2 = 2 + 3"
-  let state0 ← GoalState.create rootExpr
-  let tactic := "exact?"
-  let state1? ← state0.tacticOn (goalId := 0) (tactic := tactic)
-  let .failure messages := state1? | fail "Must fail"
-  checkEq "messages" messages #["`exact?` could not close the goal. Try `apply?` to see partial suggestions."]
-
-def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
-  [
-    ("exact?", test_exact_q),
-  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
-
-end Pantograph.Test.Tactic.Special

doc/rationale.md

@@ -47,16 +47,11 @@ include:
 
 - If a tactic loses track of metavariables, it will not be caught until the end
   of the proof search. This is a bug in the tactic itself.
-- Although a timeout feature exists in Pantograph, it relies on the coöperative
+- Timeouts for executing tactics is not available. Maybe this will change in the
-  multitasking from the tactic implementation. There is nothing preventing a
+  future.
-  buggy tactic from stalling Lean if it does not check for cancellation often.
-- For the same reason as above, there is no graceful way to stop a tactic which
-  leaks infinite memory. Users who wish to have this behaviour should run
-  Pantograph in a controlled environment with limited allocations. e.g.
-  Linux control groups.
 - Interceptions of parsing errors generally cannot be turned into goals (e.g.
-  `def mystery : Nat := :=`) due to Lean's parsing system. This question is also
+  `def mystery : Nat := :=`) due to Lean's parsing system.
-  not well-defined.
+
 
 ## References
 

doc/repl.md

@@ -22,9 +22,6 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   automatic mode (flag: `"automaticMode"`).  By default it is turned on, with
   all goals automatically resuming. This makes Pantograph act like a gym,
   with no resumption necessary to manage your goals.
-
-  Set `timeout` to a non-zero number to specify timeout (milliseconds) for all `CoreM`
-  operations.
 * `options.print`: Display the current set of options
 * `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
   Start a new proof from a given expression or symbol
@@ -39,8 +36,6 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   - `{ "conv": <bool> }`: Enter or exit conversion tactic mode. In the case of
     exit, the goal id is ignored.
   - `{ "draft": <expr> }`: Draft an expression with `sorry`s, turning them into goals. Coupling is not allowed.
-  If the `goals` field does not exist, the tactic execution has failed. Read
-  `messages` to find the reason.
 * `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`:
   Execute continuation/resumption
   - `{ "branch": <id> }`: Continue on branch state. The current state must have no goals.
@@ -51,15 +46,14 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   Save/Load a goal state to/from a file. The environment is not carried with the
   state. The user is responsible to ensure the sender/receiver instances share
   the same environment.
-* `frontend.process { ["fileName": <fileName>,] ["file": <str>], readHeader: <bool>, inheritEnv: <bool>, invocations:
+* `frontend.process { ["fileName": <fileName>,] ["file": <str>], invocations:
   <bool>, sorrys: <bool>, typeErrorsAsGoals: <bool>, newConstants: <bool> }`:
   Executes the Lean frontend on a file, collecting the tactic invocations
   (`"invocations": true`), the sorrys and type errors into goal states
   (`"sorrys": true`), and new constants (`"newConstants": true`). In the case of
   `sorrys`, this command additionally outputs the position of each captured
-  `sorry`. Conditionally inherit the environment from executing the file.
+  `sorry`. Warning: Behaviour is unstable in case of multiple `sorry`s. Use the
-  Warning: Behaviour is unstable in case of multiple `sorry`s. Use the draft
+  draft tactic if possible.
-  tactic if possible.
 
 ## Errors
 

flake.lock

@@ -5,11 +5,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1743550720,
+        "lastModified": 1730504689,
-        "narHash": "sha256-hIshGgKZCgWh6AYJpJmRgFdR3WUbkY04o82X05xqQiY=",
+        "narHash": "sha256-hgmguH29K2fvs9szpq2r3pz2/8cJd2LPS+b4tfNFCwE=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "c621e8422220273271f52058f618c94e405bb0f5",
+        "rev": "506278e768c2a08bec68eb62932193e341f55c90",
         "type": "github"
       },
       "original": {
@@ -39,16 +39,14 @@
     "lean4-nix": {
       "inputs": {
         "flake-parts": "flake-parts_2",
-        "nixpkgs": [
+        "nixpkgs": "nixpkgs"
-          "nixpkgs"
-        ]
       },
       "locked": {
-        "lastModified": 1743534244,
+        "lastModified": 1736388194,
-        "narHash": "sha256-WnoYs2iyrfgh35eXErCOyos8E2YbW3LT1xm/EtT88/k=",
+        "narHash": "sha256-ymSrd/A8Pw+9FzbxUbR7CkFHLJK1b4SnFFWg/1e0JeE=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "5eb7f03be257e327fdb3cca9465392e68dc28a4d",
+        "rev": "90f496bc0694fb97bdfa6adedfc2dc2c841a4cf2",
         "type": "github"
       },
       "original": {
@@ -57,35 +55,49 @@
         "type": "github"
       }
     },
+    "lspec": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1728279187,
+        "narHash": "sha256-ZMqbvCqR/gHXRuIkuo7b0Yp9N1vOQR7xnrcy/SeIBoQ=",
+        "owner": "argumentcomputer",
+        "repo": "LSpec",
+        "rev": "504a8cecf8da601b9466ac727aebb6b511aae4ab",
+        "type": "github"
+      },
+      "original": {
+        "owner": "argumentcomputer",
+        "ref": "504a8cecf8da601b9466ac727aebb6b511aae4ab",
+        "repo": "LSpec",
+        "type": "github"
+      }
+    },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1743975612,
+        "lastModified": 1728500571,
-        "narHash": "sha256-o4FjFOUmjSRMK7dn0TFdAT0RRWUWD+WsspPHa+qEQT8=",
+        "narHash": "sha256-dOymOQ3AfNI4Z337yEwHGohrVQb4yPODCW9MDUyAc4w=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "a880f49904d68b5e53338d1e8c7bf80f59903928",
+        "rev": "d51c28603def282a24fa034bcb007e2bcb5b5dd0",
         "type": "github"
       },
       "original": {
         "owner": "nixos",
-        "ref": "nixos-24.11",
+        "ref": "nixos-24.05",
         "repo": "nixpkgs",
         "type": "github"
       }
     },
     "nixpkgs-lib": {
       "locked": {
-        "lastModified": 1743296961,
+        "lastModified": 1730504152,
-        "narHash": "sha256-b1EdN3cULCqtorQ4QeWgLMrd5ZGOjLSLemfa00heasc=",
+        "narHash": "sha256-lXvH/vOfb4aGYyvFmZK/HlsNsr/0CVWlwYvo2rxJk3s=",
-        "owner": "nix-community",
+        "type": "tarball",
-        "repo": "nixpkgs.lib",
+        "url": "https://github.com/NixOS/nixpkgs/archive/cc2f28000298e1269cea6612cd06ec9979dd5d7f.tar.gz"
-        "rev": "e4822aea2a6d1cdd36653c134cacfd64c97ff4fa",
-        "type": "github"
       },
       "original": {
-        "owner": "nix-community",
+        "type": "tarball",
-        "repo": "nixpkgs.lib",
+        "url": "https://github.com/NixOS/nixpkgs/archive/cc2f28000298e1269cea6612cd06ec9979dd5d7f.tar.gz"
-        "type": "github"
       }
     },
     "nixpkgs-lib_2": {
@@ -100,11 +112,28 @@
         "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
       }
     },
+    "nixpkgs_2": {
+      "locked": {
+        "lastModified": 1731386116,
+        "narHash": "sha256-lKA770aUmjPHdTaJWnP3yQ9OI1TigenUqVC3wweqZuI=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "689fed12a013f56d4c4d3f612489634267d86529",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixos-24.05",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
     "root": {
       "inputs": {
         "flake-parts": "flake-parts",
         "lean4-nix": "lean4-nix",
-        "nixpkgs": "nixpkgs"
+        "lspec": "lspec",
+        "nixpkgs": "nixpkgs_2"
       }
     }
   },

flake.nix

@@ -2,11 +2,12 @@
   description = "Pantograph";
 
   inputs = {
-    nixpkgs.url = "github:nixos/nixpkgs/nixos-24.11";
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean4-nix = {
+    lean4-nix.url = "github:lenianiva/lean4-nix";
-      url = "github:lenianiva/lean4-nix";
+    lspec = {
-      inputs.nixpkgs.follows = "nixpkgs";
+      url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab";
+      flake = false;
     };
   };
 
@@ -15,6 +16,7 @@
     nixpkgs,
     flake-parts,
     lean4-nix,
+    lspec,
     ...
   }:
     flake-parts.lib.mkFlake {inherit inputs;} {
@@ -35,57 +37,32 @@
           inherit system;
           overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
         };
-        manifest = pkgs.lib.importJSON ./lake-manifest.json;
-        manifest-lspec = builtins.head manifest.packages;
         lspecLib = pkgs.lean.buildLeanPackage {
           name = "LSpec";
-          roots = ["LSpec"];
+          roots = ["Main" "LSpec"];
-          src = builtins.fetchGit {inherit (manifest-lspec) url rev;};
+          src = "${lspec}";
-        };
-        inherit (pkgs.lib.fileset) unions toSource fileFilter;
-        src = ./.;
-        set-project = unions [
-          ./Pantograph.lean
-          (fileFilter (file: file.hasExt "lean") ./Pantograph)
-        ];
-        set-repl = unions [
-          ./Main.lean
-          ./Repl.lean
-        ];
-        set-test = unions [
-          (fileFilter (file: file.hasExt "lean") ./Test)
-        ];
-        src-project = toSource {
-          root = src;
-          fileset = unions [
-            set-project
-          ];
-        };
-        src-repl = toSource {
-          root = src;
-          fileset = unions [
-            set-project
-            set-repl
-          ];
-        };
-        src-test = toSource {
-          root = src;
-          fileset = unions [
-            set-project
-            set-repl
-            set-test
-          ];
         };
         project = pkgs.lean.buildLeanPackage {
           name = "Pantograph";
           roots = ["Pantograph"];
-          src = src-project;
+          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+            src = ./.;
+            filter = path: type:
+              !(pkgs.lib.hasInfix "/Test/" path)
+              && !(pkgs.lib.hasSuffix ".md" path)
+              && !(pkgs.lib.hasSuffix "Repl.lean" path);
+          });
         };
         repl = pkgs.lean.buildLeanPackage {
           name = "Repl";
           roots = ["Main" "Repl"];
           deps = [project];
-          src = src-repl;
+          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+            src = ./.;
+            filter = path: type:
+              !(pkgs.lib.hasInfix "/Test/" path)
+              && !(pkgs.lib.hasSuffix ".md" path);
+          });
         };
         test = pkgs.lean.buildLeanPackage {
           name = "Test";
@@ -94,7 +71,11 @@
           # Environment`) and thats where `lakefile.lean` resides.
           roots = ["Test.Main"];
           deps = [lspecLib repl];
-          src = src-test;
+          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+            src = ./.;
+            filter = path: type:
+              !(pkgs.lib.hasInfix "Pantograph" path);
+          });
         };
       in rec {
         packages = {

lake-manifest.json

@@ -1,15 +1,15 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/argumentcomputer/LSpec.git",
+ [{"url": "https://github.com/lenianiva/LSpec.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a6652a48b5c67b0d8dd3930fad6390a97d127e8d",
+   "rev": "c492cecd0bc473e2f9c8b94d545d02cc0056034f",
    "name": "LSpec",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "a6652a48b5c67b0d8dd3930fad6390a97d127e8d",
+   "inputRev": "c492cecd0bc473e2f9c8b94d545d02cc0056034f",
    "inherited": false,
-   "configFile": "lakefile.toml"}],
+   "configFile": "lakefile.lean"}],
  "name": "pantograph",
  "lakeDir": ".lake"}

lakefile.lean

@@ -18,7 +18,7 @@ lean_exe repl {
 }
 
 require LSpec from git
-  "https://github.com/argumentcomputer/LSpec.git" @ "a6652a48b5c67b0d8dd3930fad6390a97d127e8d"
+  "https://github.com/lenianiva/LSpec.git" @ "c492cecd0bc473e2f9c8b94d545d02cc0056034f"
 lean_lib Test {
 }
 @[test_driver]

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.18.0
+leanprover/lean4:v4.15.0