[do not merge] Exceptions2 #361
Draft
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
inside dafny\Source\Dafny, using the command ..\..\third_party\Coco\bin\Coco.exe Dafny.atg -namespace Microsoft.Dafny -frames ..\..\third_party\Coco\src
use PartiallyResolveTypeForMemberSelection to get Type instead of `?` in error message
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} :-`.
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
|
It took me four attempts to get parsing of
I wonder whether I should preserve these commits when rebasing, so that future contributors can discover and reproduce all the issues, but this might take some tweaking to replay on top of the new master, or if I should just put the final solution into one commit, which creates a cleaner history, but with less information. |
|
You asked about preserving the four commits. I think either way is fine, so do what's easiest for you. |
|
I looked at the four commits and they look good to me. If that's the whole net effect of this pull request, then please resolve the conflicts and I'll merge it. |
RustanLeino
added
do not merge
status: implemented
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.
A more reviewable version of #348.
Still work in progress.
Once #360 is merged (or closed, doesn't matter for Exceptions), I will rebase this.
So far, I think I have everything for
:-on statement level, as well as parsing for:-on expression level, but desugaring and testing for:-on expression level is still missing.