Revert "Stop execution on ErrorBottomTotalFunction (#2088)" (#2111)

This reverts commit 9c3511c.

Author: ttuegel

kore/src/Kore/Log/ErrorBottomTotalFunction.hs

@@ -11,11 +11,6 @@ module Kore.Log.ErrorBottomTotalFunction
 
 import Prelude.Kore
 
-import Control.Monad.Catch
-    ( Exception (..)
-    , MonadThrow
-    , throwM
-    )
 import qualified Generics.SOP as SOP
 import qualified GHC.Generics as GHC
 
@@ -50,21 +45,16 @@ instance Pretty ErrorBottomTotalFunction where
             , "has resulted in \\bottom."
             ]
 
-instance Exception ErrorBottomTotalFunction where
-    toException = toException . SomeEntry
-    fromException exn =
-        fromException exn >>= \entry -> fromEntry entry
-
 instance Entry ErrorBottomTotalFunction where
     entrySeverity _ = Error
     helpDoc _ = "errors raised when a total function is undefined"
 
 instance SQL.Table ErrorBottomTotalFunction
 
 errorBottomTotalFunction
-    :: MonadThrow logger
+    :: MonadLog logger
     => InternalVariable variable
     => TermLike variable
     -> logger ()
 errorBottomTotalFunction (mapVariables (pure toVariableName) -> term) =
-    throwM ErrorBottomTotalFunction { term }
+    logEntry ErrorBottomTotalFunction { term }

kore/src/Kore/Step/Function/Evaluator.hs

@@ -21,9 +21,6 @@ import Control.Error
     , maybeT
     , throwE
     )
-import Control.Monad.Catch
-    ( MonadThrow
-    )
 import qualified Data.Foldable as Foldable
 
 import qualified Kore.Attribute.Pattern.Simplified as Attribute.Simplified
@@ -74,7 +71,6 @@ evaluateApplication
     :: forall variable simplifier
     .  ( InternalVariable variable
        , MonadSimplify simplifier
-       , MonadThrow simplifier
        )
     => SideCondition variable
     -- ^ The predicate from the configuration

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

@@ -14,10 +14,6 @@ module Kore.Step.Simplification.Application
 
 import Prelude.Kore
 
-import Control.Monad.Catch
-    ( MonadThrow
-    )
-
 import qualified Kore.Internal.Conditional as Conditional
 import qualified Kore.Internal.MultiOr as MultiOr
     ( fullCrossProduct
@@ -62,10 +58,7 @@ predicates ans substitutions, applying functions on the Application(terms),
 then merging everything into an Pattern.
 -}
 simplify
-    ::  ( InternalVariable variable
-        , MonadSimplify simplifier
-        , MonadThrow simplifier
-        )
+    :: (InternalVariable variable, MonadSimplify simplifier)
     => SideCondition variable
     -> Application Symbol (OrPattern variable)
     -> simplifier (OrPattern variable)
@@ -87,10 +80,7 @@ simplify sideCondition application = do
     childrenCrossProduct = MultiOr.fullCrossProduct children
 
 makeAndEvaluateApplications
-    ::  ( InternalVariable variable
-        , MonadSimplify simplifier
-        , MonadThrow simplifier
-        )
+    :: (InternalVariable variable, MonadSimplify simplifier)
     => SideCondition variable
     -> Symbol
     -> [Pattern variable]
@@ -99,10 +89,7 @@ makeAndEvaluateApplications =
     makeAndEvaluateSymbolApplications
 
 makeAndEvaluateSymbolApplications
-    ::  ( InternalVariable variable
-        , MonadSimplify simplifier
-        , MonadThrow simplifier
-        )
+    :: (InternalVariable variable, MonadSimplify simplifier)
     => SideCondition variable
     -> Symbol
     -> [Pattern variable]
@@ -118,10 +105,7 @@ makeAndEvaluateSymbolApplications sideCondition symbol children = do
     return (MultiOr.mergeAll orResults)
 
 evaluateApplicationFunction
-    ::  ( InternalVariable variable
-        , MonadSimplify simplifier
-        , MonadThrow simplifier
-        )
+    :: (InternalVariable variable, MonadSimplify simplifier)
     => SideCondition variable
     -- ^ The predicate from the configuration
     -> ExpandedApplication variable

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

@@ -10,9 +10,6 @@ module Kore.Step.Simplification.TermLike
 import Prelude.Kore
 
 import qualified Control.Lens.Combinators as Lens
-import Control.Monad.Catch
-    ( MonadThrow
-    )
 import Data.Functor.Const
 import qualified Data.Functor.Foldable as Recursive
 
@@ -170,7 +167,6 @@ simplify
     .  HasCallStack
     => InternalVariable variable
     => MonadSimplify simplifier
-    => MonadThrow simplifier
     => SideCondition variable
     -> TermLike variable
     -> simplifier (OrPattern variable)

kore/test/Test/Kore/Builtin/Definition.hs

@@ -437,7 +437,7 @@ elementMapSymbol =
 
 concatMapSymbol :: Internal.Symbol
 concatMapSymbol =
-    binarySymbol "concatMap" mapSort & hook "MAP.concat" & function
+    binarySymbol "concatMap" mapSort & hook "MAP.concat" & functional
 
 inKeysMapSymbol :: Internal.Symbol
 inKeysMapSymbol =
@@ -596,7 +596,7 @@ elementSet x = mkApplySymbol elementSetSymbol [x]
 
 concatSetSymbol :: Internal.Symbol
 concatSetSymbol =
-    binarySymbol "concatSet" setSort & hook "SET.concat" & function
+    binarySymbol "concatSet" setSort & hook "SET.concat" & functional
 
 concatSet
     :: TermLike VariableName

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

@@ -10,9 +10,6 @@ import Test.Tasty.HUnit
 import Control.Monad
     ( void
     )
-import Control.Monad.Catch
-    ( MonadThrow
-    )
 
 import Kore.Internal.OrPattern
     ( OrPattern
@@ -48,7 +45,7 @@ simplifyEvaluated original =
 
 newtype TestSimplifier a = TestSimplifier { getTestSimplifier :: Simplifier a }
     deriving (Functor, Applicative, Monad)
-    deriving (MonadLog, MonadSMT, MonadThrow)
+    deriving (MonadLog, MonadSMT)
 
 instance MonadSimplify TestSimplifier where
     askMetadataTools = TestSimplifier askMetadataTools