Remove _PREDICATE sort

kore/app/exec/Main.hs

@@ -91,9 +91,13 @@ import Kore.Reachability (
     SomeClaim,
     StuckClaim (..),
     getConfiguration,
+    lensClaimPattern,
  )
 import qualified Kore.Reachability.Claim as Claim
 import Kore.Rewrite
+import Kore.Rewrite.ClaimPattern (
+    getClaimPatternSort,
+ )
 import Kore.Rewrite.RewritingVariable
 import Kore.Rewrite.RulePattern (
     mapRuleVariables,
@@ -113,9 +117,6 @@ import Kore.Syntax.Definition (
     Sentence (..),
  )
 import qualified Kore.Syntax.Definition as Definition.DoNotUse
-import Kore.TopBottom (
-    isTop,
- )
 import Kore.Unparser (
     unparse,
  )
@@ -714,18 +715,22 @@ koreProve execOptions proveOptions = do
             maybeAlreadyProvenModule
 
     let ProveClaimsResult{stuckClaims, provenClaims} = proveResult
-    let (exitCode, final)
-            | noStuckClaims = success
-            | otherwise =
-                stuckPatterns
-                    & OrPattern.toTermLike
-                    & failure
+    let (exitCode, final) =
+            case foldFirst stuckClaims of
+                Nothing -> success -- stuckClaims is empty
+                Just claim ->
+                    stuckPatterns
+                        & OrPattern.toTermLike (getClaimPatternSort $ claimPattern claim)
+                        & failure
           where
-            noStuckClaims = isTop stuckClaims
             stuckPatterns =
                 OrPattern.fromPatterns (MultiAnd.map getStuckConfig stuckClaims)
             getStuckConfig =
                 getRewritingPattern . getConfiguration . getStuckClaim
+            claimPattern claim =
+                claim
+                    & getStuckClaim
+                    & Lens.view lensClaimPattern
     lift $ for_ saveProofs $ saveProven specModule provenClaims
     lift $ renderResult execOptions (unparse final)
     return (kFileLocations definition, exitCode)

kore/src/Kore/Builtin/AssociativeCommutative.hs

@@ -115,6 +115,7 @@ import Kore.Rewrite.RewritingVariable (
 import Kore.Simplify.Simplify as Simplifier
 import Kore.Sort (
     Sort,
+    sameSort,
  )
 import Kore.Syntax.Variable
 import Kore.Unification.Unify (
@@ -1400,7 +1401,10 @@ unifyEqualsElementLists
 
             let remainder2Terms = map fromConcreteOrWithVariable remainder2
 
-            case elementListAsInternal tools (termLikeSort first) remainder2Terms of
+            case elementListAsInternal
+                tools
+                (sameSort (termLikeSort first) (termLikeSort second))
+                remainder2Terms of
                 Nothing ->
                     debugUnifyBottomAndReturnBottom
                         "Duplicated element in unification results"

kore/src/Kore/Builtin/Builtin.hs

@@ -96,9 +96,6 @@ import Kore.Simplify.Simplify (
 import qualified Kore.Simplify.Simplify as AttemptedAxiomResults (
     AttemptedAxiomResults (..),
  )
-import Kore.Sort (
-    predicateSort,
- )
 import Kore.Unparser
 import Prelude.Kore
 
@@ -448,19 +445,15 @@ isSymbol builtinName Symbol{symbolAttributes = Attribute.Symbol{hook}} =
 
 {- | Is the given sort hooked to the named builtin?
 
-Returns Nothing if the sort is unknown (i.e. the _PREDICATE sort).
-Returns Just False if the sort is a variable.
+Returns Nothing 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 ::

kore/src/Kore/Builtin/EqTerm.hs

@@ -9,12 +9,12 @@ module Kore.Builtin.EqTerm (
 ) where
 
 import qualified Control.Monad as Monad
+import Kore.Internal.ApplicationSorts (applicationSortsResult)
 import qualified Kore.Internal.MultiOr as MultiOr
 import qualified Kore.Internal.OrPattern as OrPattern
 import Kore.Internal.Pattern (
     Pattern,
  )
-import qualified Kore.Internal.Pattern as Pattern
 import qualified Kore.Internal.SideCondition as SideCondition
 import Kore.Internal.TermLike as TermLike
 import Kore.Rewrite.RewritingVariable (
@@ -48,7 +48,6 @@ matchEqTerm selectSymbol (App_ symbol [operand1, operand2]) = do
 matchEqTerm _ _ = Nothing
 
 {- | Unification for an equality-like symbol.
-
 This function is suitable only for equality simplification.
 -}
 unifyEqTerm ::
@@ -63,8 +62,11 @@ unifyEqTerm unifyChildren (NotSimplifier notSimplifier) eqTerm value =
     do
         solution <- unifyChildren operand1 operand2 & OrPattern.gather
         let solution' = MultiOr.map eraseTerm solution
-        (if value then pure else notSimplifier SideCondition.top) solution'
+        (if value then pure else mkNotSimplified) solution'
             >>= Unify.scatter
   where
-    EqTerm{operand1, operand2} = eqTerm
-    eraseTerm = Pattern.fromCondition_ . Pattern.withoutTerm
+    EqTerm{symbol, operand1, operand2} = eqTerm
+    eqSort = applicationSortsResult . symbolSorts $ symbol
+    eraseTerm conditional = conditional $> (mkTop eqSort)
+    mkNotSimplified notChild =
+        notSimplifier SideCondition.top Not{notSort = eqSort, notChild}

kore/src/Kore/Builtin/Int.hs

@@ -126,6 +126,7 @@ import Kore.Internal.Predicate (
  )
 import qualified Kore.Internal.SideCondition as SideCondition
 import Kore.Internal.Symbol (
+    applicationSortsResult,
     symbolHook,
  )
 import Kore.Internal.TermLike as TermLike
@@ -524,10 +525,13 @@ unifyIntEq unifyChildren (NotSimplifier notSimplifier) unifyData =
             MultiOr.map eraseTerm solution
                 & if internalBoolValue internalBool
                     then pure
-                    else notSimplifier SideCondition.top
+                    else mkNotSimplified
         scattered <- Unify.scatter solution'
         return scattered{term = mkInternalBool internalBool}
   where
     UnifyIntEq{eqTerm, internalBool} = unifyData
-    EqTerm{operand1, operand2} = eqTerm
-    eraseTerm = Pattern.fromCondition_ . Pattern.withoutTerm
+    EqTerm{symbol, operand1, operand2} = eqTerm
+    eqSort = applicationSortsResult . symbolSorts $ symbol
+    eraseTerm conditional = conditional $> (mkTop eqSort)
+    mkNotSimplified notChild =
+        notSimplifier SideCondition.top Not{notSort = eqSort, notChild}

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/KEqual.hs

@@ -276,13 +276,16 @@ unifyKequalsEq unifyChildren (NotSimplifier notSimplifier) unifyData =
             MultiOr.map eraseTerm solution
                 & if internalBoolValue internalBool
                     then pure
-                    else notSimplifier SideCondition.top
+                    else mkNotSimplified
         scattered <- Unify.scatter solution'
         return (scattered :: Pattern RewritingVariableName){term = mkInternalBool internalBool}
   where
     UnifyKequalsEq{eqTerm, internalBool} = unifyData
-    EqTerm{operand1, operand2} = eqTerm
-    eraseTerm = Pattern.fromCondition_ . Pattern.withoutTerm
+    EqTerm{symbol, operand1, operand2} = eqTerm
+    eqSort = applicationSortsResult . symbolSorts $ symbol
+    eraseTerm conditional = conditional $> (mkTop eqSort)
+    mkNotSimplified notChild =
+        notSimplifier SideCondition.top Not{notSort = eqSort, notChild}
 
 -- | The @KEQUAL.ite@ hooked symbol applied to @term@-type arguments.
 data IfThenElse term = IfThenElse

kore/src/Kore/Builtin/List.hs

@@ -277,7 +277,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
@@ -629,7 +629,7 @@ unifyEquals
                 "Cannot unify lists of different length."
                 term1
                 term2
-            return Pattern.bottom
+            return (Pattern.bottomOf $ termLikeSort term1)
 
         unifyEqualsFramedRightRight ::
             TermLike.Symbol ->

kore/src/Kore/Builtin/Map.hs

@@ -89,6 +89,7 @@ import Kore.Internal.Symbol (
  )
 import Kore.Internal.TermLike (
     Key,
+    Not (..),
     TermLike,
     retractKey,
     termLikeSort,
@@ -707,13 +708,14 @@ matchUnifyNotInKeys first second
 unifyNotInKeys ::
     forall unifier.
     MonadUnify unifier =>
+    Sort ->
     TermSimplifier RewritingVariableName unifier ->
     NotSimplifier unifier ->
     UnifyNotInKeysResult ->
     unifier (Pattern RewritingVariableName)
-unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) unifyData =
+unifyNotInKeys resultSort unifyChildren (NotSimplifier notSimplifier) unifyData =
     case unifyData of
-        NullKeysNullOpaques -> return Pattern.top
+        NullKeysNullOpaques -> return (Pattern.topOf resultSort)
         NonNullKeysOrMultipleOpaques unifyData' ->
             do
                 -- Concrete keys are constructor-like, therefore they are defined
@@ -750,18 +752,19 @@ unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) unifyData =
             >>= Unify.scatter
 
     eraseTerm =
-        Pattern.fromCondition_ . Pattern.withoutTerm
+        Pattern.fromCondition resultSort . Pattern.withoutTerm
 
     unifyAndNegate t1 t2 =
         do
             -- Erasing the unified term is valid here because
             -- the terms are all wrapped in \ceil below.
             unificationSolutions <-
-                fmap eraseTerm
-                    <$> Unify.gather (unifyChildren t1 t2)
-            notSimplifier
-                SideCondition.top
-                (OrPattern.fromPatterns unificationSolutions)
+                fmap eraseTerm <$> Unify.gather (unifyChildren t1 t2)
+            (notSimplifier SideCondition.top)
+                Not
+                    { notSort = resultSort
+                    , notChild = OrPattern.fromPatterns unificationSolutions
+                    }
             >>= Unify.scatter
 
-    collectConditions terms = fold terms & Pattern.fromCondition_
+    collectConditions terms = fold terms & Pattern.fromCondition resultSort

kore/src/Kore/Builtin/String.hs

@@ -574,10 +574,13 @@ unifyStringEq unifyChildren (NotSimplifier notSimplifier) unifyData =
             MultiOr.map eraseTerm solution
                 & if internalBoolValue internalBool
                     then pure
-                    else notSimplifier SideCondition.top
+                    else mkNotSimplified
         scattered <- Unify.scatter solution'
         return scattered{term = mkInternalBool internalBool}
   where
     UnifyStringEq{eqTerm, internalBool} = unifyData
-    EqTerm{operand1, operand2} = eqTerm
-    eraseTerm = Pattern.fromCondition_ . Pattern.withoutTerm
+    EqTerm{symbol, operand1, operand2} = eqTerm
+    eqSort = applicationSortsResult . symbolSorts $ symbol
+    eraseTerm conditional = conditional $> (mkTop eqSort)
+    mkNotSimplified notChild =
+        notSimplifier SideCondition.top Not{notSort = eqSort, notChild}

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

@@ -91,7 +91,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/Equation/Validate.hs

@@ -13,6 +13,7 @@ import qualified Data.Functor.Foldable as Recursive
 import Data.Text (
     pack,
  )
+import Kore.AST.AstWithLocation
 import Kore.AST.Error
 import Kore.Attribute.Axiom (
     Assoc (..),
@@ -36,11 +37,18 @@ import Kore.Equation.Sentence (
     fromSentenceAxiom,
  )
 import Kore.Internal.Predicate (
+    Predicate,
     pattern PredicateCeil,
     pattern PredicateIn,
  )
 import qualified Kore.Internal.Predicate as Predicate
 import qualified Kore.Internal.Symbol as Symbol
+import Kore.Internal.TermLike (
+    AstLocation,
+    InternalVariable,
+    TermLike,
+    mkSortVariable,
+ )
 import qualified Kore.Internal.TermLike as TermLike
 import Kore.Syntax.Definition
 import Kore.Syntax.Variable
@@ -50,6 +58,7 @@ import Kore.Unparser (
 import Kore.Validate.Verifier
 import qualified Kore.Verified as Verified
 import Prelude.Kore
+import Pretty (Doc)
 import qualified Pretty
 
 validateAxiom ::
@@ -121,25 +130,42 @@ validateAxiom attrs verified =
             failOnJust
                 eq
                 "Expected variable, but found:"
-                $ asum $ getNotVar <$> termLikeF
+                (fmap unparseWithLocation $ asum $ getNotVar <$> termLikeF)
 
         getNotVar (TermLike.Var_ _) = Nothing
         getNotVar term = Just term
 
+    unparseWithLocation ::
+        AstWithLocation variable =>
+        InternalVariable variable =>
+        TermLike variable ->
+        (Doc ann, AstLocation)
+    unparseWithLocation t = (unparse t, locationFromAst t)
+
     checkArg _ Nothing = return ()
     checkArg eq (Just arg) =
         traverse_
             ( failOnJust eq "Found invalid subterm in argument of function equation:"
-                . checkArgIn
+                . checkArgInAndUnparse
             )
             $ Predicate.getMultiAndPredicate arg
       where
-        checkArgIn (PredicateIn (TermLike.Var_ _) term) =
-            findBadArgSubterm term
-        checkArgIn (PredicateCeil (TermLike.And_ _ (TermLike.Var_ _) term)) =
-            findBadArgSubterm term
-        checkArgIn badArg = Just $ Predicate.fromPredicate_ badArg
-
+        checkArgInAndUnparse ::
+            AstWithLocation variable =>
+            InternalVariable variable =>
+            Predicate variable ->
+            Maybe (Doc ann, AstLocation)
+        checkArgInAndUnparse predicate =
+            checkArgIn predicate <&> unparseWithLocation
+          where
+            checkArgIn (PredicateIn (TermLike.Var_ _) term) =
+                findBadArgSubterm term
+            checkArgIn (PredicateCeil (TermLike.And_ _ (TermLike.Var_ _) term)) =
+                findBadArgSubterm term
+            checkArgIn badArg =
+                -- use dummy sort variable for pretty printing inside failOnJust
+                -- the term's AstLocation will be AstLocationNone
+                Just $ Predicate.fromPredicate (mkSortVariable "_") badArg
         findBadArgSubterm term = case term of
             _
                 | TermLike.isConstructorLike term -> descend
@@ -175,14 +201,14 @@ validateAxiom attrs verified =
             descend = asum $ findBadArgSubterm <$> termF
 
     failOnJust _ _ Nothing = return ()
-    failOnJust eq errorMessage (Just term) =
+    failOnJust eq errorMessage (Just (term, location)) =
         koreFailWithLocations
-            [term]
+            [location]
             ( pack $
                 show $
                     Pretty.vsep
                         [ errorMessage
-                        , Pretty.indent 4 $ unparse term
+                        , Pretty.indent 4 term
                         , "The equation that the above occurs in is:"
                         , Pretty.indent 4 $ Pretty.pretty eq
                         ]