search

tlaplus-community / tree-sitter-tlaplus

A tree-sitter grammar for TLA⁺ and PlusCal
MIT License
57 stars 10 forks source link

Wrong precedence for prime operator #84

Closed craft095 closed 1 year ago

craft095 commented 1 year ago

Hello,

tree-sitter parses following expressions incorrectly: [] y' produces ([] y)' expected [] (y') <> y' produces (<> y)' expected <> (y') ENABLED y' produces (ENABLED y)' expected ENABLED (y') UNCHANGED y' produces (UNCHANGED y)' expected UNCHANGED (y')

Interestingly, following is parsed correctly -y' produces -(y') ~y' produces ~(y') DOMAIN y' produces DOMAIN (y') SUBSET y' produces SUBSET (y') UNION y' produces UNION (y')

Thanks for the great library!

ahelwer commented 1 year ago

Thanks for the report! I will look into this some time next week. @will62794 for FYI

ahelwer commented 1 year ago

@craft095 can you double check that SANY parses these as you state are correct instead of giving you a parse error? TLA+ takes an idiosyncratic approach to operator precedence where operators have precedence ranges, and if the range of two operators overlap it's a parse error for them to not be disambiguated with parentheses. The prime operator has precedence 15-15 versus the prefix operators you list have precedence 4-15, per page 271 of specifying systems. See section 15.2.1 on page 283 for an explanation of the rules.

craft095 commented 1 year ago

@ahelwer You are right: those indeed result in parse errors. I created a bunch of test cases for my TLA+ style checking tool, and some of these tests happened to be syntactically incorrect. Sorry about that. Thank you!