Linear \and simplification (#2107)

* Export Kore.Internal.Pattern.syncSort

* simplifyConjunctionByAssumption: Use clearer terminology

Author: ttuegel

kore/src/Kore/Internal/MultiAnd.hs

@@ -16,6 +16,8 @@ module Kore.Internal.MultiAnd
     , extractPatterns
     , make
     , toPredicate
+    , fromPredicate
+    , fromTermLike
     , singleton
     , toPattern
     , map
@@ -28,6 +30,7 @@ import Prelude.Kore hiding
 import Control.DeepSeq
     ( NFData
     )
+import qualified Data.Functor.Foldable as Recursive
 import qualified Data.Set as Set
 import qualified Generics.SOP as SOP
 import qualified GHC.Exts as GHC
@@ -40,11 +43,14 @@ import Kore.Internal.Pattern
 import qualified Kore.Internal.Pattern as Pattern
 import Kore.Internal.Predicate
     ( Predicate
+    , getMultiAndPredicate
     , makeAndPredicate
     , makeTruePredicate_
     )
 import Kore.Internal.TermLike
-    ( mkAnd
+    ( TermLike
+    , TermLikeF (..)
+    , mkAnd
     )
 import Kore.Internal.Variable
 import Kore.TopBottom
@@ -88,6 +94,27 @@ instance Debug child => Debug (MultiAnd child)
 
 instance (Debug child, Diff child) => Diff (MultiAnd child)
 
+instance
+    InternalVariable variable
+    => From (MultiAnd (Predicate variable)) (Predicate variable)
+  where
+    from = toPredicate
+    {-# INLINE from #-}
+
+instance
+    InternalVariable variable
+    => From (Predicate variable) (MultiAnd (Predicate variable))
+  where
+    from = fromPredicate
+    {-# INLINE from #-}
+
+instance
+    InternalVariable variable
+    => From (TermLike variable) (MultiAnd (TermLike variable))
+  where
+    from = fromTermLike
+    {-# INLINE from #-}
+
 {-| 'AndBool' is an some sort of Bool data type used when evaluating things
 inside a 'MultiAnd'.
 -}
@@ -184,6 +211,21 @@ toPredicate (MultiAnd predicates) =
         [] -> makeTruePredicate_
         _  -> foldr1 makeAndPredicate predicates
 
+fromPredicate
+    :: InternalVariable variable
+    => Predicate variable
+    -> MultiAnd (Predicate variable)
+fromPredicate = make . getMultiAndPredicate
+
+fromTermLike
+    :: InternalVariable variable
+    => TermLike variable
+    -> MultiAnd (TermLike variable)
+fromTermLike termLike =
+    case Recursive.project termLike of
+        _ :< AndF andF -> foldMap fromTermLike andF
+        _              -> make [termLike]
+
 toPattern
     :: InternalVariable variable
     => MultiAnd (Pattern variable)

kore/src/Kore/Internal/Pattern.hs

@@ -7,6 +7,7 @@ Representation of program configurations as conditional patterns.
 module Kore.Internal.Pattern
     ( Pattern
     , coerceSort
+    , syncSort
     , patternSort
     , fromCondition
     , fromCondition_