-
Notifications
You must be signed in to change notification settings - Fork 43
Overhaul Predicate simplifier: Equals, v2 #2766
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Conversation
|
|
JKTKops
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Couple of minor comments, but looks good to me.
| _ -> simplifyPredicateTODO sideCondition predicate & MultiOr.observeAllT | ||
| where | ||
| _ :< predicateF = Recursive.project predicate | ||
| ~avoid = freeVariableNames sideCondition |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Aren't where bindings lazy by default? What is this ~ for?
This line wasn't changed, but asking anyway while we're here.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We have Strict on by default, maybe this changes the behavior? I don't know for certain, though.
kore/src/Kore/Simplify/Predicate.hs
Outdated
| simplifier NormalForm | ||
| simplifyEquals sideCondition sort equals = | ||
| Equals.simplify sideCondition equals' | ||
| >>= return . MultiOr.map (from @(Condition _)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why m >>= return . f instead of fmap f m?
|
|
|
Fixes #2570
Completes all cases of
Predicate.simplify.I didn't add any tests for
simplifyEqualsbecause it only callsEquals.simplify, which we will need to modify for #2610.Review checklist
The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.