Simplification attribute: parse and use optional priority argument (#1933)

Author: ana-pantilie

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

@@ -151,7 +151,7 @@ anyRewrite rewrites =
     Strategy.any (rewriteStep <$> rewrites)
 
 priorityAllStrategy
-    :: From rewrite (Attribute.Priority, Attribute.Owise)
+    :: From rewrite Attribute.PriorityAttributes
     => [rewrite]
     -> Strategy (Prim rewrite)
 priorityAllStrategy rewrites =
@@ -160,7 +160,7 @@ priorityAllStrategy rewrites =
     priorityGroups = groupSortOn Attribute.getPriorityOfAxiom rewrites
 
 priorityAnyStrategy
-    :: From rewrite (Attribute.Priority, Attribute.Owise)
+    :: From rewrite Attribute.PriorityAttributes
     => [rewrite]
     -> Strategy (Prim rewrite)
 priorityAnyStrategy rewrites =

kore/src/Kore/Step/RulePattern.hs

@@ -248,7 +248,7 @@ instance TopBottom (RulePattern variable) where
     isTop _ = False
     isBottom _ = False
 
-instance From (RulePattern variable) (Attribute.Priority, Attribute.Owise) where
+instance From (RulePattern variable) Attribute.PriorityAttributes where
     from = from @(Attribute.Axiom _ _) . attributes
 
 instance From (RulePattern variable) Attribute.HeatCool where
@@ -542,7 +542,7 @@ instance
     freeVariables (RewriteRule rule) = freeVariables rule
     {-# INLINE freeVariables #-}
 
-instance From (RewriteRule variable) (Attribute.Priority, Attribute.Owise) where
+instance From (RewriteRule variable) Attribute.PriorityAttributes where
     from = from @(RulePattern _) . getRewriteRule
 
 instance From (RewriteRule variable) Attribute.HeatCool where

kore/src/Kore/Strategies/Rule.hs

@@ -18,15 +18,10 @@ import qualified Generics.SOP as SOP
 import qualified GHC.Generics as GHC
 
 import Debug
+import qualified Kore.Attribute.Axiom as Attribute
 import Kore.Attribute.Label as Attribute
     ( Label
     )
-import Kore.Attribute.Owise as Attribute
-    ( Owise
-    )
-import Kore.Attribute.Priority as Attribute
-    ( Priority
-    )
 import Kore.Attribute.RuleIndex as Attribute
     ( RuleIndex
     )
@@ -66,7 +61,7 @@ instance Diff (Rule OnePathRule)
 instance ToRulePattern (Rule OnePathRule) where
     toRulePattern = getRewriteRule . unRewritingRule . unRuleOnePath
 
-instance From (Rule OnePathRule) (Attribute.Priority, Attribute.Owise) where
+instance From (Rule OnePathRule) Attribute.PriorityAttributes where
     from = from @(RewriteRule _) . unRuleOnePath
 
 -- * All-path reachability
@@ -86,7 +81,7 @@ instance Diff (Rule AllPathRule)
 instance ToRulePattern (Rule AllPathRule) where
     toRulePattern = getRewriteRule . unRewritingRule . unRuleAllPath
 
-instance From (Rule AllPathRule) (Attribute.Priority, Attribute.Owise) where
+instance From (Rule AllPathRule) Attribute.PriorityAttributes where
     from = from @(RewriteRule _) . unRuleAllPath
 
 -- * Reachability
@@ -107,8 +102,7 @@ instance Diff (Rule ReachabilityRule)
 instance ToRulePattern (Rule ReachabilityRule) where
     toRulePattern = getRewriteRule . unRewritingRule . unReachabilityRewriteRule
 
-instance From (Rule ReachabilityRule) (Attribute.Priority, Attribute.Owise)
-  where
+instance From (Rule ReachabilityRule) Attribute.PriorityAttributes where
     from = from @(RewriteRule _) . unReachabilityRewriteRule
 
 instance From (Rule ReachabilityRule) Attribute.SourceLocation where

kore/test/Test/Kore/Attribute/Simplification.hs

@@ -1,8 +1,11 @@
 module Test.Kore.Attribute.Simplification
     ( test_simplification
+    , test_simplification_with_argument
     , test_Attributes
+    , test_Attributes_with_argument
     , test_duplicate
-    , test_arguments
+    , test_arguments_wrong_type
+    , test_multiple_arguments
     , test_parameters
     ) where
 
@@ -22,32 +25,56 @@ parseSimplification = parseAttributes
 test_simplification :: TestTree
 test_simplification =
     testCase "[simplification{}()] :: Simplification"
-        $ expectSuccess Simplification { isSimplification = True }
-        $ parseSimplification $ Attributes [ simplificationAttribute ]
+        $ expectSuccess (IsSimplification Nothing)
+        $ parseSimplification $ Attributes [ simplificationAttribute Nothing ]
+
+test_simplification_with_argument :: TestTree
+test_simplification_with_argument =
+    testCase "[simplification{}(\"5\")] :: Simplification"
+        $ expectSuccess (IsSimplification (Just 5))
+        $ parseSimplification $ Attributes [ simplificationAttribute (Just 5) ]
 
 test_Attributes :: TestTree
 test_Attributes =
     testCase "[simplification{}()] :: Attributes"
         $ expectSuccess attrs $ parseAttributes attrs
   where
-    attrs = Attributes [ simplificationAttribute ]
+    attrs = Attributes [ simplificationAttribute Nothing ]
+
+test_Attributes_with_argument :: TestTree
+test_Attributes_with_argument =
+    testCase "[simplification{}(\"5\")] :: Attributes"
+        $ expectSuccess attrs $ parseAttributes attrs
+  where
+    attrs = Attributes [ simplificationAttribute (Just 5) ]
 
 test_duplicate :: TestTree
 test_duplicate =
     testCase "[simplification{}(), simplification{}()]"
         $ expectFailure
         $ parseSimplification
-        $ Attributes [ simplificationAttribute, simplificationAttribute ]
+        $ Attributes [ simplificationAttribute Nothing, simplificationAttribute Nothing ]
 
-test_arguments :: TestTree
-test_arguments =
+test_arguments_wrong_type :: TestTree
+test_arguments_wrong_type =
     testCase "[simplification{}(\"illegal\")]"
         $ expectFailure
         $ parseSimplification $ Attributes [ illegalAttribute ]
   where
     illegalAttribute =
         attributePattern simplificationSymbol [attributeString "illegal"]
 
+test_multiple_arguments :: TestTree
+test_multiple_arguments =
+    testCase "[simplification{}(\"3\", \"26\")]"
+        $ expectFailure
+        $ parseSimplification $ Attributes [ illegalAttributes ]
+  where
+    illegalAttributes =
+        attributePattern
+            simplificationSymbol
+            [ attributeInteger 3, attributeInteger 26 ]
+
 test_parameters :: TestTree
 test_parameters =
     testCase "[simplification{illegal}()]"