Replace ListT and BranchT with LogicT (#1806)

* Replace ListT and BranchT with LogicT

* Logic: Linting

* termEqualsAnd: Omit lowerLogicT

* TermLikeSimplifier: Use any MonadLogic

* simplifyConditionalTerm: Generalize from LogicT

* Logic: Add missing module header

* Keep names observeAll and observeAllT consistent

Co-authored-by: rv-jenkins <[email protected]>

Author: ttuegel

kore/package.yaml

@@ -67,6 +67,7 @@ dependencies:
   - haskeline >=0.7
   - integer-gmp >=1.0
   - lens >=4.17
+  - logict >=0.7
   - megaparsec >= 7.0.4
   - memory >=0.14
   - mmorph >=1.1

kore/src/Branch.hs

@@ -58,7 +58,6 @@ import Data.Reflection
     )
 import qualified Data.Reflection as Reflection
 
-import Branch
 import qualified Kore.Attribute.Pattern.Simplified as Attribute
     ( Simplified
     )
@@ -119,6 +118,7 @@ import Kore.Unparser
     , unparseToString
     )
 import qualified Kore.Unparser as Unparser
+import Logic
 import Pretty
     ( Doc
     )
@@ -978,7 +978,7 @@ unifyEqualsNormalizedAc
 
     simplify :: TermLike variable -> unifier (Pattern variable)
     simplify term =
-        alternate $ simplifyConditionalTerm SideCondition.topTODO term
+        lowerLogicT $ simplifyConditionalTerm SideCondition.topTODO term
 
     simplifyPair
         :: (TermLike variable, Domain.Value normalized (TermLike variable))
@@ -1017,7 +1017,7 @@ unifyEqualsNormalizedAc
       where
         simplifyTermLike :: TermLike variable -> unifier (Pattern variable)
         simplifyTermLike term =
-            alternate $ simplifyConditionalTerm SideCondition.topTODO term
+            lowerLogicT $ simplifyConditionalTerm SideCondition.topTODO term
 
 buildResultFromUnifiers
     :: forall normalized unifier variable

kore/src/Kore/Builtin/AssociativeCommutative.hs

@@ -46,7 +46,6 @@ import Data.Text
     ( Text
     )
 
-import qualified Branch
 import Kore.Attribute.Hook
     ( Hook (..)
     )
@@ -78,6 +77,7 @@ import Kore.Unification.Unify as Unify
 import Kore.Unification.Unify
     ( MonadUnify
     )
+import qualified Logic
 
 verifiers :: Builtin.Verifiers
 verifiers =
@@ -302,13 +302,11 @@ unifyIfThenElse unifyChildren a b =
             let branchCondition = takeCondition True condition
             Pattern.andCondition solution branchCondition
                 & simplifyCondition SideCondition.top
-                & Branch.gather
-                & (>>= Unify.scatter)
+                & Logic.lowerLogicT
         takeBranch2 IfThenElse { condition, branch2 } = do
             solution <- unifyChildren branch2 termLike2
             let branchCondition = takeCondition False condition
             Pattern.andCondition solution branchCondition
                 & simplifyCondition SideCondition.top
-                & Branch.gather
-                & (>>= Unify.scatter)
+                & Logic.lowerLogicT
     worker _ _ = empty

kore/src/Kore/Builtin/KEqual.hs

@@ -292,7 +292,7 @@ checkRequires sideCondition predicate requires =
     -- Collect the simplified results. If they are \bottom, then \and(predicate,
     -- requires) is valid; otherwise, the required pre-conditions are not met
     -- and the rule will not be applied.
-    & (OrCondition.gather >=> assertBottom)
+    & (OrCondition.observeAllT >=> assertBottom)
   where
     simplifyCondition = Simplifier.simplifyCondition sideCondition'
 

kore/src/Kore/Equation/Application.hs

@@ -21,6 +21,7 @@ module Kore.Internal.MultiOr
     , flattenGeneric
     , fullCrossProduct
     , gather
+    , observeAllT
     , make
     , merge
     , mergeAll
@@ -44,14 +45,15 @@ import GHC.Exts
     )
 import qualified GHC.Generics as GHC
 
-import Branch
-    ( BranchT
-    )
-import qualified Branch as BranchT
 import Kore.Debug
 import Kore.TopBottom
     ( TopBottom (..)
     )
+import Logic
+    ( LogicT
+    , MonadLogic
+    )
+import qualified Logic
 
 {-| 'MultiOr' is a Matching logic or of its children
 
@@ -348,7 +350,8 @@ crossProductGeneric
 crossProductGeneric joiner (MultiOr first) (MultiOr second) =
     MultiOr $ joiner <$> first <*> second
 
-gather
-    :: (Ord a, TopBottom a, Monad m)
-    => BranchT m a -> m (MultiOr a)
-gather branched = make <$> BranchT.gather branched
+gather :: (Ord a, TopBottom a, MonadLogic m) => m a -> m (MultiOr a)
+gather act = make <$> Logic.gather act
+
+observeAllT :: (Ord a, TopBottom a, Monad m) => LogicT m a -> m (MultiOr a)
+observeAllT act = make <$> Logic.observeAllT act

kore/src/Kore/Internal/MultiOr.hs

@@ -10,7 +10,8 @@ module Kore.Internal.OrCondition
     , fromConditions
     , fromCondition
     , fromPredicate
-    , gather
+    , MultiOr.gather
+    , MultiOr.observeAllT
     , bottom
     , top
     , isFalse
@@ -22,9 +23,6 @@ import Prelude.Kore
 
 import qualified Data.Foldable as Foldable
 
-import Branch
-    ( BranchT
-    )
 import Kore.Internal.Condition
     ( Condition
     )
@@ -47,7 +45,6 @@ import Kore.TopBottom
     ( TopBottom (..)
     )
 
-
 {-| The disjunction of 'Condition'.
 -}
 type OrCondition variable = MultiOr (Condition variable)
@@ -113,8 +110,3 @@ toPredicate
     => MultiOr (Predicate variable) -> Predicate variable
 toPredicate multiOr =
     Predicate.makeMultipleOrPredicate (MultiOr.extractPatterns multiOr)
-
-gather
-    :: (InternalVariable variable, Monad m)
-    => BranchT m (Condition variable) -> m (OrCondition variable)
-gather = MultiOr.gather

kore/src/Kore/Internal/OrCondition.hs

@@ -12,7 +12,6 @@ module Kore.Internal.OrPattern
     , toPatterns
     , fromPattern
     , fromTermLike
-    , gather
     , bottom
     , isFalse
     , isPredicate
@@ -23,15 +22,14 @@ module Kore.Internal.OrPattern
     , targetBinder
     , MultiOr.flatten
     , MultiOr.filterOr
+    , MultiOr.gather
+    , MultiOr.observeAllT
     ) where
 
 import Prelude.Kore
 
 import qualified Data.Foldable as Foldable
 
-import Branch
-    ( BranchT
-    )
 import Kore.Internal.Condition
     ( Condition
     )
@@ -200,11 +198,6 @@ coerceSort sort =
     . map (Pattern.coerceSort sort)
     . toPatterns
 
-gather
-    :: (InternalVariable variable, Monad m)
-    => BranchT m (Pattern variable) -> m (OrPattern variable)
-gather = MultiOr.gather
-
 targetBinder
     :: forall variable
     .  InternalVariable variable

kore/src/Kore/Internal/OrPattern.hs

@@ -57,10 +57,10 @@ import System.Clock
     )
 
 import Control.Monad.Counter
-import ListT
-    ( ListT (..)
-    , mapListT
+import Logic
+    ( LogicT
     )
+import qualified Logic
 
 {- | Monad that can also handle profiling events.
 -}
@@ -274,8 +274,8 @@ instance MonadProfiler m => MonadProfiler (ExceptT e m)
 
 instance MonadProfiler m => MonadProfiler (IdentityT m)
 
-instance MonadProfiler m => MonadProfiler (ListT m) where
-    profile a = mapListT (profile a)
+instance MonadProfiler m => MonadProfiler (LogicT m) where
+    profile a = Logic.mapLogicT (profile a)
     {-# INLINE profile #-}
 
 instance MonadProfiler m => MonadProfiler (MaybeT m)