Exceptions #365
Merged
Exceptions #365
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
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.
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
|
Can you point me to some documentation on this new feature? I'm going to try to update the reference manual and need to collect documentation of features since it was last edited. |
|
Here is the current description of the feature: dafny-lang/rfcs#1 |
|
You can also find some of this information as comments in Resolver.cs:
|
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.
This PR might contain everything needed to get desugaring of
:-.I say might because I have not yet tested it as thoroughly as I think it should be tested, but I'm blocked on #364.
Still to be tested:
:-:-on expression level, should it also print the desugared term?Result<T>instead ofNatOutcomewhereTis hardcoded toNat:-on expression level