Inefficient Equation renaming #2438
Merged
Conversation
This file contains hidden or 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
ttuegel
suggested changes
Mar 4, 2021
Comment on lines
159
to
163
| attemptEquation | ||
| sideCondition | ||
| (not . freeEquationVariableName >>= assert -> termLike) | ||
| equation | ||
| = |
There was a problem hiding this comment.
Suggested change
| attemptEquation | |
| sideCondition | |
| (not . freeEquationVariableName >>= assert -> termLike) | |
| equation | |
| = | |
| attemptEquation sideCondition termLike equation = | |
| assert (not $ freeEquationVariableName termLike) $ |
Comment on lines
316
to
321
| freeEquationVariableName | ||
| :: HasFreeVariables pat RewritingVariableName => pat -> Bool | ||
| freeEquationVariableName pat = | ||
| any | ||
| isSomeEquationVariableName | ||
| (from @_ @(Set.Set _) . freeVariables @_ @RewritingVariableName $ pat) |
There was a problem hiding this comment.
I suggest naming this function hasFreeEquationVariables.
Comment on lines
79
to
92
|
|
||
| assertNoFreeEquationVariableName | ||
| :: Condition RewritingVariableName | ||
| -> Condition RewritingVariableName | ||
| assertNoFreeEquationVariableName (Conditional () predicate substitution) = | ||
| let | ||
| predicate' = | ||
| assert (not . freeEquationVariableName $ predicate) predicate | ||
| substitution' = | ||
| mapTerms | ||
| (\t -> assert (not . freeEquationVariableName $ t) t) | ||
| substitution | ||
| in | ||
| Conditional () predicate' substitution' |
There was a problem hiding this comment.
This assertion should appear in Kore.Equation.Application after matching and unification on function arguments.
…m:kframework/kore into initialize-equations-EquationVariableName
…m:kframework/kore into initialize-equations-EquationVariableName
ana-pantilie
reviewed
Mar 5, 2021
Comment on lines
198
to
199
| assert (not . hasFreeEquationVariableName $ equation') | ||
| $ assert (not . hasFreeEquationVariableName $ predicate) |
There was a problem hiding this comment.
Could this be factored out? I think it's a little too verbose and it takes longer to read than necessary.
| @@ -156,6 +157,7 @@ attemptEquation | |||
| -> Equation RewritingVariableName | |||
| -> simplifier (AttemptEquationResult RewritingVariableName) | |||
| attemptEquation sideCondition termLike equation = | |||
| assert (not $ hasFreeEquationVariableName termLike) $ | |||
There was a problem hiding this comment.
Do we ever use hasFreeEquationVariableName on its own (without negating it)? Could we just turn hasFreeEquationVariableName into withoutFreeEquationVariables?
ttuegel
approved these changes
Mar 9, 2021
ana-pantilie
approved these changes
Mar 10, 2021
Closed
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 #2120
This pull request addresses the last two checkboxes, but
Targetwas already removed in #2344.Review checklist
The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.