From 7278cb8433fb1cb393d1993833fd370a6d6ec3b6 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 6 May 2021 16:30:57 -0500 Subject: [PATCH 1/4] OrPattern.toTermLike: Use correct sort --- kore/src/Kore/Exec.hs | 7 ++++--- kore/src/Kore/Internal/MultiOr.hs | 10 ++++++++++ kore/src/Kore/Internal/OrPattern.hs | 7 ++++--- kore/src/Kore/Step/ClaimPattern.hs | 13 ++++++------- kore/src/Kore/Step/Implication.hs | 13 ++++++------- kore/src/Kore/Step/Simplification/Equals.hs | 11 ++++++++--- kore/test/Test/Kore/Step/Simplification/Pattern.hs | 3 ++- 7 files changed, 40 insertions(+), 24 deletions(-) diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs index 83202e1ede..48ee8c9d3d 100644 --- a/kore/src/Kore/Exec.hs +++ b/kore/src/Kore/Exec.hs @@ -265,9 +265,10 @@ exec <$> finalConfigs exitCode <- getExitCode verifiedModule finalConfigs' let finalTerm = - forceSort initialSort $ - OrPattern.toTermLike - (MultiOr.map getRewritingPattern finalConfigs') + OrPattern.toTermLike + initialSort + (MultiOr.map getRewritingPattern finalConfigs') + & forceSort initialSort return (exitCode, finalTerm) where dropStrategy = snd diff --git a/kore/src/Kore/Internal/MultiOr.hs b/kore/src/Kore/Internal/MultiOr.hs index 93c90a1322..31e375fbc5 100644 --- a/kore/src/Kore/Internal/MultiOr.hs +++ b/kore/src/Kore/Internal/MultiOr.hs @@ -42,6 +42,9 @@ import GHC.Exts ( ) import qualified GHC.Generics as GHC import qualified Generics.SOP as SOP +import Kore.Attribute.Pattern.FreeVariables ( + HasFreeVariables (..), + ) import Kore.Debug import Kore.Internal.MultiAnd ( MultiAnd, @@ -111,6 +114,13 @@ instance (Ord child, TopBottom child) => From [child] (MultiOr child) where instance From (MultiOr child) [child] where from = getMultiOr +instance + (Ord variable, HasFreeVariables child variable) => + HasFreeVariables (MultiOr child) variable + where + freeVariables = foldMap freeVariables . getMultiOr + {-# INLINE freeVariables #-} + bottom :: MultiOr term bottom = MultiOr [] diff --git a/kore/src/Kore/Internal/OrPattern.hs b/kore/src/Kore/Internal/OrPattern.hs index 429e800cd2..b1ca7a7c2d 100644 --- a/kore/src/Kore/Internal/OrPattern.hs +++ b/kore/src/Kore/Internal/OrPattern.hs @@ -58,7 +58,7 @@ import Kore.Internal.TermLike ( InternalVariable, Sort, TermLike, - mkBottom_, + mkBottom, mkOr, ) import Kore.Syntax.Variable @@ -201,11 +201,12 @@ isPredicate = all Pattern.isPredicate -- | Transforms a 'Pattern' into a 'TermLike'. toTermLike :: InternalVariable variable => + Sort -> OrPattern variable -> TermLike variable -toTermLike multiOr = +toTermLike sort multiOr = case toList multiOr of - [] -> mkBottom_ + [] -> mkBottom sort [patt] -> Pattern.toTermLike patt patts -> foldr1 mkOr (Pattern.toTermLike <$> patts) diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs index 6695cc26b7..726fdf0267 100644 --- a/kore/src/Kore/Step/ClaimPattern.hs +++ b/kore/src/Kore/Step/ClaimPattern.hs @@ -121,7 +121,7 @@ instance Pretty ClaimPattern where , "existentials:" , Pretty.indent 4 (Pretty.list $ unparse <$> existentials) , "right:" - , Pretty.indent 4 (unparse $ OrPattern.toTermLike right) + , Pretty.indent 4 (unparse $ OrPattern.toTermLike sort right) ] where ClaimPattern @@ -129,6 +129,7 @@ instance Pretty ClaimPattern where , right , existentials } = claimPattern' + sort = TermLike.termLikeSort (Pattern.term left) instance TopBottom ClaimPattern where isTop _ = False @@ -141,13 +142,11 @@ freeVariablesRight :: ClaimPattern -> FreeVariables RewritingVariableName freeVariablesRight claimPattern'@(ClaimPattern _ _ _ _) = - freeVariables - ( TermLike.mkExistsN - existentials - (OrPattern.toTermLike right) - ) + freeVariables right + & FreeVariables.bindVariables boundVariables where ClaimPattern{right, existentials} = claimPattern' + boundVariables = inject @(SomeVariable _) <$> existentials freeVariablesLeft :: ClaimPattern -> @@ -214,7 +213,7 @@ claimPatternToTerm modality representation@(ClaimPattern _ _ _ _) = & Pattern.toTermLike & getRewritingTerm rightPattern = - TermLike.mkExistsN existentials (OrPattern.toTermLike right) + TermLike.mkExistsN existentials (OrPattern.toTermLike sort right) & getRewritingTerm substituteRight :: diff --git a/kore/src/Kore/Step/Implication.hs b/kore/src/Kore/Step/Implication.hs index 719e11e821..aa183bba32 100644 --- a/kore/src/Kore/Step/Implication.hs +++ b/kore/src/Kore/Step/Implication.hs @@ -123,7 +123,7 @@ instance Pretty (Implication modality) where , "existentials:" , Pretty.indent 4 (Pretty.list $ unparse <$> existentials) , "right:" - , Pretty.indent 4 (unparse $ OrPattern.toTermLike right) + , Pretty.indent 4 (unparse $ OrPattern.toTermLike sort right) ] where Implication @@ -131,6 +131,7 @@ instance Pretty (Implication modality) where , right , existentials } = implication' + sort = TermLike.termLikeSort (Pattern.term left) instance TopBottom (Implication modality) where isTop _ = False @@ -143,13 +144,11 @@ freeVariablesRight :: Implication modality -> FreeVariables RewritingVariableName freeVariablesRight implication'@(Implication _ _ _ _ _) = - freeVariables - ( TermLike.mkExistsN - existentials - (OrPattern.toTermLike right) - ) + freeVariables right + & FreeVariables.bindVariables boundVariables where Implication{right, existentials} = implication' + boundVariables = inject @(SomeVariable _) <$> existentials freeVariablesLeft :: Implication modality -> @@ -217,7 +216,7 @@ implicationToTerm representation@(Implication _ _ _ _ _) = & Predicate.fromPredicate sort & getRewritingTerm rightPattern = - TermLike.mkExistsN existentials (OrPattern.toTermLike right) + TermLike.mkExistsN existentials (OrPattern.toTermLike sort right) & getRewritingTerm substituteRight :: diff --git a/kore/src/Kore/Step/Simplification/Equals.hs b/kore/src/Kore/Step/Simplification/Equals.hs index 14f0786592..a0fd9acac9 100644 --- a/kore/src/Kore/Step/Simplification/Equals.hs +++ b/kore/src/Kore/Step/Simplification/Equals.hs @@ -161,11 +161,16 @@ simplify :: SideCondition RewritingVariableName -> Equals Sort (OrPattern RewritingVariableName) -> simplifier (OrPattern RewritingVariableName) -simplify sideCondition Equals{equalsFirst = first, equalsSecond = second} = +simplify sideCondition equals = simplifyEvaluated sideCondition first' second' where - (first', second') = - minMaxBy (on compareForEquals OrPattern.toTermLike) first second + Equals + { equalsOperandSort + , equalsFirst = first + , equalsSecond = second + } = equals + comparison = on compareForEquals (OrPattern.toTermLike equalsOperandSort) + (first', second') = minMaxBy comparison first second {- TODO (virgil): Preserve pattern sorts under simplification. diff --git a/kore/test/Test/Kore/Step/Simplification/Pattern.hs b/kore/test/Test/Kore/Step/Simplification/Pattern.hs index 3973e44ce0..e612df6536 100644 --- a/kore/test/Test/Kore/Step/Simplification/Pattern.hs +++ b/kore/test/Test/Kore/Step/Simplification/Pattern.hs @@ -313,8 +313,9 @@ test_Pattern_simplify_equalityterm = ) ] first = Mock.cf + sort = termLikeSort first second = - OrPattern.toTermLike + OrPattern.toTermLike sort . OrPattern.fromPatterns $ [ Conditional { term = Mock.cg From 7bede00abc99c27e74dc4204d6aff35026471fde Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 6 May 2021 20:28:35 -0500 Subject: [PATCH 2/4] [WIP] OrPattern.toPattern: Add Sort argument --- kore/src/Kore/Internal/OrPattern.hs | 5 +++-- kore/src/Kore/Step/Simplification/Next.hs | 15 +++++++------- kore/src/Kore/Step/Simplification/Rewrites.hs | 20 ++++++++++--------- 3 files changed, 22 insertions(+), 18 deletions(-) diff --git a/kore/src/Kore/Internal/OrPattern.hs b/kore/src/Kore/Internal/OrPattern.hs index b1ca7a7c2d..6077a2d899 100644 --- a/kore/src/Kore/Internal/OrPattern.hs +++ b/kore/src/Kore/Internal/OrPattern.hs @@ -164,11 +164,12 @@ isTrue = isTop toPattern :: forall variable. InternalVariable variable => + Sort -> OrPattern variable -> Pattern variable -toPattern multiOr = +toPattern sort multiOr = case toList multiOr of - [] -> Pattern.bottom + [] -> Pattern.bottomOf sort [patt] -> patt patts -> foldr1 mergeWithOr patts where diff --git a/kore/src/Kore/Step/Simplification/Next.hs b/kore/src/Kore/Step/Simplification/Next.hs index aac0422a88..f8a25a8c7b 100644 --- a/kore/src/Kore/Step/Simplification/Next.hs +++ b/kore/src/Kore/Step/Simplification/Next.hs @@ -37,14 +37,15 @@ Right now this does not do any actual simplification. simplify :: Next Sort (OrPattern RewritingVariableName) -> OrPattern RewritingVariableName -simplify Next{nextChild = child} = simplifyEvaluated child +simplify Next{nextChild = child, nextSort = sort} = simplifyEvaluated sort child simplifyEvaluated :: + Sort -> OrPattern RewritingVariableName -> OrPattern RewritingVariableName -simplifyEvaluated simplified = - OrPattern.fromTermLike $ - TermLike.markSimplified $ - mkNext $ - Pattern.toTermLike $ - OrPattern.toPattern simplified +simplifyEvaluated sort simplified = + OrPattern.toPattern sort simplified + & Pattern.toTermLike + & mkNext + & TermLike.markSimplified + & OrPattern.fromTermLike diff --git a/kore/src/Kore/Step/Simplification/Rewrites.hs b/kore/src/Kore/Step/Simplification/Rewrites.hs index 5eec2bc514..6d21620a28 100644 --- a/kore/src/Kore/Step/Simplification/Rewrites.hs +++ b/kore/src/Kore/Step/Simplification/Rewrites.hs @@ -38,8 +38,9 @@ simplify Rewrites { rewritesFirst = first , rewritesSecond = second + , rewritesSort = sort } = - simplifyEvaluatedRewrites first second + simplifyEvaluatedRewrites sort first second {- TODO (virgil): Preserve pattern sorts under simplification. @@ -55,21 +56,22 @@ will make it even more useful to carry around. -} simplifyEvaluatedRewrites :: + Sort -> OrPattern RewritingVariableName -> OrPattern RewritingVariableName -> OrPattern RewritingVariableName -simplifyEvaluatedRewrites first second = +simplifyEvaluatedRewrites sort first second = makeEvaluateRewrites - (OrPattern.toPattern first) - (OrPattern.toPattern second) + (OrPattern.toPattern sort first) + (OrPattern.toPattern sort second) makeEvaluateRewrites :: Pattern RewritingVariableName -> Pattern RewritingVariableName -> OrPattern RewritingVariableName makeEvaluateRewrites first second = - OrPattern.fromTermLike $ - TermLike.markSimplified $ - mkRewrites - (Pattern.toTermLike first) - (Pattern.toTermLike second) + mkRewrites + (Pattern.toTermLike first) + (Pattern.toTermLike second) + & TermLike.markSimplified + & OrPattern.fromTermLike From 6534c5a4640033e7016fa9ddd1cf924cef9104be Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 6 May 2021 20:28:55 -0500 Subject: [PATCH 3/4] [WIP] Remove Pattern.bottom --- kore/src/Kore/Internal/Pattern.hs | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/kore/src/Kore/Internal/Pattern.hs b/kore/src/Kore/Internal/Pattern.hs index cee83d78f1..e00b1eba42 100644 --- a/kore/src/Kore/Internal/Pattern.hs +++ b/kore/src/Kore/Internal/Pattern.hs @@ -13,7 +13,6 @@ module Kore.Internal.Pattern ( fromCondition_, fromTermAndPredicate, fromPredicateSorted, - bottom, bottomOf, isBottom, isTop, @@ -81,7 +80,6 @@ import Kore.Internal.TermLike ( TermLike, mkAnd, mkBottom, - mkBottom_, mkTop, mkTop_, termLikeSort, @@ -239,17 +237,6 @@ toTermLike Conditional{term, predicate, substitution} = predicateTermLike = Predicate.fromPredicate sort predicate' sort = termLikeSort pattern' -{- |'bottom' is an expanded pattern that has a bottom condition and that -should become Bottom when transformed to a ML pattern. --} -bottom :: InternalVariable variable => Pattern variable -bottom = - Conditional - { term = mkBottom_ - , predicate = Predicate.makeFalsePredicate - , substitution = mempty - } - {- | An 'Pattern' where the 'term' is 'Bottom' of the given 'Sort'. The 'predicate' is set to 'makeFalsePredicate'. From 96eae24a8440f3e8d9250b1a836698e4d0e330c9 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 6 May 2021 20:29:06 -0500 Subject: [PATCH 4/4] [WIP] Remove TermLike.mkBottom_ --- kore/src/Kore/Internal/TermLike.hs | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index e9a7ba0f2b..81682b55a8 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -91,7 +91,6 @@ module Kore.Internal.TermLike ( mkSignedness, -- * Predicate constructors - mkBottom_, mkCeil_, mkEquals_, mkFloor_, @@ -975,19 +974,6 @@ mkBottom :: mkBottom bottomSort = updateCallStack $ synthesize (BottomF Bottom{bottomSort}) -{- | Construct a 'Bottom' pattern in 'predicateSort'. - -This should not be used outside "Kore.Internal.Predicate"; please use -'mkBottom' instead. - -See also: 'mkBottom' --} -mkBottom_ :: - HasCallStack => - InternalVariable variable => - TermLike variable -mkBottom_ = updateCallStack $ mkBottom predicateSort - {- | Construct a 'Ceil' pattern in the given sort. See also: 'mkCeil_'