Remove MultiAnd's Functor instance (#2139)

* Remove Functor instance from MultiAnd

* Remove MultiAnd.extractPatterns

* MultiAnd: define Semigroup and Monoid instances

Co-authored-by: Thomas Tuegel <[email protected]>

Author: ana-pantilie

kore/src/Kore/Exec.hs

@@ -80,9 +80,6 @@ import Kore.IndexedModule.Resolvers
     ( resolveInternalSymbol
     )
 import qualified Kore.Internal.Condition as Condition
-import qualified Kore.Internal.MultiAnd as MultiAnd
-    ( extractPatterns
-    )
 import Kore.Internal.Pattern
     ( Pattern
     )
@@ -712,7 +709,7 @@ initializeProver definitionModule specModule maybeTrustedModule = do
         simplifyToList :: SomeClaim -> simplifier [SomeClaim]
         simplifyToList rule = do
             simplified <- simplifyRuleLhs rule
-            let result = MultiAnd.extractPatterns simplified
+            let result = Foldable.toList simplified
             when (null result) $ warnTrivialClaimRemoved rule
             return result
 

kore/src/Kore/Internal/MultiAnd.hs

@@ -14,25 +14,28 @@ Portability : portable
 module Kore.Internal.MultiAnd
     ( MultiAnd
     , top
-    , extractPatterns
     , make
     , toPredicate
     , fromPredicate
     , fromTermLike
     , singleton
     , toPattern
     , map
+    , traverse
     ) where
 
 import Prelude.Kore hiding
     ( map
+    , traverse
     )
 
 import Control.DeepSeq
     ( NFData
     )
+import qualified Data.Foldable as Foldable
 import qualified Data.Functor.Foldable as Recursive
 import qualified Data.Set as Set
+import qualified Data.Traversable as Traversable
 import qualified Generics.SOP as SOP
 import qualified GHC.Exts as GHC
 import qualified GHC.Generics as GHC
@@ -72,9 +75,7 @@ A non-empty 'MultiAnd' would also have a nice symmetry between 'Top' and
 -}
 newtype MultiAnd child = MultiAnd { getMultiAnd :: [child] }
     deriving (Eq, Ord, Show)
-    deriving (Semigroup, Monoid)
-    deriving (Functor, Applicative, Monad, Alternative)
-    deriving (Foldable, Traversable)
+    deriving (Foldable)
     deriving (GHC.Generic, GHC.IsList)
 
 instance SOP.Generic (MultiAnd child)
@@ -95,6 +96,14 @@ instance Debug child => Debug (MultiAnd child)
 
 instance (Debug child, Diff child) => Diff (MultiAnd child)
 
+instance (Ord child, TopBottom child) => Semigroup (MultiAnd child) where
+    (MultiAnd []) <> b = b
+    a <> (MultiAnd []) = a
+    (MultiAnd a) <> (MultiAnd b) = make (a <> b)
+
+instance (Ord child, TopBottom child) => Monoid (MultiAnd child) where
+    mempty = make []
+
 instance
     InternalVariable variable
     => From (MultiAnd (Predicate variable)) (Predicate variable)
@@ -148,12 +157,6 @@ make patts = filterAnd (MultiAnd patts)
 singleton :: (Ord term, TopBottom term) => term -> MultiAnd term
 singleton term = make [term]
 
-{-| Returns the patterns inside an @\and@.
--}
-extractPatterns :: MultiAnd term -> [term]
-extractPatterns = getMultiAnd
-
-
 {- | Simplify the conjunction.
 
 The arguments are simplified by filtering on @\\top@ and @\\bottom@. The
@@ -245,4 +248,15 @@ map
     => (child1 -> child2)
     -> MultiAnd child1
     -> MultiAnd child2
-map f = make . fmap f . extractPatterns
+map f = make . fmap f . Foldable.toList
+{-# INLINE map #-}
+
+traverse
+    :: Ord child2
+    => TopBottom child2
+    => Applicative f
+    => (child1 -> f child2)
+    -> MultiAnd child1
+    -> f (MultiAnd child2)
+traverse f = fmap make . Traversable.traverse f . Foldable.toList
+{-# INLINE traverse #-}

kore/src/Kore/Internal/MultiOr.hs

@@ -194,7 +194,7 @@ distributeAnd =
     foldr (crossProductGeneric and') (singleton MultiAnd.top)
   where
     and' term ma =
-        term : MultiAnd.extractPatterns ma & MultiAnd.make
+        MultiAnd.singleton term <> ma
 
 distributeApplication
     :: Ord head

kore/src/Kore/Step/Axiom/Matcher.hs

@@ -197,7 +197,7 @@ matchIncremental termLike1 termLike2 =
         MatcherState
             { queued = Set.singleton (Constraint (Pair termLike1 termLike2))
             , deferred = empty
-            , predicate = empty
+            , predicate = mempty
             , substitution = mempty
             , bound = mempty
             , targets = free1
@@ -521,7 +521,7 @@ substitute eVariable termLike = do
         -- Apply the substitution to the accumulated matching solution.
         >>= (field @"substitution" . traverse) substitute1
         >>= Monad.State.put
-    field @"predicate" . Lens.mapped %= Predicate.substitute subst
+    field @"predicate" %= MultiAnd.map (Predicate.substitute subst)
 
     return ()
   where
@@ -581,7 +581,7 @@ setSubstitute sVariable termLike = do
 
     -- Apply the substitution to the accumulated matching solution.
     field @"substitution" . Lens.mapped %= substitute1
-    field @"predicate" . Lens.mapped %= Predicate.substitute subst
+    field @"predicate" %= MultiAnd.map (Predicate.substitute subst)
 
     return ()
   where

kore/src/Kore/Step/Remainder.hs

@@ -119,7 +119,7 @@ unificationConditions
     -- ^ Unification solution
     -> MultiAnd (Predicate RewritingVariableName)
 unificationConditions Conditional { predicate, substitution } =
-    pure predicate <|> substitutionConditions substitution'
+    MultiAnd.singleton predicate <> substitutionConditions substitution'
   where
     substitution' = Substitution.filter isSomeConfigVariable substitution
 

kore/src/Kore/Step/Rule/Simplify.hs

@@ -22,8 +22,6 @@ import Kore.Internal.MultiAnd
     ( MultiAnd
     )
 import qualified Kore.Internal.MultiAnd as MultiAnd
-    ( make
-    )
 import qualified Kore.Internal.OrPattern as OrPattern
 import Kore.Internal.Pattern
     ( Pattern
@@ -144,21 +142,27 @@ instance SimplifyRuleLHS ClaimPattern
 
 instance SimplifyRuleLHS (RewriteRule VariableName) where
     simplifyRuleLhs =
-        fmap (fmap RewriteRule) . simplifyRuleLhs . getRewriteRule
+        fmap (MultiAnd.map RewriteRule)
+        . simplifyRuleLhs
+        . getRewriteRule
 
 instance SimplifyRuleLHS OnePathClaim where
     simplifyRuleLhs =
-        fmap (fmap OnePathClaim) . simplifyClaimRule . getOnePathClaim
+        fmap (MultiAnd.map OnePathClaim)
+        . simplifyClaimRule
+        . getOnePathClaim
 
 instance SimplifyRuleLHS AllPathClaim where
     simplifyRuleLhs =
-        fmap (fmap AllPathClaim) . simplifyClaimRule . getAllPathClaim
+        fmap (MultiAnd.map AllPathClaim)
+        . simplifyClaimRule
+        . getAllPathClaim
 
 instance SimplifyRuleLHS SomeClaim where
     simplifyRuleLhs (OnePath rule) =
-        (fmap . fmap) OnePath $ simplifyRuleLhs rule
+        (fmap . MultiAnd.map) OnePath $ simplifyRuleLhs rule
     simplifyRuleLhs (AllPath rule) =
-        (fmap . fmap) AllPath $ simplifyRuleLhs rule
+        (fmap . MultiAnd.map) AllPath $ simplifyRuleLhs rule
 
 simplifyClaimRule
     :: forall simplifier

kore/src/Kore/Step/RulePattern.hs

@@ -551,6 +551,10 @@ instance From (RewriteRule variable) Attribute.PriorityAttributes where
 instance From (RewriteRule variable) Attribute.HeatCool where
     from = from @(RulePattern _) . getRewriteRule
 
+instance TopBottom (RewriteRule variable) where
+    isTop _ = False
+    isBottom _ = False
+
 {-  | Implication-based pattern.
 -}
 newtype ImplicationRule variable =

kore/src/Kore/Step/Simplification/And.hs

@@ -143,7 +143,7 @@ simplify
     -> simplifier (OrPattern variable)
 simplify notSimplifier sideCondition orPatterns =
     OrPattern.observeAllT $ do
-        patterns <- traverse scatter orPatterns
+        patterns <- MultiAnd.traverse scatter orPatterns
         makeEvaluate notSimplifier sideCondition patterns
 
 {- | 'makeEvaluate' simplifies a 'MultiAnd' of 'Pattern's.
@@ -179,7 +179,11 @@ makeEvaluateNonBool notSimplifier sideCondition patterns = do
             let (term1, condition1) = Pattern.splitTerm pattern1
             unified <- termAnd notSimplifier term1 term2
             pure (Pattern.andCondition unified condition1)
-    unified <- Foldable.foldlM unify Pattern.top (term <$> patterns)
+    unified <-
+        Foldable.foldlM
+            unify
+            Pattern.top
+            (term <$> Foldable.toList patterns)
     let substitutions =
             Pattern.substitution unified
             <> foldMap Pattern.substitution patterns

kore/src/Kore/Step/Simplification/Not.hs

@@ -111,7 +111,8 @@ simplifyEvaluated
 simplifyEvaluated sideCondition simplified =
     OrPattern.observeAllT $ do
         let not' = Not { notChild = simplified, notSort = () }
-        andPattern <- scatterAnd (makeEvaluateNot <$> distributeNot not')
+        andPattern <-
+            scatterAnd (MultiAnd.map makeEvaluateNot (distributeNot not'))
         mkMultiAndPattern sideCondition andPattern
 
 simplifyEvaluatedPredicate
@@ -122,7 +123,11 @@ simplifyEvaluatedPredicate notChild =
     OrCondition.observeAllT $ do
         let not' = Not { notChild = notChild, notSort = () }
         andPredicate <-
-            scatterAnd (makeEvaluateNotPredicate <$> distributeNot not')
+            scatterAnd
+                ( MultiAnd.map
+                    makeEvaluateNotPredicate
+                    (distributeNot not')
+                )
         mkMultiAndPredicate andPredicate
 
 {-|'makeEvaluate' simplifies a 'Not' pattern given its 'Pattern'

kore/src/Kore/Step/Simplification/TermLike.hs

@@ -340,7 +340,9 @@ simplify sideCondition = \termLike ->
             AndF andF -> do
                 let conjuncts = foldMap MultiAnd.fromTermLike andF
                 And.simplify Not.notSimplifier sideCondition
-                    =<< simplifyChildren conjuncts
+                    =<< MultiAnd.traverse
+                        (simplifyTermLike sideCondition)
+                        conjuncts
             ApplySymbolF applySymbolF ->
                 Application.simplify sideCondition
                     =<< simplifyChildren applySymbolF