Remove _PREDICATE sort

kore/src/Kore/Exec.hs

@@ -265,9 +265,10 @@ exec
                                 <$> finalConfigs
             exitCode <- getExitCode verifiedModule finalConfigs'
             let finalTerm =
-                    forceSort initialSort $
-                        OrPattern.toTermLike
-                            (MultiOr.map getRewritingPattern finalConfigs')
+                    OrPattern.toTermLike
+                        initialSort
+                        (MultiOr.map getRewritingPattern finalConfigs')
+                        & forceSort initialSort
             return (exitCode, finalTerm)
       where
         dropStrategy = snd

kore/src/Kore/Internal/MultiOr.hs

@@ -42,6 +42,9 @@ import GHC.Exts (
  )
 import qualified GHC.Generics as GHC
 import qualified Generics.SOP as SOP
+import Kore.Attribute.Pattern.FreeVariables (
+    HasFreeVariables (..),
+ )
 import Kore.Debug
 import Kore.Internal.MultiAnd (
     MultiAnd,
@@ -111,6 +114,13 @@ instance (Ord child, TopBottom child) => From [child] (MultiOr child) where
 instance From (MultiOr child) [child] where
     from = getMultiOr
 
+instance
+    (Ord variable, HasFreeVariables child variable) =>
+    HasFreeVariables (MultiOr child) variable
+    where
+    freeVariables = foldMap freeVariables . getMultiOr
+    {-# INLINE freeVariables #-}
+
 bottom :: MultiOr term
 bottom = MultiOr []
 

kore/src/Kore/Internal/OrPattern.hs

@@ -58,7 +58,7 @@ import Kore.Internal.TermLike (
     InternalVariable,
     Sort,
     TermLike,
-    mkBottom_,
+    mkBottom,
     mkOr,
  )
 import Kore.Syntax.Variable
@@ -164,11 +164,12 @@ isTrue = isTop
 toPattern ::
     forall variable.
     InternalVariable variable =>
+    Sort ->
     OrPattern variable ->
     Pattern variable
-toPattern multiOr =
+toPattern sort multiOr =
     case toList multiOr of
-        [] -> Pattern.bottom
+        [] -> Pattern.bottomOf sort
         [patt] -> patt
         patts -> foldr1 mergeWithOr patts
   where
@@ -201,11 +202,12 @@ isPredicate = all Pattern.isPredicate
 -- | Transforms a 'Pattern' into a 'TermLike'.
 toTermLike ::
     InternalVariable variable =>
+    Sort ->
     OrPattern variable ->
     TermLike variable
-toTermLike multiOr =
+toTermLike sort multiOr =
     case toList multiOr of
-        [] -> mkBottom_
+        [] -> mkBottom sort
         [patt] -> Pattern.toTermLike patt
         patts -> foldr1 mkOr (Pattern.toTermLike <$> patts)
 

kore/src/Kore/Internal/Pattern.hs

@@ -13,7 +13,6 @@ module Kore.Internal.Pattern (
     fromCondition_,
     fromTermAndPredicate,
     fromPredicateSorted,
-    bottom,
     bottomOf,
     isBottom,
     isTop,
@@ -81,7 +80,6 @@ import Kore.Internal.TermLike (
     TermLike,
     mkAnd,
     mkBottom,
-    mkBottom_,
     mkTop,
     mkTop_,
     termLikeSort,
@@ -239,17 +237,6 @@ toTermLike Conditional{term, predicate, substitution} =
         predicateTermLike = Predicate.fromPredicate sort predicate'
         sort = termLikeSort pattern'
 
-{- |'bottom' is an expanded pattern that has a bottom condition and that
-should become Bottom when transformed to a ML pattern.
--}
-bottom :: InternalVariable variable => Pattern variable
-bottom =
-    Conditional
-        { term = mkBottom_
-        , predicate = Predicate.makeFalsePredicate
-        , substitution = mempty
-        }
-
 {- | An 'Pattern' where the 'term' is 'Bottom' of the given 'Sort'.
 
 The 'predicate' is set to 'makeFalsePredicate'.

kore/src/Kore/Internal/TermLike.hs

@@ -91,7 +91,6 @@ module Kore.Internal.TermLike (
     mkSignedness,
 
     -- * Predicate constructors
-    mkBottom_,
     mkCeil_,
     mkEquals_,
     mkFloor_,
@@ -975,19 +974,6 @@ mkBottom ::
 mkBottom bottomSort =
     updateCallStack $ synthesize (BottomF Bottom{bottomSort})
 
-{- | Construct a 'Bottom' pattern in 'predicateSort'.
-
-This should not be used outside "Kore.Internal.Predicate"; please use
-'mkBottom' instead.
-
-See also: 'mkBottom'
--}
-mkBottom_ ::
-    HasCallStack =>
-    InternalVariable variable =>
-    TermLike variable
-mkBottom_ = updateCallStack $ mkBottom predicateSort
-
 {- | Construct a 'Ceil' pattern in the given sort.
 
 See also: 'mkCeil_'

kore/src/Kore/Step/ClaimPattern.hs

@@ -121,14 +121,15 @@ instance Pretty ClaimPattern where
             , "existentials:"
             , Pretty.indent 4 (Pretty.list $ unparse <$> existentials)
             , "right:"
-            , Pretty.indent 4 (unparse $ OrPattern.toTermLike right)
+            , Pretty.indent 4 (unparse $ OrPattern.toTermLike sort right)
             ]
       where
         ClaimPattern
             { left
             , right
             , existentials
             } = claimPattern'
+        sort = TermLike.termLikeSort (Pattern.term left)
 
 instance TopBottom ClaimPattern where
     isTop _ = False
@@ -141,13 +142,11 @@ freeVariablesRight ::
     ClaimPattern ->
     FreeVariables RewritingVariableName
 freeVariablesRight claimPattern'@(ClaimPattern _ _ _ _) =
-    freeVariables
-        ( TermLike.mkExistsN
-            existentials
-            (OrPattern.toTermLike right)
-        )
+    freeVariables right
+        & FreeVariables.bindVariables boundVariables
   where
     ClaimPattern{right, existentials} = claimPattern'
+    boundVariables = inject @(SomeVariable _) <$> existentials
 
 freeVariablesLeft ::
     ClaimPattern ->
@@ -214,7 +213,7 @@ claimPatternToTerm modality representation@(ClaimPattern _ _ _ _) =
             & Pattern.toTermLike
             & getRewritingTerm
     rightPattern =
-        TermLike.mkExistsN existentials (OrPattern.toTermLike right)
+        TermLike.mkExistsN existentials (OrPattern.toTermLike sort right)
             & getRewritingTerm
 
 substituteRight ::

kore/src/Kore/Step/Implication.hs

@@ -123,14 +123,15 @@ instance Pretty (Implication modality) where
             , "existentials:"
             , Pretty.indent 4 (Pretty.list $ unparse <$> existentials)
             , "right:"
-            , Pretty.indent 4 (unparse $ OrPattern.toTermLike right)
+            , Pretty.indent 4 (unparse $ OrPattern.toTermLike sort right)
             ]
       where
         Implication
             { left
             , right
             , existentials
             } = implication'
+        sort = TermLike.termLikeSort (Pattern.term left)
 
 instance TopBottom (Implication modality) where
     isTop _ = False
@@ -143,13 +144,11 @@ freeVariablesRight ::
     Implication modality ->
     FreeVariables RewritingVariableName
 freeVariablesRight implication'@(Implication _ _ _ _ _) =
-    freeVariables
-        ( TermLike.mkExistsN
-            existentials
-            (OrPattern.toTermLike right)
-        )
+    freeVariables right
+        & FreeVariables.bindVariables boundVariables
   where
     Implication{right, existentials} = implication'
+    boundVariables = inject @(SomeVariable _) <$> existentials
 
 freeVariablesLeft ::
     Implication modality ->
@@ -217,7 +216,7 @@ implicationToTerm representation@(Implication _ _ _ _ _) =
             & Predicate.fromPredicate sort
             & getRewritingTerm
     rightPattern =
-        TermLike.mkExistsN existentials (OrPattern.toTermLike right)
+        TermLike.mkExistsN existentials (OrPattern.toTermLike sort right)
             & getRewritingTerm
 
 substituteRight ::

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

@@ -161,11 +161,16 @@ simplify ::
     SideCondition RewritingVariableName ->
     Equals Sort (OrPattern RewritingVariableName) ->
     simplifier (OrPattern RewritingVariableName)
-simplify sideCondition Equals{equalsFirst = first, equalsSecond = second} =
+simplify sideCondition equals =
     simplifyEvaluated sideCondition first' second'
   where
-    (first', second') =
-        minMaxBy (on compareForEquals OrPattern.toTermLike) first second
+    Equals
+        { equalsOperandSort
+        , equalsFirst = first
+        , equalsSecond = second
+        } = equals
+    comparison = on compareForEquals (OrPattern.toTermLike equalsOperandSort)
+    (first', second') = minMaxBy comparison first second
 
 {- TODO (virgil): Preserve pattern sorts under simplification.
 

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

@@ -37,14 +37,15 @@ Right now this does not do any actual simplification.
 simplify ::
     Next Sort (OrPattern RewritingVariableName) ->
     OrPattern RewritingVariableName
-simplify Next{nextChild = child} = simplifyEvaluated child
+simplify Next{nextChild = child, nextSort = sort} = simplifyEvaluated sort child
 
 simplifyEvaluated ::
+    Sort ->
     OrPattern RewritingVariableName ->
     OrPattern RewritingVariableName
-simplifyEvaluated simplified =
-    OrPattern.fromTermLike $
-        TermLike.markSimplified $
-            mkNext $
-                Pattern.toTermLike $
-                    OrPattern.toPattern simplified
+simplifyEvaluated sort simplified =
+    OrPattern.toPattern sort simplified
+        & Pattern.toTermLike
+        & mkNext
+        & TermLike.markSimplified
+        & OrPattern.fromTermLike

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

@@ -38,8 +38,9 @@ simplify
     Rewrites
         { rewritesFirst = first
         , rewritesSecond = second
+        , rewritesSort = sort
         } =
-        simplifyEvaluatedRewrites first second
+        simplifyEvaluatedRewrites sort first second
 
 {- TODO (virgil): Preserve pattern sorts under simplification.
 
@@ -55,21 +56,22 @@ will make it even more useful to carry around.
 
 -}
 simplifyEvaluatedRewrites ::
+    Sort ->
     OrPattern RewritingVariableName ->
     OrPattern RewritingVariableName ->
     OrPattern RewritingVariableName
-simplifyEvaluatedRewrites first second =
+simplifyEvaluatedRewrites sort first second =
     makeEvaluateRewrites
-        (OrPattern.toPattern first)
-        (OrPattern.toPattern second)
+        (OrPattern.toPattern sort first)
+        (OrPattern.toPattern sort second)
 
 makeEvaluateRewrites ::
     Pattern RewritingVariableName ->
     Pattern RewritingVariableName ->
     OrPattern RewritingVariableName
 makeEvaluateRewrites first second =
-    OrPattern.fromTermLike $
-        TermLike.markSimplified $
-            mkRewrites
-                (Pattern.toTermLike first)
-                (Pattern.toTermLike second)
+    mkRewrites
+        (Pattern.toTermLike first)
+        (Pattern.toTermLike second)
+        & TermLike.markSimplified
+        & OrPattern.fromTermLike

kore/test/Test/Kore/Step/Simplification/Pattern.hs

@@ -313,8 +313,9 @@ test_Pattern_simplify_equalityterm =
                         )
                     ]
             first = Mock.cf
+            sort = termLikeSort first
             second =
-                OrPattern.toTermLike
+                OrPattern.toTermLike sort
                     . OrPattern.fromPatterns
                     $ [ Conditional
                             { term = Mock.cg