From 09f6ec8db857fa58afdc53837b80f4e4cdc6f26c Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 1 Sep 2020 14:28:42 -0500 Subject: [PATCH] Revert "Revert "Stop execution on ErrorBottomTotalFunction (#2088)" (#2111)" This reverts commit a45859f26f5424dd82c006e761fee4141b11e815. --- kore/src/Kore/Log/ErrorBottomTotalFunction.hs | 14 +++++++++-- kore/src/Kore/Step/Function/Evaluator.hs | 4 ++++ .../Kore/Step/Simplification/Application.hs | 24 +++++++++++++++---- kore/src/Kore/Step/Simplification/TermLike.hs | 4 ++++ kore/test/Test/Kore/Builtin/Definition.hs | 4 ++-- .../Test/Kore/Step/Simplification/TermLike.hs | 5 +++- 6 files changed, 46 insertions(+), 9 deletions(-) diff --git a/kore/src/Kore/Log/ErrorBottomTotalFunction.hs b/kore/src/Kore/Log/ErrorBottomTotalFunction.hs index 7a663ed285..9845d16929 100644 --- a/kore/src/Kore/Log/ErrorBottomTotalFunction.hs +++ b/kore/src/Kore/Log/ErrorBottomTotalFunction.hs @@ -11,6 +11,11 @@ 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 @@ -45,6 +50,11 @@ 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" @@ -52,9 +62,9 @@ instance Entry ErrorBottomTotalFunction where instance SQL.Table ErrorBottomTotalFunction errorBottomTotalFunction - :: MonadLog logger + :: MonadThrow logger => InternalVariable variable => TermLike variable -> logger () errorBottomTotalFunction (mapVariables (pure toVariableName) -> term) = - logEntry ErrorBottomTotalFunction { term } + throwM ErrorBottomTotalFunction { term } diff --git a/kore/src/Kore/Step/Function/Evaluator.hs b/kore/src/Kore/Step/Function/Evaluator.hs index 1b01a8f3f0..ec732c911f 100644 --- a/kore/src/Kore/Step/Function/Evaluator.hs +++ b/kore/src/Kore/Step/Function/Evaluator.hs @@ -21,6 +21,9 @@ 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 @@ -71,6 +74,7 @@ evaluateApplication :: forall variable simplifier . ( InternalVariable variable , MonadSimplify simplifier + , MonadThrow simplifier ) => SideCondition variable -- ^ The predicate from the configuration diff --git a/kore/src/Kore/Step/Simplification/Application.hs b/kore/src/Kore/Step/Simplification/Application.hs index bcf6140feb..da189996b2 100644 --- a/kore/src/Kore/Step/Simplification/Application.hs +++ b/kore/src/Kore/Step/Simplification/Application.hs @@ -14,6 +14,10 @@ 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 @@ -58,7 +62,10 @@ predicates ans substitutions, applying functions on the Application(terms), then merging everything into an Pattern. -} simplify - :: (InternalVariable variable, MonadSimplify simplifier) + :: ( InternalVariable variable + , MonadSimplify simplifier + , MonadThrow simplifier + ) => SideCondition variable -> Application Symbol (OrPattern variable) -> simplifier (OrPattern variable) @@ -80,7 +87,10 @@ simplify sideCondition application = do childrenCrossProduct = MultiOr.fullCrossProduct children makeAndEvaluateApplications - :: (InternalVariable variable, MonadSimplify simplifier) + :: ( InternalVariable variable + , MonadSimplify simplifier + , MonadThrow simplifier + ) => SideCondition variable -> Symbol -> [Pattern variable] @@ -89,7 +99,10 @@ makeAndEvaluateApplications = makeAndEvaluateSymbolApplications makeAndEvaluateSymbolApplications - :: (InternalVariable variable, MonadSimplify simplifier) + :: ( InternalVariable variable + , MonadSimplify simplifier + , MonadThrow simplifier + ) => SideCondition variable -> Symbol -> [Pattern variable] @@ -105,7 +118,10 @@ makeAndEvaluateSymbolApplications sideCondition symbol children = do return (MultiOr.mergeAll orResults) evaluateApplicationFunction - :: (InternalVariable variable, MonadSimplify simplifier) + :: ( InternalVariable variable + , MonadSimplify simplifier + , MonadThrow simplifier + ) => SideCondition variable -- ^ The predicate from the configuration -> ExpandedApplication variable diff --git a/kore/src/Kore/Step/Simplification/TermLike.hs b/kore/src/Kore/Step/Simplification/TermLike.hs index 4fb78ee1d2..0e17c4f201 100644 --- a/kore/src/Kore/Step/Simplification/TermLike.hs +++ b/kore/src/Kore/Step/Simplification/TermLike.hs @@ -10,6 +10,9 @@ 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 @@ -167,6 +170,7 @@ simplify . HasCallStack => InternalVariable variable => MonadSimplify simplifier + => MonadThrow simplifier => SideCondition variable -> TermLike variable -> simplifier (OrPattern variable) diff --git a/kore/test/Test/Kore/Builtin/Definition.hs b/kore/test/Test/Kore/Builtin/Definition.hs index ed2514616c..d956a77821 100644 --- a/kore/test/Test/Kore/Builtin/Definition.hs +++ b/kore/test/Test/Kore/Builtin/Definition.hs @@ -437,7 +437,7 @@ elementMapSymbol = concatMapSymbol :: Internal.Symbol concatMapSymbol = - binarySymbol "concatMap" mapSort & hook "MAP.concat" & functional + binarySymbol "concatMap" mapSort & hook "MAP.concat" & function inKeysMapSymbol :: Internal.Symbol inKeysMapSymbol = @@ -596,7 +596,7 @@ elementSet x = mkApplySymbol elementSetSymbol [x] concatSetSymbol :: Internal.Symbol concatSetSymbol = - binarySymbol "concatSet" setSort & hook "SET.concat" & functional + binarySymbol "concatSet" setSort & hook "SET.concat" & function concatSet :: TermLike VariableName diff --git a/kore/test/Test/Kore/Step/Simplification/TermLike.hs b/kore/test/Test/Kore/Step/Simplification/TermLike.hs index 2df557999c..a505dcfae6 100644 --- a/kore/test/Test/Kore/Step/Simplification/TermLike.hs +++ b/kore/test/Test/Kore/Step/Simplification/TermLike.hs @@ -10,6 +10,9 @@ import Test.Tasty.HUnit import Control.Monad ( void ) +import Control.Monad.Catch + ( MonadThrow + ) import Kore.Internal.OrPattern ( OrPattern @@ -45,7 +48,7 @@ simplifyEvaluated original = newtype TestSimplifier a = TestSimplifier { getTestSimplifier :: Simplifier a } deriving (Functor, Applicative, Monad) - deriving (MonadLog, MonadSMT) + deriving (MonadLog, MonadSMT, MonadThrow) instance MonadSimplify TestSimplifier where askMetadataTools = TestSimplifier askMetadataTools