Fix non-exhaustive switches #1092
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
shonfeder
commented
Aug 4, 2023
Comment on lines
+430
to
449
| case 'let': | ||
| { | ||
| if (transformer.enterLet) { | ||
| newExpr = transformer.enterLet(newExpr) | ||
| } | ||
|
|
||
| const opdef = transformDefinition(transformer, newExpr.opdef) | ||
| if (opdef.kind !== 'def') { | ||
| // This should only happen if we write a bad transformer. Should never | ||
| // be a user facing issue. | ||
| throw new Error('Let operator definition transformed into non-operator definition') | ||
| } | ||
|
|
||
| newExpr.opdef = opdef | ||
| newExpr.expr = transformExpression(transformer, newExpr.expr) | ||
|
|
||
| if (transformer.exitLet) { | ||
| newExpr = transformer.exitLet(newExpr) | ||
| } | ||
| } |
There was a problem hiding this comment.
This was just a formatting change.
Comment on lines
-534
to
-535
| default: | ||
| msg = 'Unknown error' |
There was a problem hiding this comment.
This case was redundant b/c it's checked for in the if on line 483.
| return entities.length > 1 ? { kind: 'union', entities: entities } : entities[0] | ||
| } else { | ||
| return { kind: 'concrete', stateVariables: vars } | ||
| if (entity.kind == 'union') { |
There was a problem hiding this comment.
I changed this from a switch that just had one branch to a conditional.
Comment on lines
+395
to
+397
| if (!ir.isQuintBuiltin(app)) { | ||
| this.applyUserDefined(app) | ||
| } else { |
There was a problem hiding this comment.
The only change here was adding a conditional using a type guard to check whether we have a builtin before dispatching the builtins.
| @@ -51,49 +52,44 @@ export function compose(table: LookupTable, s1: Substitutions, s2: Substitutions | |||
| * given type | |||
| */ | |||
| export function applySubstitution(table: LookupTable, subs: Substitutions, t: QuintType): QuintType { | |||
| let result = t | |||
There was a problem hiding this comment.
Swapping out the mutable assignment for returning computed data.
1 task
added 5 commits
August 7, 2023 14:30
See the accompanying addition to the readme for the motivation and rationale.
Also adds a type for the builtin operator opcodes.
Apparently one of the hygiene fixes also fixed the tests for union types (which will be trashing soon) :D
thpani
force-pushed
the
static-exhaustiveness-checks-on-visitor-switches
branch
from
bab46d9
to
db9fbbb
Compare
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.
While working on the second part of #1082 I realized that there are a lot of places
where we had created type checking blind spots due to our use of mutation in
control flow via switches that really require exhaustive analysis of data types
they are operating on. This refactoring pass fixes all the places I could find
readily. This should make it a bit easier to finish #1082 correctly and should
make our code base a bit more maintainable in general.
Please see the addition to our
CONTRIBUTING.mdin the first commit for adetailed explanation and rationale.
Also closes #196, tho we will probably need followup to ensure the type is being
used everywhere it should be.
Reviewing
Please review ignoring whitespace. It's a considerably smaller diff that git is reckoning, and the bloat is just from whitespace changes required by restructuring some conditionals.
CHANGELOG.mdfor any new functionalityREADME.mdupdated for any listed functionality