Remove _PREDICATE sort (#2604)

Remove the predicate sort in favour of using known sorts at all call
sites. This mostly adds sort arguments to various functions that
previously implicitly used _PREDICATE sort. In turn this means removing
the various underbar methods previously in `Kore.Internal.TermLike`.

Author: Boarders

kore/src/Kore/Builtin/Builtin.hs

@@ -84,7 +84,7 @@ import Kore.Internal.Pattern (
  )
 import Kore.Internal.Pattern as Pattern (
     fromTermLike,
-    top,
+    topOf,
     withCondition,
  )
 import Kore.Internal.Predicate (
@@ -101,9 +101,6 @@ import Kore.Internal.TermLike as TermLike
 import Kore.Rewriting.RewritingVariable (
     RewritingVariableName,
  )
-import Kore.Sort (
-    predicateSort,
- )
 import Kore.Step.Simplification.SimplificationType as SimplificationType (
     SimplificationType (..),
  )
@@ -473,19 +470,19 @@ isSymbol builtinName Symbol{symbolAttributes = Attribute.Symbol{hook}} =
 
 {- | Is the given sort hooked to the named builtin?
 
+TO DO (callan): fix documentation here
+
 Returns Nothing if the sort is unknown (i.e. the _PREDICATE sort).
 Returns Just False if the sort is a variable.
 -}
 isSort :: Text -> SmtMetadataTools attr -> Sort -> Maybe Bool
 isSort builtinName tools sort
-    | isPredicateSort = Nothing
     | SortVariableSort _ <- sort = Nothing
     | otherwise =
         let MetadataTools{sortAttributes} = tools
             Attribute.Sort{hook} = sortAttributes sort
          in Just (getHook hook == Just builtinName)
-  where
-    isPredicateSort = sort == predicateSort
+
 
 -- | Run a function evaluator that can terminate early.
 getAttemptedAxiom ::
@@ -510,9 +507,10 @@ unifyEqualsUnsolved SimplificationType.And a b = do
             unified
     predicate <- Monad.Unify.scatter orCondition
     return (unified `Pattern.withCondition` predicate)
-unifyEqualsUnsolved SimplificationType.Equals a b =
+unifyEqualsUnsolved SimplificationType.Equals a b = do
+    let sort = TermLike.termLikeSort a
     return
-        Pattern.top
+        (Pattern.topOf sort)
             { predicate = Predicate.markSimplified $ makeEqualsPredicate a b
             }
 

kore/src/Kore/Builtin/EqTerm.hs

@@ -72,5 +72,6 @@ unifyEqTerm unifyChildren (NotSimplifier notSimplifier) eqTerm termLike2
                 >>= Unify.scatter
     | otherwise = empty
   where
+    sort = TermLike.termLikeSort termLike2
     EqTerm{operand1, operand2} = eqTerm
-    eraseTerm = Pattern.fromCondition_ . Pattern.withoutTerm
+    eraseTerm = Pattern.fromCondition sort . Pattern.withoutTerm

kore/src/Kore/Builtin/Int/Int.hs

@@ -101,7 +101,7 @@ asPartialPattern ::
     Maybe Integer ->
     Pattern variable
 asPartialPattern resultSort =
-    maybe Pattern.bottom (asPattern resultSort)
+    maybe (Pattern.bottomOf resultSort) (asPattern resultSort)
 
 randKey :: IsString s => s
 randKey = "INT.rand"

kore/src/Kore/Builtin/List.hs

@@ -275,7 +275,7 @@ evalGet _ resultSort [_list, _ix] = do
     emptyList <|> bothConcrete
   where
     maybeBottom =
-        maybe Pattern.bottom Pattern.fromTermLike
+        maybe (Pattern.bottomOf resultSort) Pattern.fromTermLike
 evalGet _ _ _ = Builtin.wrongArity getKey
 
 evalUpdate :: Builtin.Function
@@ -560,7 +560,7 @@ unifyEquals
                 "Cannot unify lists of different length."
                 first
                 second
-            return Pattern.bottom
+            return (Pattern.bottomOf sort1)
 
         unifyEqualsFramedRightRight ::
             TermLike.Symbol ->

kore/src/Kore/Builtin/Map.hs

@@ -631,8 +631,10 @@ unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) a b =
             >>= Unify.scatter
             & lift
 
+    sort1 = TermLike.termLikeSort a
+
     eraseTerm =
-        Pattern.fromCondition_ . Pattern.withoutTerm
+        Pattern.fromCondition sort1 . Pattern.withoutTerm
 
     unifyAndNegate t1 t2 =
         do
@@ -646,7 +648,7 @@ unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) a b =
                 (OrPattern.fromPatterns unificationSolutions)
             >>= Unify.scatter
 
-    collectConditions terms = fold terms & Pattern.fromCondition_
+    collectConditions terms = fold terms & Pattern.fromCondition sort1
 
     worker ::
         TermLike RewritingVariableName ->
@@ -663,7 +665,7 @@ unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) a b =
                     mapKeys = symbolicKeys <> concreteKeys
                     opaqueElements = opaque . unwrapAc $ normalizedMap
                 if null mapKeys && null opaqueElements
-                    then return Pattern.top
+                    then return (Pattern.topOf sort1)
                     else do
                         Monad.guard (not (null mapKeys) || (length opaqueElements > 1))
                         -- Concrete keys are constructor-like, therefore they are defined

kore/src/Kore/Builtin/String/String.hs

@@ -90,7 +90,7 @@ asPartialPattern ::
     Maybe Text ->
     Pattern variable
 asPartialPattern resultSort =
-    maybe Pattern.bottom (asPattern resultSort)
+    maybe (Pattern.bottomOf resultSort) (asPattern resultSort)
 
 eqKey :: IsString s => s
 eqKey = "STRING.eq"

kore/src/Kore/Internal/Inj.hs

@@ -85,7 +85,7 @@ instance Unparse a => Unparse (Inj a) where
 
 instance Synthetic Sort Inj where
     synthetic Inj{injFrom, injTo, injChild} =
-        injTo & seq (matchSort injFrom injChild)
+        injTo & seq (sameSort injFrom injChild)
     {-# INLINE synthetic #-}
 
 instance Synthetic (FreeVariables variable) Inj where

kore/src/Kore/Internal/OrPattern.hs

@@ -16,6 +16,7 @@ module Kore.Internal.OrPattern (
     bottom,
     isFalse,
     isPredicate,
+    tryGetSort,
     top,
     isTrue,
     toPattern,
@@ -58,7 +59,7 @@ import Kore.Internal.TermLike (
     InternalVariable,
     Sort,
     TermLike,
-    mkBottom_,
+    mkBottom,
     mkOr,
  )
 import Kore.Syntax.Variable
@@ -151,10 +152,12 @@ isFalse = isBottom
 
 @
 'isTrue' top == True
+
+To do (Callan): should this be renamed `topOf` as elsewhere?
 @
 -}
-top :: InternalVariable variable => OrPattern variable
-top = fromPattern Pattern.top
+top :: InternalVariable variable => Sort -> OrPattern variable
+top sort = fromPattern (Pattern.topOf sort)
 
 -- | 'isTrue' checks if the 'Or' has a single top pattern.
 isTrue :: OrPattern variable -> Bool
@@ -164,11 +167,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
@@ -198,14 +202,23 @@ toPattern multiOr =
 isPredicate :: OrPattern variable -> Bool
 isPredicate = all Pattern.isPredicate
 
+-- | Gets the `Sort` of a non-empty 'OrPattern' and othewise returns `Nothing`.
+tryGetSort :: OrPattern variable -> Maybe Sort
+tryGetSort multiOr =
+  case toList multiOr of
+    [] -> Nothing
+    p : _ -> Just (Pattern.patternSort p)
+
+
 -- | 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

@@ -10,17 +10,14 @@ module Kore.Internal.Pattern (
     syncSort,
     patternSort,
     fromCondition,
-    fromCondition_,
     fromTermAndPredicate,
     fromPredicateSorted,
-    bottom,
     bottomOf,
     isBottom,
     isTop,
     Kore.Internal.Pattern.mapVariables,
     splitTerm,
     toTermLike,
-    top,
     topOf,
     fromTermLike,
     Kore.Internal.Pattern.freeElementVariables,
@@ -81,9 +78,7 @@ import Kore.Internal.TermLike (
     TermLike,
     mkAnd,
     mkBottom,
-    mkBottom_,
     mkTop,
-    mkTop_,
     termLikeSort,
  )
 import qualified Kore.Internal.TermLike as TermLike
@@ -110,11 +105,7 @@ fromTermAndPredicate term predicate =
         , predicate
         , substitution = mempty
         }
-fromCondition_ ::
-    InternalVariable variable =>
-    Condition variable ->
-    Pattern variable
-fromCondition_ = (<$) mkTop_
+
 fromCondition ::
     InternalVariable variable =>
     Sort ->
@@ -239,17 +230,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'.
@@ -262,17 +242,6 @@ bottomOf resultSort =
         , substitution = mempty
         }
 
-{- |'top' is an expanded pattern that has a top condition and that
-should become Top when transformed to a ML pattern.
--}
-top :: InternalVariable variable => Pattern variable
-top =
-    Conditional
-        { term = mkTop_
-        , predicate = Predicate.makeTruePredicate
-        , substitution = mempty
-        }
-
 -- | An 'Pattern' where the 'term' is 'Top' of the given 'Sort'.
 topOf :: InternalVariable variable => Sort -> Pattern variable
 topOf resultSort =
@@ -342,7 +311,7 @@ coerceSort
             { term =
                 if isTop term
                     then mkTop sort
-                    else TermLike.forceSort sort term
+                    else TermLike.sameTermLikeSort sort term
             , -- Need to override this since a 'ceil' (say) over a predicate is that
               -- predicate with a different sort.
               predicate = predicate
@@ -410,9 +379,10 @@ substitute subst Conditional{term, predicate, substitution} =
 
 fromMultiAnd ::
     InternalVariable variable =>
+    Sort ->
     MultiAnd (Pattern variable) ->
     Pattern variable
-fromMultiAnd patterns =
+fromMultiAnd sort patterns =
     foldr
         ( \pattern1 ->
             pure
@@ -422,4 +392,4 @@ fromMultiAnd patterns =
         )
         Nothing
         patterns
-        & fromMaybe top
+        & fromMaybe (topOf sort)

kore/src/Kore/Internal/Predicate.hs

@@ -143,9 +143,6 @@ import Kore.Internal.TermLike hiding (
     substitute,
  )
 import qualified Kore.Internal.TermLike as TermLike
-import Kore.Sort (
-    predicateSort,
- )
 import Kore.TopBottom (
     TopBottom (..),
  )
@@ -454,11 +451,13 @@ fromPredicate sort = Recursive.fold worker
             OrF (Or () t1 t2) -> TermLike.mkOr t1 t2
             TopF _ -> TermLike.mkTop sort
 
+
 fromPredicate_ ::
     InternalVariable variable =>
     Predicate variable ->
     TermLike variable
-fromPredicate_ = fromPredicate predicateSort
+fromPredicate_ = fromPredicate undefined
+
 
 {- | Simple type used to track whether a predicate building function performed
     a simplification that changed the shape of the resulting term. This is
@@ -682,7 +681,7 @@ makeInPredicate' ::
     TermLike variable ->
     (Predicate variable, HasChanged)
 makeInPredicate' t1 t2 =
-    (TermLike.makeSortsAgree makeInWorker t1 t2, NotChanged)
+    (TermLike.checkSortsAgree makeInWorker t1 t2, NotChanged)
   where
     makeInWorker t1' t2' _ = synthesize $ InF $ In () () t1' t2'
 
@@ -699,7 +698,7 @@ makeEqualsPredicate' ::
     TermLike variable ->
     (Predicate variable, HasChanged)
 makeEqualsPredicate' t1 t2 =
-    (TermLike.makeSortsAgree makeEqualsWorker t1 t2, NotChanged)
+    (TermLike.checkSortsAgree makeEqualsWorker t1 t2, NotChanged)
   where
     makeEqualsWorker t1' t2' _ = synthesize $ EqualsF $ Equals () () t1' t2'