Merge branch 'master' into issue-1665--refactor

Author: ttuegel

kore/app/exec/Main.hs

@@ -89,11 +89,11 @@ import Kore.IndexedModule.IndexedModule
 import qualified Kore.IndexedModule.MetadataToolsBuilder as MetadataTools
     ( build
     )
+import qualified Kore.Internal.OrPattern as OrPattern
 import Kore.Internal.Pattern
     ( Conditional (..)
     , Pattern
     )
-import qualified Kore.Internal.Pattern as Pattern
 import Kore.Internal.Predicate
     ( makePredicate
     )
@@ -678,12 +678,15 @@ koreProve execOptions proveOptions = do
             maybeAlreadyProvenModule
 
     (exitCode, final) <- case proveResult of
-        Left Stuck { stuckPattern, provenClaims } -> do
+        Left Stuck { stuckPatterns, provenClaims } -> do
             maybe
                 (return ())
                 (lift . saveProven specModule provenClaims)
                 saveProofs
-            return (failure $ Pattern.toTermLike stuckPattern)
+            stuckPatterns
+                & OrPattern.toTermLike
+                & failure
+                & return
         Right () -> return success
 
     lift $ renderResult execOptions (unparse final)

kore/package.yaml

@@ -156,6 +156,7 @@ library:
   source-dirs: src
 
 _common-exe: &common-exe
+  ghc-options: -eventlog
   when:
     - condition: flag(threaded)
       then:

kore/src/Kore/Attribute/Axiom.hs

@@ -28,6 +28,7 @@ module Kore.Attribute.Axiom
     , Constructor (..)
     , RuleIndex (..)
     , UniqueId (..)
+    , PriorityAttributes (..)
     , axiomSymbolToSymbolOrAlias
     , mapAxiomVariables
     , parseAxiomAttributes
@@ -207,8 +208,13 @@ instance
             , from . owise
             ]
 
-instance From (Axiom symbol variable) (Priority, Owise) where
-    from Axiom { priority, owise } = (priority, owise)
+instance From (Axiom symbol variable) PriorityAttributes where
+    from Axiom { priority, owise, simplification } =
+        PriorityAttributes
+            { priorityAttr = priority
+            , owiseAttr = owise
+            , simplificationAttr = simplification
+            }
 
 instance From (Axiom symbol variable) HeatCool where
     from Axiom { heatCool } = heatCool
@@ -280,10 +286,49 @@ mapAxiomVariables adj axiom@Axiom { concrete, symbolic } =
         , symbolic = mapSymbolicVariables adj symbolic
         }
 
+data PriorityAttributes =
+    PriorityAttributes
+    { priorityAttr :: !Priority
+    , owiseAttr :: !Owise
+    , simplificationAttr :: !Simplification
+    }
+
 getPriorityOfAxiom
-    :: forall attrs. From attrs (Priority, Owise) => attrs -> Integer
-getPriorityOfAxiom attrs
-  | isOwise   = owisePriority
-  | otherwise = fromMaybe defaultPriority getPriority
-  where
-    (Priority { getPriority }, Owise { isOwise }) = from @attrs attrs
+    :: forall attrs
+    .  HasCallStack
+    => From attrs PriorityAttributes
+    => attrs
+    -> Integer
+getPriorityOfAxiom
+    (from @attrs ->
+        PriorityAttributes
+            { priorityAttr
+            , owiseAttr
+            , simplificationAttr
+            }
+    )
+  =
+    case (priorityAttr, owiseAttr, simplificationAttr) of
+        (Priority Nothing, Owise True, NotSimplification) ->
+            owisePriority
+        (Priority Nothing, Owise False, NotSimplification) ->
+            defaultPriority
+        (Priority (Just value), Owise False, NotSimplification) ->
+            value
+        (Priority Nothing, Owise False, IsSimplification Nothing) ->
+            defaultSimplificationPriority
+        (Priority Nothing, Owise False, IsSimplification (Just value)) ->
+            value
+        -- TODO: remove this case once the frontend
+        -- modifies the simplification attribute
+        -- to take an optional priority value
+        (Priority (Just value), Owise False, IsSimplification Nothing) ->
+            value
+        errorCase@(_, _, _) ->
+            error
+                ("An axiom cannot have the following \
+                \ combination of attributes: "
+                <> show errorCase
+                <> " Please report this error."
+                )
+

kore/src/Kore/Attribute/Parser.hs

@@ -40,6 +40,7 @@ module Kore.Attribute.Parser
     , getTwoParams
     , getZeroArguments
     , getOneArgument
+    , getZeroOrOneArguments
     , getTwoArguments
     , getSymbolOrAlias
     , Kore.Attribute.Parser.getStringLiteral
@@ -278,6 +279,19 @@ getOneArgument =
           where
             arity = length args
 
+getZeroOrOneArguments
+    :: [AttributePattern]
+    -> Parser (Maybe AttributePattern)
+getZeroOrOneArguments =
+    \case
+        [] -> return Nothing
+        [arg] -> return (Just arg)
+        args ->
+            Kore.Error.koreFail
+                ("expected at most one argument, found " <> show arity)
+          where
+            arity = length args
+
 {- | Accept exactly two arguments.
  -}
 getTwoArguments
@@ -317,7 +331,7 @@ getStringLiteral kore =
         _ :< StringLiteralF (Const lit) -> return lit
         _ -> Kore.Error.koreFail "expected string literal pattern"
 
-{- | Accept a string literal.
+{- | Accept a variable.
  -}
 getVariable :: AttributePattern -> Parser (SomeVariable VariableName)
 getVariable kore =

kore/src/Kore/Attribute/Simplification.hs

@@ -19,20 +19,30 @@ Informal example of an axiom that would use the simplification attribute:
 module Kore.Attribute.Simplification
     ( Simplification (..)
     , simplificationId, simplificationSymbol, simplificationAttribute
+    , defaultSimplificationPriority
     ) where
 
 import Prelude.Kore
 
+import Data.Maybe
+    ( maybeToList
+    )
 import qualified Generics.SOP as SOP
 import qualified GHC.Generics as GHC
 
 import Kore.Attribute.Parser as Parser
 import Kore.Debug
 
+type SimplificationPriority = Maybe Integer
+
 {- | @Simplification@ represents the @simplification@ attribute for axioms.
+    It takes an optional integer argument which represents the rule's priority.
+    This allows the possibility of ordering the application of simplification rules.
  -}
-newtype Simplification = Simplification { isSimplification :: Bool }
-    deriving (Eq, GHC.Generic, Ord, Show)
+data Simplification
+    = IsSimplification !SimplificationPriority
+    | NotSimplification
+    deriving (Eq, Ord, Show, GHC.Generic)
 
 instance SOP.Generic Simplification
 
@@ -45,7 +55,7 @@ instance Diff Simplification
 instance NFData Simplification
 
 instance Default Simplification where
-    def = Simplification False
+    def = NotSimplification
 
 -- | Kore identifier representing the @simplification@ attribute symbol.
 simplificationId :: Id
@@ -60,11 +70,36 @@ simplificationSymbol =
         }
 
 -- | Kore pattern representing the @simplification@ attribute.
-simplificationAttribute :: AttributePattern
-simplificationAttribute = attributePattern_ simplificationSymbol
+simplificationAttribute :: Maybe Integer -> AttributePattern
+simplificationAttribute priority =
+    attributePattern
+        simplificationSymbol
+        (fmap attributeInteger (maybeToList priority))
+
+defaultSimplificationPriority :: Integer
+defaultSimplificationPriority = 50
 
 instance ParseAttributes Simplification where
-    parseAttribute = parseBoolAttribute simplificationId
+    parseAttribute =
+        withApplication' parseSimplification
+      where
+        parseSimplification params args NotSimplification = do
+            Parser.getZeroParams params
+            arg <- Parser.getZeroOrOneArguments args
+            case arg of
+                Just arg' -> do
+                    stringLiteral <- Parser.getStringLiteral arg'
+                    integer <- Parser.parseInteger stringLiteral
+                    return (IsSimplification (Just integer))
+                Nothing ->
+                    return (IsSimplification Nothing)
+        parseSimplification _ _ _ =
+            failDuplicate'
+
+        withApplication' = Parser.withApplication simplificationId
+        failDuplicate' = Parser.failDuplicate simplificationId
 
 instance From Simplification Attributes where
-    from = toBoolAttributes simplificationAttribute
+    from NotSimplification = def
+    from (IsSimplification maybePriority) =
+        from @AttributePattern (simplificationAttribute maybePriority)

kore/src/Kore/Equation/Equation.hs

@@ -354,10 +354,9 @@ refreshVariables
 
 isSimplificationRule :: Equation variable -> Bool
 isSimplificationRule Equation { attributes } =
-    isSimplification
-  where
-    Attribute.Simplification { isSimplification } =
-        Attribute.simplification attributes
+    case Attribute.simplification attributes of
+        Attribute.IsSimplification _ -> True
+        _ -> False
 
 equationPriority :: Equation variable -> Integer
 equationPriority = Attribute.getPriorityOfAxiom . attributes

kore/src/Kore/Exec.hs

@@ -224,7 +224,10 @@ exec breadthLimit verifiedModule strategy initialTerm =
                 let
                     updateQueue = \as ->
                         Strategy.unfoldDepthFirst as
-                        >=> lift . Strategy.applyBreadthLimit breadthLimit
+                        >=> lift
+                            . Strategy.applyBreadthLimit
+                                breadthLimit
+                                dropStrategy
                     transit instr config =
                         Strategy.transitionRule transitionRule instr config
                         & runTransitionT
@@ -238,6 +241,7 @@ exec breadthLimit verifiedModule strategy initialTerm =
         let finalTerm = forceSort initialSort $ Pattern.toTermLike finalConfig
         return (exitCode, finalTerm)
   where
+    dropStrategy = snd
     -- Get the first final configuration of an execution graph.
     getFinalConfigOf = takeFirstResult >=> orElseBottom
       where

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)
         ]