Remove _PREDICATE sort #2719
Remove _PREDICATE sort #2719
Conversation
Remove the predicate sort in favour of using known sorts at all call sites. This mostly adds sort arguments to various functions that previously implicitly used _PREDICATE sort. In turn this means removing the various underbar methods previously in `Kore.Internal.TermLike`.
|
|
| , Pretty.indent 4 (unparse $ fromPredicate_ <$> termLikeF) | ||
| , Pretty.indent | ||
| 4 | ||
| (unparse $ fromPredicate (mkSortVariable "_") <$> termLikeF) |
There was a problem hiding this comment.
Why not call pretty directly instead of fromPredicate and unparse?
There was a problem hiding this comment.
termLikeF is a TermLikeF variable (Predicate variable). TermLikeF doesn't have a Pretty instance, and the use of its Unparse instance would require Predicate to have an Unparse instance as well.
There was a problem hiding this comment.
Ah, I see. Thanks for explaning!
kore/src/Kore/Internal/Predicate.hs
Outdated
| ) | ||
| where | ||
| term = fromPredicate_ (synthesize predF) | ||
| term = fromPredicate (mkSortVariable "_") (synthesize predF) |
| case predicate of | ||
| PredicateEquals t1 t2 -> | ||
| case retractLocalFunction (TermLike.mkEquals_ t1 t2) of | ||
| case retractLocalFunction (TermLike.mkEquals (TermLike.termLikeSort t1) t1 t2) of |
There was a problem hiding this comment.
I think retractLocalFunction should take a Predicate instead of a TermLike, so we should construct a Predicate \\equals here between the two terms, and send it to retractLocalFunction.
kore/src/Kore/Repl/Interpreter.hs
Outdated
| , provenValue = makeAuxReplOutput "Proven." | ||
| } | ||
| where | ||
| -- Dummy sort used to unparse configurations. |
There was a problem hiding this comment.
I wouldn't call this a "dummy sort", it's just a variable.
| -- Dummy sort used to unparse configurations. | |
| -- Sort variable used to unparse configurations. |
kore/src/Kore/Rewrite/Implication.hs
Outdated
| } = implication' | ||
| rightTerm = | ||
| case OrPattern.tryGetSort right of | ||
| Nothing -> error "to do" |
There was a problem hiding this comment.
This shouldn't be an error, right?
kore/src/Kore/Simplify/AndTerms.hs
Outdated
| lift $ Builtin.Map.unifyEquals childTransformers tools unifyData | ||
| | Just unifyData <- Builtin.Map.matchUnifyNotInKeys first second = | ||
| lift $ Builtin.Map.unifyNotInKeys childTransformers notSimplifier unifyData | ||
| lift $ Builtin.Map.unifyNotInKeys (termLikeSort first) childTransformers notSimplifier unifyData |
There was a problem hiding this comment.
Same question as above.
| AndF andF -> do | ||
| let conjuncts = foldMap MultiAnd.fromTermLike andF | ||
| And.simplify Not.notSimplifier sideCondition | ||
| And.simplify sort Not.notSimplifier sideCondition |
There was a problem hiding this comment.
I think it's a little weird and inconsistent that some of the simplifiers take that sort argument while others don't. Is there any reason for this?
There was a problem hiding this comment.
And.makeEvaluate might receive an empty MultiAnd, so this pr gave it a Sort parameter in order to be able to return a \top. And.simplify calls And.makeEvaluate, but its MultiAnd (OrPattern RewritingVariableName) might not contain any Pattern either. That's why now it has a Sort parameter.
There was a problem hiding this comment.
I understand. Could you add a small comment in each place where the sort argument is needed? For example, here we can say "MultiAnd doesn't preserve the sort so we need to send it as an external argument".
There was a problem hiding this comment.
Could you add ^?
Edit: sorry, the comment isn't visible in the review. Please take a look at my responses to our discussions above.
kore/src/Kore/Simplify/Top.hs
Outdated
| Top Sort child -> | ||
| OrPattern RewritingVariableName | ||
| simplify _ = OrPattern.top | ||
| simplify sort _ = OrPattern.topOf sort |
There was a problem hiding this comment.
Why not just get the sort from the Top Sort child type?
| mkEquals | ||
| kSort |
There was a problem hiding this comment.
I was thinking about this, and I want to be 100% sure I understand this. I'd expect the ==_ (where _ is K, Int etc.) to return a Bool. The reason this doesn't return Bool here but kSort is because \\equals is a predicate and we can give it any result sort. If we did \\and unification instead, the resulting sort would be Bool, right?
There was a problem hiding this comment.
Yes, if I replace mkEquals with mkAnd, the result sort is Bool
There was a problem hiding this comment.
Cool. Could you add some similar tests with mkAnd as well?
kore/test/Test/Kore/Simplify/Or.hs
Outdated
| [ prettyOr or1 or2 | ||
| , "to become:" | ||
| , Unparser.unparse $ OrPattern.toTermLike expected | ||
| , Unparser.unparse $ OrPattern.toTermLike (mkSortVariable "_") expected |
There was a problem hiding this comment.
If we have a sort here, we should use that. I guess we should use a sort variable only if the OrPattern is \\bottom.
| evaluateExpectTopK :: | ||
| (MonadSMT smt, MonadLog smt, MonadProf smt, MonadMask smt) => | ||
| TermLike RewritingVariableName -> | ||
| Hedgehog.PropertyT smt () | ||
| evaluateExpectTopK termLike = do | ||
| actual <- evaluateT termLike | ||
| OrPattern.topOf kSort Hedgehog.=== actual | ||
|
|
There was a problem hiding this comment.
Let us give this function the HasCallStack constraint. This allows the test-suite to print more precise source locations of failed tests.
kore/src/Kore/Simplify/Equals.hs
Outdated
| (first', second') = | ||
| minMaxBy (on compareForEquals (OrPattern.toTermLike sort)) first second | ||
|
|
||
| {- TODO (virgil): Preserve pattern sorts under simplification. |
There was a problem hiding this comment.
I think this change resolves the TODO from the comment, so we should remove it.
kore/src/Kore/Simplify/Equals.hs
Outdated
| secondCeil <- makeEvaluateCeil sideCondition second' | ||
| firstCeilNegation <- Not.simplifyEvaluated sideCondition firstCeil | ||
| secondCeilNegation <- Not.simplifyEvaluated sideCondition secondCeil | ||
| let termSort = termLikeSort firstTerm |
There was a problem hiding this comment.
Is there a difference between termSort and sort from the where-clause? Otherwise, I'd suggest keeping only one definition.
|
|
| case elementListAsInternal tools (termLikeSort first) remainder2Terms of | ||
| case elementListAsInternal | ||
| tools | ||
| (sameSort (termLikeSort first) (termLikeSort first)) |
There was a problem hiding this comment.
Did you mean
| (sameSort (termLikeSort first) (termLikeSort first)) | |
| (sameSort (termLikeSort first) (termLikeSort second)) |
| This function is suitable only for equality simplification. | ||
| -} | ||
| unifyEqTerm :: |
kore/src/Kore/Simplify/AndTerms.hs
Outdated
| lift $ bottomTermEquals SideCondition.topTODO unifyData | ||
| lift $ | ||
| bottomTermEquals | ||
| (sameSort (termLikeSort first) (termLikeSort first)) |
There was a problem hiding this comment.
This is checking first and first again.
kore/src/Kore/Simplify/AndTerms.hs
Outdated
| lift $ Builtin.Map.unifyNotInKeys childTransformers notSimplifier unifyData | ||
| lift $ | ||
| Builtin.Map.unifyNotInKeys | ||
| (sameSort (termLikeSort first) (termLikeSort first)) |
There was a problem hiding this comment.
This is checking first and first again.
| AndF andF -> do | ||
| let conjuncts = foldMap MultiAnd.fromTermLike andF | ||
| And.simplify Not.notSimplifier sideCondition | ||
| And.simplify sort Not.notSimplifier sideCondition |
There was a problem hiding this comment.
Could you add ^?
Edit: sorry, the comment isn't visible in the review. Please take a look at my responses to our discussions above.
|
|
|
Fixes #2152.
Opening a new pull request to avoid spamming the original author with notifications.
Review checklist
The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.