Lean4
/-- Parse an infotree to find all the sequences of tactics contained within `stx`.
We consider a sequence here to be a maximal interval of tactics joined by `;` or newlines.
This function returns an array of sequences. For example, a proof of the form:
```
by
tac1
· tac2; tac3
· tac4; tac5
```
would result in three sequences:
* `#[tac1, (· tac2; tac3), (· tac4; tac5)]`
* `#[tac2, tac3]`
* `#[tac4, tac5]`
Similarly, a declaration with multiple `by` blocks results in each of the blocks getting its
own sequence.
-/
def findTacticSeqs (stx : Syntax) (tree : InfoTree) : CommandElabM (Array (Array (ContextInfo × TacticInfo))) := do
let some enclosingRange := stx.getRange? |
throw
(Exception.error stx m!"operating on syntax without range")
-- Turn the CommandElabM into a surrounding context for traversing the tree.
let ctx ← read
let state ← get
let ctxInfo := { env := state.env, fileMap := ctx.fileMap, ngen := state.ngen }
let out ←
tree.visitM (m := CommandElabM) (ctx? := some ctxInfo)
(fun _ i _ => do
if let some range := i.stx.getRange? then
pure <| enclosingRange.start <= range.start && range.stop <= enclosingRange.stop
else
pure false)
(fun ctx i _c cs => do
let relevantChildren := (cs.filterMap id).toArray
let childTactics := relevantChildren.filterMap Prod.fst
let childSequences := (relevantChildren.map Prod.snd).flatten
let stx := i.stx
if let some (.original _ _ _ _) := stx.getHeadInfo? then
-- Punctuation: skip this.
if stx.getKind ∈ [`«;», `Lean.cdotTk, `«]», nullKind, `«by»] then
return
(none, childSequences)
-- Tactic modifiers: return the children unmodified.
if stx.getKind ∈ [``Lean.Parser.Tactic.withAnnotateState] then
return
(childTactics[0]?, childSequences)
-- Tactic sequencing operators: collect all the child tactics into a new sequence.
if
stx.getKind ∈
[``Lean.Parser.Tactic.tacticSeq, ``Lean.Parser.Tactic.tacticSeq1Indented,
``Lean.Parser.Term.byTactic] then
return
(none, if childTactics.isEmpty then childSequences else childSequences.push childTactics)
-- Remaining options: plain pieces of syntax.
-- We discard `childTactics` here, because those are either already picked up by a
-- sequencing operator, or come from macros.
if let .ofTacticInfo i := i then
return ((ctx, i), childSequences)
return (none, childSequences)
else
return (none, childSequences))
return (out.map Prod.snd).getD #[]
