Fix simple-ltid.cu #661
Merged
Fix simple-ltid.cu #661
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
A rewrite rule is added which ensures that any permission that gets written to Perm(field, integerExpression) gets rewritten to Perm(field, fracExpression). Previously the rewrite system could produce terms that were not well-typed (i.e. produced non-well-typed terms). simple-ltid.cu is also removed from suite problem-fail.
The rule perm_fix_frac is moved to the end as it seems to interefere with applying the rule for Perm(xs[*], e1). Doing it later should still work, and not interfere with the rule for xs[*].
Previously the typechecker would force the secon argument of a Perm to be frac. This would cause the rewriter to rewrite an int variable as a frac. We narrow this to only forcing literals to be frac, and leave all other types as they are. This ensures expressions like "read" are not matched against rewrite matching variables of type int.
24 tasks
Vescatur
requested changes
Jul 16, 2021
|
Kudos, SonarCloud Quality Gate passed! |
|
After some discussion with @Vescatur we decided to merge the PR. |
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.
To fix simple-ltid.cu, typechecking had to be made stricter.
Typechecking is made less lenient, by not forcing arguments of Perm to frac. Specifically, before, given
Perm(x.f, a),awould always be forced to be typechecked asfrac, even if it is anint. This PR changes it such thatais only forced to be a frac if it is a literal (say, 1 or 0). Otherwise, the type is left as is.By not forcing all possible arguments of perm to frac, some rewrite rules had to be changed to match a frac explicitly, instead of an integer.
Additionally, a rewrite rule is added that rewrites any expression
Perm(f, a), whereais of typeint, toPerm(f, a \ 1), such that passing anintto a perm works out as expected, instead of causing an error. This was also needed to get simple-litd.cu to work.