Merge pull request 'feat: Add support for the `have`, `conv`, and `calc` tactics' (#59) from goal/have-conv-calc into dev

Reviewed-on: #59

Pantograph.lean

@@ -71,7 +71,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     Environment.addDecl args
   expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
     let state ← get
-    exprEcho args.expr state.options
+    exprEcho args.expr args.type? state.options
   options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
     let state ← get
     let options := state.options
@@ -93,11 +93,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
     let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
-      | .some expr, .none => do
-        let expr ← match ← exprParse expr with
-          | .error e => return .error e
-          | .ok expr => pure $ expr
-        return .ok $ ← GoalState.create expr
+      | .some expr, .none => goalStartExpr expr
       | .none, .some copyFrom =>
         (match env.find? <| copyFrom.toName with
         | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
@@ -118,12 +114,22 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     match state.goalStates.find? args.stateId with
     | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
     | .some goalState => do
-      let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
-        | .some tactic, .none => do
+      let nextGoalState?: Except _ GoalState ←
+        match args.tactic?, args.expr?, args.have?, args.calc?, args.conv?  with
+        | .some tactic, .none, .none, .none, .none => do
           pure ( Except.ok (← goalTactic goalState args.goalId tactic))
-        | .none, .some expr => do
-          pure ( Except.ok (← goalTryAssign goalState args.goalId expr))
-        | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied")
+        | .none, .some expr, .none, .none, .none => do
+          pure ( Except.ok (← goalAssign goalState args.goalId expr))
+        | .none, .none, .some type, .none, .none => do
+          let binderName := args.binderName?.getD ""
+          pure ( Except.ok (← goalHave goalState args.goalId binderName type))
+        | .none, .none, .none, .some pred, .none => do
+          pure ( Except.ok (← goalCalc goalState args.goalId pred))
+        | .none, .none, .none, .none, .some true => do
+          pure ( Except.ok (← goalConv goalState args.goalId))
+        | .none, .none, .none, .none, .some false => do
+          pure ( Except.ok (← goalConvExit goalState))
+        | _, _, _, _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr, have} must be supplied")
       match nextGoalState? with
       | .error error => return .error error
       | .ok (.success nextGoalState) =>
@@ -141,6 +147,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         return .ok { parseError? := .some message }
       | .ok (.indexError goalId) =>
         return .error $ errorIndex s!"Invalid goal id index {goalId}"
+      | .ok (.invalidAction message) =>
+        return .error $ errorI "invalid" message
       | .ok (.failure messages) =>
         return .ok { tacticErrors? := .some messages }
   goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
@@ -152,7 +160,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         | .some branchId, .none => do
           match state.goalStates.find? branchId with
           | .none => return .error $ errorIndex s!"Invalid state index {branchId}"
-          | .some branch => pure $ target.continue branch
+          | .some branch => pure $ goalContinue target branch
         | .none, .some goals =>
           pure $ goalResume target goals
         | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"

Pantograph/Environment.lean

@@ -7,14 +7,15 @@ open Pantograph
 
 namespace Pantograph.Environment
 
-def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool :=
-  isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ info.isUnsafe
+def isNameInternal (n: Lean.Name): Bool :=
+  -- Returns true if the name is an implementation detail which should not be shown to the user.
+  isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ n.isAuxLemma ∨ n.hasMacroScopes
   where
   isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with
     | .str _ name => name == "Lean"
     | _ => true
 
-def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
+def toCompactSymbolName (n: Lean.Name) (info: Lean.ConstantInfo): String :=
   let pref := match info with
   | .axiomInfo  _ => "a"
   | .defnInfo   _ => "d"
@@ -26,14 +27,14 @@ def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
   | .recInfo    _ => "r"
   s!"{pref}{toString n}"
 
-def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
-  if is_symbol_unsafe_or_internal n info
+def toFilteredSymbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
+  if isNameInternal n || info.isUnsafe
   then Option.none
-  else Option.some <| to_compact_symbol_name n info
+  else Option.some <| toCompactSymbolName n info
 def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do
   let env ← Lean.MonadEnv.getEnv
   let names := env.constants.fold (init := #[]) (λ acc name info =>
-    match to_filtered_symbol name info with
+    match toFilteredSymbol name info with
     | .some x => acc.push x
     | .none => acc)
   return { symbols := names }
@@ -58,12 +59,18 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
     value? := ← value?.mapM (λ v => serialize_expression options v |>.run'),
     publicName? := Lean.privateToUserName? name |>.map (·.toString),
     -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
-    typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none,
-    valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none,
+    typeDependency? := if args.dependency?.getD false
+      then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n)
+      else .none,
+    valueDependency? := ← if args.dependency?.getD false
+      then info.value?.mapM (λ e => do
+        let e ← unfoldAuxLemmas e
+        pure $ e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => name_to_ast n) )
+      else pure (.none),
     module? := module?
   }
-  let result := match info with
-    | .inductInfo induct => { core with inductInfo? := .some {
+  let result ← match info with
+    | .inductInfo induct => pure { core with inductInfo? := .some {
           numParams := induct.numParams,
           numIndices := induct.numIndices,
           all := induct.all.toArray.map (·.toString),
@@ -72,32 +79,38 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
           isReflexive := induct.isReflexive,
           isNested := induct.isNested,
       } }
-    | .ctorInfo ctor => { core with constructorInfo? := .some {
+    | .ctorInfo ctor => pure { core with constructorInfo? := .some {
           induct := ctor.induct.toString,
           cidx := ctor.cidx,
           numParams := ctor.numParams,
           numFields := ctor.numFields,
       } }
-    | .recInfo r => { core with recursorInfo? := .some {
+    | .recInfo r => pure { core with recursorInfo? := .some {
           all := r.all.toArray.map (·.toString),
           numParams := r.numParams,
           numIndices := r.numIndices,
           numMotives := r.numMotives,
           numMinors := r.numMinors,
+          rules := ← r.rules.toArray.mapM (λ rule => do
+              pure {
+                ctor := rule.ctor.toString,
+                nFields := rule.nfields,
+                rhs := ← (serialize_expression options rule.rhs).run',
+              })
           k := r.k,
       } }
-    | _ => core
+    | _ => pure core
   return .ok result
 def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
   let env ← Lean.MonadEnv.getEnv
   let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do
-    let type ← match syntax_from_str env args.type with
+    let type ← match parseTerm env args.type with
       | .ok syn => do
-        match ← syntax_to_expr syn with
+        match ← elabTerm syn with
         | .error e => return .error e
         | .ok expr => pure expr
       | .error e => return .error e
-    let value ← match syntax_from_str env args.value with
+    let value ← match parseTerm env args.value with
       | .ok syn => do
         try
           let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .some type)

Pantograph/Goal.lean

@@ -1,3 +1,8 @@
+/-
+Functions for handling metavariables
+
+All the functions starting with `try` resume their inner monadic state.
+-/
 import Pantograph.Protocol
 import Lean
 
@@ -10,6 +15,11 @@ def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
 namespace Pantograph
 open Lean
 
+def filename: String := "<pantograph>"
+
+/--
+Represents an interconnected set of metavariables, or a state in proof search
+ -/
 structure GoalState where
   savedState : Elab.Tactic.SavedState
 
@@ -18,21 +28,22 @@ structure GoalState where
   -- New metavariables acquired in this state
   newMVars: SSet MVarId
 
-  -- The id of the goal in the parent
-  parentGoalId: Nat := 0
-
   -- Parent state metavariable source
-  parentMVar: Option MVarId
+  parentMVar?: Option MVarId
 
-abbrev M := Elab.TermElabM
+  -- Existence of this field shows that we are currently in `conv` mode.
+  convMVar?: Option (MVarId × MVarId) := .none
+  -- Previous RHS for calc, so we don't have to repeat it every time
+  -- WARNING: If using `state with` outside of `calc`, this must be set to `.none`
+  calcPrevRhs?: Option Expr := .none
 
-protected def GoalState.create (expr: Expr): M GoalState := do
+protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
   -- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context.
   -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
 
   --Elab.Term.synthesizeSyntheticMVarsNoPostponing
   --let expr ← instantiateMVars expr
-  let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous))
+  let goal ← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous)
   let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
   let root := goal.mvarId!
   let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root]}
@@ -40,28 +51,38 @@ protected def GoalState.create (expr: Expr): M GoalState := do
     savedState,
     root,
     newMVars := SSet.insert .empty root,
-    parentMVar := .none,
+    parentMVar? := .none,
   }
-protected def GoalState.goals (state: GoalState): List MVarId := state.savedState.tactic.goals
-
-protected def GoalState.runM {α: Type} (state: GoalState) (m: Elab.TermElabM α) : M α := do
-  state.savedState.term.restore
-  m
-
+protected def GoalState.isConv (state: GoalState): Bool :=
+  state.convMVar?.isSome
+protected def GoalState.goals (state: GoalState): List MVarId :=
+  state.savedState.tactic.goals
 protected def GoalState.mctx (state: GoalState): MetavarContext :=
   state.savedState.term.meta.meta.mctx
 protected def GoalState.env (state: GoalState): Environment :=
   state.savedState.term.meta.core.env
 private def GoalState.mvars (state: GoalState): SSet MVarId :=
   state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
+protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
+  state.savedState.term.meta.restore
 private def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
   state.savedState.term.restore
-def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
-  state.savedState.term.meta.restore
+private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do
+  state.savedState.restore
+  Elab.Tactic.setGoals [goal]
+
+private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext): SSet MVarId :=
+  mctxNew.decls.foldl (fun acc mvarId mvarDecl =>
+    if let .some prevMVarDecl := mctxOld.decls.find? mvarId then
+      assert! prevMVarDecl.type == mvarDecl.type
+      acc
+    else
+      acc.insert mvarId
+    ) SSet.empty
 
 /-- Inner function for executing tactic on goal state -/
 def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) :
-    M (Except (Array String) Elab.Tactic.SavedState):= do
+    Elab.TermElabM (Except (Array String) Elab.Tactic.SavedState):= do
   let tacticM (stx: Syntax):  Elab.Tactic.TacticM (Except (Array String) Elab.Tactic.SavedState) := do
     state.restore
     Elab.Tactic.setGoals [goal]
@@ -87,19 +108,22 @@ inductive TacticResult where
   | parseError (message: String)
   -- The goal index is out of bounds
   | indexError (goalId: Nat)
+  -- The given action cannot be executed in the state
+  | invalidAction (message: String)
 
 /-- Execute tactic on given state -/
-protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String):
-    M TacticResult := do
+protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String):
+    Elab.TermElabM TacticResult := do
   state.restoreElabM
   let goal ← match state.savedState.tactic.goals.get? goalId with
     | .some goal => pure $ goal
     | .none => return .indexError goalId
+  goal.checkNotAssigned `GoalState.tryTactic
   let tactic ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
-    (catName := `tactic)
+    (catName := if state.isConv then `conv else `tactic)
     (input := tactic)
-    (fileName := "<stdin>") with
+    (fileName := filename) with
     | .ok stx => pure $ stx
     | .error error => return .parseError error
   match (← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic)) with
@@ -108,25 +132,59 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String
   | .ok nextSavedState =>
     -- Assert that the definition of metavariables are the same
     let nextMCtx := nextSavedState.term.meta.meta.mctx
-    let prevMCtx := state.savedState.term.meta.meta.mctx
+    let prevMCtx := state.mctx
     -- Generate a list of mvarIds that exist in the parent state; Also test the
     -- assertion that the types have not changed on any mvars.
-    let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
-      if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
-        assert! prevMVarDecl.type == mvarDecl.type
-        return acc
-      else
-        return acc.insert mvarId
-      ) SSet.empty
     return .success {
-      root := state.root,
+      state with
       savedState := nextSavedState
-      newMVars,
-      parentGoalId := goalId,
-      parentMVar := .some goal,
+      newMVars := newMVarSet prevMCtx nextMCtx,
+      parentMVar? := .some goal,
+      calcPrevRhs? := .none,
     }
 
-protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do
+/-- Assumes elabM has already been restored. Assumes expr has already typechecked -/
+protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
+      Elab.TermElabM TacticResult := do
+  let goalType ← goal.getType
+  try
+    -- For some reason this is needed. One of the unit tests will fail if this isn't here
+    let error?: Option String ← goal.withContext (do
+      let exprType ← Meta.inferType expr
+      if ← Meta.isDefEq goalType exprType then
+        pure .none
+      else do
+        return .some s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} != {← Meta.ppExpr goalType}"
+    )
+    if let .some error := error? then
+      return .parseError error
+    goal.checkNotAssigned `GoalState.assign
+    goal.assign expr
+    if (← getThe Core.State).messages.hasErrors then
+      let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
+      let errors ← (messages.map Message.data).mapM fun md => md.toString
+      return .failure errors
+    else
+      let prevMCtx := state.savedState.term.meta.meta.mctx
+      let nextMCtx ← getMCtx
+      -- Generate a list of mvarIds that exist in the parent state; Also test the
+      -- assertion that the types have not changed on any mvars.
+      let newMVars := newMVarSet prevMCtx nextMCtx
+      let nextGoals ← newMVars.toList.filterM (λ mvar => do pure !(← mvar.isAssigned))
+      return .success {
+        root := state.root,
+        savedState := {
+          term := ← MonadBacktrack.saveState,
+          tactic := { goals := nextGoals }
+        },
+        newMVars,
+        parentMVar? := .some goal,
+      }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String):
+      Elab.TermElabM TacticResult := do
   state.restoreElabM
   let goal ← match state.savedState.tactic.goals.get? goalId with
     | .some goal => pure goal
@@ -135,50 +193,221 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String
     (env := state.env)
     (catName := `term)
     (input := expr)
-    (fileName := "<stdin>") with
+    (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  let tacticM:  Elab.Tactic.TacticM TacticResult := do
+  let goalType ← goal.getType
+  try
+    let expr ← goal.withContext $
+      Elab.Term.elabTermAndSynthesize (stx := expr) (expectedType? := .some goalType)
+    state.assign goal expr
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+-- Specialized Tactics
+
+protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure goal
+    | .none => return .indexError goalId
+  let type ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := type)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  let binderName := binderName.toName
+  try
+    -- Implemented similarly to the intro tactic
+    let nextGoals: List MVarId ← goal.withContext $ (do
+      let type ← Elab.Term.elabType (stx := type)
+      let lctx ← MonadLCtx.getLCtx
+
+      -- The branch goal inherits the same context, but with a different type
+      let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
+
+      -- Create the context for the `upstream` goal
+      let fvarId ← mkFreshFVarId
+      let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
+      let fvar   := mkFVar fvarId
+      let mvarUpstream ←
+        withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
+          Meta.withNewLocalInstances #[fvar] 0 (do
+            let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
+              (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
+            let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
+            goal.assign expr
+            pure mvarUpstream)
+
+      pure [mvarBranch.mvarId!, mvarUpstream.mvarId!]
+    )
+    return .success {
+      root := state.root,
+      savedState := {
+        term := ← MonadBacktrack.saveState,
+        tactic := { goals := nextGoals }
+      },
+      newMVars := nextGoals.toSSet,
+      parentMVar? := .some goal,
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+/-- Enter conv tactic mode -/
+protected def GoalState.conv (state: GoalState) (goalId: Nat):
+      Elab.TermElabM TacticResult := do
+  if state.convMVar?.isSome then
+    return .invalidAction "Already in conv state"
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure goal
+    | .none => return .indexError goalId
+  let tacticM :  Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do
+    state.restoreTacticM goal
+
+    -- See Lean.Elab.Tactic.Conv.convTarget
+    let convMVar ← Elab.Tactic.withMainContext do
+      let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
+      Elab.Tactic.setGoals [newGoal.mvarId!]
+      pure rhs.mvarId!
+    return (← MonadBacktrack.saveState, convMVar)
+  try
+    let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
+    let prevMCtx := state.mctx
+    let nextMCtx := nextSavedState.term.meta.meta.mctx
+    return .success {
+      root := state.root,
+      savedState := nextSavedState
+      newMVars := newMVarSet prevMCtx nextMCtx,
+      parentMVar? := .some goal,
+      convMVar? := .some (convRhs, goal),
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+/-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/
+protected def GoalState.convExit (state: GoalState):
+      Elab.TermElabM TacticResult := do
+  let (convRhs, convGoal) ← match state.convMVar? with
+    | .some mvar => pure mvar
+    | .none => return .invalidAction "Not in conv state"
+  let tacticM :  Elab.Tactic.TacticM Elab.Tactic.SavedState:= do
+    -- Vide `Lean.Elab.Tactic.Conv.convert`
     state.savedState.restore
-    Elab.Tactic.setGoals [goal]
-    try
-      let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
-      -- Attempt to unify the expression
-      let goalType ← goal.getType
-      let exprType ← Meta.inferType expr
-      if !(← Meta.isDefEq goalType exprType) then
-        return .failure #["Type unification failed", toString (← Meta.ppExpr goalType), toString (← Meta.ppExpr exprType)]
-      goal.checkNotAssigned `GoalState.tryAssign
-      goal.assign expr
-      if (← getThe Core.State).messages.hasErrors then
-        let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
-        let errors ← (messages.map Message.data).mapM fun md => md.toString
-        return .failure errors
+
+    -- Close all existing goals with `refl`
+    for mvarId in (← Elab.Tactic.getGoals) do
+      liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
+    Elab.Tactic.pruneSolvedGoals
+    unless (← Elab.Tactic.getGoals).isEmpty do
+      throwError "convert tactic failed, there are unsolved goals\n{Elab.goalsToMessageData (← Elab.Tactic.getGoals)}"
+
+    Elab.Tactic.setGoals [convGoal]
+
+    let targetNew ← instantiateMVars (.mvar convRhs)
+    let proof ← instantiateMVars (.mvar convGoal)
+
+    Elab.Tactic.liftMetaTactic1 fun mvarId => mvarId.replaceTargetEq targetNew proof
+    MonadBacktrack.saveState
+  try
+    let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
+    let nextMCtx := nextSavedState.term.meta.meta.mctx
+    let prevMCtx := state.savedState.term.meta.meta.mctx
+    return .success {
+      root := state.root,
+      savedState := nextSavedState
+      newMVars := newMVarSet prevMCtx nextMCtx,
+      parentMVar? := .some convGoal,
+      convMVar? := .none
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  if state.convMVar?.isSome then
+    return .invalidAction "Cannot initiate `calc` while in `conv` state"
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure goal
+    | .none => return .indexError goalId
+  let `(term|$pred) ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := pred)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  try
+    goal.withContext do
+    let target ← instantiateMVars (← goal.getDecl).type
+    let tag := (← goal.getDecl).userName
+
+    let mut step ← Elab.Term.elabType <| ← do
+      if let some prevRhs := state.calcPrevRhs? then
+        Elab.Term.annotateFirstHoleWithType pred (← Meta.inferType prevRhs)
       else
-        let prevMCtx := state.savedState.term.meta.meta.mctx
-        let nextMCtx ← getMCtx
-        -- Generate a list of mvarIds that exist in the parent state; Also test the
-        -- assertion that the types have not changed on any mvars.
-        let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
-          if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
-            assert! prevMVarDecl.type == mvarDecl.type
-            return acc
-          else
-            return mvarId :: acc
-          ) []
-        -- The new goals are the newMVars that lack an assignment
-        Elab.Tactic.setGoals (← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned)))
-        let nextSavedState ← MonadBacktrack.saveState
-        return .success {
-          root := state.root,
-          savedState := nextSavedState,
-          newMVars := newMVars.toSSet,
-          parentGoalId := goalId,
-          parentMVar := .some goal,
-        }
-    catch exception =>
-      return .failure #[← exception.toMessageData.toString]
-  tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
+        pure pred
+
+    let some (_, lhs, rhs) ← Elab.Term.getCalcRelation? step |
+      throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}"
+    if let some prevRhs := state.calcPrevRhs? then
+      unless (← Meta.isDefEqGuarded lhs prevRhs) do
+        throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- "
+
+    -- Creates a mvar to represent the proof that the calc tactic solves the
+    -- current branch
+    -- In the Lean `calc` tactic this is gobbled up by
+    -- `withCollectingNewGoalsFrom`
+    let mut proof ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) step
+      (userName := tag ++ `calc)
+    let mvarBranch := proof.mvarId!
+
+    let calcPrevRhs? := Option.some rhs
+    let mut proofType ← Meta.inferType proof
+    let mut remainder := Option.none
+
+    -- The calc tactic either solves the main goal or leaves another relation.
+    -- Replace the main goal, and save the new goal if necessary
+    if ¬(← Meta.isDefEq proofType target) then
+      let rec throwFailed :=
+        throwError "'calc' tactic failed, has type{indentExpr proofType}\nbut it is expected to have type{indentExpr target}"
+      let some (_, _, rhs) ← Elab.Term.getCalcRelation? proofType | throwFailed
+      let some (r, _, rhs') ← Elab.Term.getCalcRelation? target | throwFailed
+      let lastStep := mkApp2 r rhs rhs'
+      let lastStepGoal ← Meta.mkFreshExprSyntheticOpaqueMVar lastStep tag
+      (proof, proofType) ← Elab.Term.mkCalcTrans proof proofType lastStepGoal lastStep
+      unless (← Meta.isDefEq proofType target) do throwFailed
+      remainder := .some lastStepGoal.mvarId!
+    goal.assign proof
+
+    let goals := [ mvarBranch ] ++ remainder.toList
+    return .success {
+      root := state.root,
+      savedState := {
+        term := ← MonadBacktrack.saveState,
+        tactic := { goals },
+      },
+      newMVars := goals.toSSet,
+      parentMVar? := .some goal,
+      calcPrevRhs?
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+
+protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do
+  let goal ← state.savedState.tactic.goals.get? goalId
+  return {
+    state with
+    savedState := {
+      state.savedState with
+      tactic := { goals := [goal] },
+    },
+    calcPrevRhs? := .none,
+  }
 
 /--
 Brings into scope a list of goals
@@ -197,8 +426,8 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S
         term := state.savedState.term,
         tactic := { goals := unassigned },
       },
+      calcPrevRhs? := .none,
     }
-
 /--
 Brings into scope all goals from `branch`
 -/
@@ -221,10 +450,14 @@ protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
     assert! goalState.goals.isEmpty
     return expr
 protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
-  let parent ← goalState.parentMVar
+  let parent ← goalState.parentMVar?
   let expr := goalState.mctx.eAssignment.find! parent
   let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
   return expr
+protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): Option Expr := do
+  let expr ← goalState.mctx.eAssignment.find? mvar
+  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
+  return expr
 
 
 end Pantograph

Pantograph/Library.lean

@@ -36,13 +36,15 @@ end Lean
 
 namespace Pantograph
 
+def defaultTermElabMContext: Lean.Elab.Term.Context := {
+    autoBoundImplicit := true,
+    declName? := some "_pantograph".toName,
+    errToSorry := false
+  }
 def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α :=
   metaM.run'
 def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α :=
-  termElabM.run' (ctx := {
-    declName? := .none,
-    errToSorry := false,
-  }) |>.run'
+  termElabM.run' (ctx := defaultTermElabMContext) |>.run'
 
 def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
 
@@ -63,7 +65,7 @@ def createCoreContext (options: Array String): IO Lean.Core.Context := do
     currNamespace := Lean.Name.str .anonymous "Aniva"
     openDecls := [],     -- No 'open' directives needed
     fileName := "<Pantograph>",
-    fileMap := { source := "", positions := #[0], lines := #[1] },
+    fileMap := { source := "", positions := #[0] },
     options := options
   }
 
@@ -109,71 +111,103 @@ def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
     Lean.CoreM (Protocol.CR Protocol.EnvAddResult) :=
   Environment.addDecl { name, type, value, isTheorem }
 
-/-- This must be a TermElabM since the parsed expr contains extra information -/
-def exprParse (s: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
+def parseElabType (type: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
   let env ← Lean.MonadEnv.getEnv
-  let syn ← match syntax_from_str env s with
+  let syn ← match parseTerm env type with
     | .error str => return .error $ errorI "parsing" str
     | .ok syn => pure syn
-  match ← syntax_to_expr syn with
+  match ← elabType syn with
   | .error str => return .error $ errorI "elab" str
-  | .ok expr => return .ok expr
+  | .ok expr => return .ok (← Lean.instantiateMVars expr)
+
+/-- This must be a TermElabM since the parsed expr contains extra information -/
+def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
+  let env ← Lean.MonadEnv.getEnv
+  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 => return .error $ errorI "parsing" str
+    | .ok syn => pure syn
+  match ← elabTerm syn expectedType? with
+  | .error str => return .error $ errorI "elab" str
+  | .ok expr => return .ok (← Lean.instantiateMVars expr)
 
 @[export pantograph_expr_echo_m]
-def exprEcho (expr: String) (options: @&Protocol.Options):
-    Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
-  let termElabM: Lean.Elab.TermElabM _ := do
-    let expr ← match ← exprParse expr with
+def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options):
+    Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) :=
+  runTermElabM do
+    let expr ← match ← parseElabExpr expr expectedType? with
       | .error e => return .error e
       | .ok expr => pure expr
     try
-      let type ← Lean.Meta.inferType expr
+      let type ← unfoldAuxLemmas (← Lean.Meta.inferType expr)
       return .ok {
           type := (← serialize_expression options type),
           expr := (← serialize_expression options expr)
       }
     catch exception =>
       return .error $ errorI "typing" (← exception.toMessageData.toString)
-  runTermElabM termElabM
 
 @[export pantograph_goal_start_expr_m]
 def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) :=
-  let termElabM: Lean.Elab.TermElabM _ := do
-    let expr ← match ← exprParse expr with
+  runTermElabM do
+    let expr ← match ← parseElabType expr with
       | .error e => return .error e
       | .ok expr => pure $ expr
     return .ok $ ← GoalState.create expr
-  runTermElabM termElabM
 
 @[export pantograph_goal_tactic_m]
 def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult :=
-  runTermElabM <| GoalState.execute state goalId tactic
+  runTermElabM <| state.tryTactic goalId tactic
 
-@[export pantograph_goal_try_assign_m]
-def goalTryAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult :=
-  runTermElabM <| GoalState.tryAssign state goalId expr
+@[export pantograph_goal_assign_m]
+def goalAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult :=
+  runTermElabM <| state.tryAssign goalId expr
 
-@[export pantograph_goal_continue]
-def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=
-  target.continue branch
+@[export pantograph_goal_have_m]
+def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult :=
+  runTermElabM <| state.tryHave goalId binderName type
+
+@[export pantograph_goal_conv_m]
+def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult :=
+  runTermElabM <| state.conv goalId
+
+@[export pantograph_goal_conv_exit_m]
+def goalConvExit (state: GoalState): Lean.CoreM TacticResult :=
+  runTermElabM <| state.convExit
+
+@[export pantograph_goal_calc_m]
+def goalCalc (state: GoalState) (goalId: Nat) (pred: String): Lean.CoreM TacticResult :=
+  runTermElabM <| state.tryCalc goalId pred
+
+@[export pantograph_goal_focus]
+def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
+  state.focus goalId
 
 @[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_continue]
+def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=
+  target.continue branch
+
 @[export pantograph_goal_serialize_m]
 def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) :=
   runMetaM <| state.serializeGoals (parent := .none) options
 
 @[export pantograph_goal_print_m]
-def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := do
-  let metaM := do
+def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult :=
+  runMetaM do
     state.restoreMetaM
     return {
-      root? := ← state.rootExpr?.mapM (λ expr => serialize_expression options expr),
-      parent? := ← state.parentExpr?.mapM (λ expr => serialize_expression options expr),
+      root? := ← state.rootExpr?.mapM (λ expr => do
+        serialize_expression options (← unfoldAuxLemmas expr)),
+      parent? := ← state.parentExpr?.mapM (λ expr => do
+        serialize_expression options (← unfoldAuxLemmas expr)),
     }
-  runMetaM metaM
 
 
 end Pantograph

Pantograph/Protocol.lean

@@ -98,6 +98,7 @@ structure StatResult where
 -- Return the type of an expression
 structure ExprEcho where
   expr: String
+  type?: Option String
   deriving Lean.FromJson
 structure ExprEchoResult where
   expr: Expression
@@ -137,12 +138,20 @@ structure ConstructorInfo where
   numParams: Nat
   numFields: Nat
   deriving Lean.ToJson
+
+/-- See `Lean/Declaration.lean` -/
+structure RecursorRule where
+  ctor: String
+  nFields: Nat
+  rhs: Expression
+  deriving Lean.ToJson
 structure RecursorInfo where
   all: Array String
   numParams: Nat
   numIndices: Nat
   numMotives: Nat
   numMinors: Nat
+  rules: Array RecursorRule
   k: Bool
   deriving Lean.ToJson
 structure EnvInspectResult where
@@ -200,6 +209,14 @@ structure GoalTactic where
   -- One of the fields here must be filled
   tactic?: Option String := .none
   expr?: Option String := .none
+  have?: Option String := .none
+  calc?: Option String := .none
+  -- true to enter `conv`, `false` to exit. In case of exit the `goalId` is ignored.
+  conv?: Option Bool := .none
+
+  -- In case of the `have` tactic, the new free variable name is provided here
+  binderName?: Option String := .none
+
   deriving Lean.FromJson
 structure GoalTacticResult where
   -- The next goal state id. Existence of this field shows success
@@ -243,7 +260,7 @@ structure GoalPrintResult where
   -- The root expression
   root?: Option Expression := .none
   -- The filling expression of the parent goal
-  parent?: Option Expression := .none
+  parent?: Option Expression
   deriving Lean.ToJson
 
 -- Diagnostic Options, not available in REPL

Pantograph/Serial.lean

@@ -6,35 +6,37 @@ import Lean
 import Pantograph.Protocol
 import Pantograph.Goal
 
-namespace Pantograph
 open Lean
 
+-- Symbol processing functions --
+
+def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
+
+namespace Pantograph
+
+/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
+def unfoldAuxLemmas (e : Lean.Expr) : Lean.CoreM Lean.Expr := do
+  Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
+
 --- Input Functions ---
 
-
-/-- Read a theorem from the environment -/
-def expr_from_const (env: Environment) (name: Name): Except String Lean.Expr :=
-  match env.find? name with
-  | none       => throw s!"Symbol not found: {name}"
-  | some cInfo => return cInfo.type
 /-- Read syntax object from string -/
-def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
+def parseTerm (env: Environment) (s: String): Except String Syntax :=
   Parser.runParserCategory
     (env := env)
     (catName := `term)
     (input := s)
     (fileName := "<stdin>")
 
-
 /-- Parse a syntax object. May generate additional metavariables! -/
-def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do
+def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do
   try
     let expr ← Elab.Term.elabType syn
     return .ok expr
   catch ex => return .error (← ex.toMessageData.toString)
-def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do
+def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElabM (Except String Expr) := do
   try
-    let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .none)
+    let expr ← Elab.Term.elabTerm (stx := syn) expectedType?
     return .ok expr
   catch ex => return .error (← ex.toMessageData.toString)
 
@@ -84,6 +86,8 @@ partial def serialize_sort_level_ast (level: Level) (sanitize: Bool): String :=
 
 /--
  Completely serializes an expression tree. Json not used due to compactness
+
+A `_` symbol in the AST indicates automatic deductions not present in the original expression.
 -/
 partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): MetaM String := do
   self expr
@@ -145,10 +149,13 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
       self inner
     | .proj typeName idx inner => do
       let env ← getEnv
+      let ctor := getStructureCtor env typeName
       let fieldName := getStructureFields env typeName |>.get! idx
       let projectorName := getProjFnForField? env typeName fieldName |>.get!
-      let e := Expr.app (.const  projectorName []) inner
-      self e
+
+      let autos := String.intercalate " " (List.replicate ctor.numParams "_")
+      let inner ← self inner
+      pure s!"((:c {projectorName}) {autos} {inner})"
   -- Elides all unhygenic names
   binder_info_to_ast : Lean.BinderInfo → String
     | .default => ""
@@ -158,14 +165,12 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
   of_name (name: Name) := name_to_ast name sanitize
 
 def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
-  let pp := toString (← Meta.ppExpr e)
-  let pp?: Option String := match options.printExprPretty with
-    | true => .some pp
-    | false => .none
-  let sexp: String ← serialize_expression_ast e
-  let sexp?: Option String := match options.printExprAST with
-    | true => .some sexp
-    | false => .none
+  let pp?: Option String ← match options.printExprPretty with
+    | true => pure $ .some $ toString $ ← Meta.ppExpr e
+    | false => pure $ .none
+  let sexp?: Option String ← match options.printExprAST with
+    | true => pure $ .some $ ← serialize_expression_ast e
+    | false => pure $ .none
   return {
     pp?,
     sexp?
@@ -249,9 +254,7 @@ protected def GoalState.serializeGoals
     MetaM (Array Protocol.Goal):= do
   state.restoreMetaM
   let goals := state.goals.toArray
-  let parentDecl? := parent.bind (λ parentState =>
-    let parentGoal := parentState.goals.get! state.parentGoalId
-    parentState.mctx.findDecl? parentGoal)
+  let parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar?.get!)
   goals.mapM fun goal => do
     match state.mctx.findDecl? goal with
     | .some mvarDecl =>

Pantograph/Version.lean

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

README.md

@@ -1,11 +1,16 @@
 # Pantograph
 
-An interaction system for Lean 4.
+A Machine-to-Machine interaction system for Lean 4.
 
 ![Pantograph](doc/icon.svg)
 
+Pantograph provides interfaces to execute proofs, construct expressions, and
+examine the symbol list of a Lean project for machine learning.
+
 ## Installation
 
+For Nix based workflow, see below.
+
 Install `elan` and `lake`. Execute
 ``` sh
 make build/bin/pantograph
@@ -20,7 +25,7 @@ LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
 ```
 The provided `flake.nix` has a develop environment with Lean already setup.
 
-## Usage
+## Executable Usage
 
 ``` sh
 pantograph MODULES|LEAN_OPTIONS
@@ -63,11 +68,11 @@ stat
 ```
 where the application of `assumption` should lead to a failure.
 
-## Commands
+### Commands
 
 See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON.
 - `reset`: Delete all cached expressions and proof trees
-- `expr.echo {"expr": <expr>}`: Determine the type of an expression and round-trip it
+- `expr.echo {"expr": <expr>, "type": <optional expected type>}`: Determine the type of an expression and round-trip it
 - `env.catalog`: Display a list of all safe Lean symbols in the current environment
 - `env.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
   given symbol; If value flag is set, the value is printed or hidden. By default
@@ -76,13 +81,18 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
 - `options.print`: Display the current set of options
 - `goal.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new goal from a given expression or symbol
-- `goal.tactic {"stateId": <id>, "goalId": <id>, ["tactic": <tactic>], ["expr": <expr>]}`: Execute a tactic string on a given goal
+- `goal.tactic {"stateId": <id>, "goalId": <id>, ["tactic": <tactic>], ["expr":
+  <expr>]}`: Execute a tactic string on a given goal. `tactic` executes an
+  ordinary tactic, `expr` assigns an expression to the current goal, `have`
+  executes the have tactic, ``calc` (of the form `lhs op rhs`) executes one step
+  of `calc`, and `"conv": true`/`"conv": false` enters/exits conversion tactic
+  mode.
 - `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`: Continue from a proof state
 - `goal.remove {"stateIds": [<id>]}"`: Remove a bunch of stored goals.
 - `goal.print {"stateId": <id>}"`: Print a goal state
 - `stat`: Display resource usage
 
-## Errors
+### Errors
 
 When an error pertaining to the execution of a command happens, the returning JSON structure is
 
@@ -97,16 +107,35 @@ Common error forms:
   input of another is broken. For example, attempting to query a symbol not
   existing in the library or indexing into a non-existent proof state.
 
-## Troubleshooting
+### Troubleshooting
 
 If lean encounters stack overflow problems when printing catalog, execute this before running lean:
 ```sh
 ulimit -s unlimited
 ```
 
-## Testing
+## Library Usage
+
+`Pantograph/Library.lean` exposes a series of interfaces which allow FFI call
+with `Pantograph` which mirrors the REPL commands above. It is recommended to
+call Pantograph via this FFI since it provides a tremendous speed up.
+
+## Developing
+
+### Testing
 
 The tests are based on `LSpec`. To run tests,
 ``` sh
 make test
 ```
+
+## Nix based workflow
+
+The included Nix flake provides build targets for `sharedLib` and `executable`.
+The executable can be used as-is, but linking against the shared library
+requires the presence of `lean-all`.
+
+To run tests:
+``` sh
+nix flake check
+```

Test/Common.lean

@@ -1,9 +1,14 @@
-import Pantograph.Protocol
 import Pantograph.Goal
+import Pantograph.Library
+import Pantograph.Protocol
+import Lean
 import LSpec
 
+open Lean
+
 namespace Pantograph
 
+-- Auxiliary functions
 namespace Protocol
 /-- Set internal names to "" -/
 def Goal.devolatilize (goal: Goal): Goal :=
@@ -20,6 +25,9 @@ def Goal.devolatilize (goal: Goal): Goal :=
 deriving instance DecidableEq, Repr for Expression
 deriving instance DecidableEq, Repr for Variable
 deriving instance DecidableEq, Repr for Goal
+deriving instance DecidableEq, Repr for ExprEchoResult
+deriving instance DecidableEq, Repr for InteractionError
+deriving instance DecidableEq, Repr for Option
 end Protocol
 
 def TacticResult.toString : TacticResult → String
@@ -29,18 +37,18 @@ def TacticResult.toString : TacticResult → String
     s!".failure {messages}"
   | .parseError error => s!".parseError {error}"
   | .indexError index => s!".indexError {index}"
+  | .invalidAction error => s!".invalidAction {error}"
 
+namespace Test
+
+def expectationFailure (desc: String) (error: String): LSpec.TestSeq := LSpec.test desc (LSpec.ExpectationFailure "ok _" error)
 def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
 
-open Lean
+def parseFailure (error: String) := expectationFailure "parse" error
+def elabFailure (error: String) := expectationFailure "elab" error
 
-def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq): IO LSpec.TestSeq := do
-  let coreContext: Core.Context := {
-    currNamespace := Name.str .anonymous "Aniva"
-    openDecls := [],     -- No 'open' directives needed
-    fileName := "<Pantograph/Test>",
-    fileMap := { source := "", positions := #[0], lines := #[1] }
-  }
+def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array String := #[]): IO LSpec.TestSeq := do
+  let coreContext: Core.Context ← createCoreContext options
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
   | .error exception =>
     return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
@@ -48,9 +56,8 @@ def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq): IO LSpec.TestSe
 def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
   runCoreMSeq env metaM.run'
 def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
-  termElabM.run' (ctx := {
-    declName? := .none,
-    errToSorry := false,
-  })
+  termElabM.run' (ctx := Pantograph.defaultTermElabMContext)
+
+end Test
 
 end Pantograph

Test/Environment.lean

@@ -2,25 +2,42 @@ import LSpec
 import Pantograph.Serial
 import Pantograph.Environment
 import Test.Common
+import Lean
 
+open Lean
 namespace Pantograph.Test.Environment
 
 open Pantograph
-open Lean
 
 deriving instance DecidableEq, Repr for Protocol.InductInfo
 deriving instance DecidableEq, Repr for Protocol.ConstructorInfo
+deriving instance DecidableEq, Repr for Protocol.RecursorRule
 deriving instance DecidableEq, Repr for Protocol.RecursorInfo
 deriving instance DecidableEq, Repr for Protocol.EnvInspectResult
 
-def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do
+def test_catalog: IO LSpec.TestSeq := do
+  let env: Environment ← importModules
+    (imports := #[`Init])
+    (opts := {})
+    (trustLevel := 1)
+  let inner: CoreM LSpec.TestSeq := do
+    let catalogResult ← Environment.catalog {}
+    let symbolsWithNum := env.constants.fold (init := #[]) (λ acc name info =>
+      match (Environment.toFilteredSymbol name info).isSome && (name matches .num _ _) with
+      | false => acc
+      | true => acc.push name
+      )
+    return LSpec.check "No num symbols" (symbolsWithNum.size == 0)
+  runCoreMSeq env inner
+
+def test_symbol_visibility: IO LSpec.TestSeq := do
   let entries: List (Name × Bool) := [
     ("Nat.add_comm".toName, false),
-    ("Lean.Name".toName, true)
+    ("Lean.Name".toName, true),
+    ("Init.Data.Nat.Basic._auxLemma.4".toName, true),
   ]
   let suite := entries.foldl (λ suites (symbol, target) =>
-    let constant := env.constants.find! symbol
-    let test := LSpec.check symbol.toString ((Environment.is_symbol_unsafe_or_internal symbol constant) == target)
+    let test := LSpec.check symbol.toString ((Environment.isNameInternal symbol) == target)
     LSpec.TestSeq.append suites test) LSpec.TestSeq.done
   return suite
 
@@ -29,7 +46,11 @@ inductive ConstantCat where
   | ctor (info: Protocol.ConstructorInfo)
   | recursor (info: Protocol.RecursorInfo)
 
-def test_inspect (env: Environment): IO LSpec.TestSeq := do
+def test_inspect: IO LSpec.TestSeq := do
+  let env: Environment ← importModules
+    (imports := #[`Init])
+    (opts := {})
+    (trustLevel := 1)
   let testCases: List (String × ConstantCat) := [
     ("Or", ConstantCat.induct {
       numParams := 2,
@@ -49,6 +70,7 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
       numIndices := 1,
       numMotives := 1,
       numMinors := 1,
+      rules := #[{ ctor := "Eq.refl", nFields := 0, rhs := { pp? := .some "fun {α} a motive refl => refl" } }]
       k := true,
     }),
     ("ForM.rec", ConstantCat.recursor {
@@ -57,6 +79,7 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
       numIndices := 0,
       numMotives := 1,
       numMinors := 1,
+      rules := #[{ ctor := "ForM.mk", nFields := 1, rhs := { pp? := .some "fun m γ α motive mk forM => mk forM" } }]
       k := false,
     })
   ]
@@ -74,14 +97,11 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
     ) LSpec.TestSeq.done
   runCoreMSeq env inner
 
-def suite: IO LSpec.TestSeq := do
-  let env: Environment ← importModules
-    (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
-    (opts := {})
-    (trustLevel := 1)
-
-  return LSpec.group "Environment" $
-    (LSpec.group "Symbol visibility" (← test_symbol_visibility env)) ++
-    (LSpec.group "Inspect" (← test_inspect env))
+def suite: List (String × IO LSpec.TestSeq) :=
+  [
+    ("Catalog", test_catalog),
+    ("Symbol Visibility", test_symbol_visibility),
+    ("Inspect", test_inspect),
+  ]
 
 end Pantograph.Test.Environment

Test/Integration.lean

@@ -21,13 +21,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d
   let context: Context := {
     imports := ["Init"]
   }
-  let coreContext: Lean.Core.Context := {
-    currNamespace := Lean.Name.str .anonymous "Aniva"
-    openDecls := [],
-    fileName := "<Test>",
-    fileMap := { source := "", positions := #[0], lines := #[1] },
-    options := Lean.Options.empty
-  }
+  let coreContext: Lean.Core.Context ← createCoreContext #[]
   let commands: MainM LSpec.TestSeq :=
     steps.foldlM (λ suite step => do
       let result ← step
@@ -38,8 +32,18 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d
   catch ex =>
     return LSpec.check s!"Uncaught IO exception: {ex.toString}" false
 
+def test_elab : IO LSpec.TestSeq :=
+  subroutine_runner [
+    subroutine_step "expr.echo"
+      [("expr", .str "λ {α : Sort (u + 1)} => List α")]
+     (Lean.toJson ({
+       type := { pp? := .some "{α : Type u} → Type u" },
+       expr := { pp? := .some "fun {α} => List α" }
+     }: Protocol.ExprEchoResult)),
+  ]
+
 def test_option_modify : IO LSpec.TestSeq :=
-  let pp? := Option.some "∀ (n : Nat), n + 1 = Nat.succ n"
+  let pp? := Option.some "∀ (n : Nat), n + 1 = n.succ"
   let sexp? := Option.some "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))"
   let module? := Option.some "Init.Data.Nat.Basic"
   let options: Protocol.Options := {}
@@ -79,22 +83,22 @@ def test_malformed_command : IO LSpec.TestSeq :=
   ]
 def test_tactic : IO LSpec.TestSeq :=
   let goal1: Protocol.Goal := {
-    name := "_uniq.10",
+    name := "_uniq.11",
     target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
-    vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
+    vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
   }
   let goal2: Protocol.Goal := {
-    name := "_uniq.13",
+    name := "_uniq.14",
     target := { pp? := .some "x ∨ y → y ∨ x" },
     vars := #[
-      { name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
-      { name := "_uniq.12", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
+      { name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
+      { name := "_uniq.13", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
     ],
   }
   subroutine_runner [
     subroutine_step "goal.start"
       [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
-     (Lean.toJson ({stateId := 0, root := "_uniq.8"}:
+     (Lean.toJson ({stateId := 0, root := "_uniq.9"}:
       Protocol.GoalStartResult)),
     subroutine_step "goal.tactic"
       [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
@@ -103,6 +107,12 @@ def test_tactic : IO LSpec.TestSeq :=
        goals? := #[goal1],
      }:
       Protocol.GoalTacticResult)),
+    subroutine_step "goal.print"
+      [("stateId", .num 1)]
+     (Lean.toJson ({
+       parent? := .some { pp? := .some "fun x => ?m.12 x" },
+     }:
+      Protocol.GoalPrintResult)),
     subroutine_step "goal.tactic"
       [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
      (Lean.toJson ({
@@ -112,7 +122,7 @@ def test_tactic : IO LSpec.TestSeq :=
       Protocol.GoalTacticResult))
   ]
 
-def test_env : IO LSpec.TestSeq :=
+def test_env_add_inspect : IO LSpec.TestSeq :=
   let name1 := "Pantograph.mystery"
   let name2 := "Pantograph.mystery2"
   subroutine_runner [
@@ -142,19 +152,20 @@ def test_env : IO LSpec.TestSeq :=
     subroutine_step "env.inspect"
       [("name", .str name2)]
      (Lean.toJson ({
-       value? := .some { pp? := .some "fun a => Int.ofNat a + 1" },
+       value? := .some { pp? := .some "fun a => ↑a + 1" },
        type := { pp? := .some "Nat → Int" },
      }:
       Protocol.EnvInspectResult))
   ]
 
-def suite: IO LSpec.TestSeq := do
-
-  return LSpec.group "Integration" $
-    (LSpec.group "Option modify" (← test_option_modify)) ++
-    (LSpec.group "Malformed command" (← test_malformed_command)) ++
-    (LSpec.group "Tactic" (← test_tactic)) ++
-    (LSpec.group "Env" (← test_env))
+def suite: List (String × IO LSpec.TestSeq) :=
+  [
+    ("Elab", test_elab),
+    ("Option modify", test_option_modify),
+    ("Malformed command", test_malformed_command),
+    ("Tactic", test_tactic),
+    ("env.add env.inspect", test_env_add_inspect),
+  ]
 
 
 end Pantograph.Test.Integration

Test/Library.lean

@@ -0,0 +1,38 @@
+import LSpec
+import Lean
+import Pantograph.Library
+import Test.Common
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Test.Library
+
+def test_expr_echo (env: Environment): IO LSpec.TestSeq := do
+  let inner: CoreM LSpec.TestSeq := do
+    let prop_and_proof := "⟨∀ (x: Prop), x → x, λ (x: Prop) (h: x) => h⟩"
+    let tests := LSpec.TestSeq.done
+    let echoResult ← exprEcho prop_and_proof (options := {})
+    let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
+      type := { pp? := "?m.2" }, expr := { pp? := "?m.3" }
+    }))
+    let echoResult ← exprEcho prop_and_proof (expectedType? := .some "Σ' p:Prop, p") (options := { printExprAST := true })
+    let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
+      type := {
+        pp? := "(p : Prop) ×' p",
+        sexp? := "((:c PSigma) (:sort 0) (:lambda p (:sort 0) 0))",
+      },
+      expr := {
+        pp? := "⟨∀ (x : Prop), x → x, fun x h => h⟩",
+        sexp? := "((:c PSigma.mk) (:sort 0) (:lambda p (:sort 0) 0) (:forall x (:sort 0) (:forall _ 0 1)) (:lambda x (:sort 0) (:lambda h 0 0)))",
+      }
+    }))
+    return tests
+  runCoreMSeq env (options := #["pp.proofs.threshold=100"]) inner
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("expr_echo", test_expr_echo env),
+  ]
+
+end Pantograph.Test.Library

Test/Main.lean

@@ -1,21 +1,53 @@
 import LSpec
 import Test.Environment
-import Test.Holes
 import Test.Integration
+import Test.Library
+import Test.Metavar
 import Test.Proofs
 import Test.Serial
 
+-- Test running infrastructure
+
+namespace Pantograph.Test
+
+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 (filter: Option String) (tests: List (String × IO LSpec.TestSeq)): IO LSpec.TestSeq := do
+  let tests: List (String × IO LSpec.TestSeq) := match filter with
+    | .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))
+  let all := tasks.foldl (λ acc (name, task) =>
+    let v: Except IO.Error LSpec.TestSeq := Task.get task
+    match v with
+    | .ok case => acc ++ (LSpec.group name case)
+    | .error e => acc ++ (expectationFailure name e.toString)
+    ) LSpec.TestSeq.done
+  return all
+
+end Pantograph.Test
+
 open Pantograph.Test
 
-def main := do
+/-- Main entry of tests; Provide an argument to filter tests by prefix -/
+def main (args: List String) := do
+  let name_filter := args.head?
   Lean.initSearchPath (← Lean.findSysroot)
+  let env_default: Lean.Environment ← Lean.importModules
+    (imports := #[`Init])
+    (opts := {})
+    (trustLevel := 1)
 
-  let suites := [
-    Holes.suite,
-    Integration.suite,
-    Proofs.suite,
-    Serial.suite,
-    Environment.suite
+  let suites: List (String × List (String × IO LSpec.TestSeq)) := [
+    ("Environment", Environment.suite),
+    ("Integration", Integration.suite),
+    ("Library", Library.suite env_default),
+    ("Metavar", Metavar.suite env_default),
+    ("Proofs", Proofs.suite env_default),
+    ("Serial", Serial.suite env_default),
   ]
-  let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done
-  LSpec.lspecIO $ all
+  let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
+  LSpec.lspecIO (← runTestGroup name_filter tests)

Test/Metavar.lean

@@ -2,26 +2,48 @@ import LSpec
 import Pantograph.Goal
 import Pantograph.Serial
 import Test.Common
+import Lean
 
-namespace Pantograph.Test.Holes
+namespace Pantograph.Test.Metavar
 open Pantograph
 open Lean
 
-abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M)
+abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM)
 
 def addTest (test: LSpec.TestSeq): TestM Unit := do
   set $ (← get) ++ test
 
+-- Tests that all delay assigned mvars are instantiated
+def test_instantiate_mvar: TestM Unit := do
+  let env ← Lean.MonadEnv.getEnv
+  let value := "@Nat.le_trans 2 2 5 (@of_eq_true (@LE.le Nat instLENat 2 2) (@eq_true (@LE.le Nat instLENat 2 2) (@Nat.le_refl 2))) (@of_eq_true (@LE.le Nat instLENat 2 5) (@eq_true_of_decide (@LE.le Nat instLENat 2 5) (@Nat.decLe 2 5) (@Eq.refl Bool Bool.true)))"
+  let syn ← match parseTerm env value with
+    | .ok s => pure $ s
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let expr ← match ← elabTerm syn with
+    | .ok expr => pure $ expr
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let t ← Lean.Meta.inferType expr
+  addTest $ LSpec.check "typing" ((toString (← serialize_expression_ast t)) =
+    "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))")
+  return ()
+
+
+
 def startProof (expr: String): TestM (Option GoalState) := do
   let env ← Lean.MonadEnv.getEnv
-  let syn? := syntax_from_str env expr
+  let syn? := parseTerm env expr
   addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
   match syn? with
   | .error error =>
     IO.println error
     return Option.none
   | .ok syn =>
-    let expr? ← syntax_to_expr_type syn
+    let expr? ← elabType syn
     addTest $ LSpec.check s!"Elaborating" expr?.isOk
     match expr? with
     | .error error =>
@@ -44,16 +66,8 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O
 def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
   let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
 
-  let coreContext: Lean.Core.Context := {
-    currNamespace := Name.append .anonymous "Aniva",
-    openDecls := [],     -- No 'open' directives needed
-    fileName := "<Pantograph>",
-    fileMap := { source := "", positions := #[0], lines := #[1] }
-  }
-  let metaM := termElabM.run' (ctx := {
-    declName? := some "_pantograph",
-    errToSorry := false
-  })
+  let coreContext: Lean.Core.Context ← createCoreContext #[]
+  let metaM := termElabM.run' (ctx := defaultTermElabMContext)
   let coreM := metaM.run'
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
   | .error exception =>
@@ -70,7 +84,7 @@ def test_m_couple: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -79,7 +93,7 @@ def test_m_couple: TestM Unit := do
     #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
   addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
   -- Set m to 3
-  let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 3") with
+  let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "exact 3") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -93,6 +107,63 @@ def test_m_couple: TestM Unit := do
   addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ 3", .some "3 ≤ 5"])
   addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+
+def test_m_couple_simp: TestM Unit := do
+  let state? ← startProof "(2: Nat) ≤ 5"
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with
+    | .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"])
+  let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "exact 2") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
+  let state1b ← match state2.continue state1 with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  addTest $ LSpec.check "exact 2" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "2 ≤ 2", .some "2 ≤ 5"])
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+  let state3 ← match ← state1b.tryTactic (goalId := 0) (tactic := "simp") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let state4 ← match state3.continue state1b with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  let state5 ← match ← state4.tryTactic (goalId := 0) (tactic := "simp") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+
+  state5.restoreMetaM
+  let root ← match state5.rootExpr? with
+    | .some e => pure e
+    | .none =>
+      addTest $ assertUnreachable "(5 root)"
+      return ()
+  let rootStr: String := toString (← Lean.Meta.ppExpr root)
+  addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (Init.Data.Nat.Basic._auxLemma.4 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
+  let unfoldedRoot ←  unfoldAuxLemmas root
+  addTest $ LSpec.check "(5 root)" ((toString (← Lean.Meta.ppExpr unfoldedRoot)) =
+    "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
   return ()
 
 def test_proposition_generation: TestM Unit := do
@@ -103,7 +174,7 @@ def test_proposition_generation: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply PSigma.mk") with
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply PSigma.mk") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -145,7 +216,7 @@ def test_partial_continuation: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -153,7 +224,7 @@ def test_partial_continuation: TestM Unit := do
   addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
 
-  let state2 ← match ← state1.execute (goalId := 2) (tactic := "apply Nat.succ") with
+  let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "apply Nat.succ") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -169,7 +240,7 @@ def test_partial_continuation: TestM Unit := do
       return ()
     | .ok state => pure state
   addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
+    #[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
   addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
 
   -- Roundtrip
@@ -183,7 +254,7 @@ def test_partial_continuation: TestM Unit := do
       return ()
     | .ok state => pure state
   addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
+    #[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
   addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
 
   -- Continuation should fail if the state does not exist:
@@ -197,21 +268,14 @@ def test_partial_continuation: TestM Unit := do
   return ()
 
 
-def suite: IO LSpec.TestSeq := do
-  let env: Lean.Environment ← Lean.importModules
-    (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
-    (opts := {})
-    (trustLevel := 1)
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
+    ("Instantiate", test_instantiate_mvar),
     ("2 < 5", test_m_couple),
+    ("2 < 5", test_m_couple_simp),
     ("Proposition Generation", test_proposition_generation),
     ("Partial Continuation", test_partial_continuation)
   ]
-  let tests ← tests.foldlM (fun acc tests => do
-    let (name, tests) := tests
-    let tests ← proofRunner env tests
-    return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
+  tests.map (fun (name, test) => (name, proofRunner env test))
 
-  return LSpec.group "Holes" tests
-
-end Pantograph.Test.Holes
+end Pantograph.Test.Metavar

Test/Proofs.lean

@@ -14,7 +14,7 @@ inductive Start where
   | copy (name: String) -- Start from some name in the environment
   | expr (expr: String) -- Start from some expression
 
-abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M)
+abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM)
 
 def addTest (test: LSpec.TestSeq): TestM Unit := do
   set $ (← get) ++ test
@@ -32,14 +32,14 @@ def startProof (start: Start): TestM (Option GoalState) := do
     | .none =>
       return Option.none
   | .expr expr =>
-    let syn? := syntax_from_str env expr
+    let syn? := parseTerm env expr
     addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
     match syn? with
     | .error error =>
       IO.println error
       return Option.none
     | .ok syn =>
-      let expr? ← syntax_to_expr_type syn
+      let expr? ← elabType syn
       addTest $ LSpec.check s!"Elaborating" expr?.isOk
       match expr? with
       | .error error =>
@@ -62,16 +62,8 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O
 def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
   let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
 
-  let coreContext: Lean.Core.Context := {
-    currNamespace := Name.append .anonymous "Aniva",
-    openDecls := [],     -- No 'open' directives needed
-    fileName := "<Pantograph>",
-    fileMap := { source := "", positions := #[0], lines := #[1] }
-  }
-  let metaM := termElabM.run' (ctx := {
-    declName? := some "_pantograph",
-    errToSorry := false
-  })
+  let coreContext: Lean.Core.Context ← createCoreContext #[]
+  let metaM := termElabM.run' (ctx := defaultTermElabMContext)
   let coreM := metaM.run'
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
   | .error exception =>
@@ -83,7 +75,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
 example: ∀ (a b: Nat), a + b = b + a := by
   intro n m
   rw [Nat.add_comm]
-def proof_nat_add_comm (manual: Bool): TestM Unit := do
+def test_nat_add_comm (manual: Bool): TestM Unit := do
   let state? ← startProof <| match manual with
     | false => .copy "Nat.add_comm"
     | true => .expr "∀ (a b: Nat), a + b = b + a"
@@ -94,7 +86,7 @@ def proof_nat_add_comm (manual: Bool): TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro n m") with
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro n m") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -102,13 +94,13 @@ def proof_nat_add_comm (manual: Bool): TestM Unit := do
   addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"])
 
-  match ← state1.execute (goalId := 0) (tactic := "assumption") with
+  match ← state1.tryTactic (goalId := 0) (tactic := "assumption") with
   | .failure #[message] =>
     addTest $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
   | other => do
     addTest $ assertUnreachable $ other.toString
 
-  let state2 ← match ← state1.execute (goalId := 0) (tactic := "rw [Nat.add_comm]") with
+  let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "rw [Nat.add_comm]") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -116,7 +108,7 @@ def proof_nat_add_comm (manual: Bool): TestM Unit := do
   addTest $ LSpec.test "rw [Nat.add_comm]" state2.goals.isEmpty
 
   return ()
-def proof_delta_variable: TestM Unit := do
+def test_delta_variable: TestM Unit := do
   let options: Protocol.Options := { noRepeat := true }
   let state? ← startProof <| .expr "∀ (a b: Nat), a + b = b + a"
   addTest $ LSpec.check "Start goal" state?.isSome
@@ -126,14 +118,14 @@ def proof_delta_variable: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro n") with
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro n") with
     | .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.execute (goalId := 0) (tactic := "intro m") with
+  let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "intro m") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -157,7 +149,7 @@ example (w x y z : Nat) (p : Nat → Prop)
         (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
   simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *
   assumption
-def proof_arith: TestM Unit := do
+def test_arith: TestM Unit := do
   let state? ← startProof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)")
   let state0 ← match state? with
     | .some state => pure state
@@ -165,26 +157,28 @@ def proof_arith: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "intros") with
+  let tactic := "intros"
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check "intros" (state1.goals.length = 1)
+  addTest $ LSpec.check tactic (state1.goals.length = 1)
   addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
-  let state2 ← match ← state1.execute (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
+  let state2 ← match ← state1.tryTactic (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
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "simp ..." (state2.goals.length = 1)
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
-  let state3 ← match ← state2.execute (goalId := 0) (tactic := "assumption") with
+  let tactic := "assumption"
+  let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.test "assumption" state3.goals.isEmpty
+  addTest $ LSpec.test tactic state3.goals.isEmpty
   addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
   return ()
 
@@ -203,7 +197,7 @@ example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
     assumption
   . apply Or.inl
     assumption
-def proof_or_comm: TestM Unit := do
+def test_or_comm: TestM Unit := do
   let state? ← startProof (.expr "∀ (p q: Prop), p ∨ q → q ∨ p")
   let state0 ← match state? with
     | .some state => pure state
@@ -213,21 +207,24 @@ def proof_or_comm: TestM Unit := do
   addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone
   addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone
 
-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") with
+  let tactic := "intro p q h"
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
+  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"])
   addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
   addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
-  let state2 ← match ← state1.execute (goalId := 0) (tactic := "cases h") with
+
+  let tactic := "cases h"
+  let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check "cases h" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
+  addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[branchGoal "inl" "p", branchGoal "inr" "q"])
   addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
@@ -235,32 +232,32 @@ def proof_or_comm: TestM Unit := do
   let state2parent ← serialize_expression_ast state2.parentExpr?.get! (sanitize := false)
   -- This is due to delayed assignment
   addTest $ LSpec.test "(2 parent)" (state2parent ==
-    "((:mv _uniq.45) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
+    "((:mv _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
 
-  let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with
+  let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   let state3_1parent ← serialize_expression_ast state3_1.parentExpr?.get! (sanitize := false)
-  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.83))")
+  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.78))")
   addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
-  let state4_1 ← match ← state3_1.execute (goalId := 0) (tactic := "assumption") with
+  let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
   let state4_1parent ← serialize_expression_ast state4_1.parentExpr?.get! (sanitize := false)
-  addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.49)")
+  addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.47)")
   addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
-  let state3_2 ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with
+  let state3_2 ← match ← state2.tryTactic (goalId := 1) (tactic := "apply Or.inl") with
     | .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.execute (goalId := 0) (tactic := "assumption") with
+  let state4_2 ← match ← state3_2.tryTactic (goalId := 0) (tactic := "assumption") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -274,13 +271,13 @@ def proof_or_comm: TestM Unit := do
       return ()
     | .ok state => pure state
   addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals.get! 0])
-  let state3_1 ← match ← state2b.execute (goalId := 0) (tactic := "apply Or.inr") with
+  let state3_1 ← match ← state2b.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
     | .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.execute (goalId := 0) (tactic := "assumption") with
+  let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -301,24 +298,268 @@ def proof_or_comm: TestM Unit := do
       ]
     }
 
+def test_have: TestM Unit := do
+  let state? ← startProof (.expr "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+  let tactic := "intro p q h"
+  let state1 ← match ← state0.tryTactic (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 [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"])
 
-def suite: IO LSpec.TestSeq := do
-  let env: Lean.Environment ← Lean.importModules
-    (imports := #[{ module := Name.append .anonymous "Init", runtimeOnly := false}])
-    (opts := {})
-    (trustLevel := 1)
+  let expr := "Or.inl (Or.inl h)"
+  let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[])
+
+  let haveBind := "y"
+  let haveType := "p ∨ q"
+  let state2 ← match ← state1.tryHave (goalId := 0) (binderName := haveBind) (type := haveType) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"have {haveBind}: {haveType}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[
+      buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "p ∨ q",
+      buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p"), ("y", "p ∨ q")] "(p ∨ q) ∨ p ∨ q"
+    ])
+
+  let expr := "Or.inl h"
+  let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[])
+
+  let state2b ← match state3.continue state2 with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let expr := "Or.inl y"
+  let state4 ← match ← state2b.tryAssign (goalId := 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[])
+
+  addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome
+
+example : ∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2 := by
+  intro a b c1 c2 h
+  conv =>
+    lhs
+    congr
+    . rw [Nat.add_comm]
+    . rfl
+  exact h
+
+def test_conv: TestM Unit := do
+  let state? ← startProof (.expr "∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let tactic := "intro a b c1 c2 h"
+  let state1 ← match ← state0.tryTactic (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) =
+    #[interiorGoal [] "a + b + c1 = b + a + c2"])
+
+  let state2 ← match ← state1.conv (goalId := 0) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }])
+
+  let convTactic := "rhs"
+  let state3R ← match ← state2.tryTactic (goalId := 0) convTactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  {convTactic} (discard)" ((← state3R.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[{ interiorGoal [] "b + a + c2" with isConversion := true }])
+
+  let convTactic := "lhs"
+  let state3L ← match ← state2.tryTactic (goalId := 0) convTactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  {convTactic}" ((← state3L.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[{ interiorGoal [] "a + b + c1" with isConversion := true }])
+
+  let convTactic := "congr"
+  let state4 ← match ← state3L.tryTactic (goalId := 0) convTactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  {convTactic}" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[
+      { interiorGoal [] "a + b" with isConversion := true, userName? := .some "a" },
+      { interiorGoal [] "c1" with isConversion := true, userName? := .some "a" }
+    ])
+
+  let convTactic := "rw [Nat.add_comm]"
+  let state5_1 ← match ← state4.tryTactic (goalId := 0) convTactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  · {convTactic}" ((← state5_1.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }])
+
+  let convTactic := "rfl"
+  let state6_1 ← match ← state5_1.tryTactic (goalId := 0) convTactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"    {convTactic}" ((← state6_1.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[])
+
+  let state4_1 ← match state6_1.continue state4 with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ expectationFailure "continue" e
+      return ()
+
+  let convTactic := "rfl"
+  let state6 ← match ← state4_1.tryTactic (goalId := 0) convTactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  · {convTactic}" ((← state6.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[])
+
+  let state1_1 ← match ← state6.convExit with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+
+  let tactic := "exact h"
+  let stateF ← match ← state1_1.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← stateF.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[])
+
+  where
+    h := "b + a + c1 = b + a + c2"
+    interiorGoal (free: List (String × String)) (target: String) :=
+      let free := [("a", "Nat"), ("b", "Nat"), ("c1", "Nat"), ("c2", "Nat"), ("h", h)] ++ free
+      buildGoal free target
+
+example : ∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d := by
+  intro a b c d h1 h2
+  calc a + b = b + c := by apply h1
+    _ = c + d := by apply h2
+
+def test_calc: TestM Unit := do
+  let state? ← startProof (.expr "∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+  let tactic := "intro a b c d h1 h2"
+  let state1 ← match ← state0.tryTactic (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) =
+    #[interiorGoal [] "a + b = c + d"])
+  let pred := "a + b = b + c"
+  let state2 ← match ← state1.tryCalc (goalId := 0) (pred := pred) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"calc {pred} := _" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[
+      interiorGoal [] "a + b = b + c" (.some "calc"),
+      interiorGoal [] "b + c = c + d"
+    ])
+
+  let tactic := "apply h1"
+  let state2m ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let state3 ← match state2m.continue state2 with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ expectationFailure "continue" e
+      return ()
+  let pred := "_ = c + d"
+  let state4 ← match ← state3.tryCalc (goalId := 0) (pred := pred) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"calc {pred} := _" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[
+      interiorGoal [] "b + c = c + d" (.some "calc")
+    ])
+  let tactic := "apply h2"
+  let state4m ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome
+
+
+  where
+    interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) :=
+      let free := [("a", "Nat"), ("b", "Nat"), ("c", "Nat"), ("d", "Nat"),
+        ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
+      buildGoal free target userName?
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
-    ("Nat.add_comm", proof_nat_add_comm false),
-    ("Nat.add_comm manual", proof_nat_add_comm true),
-    ("Nat.add_comm delta", proof_delta_variable),
-    ("arithmetic", proof_arith),
-    ("Or.comm", proof_or_comm)
+    ("Nat.add_comm", test_nat_add_comm false),
+    ("Nat.add_comm manual", test_nat_add_comm true),
+    ("Nat.add_comm delta", test_delta_variable),
+    ("arithmetic", test_arith),
+    ("Or.comm", test_or_comm),
+    ("have", test_have),
+    ("conv", test_conv),
+    ("calc", test_calc),
   ]
-  let tests ← tests.foldlM (fun acc tests => do
-    let (name, tests) := tests
-    let tests ← proofRunner env tests
-    return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
+  tests.map (fun (name, test) => (name, proofRunner env test))
+
 
-  return LSpec.group "Proofs" tests
 
 end Pantograph.Test.Proofs

Test/Serial.lean

@@ -1,11 +1,12 @@
 import LSpec
 import Pantograph.Serial
 import Test.Common
+import Lean
 
+open Lean
 namespace Pantograph.Test.Serial
 
 open Pantograph
-open Lean
 
 deriving instance Repr, DecidableEq for Protocol.BoundExpression
 
@@ -20,14 +21,13 @@ def test_name_to_ast: LSpec.TestSeq :=
 def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
   let entries: List (Name × Protocol.BoundExpression) := [
     ("Nat.add_comm".toName, { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }),
-    ("Nat.le_of_succ_le".toName, { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "Nat.succ n ≤ m")], target := "n ≤ m" })
+    ("Nat.le_of_succ_le".toName, { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "n.succ ≤ m")], target := "n ≤ m" })
   ]
-  let coreM: CoreM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
+  runCoreMSeq env $ entries.foldlM (λ suites (symbol, target) => do
     let env ← MonadEnv.getEnv
     let expr := env.find? symbol |>.get! |>.type
     let test := LSpec.check symbol.toString ((← type_expr_to_bound expr) = target)
     return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run'
-  runCoreMSeq env coreM
 
 def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
   let entries: List (String × String) := [
@@ -40,51 +40,67 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
     ("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"),
     ("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))")
   ]
-  let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
+  runMetaMSeq env $ entries.foldlM (λ suites (symbol, target) => do
     let env ← MonadEnv.getEnv
     let expr := env.find? symbol.toName |>.get! |>.type
     let test := LSpec.check symbol ((← serialize_expression_ast expr) = target)
     return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
-  runMetaMSeq env metaM
 
-def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
+def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
   let entries: List (String × String) := [
     ("λ x: Nat × Bool => x.1", "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
-    ("λ x: Array Nat => x.data", "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))")
+    ("λ x: Array Nat => x.data", "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
+    -- This tests `autoBoundImplicit`
+    ("λ {α : Sort (u + 1)} => List α", "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"),
   ]
   let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do
     let env ← MonadEnv.getEnv
-    let s := syntax_from_str env source |>.toOption |>.get!
-    let expr := (← syntax_to_expr s) |>.toOption |>.get!
+    let s ← match parseTerm env source with
+      | .ok s => pure s
+      | .error e => return parseFailure e
+    let expr ← match (← elabTerm s) with
+      | .ok expr => pure expr
+      | .error e => return elabFailure e
     let test := LSpec.check source ((← serialize_expression_ast expr) = target)
     return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
-  let metaM := termElabM.run' (ctx := {
-    declName? := some "_pantograph",
-    errToSorry := false
-  })
-  runMetaMSeq env metaM
+  runMetaMSeq env $ termElabM.run' (ctx := defaultTermElabMContext)
+
+def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
+  let entries: List (Expr × String) := [
+    (.lam `p (.sort .zero)
+        (.lam `q (.sort .zero)
+          (.lam `k (mkApp2 (.const `And []) (.bvar 1) (.bvar 0))
+            (.proj `And 1 (.bvar 0))
+            .default)
+        .implicit)
+      .implicit,
+      "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :implicit) :implicit)"
+    ),
+  ]
+  let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do
+    let env ← MonadEnv.getEnv
+    let testCaseName := target.take 10
+    let test := LSpec.check   testCaseName ((← serialize_expression_ast expr) = target)
+    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
+  runMetaMSeq env $ termElabM.run' (ctx := defaultTermElabMContext)
 
 -- Instance parsing
-def test_instance (env: Environment): IO LSpec.TestSeq := do
-  let metaM: MetaM LSpec.TestSeq := do
+def test_instance (env: Environment): IO LSpec.TestSeq :=
+  runMetaMSeq env do
     let env ← MonadEnv.getEnv
     let source := "λ x y: Nat => HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) x y"
-    let s := syntax_from_str env source |>.toOption |>.get!
-    let _expr := (← runTermElabMInMeta <| syntax_to_expr s) |>.toOption |>.get!
+    let s := parseTerm env source |>.toOption |>.get!
+    let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get!
     return LSpec.TestSeq.done
-  runMetaMSeq env metaM
 
-def suite: IO LSpec.TestSeq := do
-  let env: Environment ← importModules
-    (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
-    (opts := {})
-    (trustLevel := 1)
-
-  return LSpec.group "Serialization" $
-    (LSpec.group "name_to_ast" test_name_to_ast) ++
-    (LSpec.group "Expression binder" (← test_expr_to_binder env)) ++
-    (LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env)) ++
-    (LSpec.group "Sexp from expr" (← test_sexp_of_expr env)) ++
-    (LSpec.group "Instance" (← test_instance env))
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("name_to_ast", do pure test_name_to_ast),
+    ("Expression binder", test_expr_to_binder env),
+    ("Sexp from symbol", test_sexp_of_symbol env),
+    ("Sexp from elaborated expr", test_sexp_of_elab env),
+    ("Sexp from expr", test_sexp_of_expr env),
+    ("Instance", test_instance env),
+  ]
 
 end Pantograph.Test.Serial

flake.lock

@@ -5,11 +5,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1696343447,
-        "narHash": "sha256-B2xAZKLkkeRFG5XcHHSXXcP7To9Xzr59KXeZiRf4vdQ=",
+        "lastModified": 1709336216,
+        "narHash": "sha256-Dt/wOWeW6Sqm11Yh+2+t0dfEWxoMxGBvv3JpIocFl9E=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "c9afaba3dfa4085dbd2ccb38dfade5141e33d9d4",
+        "rev": "f7b3c975cf067e56e7cda6cb098ebe3fb4d74ca2",
         "type": "github"
       },
       "original": {
@@ -38,19 +38,20 @@
         "flake-utils": "flake-utils",
         "lean4-mode": "lean4-mode",
         "nix": "nix",
-        "nixpkgs": "nixpkgs_2"
+        "nixpkgs": "nixpkgs_2",
+        "nixpkgs-old": "nixpkgs-old"
       },
       "locked": {
-        "lastModified": 1710520221,
-        "narHash": "sha256-8Fm4bj9sqqsUHFZweSdGMM5GdUX3jkGK/ggGq27CeQc=",
+        "lastModified": 1711508550,
+        "narHash": "sha256-UK4DnYmwXLcqHA316Zkn0cnujdYlxqUf+b6S4l56Q3s=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "f70895ede54501adf0db77474f452a7fef40d0b3",
+        "rev": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
         "type": "github"
       },
       "original": {
         "owner": "leanprover",
-        "ref": "f70895ede54501adf0db77474f452a7fef40d0b3",
+        "ref": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
         "repo": "lean4",
         "type": "github"
       }
@@ -87,6 +88,23 @@
         "type": "github"
       }
     },
+    "lspec": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1701971219,
+        "narHash": "sha256-HYDRzkT2UaLDrqKNWesh9C4LJNt0JpW0u68wYVj4Byw=",
+        "owner": "lurk-lab",
+        "repo": "LSpec",
+        "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+        "type": "github"
+      },
+      "original": {
+        "owner": "lurk-lab",
+        "ref": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+        "repo": "LSpec",
+        "type": "github"
+      }
+    },
     "nix": {
       "inputs": {
         "lowdown-src": "lowdown-src",
@@ -126,11 +144,11 @@
     "nixpkgs-lib": {
       "locked": {
         "dir": "lib",
-        "lastModified": 1696019113,
-        "narHash": "sha256-X3+DKYWJm93DRSdC5M6K5hLqzSya9BjibtBsuARoPco=",
+        "lastModified": 1709237383,
+        "narHash": "sha256-cy6ArO4k5qTx+l5o+0mL9f5fa86tYUX3ozE1S+Txlds=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "f5892ddac112a1e9b3612c39af1b72987ee5783a",
+        "rev": "1536926ef5621b09bba54035ae2bb6d806d72ac8",
         "type": "github"
       },
       "original": {
@@ -141,6 +159,23 @@
         "type": "github"
       }
     },
+    "nixpkgs-old": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1581379743,
+        "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-19.03",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
     "nixpkgs-regression": {
       "locked": {
         "lastModified": 1643052045,
@@ -175,11 +210,11 @@
     },
     "nixpkgs_3": {
       "locked": {
-        "lastModified": 1697456312,
-        "narHash": "sha256-roiSnrqb5r+ehnKCauPLugoU8S36KgmWraHgRqVYndo=",
+        "lastModified": 1711703276,
+        "narHash": "sha256-iMUFArF0WCatKK6RzfUJknjem0H9m4KgorO/p3Dopkk=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "ca012a02bf8327be9e488546faecae5e05d7d749",
+        "rev": "d8fe5e6c92d0d190646fb9f1056741a229980089",
         "type": "github"
       },
       "original": {
@@ -193,6 +228,7 @@
       "inputs": {
         "flake-parts": "flake-parts",
         "lean": "lean",
+        "lspec": "lspec",
         "nixpkgs": "nixpkgs_3"
       }
     }

flake.nix

@@ -4,7 +4,14 @@
   inputs = {
     nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean.url = "github:leanprover/lean4?ref=f70895ede54501adf0db77474f452a7fef40d0b3";
+    lean = {
+      url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2";
+      # Do not follow input's nixpkgs since it could cause build failures
+    };
+    lspec = {
+      url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114";
+      flake = false;
+    };
   };
 
   outputs = inputs @ {
@@ -12,6 +19,7 @@
     nixpkgs,
     flake-parts,
     lean,
+    lspec,
     ...
   } : flake-parts.lib.mkFlake { inherit inputs; } {
     flake = {
@@ -22,10 +30,34 @@
     ];
     perSystem = { system, pkgs, ... }: let
       leanPkgs = lean.packages.${system};
+      lspecLib = leanPkgs.buildLeanPackage {
+        name = "LSpec";
+        roots = [ "Main" "LSpec" ];
+        src = "${lspec}";
+      };
       project = leanPkgs.buildLeanPackage {
         name = "Pantograph";
         roots = [ "Main" "Pantograph" ];
-        src = ./.;
+        src = pkgs.lib.cleanSourceWith {
+          src = ./.;
+          filter = path: type:
+            !(pkgs.lib.hasInfix "/Test/" path) &&
+            !(pkgs.lib.hasSuffix ".md" path) &&
+            !(pkgs.lib.hasSuffix "Makefile" path);
+        };
+      };
+      test = leanPkgs.buildLeanPackage {
+        name = "Test";
+        # NOTE: The src directory must be ./. since that is where the import
+        # root begins (e.g. `import Test.Environment` and not `import
+        # Environment`) and thats where `lakefile.lean` resides.
+        roots = [ "Test.Main" ];
+        deps = [ lspecLib project ];
+        src = pkgs.lib.cleanSourceWith {
+          src = ./.;
+          filter = path: type:
+            !(pkgs.lib.hasInfix "Pantograph" path);
+        };
       };
     in rec {
       packages = {
@@ -33,7 +65,17 @@
         inherit (project) sharedLib executable;
         default = project.executable;
       };
-      devShells.default = project.devShell;
+      checks = {
+        test = pkgs.runCommand "test" {
+          buildInputs = [ test.executable leanPkgs.lean-all ];
+        } ''
+          #export LEAN_SRC_PATH="${./.}"
+          ${test.executable}/bin/test > $out
+        '';
+      };
+      devShells.default = pkgs.mkShell {
+        buildInputs = [ leanPkgs.lean-all leanPkgs.lean ];
+      };
     };
   };
 }

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:4.7.0-rc2
+leanprover/lean4:nightly-2024-03-27