Left-associative parsing

Stream: lean4

[Arthur Adjedj]

Hi, when trying to make a parser for a functional programming langage, I encountered the following issue: here, a b c parses as a syntax of the form [a,[b,[c]]] when I'd like it to be parsed as [a,[b,c]]. What would be the easiest way to do that ?

declare_syntax_cat foo
syntax ident : foo
syntax foo foo+ : foo

#check `(foo|a b c)

[James Gallicchio]

I think that is just how the + combinator works (it accepts at least 1 but potentially more foos). You may want a more explicit recursion like so:

declare_syntax_cat foo
syntax:11 ident : foo
syntax:10 foo:11 foo:10 : foo

#check `(foo|a b c)

using precedences you can make the desired associativity clear :)

[James Gallicchio]

(swapping the 10 and 11 in the last rule gives a left-associative parse tree)

[Arthur Adjedj]

That's exactly what I was looking for ! Thanks a lot :)

[James Gallicchio]

I'm not sure if you've stumbled onto it yet but the metaprogramming book is a great general resource on syntax/macros/elaboration. Might be worth a gander :D

[Arthur Adjedj]

I did, and I thought that working with precedences would probably resolve the issue, but it wasn't clear to me how. In particular, the book only shows (and doesn't detail) that you can put precedence on the syntax keyword, but not on the syntax categories themselves like syntax foo:10 : bar, this was the missing piece for me. I should have probably paid more attention to the part describing notations, which did introduce precedence.

[James Gallicchio]

That's a good point. Maybe open an issue on the repo, since (IMO) that should be discussed when it brings up precedences