Remove MultiOr's Functor instance (#2134)

* WIP: remove Functor instance from MultiOr

* WIP: remove Functor instance from MultiOr

* WIP: remove Functor instance from MultiOr

* Simplification.Inj: refactor awkward map of MultiOr

* WIP: remove Functor instance from MultiOr

* WIP: remove Functor instance from MultiOr

* Simplification.Builtin: use Logic monad instead of MultiOr as a monad

* WIP: remove Functor instance from MultiOr

* WIP: remove Functor instance of Result

* Remove Functor instance from Result

* MultiOr: traverseLogic

* MultiOr: reimplement fullCrossProduct in terms of MultiAnd and MultiOr

* Use old fullCrossProduct in Application simplification

* MultiOr: split fullCrossProduct into distributeAnd and distributeApplication

* Use MultiOr.traverse

* test_distributeAnd + test_distributeApplication

* WIP Address review comments

* Update kore/src/Kore/Step/Simplification/Implies.hs

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

* Update kore/src/Kore/Step/Simplification/In.hs

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

* Update kore/src/Kore/Syntax/DomainValue.hs

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

* Update kore/src/Kore/Internal/Inj.hs

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

* Address review comments

* Address review comment

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

Author: ana-pantilie

kore/src/Kore/Builtin/EqTerm.hs

@@ -18,6 +18,7 @@ import Control.Error
 import qualified Control.Monad as Monad
 
 import qualified Kore.Builtin.Bool as Bool
+import qualified Kore.Internal.MultiOr as MultiOr
 import qualified Kore.Internal.OrPattern as OrPattern
 import Kore.Internal.Pattern
     ( Pattern
@@ -72,7 +73,7 @@ unifyEqTerm unifyChildren (NotSimplifier notSimplifier) eqTerm termLike2
   | Just value2 <- Bool.matchBool termLike2
   = lift $ do
     solution <- unifyChildren operand1 operand2 & OrPattern.gather
-    let solution' = fmap eraseTerm solution
+    let solution' = MultiOr.map eraseTerm solution
     (if value2 then pure else notSimplifier SideCondition.top) solution'
         >>= Unify.scatter
   | otherwise = empty

kore/src/Kore/Exec.hs

@@ -44,6 +44,7 @@ import Control.Monad.Trans.Except
 import Data.Coerce
     ( coerce
     )
+import qualified Data.Foldable as Foldable
 import qualified Data.List as List
 import qualified Data.Map.Strict as Map
 import Data.Text
@@ -82,7 +83,6 @@ import qualified Kore.Internal.Condition as Condition
 import qualified Kore.Internal.MultiAnd as MultiAnd
     ( extractPatterns
     )
-import qualified Kore.Internal.MultiOr as MultiOr
 import Kore.Internal.Pattern
     ( Pattern
     )
@@ -342,7 +342,7 @@ search breadthLimit verifiedModule strategy termLike searchPattern searchConfig
             $ Pattern.fromTermLike termLike
         let
             initialPattern =
-                case MultiOr.extractPatterns simplifiedPatterns of
+                case Foldable.toList simplifiedPatterns of
                     [] -> Pattern.bottomOf (termLikeSort termLike)
                     (config : _) -> config
             runStrategy' =
@@ -356,7 +356,7 @@ search breadthLimit verifiedModule strategy termLike searchPattern searchConfig
                 (match SideCondition.topTODO (mkRewritingPattern searchPattern))
                 executionGraph
         let
-            solutions = concatMap MultiOr.extractPatterns solutionsLists
+            solutions = concatMap Foldable.toList solutionsLists
             orPredicate =
                 makeMultipleOrPredicate (Condition.toPredicate <$> solutions)
         return

kore/src/Kore/Internal/Inj.hs

@@ -36,6 +36,9 @@ import Kore.Sort
 import Kore.Syntax.Application
     ( Application (..)
     )
+import Kore.TopBottom
+    ( TopBottom (..)
+    )
 import Kore.Unparser
 import qualified Pretty
 
@@ -99,6 +102,10 @@ instance Synthetic (FreeVariables variable) Inj where
     synthetic = injChild
     {-# INLINE synthetic #-}
 
+instance TopBottom a => TopBottom (Inj a) where
+    isTop _ = False
+    isBottom Inj { injChild } = isBottom injChild
+
 toSymbol :: Inj a -> Symbol
 toSymbol inj@(Inj _ _ _ _ _) =
     Symbol

kore/src/Kore/Internal/MultiAnd.hs

@@ -13,6 +13,7 @@ Portability : portable
 
 module Kore.Internal.MultiAnd
     ( MultiAnd
+    , top
     , extractPatterns
     , make
     , toPredicate
@@ -115,6 +116,9 @@ instance
     from = fromTermLike
     {-# INLINE from #-}
 
+top :: MultiAnd term
+top = MultiAnd []
+
 {-| 'AndBool' is an some sort of Bool data type used when evaluating things
 inside a 'MultiAnd'.
 -}

kore/src/Kore/Internal/MultiOr.hs

@@ -13,47 +13,62 @@ Portability : portable
 
 module Kore.Internal.MultiOr
     ( MultiOr (..)
-    , crossProductGeneric
-    , crossProductGenericF
-    , extractPatterns
+    , bottom
     , filterOr
     , flatten
-    , flattenGeneric
-    , fullCrossProduct
+    , distributeAnd
+    , distributeApplication
     , gather
     , observeAllT
+    , observeAll
     , make
     , merge
     , mergeAll
     , singleton
     , map
+    , traverse
     -- * Re-exports
     , Alternative (..)
     ) where
 
 import Prelude.Kore hiding
     ( map
+    , traverse
     )
 
 import Control.DeepSeq
     ( NFData
     )
+import qualified Control.Lens as Lens
+import qualified Data.Foldable as Foldable
+import Data.Generics.Product
+    ( field
+    )
 import Data.List
     ( foldl'
     )
 import qualified Data.Set as Set
+import qualified Data.Traversable as Traversable
 import qualified Generics.SOP as SOP
 import GHC.Exts
     ( IsList
     )
 import qualified GHC.Generics as GHC
 
 import Kore.Debug
+import Kore.Internal.MultiAnd
+    ( MultiAnd
+    )
+import qualified Kore.Internal.MultiAnd as MultiAnd
+import Kore.Syntax.Application
+    ( Application (..)
+    )
 import Kore.TopBottom
     ( TopBottom (..)
     )
 import Logic
-    ( LogicT
+    ( Logic
+    , LogicT
     , MonadLogic
     )
 import qualified Logic
@@ -73,17 +88,12 @@ patterns.
 -}
 newtype MultiOr child = MultiOr { getMultiOr :: [child] }
     deriving
-        ( Alternative
-        , Applicative
-        , Eq
+        ( Eq
         , Foldable
-        , Functor
         , GHC.Generic
         , IsList
-        , Monad
         , Ord
         , Show
-        , Traversable
         )
 
 instance SOP.Generic (MultiOr child)
@@ -119,6 +129,9 @@ instance (Ord child, TopBottom child) => From [child] (MultiOr child) where
 instance From (MultiOr child) [child] where
     from = getMultiOr
 
+bottom :: MultiOr term
+bottom = MultiOr []
+
 {-| 'OrBool' is an some sort of Bool data type used when evaluating things
 inside a 'MultiOr'.
 -}
@@ -172,54 +185,37 @@ singleton term
   | isBottom term = MultiOr []
   | otherwise     = MultiOr [term]
 
-{-| 'extractPatterns' instantiates 'getMultiOr' at 'Pattern'.
-
-It returns the patterns inside an @\or@.
--}
-extractPatterns
-    :: MultiOr term
-    -> [term]
-extractPatterns = getMultiOr
-
-{-| 'fullCrossProduct' distributes all the elements in a list of or, making
-all possible tuples. Each of these tuples will be an element of the resulting
-or. This is useful when, say, distributing 'And' or 'Application' patterns
-over 'Or'.
-
-As an example,
-
-@
-fullCrossProduct
-    [ make [a1, a2]
-    , make [b1, b2]
-    , make [c1, c2]
-    ]
-@
-
-will produce something equivalent to
-
-@
-makeGeneric
-    [ [a1, b1, c1]
-    , [a1, b1, c2]
-    , [a1, b2, c1]
-    , [a1, b2, c2]
-    , [a2, b1, c1]
-    , [a2, b1, c2]
-    , [a2, b2, c1]
-    , [a2, b2, c2]
-    ]
-@
-
--}
-fullCrossProduct
-    :: [MultiOr term]
-    -> MultiOr [term]
-fullCrossProduct [] = MultiOr [[]]
-fullCrossProduct ors =
-    foldr (crossProductGeneric (:)) lastOrsWithLists (init ors)
+distributeAnd
+    :: Ord term
+    => TopBottom term
+    => MultiAnd (MultiOr term)
+    -> MultiOr (MultiAnd term)
+distributeAnd =
+    foldr (crossProductGeneric and') (singleton MultiAnd.top)
   where
-    lastOrsWithLists = fmap (: []) (last ors)
+    and' term ma =
+        term : MultiAnd.extractPatterns ma & MultiAnd.make
+
+distributeApplication
+    :: Ord head
+    => Ord term
+    => TopBottom term
+    => Application head (MultiOr term)
+    -> MultiOr (Application head term)
+distributeApplication
+    Application
+        { applicationSymbolOrAlias
+        , applicationChildren
+        }
+  =
+    foldr
+        (crossProductGeneric applyTo)
+        (singleton application)
+        applicationChildren
+  where
+      applyTo term = Lens.over (field @"applicationChildren") (term :)
+      application =
+          Application { applicationSymbolOrAlias, applicationChildren = [] }
 
 {-| 'flatten' transforms a MultiOr (MultiOr term)
 into a (MultiOr term) by or-ing all the inner elements.
@@ -308,18 +304,6 @@ flattenGeneric
 flattenGeneric (MultiOr []) = MultiOr []
 flattenGeneric (MultiOr ors) = foldr1 mergeGeneric ors
 
-{-| The same as 'crossProductGeneric' except that it works under an
-applicative thing.
--}
-crossProductGenericF
-    :: Applicative f
-    => (child1 -> child2 -> f child3)
-    -> MultiOr child1
-    -> MultiOr child2
-    -> f (MultiOr child3)
-crossProductGenericF joiner (MultiOr first) (MultiOr second) =
-    MultiOr <$> sequenceA (joiner <$> first <*> second)
-
 {-| 'crossProductGeneric' makes all pairs between the elements of two ors,
 then applies the given function to the result.
 
@@ -346,12 +330,14 @@ makeGeneric
 
 -}
 crossProductGeneric
-    :: (child1 -> child2 -> child3)
+    :: Ord child3
+    => TopBottom child3
+    => (child1 -> child2 -> child3)
     -> MultiOr child1
     -> MultiOr child2
     -> MultiOr child3
 crossProductGeneric joiner (MultiOr first) (MultiOr second) =
-    MultiOr $ joiner <$> first <*> second
+    make $ joiner <$> first <*> second
 
 gather :: (Ord a, TopBottom a, MonadLogic m) => m a -> m (MultiOr a)
 gather act = make <$> Logic.gather act
@@ -361,10 +347,26 @@ observeAllT :: (Ord a, TopBottom a, Monad m) => LogicT m a -> m (MultiOr a)
 observeAllT act = make <$> Logic.observeAllT act
 {-# INLINE observeAllT #-}
 
+observeAll :: (Ord a, TopBottom a) => Logic a -> MultiOr a
+observeAll = make . Logic.observeAll
+{-# INLINE observeAll #-}
+
 map
     :: Ord child2
     => TopBottom child2
     => (child1 -> child2)
     -> MultiOr child1
     -> MultiOr child2
-map f = make . fmap f . extractPatterns
+map f = make . fmap f . Foldable.toList
+{-# INLINE map #-}
+
+-- | Warning: 'traverse' should not be used with 'LogicT'.
+traverse
+    :: Ord child2
+    => TopBottom child2
+    => Applicative f
+    => (child1 -> f child2)
+    -> MultiOr child1
+    -> f (MultiOr child2)
+traverse f = fmap make . Traversable.traverse f . Foldable.toList
+{-# INLINE traverse #-}

kore/src/Kore/Internal/OrCondition.hs

@@ -109,4 +109,4 @@ toPredicate
     :: InternalVariable variable
     => MultiOr (Predicate variable) -> Predicate variable
 toPredicate multiOr =
-    Predicate.makeMultipleOrPredicate (MultiOr.extractPatterns multiOr)
+    Predicate.makeMultipleOrPredicate (Foldable.toList multiOr)

kore/src/Kore/Internal/OrPattern.hs

@@ -26,6 +26,7 @@ module Kore.Internal.OrPattern
     , MultiOr.gather
     , MultiOr.observeAllT
     , MultiOr.map
+    , MultiOr.traverse
     ) where
 
 import Prelude.Kore
@@ -153,7 +154,7 @@ toPattern
     => OrPattern variable
     -> Pattern variable
 toPattern multiOr =
-    case MultiOr.extractPatterns multiOr of
+    case Foldable.toList multiOr of
         [] -> Pattern.bottom
         [patt] -> patt
         patts -> Foldable.foldr1 mergeWithOr patts
@@ -189,7 +190,7 @@ toTermLike
     :: InternalVariable variable
     => OrPattern variable -> TermLike variable
 toTermLike multiOr =
-    case MultiOr.extractPatterns multiOr of
+    case Foldable.toList multiOr of
         [] -> mkBottom_
         [patt] -> Pattern.toTermLike patt
         patts -> Foldable.foldr1 mkOr (Pattern.toTermLike <$> patts)
@@ -213,13 +214,15 @@ targetBinder Binder { binderVariable, binderChild } =
             targetIfEqual
             $ unElementVariableName . variableName $ binderVariable
         newChild =
-            Pattern.mapVariables
-                AdjSomeVariableName
-                { adjSomeVariableNameElement =
-                    ElementVariableName targetBoundVariables
-                , adjSomeVariableNameSet = SetVariableName NonTarget
-                }
-            <$> binderChild
+            MultiOr.map
+                (Pattern.mapVariables
+                    AdjSomeVariableName
+                    { adjSomeVariableNameElement =
+                        ElementVariableName targetBoundVariables
+                    , adjSomeVariableNameSet = SetVariableName NonTarget
+                    }
+                )
+                binderChild
      in Binder
          { binderVariable = newVar
          , binderChild = newChild