Fixes parsing of magic wands#1044
Conversation
There was a problem hiding this comment.
Pull request overview
This PR addresses a parser ambiguity introduced by the switch to {...} predicate-constructor arguments: braces following a magic-wand package statement could be parsed as predicate-constructor args of the wand’s RHS expression instead of as the package proof block (issue #1043). The fix tightens the grammar/translation so postfix predicate constructors must end in an explicit selector, preventing {} from attaching to arbitrary primary expressions like P().
Changes:
- Restrict postfix predicate constructors to
primaryExpr . IDENTIFIER { ... }and add a dedicated parenthesized escape form in the grammar. - Update parse-tree translation to match the new parse-tree shape for predicate constructors (including parenthesized forms).
- Add regression and unit tests for selector-ended predicate constructors and the original wand-proof-block regression.
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
| src/main/antlr4/GobraParser.g4 | Tightens predicate-constructor postfix syntax to require a final selector and adds an explicit parenthesized escape alternative. |
| src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala | Updates translation logic to construct PPredConstructor only for selector-ended bases and for the new parenthesized escape rule. |
| src/test/scala/viper/gobra/parsing/ParserUnitTests.scala | Adds unit tests to ensure selector-ended (and parenthesized selector-ended) predicate constructors parse as PPredConstructor. |
| src/test/resources/regressions/issues/001043.gobra | Adds a regression program covering the original package P() --* P() {} failure mode and predicate constructors within wands. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
jcp19
left a comment
jcp19
left a comment
There was a problem hiding this comment.
LGTM, just have one question
| // This postfix form must select the predicate identifier explicitly. Requiring a final selector | ||
| // prevents the `{ ... }` of an enclosing construct (for example, a magic-wand package proof block | ||
| // after `P() --* P()`) from being consumed as predicate-constructor arguments after an arbitrary | ||
| // primary expression. The receiver before the final selector can still be any primary expression. | ||
| // Single- and two-component unparenthesized names (`P{...}` and `pkg.P{...}`) are parsed as | ||
| // composite literals and disambiguated later. Keep the documented parenthesized escape syntax | ||
| // (`(P){...}` and `(pkg.P){...}`) with the same restriction: either a bare predicate name or a | ||
| // primary expression with a final selected predicate identifier. |
There was a problem hiding this comment.
this is super verbose and not very clear. Does this impose restrictions on the kinds of predicate instance expressions that one can construct? If so, which kinds of expressions does it disallow? Orienting the comment around that and explaining why those restrictions are in place would make it clear to me (ideally, the comment would also be shorter and more to the point)
There was a problem hiding this comment.
Not sure I excelled at making it more concise but the comment clarifies now how we parse predicate constructors
There was a problem hiding this comment.
looks much better now, thanks!
|
LGTM |
Fixes #1043