[do not merge] WIP Exceptions #348
Closed
Conversation
This file contains 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
DeclareDatatype and related functions taken from C# and simplified as recommended, only add to make sure program compiles end-to-end cr https://code.amazon.com/reviews/CR-9639411
… /compile:3 is set
…nto java-compiler
cr https://code.amazon.com/reviews/CR-9853069 Change tuple size identification
…nto java-compiler
Java compiler
Outright forbid the previously deprecated semi-colon at the end of (co)datatype declarations (since it clashes with where the curly braces for the type members go.)
Oddly enough, although this commit only changes the compiler and the compiler is not invoked in Test/cloudmake/CloudMake-ConsistentBuild.dfy, this file started failing under lit. From the command line, it was fine. Adding command-line flag `/restartProver` seems to stabilize the verification back to normal.
This name-clash bug was detected by Travis, but didn't show up with the VS 2019 Community C# compiler. Evidently, warnings produced by the VS compiler don't show up in the output, whereas the C# compiler on Travis does.
Coco says "LL1 warning in UnaryExpression: lbrace is start of several alternatives"
is start of several alternatives"
The problem was that I made the `var pattern` part preceding `:=` or
`:|` optional (from Coco's point of view), because it's optional for
`:-`, and enforced presence of `var pattern` using `SemErr`.
However, since `:|` can be preceded by attributes, which start by
`{`, and set display starts by `{` as well, one look-ahead is not
enough any more when parsing an expression, as we have to determine
whether we should parse a `{:myAttribute} :|` (which will later be
rejected by a SemErr saying that `:|` needs an LHS) or a `{1, 2, 3}`.
The idea is to leave the `LetExpr` rule untouched wrt master,
and write a separate rule for `LetOrFailExpr` for `:-`, which turns
out to introduce less code duplication than feared, and is simpler
to read too.
But now we have to disambiguate between `LetExpr` and `LetOrFailExpr`,
which would require lookahead until we encounter `:=`, `:|`, or `:-`,
which we would have to implement manually without being able to
reuse Coco-generated code for rules, which does not sound like a
good thing to try.
This reverts commit b6f9aa1.
Make `{:` a token instead of two separate tokens.
This looks like a neat thing to do, because it allows us to get
rid of many `IF(IsAttribute())` manual disambiguations.
Note that IsExistentialGuard needed to be updated to look for
lbracecolon instead of lbrace followed by colon.
Also note that strictly speaking, this is a breaking change:
Previously, `{ :myAttribute}` was accepted, but now it isn't any
more, and you have to remove the space.
But the whole test suite passes, so I think it's ok to enforce
a consistent style of not allowing a space between `{` and `:`.
However, we get more Coco warnings:
(Note that "deletable structure" seems to be Coco jargon for an optional
piece of syntax, i.e. what's written as "{ foo }" in Coco)
LL1 warning in IteratorSpec: lbracecolon is start & successor of deletable structure
LL1 warning in IteratorSpec: lbracecolon is start & successor of deletable structure
LL1 warning in IteratorSpec: lbracecolon is start & successor of deletable structure
LL1 warning in IteratorSpec: lbracecolon is start & successor of deletable structure
LL1 warning in MethodSpec: lbracecolon is start & successor of deletable structure
LL1 warning in MethodSpec: lbracecolon is start & successor of deletable structure
LL1 warning in MethodSpec: lbracecolon is start & successor of deletable structure
LL1 warning in MethodSpec: lbracecolon is start & successor of deletable structure
LL1 warning in FunctionSpec: lbracecolon is start & successor of deletable structure
LL1 warning in FunctionSpec: lbracecolon is start & successor of deletable structure
LL1 warning in AssertStmt: lbracecolon is start & successor of deletable structure
LL1 warning in AssumeStmt: lbracecolon is start & successor of deletable structure
LL1 warning in ModifyStmt: lbracecolon is start & successor of deletable structure
LL1 warning in LoopSpec: lbracecolon is start & successor of deletable structure
LL1 warning in LoopSpec: lbracecolon is start & successor of deletable structure
LL1 warning in LoopSpec: lbracecolon is start & successor of deletable structure
And these are to be taken seriously: They happen whenever a list of attributes
(which can be of length 0) precedes an Expression (which now can start with
attributes, too), so it's ambiguous whether the attributes belong to the thing
being parsed, or whether they belong to the Expression because the Expression
starts with a `{:attr} :|` or a `{:attr} :-`.
time lit tests
except the two warnings which are already present on master: Coco/R (Apr 19, 2011) checking OldSemi deletable OptGenericInstantiation deletable parser + scanner generated 0 errors detected
rerunning coco to fix merge conflicts in Parser.cs
|
Can you rebase this PR to start after the big java-compiler and type-members merges? |
RustanLeino
reviewed
Aug 20, 2019
| @@ -773,6 +765,7 @@ TOKENS | |||
| ensures = "ensures". | |||
| ghost = "ghost". | |||
| witness = "witness". | |||
| lbracecolon = "{:". | |||
There was a problem hiding this comment.
This is a change to the grammar, since the previous grammar treated "{" and ":" as two separate tokens. I like the way this change simplifies the grammar. This could be made into a separate pull request.
RustanLeino
reviewed
Aug 20, 2019
This was referenced Aug 22, 2019
|
Superseded by #361 |
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.
I'd like to use this PR to get early feedback on the Exceptions feature implementation.
So far I only have a tiny change: I added
:-as an alias for:=(not what we eventually want), but instead of literally making it an alias, I already create a new AST nodeAssignOrReturnStmtfor it, and use the resolver to set itsResolvedStmtfield.