Fancy syntax for syntax

Stream: metaprogramming / tactics

[Will Bradley]

In BEq.lean, I came across the following code:

def mkMatch (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Term := do
  let discrs ← mkDiscrs header indVal
  let alts ← mkAlts
  `(match $[$discrs],* with $alts:matchAlt*)

I think it separates every element of discrs with a comma, but I'm not sure. Where in the language reference is this documented? I worry I'm missing out on other features

[Kyle Miller]

The core idea is that parsers generally have both a syntax for normal terms and a syntax for antiquotations.

Here's the definition of match syntax: https://github.com/leanprover/lean4/blob/5e40f4af52c50ff670c2b09b87930b42ff30a6ba/src/Lean/Parser/Term.lean#L469

Notice that the discriminants appear using the sepBy1 matchDiscr ", " parser. The sepBy1 p s's parser also recognizes the antiquotation syntax $[p]s*. Antiquotations are parseable everywhere. For example, while this doesn't elaborate, it does parse:

#check match $[t],* with | _ => _

It's up to elaborators to make sense of it. For example, the syntax quotation `(...) notation knows to interpret a sepBy1 antiquotation by taking the array inside and constructing the appropriate Syntax that sepBy1 would generate itself.

Without this point of view — that antiquotations come from the parsers themselves — it's easy to get the wrong idea of what's allowed and why they work! In particular, it's not that $[$discrs],* is a way to separate the discrs array with commas, but that it's a way to hook into the sepBy1 that's there in the parser.

By the way, the full form of this would be $[$discrs:matchDiscr],*. Often parsing can figure out which antiquotation it is supposed to be for, like in this case, but for a given syntax foo, the full form of the antiquotation it can parse is $x:foo, where x is an ident or a parenthesized term.

[Kyle Miller]

The Lean Language Reference has some documentation on antiquotations around here: https://lean-lang.org/doc/reference/latest///Notations-and-Macros/Macros/#quotation