Syntax categories and non-leading parsers

Stream: lean4

[Thomas Murrills]

Consider a situation where we want to, for example, introduce an extensible class of headers for match alts.

declare_syntax_category customAltHeader

We'd want something like either of the following to work:

-- `matchAlts` is not a leading parser, so fails
syntax customMatches := customAltHeader Lean.Parser.Term.matchAlts

-- `customAltHeader` is not even a parser, so this doesn't make sense
def Parser.customMatches := leading_parser customAltHeader >> Lean.Parser.Term.matchAlts

I could wrap matchAlts in a leading_parser then use syntax, but I'm a bit wary of this—would it change the behavior of something that appears everywhere?

What's the best way to accomplish this?

[Thomas Murrills]

(I'm also realizing that I have to do this with multiple non-leading parsers if I go the wrapping route, so I'm hoping for a more elegant solution! :) )

[Kyle Miller]

I'm a little confused, docs#Lean.Parser.Term.matchAlts uses leading_parser, and you can use any Parser with syntax whether or not it's using leading_parser. That macro just sets up creating a Syntax node whose kind is given by the current declaration's identifier, as well as setting up being able to handle antiquotations.

It seems like somehow matchAlts isn't working maybe because it's got an (optional) argument?

[Kyle Miller]

Making it not have an argument makes it work.

declare_syntax_cat customAltHeader

def myMatchAlts := Lean.Parser.Term.matchAlts

syntax customMatches := customAltHeader myMatchAlts

[Thomas Murrills]

Ah, ok, so when I wrapped it in leading_parser and it worked, I was really just eliminating the argument.

[Thomas Murrills]

(I’m realizing I mixed up a recent brush with “non-leading parsers don’t work in standalone syntax quotation matches” with “non-leading parsers don’t work in syntax declarations”, and was more ready to believe the leading_parser was the crucial bit…)