Repository navigation
Conversation
lemmy
added
bug
lemmy
marked this pull request as ready for review
November 6, 2026 02:29
There was a problem hiding this comment.
🟢 Approval recommended
No active review issues remain to block approval of the operator-precedence changes.
No open issues 🎉
What changed in this PR
This PR addresses the tlapm side of the ambiguity reported in tlaplus/rfcs#28 by rejecting conflicting operator precedence unless associativity resolves it.
Changes:
- Track canonical operator names so aliases retain consistent associativity.
- Reject ambiguous expressions with a diagnostic requesting parentheses.
- Add precedence regression tests and explicitly parenthesize affected LSP test expressions.
| File | Description |
|---|---|
test/parser/precedence_tests.ml |
Tests ambiguity rejection, parentheses, associativity, and aliases. |
test/parser/dune |
Registers the precedence test suite. |
src/pars/pco.mli |
Documents canonical operator names in parser items. |
src/pars/pco.ml |
Detects precedence conflicts during operator resolution. |
src/pars.mli |
Updates the exposed operator-item type. |
src/expr/e_parser.ml |
Supplies canonical names for expression operators. |
lsp/test/test_decompose_goal.ml |
Parenthesizes chained equivalence expressions. |
lsp/test/test_decompose_assm.ml |
Parenthesizes chained implication expressions. |
Review effort: Balanced
lemmy
force-pushed
the
mku-gh892
branch
2 times, most recently
from
November 7, 2026 02:17
4ac4f6b to
da58bcd
Compare
Member
Author
Contributor
|
Please stop tagging me to review slop PRs that you don't understand |
lemmy
force-pushed
the
mku-gh892
branch
2 times, most recently
from
November 8, 2026 16:57
684864c to
38a6f2a
Compare
Precedence tests need to verify grouping, distinguish ambiguity from unrelated syntax errors, and guard against rejecting valid input. [Tests] Co-authored-by: GPT-6.1 Sol Ultra <noreply@openai.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Stable printer output does not guarantee preserved expression structure or label scope. Round-trip checks must compare the original and reparsed expressions. [Tests] Co-authored-by: GPT-6.1 Sol Ultra <noreply@openai.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Associativity applies to repetitions of one infix operator, including its aliases. Precedence resolution needs canonical operator names to distinguish these chains from mixed operators. [Refactor] Co-authored-by: GPT-6.1 Sol Ultra <noreply@openai.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Overlapping precedence ranges can leave expression grouping unspecified. Require parentheses unless associativity resolves the conflict for the same canonical operator. Implements the decision in tlaplus/rfcs#28. [Bug][Tests] Co-authored-by: GPT-6.1 Sol Ultra <noreply@openai.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
The authoritative Summary of TLA+ and SANY's Operators.java define % as non-associative (assocNone, precedence 100-110 in SANY). A % B % C requires parentheses to specify its grouping. Implements the decision in tlaplus/rfcs#28. [Bug][Tests] Co-authored-by: GPT-6.1 Sol Ultra <noreply@openai.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Missing parentheses can change product nesting, subscript grouping, or label scope when reparsed. LSP proof decomposition needs the printer to preserve that structure when generating proof steps. [Bug][Tests] Co-authored-by: GPT-6.1 Sol Ultra <noreply@openai.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Member
Author
|
@damiendoligez Would you prefer that I move the formatter changes (94d1a77) into a separate PR to keep this PR focused solely on the soundness issue? |
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
tlaplus/rfcs#28