Writing parsers

Stream: lean4

[Thomas Murrills]

I've got a couple of related questions about manually-defined parsers (via def myParser : Parser := ...):

1. What are the rules around using functions that return parsers within syntax declarations? For example, something like sepByIndent ident ", " (allowTrailingSep := true) doesn't seem to work in that context, but many(p) is ok (but not many p). (I couldn't find any info on this in the metaprogramming book.)
2. If your parser is too complicated for syntax, how do you then match on syntax that gets parsed by it—or even just extract various pieces? For example, how would you extract the syntax consumed by sepByIndent ... and act on it, say, during elaboration?
3. Can you use parsers in antiquotations somehow? For example in $x:ident, ident is a parser; but how do we use more complicated expressions that evaluate to parsers?

[Thomas Murrills]

@Gabriel Ebner provided one possible answer to number 3 implicitly in Creating SyntaxNodeKinds for parsers: if you give a name to your parser using def with leading_parser, i.e. def myParser : Parser := leading_parser ..., then antiquotations of the form$x:myParser will be automatically usable. (Thanks!)

[Gabriel Ebner]

To answer your other questions. Iirc you can use any Parser in a ParserDescr (what syntax produces). The other way around doesn't work (without criminal energy)

[Gabriel Ebner]

Parser combinators like many1 work in ParserDescr if you export them using register_parser_alias

[Gabriel Ebner]

That only works for Parser -> Parser and Parser -> Parser -> Parser though.

[Gabriel Ebner]

sepBy is hard coded

[Gabriel Ebner]

As for 2: antiquotations are part of the parser. sepBy also parses $x,* and $[x],*.

[Gabriel Ebner]

For those strings the parser simply produces an antiquotation node.

[Gabriel Ebner]

The syntax matches are hard coded iirc. You can't define your own antiquotation with a HashMap Name Term for example.

[Sebastian Ullrich]

The antiquotation kinds do not directly correspond to parsers but to invocations of docs4#Lean.Parser.mkAntiquot. syntax := and leading_parser implicitly introduce this parser, yes.

[Thomas Murrills]

That's all very useful info! Thanks! :)