Why `getOptional?` is not working for `(tacticSeq)?`?

Stream: metaprogramming / tactics

[Dexin Zhang]

I have this example:

syntax (name := test) "test" ("by " colGt tacticSeqIndentGt)? : tactic
@[tactic test] def implTest : Tactic := fun stx => do
  logInfo m!"{repr stx[1]}, {stx[1].getOptional?}"

example : True := by
  test
  test by trivial
  sorry

I see stx[1] got something in the second test, but stx[1].getOptional? is returning none. Is it designed that way, or is that a bug?

[Robin Arnez]

Hmm I see the documentatation is not the best here, better would maybe be

/--
Assuming `stx` was parsed by `optional`, returns the enclosed syntax
if it parsed exactly one syntax node and `none` otherwise.
-/

In other words, docs#Lean.Syntax.getOptional? only works when there is exactly one node inside of it; here you have 2 though: "by " and tacticSeqIndentGt.
Anyways, you should usually not need to bother with this, use elab or elab_rules or in general syntax match instead:

import Lean

syntax (name := test) "test" ("by " colGt tacticSeqIndentGt)? : tactic

open Lean in
elab_rules : tactic
| `(tactic| test $[by $seq]?) =>
  logInfo m!"{seq}"

example : True := by
  test -- none
  test by trivial -- some (trivial)
  sorry

[Dexin Zhang]

Robin Arnez said:

Hmm I see the documentatation is not the best here, better would maybe be

/--
Assuming `stx` was parsed by `optional`, returns the enclosed syntax
if it parsed exactly one syntax node and `none` otherwise.
-/

In other words, docs#Lean.Syntax.getOptional? only works when there is exactly one node inside of it; here you have 2 though: "by " and tacticSeqIndentGt.
Anyways, you should usually not need to bother with this, use elab or elab_rules or in general syntax match instead:

[Dexin Zhang]

Thanks! I found that doing matching on stx[2].getArgs also solves the problem, but I felt that's not the standard way to do so. Your solution is definitely more elegant!