aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 15 Pull Requests 3 Packages Projects Releases Wiki Activity

Merge pull request 'feat(goal): Add unshielded tactic execution mode' (#219) from goal/automatic-mode into dev 

Reviewed-on: #219
This commit is contained in:
Leni Aniva 2025-06-26 15:52:16 -07:00
parent 3e266dc505 9a9659fdb2
commit 7c300e081d
14 changed files with 707 additions and 493 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
Pantograph/Delate.lean
View File

@ -454,7 +454,6 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.
dependentMVars?,
}
/-- Adapted from ppGoal -/
def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
: MetaM Protocol.Goal := do
@ -520,7 +519,6 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
return {
name := goal.name.toString,
userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
isConversion := isLHSGoal? mvarDecl.type |>.isSome,
target := (← serializeExpression options (← instantiate mvarDecl.type)),
vars := vars.reverse.toArray
}
@ -530,17 +528,20 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
protected def GoalState.serializeGoals
(state: GoalState)
(parent: Option GoalState := .none)
(options: @&Protocol.Options := {}):
MetaM (Array Protocol.Goal):= do
state.restoreMetaM
let goals := state.goals.toArray
let parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar?.get!)
goals.mapM fun goal => do
let fragment := match state.fragments[goal]? with
| .none => .tactic
| .some $ .calc .. => .calc
| .some $ .conv .. => .conv
| .some $ .convSentinel .. => .conv
match state.mctx.findDecl? goal with
| .some mvarDecl =>
let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := parentDecl?)
pure serializedGoal
let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := .none)
pure { serializedGoal with fragment }
| .none => throwError s!"Metavariable does not exist in context {goal.name}"
/-- Print the metavariables in a readable format -/
@ -606,7 +607,9 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState :
userNameToString : Name → String
| .anonymous => ""
| other => s!"[{other}]"
parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
parentHasMVar (mvarId: MVarId): Bool := match parent? with
| .some state => state.mctx.decls.contains mvarId
| .none => true
initialize
registerTraceClass `Pantograph.Delate

264
Pantograph/Goal.lean
View File

@ -10,22 +10,69 @@ import Lean
namespace Pantograph
open Lean
/-- The acting area of a tactic -/
inductive Site where
-- Dormant all other goals
| focus (goal : MVarId)
-- Move the goal to the first in the list
| prefer (goal : MVarId)
-- Execute as-is, no goals go dormant
| unfocus
deriving BEq, Inhabited
instance : Coe MVarId Site where
coe := .focus
instance : ToString Site where
toString
| .focus { name } => s!"[{name}]"
| .prefer { name } => s!"[{name},...]"
| .unfocus => "[*]"
/-- Executes a `TacticM` on a site and return affected goals -/
protected def Site.runTacticM (site : Site)
{ m } [Monad m] [MonadLiftT Elab.Tactic.TacticM m] [MonadControlT Elab.Tactic.TacticM m] [MonadMCtx m] [MonadError m]
(f : m α) : m (α × List MVarId) :=
match site with
| .focus goal => do
Elab.Tactic.setGoals [goal]
let a ← f
return (a, [goal])
| .prefer goal => do
let before ← Elab.Tactic.getUnsolvedGoals
let otherGoals := before.filter (· != goal)
Elab.Tactic.setGoals (goal :: otherGoals)
let a ← f
let after ← Elab.Tactic.getUnsolvedGoals
let parents := before.filter (¬ after.contains ·)
Elab.Tactic.pruneSolvedGoals
return (a, parents)
| .unfocus => do
let before ← Elab.Tactic.getUnsolvedGoals
let a ← f
let after ← Elab.Tactic.getUnsolvedGoals
let parents := before.filter (¬ after.contains ·)
Elab.Tactic.pruneSolvedGoals
return (a, parents)
/--
Represents an interconnected set of metavariables, or a state in proof search
Kernel view of the state of a proof
-/
structure GoalState where
-- Captured `TacticM` state
savedState : Elab.Tactic.SavedState
-- The root hole which is the search target
-- The root goal which is the search target
root: MVarId
-- Parent state metavariable source
parentMVar?: Option MVarId := .none
-- Parent goals assigned to produce this state
parentMVars : List MVarId := []
-- Any goal associated with a fragment has a partial tactic which has not
-- finished executing.
fragments : FragmentMap := .empty
def throwNoGoals { m α } [Monad m] [MonadError m] : m α := throwError "no goals to be solved"
@[export pantograph_goal_state_create_m]
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.
@ -39,7 +86,6 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
return {
root := root.mvarId!,
savedState,
parentMVar? := .none,
}
@[export pantograph_goal_state_create_from_mvars_m]
protected def GoalState.createFromMVars (goals: List MVarId) (root: MVarId): MetaM GoalState := do
@ -48,10 +94,19 @@ protected def GoalState.createFromMVars (goals: List MVarId) (root: MVarId): Met
return {
root,
savedState,
parentMVar? := .none,
}
@[always_inline]
protected def GoalState.goals (state: GoalState): List MVarId :=
state.savedState.tactic.goals
@[always_inline]
protected def GoalState.mainGoal? (state : GoalState) : Option MVarId :=
state.goals.head?
@[always_inline]
protected def GoalState.actingGoal? (state : GoalState) (site : Site) : Option MVarId := do
match site with
| .focus goal | .prefer goal => return goal
| .unfocus => state.mainGoal?
@[export pantograph_goal_state_goals]
protected def GoalState.goalsArray (state: GoalState): Array MVarId := state.goals.toArray
protected def GoalState.mctx (state: GoalState): MetavarContext :=
@ -63,8 +118,10 @@ protected def GoalState.env (state: GoalState): Environment :=
protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): Option Meta.Context := do
let mvarDecl ← state.mctx.findDecl? mvarId
return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances }
@[always_inline]
protected def GoalState.metaState (state: GoalState): Meta.State :=
state.savedState.term.meta.meta
@[always_inline]
protected def GoalState.coreState (state: GoalState): Core.SavedState :=
state.savedState.term.meta.core
@ -72,18 +129,18 @@ protected def GoalState.withContext' (state: GoalState) (mvarId: MVarId) (m: Met
mvarId.withContext m |>.run' (← read) state.metaState
protected def GoalState.withContext { m } [MonadControlT MetaM m] [Monad m] (state: GoalState) (mvarId: MVarId) : m α → m α :=
Meta.mapMetaM <| state.withContext' mvarId
/-- Uses context of the first parent -/
protected def GoalState.withParentContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
Meta.mapMetaM <| state.withContext' state.parentMVar?.get!
Meta.mapMetaM <| state.withContext' state.parentMVars[0]!
protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
Meta.mapMetaM <| state.withContext' state.root
private def GoalState.mvars (state: GoalState): SSet MVarId :=
state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
-- Restore the name generator and macro scopes of the core state
protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit := do
let savedCore := state.coreState
private def restoreCoreMExtra (state : Core.SavedState) : CoreM Unit :=
modifyGetThe Core.State (fun st => ((),
{ st with nextMacroScope := savedCore.nextMacroScope, ngen := savedCore.ngen }))
{ st with nextMacroScope := state.nextMacroScope, ngen := state.ngen }))
-- Restore the name generator and macro scopes of the core state
protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit :=
restoreCoreMExtra state.coreState
protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit := do
state.restoreCoreMExtra
state.savedState.term.meta.restore
@ -94,40 +151,13 @@ private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tac
state.restoreElabM
Elab.Tactic.setGoals [goal]
@[export pantograph_goal_state_focus]
protected def GoalState.focus (state : GoalState) (goal : MVarId): Option GoalState := do
return {
state with
savedState := {
state.savedState with
tactic := { goals := [goal] },
},
}
/-- Immediately bring all parent goals back into scope. Used in automatic mode -/
@[export pantograph_goal_state_immediate_resume]
protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): GoalState :=
-- Prune parents solved goals
let mctx := state.mctx
let parentGoals := parent.goals.filter λ goal =>
let isDuplicate := state.goals.contains goal
let isSolved := mctx.eAssignment.contains goal || mctx.dAssignment.contains goal
(¬ isDuplicate) && (¬ isSolved)
{
state with
savedState := {
state.savedState with
tactic := { goals := state.goals ++ parentGoals },
},
}
/--
Brings into scope a list of goals. User must ensure `goals` are distinct.
-/
@[export pantograph_goal_state_resume]
protected def GoalState.resume (state : GoalState) (goals : List MVarId) : Except String GoalState := do
if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString)
if ¬ (goals.all (state.mctx.decls.contains ·)) then
let invalid_goals := goals.filter (λ goal => ¬ state.mctx.decls.contains goal) |>.map (·.name.toString)
.error s!"Goals {invalid_goals} are not in scope"
-- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
let unassigned := goals.filter λ goal =>
@ -165,17 +195,21 @@ protected def GoalState.isSolved (goalState : GoalState) : Bool :=
| .some e => ¬ e.hasExprMVar
| .none => true
goalState.goals.isEmpty && solvedRoot
@[export pantograph_goal_state_parent_expr]
protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
let parent ← goalState.parentMVar?
let expr := goalState.mctx.eAssignment.find! parent
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
return expr
@[export pantograph_goal_state_get_mvar_e_assignment]
protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarId): Option Expr := do
let expr ← goalState.mctx.eAssignment.find? mvarId
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
return expr
@[export pantograph_goal_state_parent_exprs]
protected def GoalState.parentExprs (state : GoalState) : List Expr :=
state.parentMVars.map λ goal => state.getMVarEAssignment goal |>.get!
@[always_inline]
protected def GoalState.hasUniqueParent (state : GoalState) : Bool :=
state.parentMVars.length == 1
@[always_inline]
protected def GoalState.parentExpr! (state : GoalState) : Expr :=
assert! state.parentMVars.length == 1
(state.getMVarEAssignment state.parentMVars[0]!).get!
deriving instance BEq for DelayedMetavarAssignment
@ -187,7 +221,8 @@ if conflicting assignments exist. We also assume the monotonicity property: In a
chain of descending goal states, a mvar cannot be unassigned, and once assigned
its assignment cannot change. -/
@[export pantograph_goal_state_replay_m]
protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM GoalState := do
protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM GoalState :=
withTraceNode `Pantograph.GoalState.replay (fun _ => return m!"replay") do
let srcNGen := src.coreState.ngen
let srcNGen' := src'.coreState.ngen
let dstNGen := dst.coreState.ngen
@ -211,6 +246,8 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM
else
id
| id => id
let mapMVar : MVarId → MVarId
| { name } => ⟨mapId name⟩
let rec mapLevel : Level → Level
| .succ x => .succ (mapLevel x)
| .max l1 l2 => .max (mapLevel l1) (mapLevel l2)
@ -224,7 +261,7 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM
let mapDelayedAssignment (d : DelayedMetavarAssignment) : CoreM DelayedMetavarAssignment := do
let { mvarIdPending, fvars } := d
return {
mvarIdPending := ⟨mapId mvarIdPending.name⟩,
mvarIdPending := mapMVar mvarIdPending,
fvars := ← fvars.mapM mapExpr,
}
let mapLocalDecl (ldecl : LocalDecl) : CoreM LocalDecl := do
@ -305,6 +342,7 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM
}
}
let m : MetaM Meta.SavedState := Meta.withMCtx mctx do
restoreCoreMExtra savedMeta.core
savedMeta.restore
for (lmvarId, l') in src'.mctx.lAssignment do
@ -336,7 +374,7 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM
throwError "Conflicting assignment of expr metavariable (d != d) {mvarId.name}"
Meta.saveState
let goals :=dst.savedState.tactic.goals ++
let goals := dst.savedState.tactic.goals ++
src'.savedState.tactic.goals.map (⟨mapId ·.name⟩)
let fragments ← src'.fragments.foldM (init := dst.fragments) λ acc mvarId' fragment' => do
let mvarId := ⟨mapId mvarId'.name⟩
@ -355,18 +393,21 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM
meta := ← m.run',
},
},
parentMVars := dst.parentMVars ++ src.parentMVars.map mapMVar,
fragments,
}
--- Tactic execution functions ---
-- Mimics `Elab.Term.logUnassignedUsingErrorInfos`
/--
These descendants serve as "seed" mvars. If a MVarError's mvar is related to one
of these seed mvars, it means an error has occurred when a tactic was executing
on `src`. `evalTactic`, will not capture these mvars, so we need to manually
find them and save them into the goal list. See the rationales document for the
inspiration of this function.
-/
private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) := do
-- These descendants serve as "seed" mvars. If a MVarError's mvar is related
-- to one of these seed mvars, it means an error has occurred when a tactic
-- was executing on `src`. `evalTactic`, will not capture these mvars, so we
-- need to manually find them and save them into the goal list.
-- Mimics `Elab.Term.logUnassignedUsingErrorInfos`
let descendants ← Meta.getMVars (.mvar src)
--let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants
let mut alreadyVisited : MVarIdSet := {}
@ -381,6 +422,7 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId)
result := mvarDeps.foldl (·.insert ·) result
return result.toList
/-- Merger of two unique lists -/
private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId :=
let li2' := li2.filter (¬ li1.contains ·)
li1 ++ li2'
@ -390,28 +432,29 @@ Set `guardMVarErrors` to true to capture mvar errors. Lean will not
automatically collect mvars from text tactics (vide
`test_tactic_failure_synthesize_placeholder`)
-/
protected def GoalState.step' { α } (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM α) (guardMVarErrors : Bool := false)
protected def GoalState.step' { α } (state : GoalState) (site : Site) (tacticM : Elab.Tactic.TacticM α) (guardMVarErrors : Bool := false)
: Elab.TermElabM (α × GoalState) := do
unless (← getMCtx).decls.contains goal do
throwError s!"Goal is not in context: {goal.name}"
goal.checkNotAssigned `GoalState.step
let (a, { goals }) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
let ((a, parentMVars), { goals }) ← site.runTacticM tacticM
|>.run { elaborator := .anonymous }
|>.run state.savedState.tactic
let nextElabState ← MonadBacktrack.saveState
--Elab.Term.synthesizeSyntheticMVarsNoPostponing
let goals ← if guardMVarErrors then
pure $ mergeMVarLists goals (← collectAllErroredMVars goal)
parentMVars.foldlM (init := goals) λ goals parent => do
let errors ← collectAllErroredMVars parent
return mergeMVarLists goals errors
else
pure goals
let state' := {
state with
savedState := { term := nextElabState, tactic := { goals }, },
parentMVar? := .some goal,
parentMVars,
}
return (a, state')
protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false)
protected def GoalState.step (state : GoalState) (site : Site) (tacticM : Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false)
: Elab.TermElabM GoalState :=
Prod.snd <$> GoalState.step' state goal tacticM guardMVarErrors
Prod.snd <$> GoalState.step' state site tacticM guardMVarErrors
/-- Response for executing a tactic -/
inductive TacticResult where
@ -424,21 +467,21 @@ inductive TacticResult where
-- The given action cannot be executed in the state
| invalidAction (message : String)
private def dumpMessageLog (prevMessageLength : Nat) : CoreM (Bool × Array String) := do
private def dumpMessageLog (prevMessageLength : Nat := 0) : CoreM (Bool × Array String) := do
let newMessages := (← Core.getMessageLog).toList.drop prevMessageLength
let hasErrors := newMessages.any (·.severity == .error)
let newMessages ← newMessages.mapM λ m => m.toString
Core.resetMessageLog
return (hasErrors, newMessages.toArray)
/-- Execute a `TermElabM` producing a goal state, capturing the error and turn it into a `TacticResult` -/
def withCapturingError (elabM : Elab.Term.TermElabM GoalState) : Elab.TermElabM TacticResult := do
-- FIXME: Maybe message log should be empty
let prevMessageLength := (← Core.getMessageLog).toList.length
assert! (← Core.getMessageLog).toList.isEmpty
try
let state ← elabM
-- Check if error messages have been generated in the core.
let (hasError, newMessages) ← dumpMessageLog prevMessageLength
let (hasError, newMessages) ← dumpMessageLog
if hasError then
return .failure newMessages
else
@ -446,62 +489,58 @@ def withCapturingError (elabM : Elab.Term.TermElabM GoalState) : Elab.TermElabM
catch exception =>
match exception with
| .internal _ =>
let (_, messages) ← dumpMessageLog prevMessageLength
let (_, messages) ← dumpMessageLog
return .failure messages
| _ => return .failure #[← exception.toMessageData.toString]
/-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
protected def GoalState.tryTacticM
(state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
(state: GoalState) (site : Site)
(tacticM: Elab.Tactic.TacticM Unit)
(guardMVarErrors : Bool := false)
: Elab.TermElabM TacticResult := do
: Elab.TermElabM TacticResult :=
withCapturingError do
state.step goal tacticM guardMVarErrors
state.step site tacticM guardMVarErrors
/-- Execute a string tactic on given state. Restores TermElabM -/
@[export pantograph_goal_state_try_tactic_m]
protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: String):
protected def GoalState.tryTactic (state: GoalState) (site : Site) (tactic: String):
Elab.TermElabM TacticResult := do
state.restoreElabM
/-
let .some goal := state.actingGoal? site | throwNoGoals
if let .some fragment := state.fragments[goal]? then
return ← withCapturingError do
let (moreFragments, state') ← state.step' goal (fragment.step goal tactic)
let fragments := moreFragments.fold (init := state.fragments.erase goal) λ acc mvarId f =>
acc.insert mvarId f
return { state' with fragments } -/
let catName := match isLHSGoal? (← goal.getType) with
| .some _ => `conv
| .none => `tactic
let (fragments, state') ← state.step' site do
fragment.step goal tactic $ state.fragments.erase goal
return { state' with fragments }
-- Normal tactic without fragment
let tactic ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := catName)
(env := ← getEnv)
(catName := `tactic)
(input := tactic)
(fileName := ← getFileName) with
| .ok stx => pure $ stx
| .error error => return .parseError error
let tacticM := Elab.Tactic.evalTactic tactic
withCapturingError do
state.step goal tacticM (guardMVarErrors := true)
state.step site tacticM (guardMVarErrors := true)
-- Specialized Tactics
protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String):
Elab.TermElabM TacticResult := do
protected def GoalState.tryAssign (state : GoalState) (site : Site) (expr : String)
: Elab.TermElabM TacticResult := do
state.restoreElabM
let expr ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(env := ← getEnv)
(catName := `term)
(input := expr)
(fileName := ← getFileName) with
| .ok syn => pure syn
| .error error => return .parseError error
state.tryTacticM goal $ Tactic.evalAssign expr
state.tryTacticM site $ Tactic.evalAssign expr
protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String):
Elab.TermElabM TacticResult := do
protected def GoalState.tryLet (state : GoalState) (site : Site) (binderName : String) (type : String)
: Elab.TermElabM TacticResult := do
state.restoreElabM
let type ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
@ -510,28 +549,30 @@ protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: St
(fileName := ← getFileName) with
| .ok syn => pure syn
| .error error => return .parseError error
state.tryTacticM goal $ Tactic.evalLet binderName.toName type
state.tryTacticM site $ Tactic.evalLet binderName.toName type
/-- Enter conv tactic mode -/
@[export pantograph_goal_state_conv_enter_m]
protected def GoalState.conv (state : GoalState) (goal : MVarId) :
protected def GoalState.convEnter (state : GoalState) (site : Site) :
Elab.TermElabM TacticResult := do
let .some goal := state.actingGoal? site | throwNoGoals
if let .some (.conv ..) := state.fragments[goal]? then
return .invalidAction "Already in conv state"
goal.checkNotAssigned `GoalState.conv
withCapturingError do
let (fragment, state') ← state.step' goal Fragment.enterConv
let (fragments, state') ← state.step' site Fragment.enterConv
return {
state' with
fragments := state'.fragments.insert goal fragment
fragments := fragments.fold (init := state'.fragments) λ acc goal fragment =>
acc.insert goal fragment
}
/-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/
@[export pantograph_goal_state_conv_exit_m]
protected def GoalState.convExit (state : GoalState) (goal : MVarId):
/-- Exit from a tactic fragment. -/
@[export pantograph_goal_state_fragment_exit_m]
protected def GoalState.fragmentExit (state : GoalState) (site : Site):
Elab.TermElabM TacticResult := do
let .some fragment@(.conv ..) := state.fragments[goal]? |
return .invalidAction "Not in conv state"
let .some goal := state.actingGoal? site | throwNoGoals
let .some fragment := state.fragments[goal]? |
return .invalidAction "Goal does not have a fragment"
withCapturingError do
let (fragments, state') ← state.step' goal (fragment.exit goal state.fragments)
return {
@ -543,18 +584,17 @@ protected def GoalState.calcPrevRhsOf? (state : GoalState) (goal : MVarId) : Opt
let .some (.calc prevRhs?) := state.fragments[goal]? | .none
prevRhs?
@[export pantograph_goal_state_try_calc_m]
protected def GoalState.tryCalc (state : GoalState) (goal : MVarId) (pred : String)
@[export pantograph_goal_state_calc_enter_m]
protected def GoalState.calcEnter (state : GoalState) (site : Site)
: Elab.TermElabM TacticResult := do
let prevRhs? := state.calcPrevRhsOf? goal
let .some goal := state.actingGoal? site | throwNoGoals
if let .some _ := state.fragments[goal]? then
return .invalidAction "Goal already has a fragment"
withCapturingError do
let (moreFragments, state') ← state.step' goal do
let fragment := Fragment.calc prevRhs?
fragment.step goal pred
let fragments := moreFragments.fold (init := state.fragments.erase goal) λ acc mvarId f =>
acc.insert mvarId f
let fragment := Fragment.enterCalc
let fragments := state.fragments.insert goal fragment
return {
state' with
state with
fragments,
}

25
Pantograph/Library.lean
View File

@ -117,10 +117,10 @@ def goalStartExpr (expr: String) : Protocol.FallibleT Elab.TermElabM GoalState :
@[export pantograph_goal_serialize_m]
def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) :=
runMetaM <| state.serializeGoals (parent := .none) options
runMetaM <| state.serializeGoals options
@[export pantograph_goal_print_m]
def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Bool) (extraMVars : Array String) (options: @&Protocol.Options)
def goalPrint (state: GoalState) (rootExpr: Bool) (parentExprs: Bool) (goals: Bool) (extraMVars : Array String) (options: @&Protocol.Options)
: CoreM Protocol.GoalPrintResult := runMetaM do
state.restoreMetaM
@ -130,9 +130,10 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
serializeExpression options (← instantiateAll expr)
else
pure .none
let parent? ← if parentExpr then
state.parentExpr?.mapM λ expr => state.withParentContext do
serializeExpression options (← instantiateAll expr)
let parentExprs? ← if parentExprs then
.some <$> state.parentMVars.mapM λ parent => parent.withContext do
let val := state.getMVarEAssignment parent |>.get!
serializeExpression options (← instantiateAll val)
else
pure .none
let goals ← if goals then
@ -148,7 +149,7 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
let env ← getEnv
return {
root?,
parent?,
parentExprs?,
goals,
extraMVars,
rootHasSorry := rootExpr?.map (·.hasSorry) |>.getD false,
@ -157,26 +158,26 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
}
@[export pantograph_goal_have_m]
protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): Elab.TermElabM TacticResult := do
protected def GoalState.tryHave (state: GoalState) (site : Site) (binderName: String) (type: String): Elab.TermElabM TacticResult := do
let type ← match (← parseTermM type) with
| .ok syn => pure syn
| .error error => return .parseError error
state.restoreElabM
state.tryTacticM goal $ Tactic.evalHave binderName.toName type
state.tryTacticM site $ Tactic.evalHave binderName.toName type
@[export pantograph_goal_try_define_m]
protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): Elab.TermElabM TacticResult := do
protected def GoalState.tryDefine (state: GoalState) (site : Site) (binderName: String) (expr: String): Elab.TermElabM TacticResult := do
let expr ← match (← parseTermM expr) with
| .ok syn => pure syn
| .error error => return .parseError error
state.restoreElabM
state.tryTacticM goal (Tactic.evalDefine binderName.toName expr)
state.tryTacticM site $ Tactic.evalDefine binderName.toName expr
@[export pantograph_goal_try_draft_m]
protected def GoalState.tryDraft (state: GoalState) (goal: MVarId) (expr: String): Elab.TermElabM TacticResult := do
protected def GoalState.tryDraft (state: GoalState) (site : Site) (expr: String): Elab.TermElabM TacticResult := do
let expr ← match (← parseTermM expr) with
| .ok syn => pure syn
| .error error => return .parseError error
state.restoreElabM
state.tryTacticM goal (Tactic.evalDraft expr)
state.tryTacticM site $ Tactic.evalDraft expr
-- Cancel the token after a timeout.
@[export pantograph_run_cancel_token_with_timeout_m]

34
Pantograph/Protocol.lean
View File

@ -60,16 +60,21 @@ structure Variable where
type?: Option Expression := .none
value?: Option Expression := .none
deriving Lean.ToJson
inductive Fragment where
| tactic
| conv
| calc
deriving BEq, DecidableEq, Repr, Lean.ToJson
structure Goal where
name: String := ""
/-- Name of the metavariable -/
userName?: Option String := .none
/-- Is the goal in conversion mode -/
isConversion: Bool := false
name : String := ""
/-- User-facing name -/
userName? : Option String := .none
fragment : Fragment := .tactic
/-- target expression type -/
target: Expression
target : Expression
/-- Variables -/
vars: Array Variable := #[]
vars : Array Variable := #[]
deriving Lean.ToJson
@ -87,6 +92,7 @@ structure InteractionError where
deriving Lean.ToJson
def errorIndex (desc: String): InteractionError := { error := "index", desc }
def errorOperation (desc: String): InteractionError := { error := "operation", desc }
def errorExpr (desc: String): InteractionError := { error := "expr", desc }
@ -248,17 +254,17 @@ structure GoalStartResult where
root: String
deriving Lean.ToJson
structure GoalTactic where
-- Identifiers for tree, state, and goal
stateId: Nat
goalId: Nat := 0
-- If omitted, act on the first goal
goalId?: Option Nat := .none
-- If set to true, goal will not go dormant. Defaults to `automaticMode`
autoResume?: Option Bool := .none
-- One of the fields here must be filled
tactic?: Option String := .none
mode?: Option String := .none -- Changes the current category to {"tactic", "calc", "conv"}
expr?: Option String := .none
have?: Option String := .none
let?: 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
draft?: Option String := .none
-- In case of the `have` tactic, the new free variable name is provided here
@ -308,8 +314,8 @@ structure GoalPrint where
-- Print root?
rootExpr?: Option Bool := .some False
-- Print the parent expr?
parentExpr?: Option Bool := .some False
-- Print the parent expressions
parentExprs?: Option Bool := .some False
-- Print goals?
goals?: Option Bool := .some False
-- Print values of extra mvars?
@ -319,7 +325,7 @@ structure GoalPrintResult where
-- The root expression
root?: Option Expression := .none
-- The filling expression of the parent goal
parent?: Option Expression := .none
parentExprs?: Option (List Expression) := .none
goals: Array Goal := #[]
extraMVars: Array Expression := #[]

10
Pantograph/Serial.lean
View File

@ -103,7 +103,7 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :
tactic
}
root,
parentMVar?,
parentMVars,
fragments,
} := goalState
Pantograph.pickle path (
@ -115,7 +115,7 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :
tactic,
root,
parentMVar?,
parentMVars,
fragments,
)
@ -131,7 +131,7 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
tactic,
root,
parentMVar?,
parentMVars,
fragments,
), region) ← Pantograph.unpickle (
PHashMap Name ConstantInfo ×
@ -142,7 +142,7 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
Elab.Tactic.State ×
MVarId ×
Option MVarId ×
List MVarId ×
FragmentMap
) path
let env ← env.replay (Std.HashMap.ofList map₂.toList)
@ -162,7 +162,7 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
tactic,
},
root,
parentMVar?,
parentMVars,
fragments,
}
return (goalState, region)

117
Pantograph/Tactic/Fragment.lean
View File

@ -4,6 +4,13 @@ Here, a unified system handles all fragments.
Inside a tactic fragment, the parser category may be different. An incomplete
fragmented tactic may not be elaboratable..
In line with continuation/resumption paradigms, the exit function of a fragment
tactic is responsible for resuming incomplete goals with fragments. For example,
when a conversion tactic finishes, the sentinels should resume the root of the
conversion tactic goal. The user cannot be expected to execute this resumption,
since the root is automatically dormanted at the entry of the conversion tactic
mode.
-/
import Lean.Meta
import Lean.Elab
@ -14,59 +21,79 @@ namespace Pantograph
inductive Fragment where
| calc (prevRhs? : Option Expr)
| conv (rhs : MVarId) (dormant : List MVarId)
deriving BEq
| conv (rhs : MVarId)
-- This goal is spawned from a `conv`
| convSentinel (parent : MVarId)
deriving BEq, Inhabited
abbrev FragmentMap := Std.HashMap MVarId Fragment
def FragmentMap.empty : FragmentMap := Std.HashMap.emptyWithCapacity 2
protected def FragmentMap.filter (map : FragmentMap) (pred : MVarId → Fragment → Bool) : FragmentMap :=
map.fold (init := FragmentMap.empty) λ acc mvarId fragment =>
if pred mvarId fragment then
acc.insert mvarId fragment
else
acc
protected def Fragment.map (fragment : Fragment) (mapExpr : Expr → CoreM Expr) : CoreM Fragment :=
let mapMVarId (mvarId : MVarId) : CoreM MVarId :=
let mapMVar (mvarId : MVarId) : CoreM MVarId :=
return (← mapExpr (.mvar mvarId)) |>.mvarId!
match fragment with
| .calc prevRhs? => return .calc (← prevRhs?.mapM mapExpr)
| .conv rhs dormant => do
let rhs' ← mapMVarId rhs
let dormant' ← dormant.mapM mapMVarId
return .conv rhs' dormant'
| .conv rhs => do
let rhs' ← mapMVar rhs
return .conv rhs'
| .convSentinel parent => do
return .convSentinel (← mapMVar parent)
protected def Fragment.enterCalc : Elab.Tactic.TacticM Fragment := do
return .calc .none
protected def Fragment.enterConv : Elab.Tactic.TacticM Fragment := do
protected def Fragment.enterCalc : Fragment := .calc .none
protected def Fragment.enterConv : Elab.Tactic.TacticM FragmentMap := do
let goal ← Elab.Tactic.getMainGoal
let rhs ← goal.withContext do
let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
Elab.Tactic.replaceMainGoal [newGoal.mvarId!]
pure rhs.mvarId!
let otherGoals := (← Elab.Tactic.getGoals).filter (· != goal)
return conv rhs otherGoals
goal.checkNotAssigned `GoalState.conv
let (rhs, newGoal) ← goal.withContext do
let target ← instantiateMVars (← goal.getType)
let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor target
pure (rhs.mvarId!, newGoal.mvarId!)
Elab.Tactic.replaceMainGoal [newGoal]
return FragmentMap.empty
|>.insert goal (.conv rhs)
|>.insert newGoal (.convSentinel goal)
protected def Fragment.exit (fragment : Fragment) (goal : MVarId) (fragments : FragmentMap)
protected partial def Fragment.exit (fragment : Fragment) (goal : MVarId) (fragments : FragmentMap)
: Elab.Tactic.TacticM FragmentMap :=
match fragment with
| .calc .. => do
Elab.Tactic.setGoals [goal]
return fragments.erase goal
| .conv rhs otherGoals => do
-- FIXME: Only process the goals that are descendants of `goal`
let goals := (← Elab.Tactic.getGoals).filter λ goal => true
--match fragments[goal]? with
--| .some f => fragment == f
--| .none => false -- Not a conv goal from this
| .conv rhs => do
let goals := (← Elab.Tactic.getGoals).filter λ descendant =>
match fragments[descendant]? with
| .some s => (.convSentinel goal) == s
| _ => false -- Not a conv goal from this
-- Close all existing goals with `refl`
for mvarId in goals do
liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
Elab.Tactic.pruneSolvedGoals
unless (← goals.filterM (·.isAssignedOrDelayedAssigned)).isEmpty do
throwError "convert tactic failed, there are unsolved goals\n{Elab.goalsToMessageData (goals)}"
Elab.Tactic.setGoals $ [goal] ++ otherGoals
-- Ensure the meta tactic runs on `goal` even if its dormant by forcing resumption
Elab.Tactic.setGoals $ goal :: (← Elab.Tactic.getGoals)
let targetNew ← instantiateMVars (.mvar rhs)
let proof ← instantiateMVars (.mvar goal)
Elab.Tactic.liftMetaTactic1 (·.replaceTargetEq targetNew proof)
return fragments.erase goal
protected def Fragment.step (fragment : Fragment) (goal : MVarId) (s : String)
-- Try to solve maiinline by rfl
let mvarId ← Elab.Tactic.getMainGoal
liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
Elab.Tactic.pruneSolvedGoals
return fragments.filter λ mvarId fragment =>
!(mvarId == goal || fragment == .convSentinel goal)
| .convSentinel parent =>
let parentFragment := fragments[parent]!
parentFragment.exit parent (fragments.erase goal)
protected def Fragment.step (fragment : Fragment) (goal : MVarId) (s : String) (map : FragmentMap)
: Elab.Tactic.TacticM FragmentMap := goal.withContext do
assert! ¬ (← goal.isAssigned)
match fragment with
@ -121,9 +148,41 @@ protected def Fragment.step (fragment : Fragment) (goal : MVarId) (s : String)
let goals := [ mvarBranch ] ++ remainder?.toList
Elab.Tactic.setGoals goals
match remainder? with
| .some goal => return FragmentMap.empty.insert goal $ .calc (.some rhs)
| .none => return .empty
| .some goal => return map.erase goal |>.insert goal $ .calc (.some rhs)
| .none => return map
| .conv .. => do
throwError "Direct operation on conversion tactic parent goal is not allowed"
| fragment@(.convSentinel parent) => do
assert! isLHSGoal? (← goal.getType) |>.isSome
let tactic ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `conv)
(input := s)
(fileName := ← getFileName) with
| .ok stx => pure $ stx
| .error error => throwError error
let oldGoals ← Elab.Tactic.getGoals
-- Label newly generated goals as conv sentinels
Elab.Tactic.evalTactic tactic
let newConvGoals ← (← Elab.Tactic.getUnsolvedGoals).filterM λ g => do
-- conv tactic might generate non-conv goals
if oldGoals.contains g then
return false
return isLHSGoal? (← g.getType) |>.isSome
-- Conclude the conv by exiting the parent fragment if new goals is empty
if newConvGoals.isEmpty then
let hasSiblingFragment := map.fold (init := false) λ flag _ fragment =>
if flag then
true
else match fragment with
| .convSentinel parent' => parent == parent'
| _ => false
if ¬ hasSiblingFragment then
-- This fragment must exist since we have conv goals
let parentFragment := map[parent]!
-- All descendants exhausted. Exit from the parent conv.
return ← parentFragment.exit parent map
return newConvGoals.foldl (init := map) λ acc g =>
acc.insert g fragment
end Pantograph

140
Repl.lean
View File

@ -97,6 +97,77 @@ def liftTermElabM { α } (termElabM : Elab.TermElabM α) (levelNames : List Name
}
runCoreM $ termElabM.run' context state |>.run'
section Goal
def goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult := do
let state ← getMainState
let .some goalState := state.goalStates[args.stateId]? |
Protocol.throw $ Protocol.errorIndex s!"Invalid state index {args.stateId}"
let unshielded := args.autoResume?.getD state.options.automaticMode
let site ← match args.goalId?, unshielded with
| .some goalId, true => do
let .some goal := goalState.goals[goalId]? |
Protocol.throw $ Protocol.errorIndex s!"Invalid goal index {goalId}"
pure (.prefer goal)
| .some goalId, false => do
let .some goal := goalState.goals[goalId]? |
Protocol.throw $ Protocol.errorIndex s!"Invalid goal index {goalId}"
pure (.focus goal)
| .none, true => pure .unfocus
| .none, false => do
let .some goal := goalState.mainGoal? |
Protocol.throw $ Protocol.errorIndex s!"No goals to be solved"
pure (.focus goal)
let nextGoalState?: Except _ TacticResult ← liftTermElabM do
-- NOTE: Should probably use a macro to handle this...
match args.tactic?, args.mode?, args.expr?, args.have?, args.let?, args.draft? with
| .some tactic, .none, .none, .none, .none, .none => do
pure $ Except.ok $ ← goalState.tryTactic site tactic
| .none, .some mode, .none, .none, .none, .none => match mode with
| "tactic" => do -- Exit from the current fragment
pure $ Except.ok $ ← goalState.fragmentExit site
| "conv" => do
pure $ Except.ok $ ← goalState.convEnter site
| "calc" => do
pure $ Except.ok $ ← goalState.calcEnter site
| _ => pure $ .error $ Protocol.errorOperation s!"Invalid mode {mode}"
| .none, .none, .some expr, .none, .none, .none => do
pure $ Except.ok $ ← goalState.tryAssign site expr
| .none, .none, .none, .some type, .none, .none => do
let binderName := args.binderName?.getD ""
pure $ Except.ok $ ← goalState.tryHave site binderName type
| .none, .none, .none, .none, .some type, .none => do
let binderName := args.binderName?.getD ""
pure $ Except.ok $ ← goalState.tryLet site binderName type
| .none, .none, .none, .none, .none, .some draft => do
pure $ Except.ok $ ← goalState.tryDraft site draft
| _, _, _, _, _, _ =>
pure $ .error $ Protocol.errorOperation
"Exactly one of {tactic, mode, expr, have, let, draft} must be supplied"
match nextGoalState? with
| .error error => Protocol.throw error
| .ok (.success nextGoalState messages) => do
let nextStateId ← newGoalState nextGoalState
let parentExprs := nextGoalState.parentExprs
let hasSorry := parentExprs.any (·.hasSorry)
let hasUnsafe := parentExprs.any ((← getEnv).hasUnsafe ·)
let goals ← runCoreM $ nextGoalState.serializeGoals (options := state.options) |>.run'
return {
nextStateId? := .some nextStateId,
goals? := .some goals,
messages? := .some messages,
hasSorry,
hasUnsafe,
}
| .ok (.parseError message) =>
return { messages? := .none, parseError? := .some message }
| .ok (.invalidAction message) =>
Protocol.throw $ errorI "invalid" message
| .ok (.failure messages) =>
return { messages? := .some messages }
end Goal
section Frontend
structure CompilationUnit where
@ -225,7 +296,6 @@ def execute (command: Protocol.Command): MainM Json := do
return toJson error
where
errorCommand := errorI "command"
errorIndex := errorI "index"
errorIO := errorI "io"
-- Command Functions
reset (_: Protocol.Reset): EMainM Protocol.StatResult := do
@ -290,7 +360,7 @@ def execute (command: Protocol.Command): MainM Json := do
| .some expr, .none => goalStartExpr expr |>.run
| .none, .some copyFrom => do
(match (← getEnv).find? <| copyFrom.toName with
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
| .none => return .error <| Protocol.errorIndex s!"Symbol not found: {copyFrom}"
| .some cInfo => return .ok (← GoalState.create cInfo.type))
| _, _ =>
return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied"
@ -299,70 +369,14 @@ def execute (command: Protocol.Command): MainM Json := do
| .ok goalState =>
let stateId ← newGoalState goalState
return { stateId, root := goalState.root.name.toString }
goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult := do
let state ← getMainState
let .some goalState := state.goalStates[args.stateId]? |
Protocol.throw $ errorIndex s!"Invalid state index {args.stateId}"
-- FIXME: Allow proper conversion tactic exit even in automatic mode
let .some goal := goalState.goals[args.goalId]? |
Protocol.throw $ errorIndex s!"Invalid goal index {args.goalId}"
let nextGoalState?: Except _ TacticResult ← liftTermElabM do
-- NOTE: Should probably use a macro to handle this...
match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv?, args.draft? with
| .some tactic, .none, .none, .none, .none, .none, .none => do
pure <| Except.ok <| ← goalState.tryTactic goal tactic
| .none, .some expr, .none, .none, .none, .none, .none => do
pure <| Except.ok <| ← goalState.tryAssign goal expr
| .none, .none, .some type, .none, .none, .none, .none => do
let binderName := args.binderName?.getD ""
pure <| Except.ok <| ← goalState.tryHave goal binderName type
| .none, .none, .none, .some type, .none, .none, .none => do
let binderName := args.binderName?.getD ""
pure <| Except.ok <| ← goalState.tryLet goal binderName type
| .none, .none, .none, .none, .some pred, .none, .none => do
pure <| Except.ok <| ← goalState.tryCalc goal pred
| .none, .none, .none, .none, .none, .some true, .none => do
pure <| Except.ok <| ← goalState.conv goal
| .none, .none, .none, .none, .none, .some false, .none => do
pure <| Except.ok <| ← goalState.convExit goal
| .none, .none, .none, .none, .none, .none, .some draft => do
pure <| Except.ok <| ← goalState.tryDraft goal draft
| _, _, _, _, _, _, _ =>
let error := errorI "arguments" "Exactly one of {tactic, expr, have, let, calc, conv, draft} must be supplied"
pure $ .error error
match nextGoalState? with
| .error error => Protocol.throw error
| .ok (.success nextGoalState messages) => do
let nextGoalState ← match state.options.automaticMode, args.conv? with
| true, .none => do
pure $ nextGoalState.immediateResume goalState
| true, .some true => pure nextGoalState
| true, .some false => pure nextGoalState
| false, _ => pure nextGoalState
let nextStateId ← newGoalState nextGoalState
let parentExpr := nextGoalState.parentExpr?.get!
let goals ← runCoreM $ nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
return {
nextStateId? := .some nextStateId,
goals? := .some goals,
messages? := .some messages,
hasSorry := parentExpr.hasSorry,
hasUnsafe := (← getEnv).hasUnsafe parentExpr,
}
| .ok (.parseError message) =>
return { messages? := .none, parseError? := .some message }
| .ok (.invalidAction message) =>
Protocol.throw $ errorI "invalid" message
| .ok (.failure messages) =>
return { messages? := .some messages }
goal_continue (args: Protocol.GoalContinue): EMainM Protocol.GoalContinueResult := do
let state ← getMainState
let .some target := state.goalStates[args.target]? |
Protocol.throw $ errorIndex s!"Invalid state index {args.target}"
Protocol.throw $ Protocol.errorIndex s!"Invalid state index {args.target}"
let nextGoalState? : GoalState ← match args.branch?, args.goals? with
| .some branchId, .none => do
match state.goalStates[branchId]? with
| .none => Protocol.throw $ errorIndex s!"Invalid state index {branchId}"
| .none => Protocol.throw $ Protocol.errorIndex s!"Invalid state index {branchId}"
| .some branch => pure $ target.continue branch
| .none, .some goals =>
let goals := goals.toList.map (λ n => { name := n.toName })
@ -385,11 +399,11 @@ def execute (command: Protocol.Command): MainM Json := do
goal_print (args: Protocol.GoalPrint): EMainM Protocol.GoalPrintResult := do
let state ← getMainState
let .some goalState := state.goalStates[args.stateId]? |
Protocol.throw $ errorIndex s!"Invalid state index {args.stateId}"
Protocol.throw $ Protocol.errorIndex s!"Invalid state index {args.stateId}"
let result ← liftMetaM <| goalPrint
goalState
(rootExpr := args.rootExpr?.getD False)
(parentExpr := args.parentExpr?.getD False)
(parentExprs := args.parentExprs?.getD False)
(goals := args.goals?.getD False)
(extraMVars := args.extraMVars?.getD #[])
(options := state.options)
@ -397,7 +411,7 @@ def execute (command: Protocol.Command): MainM Json := do
goal_save (args: Protocol.GoalSave): EMainM Protocol.GoalSaveResult := do
let state ← getMainState
let .some goalState := state.goalStates[args.id]? |
Protocol.throw $ errorIndex s!"Invalid state index {args.id}"
Protocol.throw $ Protocol.errorIndex s!"Invalid state index {args.id}"
goalStatePickle goalState args.path
return {}
goal_load (args: Protocol.GoalLoad): EMainM Protocol.GoalLoadResult := do

4
Test/Integration.lean
View File

@ -88,10 +88,10 @@ def test_tactic : Test := do
({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult)
step "goal.tactic" ({ stateId := 0, tactic? := .some "intro x" }: Protocol.GoalTactic)
({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult)
step "goal.print" ({ stateId := 1, parentExpr? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
step "goal.print" ({ stateId := 1, parentExprs? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
({
root? := .some { pp? := "fun x => ?m.11"},
parent? := .some { pp? := .some "fun x => ?m.11" },
parentExprs? := .some [{ pp? := .some "fun x => ?m.11" }],
}: Protocol.GoalPrintResult)
step "goal.tactic" ({ stateId := 1, tactic? := .some "intro y" }: Protocol.GoalTactic)
({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult)

1
Test/Main.lean
View File

@ -55,6 +55,7 @@ def main (args: List String) := do
("Delate", Delate.suite),
("Serial", Serial.suite),
("Tactic/Assign", Tactic.Assign.suite),
("Tactic/Fragment", Tactic.Fragment.suite),
("Tactic/Prograde", Tactic.Prograde.suite),
("Tactic/Special", Tactic.Special.suite),
]

250
Test/Proofs.lean
View File

@ -32,7 +32,7 @@ def startProof (start: Start): TestM (Option GoalState) := do
let expr ← parseSentence expr
return .some $ ← GoalState.create (expr := expr)
def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String)
private def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String)
(userName?: Option String := .none): Protocol.Goal :=
{
name,
@ -43,7 +43,7 @@ def buildNamedGoal (name: String) (nameType: List (String × String)) (target: S
type? := .some { pp? := .some x.snd },
})).toArray
}
def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
private def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
Protocol.Goal :=
{
userName?,
@ -53,7 +53,7 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O
type? := .some { pp? := .some x.snd },
})).toArray
}
def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
private 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 ← createCoreContext #[]
@ -77,7 +77,7 @@ def test_identity: TestM Unit := do
addTest $ LSpec.check "intro" ((← state1.serializeGoals (options := ← read)).map (·.name) =
#[inner])
let state1parent ← state1.withParentContext do
serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
serializeExpressionSexp (← instantiateAll state1.parentExpr!)
addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda h 0 (:subst (:mv {inner}) 1 0)))")
-- Individual test cases
@ -117,41 +117,6 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
addTest $ LSpec.test "rw [Nat.add_comm]" state2.goals.isEmpty
return ()
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
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let state1 ← match ← state0.tacticOn (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.tacticOn (goalId := 0) (tactic := "intro m") with
| .success state _ => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "intro m" ((← state2.serializeGoals (parent := state1) options).map (·.devolatilize) =
#[buildGoalSelective [("n", .none), ("m", .some "Nat")] "n + m = m + n"])
return ()
where
-- Like `buildGoal` but allow certain variables to be elided.
buildGoalSelective (nameType: List (String × Option String)) (target: String): Protocol.Goal :=
{
target := { pp? := .some target},
vars := (nameType.map fun x => ({
userName := x.fst,
type? := x.snd.map (λ type => { pp? := type }),
})).toArray
}
example (w x y z : Nat) (p : Nat → Prop)
(h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
@ -212,8 +177,8 @@ def test_or_comm: TestM Unit := do
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone
addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone
checkTrue "(0 parent)" state0.parentMVars.isEmpty
checkTrue "(0 root)" state0.rootExpr?.isNone
let tactic := "intro p q h"
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
@ -237,11 +202,11 @@ def test_or_comm: TestM Unit := do
{ name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" } }
]
}])
checkTrue "(1 parent)" state1.parentExpr?.isSome
checkTrue "(1 parent)" state1.hasUniqueParent
checkTrue "(1 root)" $ ¬ state1.isSolved
let state1parent ← state1.withParentContext do
serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
serializeExpressionSexp (← instantiateAll state1.parentExpr!)
addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) 2 1 0))))")
let tactic := "cases h"
let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := tactic) with
@ -256,11 +221,11 @@ def test_or_comm: TestM Unit := do
let (caseL, caseR) := (state2g0.name.toString, state2g1.name.toString)
addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
#[caseL, caseR])
checkTrue "(2 parent exists)" state2.parentExpr?.isSome
checkTrue "(2 parent exists)" state2.hasUniqueParent
checkTrue "(2 root)" $ ¬ state2.isSolved
let state2parent ← state2.withParentContext do
serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!)
serializeExpressionSexp (← instantiateAll state2.parentExpr!)
let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))"
let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))"
let motive := s!"(:lambda t {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))"
@ -276,7 +241,7 @@ def test_or_comm: TestM Unit := do
addTest $ assertUnreachable $ other.toString
return ()
let state3_1parent ← state3_1.withParentContext do
serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!)
serializeExpressionSexp (← instantiateAll state3_1.parentExpr!)
let [state3_1goal0] := state3_1.goals | fail "Should have 1 goal"
addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv {state3_1goal0}))")
addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
@ -286,7 +251,7 @@ def test_or_comm: TestM Unit := do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check " assumption" state4_1.goals.isEmpty
let state4_1parent ← instantiateAll state4_1.parentExpr?.get!
let state4_1parent ← instantiateAll state4_1.parentExpr!
addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
checkTrue "(4_1 root)" $ ¬ state4_1.isSolved
let state3_2 ← match ← state2.tacticOn (goalId := 1) (tactic := "apply Or.inl") with
@ -336,194 +301,6 @@ def test_or_comm: TestM Unit := do
]
}
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.tacticOn (goalId := 0) (tactic := tactic) with
| .success state _ => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[interiorGoal [] "a + b + c1 = b + a + c2"])
let goalConv := state1.goals[0]!
let state2 ← match ← state1.conv (state1.get! 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.tacticOn (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.tacticOn (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.tacticOn (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.tacticOn (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.tacticOn (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.tacticOn (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 goalConv with
| .success state _ => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let tactic := "exact h"
let stateF ← match ← state1_1.tacticOn (goalId := 0) (tactic := tactic) with
| .success state _ => pure state
| 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.tacticOn (goalId := 0) (tactic := tactic) with
| .success state _ => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[interiorGoal [] "a + b = c + d"])
let pred := "a + b = b + c"
let state2 ← match ← state1.tryCalc (state1.get! 0) (pred := pred) with
| .success state _ => pure state
| 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"
])
addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 0) |>.isNone)
addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 1) |>.isSome)
let tactic := "apply h1"
let state2m ← match ← state2.tacticOn (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 (state3.get! 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")
])
addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? (state4.get! 0) |>.isNone)
let tactic := "apply h2"
let state4m ← match ← state4.tacticOn (goalId := 0) (tactic := tactic) with
| .success state _ => pure state
| 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 test_tactic_failure_unresolved_goals : TestM Unit := do
let state? ← startProof (.expr "∀ (p : Nat → Prop), ∃ (x : Nat), p (0 + x + 0)")
let state0 ← match state? with
@ -600,11 +377,8 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
("identity", test_identity),
("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),
("conv", test_conv),
("calc", test_calc),
("tactic failure with unresolved goals", test_tactic_failure_unresolved_goals),
("tactic failure with synthesize placeholder", test_tactic_failure_synthesize_placeholder),
("deconstruct", test_deconstruct),

4
Test/Serial.lean
View File

@ -87,12 +87,12 @@ def test_pickling_env_extensions : TestM Unit := do
let .ok value ← elabTerm (← `(term|sorry)) (.some type) | unreachable!
pure (type, value)
let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type value) | unreachable!
let parentExpr := state1.parentExpr?.get!
let parentExpr := state1.parentExpr!
checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma
goalStatePickle state1 statePath
let ((), _) ← runCoreM coreDst $ transformTestT runTermElabMInCore do
let (state1, _) ← goalStateUnpickle statePath (← getEnv)
let parentExpr := state1.parentExpr?.get!
let parentExpr := state1.parentExpr!
checkTrue "dst has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma
return ()

1
Test/Tactic.lean
View File

@ -1,3 +1,4 @@
import Test.Tactic.Assign
import Test.Tactic.Fragment
import Test.Tactic.Prograde
import Test.Tactic.Special

312
Test/Tactic/Fragment.lean Normal file
View File

@ -0,0 +1,312 @@
import Pantograph.Goal
import Test.Common
open Lean
namespace Pantograph.Test.Tactic.Fragment
private def buildGoal (nameType: List (String × String)) (target: String):
Protocol.Goal :=
{
target := { pp? := .some target},
vars := (nameType.map fun x => ({
userName := x.fst,
type? := .some { pp? := .some x.snd },
})).toArray
}
abbrev TestM := TestT $ Elab.TermElabM
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_simple: TestM Unit := do
let rootTarget ← parseSentence "∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2"
let state0 ← GoalState.create rootTarget
let tactic := "intro a b c1 c2 h"
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state _ => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
#[interiorGoal [] "a + b + c1 = b + a + c2"])
let goalConv := state1.goals[0]!
let state2 ← match ← state1.convEnter (state1.get! 0) with
| .success state _ => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals).map (·.devolatilize) =
#[{ interiorGoal [] "a + b + c1 = b + a + c2" with fragment := .conv }])
let convTactic := "rhs"
let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with
| .success state _ => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!" {convTactic} (discard)" ((← state3R.serializeGoals).map (·.devolatilize) =
#[{ interiorGoal [] "b + a + c2" with fragment := .conv }])
let convTactic := "lhs"
let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with
| .success state _ => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!" {convTactic}" ((← state3L.serializeGoals).map (·.devolatilize) =
#[{ interiorGoal [] "a + b + c1" with fragment := .conv }])
let convTactic := "congr"
let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with
| .success state _ => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!" {convTactic}" ((← state4.serializeGoals).map (·.devolatilize) =
#[
{ interiorGoal [] "a + b" with fragment := .conv, userName? := .some "a" },
{ interiorGoal [] "c1" with fragment := .conv, userName? := .some "a" }
])
let convTactic := "rw [Nat.add_comm]"
let state5_1 ← match ← state4.tacticOn (goalId := 0) convTactic with
| .success state _ => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!" · {convTactic}" ((← state5_1.serializeGoals).map (·.devolatilize) =
#[{ interiorGoal [] "b + a" with fragment := .conv, userName? := .some "a" }])
let convTactic := "rfl"
let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with
| .success state _ => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!" {convTactic}" ((← state6_1.serializeGoals).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 state1_1 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
| .success state _ => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!" · {convTactic}" ((← state1_1.serializeGoals).map (·.devolatilize) =
#[interiorGoal [] "b + a + c1 = b + a + c2"])
checkEq "(fragments)" state1_1.fragments.size 0
/-
let state1_1 ← match ← state6.fragmentExit goalConv with
| .success state _ => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
-/
let tactic := "exact h"
let stateF ← match ← state1_1.tacticOn (goalId := 0) (tactic := tactic) with
| .success state _ => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← stateF.serializeGoals).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 (p : Prop) (x y z : Nat) : p → (p → x = y) → x + z = y + z ∧ p := by
intro hp hi
apply And.intro
conv =>
rhs
arg 1
rw [←hi]
rfl
tactic => exact hp
exact hp
def test_conv_unshielded : TestM Unit := do
let rootTarget ← parseSentence "∀ (p : Prop) (x y z : Nat), p → (p → x = y) → x + z = y + z ∧ p"
let state ← GoalState.create rootTarget
let tactic := "intro p x y z hp hi"
let .success state _ ← state.tacticOn 0 tactic | fail "intro failed"
let tactic := "apply And.intro"
let .success state _ ← state.tacticOn 0 tactic | fail "apply failed"
let .success state _ ← state.convEnter (.prefer state.goals[0]!) | fail "Cannot enter conversion tactic mode"
let .success state _ ← state.tryTactic .unfocus "rhs" | fail "rhs failed"
let tactic := "arg 1"
let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
checkEq s!" {tactic}" ((← state.serializeGoals).map (·.devolatilize))
#[
{ interiorGoal [] "y" with fragment := .conv },
{ interiorGoal [] "p" with userName? := "right", },
]
let tactic := "rw [←hi]"
let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
checkEq s!" {tactic}" state.goals.length 3
let tactic := "rfl"
let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
checkEq s!" {tactic}" ((← state.serializeGoals).map (·.devolatilize))
#[
interiorGoal [] "p",
{ interiorGoal [] "p" with userName? := "right", },
]
checkEq "(n goals)" state.goals.length 2
checkEq "(fragments)" state.fragments.size 0
let tactic := "exact hp"
let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
let tactic := "exact hp"
let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
let root? := state.rootExpr?
checkTrue "root" root?.isSome
where
interiorGoal (free: List (String × String)) (target: String) :=
let free := [("p", "Prop"), ("x", "Nat"), ("y", "Nat"), ("z", "Nat"), ("hp", "p"), ("hi", "p → x = y")] ++ free
buildGoal free target
example : ∀ (x y z w : Nat), y = z → x + z = w → x + y = w := by
intro x y z w hyz hxzw
conv =>
lhs
arg 2
rw [hyz]
rfl
exact hxzw
def test_conv_unfinished : TestM Unit := do
let rootTarget ← parseSentence "∀ (x y z w : Nat), y = z → x + z = w → x + y = w"
let state ← GoalState.create rootTarget
let tactic := "intro x y z w hyz hxzw"
let .success state _ ← state.tacticOn 0 tactic | fail "intro failed"
let convParent := state.goals[0]!
let .success state _ ← state.convEnter (.prefer convParent) | fail "Cannot enter conversion tactic mode"
let .success state _ ← state.tryTactic .unfocus "lhs" | fail "rhs failed"
let tactic := "arg 2"
let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
checkEq s!" {tactic}" ((← state.serializeGoals).map (·.devolatilize))
#[
{ interiorGoal [] "y" with fragment := .conv },
]
let tactic := "rw [hyz]"
let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
checkEq s!" {tactic}" ((← state.serializeGoals).map (·.devolatilize))
#[
{ interiorGoal [] "z" with fragment := .conv },
]
checkTrue " (fragment)" $ state.fragments.contains state.mainGoal?.get!
checkTrue " (fragment parent)" $ state.fragments.contains convParent
checkTrue " (main goal)" state.mainGoal?.isSome
let tactic := "rfl"
let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
checkEq s!" {tactic}" ((← state.serializeGoals).map (·.devolatilize))
#[
interiorGoal [] "x + z = w",
]
checkEq "(fragments)" state.fragments.size 0
checkEq s!" {tactic}" state.goals.length 1
let tactic := "exact hxzw"
let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
let root? := state.rootExpr?
checkTrue "root" root?.isSome
where
interiorGoal (free: List (String × String)) (target: String) :=
let free := [("x", "Nat"), ("y", "Nat"), ("z", "Nat"), ("w", "Nat"), ("hyz", "y = z"), ("hxzw", "x + z = w")] ++ 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 rootTarget ← parseSentence "∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d"
let state0 ← GoalState.create rootTarget
let tactic := "intro a b c d h1 h2"
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state _ => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
#[interiorGoal [] "a + b = c + d"])
let pred := "a + b = b + c"
let .success state1 _ ← state1.calcEnter state1.mainGoal?.get! | fail "Could not enter calc"
let state2 ← match ← state1.tacticOn 0 pred with
| .success state _ => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!"calc {pred} := _" ((← state2.serializeGoals).map (·.devolatilize) =
#[
{ interiorGoal [] "a + b = b + c" with userName? := .some "calc" },
{ interiorGoal [] "b + c = c + d" with fragment := .calc },
])
addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 0) |>.isNone)
addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 1) |>.isSome)
let tactic := "apply h1"
let state2m ← match ← state2.tacticOn (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.tacticOn 0 pred with
| .success state _ => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!"calc {pred} := _" ((← state4.serializeGoals).map (·.devolatilize) =
#[
{ interiorGoal [] "b + c = c + d" with userName? := .some "calc" },
])
addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? (state4.get! 0) |>.isNone)
let tactic := "apply h2"
let state4m ← match ← state4.tacticOn (goalId := 0) (tactic := tactic) with
| .success state _ => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
checkEq "(fragments)" state4m.fragments.size 0
addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome
where
interiorGoal (free: List (String × String)) (target: String) :=
let free := [("a", "Nat"), ("b", "Nat"), ("c", "Nat"), ("d", "Nat"),
("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
buildGoal free target
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[
("conv simple", test_conv_simple),
("conv unshielded", test_conv_unshielded),
("conv unfinished", test_conv_unfinished),
("calc", test_calc),
] |>.map (λ (name, t) => (name, runTestTermElabM env t))
end Pantograph.Test.Tactic.Fragment

21
doc/repl.md
View File

@ -13,7 +13,7 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
only the values of definitions are printed.
* `env.save { "path": <fileName> }`, `env.load { "path": <fileName> }`: Save/Load the
current environment to/from a file
* `env.module_read { "module": <name }`: Reads a list of symbols from a module
* `env.module_read { "module": <name> }`: Reads a list of symbols from a module
* `env.describe {}`: Describes the imports and modules in the current environment
* `options.set { key: value, ... }`: Set one or more options (not Lean options; those
have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
@ -28,16 +28,19 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
* `options.print`: Display the current set of options
* `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
Start a new proof from a given expression or symbol
* `goal.tactic {"stateId": <id>, "goalId": <id>, ...}`: Execute a tactic string on a
given goal. The tactic is supplied as additional key-value pairs in one of the following formats:
- `{ "tactic": <tactic> }`: Execute an ordinary tactic
- `{ "expr": <expr> }`: Assign the given proof term to the current goal
- `{ "have": <expr>, "binderName": <name> }`: Execute `have` and creates a branch goal
- `{ "calc": <expr> }`: Execute one step of a `calc` tactic. Each step must
* `goal.tactic {"stateId": <id>, ["goalId": <id>], ["autoResume": <bool>], ...}`:
Execute a tactic string on a given goal site. The tactic is supplied as additional
key-value pairs in one of the following formats:
- `{ "tactic": <tactic> }`: Executes a tactic in the current mode
- `{ "mode": <mode> }`: Enter a different tactic mode. The permitted values
are `tactic` (default), `conv`, `calc`. In case of `calc`, each step must
be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set
to the previous `rhs`.
- `{ "conv": <bool> }`: Enter or exit conversion tactic mode.
- `{ "draft": <expr> }`: Draft an expression with `sorry`s, turning them into goals. Coupling is not allowed.
- `{ "expr": <expr> }`: Assign the given proof term to the current goal
- `{ "have": <expr>, "binderName": <name> }`: Execute `have` and creates a branch goal
- `{ "let": <expr>, "binderName": <name> }`: Execute `let` and creates a branch goal
- `{ "draft": <expr> }`: Draft an expression with `sorry`s, turning them into
goals. Coupling is not allowed.
If the `goals` field does not exist, the tactic execution has failed. Read
`messages` to find the reason.
* `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`: