Annotating nested types in syntax matches

Stream: lean4

[Eric Wieser]

Is there any way to combine these two syntax matches into one? I can't work out how to add :declaration into the second match:

import Lean
open Lean

def getModifiers (s : TSyntax `command) :
    Option (TSyntax ``Parser.Command.declModifiers) := do
  let `(command| $d:declaration) := s | failure
  let `(command| $m:declModifiers $_d) := d | failure
  return m

[Eric Wieser]

Actually, even this doesn't seem to do what I expect; the second syntax match is not using the knowledge that the syntax is a declaration, and still tries to match against

syntax (name := ohno) declModifiers ident : command

elab_rules : command
| `(command| $m:declModifiers $_:ident) => pure ()

[Eric Wieser]

It does still produce the right answer at least:

-- none
#eval show MetaM _ from return getModifiers <| ←`(@[simp] wat)

[Eric Wieser]

The generated code here is very strange:

import Lean
open Lean

syntax (name := ohno) declModifiers ident : command

elab_rules : command
| `(command| $m:declModifiers $_:ident) => pure ()

def getModifiers (s : TSyntax `command) :
    Option (TSyntax ``Parser.Command.declModifiers) := do
  let `(command| $m:declModifiers $_d) := s | failure
  return m

#print getModifiers

it seems to be checking for a declaration inside my ohno node.

[Kyle Miller]

Looking at docs#Lean.Parser.Command.declaration, the declModifiers are part of the declaration, so trying to match $m:declModifiers $d:declaration doesn't make sense

[Kyle Miller]

I'm a bit confused why this doesn't work

def getModifiers (s : TSyntax `command) :
    Option (TSyntax ``Parser.Command.declModifiers) := do
  let `(command| $m:declModifiers $d:Lean.Parser.Command.definition) := s | failure
  return m

but I seem to remember having the experience that you can't match on a whole declModifiers, but rather you have to match each of its components.

[Eric Wieser]

Kyle Miller said:

trying to match $m:declModifiers $d:declaration doesn't make sense

I want to match ($m:declModifiers $d):declaration, as opposed to "any old syntax that starts with declModifiers"

[Eric Wieser]

Unfortunately that notation doesn't exist

[Kyle Miller]

Oh right, I read that completely backwards, sorry

[Kyle Miller]

I've felt that there should be an extension to $[...] syntax where they can be used as "quotation parentheses" to group anything, and that you should be able to put a syntax kind after them. Currently, they only work for $[...]? and $[...]*, etc.

[Kyle Miller]

This would enable this solution to your problem: let `(command| $[$m:declModifiers $_d]:declaration) := s | failure

[Kyle Miller]

I've run into cases where it's impossible to write patterns without this $[...] feature, and instead I needed to split them up across multiple patterns.

They could also be used to prevent parenthesis insertion, which can be an issue since parentheses do create a syntax node.

[Eric Wieser]

I think this might explain why I have never been able to grok $[...] syntax; I falsely assumed it was valid in some context by itself.

[Eric Wieser]

I guess this would also work for $[$m:declModifiers $_d]%$tk? (not that I actually need that)

[Kyle Miller]

Yeah, that would be nice to have. The abs app unexpander could be simplified a bit if you could assign a matched term to a variable.

[Kyle Miller]

Using this non-existent syntax, one of the patterns is $_ $[- $a] since without that grouping the - would be subtraction rather than negation, but you can't use parentheses because that would entail needing parentheses to exist (and they don't exist when app unexpanders are run).

The actual pattern needed is $_ $[- $_]%$a, so that this a can be dropped into another expression.