diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index 14b4f9a465..0daef001fa 100644 --- a/kore/app/exec/Main.hs +++ b/kore/app/exec/Main.hs @@ -367,17 +367,13 @@ parseKoreExecOptions startTime = option (readSum "strategy" strategies) ( metavar "STRATEGY" <> long "strategy" - -- TODO (thomas.tuegel): Make defaultStrategy the default when it - -- works correctly. - <> value ("any", priorityAnyStrategy) + <> value ("all", priorityAllStrategy) <> help "Select rewrites using STRATEGY." ) where strategies = [ ("any", priorityAnyStrategy) , ("all", priorityAllStrategy) - , ("any-heating-cooling", heatingCooling priorityAnyStrategy) - , ("all-heating-cooling", heatingCooling priorityAllStrategy) ] breadth = option auto diff --git a/kore/src/Kore/Attribute/Axiom.hs b/kore/src/Kore/Attribute/Axiom.hs index 761d13e148..d8411d9c3a 100644 --- a/kore/src/Kore/Attribute/Axiom.hs +++ b/kore/src/Kore/Attribute/Axiom.hs @@ -9,7 +9,6 @@ Maintainer : thomas.tuegel@runtimeverification.com module Kore.Attribute.Axiom ( Axiom (..) - , HeatCool (..) , ProductionID (..) , Priority (..) , Owise (..) @@ -61,7 +60,6 @@ import Kore.Attribute.Axiom.Symbolic import Kore.Attribute.Axiom.Unit import Kore.Attribute.Comm import Kore.Attribute.Functional -import Kore.Attribute.HeatCool import Kore.Attribute.Idem import Kore.Attribute.Label import Kore.Attribute.Overload @@ -95,9 +93,7 @@ import qualified SQL -} data Axiom symbol variable = Axiom - { heatCool :: !HeatCool - -- ^ An axiom may be denoted as a heating or cooling rule. - , productionID :: !ProductionID + { productionID :: !ProductionID -- ^ The identifier from the front-end identifying a rule or group of rules. , priority :: !Priority -- ^ A number associated to each rule, @@ -148,8 +144,7 @@ data Axiom symbol variable = instance Default (Axiom symbol variable) where def = Axiom - { heatCool = def - , productionID = def + { productionID = def , priority = def , assoc = def , comm = def @@ -177,8 +172,7 @@ instance where from = mconcat . sequence - [ from . heatCool - , from . productionID + [ from . productionID , from . priority , from . assoc , from . comm @@ -207,9 +201,6 @@ instance From (Axiom symbol variable) PriorityAttributes where , simplificationAttr = simplification } -instance From (Axiom symbol variable) HeatCool where - from Axiom { heatCool } = heatCool - instance SQL.Column (Axiom SymbolOrAlias VariableName) where -- TODO (thomas.tuegel): Use a foreign key. defineColumn tableName _ = @@ -234,8 +225,7 @@ parseAxiomAttribute -> Axiom SymbolOrAlias VariableName -> Parser (Axiom SymbolOrAlias VariableName) parseAxiomAttribute freeVariables attr = - typed @HeatCool (parseAttribute attr) - Monad.>=> typed @ProductionID (parseAttribute attr) + typed @ProductionID (parseAttribute attr) Monad.>=> typed @Priority (parseAttribute attr) Monad.>=> typed @Assoc (parseAttribute attr) Monad.>=> typed @Comm (parseAttribute attr) diff --git a/kore/src/Kore/Attribute/HeatCool.hs b/kore/src/Kore/Attribute/HeatCool.hs deleted file mode 100644 index 9526d8753d..0000000000 --- a/kore/src/Kore/Attribute/HeatCool.hs +++ /dev/null @@ -1,104 +0,0 @@ -{-| -Module : Kore.Attribute.HeatCool -Description : Heating and Cooling axiom attribute -Copyright : (c) Runtime Verification, 2018 -License : NCSA -Maintainer : thomas.tuegel@runtimeverification.com - --} -module Kore.Attribute.HeatCool - ( HeatCool (..) - , heatId, heatSymbol, heatAttribute - , coolId, coolSymbol, coolAttribute - ) where - -import Prelude.Kore - -import Control.Monad - ( (>=>) - ) -import Data.Default -import qualified Generics.SOP as SOP -import qualified GHC.Generics as GHC - -import Kore.Attribute.Parser as Parser -import Kore.Debug - -{- | Denote the heating or cooling phase of execution. - - -} -data HeatCool = Heat | Normal | Cool - deriving (Eq, Ord, Show) - deriving (GHC.Generic) - deriving anyclass (Hashable, NFData) - deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo) - deriving anyclass (Debug, Diff) - -instance Default HeatCool where - def = Normal - --- | Kore identifier representing the @heat@ attribute symbol. -heatId :: Id -heatId = "heat" - --- | Kore symbol representing the @heat@ attribute. -heatSymbol :: SymbolOrAlias -heatSymbol = - SymbolOrAlias - { symbolOrAliasConstructor = heatId - , symbolOrAliasParams = [] - } - --- | Kore pattern representing the @heat@ attribute. -heatAttribute :: AttributePattern -heatAttribute = attributePattern_ heatSymbol - --- | Kore identifier representing the @cool@ attribute symbol. -coolId :: Id -coolId = "cool" - --- | Kore symbol representing the @cool@ attribute. -coolSymbol :: SymbolOrAlias -coolSymbol = - SymbolOrAlias - { symbolOrAliasConstructor = coolId - , symbolOrAliasParams = [] - } - --- | Kore pattern representing the @cool@ attribute. -coolAttribute :: AttributePattern -coolAttribute = attributePattern_ coolSymbol - -instance ParseAttributes HeatCool where - parseAttribute attr = - parseHeat attr >=> parseCool attr - where - parseHeat = - withApplication' $ \params args heatCool -> do - Parser.getZeroParams params - Parser.getZeroArguments args - case heatCool of - Normal -> return Heat - Heat -> failDuplicate' - Cool -> failConflicting' - where - withApplication' = Parser.withApplication heatId - failDuplicate' = Parser.failDuplicate heatId - failConflicting' = Parser.failConflicting [coolId, heatId] - parseCool = - withApplication' $ \params args heatCool -> do - Parser.getZeroParams params - Parser.getZeroArguments args - case heatCool of - Normal -> return Cool - Cool -> failDuplicate' - Heat -> failConflicting' - where - withApplication' = Parser.withApplication coolId - failDuplicate' = Parser.failDuplicate coolId - failConflicting' = Parser.failConflicting [heatId, coolId] - -instance From HeatCool Attributes where - from Heat = from heatAttribute - from Cool = from coolAttribute - from Normal = def diff --git a/kore/src/Kore/Step.hs b/kore/src/Kore/Step.hs index 64902b1421..da794e57fe 100644 --- a/kore/src/Kore/Step.hs +++ b/kore/src/Kore/Step.hs @@ -16,7 +16,6 @@ module Kore.Step , priorityAnyStrategy , TransitionRule , transitionRule - , heatingCooling -- * Re-exports , RulePattern , Natural @@ -46,9 +45,6 @@ import qualified Kore.Step.RewriteStep as Step import Kore.Step.RulePattern ( RewriteRule (..) , RulePattern - , isCoolingRule - , isHeatingRule - , isNormalRule ) import qualified Kore.Step.Simplification.Pattern as Pattern ( simplifyTopConfiguration @@ -171,24 +167,3 @@ priorityAnyStrategy rewrites = anyRewrite sortedRewrites where sortedRewrites = sortOn Attribute.getPriorityOfAxiom rewrites - -{- | Heat the configuration, apply a normal rewrite, and cool the result. - -} --- TODO (thomas.tuegel): This strategy is not right because heating/cooling --- rules must have side conditions if encoded as \rewrites, or they must be --- \equals rules, which are not handled by this strategy. -heatingCooling - :: From rule Attribute.HeatCool - => ([rule] -> Strategy (Prim rule)) - -- ^ 'allRewrites' or 'anyRewrite' - -> [rule] - -> Strategy (Prim rule) -heatingCooling rewriteStrategy rewrites = - Strategy.sequence [Strategy.many heat, normal, Strategy.try cool] - where - heatingRules = filter isHeatingRule rewrites - heat = rewriteStrategy heatingRules - normalRules = filter isNormalRule rewrites - normal = rewriteStrategy normalRules - coolingRules = filter isCoolingRule rewrites - cool = rewriteStrategy coolingRules diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs index 7886967012..8bacc6d185 100644 --- a/kore/src/Kore/Step/ClaimPattern.hs +++ b/kore/src/Kore/Step/ClaimPattern.hs @@ -146,9 +146,6 @@ instance TopBottom ClaimPattern where instance From ClaimPattern Attribute.PriorityAttributes where from = from @(Attribute.Axiom _ _) . attributes -instance From ClaimPattern Attribute.HeatCool where - from = from @(Attribute.Axiom _ _) . attributes - freeVariablesRight :: ClaimPattern -> FreeVariables RewritingVariableName diff --git a/kore/src/Kore/Step/RulePattern.hs b/kore/src/Kore/Step/RulePattern.hs index e7ef72b17e..bef47cc46d 100644 --- a/kore/src/Kore/Step/RulePattern.hs +++ b/kore/src/Kore/Step/RulePattern.hs @@ -14,9 +14,6 @@ module Kore.Step.RulePattern , UnifyingRule (..) , rulePattern , leftPattern - , isHeatingRule - , isCoolingRule - , isNormalRule , applySubstitution , topExistsToImplicitForall , isFreeOf @@ -238,9 +235,6 @@ instance TopBottom (RulePattern variable) where instance From (RulePattern variable) Attribute.PriorityAttributes where from = from @(Attribute.Axiom _ _) . attributes -instance From (RulePattern variable) Attribute.HeatCool where - from = from @(Attribute.Axiom _ _) . attributes - -- | Creates a basic, unconstrained, Equality pattern rulePattern :: InternalVariable variable @@ -271,30 +265,6 @@ leftPattern = where (left, condition) = Pattern.splitTerm pattern' -{- | Does the axiom pattern represent a heating rule? - -} -isHeatingRule :: forall rule. From rule Attribute.HeatCool => rule -> Bool -isHeatingRule rule = - case from @rule @Attribute.HeatCool rule of - Attribute.Heat -> True - _ -> False - -{- | Does the axiom pattern represent a cooling rule? - -} -isCoolingRule :: forall rule. From rule Attribute.HeatCool => rule -> Bool -isCoolingRule rule = - case from @rule @Attribute.HeatCool rule of - Attribute.Cool -> True - _ -> False - -{- | Does the axiom pattern represent a normal rule? - -} -isNormalRule :: forall rule. From rule Attribute.HeatCool => rule -> Bool -isNormalRule rule = - case from @rule @Attribute.HeatCool rule of - Attribute.Normal -> True - _ -> False - -- | Converts the 'RHS' back to the term form. rhsToTerm :: InternalVariable variable @@ -522,9 +492,6 @@ instance instance From (RewriteRule variable) Attribute.PriorityAttributes where from = from @(RulePattern _) . getRewriteRule -instance From (RewriteRule variable) Attribute.HeatCool where - from = from @(RulePattern _) . getRewriteRule - instance TopBottom (RewriteRule variable) where isTop _ = False isBottom _ = False diff --git a/kore/test/Test/Kore/Attribute/HeatCool.hs b/kore/test/Test/Kore/Attribute/HeatCool.hs deleted file mode 100644 index c1de46d640..0000000000 --- a/kore/test/Test/Kore/Attribute/HeatCool.hs +++ /dev/null @@ -1,127 +0,0 @@ -module Test.Kore.Attribute.HeatCool - ( test_heat - , test_heat_Attributes - , test_heat_duplicate - , test_heat_arguments - , test_heat_parameters - , test_cool - , test_cool_Attributes - , test_cool_duplicate - , test_cool_arguments - , test_cool_parameters - , test_conflict - ) where - -import Prelude.Kore - -import Test.Tasty -import Test.Tasty.HUnit - -import Kore.Attribute.HeatCool -import Kore.Syntax.Pattern - -import Test.Kore.Attribute.Parser - -parseHeatCool :: Attributes -> Parser HeatCool -parseHeatCool = parseAttributes - -test_heat :: TestTree -test_heat = - testCase "[heat{}()] :: Heat" - $ expectSuccess Heat - $ parseHeatCool $ Attributes [ heatAttribute ] - -test_heat_Attributes :: TestTree -test_heat_Attributes = - testCase "[heat{}()] :: Attributes" - $ expectSuccess attrs $ parseAttributes attrs - where - attrs = Attributes [ heatAttribute ] - -test_heat_duplicate :: TestTree -test_heat_duplicate = - testCase "[heat{}(), heat{}()]" - $ expectFailure - $ parseHeatCool $ Attributes [ heatAttribute, heatAttribute ] - -test_heat_arguments :: TestTree -test_heat_arguments = - testCase "[heat{}(\"illegal\")]" - $ expectFailure - $ parseHeatCool $ Attributes [ illegalAttribute ] - where - illegalAttribute = attributePattern heatSymbol [attributeString "illegal"] - -test_heat_parameters :: TestTree -test_heat_parameters = - testCase "[heat{illegal}()]" - $ expectFailure - $ parseHeatCool $ Attributes [ illegalAttribute ] - where - illegalAttribute = - (asAttributePattern . ApplicationF) - Application - { applicationSymbolOrAlias = - SymbolOrAlias - { symbolOrAliasConstructor = heatId - , symbolOrAliasParams = - [ SortVariableSort (SortVariable "illegal") ] - } - , applicationChildren = [] - } - -test_cool :: TestTree -test_cool = - testCase "[cool{}()] :: HeatCool" - $ expectSuccess Cool - $ parseHeatCool $ Attributes [ coolAttribute ] - -test_cool_Attributes :: TestTree -test_cool_Attributes = - testCase "[cool{}()] :: Attributes" - $ expectSuccess attrs $ parseAttributes attrs - where - attrs = Attributes [ coolAttribute ] - -test_cool_duplicate :: TestTree -test_cool_duplicate = - testCase "[cool{}(), cool{}()]" - $ expectFailure - $ parseHeatCool $ Attributes [ coolAttribute, coolAttribute ] - -test_cool_arguments :: TestTree -test_cool_arguments = - testCase "[cool{}(\"illegal\")]" - $ expectFailure - $ parseHeatCool $ Attributes [ illegalAttribute ] - where - illegalAttribute = attributePattern coolSymbol [attributeString "illegal"] - -test_cool_parameters :: TestTree -test_cool_parameters = - testCase "[cool{illegal}()]" - $ expectFailure - $ parseHeatCool $ Attributes [ illegalAttribute ] - where - illegalAttribute = - (asAttributePattern . ApplicationF) - Application - { applicationSymbolOrAlias = - SymbolOrAlias - { symbolOrAliasConstructor = coolId - , symbolOrAliasParams = - [ SortVariableSort (SortVariable "illegal") ] - } - , applicationChildren = [] - } - -test_conflict :: TestTree -test_conflict = - testGroup "conflicting attributes" - [ testCase "[heat{}(), cool{}()] :: HeatCool" - $ expectFailure - $ parseHeatCool $ Attributes [ heatAttribute, coolAttribute ] - , testCase "[cool{}(), heat{}()] :: HeatCool" - $ expectFailure - $ parseHeatCool $ Attributes [ coolAttribute, heatAttribute ] - ]