Lean4
/-- Run the `config` against a sequence of tactics, using the `trigger` to determine which
subsequences should be `test`ed. -/
def runPass (config : ComplexConfig) (seq : Array (ContextInfo × TacticInfo)) : CommandElabM Unit := do
let mut acc := none
let mut firstInfo := none
let mut tacticSeq := #[]
for (ctxI, i) in seq do
if firstInfo.isNone then
firstInfo := some (ctxI, i)
let stx : TSyntax `tactic := ⟨i.stx⟩
tacticSeq := tacticSeq.push stx
match config.trigger acc stx with
| .continue ctx =>
acc := ctx
| .skip =>
acc := none
tacticSeq := #[]
firstInfo := none
| .accept ctx =>
if let some (ctxI, i) := firstInfo then
testTacticSeq config tacticSeq ctxI i ctx
else
logWarningAt stx m!"internal error in tactic analysis: accepted an empty sequence."
acc := none
match config.trigger acc (← `(tactic| done)) with
| .accept ctx =>
if let some (ctxI, i) := firstInfo then
testTacticSeq config tacticSeq ctxI i ctx
| _ =>
pure ()
