Redo everything (#1940)

Author: andreiburdusa

kore/src/Kore/Log/WarnBottomTotalFunction.hs renamed to kore/src/Kore/Log/ErrorBottomTotalFunction.hs

@@ -4,9 +4,9 @@ License     : NCSA
 
 -}
 
-module Kore.Log.WarnBottomTotalFunction
-    ( WarnBottomTotalFunction (..)
-    , warnBottomTotalFunction
+module Kore.Log.ErrorBottomTotalFunction
+    ( ErrorBottomTotalFunction (..)
+    , errorBottomTotalFunction
     ) where
 
 import Prelude.Kore
@@ -29,35 +29,35 @@ import qualified Pretty
 import Log
 import qualified SQL
 
-newtype WarnBottomTotalFunction =
-    WarnBottomTotalFunction
+newtype ErrorBottomTotalFunction =
+    ErrorBottomTotalFunction
         { term :: TermLike VariableName
         }
     deriving (Show)
     deriving (GHC.Generic)
 
-instance SOP.Generic WarnBottomTotalFunction
+instance SOP.Generic ErrorBottomTotalFunction
 
-instance SOP.HasDatatypeInfo WarnBottomTotalFunction
+instance SOP.HasDatatypeInfo ErrorBottomTotalFunction
 
-instance Pretty WarnBottomTotalFunction where
-    pretty WarnBottomTotalFunction { term } =
+instance Pretty ErrorBottomTotalFunction where
+    pretty ErrorBottomTotalFunction { term } =
         Pretty.vsep
             [ "Evaluating total function"
             , Pretty.indent 4 (unparse term)
             , "has resulted in \\bottom."
             ]
 
-instance Entry WarnBottomTotalFunction where
-    entrySeverity _ = Warning
-    helpDoc _ = "warn when a total function is undefined"
+instance Entry ErrorBottomTotalFunction where
+    entrySeverity _ = Error
+    helpDoc _ = "errors raised when a total function is undefined"
 
-instance SQL.Table WarnBottomTotalFunction
+instance SQL.Table ErrorBottomTotalFunction
 
-warnBottomTotalFunction
+errorBottomTotalFunction
     :: MonadLog logger
     => InternalVariable variable
     => TermLike variable
     -> logger ()
-warnBottomTotalFunction (mapVariables (pure toVariableName) -> term) =
-    logEntry WarnBottomTotalFunction { term }
+errorBottomTotalFunction (mapVariables (pure toVariableName) -> term) =
+    logEntry ErrorBottomTotalFunction { term }

kore/src/Kore/Log/Registry.hs

@@ -62,6 +62,9 @@ import Kore.Log.DebugSubstitutionSimplifier
 import Kore.Log.DebugUnification
     ( DebugUnification
     )
+import Kore.Log.ErrorBottomTotalFunction
+    ( ErrorBottomTotalFunction
+    )
 import Kore.Log.ErrorException
     ( ErrorException
     )
@@ -77,9 +80,6 @@ import Kore.Log.InfoAttemptUnification
 import Kore.Log.InfoReachability
     ( InfoReachability
     )
-import Kore.Log.WarnBottomTotalFunction
-    ( WarnBottomTotalFunction
-    )
 import Kore.Log.WarnDecidePredicateUnknown
     ( WarnDecidePredicateUnknown
     )
@@ -131,7 +131,7 @@ entryHelpDocs :: [Pretty.Doc ()]
     , mk $ Proxy @DebugProofState
     , mk $ Proxy @DebugAppliedRewriteRules
     , mk $ Proxy @DebugSubstitutionSimplifier
-    , mk $ Proxy @WarnBottomTotalFunction
+    , mk $ Proxy @ErrorBottomTotalFunction
     , mk $ Proxy @WarnDecidePredicateUnknown
     , mk $ Proxy @WarnFunctionWithoutEvaluators
     , mk $ Proxy @WarnSymbolSMTRepresentation

kore/src/Kore/Log/SQLite.hs

@@ -35,8 +35,8 @@ import Kore.Log.DebugEvaluateCondition
 import Kore.Log.DebugSubstitutionSimplifier
     ( DebugSubstitutionSimplifier
     )
-import Kore.Log.WarnBottomTotalFunction
-    ( WarnBottomTotalFunction
+import Kore.Log.ErrorBottomTotalFunction
+    ( ErrorBottomTotalFunction
     )
 import Kore.Log.WarnFunctionWithoutEvaluators
     ( WarnFunctionWithoutEvaluators
@@ -127,7 +127,7 @@ foldMapEntries mapEntry =
     mconcat
         [ mapEntry (Proxy @DebugEvaluateCondition)
         , mapEntry (Proxy @DebugSubstitutionSimplifier)
-        , mapEntry (Proxy @WarnBottomTotalFunction)
+        , mapEntry (Proxy @ErrorBottomTotalFunction)
         , mapEntry (Proxy @WarnFunctionWithoutEvaluators)
         , mapEntry (Proxy @WarnSymbolSMTRepresentation)
         ]

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

@@ -47,8 +47,8 @@ import qualified Kore.Internal.SideCondition.SideCondition as SideCondition
     )
 import qualified Kore.Internal.Symbol as Symbol
 import Kore.Internal.TermLike as TermLike
-import Kore.Log.WarnBottomTotalFunction
-    ( warnBottomTotalFunction
+import Kore.Log.ErrorBottomTotalFunction
+    ( errorBottomTotalFunction
     )
 import qualified Kore.Profiler.Profile as Profile
     ( axiomBranching
@@ -109,7 +109,7 @@ evaluateApplication
         & lift
     Foldable.for_ canMemoize (recordOrPattern results)
     when (Symbol.isFunctional symbol && isBottom results) $
-        lift $ warnBottomTotalFunction termLike
+        lift $ errorBottomTotalFunction termLike
     return results
   where
     finishT :: ExceptT r simplifier r -> simplifier r

kore/test/Test/Kore/Log/ErrorBottomTotalFunction.hs

@@ -0,0 +1,20 @@
+module Test.Kore.Log.ErrorBottomTotalFunction
+    ( test_instance_Table_ErrorBottomTotalFunction
+    ) where
+
+import Prelude.Kore ()
+
+import Test.Tasty
+
+import Kore.Log.ErrorBottomTotalFunction
+
+import qualified Test.Kore.Step.MockSymbols as Mock
+import Test.SQL
+
+test_instance_Table_ErrorBottomTotalFunction :: TestTree
+test_instance_Table_ErrorBottomTotalFunction =
+    testTable @ErrorBottomTotalFunction [warn1, warn2]
+
+warn1, warn2 :: ErrorBottomTotalFunction
+warn1 = ErrorBottomTotalFunction Mock.a
+warn2 = ErrorBottomTotalFunction Mock.b