Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix precedence for quantifiers and triple-op exprs #26

Merged
merged 1 commit into from
Feb 7, 2024

Conversation

jaybosamiya
Copy link
Collaborator

Fixes #25

Basically, rather than considering &&& and ||| to be prefix+binary operations (as the actual Verus parser does), we instead split them out into their own expression group. This allows us to fix the parsing precedence with respect to quantifiers.

Copy link
Contributor

@parno parno left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks reasonable to me, and I don't see places where it would create conflicts with block_exprs (as further evidenced by the block-related tests still passing).

@parno parno merged commit cbcd829 into main Feb 7, 2024
2 checks passed
@parno parno deleted the quantifier-tripleop-precedence branch February 7, 2024 18:37
jaybosamiya added a commit that referenced this pull request Feb 13, 2024
Important changes:
* reduce collapsing of various multiple single-line comments
* fixed extra spaces in if-expressions with negation (#24)
* fixed precedence for quantifiers and `&&&` and `|||` (#26)
* handle macro call statements (#27)
* improved handling of non-inline single-line comments (#28)
jaybosamiya added a commit that referenced this pull request Feb 13, 2024
Important changes:
* reduce collapsing of various multiple single-line comments
* fixed extra spaces in if-expressions with negation (#24)
* fixed precedence for quantifiers and `&&&` and `|||` (#26)
* handle macro call statements (#27)
* improved handling of non-inline single-line comments (#28)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Incorrect operator precedence for &&& and forall
2 participants