Extending tacticSeqs

Stream: lean4

[Reinier van der Gronden]

I'm looking to understand the best way of working with tacticSeqs. Up to this point, I've worked with tactic, but I want to implement a tactic that make changes to a 'group of tactics', which is basically a tacticSeq. I struggle to find ways to take an existing tacticSeq, and make some changes to it.

One of the main issues for me is that I don't properly know how to work with parsers yet, and tacticSeq seems to be some sort of parser-wrapper around a list of tactics (but not really).

a MWE for my use case is as follows:

import Lean

open
  Lean
  Lean.Elab.Tactic
  Lean.Parser.Tactic

#eval Lean.versionString -- 4.0.0, commit 7dbfaf9b751917a7fe020485bf57f41fdddcaafa

def testTactic (tacSeq : TSyntax ``tacticSeq) : TacticM Unit := do
  let tacSeqStr := toString tacSeq
  addTrace `test m!"{tacSeqStr}"

elab &"testTactic " t:tacticSeq : tactic =>
  testTactic t

example : true := by
  testTactic
    rfl
    rfl
  sorry

The testTactic now adds the trace object (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(group (Tactic.tacticRfl "rfl") []) (group (Tactic.tacticRfl "rfl") [])])). What would be the proper way of, say, extending/appending this tacticSeq with another rfl call?

Alternatively, how can you consistently get a 'list of tactics' that are inside the tacticSeq? With that, it would be easier to construct a new tacticSeq like `(tacticSeq|($[$tacs]*)), but I'm pretty sure that objects inside the tacticSeq need not necessarily be tactics, they can also be nested tacticSeqs. For example, changing the above example to

example : true := by
  testTactic
    rfl
    {
      rfl
      rfl
    }
    rfl
  sorry

Adds the trace (Tactic.tacticSeq1Indented [(group (Tactic.tacticRfl "rfl") []) (group (Tactic.tacticSeqBracketed "{" [(group (Tactic.tacticRfl "rfl") []) (group (Tactic.tacticRfl "rfl") [])] "}") []) (group (Tactic.tacticRfl "rfl") [])])), where it contains a tacticSeq, not just a list of tactics.

[Reinier van der Gronden]

For those interested, with the help of @Jannis Limperg , we have constructed a function that matches on the tacticSeq and appends a tactic to it. Our solution looks like this, with a bit of matching magic:

def mkTacticSeqAppend (ts : TSyntax ``tacticSeq) (t : TSyntax `tactic) : TermElabM (TSyntax ``tacticSeq) :=
  match ts with
  | `(tacticSeq| { $[$tacs:tactic $[;]?]* }) =>
    `(tacticSeq| { $[$(tacs.push t)]* })
  | `(tacticSeq| $[$tacs:tactic $[;]?]*) =>
    `(tacticSeq| $[$(tacs.push t)]*)
  | _ => throwError "unknown syntax"

Having access to the list of tactics inside of the tacticSeq makes it much easier to make arbitrary changes and create a new tacticSeq. The fact that the list of tacs can contain a tacticSeq(Bracketed) itself doesn't seem to matter, since this should/seems to always be interpretable as a tactic (focus a goal and execute this list of tactics).