fix: calc of multiset crashes #2079
Merged
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
MikaelMayer
added
kind: bug
RELEASE_NOTES.md
Outdated
| @@ -22,6 +22,7 @@ | |||
| - fix: Prevent refinements from changing datatype and newtype definitions (https://github.com/dafny-lang/dafny/pull/2038) | |||
| - feat: The new `older` modifier on arguments to predicates indicates that a predicate ensures the allocatedness of some of its arguments. This allows more functions to show that their quantifiers do not depend on the allocation state. For more information, see the reference manual section on `older`. (https://github.com/dafny-lang/dafny/pull/1936) | |||
| - fix: Fix `(!new)` checks (https://github.com/dafny-lang/dafny/issues/1419) | |||
| - fix: multiset keyword no more crashes the parser (https://github.com/dafny-lang/dafny/pull/2079) | |||
There was a problem hiding this comment.
nitpick: multiset keyword no longer crashes the parser
Source/Dafny/Dafny.atg
Outdated
| @@ -386,7 +386,8 @@ bool IsSetDisplay() { | |||
| if (la.kind == _lbrace) return true; | |||
| int k = scanner.Peek().kind; | |||
| if (la.kind == _iset && k == _lbrace) return true; | |||
| if (la.kind == _multiset && (k == _lbrace || k == _openparen)) return true; | |||
| // Until there is a multiset comprehension, there is no point in checking the next item. | |||
There was a problem hiding this comment.
I would remove the // and the /* comment. I don't think a future implementor of multiset comprehensions needs these.
keyboardDrummer
previously approved these changes
May 2, 2022
MikaelMayer
commented
May 2, 2022
MikaelMayer
commented
May 2, 2022
cpitclaudel
requested changes
May 2, 2022
cpitclaudel
approved these changes
May 2, 2022
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.
Fixes #2078
calc{multiset}triggers a while loop that will try to get all inner statements, but the while loop is guarded by something that checks if the next element is the start of an expression, which it is (multisetcan be the start of an expression). However, since it is not a valid expression, it will emit an error, store a dummy expression, and continue without changing the scanner's position.The problem does not arise with
isetbecause that keyword can be used both for set display and set comprehension, so the scanner can continue in any case.Since there is no multiset comprehension for now, I removed the lookahead code so that now multiset always expects a
(or a{after it, and the scanner can move on in any case.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.