diff --git a/kore/src/Kore/Internal/MultiAnd.hs b/kore/src/Kore/Internal/MultiAnd.hs index 3a5786593e..55a757a1ee 100644 --- a/kore/src/Kore/Internal/MultiAnd.hs +++ b/kore/src/Kore/Internal/MultiAnd.hs @@ -38,8 +38,14 @@ import qualified Data.Traversable as Traversable import qualified Generics.SOP as SOP import qualified GHC.Exts as GHC import qualified GHC.Generics as GHC +import Kore.Attribute.Pattern.FreeVariables + ( HasFreeVariables (..) + ) import Debug +import Kore.Internal.Condition + ( Condition + ) import Kore.Internal.Predicate ( Predicate , getMultiAndPredicate @@ -83,6 +89,11 @@ instance TopBottom child => TopBottom (MultiAnd child) where isBottom (MultiAnd [child]) = isBottom child isBottom _ = False +instance (Ord variable, HasFreeVariables a variable) => + HasFreeVariables (MultiAnd a) variable + where + freeVariables = foldMap' freeVariables + instance Debug child => Debug (MultiAnd child) instance (Debug child, Diff child) => Diff (MultiAnd child) @@ -109,6 +120,13 @@ instance from = fromPredicate {-# INLINE from #-} +instance + InternalVariable variable + => From (Condition variable) (MultiAnd (Predicate variable)) + where + from = fromPredicate . from @_ @(Predicate _) + {-# INLINE from #-} + instance InternalVariable variable => From (TermLike variable) (MultiAnd (TermLike variable)) diff --git a/kore/src/Kore/Internal/SideCondition.hs b/kore/src/Kore/Internal/SideCondition.hs index 855f2c613e..074762a304 100644 --- a/kore/src/Kore/Internal/SideCondition.hs +++ b/kore/src/Kore/Internal/SideCondition.hs @@ -17,7 +17,6 @@ module Kore.Internal.SideCondition , top , topTODO , toPredicate - , isNormalized , toRepresentation ) where @@ -37,10 +36,14 @@ import Kore.Internal.Condition ( Condition ) import qualified Kore.Internal.Condition as Condition -import qualified Kore.Internal.Conditional as Conditional +import Kore.Internal.MultiAnd + ( MultiAnd + ) +import qualified Kore.Internal.MultiAnd as MultiAnd import Kore.Internal.Predicate ( Predicate ) +import qualified Kore.Internal.Predicate as Predicate import Kore.Internal.SideCondition.SideCondition as SideCondition import Kore.Internal.Variable ( InternalVariable @@ -65,10 +68,11 @@ other purposes, say, to remove redundant parts of the result predicate. -} newtype SideCondition variable = SideCondition - { assumedTrue :: Condition variable + { assumedTrue :: MultiAnd (Predicate variable) } deriving (Eq, Ord, Show) deriving (GHC.Generic) + deriving newtype (Semigroup, Monoid) deriving anyclass (Hashable, NFData) deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo) deriving anyclass (Debug) @@ -91,52 +95,56 @@ instance TopBottom (SideCondition variable) where where SideCondition {assumedTrue} = sideCondition -instance InternalVariable variable - => HasFreeVariables (SideCondition variable) variable +instance Ord variable => HasFreeVariables (SideCondition variable) variable where - freeVariables sideCondition@(SideCondition _) = - freeVariables assumedTrue - where - SideCondition {assumedTrue} = sideCondition + freeVariables (SideCondition multiAnd) = + freeVariables multiAnd instance InternalVariable variable => Unparse (SideCondition variable) where - unparse sideCondition@(SideCondition _) = - unparse assumedTrue - where - SideCondition {assumedTrue} = sideCondition - - unparse2 sideCondition@(SideCondition _) = - unparse2 assumedTrue - where - SideCondition {assumedTrue} = sideCondition + unparse = unparse . toPredicate + unparse2 = unparse2 . toPredicate -instance From (Condition variable) (SideCondition variable) +instance From (SideCondition variable) (MultiAnd (Predicate variable)) where - from = SideCondition + from condition@(SideCondition _) = assumedTrue condition + {-# INLINE from #-} -instance From (SideCondition variable) (Condition variable) where - from = assumedTrue +instance From (MultiAnd (Predicate variable)) (SideCondition variable) + where + from = SideCondition {-# INLINE from #-} instance InternalVariable variable => From (SideCondition variable) (Predicate variable) where - from = from @(Condition variable) . from @(SideCondition variable) + from = toPredicate {-# INLINE from #-} instance InternalVariable variable => From (Predicate variable) (SideCondition variable) where - from = from @(Condition variable) . from @(Predicate variable) + from = fromPredicate + {-# INLINE from #-} + +instance InternalVariable variable => + From (Condition variable) (SideCondition variable) + where + from = fromCondition + {-# INLINE from #-} + +instance InternalVariable variable => + From (SideCondition variable) (Condition variable) + where + from = Condition.fromPredicate . toPredicate {-# INLINE from #-} -top :: InternalVariable variable => SideCondition variable -top = fromCondition Condition.top +top :: SideCondition variable +top = SideCondition MultiAnd.top -- | A 'top' 'Condition' for refactoring which should eventually be removed. -topTODO :: InternalVariable variable => SideCondition variable +topTODO :: SideCondition variable topTODO = top andCondition @@ -144,44 +152,55 @@ andCondition => SideCondition variable -> Condition variable -> SideCondition variable -andCondition SideCondition { assumedTrue } newCondition = - SideCondition merged - where - merged = assumedTrue `Condition.andCondition` newCondition +andCondition + sideCondition + (from @(Condition _) @(SideCondition _) -> newSideCondition) + = + newSideCondition <> sideCondition -assumeTrueCondition :: Condition variable -> SideCondition variable +assumeTrueCondition + :: InternalVariable variable + => Condition variable + -> SideCondition variable assumeTrueCondition = fromCondition assumeTruePredicate - :: InternalVariable variable => Predicate variable -> SideCondition variable -assumeTruePredicate predicate = - assumeTrueCondition (Condition.fromPredicate predicate) + :: InternalVariable variable + => Predicate variable + -> SideCondition variable +assumeTruePredicate = fromPredicate toPredicate :: InternalVariable variable => SideCondition variable -> Predicate variable toPredicate condition@(SideCondition _) = - Condition.toPredicate assumedTrue + MultiAnd.toPredicate assumedTrue where SideCondition { assumedTrue } = condition +fromPredicate + :: InternalVariable variable + => Predicate variable + -> SideCondition variable +fromPredicate = SideCondition . MultiAnd.fromPredicate + mapVariables :: (InternalVariable variable1, InternalVariable variable2) => AdjSomeVariableName (variable1 -> variable2) -> SideCondition variable1 -> SideCondition variable2 mapVariables adj condition@(SideCondition _) = - fromCondition (Condition.mapVariables adj assumedTrue) + MultiAnd.map (Predicate.mapVariables adj) assumedTrue + & SideCondition where SideCondition { assumedTrue } = condition -fromCondition :: Condition variable -> SideCondition variable -fromCondition = from - -fromPredicate - :: InternalVariable variable => Predicate variable -> SideCondition variable -fromPredicate = fromCondition . from +fromCondition + :: InternalVariable variable + => Condition variable + -> SideCondition variable +fromCondition = fromPredicate . Condition.toPredicate toRepresentation :: InternalVariable variable @@ -190,6 +209,3 @@ toRepresentation toRepresentation = mkRepresentation . mapVariables @_ @VariableName (pure toVariableName) - -isNormalized :: forall variable. Ord variable => SideCondition variable -> Bool -isNormalized = Conditional.isNormalized . from @_ @(Condition variable) diff --git a/kore/test/Test/Kore/Step/Rule/Simplify.hs b/kore/test/Test/Kore/Step/Rule/Simplify.hs index 14744e55e3..567b8d8f41 100644 --- a/kore/test/Test/Kore/Step/Rule/Simplify.hs +++ b/kore/test/Test/Kore/Step/Rule/Simplify.hs @@ -8,9 +8,6 @@ import Prelude.Kore import Test.Tasty -import Control.Applicative - ( ZipList (..) - ) import qualified Control.Lens as Lens import Control.Monad.Morph ( MFunctor (..) @@ -28,11 +25,8 @@ import Data.Generics.Product import Kore.Internal.Condition ( Condition - , Conditional (..) ) import qualified Kore.Internal.Condition as Condition -import qualified Kore.Internal.MultiAnd as MultiAnd -import qualified Kore.Internal.MultiOr as MultiOr import qualified Kore.Internal.OrPattern as OrPattern import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.Predicate @@ -45,7 +39,6 @@ import Kore.Internal.Predicate ) import qualified Kore.Internal.Predicate as Predicate import qualified Kore.Internal.SideCondition as SideCondition -import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.TermLike ( AdjSomeVariableName , InternalVariable @@ -65,9 +58,6 @@ import Kore.Rewriting.RewritingVariable ( RewritingVariableName , getRewritingVariable ) -import Kore.Sort - ( predicateSort - ) import Kore.Step.ClaimPattern ( ClaimPattern (..) , mkClaimPattern @@ -465,13 +455,7 @@ test_simplifyClaimRule = -- Test simplifyClaimRule through the OnePathClaim instance. testCase name $ do actual <- run (simplifyRuleLhs input) & fmap toList - -- Equivalent under associativity of \\and - let checkEquivalence - (fmap getOnePathClaim -> claims1) - (fmap getOnePathClaim -> claims2) - = - and (areEquivalent <$> ZipList claims1 <*> ZipList claims2) - assertEqual "" True (checkEquivalence expect actual) + assertEqual "" expect actual where run = runSimplifierSMT env @@ -517,15 +501,9 @@ instance MonadSimplify m => MonadSimplify (TestSimplifierT m) where (Condition.toPredicate requires) (makeCeilPredicate sort leftTerm) & liftPredicate - & Predicate.coerceSort predicateSort & Condition.fromPredicate & SideCondition.fromCondition - -- Equivalent under associativity of \\and - checkEquivalence cond1 cond2 = - (==) - (cond1 & SideCondition.toPredicate & MultiAnd.fromPredicate) - (cond2 & SideCondition.toPredicate & MultiAnd.fromPredicate) - satisfied = checkEquivalence sideCondition expectSideCondition + satisfied = sideCondition == expectSideCondition return . OrPattern.fromTermLike . (if satisfied then applyReplacements replacements else id) @@ -569,46 +547,3 @@ instance MonadSimplify m => MonadSimplify (TestSimplifierT m) where => AdjSomeVariableName (RewritingVariableName -> variable) liftRewritingVariable = pure (.) <*> pure fromVariableName <*> getRewritingVariable - --- | The terms of the implication are equivalent in respect to --- the associativity, commutativity, and idempotence of \\and. --- --- Warning: this should only be used when the distinction between the --- predicate and substitution of a pattern is not of importance. -areEquivalent - :: ClaimPattern - -> ClaimPattern - -> Bool -areEquivalent - ClaimPattern - { left = left1 - , right = right1 - , existentials = existentials1 - , attributes = attributes1 - } - ClaimPattern - { left = left2 - , right = right2 - , existentials = existentials2 - , attributes = attributes2 - } - = - let leftsAreEquivalent = - toConjunctionOfTerms left1 - == toConjunctionOfTerms left2 - rightsAreEquivalent = - MultiOr.map toConjunctionOfTerms right1 - == MultiOr.map toConjunctionOfTerms right2 - in leftsAreEquivalent - && rightsAreEquivalent - && existentials1 == existentials2 - && attributes1 == attributes2 - where - toConjunctionOfTerms Conditional { term, predicate, substitution } = - MultiAnd.fromTermLike term - <> MultiAnd.fromTermLike (Predicate.unwrapPredicate predicate) - <> MultiAnd.fromTermLike - ( Predicate.unwrapPredicate - . Substitution.toPredicate - $ substitution - ) diff --git a/test/issue-1872/1.test.out.golden b/test/issue-1872/1.test.out.golden index e4eef75f6e..7a579d020e 100644 --- a/test/issue-1872/1.test.out.golden +++ b/test/issue-1872/1.test.out.golden @@ -1,7 +1,7 @@ #Not ( { - 1 - #Equals 'QuesUnds'0 %Int 2 + #Equals + 1 } ) #And @@ -23,7 +23,7 @@ #And { - 1 - #Equals 'QuesUnds'0 %Int 2 + #Equals + 1 } diff --git a/test/issue-2095/test-issue-2095.sh.out.golden b/test/issue-2095/test-issue-2095.sh.out.golden index 9245a70dba..69e5afdeab 100644 --- a/test/issue-2095/test-issue-2095.sh.out.golden +++ b/test/issue-2095/test-issue-2095.sh.out.golden @@ -13175,8 +13175,6 @@ \not{SortGeneratedTopCell{}}( /* Sfc */ \equals{SortInt{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0"), /* Fn Sfc */ Lbl'Hash'DoCompare'LParUndsCommUndsRParUnds'MICHELSON'Unds'Int'Unds'Data'Unds'Data{}( /* Fl Fn D Sfc */ @@ -13220,7 +13218,9 @@ ) ) ) - ) + ), + /* Fl Fn D Sfa Cl */ + /* builtin: */ \dv{SortInt{}}("0") ) ) ) @@ -15113,8 +15113,6 @@ \and{SortGeneratedTopCell{}}( /* Sfc */ \equals{SortInt{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0"), /* Fn Sfc */ Lbl'Hash'DoCompare'LParUndsCommUndsRParUnds'MICHELSON'Unds'Int'Unds'Data'Unds'Data{}( /* Fl Fn D Sfc */ @@ -15158,7 +15156,9 @@ ) ) ) - ) + ), + /* Fl Fn D Sfa Cl */ + /* builtin: */ \dv{SortInt{}}("0") ), /* Sfc */ \equals{SortOptionData{}, SortGeneratedTopCell{}}(