Allowing precedence in `nodeWithAntiquot` parsers

Stream: lean4

[Anand Rao Tadipatri]

I was recently in a situation where it would have been convenient to attach a precedence to a syntax abbreviation like

syntax:80 my_stx := num <|> str

However, Lean only allows abbreviations without precedence:

syntax my_stx := num <|> str

This seems to be because unlike docs#Lean.ParserDescr.node, docs#Lean.ParserDescr.nodeWithAntiquot does not come with an argument representing precedence.

A possible workaround for this is to declare a new syntax category for the abbreviation and assign precendences while declaring the syntax that belongs to this category, but this feels a bit clunky.

declare_syntax_cat my_stx
syntax:80 num : my_stx
syntax:80 str : my_stx

Would precedences in nodeWithAntiquot parsers be a useful feature to have, or might it interfere with the existing parsing framework?

[Sebastian Ullrich]

Could you say more about the use case?

[Anand Rao Tadipatri]

The use-case was in creating a DSL for a mini programming language.
We wanted to support let declarations like

declare_syntax_cat line
syntax "let" ident (":" type)? ":=" value ";" : line

but ran into the issue of precedences for values
(so for instance, let x := 1 + 2; would not be parsed correctly unless 1 + 2 is parsed before the rest of the declaration)

The value type is defined as an abbreviation for the union of a few other types

syntax value := int <|> bool <|> ident

so setting a precedence for it is not directly possible.

[Anand Rao Tadipatri]

I was about to follow up my previous message with an #mwe, but strangely, I'm having trouble reproducing the error now! It looks like the syntax for abbreviation works just fine now.