From 16ef91d311a2f2a588b12051444c643193b474d3 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Fri, 24 Jul 2020 13:53:51 +0300 Subject: [PATCH 01/27] Add module and datatype ClaimPattern --- kore/src/Kore/Rewriting/RewritingVariable.hs | 3 ++ kore/src/Kore/Step/ClaimPattern.hs | 29 ++++++++++++++++++++ kore/src/Kore/Step/RulePattern.hs | 3 +- 3 files changed, 33 insertions(+), 2 deletions(-) create mode 100644 kore/src/Kore/Step/ClaimPattern.hs diff --git a/kore/src/Kore/Rewriting/RewritingVariable.hs b/kore/src/Kore/Rewriting/RewritingVariable.hs index ffb75aabb9..fb847c73ba 100644 --- a/kore/src/Kore/Rewriting/RewritingVariable.hs +++ b/kore/src/Kore/Rewriting/RewritingVariable.hs @@ -6,6 +6,7 @@ License : NCSA module Kore.Rewriting.RewritingVariable ( RewritingVariableName + , RewritingVariable , isConfigVariable , isRuleVariable , isSomeConfigVariable @@ -123,6 +124,8 @@ instance From VariableName RewritingVariableName where instance FreshName RewritingVariableName +type RewritingVariable = Variable RewritingVariableName + mkElementConfigVariable :: ElementVariable VariableName -> ElementVariable RewritingVariableName diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs new file mode 100644 index 0000000000..85f4db3563 --- /dev/null +++ b/kore/src/Kore/Step/ClaimPattern.hs @@ -0,0 +1,29 @@ +{-| +Copyright : (c) Runtime Verification, 2020 +License : NCSA + +-} + +module Kore.Step.ClaimPattern + ( ClaimPattern (..) + ) where + +import Kore.Internal.OrPattern + ( OrPattern + ) +import Kore.Internal.Pattern + ( Pattern + ) +import Kore.Rewriting.RewritingVariable + ( RewritingVariable + , RewritingVariableName + ) + +-- | Representation of reachability claim types. +data ClaimPattern = + ClaimPattern + { left :: !(Pattern RewritingVariableName) + , existentials :: ![RewritingVariable] + , right :: !(OrPattern RewritingVariableName) + } + diff --git a/kore/src/Kore/Step/RulePattern.hs b/kore/src/Kore/Step/RulePattern.hs index 49adf7ef3c..793e17c3f2 100644 --- a/kore/src/Kore/Step/RulePattern.hs +++ b/kore/src/Kore/Step/RulePattern.hs @@ -197,7 +197,7 @@ topExistsToImplicitForall avoid' RHS { existentials, right, ensures } = (Set.fromList $ mkSomeVariable <$> existentials) subst = TermLike.mkVar <$> rename -{- | Normal rewriting axioms and claims +{- | Normal rewriting axioms -} data RulePattern variable = RulePattern @@ -596,7 +596,6 @@ instance unparse = unparse . implicationRuleToTerm unparse2 = unparse2 . implicationRuleToTerm - {- | One-Path-Claim rule pattern. -} newtype OnePathRule = From 19c1a8bfa630d7c26cf3b28febba7cb7afaf2104 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Fri, 24 Jul 2020 15:17:48 +0300 Subject: [PATCH 02/27] ClaimPattern: onePathRuleToTerm --- kore/src/Kore/Internal/TermLike.hs | 53 ++++++++++ kore/src/Kore/Rewriting/RewritingVariable.hs | 2 + kore/src/Kore/Step/ClaimPattern.hs | 104 +++++++++++++++++++ kore/test/Test/Kore/Step/Rule.hs | 23 ++-- 4 files changed, 171 insertions(+), 11 deletions(-) diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index a2907c1c50..3b537c5e1e 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -45,6 +45,10 @@ module Kore.Internal.TermLike -- * Utility functions for dealing with sorts , forceSort , fullyOverrideSort + -- * Reachability modalities and application + , wEF + , wAF + , applyModality -- * Pure Kore pattern constructors , mkAnd , mkApplyAlias @@ -2002,3 +2006,52 @@ refreshSetBinder -> Binder (SetVariable variable) (TermLike variable) -> Binder (SetVariable variable) (TermLike variable) refreshSetBinder = refreshBinder refreshSetVariable + +-- | Weak exist finally modality symbol +weakExistsFinally :: Text +weakExistsFinally = "weakExistsFinally" + +-- | Weak always finally modality symbol +weakAlwaysFinally :: Text +weakAlwaysFinally = "weakAlwaysFinally" + +-- | 'Alias' construct for weak exist finally +wEF :: Sort -> Alias (TermLike VariableName) +wEF sort = Alias + { aliasConstructor = Id + { getId = weakExistsFinally + , idLocation = AstLocationNone + } + , aliasParams = [sort] + , aliasSorts = ApplicationSorts + { applicationSortsOperands = [sort] + , applicationSortsResult = sort + } + , aliasLeft = [] + , aliasRight = mkTop sort + } + +-- | 'Alias' construct for weak always finally +wAF :: Sort -> Alias (TermLike VariableName) +wAF sort = Alias + { aliasConstructor = Id + { getId = weakAlwaysFinally + , idLocation = AstLocationNone + } + , aliasParams = [sort] + , aliasSorts = ApplicationSorts + { applicationSortsOperands = [sort] + , applicationSortsResult = sort + } + , aliasLeft = [] + , aliasRight = mkTop sort + } + +applyModality + :: (Sort -> Alias (TermLike VariableName)) + -> TermLike VariableName + -> TermLike VariableName +applyModality modality term = + mkApplyAlias (modality sort) [term] + where + sort = termLikeSort term diff --git a/kore/src/Kore/Rewriting/RewritingVariable.hs b/kore/src/Kore/Rewriting/RewritingVariable.hs index fb847c73ba..26d237dd7c 100644 --- a/kore/src/Kore/Rewriting/RewritingVariable.hs +++ b/kore/src/Kore/Rewriting/RewritingVariable.hs @@ -27,6 +27,8 @@ module Kore.Rewriting.RewritingVariable , getResultPattern , getRemainderPredicate , getRemainderPattern + -- * For reachability rule unparsing + , getRewritingVariable ) where import Prelude.Kore diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs index 85f4db3563..25a0206adb 100644 --- a/kore/src/Kore/Step/ClaimPattern.hs +++ b/kore/src/Kore/Step/ClaimPattern.hs @@ -8,22 +8,126 @@ module Kore.Step.ClaimPattern ( ClaimPattern (..) ) where +import Prelude.Kore + +import Control.DeepSeq + ( NFData + ) +import qualified Generics.SOP as SOP +import qualified GHC.Generics as GHC + +import qualified Kore.Attribute.Axiom as Attribute +import Kore.Debug import Kore.Internal.OrPattern ( OrPattern ) +import qualified Kore.Internal.OrPattern as OrPattern import Kore.Internal.Pattern ( Pattern ) +import qualified Kore.Internal.Pattern as Pattern +import Kore.Internal.Symbol + ( Symbol + ) +import Kore.Internal.TermLike + ( TermLike + , VariableName + ) +import qualified Kore.Internal.TermLike as TermLike import Kore.Rewriting.RewritingVariable ( RewritingVariable , RewritingVariableName + , getRewritingVariable + ) +import Kore.TopBottom + ( TopBottom (..) + ) +import Kore.Unparser + ( Unparse (..) ) +import qualified Pretty + -- | Representation of reachability claim types. data ClaimPattern = ClaimPattern { left :: !(Pattern RewritingVariableName) , existentials :: ![RewritingVariable] , right :: !(OrPattern RewritingVariableName) + , attributes :: !(Attribute.Axiom Symbol RewritingVariableName) } + deriving (Eq, Ord, Show) + deriving (GHC.Generic) + +instance NFData ClaimPattern + +instance SOP.Generic ClaimPattern + +instance SOP.HasDatatypeInfo ClaimPattern + +instance Debug ClaimPattern + +instance Diff ClaimPattern + +-- | One-Path-Claim claim pattern. +newtype OnePathRule = + OnePathRule { getOnePathRule :: ClaimPattern } + deriving (Eq, GHC.Generic, Ord, Show) + +instance NFData OnePathRule + +instance SOP.Generic OnePathRule + +instance SOP.HasDatatypeInfo OnePathRule + +instance Debug OnePathRule + +instance Diff OnePathRule + +-- | Converts a 'OnePathRule' into its term representation. +-- This is intended to be used only in unparsing situations, +-- as some of the variable information related to the +-- rewriting algorithm is lost. +onePathRuleToTerm :: OnePathRule -> TermLike VariableName +onePathRuleToTerm (OnePathRule representation@(ClaimPattern _ _ _ _)) = + TermLike.mkImplies leftPattern (wEF rightPattern) + where + ClaimPattern { left, right } = representation + leftPattern = + Pattern.toTermLike left + & TermLike.mapVariables getRewritingVariable + rightPattern = + OrPattern.toTermLike right + & TermLike.mapVariables getRewritingVariable + wEF = TermLike.applyModality TermLike.wEF + +instance Unparse OnePathRule where + unparse claimPattern = + "claim {}" + <> Pretty.line' + <> Pretty.nest 4 + (unparse $ onePathRuleToTerm claimPattern) + <> Pretty.line' + <> "[]" + + unparse2 claimPattern = + "claim {}" + Pretty.<+> + unparse2 (onePathRuleToTerm claimPattern) + Pretty.<+> "[]" + +instance TopBottom OnePathRule where + isTop _ = False + isBottom _ = False + +instance From OnePathRule Attribute.SourceLocation where + from = Attribute.sourceLocation . attributes . getOnePathRule + +instance From OnePathRule Attribute.Label where + from = Attribute.label . attributes . getOnePathRule + +instance From OnePathRule Attribute.RuleIndex where + from = Attribute.identifier . attributes . getOnePathRule +instance From OnePathRule Attribute.Trusted where + from = Attribute.trusted . attributes . getOnePathRule diff --git a/kore/test/Test/Kore/Step/Rule.hs b/kore/test/Test/Kore/Step/Rule.hs index 5713f620c0..d187fe71fa 100644 --- a/kore/test/Test/Kore/Step/Rule.hs +++ b/kore/test/Test/Kore/Step/Rule.hs @@ -36,7 +36,10 @@ import Kore.Internal.ApplicationSorts import qualified Kore.Internal.Predicate as Predicate import Kore.Internal.TermLike import Kore.Step.Rule -import Kore.Step.RulePattern +import Kore.Step.RulePattern hiding + ( wAF + , wEF + ) import Kore.Syntax.Definition hiding ( Alias (..) ) @@ -246,12 +249,11 @@ test_patternToAxiomPatternAndBack = testGroup "pattern to axiomPattern to pattern" [ - let op = wEF $ termLikeSort leftP - initialPattern = mkImplies + let initialPattern = mkImplies (mkAnd (Predicate.unwrapPredicate requiresP) leftP) - (mkApplyAlias - op - [mkAnd (Predicate.unwrapPredicate ensuresP) rightP] + (applyModality + wEF + (mkAnd (Predicate.unwrapPredicate ensuresP) rightP) ) in testCase "Reachability claim wEF" $ @@ -259,12 +261,11 @@ test_patternToAxiomPatternAndBack = (Right initialPattern) (perhapsFinalPattern def initialPattern) , - let op = wAF $ termLikeSort leftP - initialPattern = mkImplies + let initialPattern = mkImplies (mkAnd (Predicate.unwrapPredicate requiresP) leftP) - (mkApplyAlias - op - [mkAnd (Predicate.unwrapPredicate ensuresP) rightP] + (applyModality + wAF + (mkAnd (Predicate.unwrapPredicate ensuresP) rightP) ) in testCase "Reachability claim wAF" $ From 0d9cf80e5ebf29dd6789204bc9b9183831a68100 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Fri, 24 Jul 2020 15:58:50 +0300 Subject: [PATCH 03/27] ClaimPattern: allPathRuleToTerm --- kore/src/Kore/Internal/TermLike.hs | 19 ++++--- kore/src/Kore/Step/ClaimPattern.hs | 87 +++++++++++++++++++++++++----- 2 files changed, 87 insertions(+), 19 deletions(-) diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index 3b537c5e1e..2838b63712 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -46,6 +46,7 @@ module Kore.Internal.TermLike , forceSort , fullyOverrideSort -- * Reachability modalities and application + , Modality , wEF , wAF , applyModality @@ -2007,16 +2008,18 @@ refreshSetBinder -> Binder (SetVariable variable) (TermLike variable) refreshSetBinder = refreshBinder refreshSetVariable --- | Weak exist finally modality symbol +type Modality = Sort -> Alias (TermLike VariableName) + +-- | Weak exists finally modality symbol. weakExistsFinally :: Text weakExistsFinally = "weakExistsFinally" --- | Weak always finally modality symbol +-- | Weak always finally modality symbol. weakAlwaysFinally :: Text weakAlwaysFinally = "weakAlwaysFinally" --- | 'Alias' construct for weak exist finally -wEF :: Sort -> Alias (TermLike VariableName) +-- | 'Alias' construct for weak exist finally. +wEF :: Modality wEF sort = Alias { aliasConstructor = Id { getId = weakExistsFinally @@ -2031,8 +2034,8 @@ wEF sort = Alias , aliasRight = mkTop sort } --- | 'Alias' construct for weak always finally -wAF :: Sort -> Alias (TermLike VariableName) +-- | 'Alias' construct for weak always finally. +wAF :: Modality wAF sort = Alias { aliasConstructor = Id { getId = weakAlwaysFinally @@ -2047,8 +2050,10 @@ wAF sort = Alias , aliasRight = mkTop sort } +-- | Apply one of the reachability modality aliases +-- to a term. applyModality - :: (Sort -> Alias (TermLike VariableName)) + :: Modality -> TermLike VariableName -> TermLike VariableName applyModality modality term = diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs index 25a0206adb..d88f7480d5 100644 --- a/kore/src/Kore/Step/ClaimPattern.hs +++ b/kore/src/Kore/Step/ClaimPattern.hs @@ -30,7 +30,8 @@ import Kore.Internal.Symbol ( Symbol ) import Kore.Internal.TermLike - ( TermLike + ( Modality + , TermLike , VariableName ) import qualified Kore.Internal.TermLike as TermLike @@ -69,6 +70,23 @@ instance Debug ClaimPattern instance Diff ClaimPattern +claimPatternToTerm + :: Modality + -> ClaimPattern + -> TermLike VariableName +claimPatternToTerm modality representation@(ClaimPattern _ _ _ _) = + TermLike.mkImplies + leftPattern + (TermLike.applyModality modality rightPattern) + where + ClaimPattern { left, right } = representation + leftPattern = + Pattern.toTermLike left + & TermLike.mapVariables getRewritingVariable + rightPattern = + OrPattern.toTermLike right + & TermLike.mapVariables getRewritingVariable + -- | One-Path-Claim claim pattern. newtype OnePathRule = OnePathRule { getOnePathRule :: ClaimPattern } @@ -89,17 +107,8 @@ instance Diff OnePathRule -- as some of the variable information related to the -- rewriting algorithm is lost. onePathRuleToTerm :: OnePathRule -> TermLike VariableName -onePathRuleToTerm (OnePathRule representation@(ClaimPattern _ _ _ _)) = - TermLike.mkImplies leftPattern (wEF rightPattern) - where - ClaimPattern { left, right } = representation - leftPattern = - Pattern.toTermLike left - & TermLike.mapVariables getRewritingVariable - rightPattern = - OrPattern.toTermLike right - & TermLike.mapVariables getRewritingVariable - wEF = TermLike.applyModality TermLike.wEF +onePathRuleToTerm (OnePathRule claimPattern) = + claimPatternToTerm TermLike.wEF claimPattern instance Unparse OnePathRule where unparse claimPattern = @@ -131,3 +140,57 @@ instance From OnePathRule Attribute.RuleIndex where instance From OnePathRule Attribute.Trusted where from = Attribute.trusted . attributes . getOnePathRule + +{- | All-Path-Claim rule pattern. +-} +newtype AllPathRule = + AllPathRule { getAllPathRule :: ClaimPattern } + deriving (Eq, GHC.Generic, Ord, Show) + +instance NFData AllPathRule + +instance SOP.Generic AllPathRule + +instance SOP.HasDatatypeInfo AllPathRule + +instance Debug AllPathRule + +instance Diff AllPathRule + +instance Unparse AllPathRule where + unparse claimPattern = + "claim {}" + <> Pretty.line' + <> Pretty.nest 4 + (unparse $ allPathRuleToTerm claimPattern) + <> Pretty.line' + <> "[]" + unparse2 claimPattern = + "claim {}" + Pretty.<+> + unparse2 (allPathRuleToTerm claimPattern) + Pretty.<+> "[]" + +instance TopBottom AllPathRule where + isTop _ = False + isBottom _ = False + +instance From AllPathRule Attribute.SourceLocation where + from = Attribute.sourceLocation . attributes . getAllPathRule + +instance From AllPathRule Attribute.Label where + from = Attribute.label . attributes . getAllPathRule + +instance From AllPathRule Attribute.RuleIndex where + from = Attribute.identifier . attributes . getAllPathRule + +instance From AllPathRule Attribute.Trusted where + from = Attribute.trusted . attributes . getAllPathRule + +-- | Converts a 'OnePathRule' into its term representation. +-- This is intended to be used only in unparsing situations, +-- as some of the variable information related to the +-- rewriting algorithm is lost. +allPathRuleToTerm :: AllPathRule -> TermLike VariableName +allPathRuleToTerm (AllPathRule claimPattern) = + claimPatternToTerm TermLike.wAF claimPattern From 6cf54feeeaadfcf47fee553e2a0170d5fa78870c Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Fri, 24 Jul 2020 16:21:15 +0300 Subject: [PATCH 04/27] ClaimPattern: add missing instances --- kore/src/Kore/Step/ClaimPattern.hs | 44 ++++++++++++++++++++++++++++-- 1 file changed, 41 insertions(+), 3 deletions(-) diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs index d88f7480d5..99dc4fa18c 100644 --- a/kore/src/Kore/Step/ClaimPattern.hs +++ b/kore/src/Kore/Step/ClaimPattern.hs @@ -47,6 +47,9 @@ import Kore.Unparser ( Unparse (..) ) +import Pretty + ( Pretty (..) + ) import qualified Pretty -- | Representation of reachability claim types. @@ -70,6 +73,42 @@ instance Debug ClaimPattern instance Diff ClaimPattern +instance From ClaimPattern Attribute.SourceLocation where + from = Attribute.sourceLocation . attributes + +instance From ClaimPattern Attribute.Label where + from = Attribute.label . attributes + +instance From ClaimPattern Attribute.RuleIndex where + from = Attribute.identifier . attributes + +instance Pretty ClaimPattern where + pretty claimPattern'@(ClaimPattern _ _ _ _) = + Pretty.vsep + [ "left:" + , Pretty.indent 4 (unparse left) + , "existentials:" + , Pretty.indent 4 (Pretty.list $ unparse <$> existentials) + , "right:" + , Pretty.indent 4 (unparse $ OrPattern.toTermLike right) + ] + where + ClaimPattern + { left + , right + , existentials + } = claimPattern' + +instance TopBottom ClaimPattern where + isTop _ = False + isBottom _ = False + +instance From ClaimPattern Attribute.PriorityAttributes where + from = from @(Attribute.Axiom _ _) . attributes + +instance From ClaimPattern Attribute.HeatCool where + from = from @(Attribute.Axiom _ _) . attributes + claimPatternToTerm :: Modality -> ClaimPattern @@ -141,8 +180,7 @@ instance From OnePathRule Attribute.RuleIndex where instance From OnePathRule Attribute.Trusted where from = Attribute.trusted . attributes . getOnePathRule -{- | All-Path-Claim rule pattern. --} +-- | All-Path-Claim claim pattern. newtype AllPathRule = AllPathRule { getAllPathRule :: ClaimPattern } deriving (Eq, GHC.Generic, Ord, Show) @@ -187,7 +225,7 @@ instance From AllPathRule Attribute.RuleIndex where instance From AllPathRule Attribute.Trusted where from = Attribute.trusted . attributes . getAllPathRule --- | Converts a 'OnePathRule' into its term representation. +-- | Converts a 'AllPathRule' into its term representation. -- This is intended to be used only in unparsing situations, -- as some of the variable information related to the -- rewriting algorithm is lost. From 6bfe65ddc9e4e16cbe27ff20ce34b6c97c40744c Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Fri, 24 Jul 2020 16:39:02 +0300 Subject: [PATCH 05/27] ClaimPattern: ReachabilityRule --- kore/src/Kore/Step/ClaimPattern.hs | 67 +++++++++++++++++++++++++++++- 1 file changed, 65 insertions(+), 2 deletions(-) diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs index 99dc4fa18c..43dd2932bf 100644 --- a/kore/src/Kore/Step/ClaimPattern.hs +++ b/kore/src/Kore/Step/ClaimPattern.hs @@ -6,6 +6,7 @@ License : NCSA module Kore.Step.ClaimPattern ( ClaimPattern (..) + , toSentence ) where import Prelude.Kore @@ -13,6 +14,7 @@ import Prelude.Kore import Control.DeepSeq ( NFData ) +import qualified Data.Default as Default import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC @@ -40,12 +42,14 @@ import Kore.Rewriting.RewritingVariable , RewritingVariableName , getRewritingVariable ) +import qualified Kore.Syntax.Definition as Syntax import Kore.TopBottom ( TopBottom (..) ) import Kore.Unparser ( Unparse (..) ) +import qualified Kore.Verified as Verified import Pretty ( Pretty (..) @@ -60,8 +64,7 @@ data ClaimPattern = , right :: !(OrPattern RewritingVariableName) , attributes :: !(Attribute.Axiom Symbol RewritingVariableName) } - deriving (Eq, Ord, Show) - deriving (GHC.Generic) + deriving (Eq, Ord, Show, GHC.Generic) instance NFData ClaimPattern @@ -232,3 +235,63 @@ instance From AllPathRule Attribute.Trusted where allPathRuleToTerm :: AllPathRule -> TermLike VariableName allPathRuleToTerm (AllPathRule claimPattern) = claimPatternToTerm TermLike.wAF claimPattern + +-- | Unified One-Path and All-Path claim pattern. +data ReachabilityRule + = OnePath !OnePathRule + | AllPath !AllPathRule + deriving (Eq, GHC.Generic, Ord, Show) + +instance NFData ReachabilityRule + +instance SOP.Generic ReachabilityRule + +instance SOP.HasDatatypeInfo ReachabilityRule + +instance Debug ReachabilityRule + +instance Diff ReachabilityRule + +instance Unparse ReachabilityRule where + unparse (OnePath rule) = unparse rule + unparse (AllPath rule) = unparse rule + unparse2 (AllPath rule) = unparse2 rule + unparse2 (OnePath rule) = unparse2 rule + +instance TopBottom ReachabilityRule where + isTop _ = False + isBottom _ = False + +instance Pretty ReachabilityRule where + pretty (OnePath (OnePathRule rule)) = + Pretty.vsep ["One-Path reachability rule:", Pretty.pretty rule] + pretty (AllPath (AllPathRule rule)) = + Pretty.vsep ["All-Path reachability rule:", Pretty.pretty rule] + +instance From ReachabilityRule Attribute.SourceLocation where + from (OnePath onePathRule) = from onePathRule + from (AllPath allPathRule) = from allPathRule + +instance From ReachabilityRule Attribute.Label where + from (OnePath onePathRule) = from onePathRule + from (AllPath allPathRule) = from allPathRule + +instance From ReachabilityRule Attribute.RuleIndex where + from (OnePath onePathRule) = from onePathRule + from (AllPath allPathRule) = from allPathRule + +instance From ReachabilityRule Attribute.Trusted where + from (OnePath onePathRule) = from onePathRule + from (AllPath allPathRule) = from allPathRule + +toSentence :: ReachabilityRule -> Verified.Sentence +toSentence rule = + Syntax.SentenceClaimSentence $ Syntax.SentenceClaim Syntax.SentenceAxiom + { sentenceAxiomParameters = [] + , sentenceAxiomPattern = patt + , sentenceAxiomAttributes = Default.def + } + where + patt = case rule of + OnePath rule' -> onePathRuleToTerm rule' + AllPath rule' -> allPathRuleToTerm rule' From 3fac67a3c8fe40ec63663bc670b126634c4cb17b Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Mon, 27 Jul 2020 11:17:04 +0300 Subject: [PATCH 06/27] ClaimPattern: FreeVariables --- kore/src/Kore/Step/ClaimPattern.hs | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs index 43dd2932bf..5faf484eeb 100644 --- a/kore/src/Kore/Step/ClaimPattern.hs +++ b/kore/src/Kore/Step/ClaimPattern.hs @@ -19,6 +19,9 @@ import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC import qualified Kore.Attribute.Axiom as Attribute +import Kore.Attribute.Pattern.FreeVariables + ( HasFreeVariables (..) + ) import Kore.Debug import Kore.Internal.OrPattern ( OrPattern @@ -112,6 +115,13 @@ instance From ClaimPattern Attribute.PriorityAttributes where instance From ClaimPattern Attribute.HeatCool where from = from @(Attribute.Axiom _ _) . attributes +instance HasFreeVariables ClaimPattern RewritingVariableName where + freeVariables claimPattern'@(ClaimPattern _ _ _ _) = + freeVariables left + <> freeVariables (OrPattern.toPattern right) + where + ClaimPattern { left, right } = claimPattern' + claimPatternToTerm :: Modality -> ClaimPattern From 5faacd32933a8f962229e74873c794c0b98f753d Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Mon, 27 Jul 2020 12:18:47 +0300 Subject: [PATCH 07/27] Rule.Expand: update to ClaimPattern --- kore/src/Kore/Internal/OrPattern.hs | 12 ++++ kore/src/Kore/Step/ClaimPattern.hs | 8 ++- kore/src/Kore/Step/Rule/Expand.hs | 85 +++++++++++++++-------------- kore/src/Kore/Step/RulePattern.hs | 3 - 4 files changed, 63 insertions(+), 45 deletions(-) diff --git a/kore/src/Kore/Internal/OrPattern.hs b/kore/src/Kore/Internal/OrPattern.hs index 2381490ffc..d4d8832610 100644 --- a/kore/src/Kore/Internal/OrPattern.hs +++ b/kore/src/Kore/Internal/OrPattern.hs @@ -20,6 +20,7 @@ module Kore.Internal.OrPattern , toPattern , toTermLike , targetBinder + , substitute , MultiOr.flatten , MultiOr.filterOr , MultiOr.gather @@ -29,6 +30,9 @@ module Kore.Internal.OrPattern import Prelude.Kore import qualified Data.Foldable as Foldable +import Data.Map.Strict + ( Map + ) import Kore.Internal.Condition ( Condition @@ -219,3 +223,11 @@ targetBinder Binder { binderVariable, binderChild } = { binderVariable = newVar , binderChild = newChild } + +substitute + :: InternalVariable variable + => Map (SomeVariableName variable) (TermLike variable) + -> OrPattern variable + -> OrPattern variable +substitute subst = + fromPatterns . fmap (Pattern.substitute subst) . toPatterns diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs index 5faf484eeb..74f5bd78e9 100644 --- a/kore/src/Kore/Step/ClaimPattern.hs +++ b/kore/src/Kore/Step/ClaimPattern.hs @@ -6,6 +6,9 @@ License : NCSA module Kore.Step.ClaimPattern ( ClaimPattern (..) + , OnePathRule (..) + , AllPathRule (..) + , ReachabilityRule (..) , toSentence ) where @@ -35,7 +38,8 @@ import Kore.Internal.Symbol ( Symbol ) import Kore.Internal.TermLike - ( Modality + ( ElementVariable + , Modality , TermLike , VariableName ) @@ -63,7 +67,7 @@ import qualified Pretty data ClaimPattern = ClaimPattern { left :: !(Pattern RewritingVariableName) - , existentials :: ![RewritingVariable] + , existentials :: ![ElementVariable RewritingVariableName] , right :: !(OrPattern RewritingVariableName) , attributes :: !(Attribute.Axiom Symbol RewritingVariableName) } diff --git a/kore/src/Kore/Step/Rule/Expand.hs b/kore/src/Kore/Step/Rule/Expand.hs index 9612b109aa..dbf3c06fac 100644 --- a/kore/src/Kore/Step/Rule/Expand.hs +++ b/kore/src/Kore/Step/Rule/Expand.hs @@ -46,6 +46,9 @@ import Kore.IndexedModule.MetadataTools ( SmtMetadataTools , findSortConstructors ) +import qualified Kore.Internal.Condition as Condition +import qualified Kore.Internal.OrPattern as OrPattern +import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.Predicate ( makeAndPredicate ) @@ -59,6 +62,9 @@ import Kore.Internal.TermLike import qualified Kore.Internal.TermLike as TermLike ( substitute ) +import Kore.Rewriting.RewritingVariable + ( RewritingVariableName + ) import Kore.Sort ( Sort (..) , SortActual (SortActual) @@ -67,13 +73,12 @@ import qualified Kore.Sort as Sort.DoNotUse import qualified Kore.Step.AntiLeft as AntiLeft ( substitute ) -import Kore.Step.RulePattern +import Kore.Step.ClaimPattern ( AllPathRule (..) + , ClaimPattern (..) , OnePathRule (..) , ReachabilityRule (..) - , RulePattern (RulePattern) ) -import qualified Kore.Step.RulePattern as RulePattern import Kore.Syntax.Variable import Kore.Variables.Fresh ( refreshVariable @@ -91,24 +96,25 @@ class ExpandSingleConstructors rule where -> rule -> rule -instance ExpandSingleConstructors (RulePattern VariableName) where +instance ExpandSingleConstructors ClaimPattern where expandSingleConstructors metadataTools - rule@(RulePattern _ _ _ _ _) + rule@(ClaimPattern _ _ _ _) = case rule of - RulePattern - {left, antiLeft, requires - , rhs = RulePattern.RHS {existentials, right, ensures} + ClaimPattern + { left + , existentials + , right } -> - let leftVariables :: [ElementVariable VariableName] + let leftVariables :: [ElementVariable RewritingVariableName] leftVariables = mapMaybe retractElementVariable $ FreeVariables.toList $ freeVariables left - allSomeVariables :: Set (SomeVariable VariableName) + allSomeVariables :: Set (SomeVariable RewritingVariableName) allSomeVariables = FreeVariables.toSet (freeVariables rule) - allElementVariables :: Set (ElementVariableName VariableName) + allElementVariables :: Set (ElementVariableName RewritingVariableName) allElementVariables = Set.fromList $ map variableName @@ -116,8 +122,8 @@ instance ExpandSingleConstructors (RulePattern VariableName) where ++ existentials expansion :: Map.Map - (SomeVariable VariableName) - (TermLike VariableName) + (SomeVariable RewritingVariableName) + (TermLike RewritingVariableName) expansion = expandVariables metadataTools @@ -131,18 +137,12 @@ instance ExpandSingleConstructors (RulePattern VariableName) where (Map.toList expansion) subst = Map.mapKeys variableName expansion in rule - { RulePattern.left = TermLike.substitute subst left - , RulePattern.antiLeft = - AntiLeft.substitute subst <$> antiLeft - , RulePattern.requires = - makeAndPredicate - (Predicate.substitute subst requires) - substitutionPredicate - , RulePattern.rhs = RulePattern.RHS - { existentials - , right = TermLike.substitute subst right - , ensures = Predicate.substitute subst ensures - } + { left = + Pattern.andCondition + (Pattern.substitute subst left) + (Condition.fromPredicate substitutionPredicate) + , existentials + , right = OrPattern.substitute subst right } instance ExpandSingleConstructors OnePathRule where @@ -169,8 +169,13 @@ instance ExpandSingleConstructors ReachabilityRule where data Expansion = Expansion - { substitution :: !(Map (SomeVariable VariableName) (TermLike VariableName)) - , stale :: !(Set (ElementVariableName VariableName)) + { substitution + :: !( Map + (SomeVariable RewritingVariableName) + (TermLike RewritingVariableName) + ) + , stale + :: !(Set (ElementVariableName RewritingVariableName)) } deriving (GHC.Generic) @@ -178,15 +183,15 @@ type Expander = State Expansion expandVariables :: SmtMetadataTools attributes - -> [ElementVariable VariableName] - -> Set (ElementVariableName VariableName) - -> Map (SomeVariable VariableName) (TermLike VariableName) + -> [ElementVariable RewritingVariableName] + -> Set (ElementVariableName RewritingVariableName) + -> Map (SomeVariable RewritingVariableName) (TermLike RewritingVariableName) expandVariables metadataTools variables stale = traverse expandAddVariable variables & flip execState Expansion { substitution = Map.empty, stale } & substitution where - expandAddVariable :: ElementVariable VariableName -> Expander () + expandAddVariable :: ElementVariable RewritingVariableName -> Expander () expandAddVariable variable = do term <- expandVariable metadataTools variable Monad.unless @@ -195,17 +200,17 @@ expandVariables metadataTools variables stale = expandVariable :: SmtMetadataTools attributes - -> ElementVariable VariableName - -> Expander (TermLike VariableName) + -> ElementVariable RewritingVariableName + -> Expander (TermLike RewritingVariableName) expandVariable metadataTools variable@Variable { variableSort } = expandSort metadataTools variable UseDirectly variableSort expandSort :: SmtMetadataTools attributes - -> ElementVariable VariableName + -> ElementVariable RewritingVariableName -> VariableUsage -> Sort - -> Expander (TermLike VariableName) + -> Expander (TermLike RewritingVariableName) expandSort metadataTools defaultVariable variableUsage sort = case findSingleConstructor sort of Just constructor -> @@ -225,9 +230,9 @@ expandSort metadataTools defaultVariable variableUsage sort = expandConstructor :: SmtMetadataTools attributes - -> ElementVariable VariableName + -> ElementVariable RewritingVariableName -> Attribute.Constructors.Constructor - -> Expander (TermLike VariableName) + -> Expander (TermLike RewritingVariableName) expandConstructor metadataTools defaultVariable @@ -235,7 +240,7 @@ expandConstructor = mkApplySymbol symbol <$> traverse expandChildSort sorts where - expandChildSort :: Sort -> Expander (TermLike VariableName) + expandChildSort :: Sort -> Expander (TermLike RewritingVariableName) expandChildSort = expandSort metadataTools defaultVariable UseAsPrototype {-| Context: we have a TermLike that contains a variables, and we @@ -262,10 +267,10 @@ data VariableUsage = maybeNewVariable :: HasCallStack - => ElementVariable VariableName + => ElementVariable RewritingVariableName -> Sort -> VariableUsage - -> Expander (TermLike VariableName) + -> Expander (TermLike RewritingVariableName) maybeNewVariable variable@Variable { variableSort } sort diff --git a/kore/src/Kore/Step/RulePattern.hs b/kore/src/Kore/Step/RulePattern.hs index 793e17c3f2..4a4fddcb9a 100644 --- a/kore/src/Kore/Step/RulePattern.hs +++ b/kore/src/Kore/Step/RulePattern.hs @@ -8,9 +8,6 @@ License : NCSA module Kore.Step.RulePattern ( RulePattern (..) , RewriteRule (..) - , OnePathRule (..) - , AllPathRule (..) - , ReachabilityRule (..) , ImplicationRule (..) , RHS (..) , HasAttributes (..) From 256c30f870f5977c8dfbee51ced782a6057ac7fe Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Mon, 27 Jul 2020 13:38:16 +0300 Subject: [PATCH 08/27] Rule.Simplify: add functionality for ClaimPattern --- kore/src/Kore/Step/ClaimPattern.hs | 78 +++++++++++++++++++++++++++++ kore/src/Kore/Step/Rule/Simplify.hs | 68 +++++++++++++++++++------ 2 files changed, 131 insertions(+), 15 deletions(-) diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs index 74f5bd78e9..ce68f188fa 100644 --- a/kore/src/Kore/Step/ClaimPattern.hs +++ b/kore/src/Kore/Step/ClaimPattern.hs @@ -10,6 +10,7 @@ module Kore.Step.ClaimPattern , AllPathRule (..) , ReachabilityRule (..) , toSentence + , applySubstitution ) where import Prelude.Kore @@ -18,6 +19,11 @@ import Control.DeepSeq ( NFData ) import qualified Data.Default as Default +import Data.Map.Strict + ( Map + ) +import qualified Data.Map.Strict as Map +import qualified Data.Set as Set import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC @@ -25,6 +31,7 @@ import qualified Kore.Attribute.Axiom as Attribute import Kore.Attribute.Pattern.FreeVariables ( HasFreeVariables (..) ) +import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables import Kore.Debug import Kore.Internal.OrPattern ( OrPattern @@ -34,12 +41,18 @@ import Kore.Internal.Pattern ( Pattern ) import qualified Kore.Internal.Pattern as Pattern +import Kore.Internal.Substitution + ( Substitution + ) +import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.Symbol ( Symbol ) import Kore.Internal.TermLike ( ElementVariable , Modality + , SomeVariable + , SomeVariableName (..) , TermLike , VariableName ) @@ -143,6 +156,71 @@ claimPatternToTerm modality representation@(ClaimPattern _ _ _ _) = OrPattern.toTermLike right & TermLike.mapVariables getRewritingVariable +substituteRight + :: Map + (SomeVariableName RewritingVariableName) + (TermLike RewritingVariableName) + -> ClaimPattern + -> ClaimPattern +substituteRight subst claimPattern'@ClaimPattern { right, existentials } = + claimPattern' + { right = OrPattern.substitute subst' right + } + where + subst' = + foldr + ( Map.delete + . inject + . TermLike.variableName + ) + subst + existentials + +-- | Apply the substitution to the claim. +substitute + :: Map + (SomeVariableName RewritingVariableName) + (TermLike RewritingVariableName) + -> ClaimPattern + -> ClaimPattern +substitute subst claimPattern'@(ClaimPattern _ _ _ _) = + substituteRight subst + $ claimPattern' + { left = Pattern.substitute subst left + } + where + ClaimPattern { left, right, existentials } = claimPattern' + +-- | Applies a substitution to a claim and checks that +-- it was fully applied, i.e. there is no substitution +-- variable left in the claim. +applySubstitution + :: HasCallStack + => Substitution RewritingVariableName + -> ClaimPattern + -> ClaimPattern +applySubstitution substitution claim = + if finalClaim `isFreeOf` substitutedVariables + then finalClaim + else error + ( "Substituted variables not removed from the rule, cannot throw " + ++ "substitution away." + ) + where + subst = Substitution.toMap substitution + finalClaim = substitute subst claim + substitutedVariables = Substitution.variables substitution + +-- |Is the rule free of the given variables? +isFreeOf + :: ClaimPattern + -> Set.Set (SomeVariable RewritingVariableName) + -> Bool +isFreeOf rule = + Set.disjoint + $ FreeVariables.toSet + $ freeVariables rule + -- | One-Path-Claim claim pattern. newtype OnePathRule = OnePathRule { getOnePathRule :: ClaimPattern } diff --git a/kore/src/Kore/Step/Rule/Simplify.hs b/kore/src/Kore/Step/Rule/Simplify.hs index 870c2fad31..d93f6e061c 100644 --- a/kore/src/Kore/Step/Rule/Simplify.hs +++ b/kore/src/Kore/Step/Rule/Simplify.hs @@ -14,6 +14,7 @@ import Control.Monad ( (>=>) ) +import qualified Kore.Internal.Condition as Condition import Kore.Internal.Conditional ( Conditional (Conditional) ) @@ -37,11 +38,18 @@ import qualified Kore.Internal.Predicate as Predicate import Kore.Internal.TermLike ( termLikeSort ) -import Kore.Step.RulePattern +import Kore.Rewriting.RewritingVariable + ( RewritingVariableName + ) +import Kore.Step.ClaimPattern ( AllPathRule (..) + , ClaimPattern (ClaimPattern) , OnePathRule (..) , ReachabilityRule (..) - , RewriteRule (..) + ) +import qualified Kore.Step.ClaimPattern as ClaimPattern +import Kore.Step.RulePattern + ( RewriteRule (..) , RulePattern (RulePattern) ) import qualified Kore.Step.RulePattern as RulePattern @@ -63,7 +71,7 @@ import Logic ) import qualified Logic --- | Simplifies the left-hand-side of a rule/claim +-- | Simplifies the left-hand-side of a rewrite rule (claim or axiom) class SimplifyRuleLHS rule where simplifyRuleLhs :: forall simplifier @@ -101,6 +109,36 @@ instance InternalVariable variable => SimplifyRuleLHS (RulePattern variable) $ makeAndPredicate predicate requires' } +instance SimplifyRuleLHS ClaimPattern + where + simplifyRuleLhs rule@(ClaimPattern _ _ _ _) = do + simplifiedTerms <- + Pattern.simplifyTopConfiguration left + fullySimplified <- SMT.Evaluator.filterMultiOr simplifiedTerms + let rules = + map (setRuleLeft rule) (MultiOr.extractPatterns fullySimplified) + return (MultiAnd.make rules) + where + ClaimPattern { left } = rule + + setRuleLeft + :: ClaimPattern + -> Pattern RewritingVariableName + -> ClaimPattern + setRuleLeft + claimPattern@ClaimPattern { left } + patt@Conditional { substitution } + = + -- TODO: take another look at this + ClaimPattern.applySubstitution + substitution + claimPattern + { ClaimPattern.left = + Condition.andCondition + patt + (Condition.eraseConditionalTerm left) + } + instance SimplifyRuleLHS (RewriteRule VariableName) where simplifyRuleLhs = fmap (fmap RewriteRule) . simplifyRuleLhs . getRewriteRule @@ -120,17 +158,16 @@ instance SimplifyRuleLHS ReachabilityRule where (fmap . fmap) AllPath $ simplifyRuleLhs rule simplifyClaimRule - :: forall simplifier variable + :: forall simplifier . MonadSimplify simplifier - => InternalVariable variable - => RulePattern variable - -> simplifier (MultiAnd (RulePattern variable)) + => ClaimPattern + -> simplifier (MultiAnd ClaimPattern) simplifyClaimRule = fmap MultiAnd.make . Logic.observeAllT . worker where simplify, filterWithSolver - :: Pattern variable - -> LogicT simplifier (Pattern variable) + :: Pattern RewritingVariableName + -> LogicT simplifier (Pattern RewritingVariableName) simplify = (return . Pattern.requireDefined) >=> Pattern.simplifyTopConfiguration @@ -138,13 +175,14 @@ simplifyClaimRule = >=> filterWithSolver filterWithSolver = SMT.Evaluator.filterBranch - worker :: RulePattern variable -> LogicT simplifier (RulePattern variable) - worker rulePattern = do - let lhs = Lens.view RulePattern.leftPattern rulePattern + worker :: ClaimPattern -> LogicT simplifier ClaimPattern + worker claimPattern = do + let lhs = ClaimPattern.left claimPattern simplified <- simplify lhs let substitution = Pattern.substitution simplified lhs' = simplified { Pattern.substitution = mempty } - rulePattern - & Lens.set RulePattern.leftPattern lhs' - & RulePattern.applySubstitution substitution + claimPattern + { ClaimPattern.left = lhs' + } + & ClaimPattern.applySubstitution substitution & return From 058f1ab0bc5b23eb77b7861f472381647e92c09b Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Mon, 27 Jul 2020 16:46:14 +0300 Subject: [PATCH 09/27] Step.Rule: parse reachability claims to ClaimPattern --- kore/src/Kore/Internal/OrPattern.hs | 10 ++++++ kore/src/Kore/Internal/Pattern.hs | 13 ++++++++ kore/src/Kore/Internal/TermLike.hs | 2 ++ kore/src/Kore/Step/ClaimPattern.hs | 14 +++++++++ kore/src/Kore/Step/Rule.hs | 48 +++++++++++++++++++---------- 5 files changed, 71 insertions(+), 16 deletions(-) diff --git a/kore/src/Kore/Internal/OrPattern.hs b/kore/src/Kore/Internal/OrPattern.hs index d4d8832610..684fbedd0d 100644 --- a/kore/src/Kore/Internal/OrPattern.hs +++ b/kore/src/Kore/Internal/OrPattern.hs @@ -21,6 +21,7 @@ module Kore.Internal.OrPattern , toTermLike , targetBinder , substitute + , parseFromTermLike , MultiOr.flatten , MultiOr.filterOr , MultiOr.gather @@ -56,6 +57,7 @@ import qualified Kore.Internal.SideCondition.SideCondition as SideCondition ) import Kore.Internal.TermLike ( InternalVariable + , pattern Or_ , Sort , TermLike , mkBottom_ @@ -231,3 +233,11 @@ substitute -> OrPattern variable substitute subst = fromPatterns . fmap (Pattern.substitute subst) . toPatterns + +parseFromTermLike + :: InternalVariable variable + => TermLike variable + -> OrPattern variable +parseFromTermLike (Or_ _ term1 term2) = + parseFromTermLike term1 <> parseFromTermLike term2 +parseFromTermLike term = fromTermLike term diff --git a/kore/src/Kore/Internal/Pattern.hs b/kore/src/Kore/Internal/Pattern.hs index 8012b76d24..5d819ce064 100644 --- a/kore/src/Kore/Internal/Pattern.hs +++ b/kore/src/Kore/Internal/Pattern.hs @@ -10,6 +10,7 @@ module Kore.Internal.Pattern , patternSort , fromCondition , fromCondition_ + , fromTermAndPredicate , fromPredicateSorted , bottom , bottomOf @@ -96,6 +97,18 @@ program configuration for Kore execution. -} type Pattern variable = Conditional variable (TermLike variable) +fromTermAndPredicate + :: InternalVariable variable + => TermLike variable + -> Predicate variable + -> Pattern variable +fromTermAndPredicate term predicate = + Conditional + { term + , predicate + , substitution = mempty + } + fromCondition_ :: InternalVariable variable => Condition variable diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index 18de160b0f..740e31df85 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -47,6 +47,8 @@ module Kore.Internal.TermLike , fullyOverrideSort -- * Reachability modalities and application , Modality + , weakExistsFinally + , weakAlwaysFinally , wEF , wAF , applyModality diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs index ce68f188fa..df461e914d 100644 --- a/kore/src/Kore/Step/ClaimPattern.hs +++ b/kore/src/Kore/Step/ClaimPattern.hs @@ -11,6 +11,10 @@ module Kore.Step.ClaimPattern , ReachabilityRule (..) , toSentence , applySubstitution + , termToExistentials + -- * For unparsing + , onePathRuleToTerm + , allPathRuleToTerm ) where import Prelude.Kore @@ -19,6 +23,7 @@ import Control.DeepSeq ( NFData ) import qualified Data.Default as Default +import qualified Data.Functor.Foldable as Recursive import Data.Map.Strict ( Map ) @@ -221,6 +226,15 @@ isFreeOf rule = $ FreeVariables.toSet $ freeVariables rule +-- | Parses a term representing a RHS into a RHS +-- TODO: move this? +termToExistentials + :: TermLike RewritingVariableName + -> [ElementVariable RewritingVariableName] +termToExistentials (TermLike.Exists_ _ v term) = + v : termToExistentials term +termToRHS _ = [] + -- | One-Path-Claim claim pattern. newtype OnePathRule = OnePathRule { getOnePathRule :: ClaimPattern } diff --git a/kore/src/Kore/Step/Rule.hs b/kore/src/Kore/Step/Rule.hs index 0b32273373..683b266462 100644 --- a/kore/src/Kore/Step/Rule.hs +++ b/kore/src/Kore/Step/Rule.hs @@ -52,13 +52,22 @@ import Kore.IndexedModule.IndexedModule import Kore.Internal.Alias ( Alias (..) ) +import qualified Kore.Internal.OrPattern as OrPattern +import qualified Kore.Internal.Pattern as Pattern import qualified Kore.Internal.Predicate as Predicate import qualified Kore.Internal.Symbol as Internal.Symbol +import Kore.Internal.TermLike + ( weakAlwaysFinally + , weakExistsFinally + ) import qualified Kore.Internal.TermLike as TermLike import Kore.Internal.Variable ( InternalVariable , VariableName ) +import Kore.Rewriting.RewritingVariable + ( mkRuleVariable + ) import Kore.Sort ( Sort (..) , SortVariable (SortVariable) @@ -66,21 +75,23 @@ import Kore.Sort import qualified Kore.Step.AntiLeft as AntiLeft ( parse ) -import Kore.Step.RulePattern +import Kore.Step.ClaimPattern ( AllPathRule (..) - , ImplicationRule (..) + , ClaimPattern (ClaimPattern) , OnePathRule (..) + , allPathRuleToTerm + , onePathRuleToTerm + ) +import qualified Kore.Step.ClaimPattern as ClaimPattern +import Kore.Step.RulePattern + ( ImplicationRule (..) , RewriteRule (..) , RulePattern (..) , allPathGlobally - , allPathRuleToTerm , implicationRuleToTerm , injectTermIntoRHS - , onePathRuleToTerm , rewriteRuleToTerm , termToRHS - , weakAlwaysFinally - , weakExistsFinally ) import Kore.Step.Simplification.ExpandAlias ( substituteInAlias @@ -102,10 +113,10 @@ newtype AxiomPatternError = AxiomPatternError () instance NFData AxiomPatternError -qualifiedAxiomOpToConstructor +reachabilityModalityToConstructor :: Alias (TermLike.TermLike VariableName) - -> Maybe (RulePattern VariableName -> QualifiedAxiomPattern VariableName) -qualifiedAxiomOpToConstructor patternHead + -> Maybe (ClaimPattern -> QualifiedAxiomPattern VariableName) +reachabilityModalityToConstructor patternHead | headName == weakExistsFinally = Just $ OnePathClaimPattern . OnePathRule | headName == weakAlwaysFinally = Just $ AllPathClaimPattern . AllPathRule | otherwise = Nothing @@ -316,13 +327,18 @@ termToAxiomPattern attributes pat = TermLike.Implies_ _ (TermLike.And_ _ requires lhs) (TermLike.ApplyAlias_ op [rhs]) - | Just constructor <- qualifiedAxiomOpToConstructor op -> - pure $ constructor RulePattern - { left = lhs - , antiLeft = Nothing - , requires = Predicate.wrapPredicate requires - , rhs = termToRHS rhs - , attributes + | Just constructor <- reachabilityModalityToConstructor op -> + let rhs' = TermLike.mapVariables (pure mkRuleVariable) rhs + attributes' = Attribute.mapAxiomVariables (pure mkRuleVariable) attributes + in pure $ constructor ClaimPattern + { ClaimPattern.left = + Pattern.fromTermAndPredicate + lhs + (Predicate.wrapPredicate requires) + & Pattern.mapVariables (pure mkRuleVariable) + , ClaimPattern.right = OrPattern.parseFromTermLike rhs' + , ClaimPattern.existentials = ClaimPattern.termToExistentials rhs' + , ClaimPattern.attributes = attributes' } TermLike.Forall_ _ _ child -> termToAxiomPattern attributes child -- implication axioms: From 12b61ca28711399010884cba875f1dd95df00d74 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Mon, 27 Jul 2020 17:48:25 +0300 Subject: [PATCH 10/27] Integrate old claim representation back --- kore/src/Kore/Step/ClaimPattern.hs | 12 +-- kore/src/Kore/Step/Rule.hs | 42 +++++++-- kore/src/Kore/Step/Rule/Expand.hs | 139 +++++++++++++++++++++++----- kore/src/Kore/Step/Rule/Simplify.hs | 49 +++++++++- kore/src/Kore/Step/RulePattern.hs | 3 + 5 files changed, 205 insertions(+), 40 deletions(-) diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs index df461e914d..8f9922d88e 100644 --- a/kore/src/Kore/Step/ClaimPattern.hs +++ b/kore/src/Kore/Step/ClaimPattern.hs @@ -23,7 +23,6 @@ import Control.DeepSeq ( NFData ) import qualified Data.Default as Default -import qualified Data.Functor.Foldable as Recursive import Data.Map.Strict ( Map ) @@ -63,8 +62,7 @@ import Kore.Internal.TermLike ) import qualified Kore.Internal.TermLike as TermLike import Kore.Rewriting.RewritingVariable - ( RewritingVariable - , RewritingVariableName + ( RewritingVariableName , getRewritingVariable ) import qualified Kore.Syntax.Definition as Syntax @@ -194,7 +192,7 @@ substitute subst claimPattern'@(ClaimPattern _ _ _ _) = { left = Pattern.substitute subst left } where - ClaimPattern { left, right, existentials } = claimPattern' + ClaimPattern { left } = claimPattern' -- | Applies a substitution to a claim and checks that -- it was fully applied, i.e. there is no substitution @@ -226,14 +224,14 @@ isFreeOf rule = $ FreeVariables.toSet $ freeVariables rule --- | Parses a term representing a RHS into a RHS --- TODO: move this? +-- TODO(Ana): move this to Internal.TermLike? +-- | Extracts all top level existential quantifications termToExistentials :: TermLike RewritingVariableName -> [ElementVariable RewritingVariableName] termToExistentials (TermLike.Exists_ _ v term) = v : termToExistentials term -termToRHS _ = [] +termToExistentials _ = [] -- | One-Path-Claim claim pattern. newtype OnePathRule = diff --git a/kore/src/Kore/Step/Rule.hs b/kore/src/Kore/Step/Rule.hs index 683b266462..11e43d0b73 100644 --- a/kore/src/Kore/Step/Rule.hs +++ b/kore/src/Kore/Step/Rule.hs @@ -93,6 +93,7 @@ import Kore.Step.RulePattern , rewriteRuleToTerm , termToRHS ) +import qualified Kore.Step.RulePattern as OLD import Kore.Step.Simplification.ExpandAlias ( substituteInAlias ) @@ -117,8 +118,18 @@ reachabilityModalityToConstructor :: Alias (TermLike.TermLike VariableName) -> Maybe (ClaimPattern -> QualifiedAxiomPattern VariableName) reachabilityModalityToConstructor patternHead - | headName == weakExistsFinally = Just $ OnePathClaimPattern . OnePathRule - | headName == weakAlwaysFinally = Just $ AllPathClaimPattern . AllPathRule + | headName == weakExistsFinally = Just $ OnePathClaimPatternNEW . OnePathRule + | headName == weakAlwaysFinally = Just $ AllPathClaimPatternNEW . AllPathRule + | otherwise = Nothing + where + headName = getId (aliasConstructor patternHead) + +qualifiedAxiomOpToConstructor + :: Alias (TermLike.TermLike VariableName) + -> Maybe (RulePattern VariableName -> QualifiedAxiomPattern VariableName) +qualifiedAxiomOpToConstructor patternHead + | headName == weakExistsFinally = Just $ OnePathClaimPattern . OLD.OnePathRule + | headName == weakAlwaysFinally = Just $ AllPathClaimPattern . OLD.AllPathRule | otherwise = Nothing where headName = getId (aliasConstructor patternHead) @@ -128,8 +139,10 @@ from function axioms (used for functional simplification). --} data QualifiedAxiomPattern variable = RewriteAxiomPattern (RewriteRule variable) - | OnePathClaimPattern OnePathRule - | AllPathClaimPattern AllPathRule + | OnePathClaimPattern OLD.OnePathRule + | AllPathClaimPattern OLD.AllPathRule + | OnePathClaimPatternNEW OnePathRule + | AllPathClaimPatternNEW AllPathRule | ImplicationAxiomPattern (ImplicationRule variable) deriving (Eq, GHC.Generic, Ord, Show) -- TODO(virgil): Rename the above since it applies to all sorts of axioms, @@ -323,7 +336,19 @@ termToAxiomPattern -> Either (Error AxiomPatternError) (QualifiedAxiomPattern VariableName) termToAxiomPattern attributes pat = case pat of - -- Reachability claims + -- OLD: Reachability claims + TermLike.Implies_ _ + (TermLike.And_ _ requires lhs) + (TermLike.ApplyAlias_ op [rhs]) + | Just constructor <- qualifiedAxiomOpToConstructor op -> + pure $ constructor RulePattern + { left = lhs + , antiLeft = Nothing + , requires = Predicate.wrapPredicate requires + , rhs = termToRHS rhs + , attributes + } + -- NEW: Reachability claims TermLike.Implies_ _ (TermLike.And_ _ requires lhs) (TermLike.ApplyAlias_ op [rhs]) @@ -379,10 +404,13 @@ axiomPatternToTerm -> TermLike.TermLike VariableName axiomPatternToTerm = \case RewriteAxiomPattern rule -> rewriteRuleToTerm rule - OnePathClaimPattern rule -> onePathRuleToTerm rule - AllPathClaimPattern rule -> allPathRuleToTerm rule + OnePathClaimPattern rule -> OLD.onePathRuleToTerm rule + AllPathClaimPattern rule -> OLD.allPathRuleToTerm rule + OnePathClaimPatternNEW rule -> onePathRuleToTerm rule + AllPathClaimPatternNEW rule -> allPathRuleToTerm rule ImplicationAxiomPattern rule -> implicationRuleToTerm rule +-- TODO(Ana): are these three functions used anywhere anymore? {- | Construct a 'VerifiedKoreSentence' corresponding to 'RewriteRule'. The requires clause must be a predicate, i.e. it can occur in any sort. diff --git a/kore/src/Kore/Step/Rule/Expand.hs b/kore/src/Kore/Step/Rule/Expand.hs index dbf3c06fac..25d8067698 100644 --- a/kore/src/Kore/Step/Rule/Expand.hs +++ b/kore/src/Kore/Step/Rule/Expand.hs @@ -55,7 +55,8 @@ import Kore.Internal.Predicate import qualified Kore.Internal.Predicate as Predicate import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.TermLike - ( TermLike + ( InternalVariable + , TermLike , mkApplySymbol , mkElemVar ) @@ -79,6 +80,10 @@ import Kore.Step.ClaimPattern , OnePathRule (..) , ReachabilityRule (..) ) +import Kore.Step.RulePattern + ( RulePattern (RulePattern) + ) +import qualified Kore.Step.RulePattern as OLD import Kore.Syntax.Variable import Kore.Variables.Fresh ( refreshVariable @@ -96,6 +101,82 @@ class ExpandSingleConstructors rule where -> rule -> rule +instance ExpandSingleConstructors (RulePattern VariableName) where + expandSingleConstructors + metadataTools + rule@(RulePattern _ _ _ _ _) + = case rule of + RulePattern + {left, antiLeft, requires + , rhs = OLD.RHS {existentials, right, ensures} + } -> + let leftVariables :: [ElementVariable VariableName] + leftVariables = + mapMaybe retractElementVariable + $ FreeVariables.toList + $ freeVariables left + allSomeVariables :: Set (SomeVariable VariableName) + allSomeVariables = + FreeVariables.toSet (freeVariables rule) + allElementVariables :: Set (ElementVariableName VariableName) + allElementVariables = + Set.fromList + $ map variableName + $ mapMaybe retract (Set.toList allSomeVariables) + ++ existentials + expansion + :: Map.Map + (SomeVariable VariableName) + (TermLike VariableName) + expansion = + expandVariables + metadataTools + leftVariables + allElementVariables + substitutionPredicate = + ( Substitution.toPredicate + . Substitution.wrap + . Substitution.mkUnwrappedSubstitution + ) + (Map.toList expansion) + subst = Map.mapKeys variableName expansion + in rule + { OLD.left = TermLike.substitute subst left + , OLD.antiLeft = + AntiLeft.substitute subst <$> antiLeft + , OLD.requires = + makeAndPredicate + (Predicate.substitute subst requires) + substitutionPredicate + , OLD.rhs = OLD.RHS + { existentials + , right = TermLike.substitute subst right + , ensures = Predicate.substitute subst ensures + } + } + +instance ExpandSingleConstructors OLD.OnePathRule where + expandSingleConstructors tools = + OLD.OnePathRule . expandSingleConstructors tools . OLD.getOnePathRule + +instance ExpandSingleConstructors OLD.AllPathRule where + expandSingleConstructors tools = + OLD.AllPathRule . expandSingleConstructors tools . OLD.getAllPathRule + +instance ExpandSingleConstructors OLD.ReachabilityRule where + expandSingleConstructors tools (OLD.OnePath rule) = + OLD.OnePath + . OLD.OnePathRule + . expandSingleConstructors tools + . OLD.getOnePathRule + $ rule + expandSingleConstructors tools (OLD.AllPath rule) = + OLD.AllPath + . OLD.AllPathRule + . expandSingleConstructors tools + . OLD.getAllPathRule + $ rule + instance ExpandSingleConstructors ClaimPattern where expandSingleConstructors metadataTools @@ -167,31 +248,33 @@ instance ExpandSingleConstructors ReachabilityRule where . getAllPathRule $ rule -data Expansion = +data Expansion variable = Expansion { substitution :: !( Map - (SomeVariable RewritingVariableName) - (TermLike RewritingVariableName) + (SomeVariable variable) + (TermLike variable) ) , stale - :: !(Set (ElementVariableName RewritingVariableName)) + :: !(Set (ElementVariableName variable)) } deriving (GHC.Generic) -type Expander = State Expansion +type Expander variable = State (Expansion variable) expandVariables - :: SmtMetadataTools attributes - -> [ElementVariable RewritingVariableName] - -> Set (ElementVariableName RewritingVariableName) - -> Map (SomeVariable RewritingVariableName) (TermLike RewritingVariableName) + :: forall variable attributes + . InternalVariable variable + => SmtMetadataTools attributes + -> [ElementVariable variable] + -> Set (ElementVariableName variable) + -> Map (SomeVariable variable) (TermLike variable) expandVariables metadataTools variables stale = traverse expandAddVariable variables & flip execState Expansion { substitution = Map.empty, stale } & substitution where - expandAddVariable :: ElementVariable RewritingVariableName -> Expander () + expandAddVariable :: ElementVariable variable -> Expander variable () expandAddVariable variable = do term <- expandVariable metadataTools variable Monad.unless @@ -199,18 +282,22 @@ expandVariables metadataTools variables stale = (field @"substitution" %= Map.insert (inject variable) term) expandVariable - :: SmtMetadataTools attributes - -> ElementVariable RewritingVariableName - -> Expander (TermLike RewritingVariableName) + :: forall variable attributes + . InternalVariable variable + => SmtMetadataTools attributes + -> ElementVariable variable + -> Expander variable (TermLike variable) expandVariable metadataTools variable@Variable { variableSort } = expandSort metadataTools variable UseDirectly variableSort expandSort - :: SmtMetadataTools attributes - -> ElementVariable RewritingVariableName + :: forall variable attributes + . InternalVariable variable + => SmtMetadataTools attributes + -> ElementVariable variable -> VariableUsage -> Sort - -> Expander (TermLike RewritingVariableName) + -> Expander variable (TermLike variable) expandSort metadataTools defaultVariable variableUsage sort = case findSingleConstructor sort of Just constructor -> @@ -229,10 +316,12 @@ expandSort metadataTools defaultVariable variableUsage sort = _ -> Nothing expandConstructor - :: SmtMetadataTools attributes - -> ElementVariable RewritingVariableName + :: forall variable attributes + . InternalVariable variable + => SmtMetadataTools attributes + -> ElementVariable variable -> Attribute.Constructors.Constructor - -> Expander (TermLike RewritingVariableName) + -> Expander variable (TermLike variable) expandConstructor metadataTools defaultVariable @@ -240,7 +329,7 @@ expandConstructor = mkApplySymbol symbol <$> traverse expandChildSort sorts where - expandChildSort :: Sort -> Expander (TermLike RewritingVariableName) + expandChildSort :: Sort -> Expander variable (TermLike variable) expandChildSort = expandSort metadataTools defaultVariable UseAsPrototype {-| Context: we have a TermLike that contains a variables, and we @@ -266,11 +355,13 @@ data VariableUsage = -- variable, so we need to generate a new one based on it. maybeNewVariable - :: HasCallStack - => ElementVariable RewritingVariableName + :: forall variable + . InternalVariable variable + => HasCallStack + => ElementVariable variable -> Sort -> VariableUsage - -> Expander (TermLike RewritingVariableName) + -> Expander variable (TermLike variable) maybeNewVariable variable@Variable { variableSort } sort diff --git a/kore/src/Kore/Step/Rule/Simplify.hs b/kore/src/Kore/Step/Rule/Simplify.hs index d93f6e061c..07f6d5936d 100644 --- a/kore/src/Kore/Step/Rule/Simplify.hs +++ b/kore/src/Kore/Step/Rule/Simplify.hs @@ -52,6 +52,7 @@ import Kore.Step.RulePattern ( RewriteRule (..) , RulePattern (RulePattern) ) +import qualified Kore.Step.RulePattern as OLD import qualified Kore.Step.RulePattern as RulePattern ( RulePattern (..) , applySubstitution @@ -126,7 +127,7 @@ instance SimplifyRuleLHS ClaimPattern -> Pattern RewritingVariableName -> ClaimPattern setRuleLeft - claimPattern@ClaimPattern { left } + claimPattern@ClaimPattern { left = left' } patt@Conditional { substitution } = -- TODO: take another look at this @@ -136,13 +137,27 @@ instance SimplifyRuleLHS ClaimPattern { ClaimPattern.left = Condition.andCondition patt - (Condition.eraseConditionalTerm left) + (Condition.eraseConditionalTerm left') } instance SimplifyRuleLHS (RewriteRule VariableName) where simplifyRuleLhs = fmap (fmap RewriteRule) . simplifyRuleLhs . getRewriteRule +instance SimplifyRuleLHS OLD.OnePathRule where + simplifyRuleLhs = + fmap (fmap OLD.OnePathRule) . simplifyClaimRuleOLD . OLD.getOnePathRule + +instance SimplifyRuleLHS OLD.AllPathRule where + simplifyRuleLhs = + fmap (fmap OLD.AllPathRule) . simplifyClaimRuleOLD . OLD.getAllPathRule + +instance SimplifyRuleLHS OLD.ReachabilityRule where + simplifyRuleLhs (OLD.OnePath rule) = + (fmap . fmap) OLD.OnePath $ simplifyRuleLhs rule + simplifyRuleLhs (OLD.AllPath rule) = + (fmap . fmap) OLD.AllPath $ simplifyRuleLhs rule + instance SimplifyRuleLHS OnePathRule where simplifyRuleLhs = fmap (fmap OnePathRule) . simplifyClaimRule . getOnePathRule @@ -157,6 +172,36 @@ instance SimplifyRuleLHS ReachabilityRule where simplifyRuleLhs (AllPath rule) = (fmap . fmap) AllPath $ simplifyRuleLhs rule +simplifyClaimRuleOLD + :: forall simplifier variable + . MonadSimplify simplifier + => InternalVariable variable + => RulePattern variable + -> simplifier (MultiAnd (RulePattern variable)) +simplifyClaimRuleOLD = + fmap MultiAnd.make . Logic.observeAllT . worker + where + simplify, filterWithSolver + :: Pattern variable + -> LogicT simplifier (Pattern variable) + simplify = + (return . Pattern.requireDefined) + >=> Pattern.simplifyTopConfiguration + >=> Logic.scatter + >=> filterWithSolver + filterWithSolver = SMT.Evaluator.filterBranch + + worker :: RulePattern variable -> LogicT simplifier (RulePattern variable) + worker rulePattern = do + let lhs = Lens.view RulePattern.leftPattern rulePattern + simplified <- simplify lhs + let substitution = Pattern.substitution simplified + lhs' = simplified { Pattern.substitution = mempty } + rulePattern + & Lens.set RulePattern.leftPattern lhs' + & RulePattern.applySubstitution substitution + & return + simplifyClaimRule :: forall simplifier . MonadSimplify simplifier diff --git a/kore/src/Kore/Step/RulePattern.hs b/kore/src/Kore/Step/RulePattern.hs index 4a4fddcb9a..27af9a973c 100644 --- a/kore/src/Kore/Step/RulePattern.hs +++ b/kore/src/Kore/Step/RulePattern.hs @@ -9,6 +9,9 @@ module Kore.Step.RulePattern ( RulePattern (..) , RewriteRule (..) , ImplicationRule (..) + , OnePathRule (..) + , AllPathRule (..) + , ReachabilityRule (..) , RHS (..) , HasAttributes (..) , ToRulePattern (..) From 6f9880df3fda69de2406831f0e018194981c32f0 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 28 Jul 2020 12:10:47 +0300 Subject: [PATCH 11/27] Step.Rule.Expand: refactor instance for ClaimPattern --- kore/src/Kore/Internal/Conditional.hs | 14 +++++ kore/src/Kore/Rewriting/RewritingVariable.hs | 2 +- kore/src/Kore/Step/Rule/Expand.hs | 55 +++++++++++--------- 3 files changed, 45 insertions(+), 26 deletions(-) diff --git a/kore/src/Kore/Internal/Conditional.hs b/kore/src/Kore/Internal/Conditional.hs index 51ff7581e1..7be50430aa 100644 --- a/kore/src/Kore/Internal/Conditional.hs +++ b/kore/src/Kore/Internal/Conditional.hs @@ -32,6 +32,9 @@ import Prelude.Kore import Control.DeepSeq ( NFData ) +import Data.Map.Strict + ( Map + ) import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC @@ -245,6 +248,17 @@ instance where from = pure +instance + InternalVariable variable + => From (Map (SomeVariable variable) (TermLike variable)) (Conditional variable ()) + where + from = + from @(Predicate variable) @(Conditional variable ()) + . from @(Substitution variable) @(Predicate variable) + . from + @(Map (SomeVariable variable) (TermLike variable)) + @(Substitution variable) + unparseConditional :: Sort -> Doc ann -- ^ term diff --git a/kore/src/Kore/Rewriting/RewritingVariable.hs b/kore/src/Kore/Rewriting/RewritingVariable.hs index 22a3a5ce49..b24865f47d 100644 --- a/kore/src/Kore/Rewriting/RewritingVariable.hs +++ b/kore/src/Kore/Rewriting/RewritingVariable.hs @@ -27,7 +27,7 @@ module Kore.Rewriting.RewritingVariable , getResultPattern , getRemainderPredicate , getRemainderPattern - -- * For reachability rule unparsing + -- * Exported for reachability rule unparsing , getRewritingVariable ) where diff --git a/kore/src/Kore/Step/Rule/Expand.hs b/kore/src/Kore/Step/Rule/Expand.hs index 25d8067698..7061a8c2e7 100644 --- a/kore/src/Kore/Step/Rule/Expand.hs +++ b/kore/src/Kore/Step/Rule/Expand.hs @@ -46,7 +46,9 @@ import Kore.IndexedModule.MetadataTools ( SmtMetadataTools , findSortConstructors ) -import qualified Kore.Internal.Condition as Condition +import Kore.Internal.Condition + ( Condition + ) import qualified Kore.Internal.OrPattern as OrPattern import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.Predicate @@ -107,7 +109,7 @@ instance ExpandSingleConstructors (RulePattern VariableName) where rule@(RulePattern _ _ _ _ _) = case rule of RulePattern - {left, antiLeft, requires + { left, antiLeft, requires , rhs = OLD.RHS {existentials, right, ensures} } -> let leftVariables :: [ElementVariable VariableName] @@ -187,20 +189,23 @@ instance ExpandSingleConstructors ClaimPattern where , existentials , right } -> - let leftVariables :: [ElementVariable RewritingVariableName] - leftVariables = - mapMaybe retractElementVariable - $ FreeVariables.toList - $ freeVariables left - allSomeVariables :: Set (SomeVariable RewritingVariableName) - allSomeVariables = - FreeVariables.toSet (freeVariables rule) - allElementVariables :: Set (ElementVariableName RewritingVariableName) - allElementVariables = - Set.fromList - $ map variableName - $ mapMaybe retract (Set.toList allSomeVariables) - ++ existentials + let leftElementVariables + :: [ElementVariable RewritingVariableName] + leftElementVariables = + extractFreeElementVariables + . freeVariables + $ left + freeElementVariables + :: [ElementVariable RewritingVariableName] + freeElementVariables = + extractFreeElementVariables + . freeVariables + $ rule + allElementVariableNames + :: Set (ElementVariableName RewritingVariableName) + allElementVariableNames = + variableName <$> freeElementVariables <> existentials + & Set.fromList expansion :: Map.Map (SomeVariable RewritingVariableName) @@ -208,23 +213,23 @@ instance ExpandSingleConstructors ClaimPattern where expansion = expandVariables metadataTools - leftVariables - allElementVariables - substitutionPredicate = - ( Substitution.toPredicate - . Substitution.wrap - . Substitution.mkUnwrappedSubstitution - ) - (Map.toList expansion) + leftElementVariables + allElementVariableNames + substitutionCondition = + from @(Map _ _) @(Condition _) expansion subst = Map.mapKeys variableName expansion in rule { left = Pattern.andCondition (Pattern.substitute subst left) - (Condition.fromPredicate substitutionPredicate) + substitutionCondition , existentials , right = OrPattern.substitute subst right } + where + extractFreeElementVariables = + mapMaybe retractElementVariable + . FreeVariables.toList instance ExpandSingleConstructors OnePathRule where expandSingleConstructors tools = From 52d53803deded064a033aa75c8f832b588375d68 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 28 Jul 2020 12:17:00 +0300 Subject: [PATCH 12/27] Step.Rule.Simplify: refactor instance for ClaimPattern --- kore/src/Kore/Step/Rule/Simplify.hs | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/kore/src/Kore/Step/Rule/Simplify.hs b/kore/src/Kore/Step/Rule/Simplify.hs index 07f6d5936d..39b9b345c7 100644 --- a/kore/src/Kore/Step/Rule/Simplify.hs +++ b/kore/src/Kore/Step/Rule/Simplify.hs @@ -25,6 +25,7 @@ import qualified Kore.Internal.MultiAnd as MultiAnd ( make ) import qualified Kore.Internal.MultiOr as MultiOr +import qualified Kore.Internal.OrPattern as OrPattern import Kore.Internal.Pattern ( Pattern ) @@ -115,9 +116,11 @@ instance SimplifyRuleLHS ClaimPattern simplifyRuleLhs rule@(ClaimPattern _ _ _ _) = do simplifiedTerms <- Pattern.simplifyTopConfiguration left - fullySimplified <- SMT.Evaluator.filterMultiOr simplifiedTerms + fullySimplified <- + SMT.Evaluator.filterMultiOr simplifiedTerms let rules = - map (setRuleLeft rule) (MultiOr.extractPatterns fullySimplified) + setRuleLeft rule + <$> OrPattern.toPatterns fullySimplified return (MultiAnd.make rules) where ClaimPattern { left } = rule @@ -130,7 +133,6 @@ instance SimplifyRuleLHS ClaimPattern claimPattern@ClaimPattern { left = left' } patt@Conditional { substitution } = - -- TODO: take another look at this ClaimPattern.applySubstitution substitution claimPattern From be962b3277d3f37208c89fbbc3af85a7efdb262e Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 28 Jul 2020 13:21:01 +0300 Subject: [PATCH 13/27] ClaimPattern: functions to construct ClaimPatterns --- kore/src/Kore/Step/ClaimPattern.hs | 58 +++++++++++++++++++++++------- 1 file changed, 46 insertions(+), 12 deletions(-) diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs index 8f9922d88e..93a7f267b3 100644 --- a/kore/src/Kore/Step/ClaimPattern.hs +++ b/kore/src/Kore/Step/ClaimPattern.hs @@ -6,6 +6,8 @@ License : NCSA module Kore.Step.ClaimPattern ( ClaimPattern (..) + , claimPattern + , claimPatternInternal , OnePathRule (..) , AllPathRule (..) , ReachabilityRule (..) @@ -142,6 +144,38 @@ instance HasFreeVariables ClaimPattern RewritingVariableName where where ClaimPattern { left, right } = claimPattern' +-- | Creates a 'ClaimPattern' from a left hand side 'Pattern' +-- and a 'TermLike' representing the right hand side pattern. The +-- 'TermLike' is parsed into an 'OrPattern' and a list of +-- existentially quantified variables. +claimPattern + :: Pattern RewritingVariableName + -> TermLike RewritingVariableName + -> ClaimPattern +claimPattern left rightTerm = + ClaimPattern + { left + , right = OrPattern.parseFromTermLike rightTerm + , existentials = termToExistentials rightTerm + , attributes = Default.def + } + +-- | Unsafe version of 'claimPattern'. The right hand side is +-- assumed to be already processed into an 'OrPattern' and +-- a list of existentially quantified variables. +claimPatternInternal + :: Pattern RewritingVariableName + -> OrPattern RewritingVariableName + -> [ElementVariable RewritingVariableName] + -> ClaimPattern +claimPatternInternal left right existentials = + ClaimPattern + { left + , right + , existentials + , attributes = Default.def + } + claimPatternToTerm :: Modality -> ClaimPattern @@ -253,22 +287,22 @@ instance Diff OnePathRule -- as some of the variable information related to the -- rewriting algorithm is lost. onePathRuleToTerm :: OnePathRule -> TermLike VariableName -onePathRuleToTerm (OnePathRule claimPattern) = - claimPatternToTerm TermLike.wEF claimPattern +onePathRuleToTerm (OnePathRule claimPattern') = + claimPatternToTerm TermLike.wEF claimPattern' instance Unparse OnePathRule where - unparse claimPattern = + unparse claimPattern' = "claim {}" <> Pretty.line' <> Pretty.nest 4 - (unparse $ onePathRuleToTerm claimPattern) + (unparse $ onePathRuleToTerm claimPattern') <> Pretty.line' <> "[]" - unparse2 claimPattern = + unparse2 claimPattern' = "claim {}" Pretty.<+> - unparse2 (onePathRuleToTerm claimPattern) + unparse2 (onePathRuleToTerm claimPattern') Pretty.<+> "[]" instance TopBottom OnePathRule where @@ -303,17 +337,17 @@ instance Debug AllPathRule instance Diff AllPathRule instance Unparse AllPathRule where - unparse claimPattern = + unparse claimPattern' = "claim {}" <> Pretty.line' <> Pretty.nest 4 - (unparse $ allPathRuleToTerm claimPattern) + (unparse $ allPathRuleToTerm claimPattern') <> Pretty.line' <> "[]" - unparse2 claimPattern = + unparse2 claimPattern' = "claim {}" Pretty.<+> - unparse2 (allPathRuleToTerm claimPattern) + unparse2 (allPathRuleToTerm claimPattern') Pretty.<+> "[]" instance TopBottom AllPathRule where @@ -337,8 +371,8 @@ instance From AllPathRule Attribute.Trusted where -- as some of the variable information related to the -- rewriting algorithm is lost. allPathRuleToTerm :: AllPathRule -> TermLike VariableName -allPathRuleToTerm (AllPathRule claimPattern) = - claimPatternToTerm TermLike.wAF claimPattern +allPathRuleToTerm (AllPathRule claimPattern') = + claimPatternToTerm TermLike.wAF claimPattern' -- | Unified One-Path and All-Path claim pattern. data ReachabilityRule From cd886e38aaaf6f3df688801d491f285ffdf83ec8 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 28 Jul 2020 13:21:23 +0300 Subject: [PATCH 14/27] Test.Step.Rule.Expand: add tests for ClaimPattern --- kore/test/Test/Kore/Step/Rule/Expand.hs | 227 ++++++++++++++++++++++-- 1 file changed, 210 insertions(+), 17 deletions(-) diff --git a/kore/test/Test/Kore/Step/Rule/Expand.hs b/kore/test/Test/Kore/Step/Rule/Expand.hs index 2c27961ae3..ce4b99fc7e 100644 --- a/kore/test/Test/Kore/Step/Rule/Expand.hs +++ b/kore/test/Test/Kore/Step/Rule/Expand.hs @@ -33,11 +33,14 @@ import Kore.IndexedModule.MetadataTools import qualified Kore.IndexedModule.MetadataTools as MetadataTools ( MetadataTools (..) ) +import qualified Kore.Internal.OrPattern as OrPattern +import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.Predicate ( Predicate , makeEqualsPredicate_ , makeTruePredicate_ ) +import qualified Kore.Internal.Predicate as Predicate import Kore.Internal.Symbol ( Symbol ) @@ -50,13 +53,20 @@ import Kore.Internal.TermLike , mkApplySymbol , mkElemVar ) +import qualified Kore.Internal.TermLike as TermLike +import Kore.Rewriting.RewritingVariable + ( mkRuleVariable + ) +import Kore.Step.ClaimPattern + ( OnePathRule (OnePathRule) + , claimPatternInternal + ) import Kore.Step.Rule.Expand import Kore.Step.RulePattern - ( OnePathRule (OnePathRule) - , RHS (..) + ( RHS (RHS) , RulePattern (RulePattern) ) -import qualified Kore.Step.RulePattern as Rule.DoNotUse +import qualified Kore.Step.RulePattern as OLD import Kore.Syntax.Id ( Id ) @@ -71,33 +81,216 @@ import Test.Kore.With ) import Test.Tasty.HUnit.Ext +newtype Pair variable = Pair (TermLike variable, Predicate variable) + +class OnePathRuleBaseOLD base where + rewritesToOLD :: base VariableName -> base VariableName -> OLD.OnePathRule + +instance OnePathRuleBaseOLD Pair where + Pair (t1, p1) `rewritesToOLD` Pair (t2, p2) = + OLD.OnePathRule RulePattern + { OLD.left = t1 + , OLD.requires = p1 + , OLD.rhs = RHS + { OLD.existentials = [] + , OLD.right = t2 + , OLD.ensures = p2 + } + , OLD.antiLeft = Nothing + , OLD.attributes = def + } + +instance OnePathRuleBaseOLD TermLike where + t1 `rewritesToOLD` t2 = + Pair (t1, makeTruePredicate_) `rewritesToOLD` Pair (t2, makeTruePredicate_) + class OnePathRuleBase base where rewritesTo :: base VariableName -> base VariableName -> OnePathRule -newtype Pair variable = Pair (TermLike variable, Predicate variable) - instance OnePathRuleBase Pair where Pair (t1, p1) `rewritesTo` Pair (t2, p2) = - OnePathRule RulePattern - { left = t1 - , requires = p1 - , rhs = RHS - { existentials = [] - , right = t2 - , ensures = p2 - } - , antiLeft = Nothing - , attributes = def - } + OnePathRule + $ claimPatternInternal + (Pattern.fromTermAndPredicate t1' p1') + (Pattern.fromTermAndPredicate t2' p2' & OrPattern.fromPattern) + [] + where + t1' = TermLike.mapVariables (pure mkRuleVariable) t1 + t2' = TermLike.mapVariables (pure mkRuleVariable) t2 + p1' = Predicate.mapVariables (pure mkRuleVariable) p1 + p2' = Predicate.mapVariables (pure mkRuleVariable) p2 instance OnePathRuleBase TermLike where t1 `rewritesTo` t2 = Pair (t1, makeTruePredicate_) `rewritesTo` Pair (t2, makeTruePredicate_) - test_expandRule :: [TestTree] test_expandRule = [ testCase "Nothing to expand" $ + let expected = Mock.f x `rewritesToOLD` Mock.g x + actual = + expandSingleConstructors + (metadataTools []) + (Mock.f x `rewritesToOLD` Mock.g x) + in assertEqual "" expected actual + , testCase "Nothing to expand without constructors" $ + let expected = Mock.f x `rewritesToOLD` Mock.g x + actual = + expandSingleConstructors + (metadataTools + [ (Mock.testSortId, noConstructor) ] + ) + (Mock.f x `rewritesToOLD` Mock.g x) + in assertEqual "" expected actual + , testCase "Nothing to expand with multiple constructors" $ + let expected = Mock.f x `rewritesToOLD` Mock.g x + actual = + expandSingleConstructors + (metadataTools + [ ( Mock.testSortId + , noConstructor + `with` constructor Mock.aSymbol + `with` constructor Mock.bSymbol + ) + ] + ) + (Mock.f x `rewritesToOLD` Mock.g x) + in assertEqual "" expected actual + , testCase "Expands variable once to constant" $ + let expected = + Pair (Mock.f Mock.a, makeEqualsPredicate_ x Mock.a) + `rewritesToOLD` + Pair (Mock.g Mock.a, makeTruePredicate_) + actual = + expandSingleConstructors + (metadataTools + [ ( Mock.testSortId + , noConstructor `with` constructor Mock.aSymbol + ) + ] + ) + (Mock.f x `rewritesToOLD` Mock.g x) + in assertEqual "" expected actual + , testCase "Expands variable once to argument constructor" $ + let expected = + Pair + ( Mock.fSort0 (expandableConstructor1 x00TestSort) + , makeEqualsPredicate_ + x0 + (expandableConstructor1 x00TestSort) + ) + `rewritesToOLD` + Pair + ( Mock.gSort0 (expandableConstructor1 x00TestSort) + , makeTruePredicate_ + ) + actual = + expandSingleConstructors + (metadataTools + [ ( Mock.testSort0Id + , noConstructor + `with` + ( constructor expandableConstructor1Symbol + `with` Mock.testSort + ) + ) + ] + ) + (Mock.fSort0 x0 `rewritesToOLD` Mock.gSort0 x0) + in assertEqual "" expected actual + , testCase "Expands variable twice." $ + let expected = + Pair + ( Mock.fSort0 (expandableConstructor1 Mock.a) + , makeEqualsPredicate_ + x0 + (expandableConstructor1 Mock.a) + ) + `rewritesToOLD` + Pair + ( Mock.gSort0 (expandableConstructor1 Mock.a) + , makeTruePredicate_ + ) + actual = + expandSingleConstructors + (metadataTools + [ ( Mock.testSort0Id + , noConstructor + `with` + ( constructor expandableConstructor1Symbol + `with` Mock.testSort + ) + ) + , ( Mock.testSortId + , noConstructor `with` constructor Mock.aSymbol + ) + ] + ) + (Mock.fSort0 x0 `rewritesToOLD` Mock.gSort0 x0) + in assertEqual "" expected actual + , testCase "Expands multiple arguments." $ + let expected = + Pair + ( Mock.fSort0 (expandableConstructor2 Mock.a Mock.a) + , makeEqualsPredicate_ + x0 + (expandableConstructor2 Mock.a Mock.a) + ) + `rewritesToOLD` + Pair + ( Mock.gSort0 (expandableConstructor2 Mock.a Mock.a) + , makeTruePredicate_ + ) + actual = + expandSingleConstructors + (metadataTools + [ ( Mock.testSort0Id + , noConstructor + `with` + ( constructor expandableConstructor2Symbol + `with` Mock.testSort + `with` Mock.testSort + ) + ) + , ( Mock.testSortId + , noConstructor `with` constructor Mock.aSymbol + ) + ] + ) + (Mock.fSort0 x0 `rewritesToOLD` Mock.gSort0 x0) + in assertEqual "" expected actual + , testCase "Expands one of multiple arguments" $ + let expected = + Pair + ( Mock.fSort0 (expandableConstructor2a x00TestSort1 Mock.a) + , makeEqualsPredicate_ + x0 + (expandableConstructor2a x00TestSort1 Mock.a) + ) + `rewritesToOLD` + Pair + ( Mock.gSort0 (expandableConstructor2a x00TestSort1 Mock.a) + , makeTruePredicate_ + ) + actual = + expandSingleConstructors + (metadataTools + [ ( Mock.testSort0Id + , noConstructor + `with` + ( constructor expandableConstructor2aSymbol + `with` Mock.testSort1 + `with` Mock.testSort + ) + ) + , ( Mock.testSortId + , noConstructor `with` constructor Mock.aSymbol + ) + ] + ) + (Mock.fSort0 x0 `rewritesToOLD` Mock.gSort0 x0) + in assertEqual "" expected actual + , testCase "Nothing to expand" $ let expected = Mock.f x `rewritesTo` Mock.g x actual = expandSingleConstructors From 17c94eced444590d3bee94caba894c43ef15b60c Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 28 Jul 2020 15:37:49 +0300 Subject: [PATCH 15/27] Test.Step.Rule: add Common.hs + add tests for ClaimPattern in Simplify.hs --- kore/test/Test/Kore/Step/Rule/Common.hs | 81 +++++ kore/test/Test/Kore/Step/Rule/Expand.hs | 70 +--- kore/test/Test/Kore/Step/Rule/Simplify.hs | 376 +++++++++++++++++++--- 3 files changed, 412 insertions(+), 115 deletions(-) create mode 100644 kore/test/Test/Kore/Step/Rule/Common.hs diff --git a/kore/test/Test/Kore/Step/Rule/Common.hs b/kore/test/Test/Kore/Step/Rule/Common.hs new file mode 100644 index 0000000000..25df1d85a2 --- /dev/null +++ b/kore/test/Test/Kore/Step/Rule/Common.hs @@ -0,0 +1,81 @@ +module Test.Kore.Step.Rule.Common + ( Pair (..) + , rewritesToOLD + , rewritesTo + ) where + +import Prelude.Kore + + +import qualified Data.Default as Default + +import qualified Kore.Internal.OrPattern as OrPattern +import qualified Kore.Internal.Pattern as Pattern +import Kore.Internal.Predicate + ( Predicate + , makeTruePredicate + ) +import qualified Kore.Internal.Predicate as Predicate +import Kore.Internal.TermLike + ( TermLike + , VariableName + ) +import qualified Kore.Internal.TermLike as TermLike +import Kore.Rewriting.RewritingVariable + ( mkRuleVariable + ) +import Kore.Step.ClaimPattern + ( OnePathRule (..) + , claimPatternInternal + ) +import Kore.Step.RulePattern + ( RHS (RHS) + , RulePattern (RulePattern) + ) +import qualified Kore.Step.RulePattern as OLD + +newtype Pair variable = Pair (TermLike variable, Predicate variable) + +class OnePathRuleBaseOLD base where + rewritesToOLD :: base VariableName -> base VariableName -> OLD.OnePathRule + +instance OnePathRuleBaseOLD Pair where + Pair (t1, p1) `rewritesToOLD` Pair (t2, p2) = + OLD.OnePathRule RulePattern + { OLD.left = t1 + , OLD.requires = p1 + , OLD.rhs = RHS + { OLD.existentials = [] + , OLD.right = t2 + , OLD.ensures = p2 + } + , OLD.antiLeft = Nothing + , OLD.attributes = Default.def + } + +instance OnePathRuleBaseOLD TermLike where + t1 `rewritesToOLD` t2 = + Pair (t1, makeTruePredicate (TermLike.termLikeSort t1)) + `rewritesToOLD` Pair (t2, makeTruePredicate (TermLike.termLikeSort t2)) + +class OnePathRuleBase base where + rewritesTo :: base VariableName -> base VariableName -> OnePathRule + +instance OnePathRuleBase Pair where + Pair (t1, p1) `rewritesTo` Pair (t2, p2) = + OnePathRule + $ claimPatternInternal + (Pattern.fromTermAndPredicate t1' p1') + (Pattern.fromTermAndPredicate t2' p2' & OrPattern.fromPattern) + [] + where + t1' = TermLike.mapVariables (pure mkRuleVariable) t1 + t2' = TermLike.mapVariables (pure mkRuleVariable) t2 + p1' = Predicate.mapVariables (pure mkRuleVariable) p1 + p2' = Predicate.mapVariables (pure mkRuleVariable) p2 + +instance OnePathRuleBase TermLike where + t1 `rewritesTo` t2 = + Pair (t1, makeTruePredicate (TermLike.termLikeSort t1)) + `rewritesTo` Pair (t2, makeTruePredicate (TermLike.termLikeSort t2)) + diff --git a/kore/test/Test/Kore/Step/Rule/Expand.hs b/kore/test/Test/Kore/Step/Rule/Expand.hs index ce4b99fc7e..e7b3a6c3e0 100644 --- a/kore/test/Test/Kore/Step/Rule/Expand.hs +++ b/kore/test/Test/Kore/Step/Rule/Expand.hs @@ -6,9 +6,6 @@ import Prelude.Kore import Test.Tasty -import Data.Default - ( def - ) import Data.Generics.Product ( field ) @@ -33,14 +30,10 @@ import Kore.IndexedModule.MetadataTools import qualified Kore.IndexedModule.MetadataTools as MetadataTools ( MetadataTools (..) ) -import qualified Kore.Internal.OrPattern as OrPattern -import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.Predicate - ( Predicate - , makeEqualsPredicate_ + ( makeEqualsPredicate_ , makeTruePredicate_ ) -import qualified Kore.Internal.Predicate as Predicate import Kore.Internal.Symbol ( Symbol ) @@ -53,20 +46,7 @@ import Kore.Internal.TermLike , mkApplySymbol , mkElemVar ) -import qualified Kore.Internal.TermLike as TermLike -import Kore.Rewriting.RewritingVariable - ( mkRuleVariable - ) -import Kore.Step.ClaimPattern - ( OnePathRule (OnePathRule) - , claimPatternInternal - ) import Kore.Step.Rule.Expand -import Kore.Step.RulePattern - ( RHS (RHS) - , RulePattern (RulePattern) - ) -import qualified Kore.Step.RulePattern as OLD import Kore.Syntax.Id ( Id ) @@ -76,54 +56,16 @@ import Test.Kore ( testId ) import qualified Test.Kore.Step.MockSymbols as Mock +import Test.Kore.Step.Rule.Common + ( Pair (..) + , rewritesTo + , rewritesToOLD + ) import Test.Kore.With ( with ) import Test.Tasty.HUnit.Ext -newtype Pair variable = Pair (TermLike variable, Predicate variable) - -class OnePathRuleBaseOLD base where - rewritesToOLD :: base VariableName -> base VariableName -> OLD.OnePathRule - -instance OnePathRuleBaseOLD Pair where - Pair (t1, p1) `rewritesToOLD` Pair (t2, p2) = - OLD.OnePathRule RulePattern - { OLD.left = t1 - , OLD.requires = p1 - , OLD.rhs = RHS - { OLD.existentials = [] - , OLD.right = t2 - , OLD.ensures = p2 - } - , OLD.antiLeft = Nothing - , OLD.attributes = def - } - -instance OnePathRuleBaseOLD TermLike where - t1 `rewritesToOLD` t2 = - Pair (t1, makeTruePredicate_) `rewritesToOLD` Pair (t2, makeTruePredicate_) - -class OnePathRuleBase base where - rewritesTo :: base VariableName -> base VariableName -> OnePathRule - -instance OnePathRuleBase Pair where - Pair (t1, p1) `rewritesTo` Pair (t2, p2) = - OnePathRule - $ claimPatternInternal - (Pattern.fromTermAndPredicate t1' p1') - (Pattern.fromTermAndPredicate t2' p2' & OrPattern.fromPattern) - [] - where - t1' = TermLike.mapVariables (pure mkRuleVariable) t1 - t2' = TermLike.mapVariables (pure mkRuleVariable) t2 - p1' = Predicate.mapVariables (pure mkRuleVariable) p1 - p2' = Predicate.mapVariables (pure mkRuleVariable) p2 - -instance OnePathRuleBase TermLike where - t1 `rewritesTo` t2 = - Pair (t1, makeTruePredicate_) `rewritesTo` Pair (t2, makeTruePredicate_) - test_expandRule :: [TestTree] test_expandRule = [ testCase "Nothing to expand" $ diff --git a/kore/test/Test/Kore/Step/Rule/Simplify.hs b/kore/test/Test/Kore/Step/Rule/Simplify.hs index 89f75c864b..950de6abb9 100644 --- a/kore/test/Test/Kore/Step/Rule/Simplify.hs +++ b/kore/test/Test/Kore/Step/Rule/Simplify.hs @@ -1,5 +1,6 @@ module Test.Kore.Step.Rule.Simplify ( test_simplifyRule + , test_simplifyClaimRuleOLD , test_simplifyClaimRule ) where @@ -18,19 +19,20 @@ import Control.Monad.Reader ) import qualified Control.Monad.Reader as Reader import qualified Data.Bifunctor as Bifunctor -import Data.Default - ( def - ) import qualified Data.Foldable as Foldable import Data.Generics.Product ( field ) +import Kore.Internal.Condition + ( Condition + ) import qualified Kore.Internal.Condition as Condition import qualified Kore.Internal.MultiAnd as MultiAnd ( extractPatterns ) import qualified Kore.Internal.OrPattern as OrPattern +import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.Predicate ( Predicate , makeAndPredicate @@ -42,7 +44,8 @@ import Kore.Internal.Predicate import qualified Kore.Internal.Predicate as Predicate import qualified Kore.Internal.SideCondition as SideCondition import Kore.Internal.TermLike - ( InternalVariable + ( AdjSomeVariableName + , InternalVariable , TermLike , mkAnd , mkElemVar @@ -51,17 +54,24 @@ import Kore.Internal.TermLike , termLikeSort ) import qualified Kore.Internal.TermLike as TermLike +import Kore.Rewriting.RewritingVariable + ( RewritingVariableName + , getRewritingVariable + ) import Kore.Sort ( predicateSort ) +import Kore.Step.ClaimPattern + ( ClaimPattern + , OnePathRule (..) + , claimPattern + ) import Kore.Step.Rule.Simplify import Kore.Step.RulePattern - ( OnePathRule (..) - , RHS (..) - , RulePattern (RulePattern) + ( RulePattern , rulePattern ) -import qualified Kore.Step.RulePattern as Rule.DoNotUse +import qualified Kore.Step.RulePattern as OLD import Kore.Step.Simplification.Data ( Env (..) , runSimplifier @@ -79,38 +89,151 @@ import Kore.Syntax.Variable ) import qualified Test.Kore.Step.MockSymbols as Mock +import Test.Kore.Step.Rule.Common + ( Pair (..) + , rewritesTo + , rewritesToOLD + ) import Test.SMT ( runNoSMT ) import Test.Tasty.HUnit.Ext -class OnePathRuleBase base where - rewritesTo :: base VariableName -> base VariableName -> OnePathRule +test_simplifyRule :: [TestTree] +test_simplifyRule = + [ testCase "No simplification needed" $ do + let rule = Mock.a `rewritesToOLD` Mock.cf + expected = [rule] -newtype Pair variable = Pair (TermLike variable, Predicate variable) + actual <- runSimplifyRule rule -instance OnePathRuleBase Pair where - Pair (t1, p1) `rewritesTo` Pair (t2, p2) = - OnePathRule RulePattern - { left = t1 - , requires = p1 - , rhs = RHS - { existentials = [] - , right = t2 - , ensures = p2 - } - , antiLeft = Nothing - , attributes = def - } + assertEqual "" expected actual -instance OnePathRuleBase TermLike where - t1 `rewritesTo` t2 = - Pair (t1, makeTruePredicate (termLikeSort t1)) - `rewritesTo` Pair (t2, makeTruePredicate (termLikeSort t2)) + , testCase "Simplify lhs term" $ do + let expected = [Mock.a `rewritesToOLD` Mock.cf] -test_simplifyRule :: [TestTree] -test_simplifyRule = - [ testCase "No simplification needed" $ do + actual <- runSimplifyRule + ( mkAnd Mock.a (mkEquals Mock.testSort Mock.a Mock.a) + `rewritesToOLD` + Mock.cf + ) + + assertEqual "" expected actual + + , testCase "Does not simplify rhs term" $ do + let rule = + Mock.a + `rewritesToOLD` + mkAnd Mock.cf (mkEquals Mock.testSort Mock.a Mock.a) + expected = [rule] + + actual <- runSimplifyRule rule + + assertEqual "" expected actual + + , testCase "Substitution in lhs term" $ do + let expected = [Mock.a `rewritesToOLD` Mock.f Mock.b] + + actual <- runSimplifyRule + ( mkAnd Mock.a (mkEquals Mock.testSort Mock.b x) + `rewritesToOLD` Mock.f x + ) + + assertEqual "" expected actual + + , testCase "Simplifies requires predicate" $ do + let expected = [Mock.a `rewritesToOLD` Mock.cf] + + actual <- runSimplifyRule + ( Pair (Mock.a, makeEqualsPredicate Mock.testSort Mock.b Mock.b) + `rewritesToOLD` + Pair (Mock.cf, makeTruePredicate Mock.testSort) + ) + + assertEqual "" expected actual + + , testCase "Does not simplify ensures predicate" $ do + let rule = + Pair (Mock.a, makeTruePredicate Mock.testSort) + `rewritesToOLD` + Pair (Mock.cf, makeEqualsPredicate Mock.testSort Mock.b Mock.b) + expected = [rule] + + actual <- runSimplifyRule rule + + assertEqual "" expected actual + + , testCase "Substitution in requires predicate" $ do + let expected = [Mock.a `rewritesToOLD` Mock.f Mock.b] + + actual <- runSimplifyRule + ( Pair (Mock.a, makeEqualsPredicate Mock.testSort Mock.b x) + `rewritesToOLD` + Pair (Mock.f x, makeTruePredicate Mock.testSort) + ) + + assertEqual "" expected actual + + , testCase "Splits rule" $ do + let expected = + [ Mock.a `rewritesToOLD` Mock.cf + , Mock.b `rewritesToOLD` Mock.cf + ] + + actual <- runSimplifyRule + ( mkOr Mock.a Mock.b + `rewritesToOLD` + Mock.cf + ) + + assertEqual "" expected actual + , testCase "Case where f(x) is defined;\ + \ Case where it is not is simplified" $ do + let expected = + [ Pair (Mock.f x, makeCeilPredicate Mock.testSort (Mock.f x)) + `rewritesToOLD` + Pair (Mock.a, makeTruePredicate Mock.testSort) + ] + + actual <- runSimplifyRule + ( Pair (Mock.f x, makeTruePredicate Mock.testSort) + `rewritesToOLD` + Pair (Mock.a, makeTruePredicate Mock.testSort) + ) + + assertEqual "" expected actual + , testCase "f(x) is always defined" $ do + let expected = + [ Mock.functional10 x `rewritesToOLD` Mock.a + ] + + actual <- runSimplifyRule + ( Pair (Mock.functional10 x, makeTruePredicate Mock.testSort) + `rewritesToOLD` + Pair (Mock.a, makeTruePredicate Mock.testSort) + ) + + assertEqual "" expected actual + , testCase "Predicate simplification removes trivial claim" $ do + let expected = [] + actual <- runSimplifyRule + ( Pair + ( Mock.b + , makeAndPredicate + (makeNotPredicate + (makeEqualsPredicate Mock.testSort x Mock.b) + ) + (makeNotPredicate + (makeNotPredicate + (makeEqualsPredicate Mock.testSort x Mock.b) + ) + ) + ) + `rewritesToOLD` + Pair (Mock.a, makeTruePredicate Mock.testSort) + ) + assertEqual "" expected actual + , testCase "No simplification needed" $ do let rule = Mock.a `rewritesTo` Mock.cf expected = [rule] @@ -247,8 +370,9 @@ test_simplifyRule = x = mkElemVar Mock.x runSimplifyRule - :: OnePathRule - -> IO [OnePathRule] + :: SimplifyRuleLHS rule + => rule + -> IO [rule] runSimplifyRule rule = fmap MultiAnd.extractPatterns $ runNoSMT @@ -256,8 +380,8 @@ runSimplifyRule rule = SMT.All.declare Mock.smtDeclarations simplifyRuleLhs rule -test_simplifyClaimRule :: [TestTree] -test_simplifyClaimRule = +test_simplifyClaimRuleOLD :: [TestTree] +test_simplifyClaimRuleOLD = [ test "infers definedness" [] rule1 [rule1'] @@ -271,14 +395,14 @@ test_simplifyClaimRule = rule1' = rule1 & requireDefined rule2 = rulePattern @VariableName (Mock.g Mock.a) Mock.b - & Lens.set (field @"requires") requires + & Lens.set (field @"requires") requiresOLD rule2' = rule2 & requireDefined & Lens.set (field @"left") (Mock.f Mock.a) - requires :: Predicate VariableName - requires = makeEqualsPredicate Mock.testSort Mock.a Mock.b + requiresOLD :: Predicate VariableName + requiresOLD = makeEqualsPredicate Mock.testSort Mock.a Mock.b requireDefined rule = Lens.over @@ -298,6 +422,74 @@ test_simplifyClaimRule = -> RulePattern VariableName -> [RulePattern VariableName] -> TestTree + test name replacementsOLD (OLD.OnePathRule -> inputOLD) (map OLD.OnePathRule -> expect) = + -- Test simplifyClaimRule through the OnePathRule instance. + testCase name $ do + actual <- run $ simplifyRuleLhs inputOLD + assertEqual "" expect (MultiAnd.extractPatterns actual) + where + run = + runNoSMT + . runSimplifier env + . flip runReaderT TestEnvOLD { replacementsOLD, inputOLD, requiresOLD } + . runTestSimplifierTOLD + env = + Mock.env + { simplifierCondition = emptyConditionSimplifier + , simplifierAxioms = mempty + } + +test_simplifyClaimRule :: [TestTree] +test_simplifyClaimRule = + [ test "infers definedness" [] + rule1 + [rule1'] + , test "includes side condition" [(Mock.g Mock.a, Mock.f Mock.a)] + rule2 + [rule2'] + ] + where + rule1, rule2, rule2' :: ClaimPattern + rule1 = claimPattern (Pattern.fromTermLike (Mock.f Mock.a)) Mock.b + rule1' = rule1 & requireDefined + rule2 = + claimPattern (Pattern.fromTermLike (Mock.g Mock.a)) Mock.b + & require aEqualsb + rule2' = + claimPattern (Pattern.fromTermLike (Mock.f Mock.a)) Mock.b + & require aEqualsb + & requireDefined + + require condition = + Lens.over + (field @"left") + (flip Pattern.andCondition condition) + + aEqualsb = + makeEqualsPredicate Mock.testSort Mock.a Mock.b + & Condition.fromPredicate + + requireDefined = + Lens.over + (field @"left") + (\left' -> + let leftTerm = Pattern.term left' + leftSort = TermLike.termLikeSort leftTerm + in Pattern.andCondition + left' + ( makeCeilPredicate leftSort leftTerm + & Condition.fromPredicate + ) + ) + + test + :: HasCallStack + => TestName + -> [(TermLike RewritingVariableName, TermLike RewritingVariableName)] + -- ^ replacements + -> ClaimPattern + -> [ClaimPattern] + -> TestTree test name replacements (OnePathRule -> input) (map OnePathRule -> expect) = -- Test simplifyClaimRule through the OnePathRule instance. testCase name $ do @@ -307,7 +499,8 @@ test_simplifyClaimRule = run = runNoSMT . runSimplifier env - . flip runReaderT TestEnv { replacements, input, requires } + . flip runReaderT TestEnv + { replacements, input, requires = aEqualsb } . runTestSimplifierT env = Mock.env @@ -315,11 +508,80 @@ test_simplifyClaimRule = , simplifierAxioms = mempty } +data TestEnvOLD = + TestEnvOLD + { replacementsOLD :: ![(TermLike VariableName, TermLike VariableName)] + , inputOLD :: !OLD.OnePathRule + , requiresOLD :: !(Predicate VariableName) + } + +newtype TestSimplifierTOLD m a = + TestSimplifierTOLD { runTestSimplifierTOLD :: ReaderT TestEnvOLD m a } + deriving (Functor, Applicative, Monad) + deriving (MonadReader TestEnvOLD) + deriving (MonadLog, MonadSMT) + +instance MonadTrans TestSimplifierTOLD where + lift = TestSimplifierTOLD . lift + +instance MFunctor TestSimplifierTOLD where + hoist f = TestSimplifierTOLD . hoist f . runTestSimplifierTOLD + +instance MonadSimplify m => MonadSimplify (TestSimplifierTOLD m) where + simplifyTermLike sideCondition termLike = do + TestEnvOLD { replacementsOLD, inputOLD, requiresOLD } <- Reader.ask + let rule = OLD.getOnePathRule inputOLD + left = Lens.view (field @"left") rule + sort = termLikeSort left + expectSideCondition = + makeAndPredicate requiresOLD (makeCeilPredicate sort left) + & liftPredicate + & Predicate.coerceSort predicateSort + & Condition.fromPredicate + & SideCondition.fromCondition + satisfied = sideCondition == expectSideCondition + return + . OrPattern.fromTermLike + . (if satisfied then applyReplacements replacementsOLD else id) + $ termLike + where + applyReplacements + :: InternalVariable variable + => [(TermLike VariableName, TermLike VariableName)] + -> TermLike variable + -> TermLike variable + applyReplacements replacements zero = + Foldable.foldl' applyReplacement zero + $ map liftReplacement replacements + + applyReplacement orig (ini, fin) + | orig == ini = fin + | otherwise = orig + + liftPredicate + :: InternalVariable variable + => Predicate VariableName + -> Predicate variable + liftPredicate = Predicate.mapVariables (pure fromVariableName) + + liftTermLike + :: InternalVariable variable + => TermLike VariableName + -> TermLike variable + liftTermLike = TermLike.mapVariables (pure fromVariableName) + + liftReplacement + :: InternalVariable variable + => (TermLike VariableName, TermLike VariableName) + -> (TermLike variable, TermLike variable) + liftReplacement = Bifunctor.bimap liftTermLike liftTermLike + data TestEnv = TestEnv - { replacements :: ![(TermLike VariableName, TermLike VariableName)] + { replacements + :: ![(TermLike RewritingVariableName, TermLike RewritingVariableName)] , input :: !OnePathRule - , requires :: !(Predicate VariableName) + , requires :: !(Condition RewritingVariableName) } newtype TestSimplifierT m a = @@ -338,10 +600,14 @@ instance MonadSimplify m => MonadSimplify (TestSimplifierT m) where simplifyTermLike sideCondition termLike = do TestEnv { replacements, input, requires } <- Reader.ask let rule = getOnePathRule input - left = Lens.view (field @"left") rule - sort = termLikeSort left + leftTerm = + Lens.view (field @"left") rule + & Pattern.term + sort = termLikeSort leftTerm expectSideCondition = - makeAndPredicate requires (makeCeilPredicate sort left) + makeAndPredicate + (Condition.toPredicate requires) + (makeCeilPredicate sort leftTerm) & liftPredicate & Predicate.coerceSort predicateSort & Condition.fromPredicate @@ -354,12 +620,12 @@ instance MonadSimplify m => MonadSimplify (TestSimplifierT m) where where applyReplacements :: InternalVariable variable - => [(TermLike VariableName, TermLike VariableName)] + => [(TermLike RewritingVariableName, TermLike RewritingVariableName)] -> TermLike variable -> TermLike variable applyReplacements replacements zero = Foldable.foldl' applyReplacement zero - $ map liftReplacement replacements + $ fmap liftReplacement replacements applyReplacement orig (ini, fin) | orig == ini = fin @@ -367,18 +633,26 @@ instance MonadSimplify m => MonadSimplify (TestSimplifierT m) where liftPredicate :: InternalVariable variable - => Predicate VariableName + => Predicate RewritingVariableName -> Predicate variable - liftPredicate = Predicate.mapVariables (pure fromVariableName) + liftPredicate = + Predicate.mapVariables liftRewritingVariable liftTermLike :: InternalVariable variable - => TermLike VariableName + => TermLike RewritingVariableName -> TermLike variable - liftTermLike = TermLike.mapVariables (pure fromVariableName) + liftTermLike = + TermLike.mapVariables liftRewritingVariable liftReplacement :: InternalVariable variable - => (TermLike VariableName, TermLike VariableName) + => (TermLike RewritingVariableName, TermLike RewritingVariableName) -> (TermLike variable, TermLike variable) liftReplacement = Bifunctor.bimap liftTermLike liftTermLike + + liftRewritingVariable + :: InternalVariable variable + => AdjSomeVariableName (RewritingVariableName -> variable) + liftRewritingVariable = + pure (.) <*> pure fromVariableName <*> getRewritingVariable From 81cd44988f66ac8018e31cb018d9686209c85cce Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 28 Jul 2020 16:50:40 +0300 Subject: [PATCH 16/27] Test.Step.Rule: fix sort issues --- kore/test/Test/Kore/Step/Rule/Common.hs | 72 +++++++- kore/test/Test/Kore/Step/Rule/Expand.hs | 13 +- kore/test/Test/Kore/Step/Rule/Simplify.hs | 191 +++++++++++++--------- 3 files changed, 190 insertions(+), 86 deletions(-) diff --git a/kore/test/Test/Kore/Step/Rule/Common.hs b/kore/test/Test/Kore/Step/Rule/Common.hs index 25df1d85a2..8483c77942 100644 --- a/kore/test/Test/Kore/Step/Rule/Common.hs +++ b/kore/test/Test/Kore/Step/Rule/Common.hs @@ -1,7 +1,7 @@ module Test.Kore.Step.Rule.Common ( Pair (..) + , RuleBase (..) , rewritesToOLD - , rewritesTo ) where import Prelude.Kore @@ -14,6 +14,7 @@ import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.Predicate ( Predicate , makeTruePredicate + , makeTruePredicate_ ) import qualified Kore.Internal.Predicate as Predicate import Kore.Internal.TermLike @@ -30,6 +31,7 @@ import Kore.Step.ClaimPattern ) import Kore.Step.RulePattern ( RHS (RHS) + , RewriteRule (RewriteRule) , RulePattern (RulePattern) ) import qualified Kore.Step.RulePattern as OLD @@ -55,13 +57,14 @@ instance OnePathRuleBaseOLD Pair where instance OnePathRuleBaseOLD TermLike where t1 `rewritesToOLD` t2 = - Pair (t1, makeTruePredicate (TermLike.termLikeSort t1)) - `rewritesToOLD` Pair (t2, makeTruePredicate (TermLike.termLikeSort t2)) + Pair (t1, makeTruePredicate_) + `rewritesToOLD` Pair (t2, makeTruePredicate_) -class OnePathRuleBase base where - rewritesTo :: base VariableName -> base VariableName -> OnePathRule +class RuleBase base rule where + rewritesTo :: base VariableName -> base VariableName -> rule + rewritesToWithSort :: base VariableName -> base VariableName -> rule -instance OnePathRuleBase Pair where +instance RuleBase Pair OnePathRule where Pair (t1, p1) `rewritesTo` Pair (t2, p2) = OnePathRule $ claimPatternInternal @@ -74,8 +77,61 @@ instance OnePathRuleBase Pair where p1' = Predicate.mapVariables (pure mkRuleVariable) p1 p2' = Predicate.mapVariables (pure mkRuleVariable) p2 -instance OnePathRuleBase TermLike where + rewritesToWithSort = rewritesTo + +instance RuleBase TermLike OnePathRule where t1 `rewritesTo` t2 = + Pair (t1, makeTruePredicate_) + `rewritesTo` Pair (t2, makeTruePredicate_) + + t1 `rewritesToWithSort` t2 = Pair (t1, makeTruePredicate (TermLike.termLikeSort t1)) - `rewritesTo` Pair (t2, makeTruePredicate (TermLike.termLikeSort t2)) + `rewritesToWithSort` Pair (t2, makeTruePredicate (TermLike.termLikeSort t2)) + +instance RuleBase Pair (RewriteRule VariableName) where + Pair (t1, p1) `rewritesTo` Pair (t2, p2) = + RewriteRule RulePattern + { OLD.left = t1 + , OLD.requires = p1 + , OLD.rhs = RHS + { OLD.existentials = [] + , OLD.right = t2 + , OLD.ensures = p2 + } + , OLD.antiLeft = Nothing + , OLD.attributes = Default.def + } + rewritesToWithSort = rewritesTo + +instance RuleBase TermLike (RewriteRule VariableName) where + t1 `rewritesTo` t2 = + Pair (t1, makeTruePredicate_) + `rewritesTo` Pair (t2, makeTruePredicate_) + t1 `rewritesToWithSort` t2 = + Pair (t1, makeTruePredicate (TermLike.termLikeSort t1)) + `rewritesToWithSort` Pair (t2, makeTruePredicate (TermLike.termLikeSort t2)) + +instance RuleBase Pair OLD.OnePathRule where + Pair (t1, p1) `rewritesTo` Pair (t2, p2) = + OLD.OnePathRule RulePattern + { OLD.left = t1 + , OLD.requires = p1 + , OLD.rhs = RHS + { OLD.existentials = [] + , OLD.right = t2 + , OLD.ensures = p2 + } + , OLD.antiLeft = Nothing + , OLD.attributes = Default.def + } + rewritesToWithSort = rewritesTo + +instance RuleBase TermLike OLD.OnePathRule where + t1 `rewritesTo` t2 = + Pair (t1, makeTruePredicate_) + `rewritesTo` Pair (t2, makeTruePredicate_) + + t1 `rewritesToWithSort` t2 = + Pair (t1, makeTruePredicate (TermLike.termLikeSort t1)) + `rewritesToWithSort` Pair (t2, makeTruePredicate (TermLike.termLikeSort t2)) diff --git a/kore/test/Test/Kore/Step/Rule/Expand.hs b/kore/test/Test/Kore/Step/Rule/Expand.hs index e7b3a6c3e0..27f5528b65 100644 --- a/kore/test/Test/Kore/Step/Rule/Expand.hs +++ b/kore/test/Test/Kore/Step/Rule/Expand.hs @@ -46,6 +46,9 @@ import Kore.Internal.TermLike , mkApplySymbol , mkElemVar ) +import Kore.Step.ClaimPattern + ( OnePathRule + ) import Kore.Step.Rule.Expand import Kore.Syntax.Id ( Id @@ -58,9 +61,10 @@ import Test.Kore import qualified Test.Kore.Step.MockSymbols as Mock import Test.Kore.Step.Rule.Common ( Pair (..) - , rewritesTo + , RuleBase , rewritesToOLD ) +import qualified Test.Kore.Step.Rule.Common as Common import Test.Kore.With ( with ) @@ -398,6 +402,13 @@ test_expandRule = in assertEqual "" expected actual ] where + rewritesTo + :: RuleBase base OnePathRule + => base VariableName + -> base VariableName + -> OnePathRule + rewritesTo = Common.rewritesTo + x = mkElemVar Mock.x x0 = mkElemVar Mock.x0 diff --git a/kore/test/Test/Kore/Step/Rule/Simplify.hs b/kore/test/Test/Kore/Step/Rule/Simplify.hs index 950de6abb9..3a88797ffb 100644 --- a/kore/test/Test/Kore/Step/Rule/Simplify.hs +++ b/kore/test/Test/Kore/Step/Rule/Simplify.hs @@ -1,5 +1,7 @@ module Test.Kore.Step.Rule.Simplify - ( test_simplifyRule + ( test_simplifyRule_RewriteRule + , test_simplifyRule_OnePathRule + , test_simplifyRule_OnePathRuleOLD , test_simplifyClaimRuleOLD , test_simplifyClaimRule ) where @@ -68,7 +70,8 @@ import Kore.Step.ClaimPattern ) import Kore.Step.Rule.Simplify import Kore.Step.RulePattern - ( RulePattern + ( RewriteRule + , RulePattern , rulePattern ) import qualified Kore.Step.RulePattern as OLD @@ -91,18 +94,18 @@ import Kore.Syntax.Variable import qualified Test.Kore.Step.MockSymbols as Mock import Test.Kore.Step.Rule.Common ( Pair (..) - , rewritesTo - , rewritesToOLD + , RuleBase ) +import qualified Test.Kore.Step.Rule.Common as Common import Test.SMT ( runNoSMT ) import Test.Tasty.HUnit.Ext -test_simplifyRule :: [TestTree] -test_simplifyRule = +test_simplifyRule_RewriteRule :: [TestTree] +test_simplifyRule_RewriteRule = [ testCase "No simplification needed" $ do - let rule = Mock.a `rewritesToOLD` Mock.cf + let rule = Mock.a `rewritesToWithSort` Mock.cf expected = [rule] actual <- runSimplifyRule rule @@ -110,11 +113,11 @@ test_simplifyRule = assertEqual "" expected actual , testCase "Simplify lhs term" $ do - let expected = [Mock.a `rewritesToOLD` Mock.cf] + let expected = [Mock.a `rewritesToWithSort` Mock.cf] actual <- runSimplifyRule ( mkAnd Mock.a (mkEquals Mock.testSort Mock.a Mock.a) - `rewritesToOLD` + `rewritesToWithSort` Mock.cf ) @@ -123,7 +126,7 @@ test_simplifyRule = , testCase "Does not simplify rhs term" $ do let rule = Mock.a - `rewritesToOLD` + `rewritesToWithSort` mkAnd Mock.cf (mkEquals Mock.testSort Mock.a Mock.a) expected = [rule] @@ -132,22 +135,11 @@ test_simplifyRule = assertEqual "" expected actual , testCase "Substitution in lhs term" $ do - let expected = [Mock.a `rewritesToOLD` Mock.f Mock.b] + let expected = [Mock.a `rewritesToWithSort` Mock.f Mock.b] actual <- runSimplifyRule ( mkAnd Mock.a (mkEquals Mock.testSort Mock.b x) - `rewritesToOLD` Mock.f x - ) - - assertEqual "" expected actual - - , testCase "Simplifies requires predicate" $ do - let expected = [Mock.a `rewritesToOLD` Mock.cf] - - actual <- runSimplifyRule - ( Pair (Mock.a, makeEqualsPredicate Mock.testSort Mock.b Mock.b) - `rewritesToOLD` - Pair (Mock.cf, makeTruePredicate Mock.testSort) + `rewritesToWithSort` Mock.f x ) assertEqual "" expected actual @@ -155,7 +147,7 @@ test_simplifyRule = , testCase "Does not simplify ensures predicate" $ do let rule = Pair (Mock.a, makeTruePredicate Mock.testSort) - `rewritesToOLD` + `rewritesToWithSort` Pair (Mock.cf, makeEqualsPredicate Mock.testSort Mock.b Mock.b) expected = [rule] @@ -163,58 +155,45 @@ test_simplifyRule = assertEqual "" expected actual - , testCase "Substitution in requires predicate" $ do - let expected = [Mock.a `rewritesToOLD` Mock.f Mock.b] - - actual <- runSimplifyRule - ( Pair (Mock.a, makeEqualsPredicate Mock.testSort Mock.b x) - `rewritesToOLD` - Pair (Mock.f x, makeTruePredicate Mock.testSort) - ) - - assertEqual "" expected actual - , testCase "Splits rule" $ do let expected = - [ Mock.a `rewritesToOLD` Mock.cf - , Mock.b `rewritesToOLD` Mock.cf + [ Mock.a `rewritesToWithSort` Mock.cf + , Mock.b `rewritesToWithSort` Mock.cf ] actual <- runSimplifyRule ( mkOr Mock.a Mock.b - `rewritesToOLD` + `rewritesToWithSort` Mock.cf ) - assertEqual "" expected actual - , testCase "Case where f(x) is defined;\ - \ Case where it is not is simplified" $ do - let expected = - [ Pair (Mock.f x, makeCeilPredicate Mock.testSort (Mock.f x)) - `rewritesToOLD` - Pair (Mock.a, makeTruePredicate Mock.testSort) - ] - - actual <- runSimplifyRule - ( Pair (Mock.f x, makeTruePredicate Mock.testSort) - `rewritesToOLD` - Pair (Mock.a, makeTruePredicate Mock.testSort) - ) - assertEqual "" expected actual , testCase "f(x) is always defined" $ do let expected = - [ Mock.functional10 x `rewritesToOLD` Mock.a + [ Mock.functional10 x `rewritesToWithSort` Mock.a ] actual <- runSimplifyRule ( Pair (Mock.functional10 x, makeTruePredicate Mock.testSort) - `rewritesToOLD` + `rewritesToWithSort` Pair (Mock.a, makeTruePredicate Mock.testSort) ) assertEqual "" expected actual - , testCase "Predicate simplification removes trivial claim" $ do + ] + where + rewritesToWithSort + :: RuleBase base (RewriteRule VariableName) + => base VariableName + -> base VariableName + -> RewriteRule VariableName + rewritesToWithSort = Common.rewritesToWithSort + + x = mkElemVar Mock.x + +test_simplifyRule_OnePathRuleOLD :: [TestTree] +test_simplifyRule_OnePathRuleOLD = + [ testCase "Predicate simplification removes trivial claim" $ do let expected = [] actual <- runSimplifyRule ( Pair @@ -229,12 +208,63 @@ test_simplifyRule = ) ) ) - `rewritesToOLD` + `rewritesToWithSort` Pair (Mock.a, makeTruePredicate Mock.testSort) ) assertEqual "" expected actual - , testCase "No simplification needed" $ do - let rule = Mock.a `rewritesTo` Mock.cf + + , testCase "Case where f(x) is defined;\ + \ Case where it is not is simplified" $ do + let expected = + [ Pair (Mock.f x, makeCeilPredicate Mock.testSort (Mock.f x)) + `rewritesToWithSort` + Pair (Mock.a, makeTruePredicate Mock.testSort) + ] + + actual <- runSimplifyRule + ( Pair (Mock.f x, makeTruePredicate Mock.testSort) + `rewritesToWithSort` + Pair (Mock.a, makeTruePredicate Mock.testSort) + ) + + assertEqual "" expected actual + + , testCase "Substitution in requires predicate" $ do + let expected = [Mock.a `rewritesToWithSort` Mock.f Mock.b] + + actual <- runSimplifyRule + ( Pair (Mock.a, makeEqualsPredicate Mock.testSort Mock.b x) + `rewritesToWithSort` + Pair (Mock.f x, makeTruePredicate Mock.testSort) + ) + + assertEqual "" expected actual + + , testCase "Simplifies requires predicate" $ do + let expected = [Mock.a `rewritesToWithSort` Mock.cf] + + actual <- runSimplifyRule + ( Pair (Mock.a, makeEqualsPredicate Mock.testSort Mock.b Mock.b) + `rewritesToWithSort` + Pair (Mock.cf, makeTruePredicate Mock.testSort) + ) + + assertEqual "" expected actual + ] + where + rewritesToWithSort + :: RuleBase base OLD.OnePathRule + => base VariableName + -> base VariableName + -> OLD.OnePathRule + rewritesToWithSort = Common.rewritesToWithSort + + x = mkElemVar Mock.x + +test_simplifyRule_OnePathRule :: [TestTree] +test_simplifyRule_OnePathRule = + [ testCase "No simplification needed" $ do + let rule = Mock.a `rewritesToWithSort` Mock.cf expected = [rule] actual <- runSimplifyRule rule @@ -242,11 +272,11 @@ test_simplifyRule = assertEqual "" expected actual , testCase "Simplify lhs term" $ do - let expected = [Mock.a `rewritesTo` Mock.cf] + let expected = [Mock.a `rewritesToWithSort` Mock.cf] actual <- runSimplifyRule ( mkAnd Mock.a (mkEquals Mock.testSort Mock.a Mock.a) - `rewritesTo` + `rewritesToWithSort` Mock.cf ) @@ -255,7 +285,7 @@ test_simplifyRule = , testCase "Does not simplify rhs term" $ do let rule = Mock.a - `rewritesTo` + `rewritesToWithSort` mkAnd Mock.cf (mkEquals Mock.testSort Mock.a Mock.a) expected = [rule] @@ -264,21 +294,21 @@ test_simplifyRule = assertEqual "" expected actual , testCase "Substitution in lhs term" $ do - let expected = [Mock.a `rewritesTo` Mock.f Mock.b] + let expected = [Mock.a `rewritesToWithSort` Mock.f Mock.b] actual <- runSimplifyRule ( mkAnd Mock.a (mkEquals Mock.testSort Mock.b x) - `rewritesTo` Mock.f x + `rewritesToWithSort` Mock.f x ) assertEqual "" expected actual , testCase "Simplifies requires predicate" $ do - let expected = [Mock.a `rewritesTo` Mock.cf] + let expected = [Mock.a `rewritesToWithSort` Mock.cf] actual <- runSimplifyRule ( Pair (Mock.a, makeEqualsPredicate Mock.testSort Mock.b Mock.b) - `rewritesTo` + `rewritesToWithSort` Pair (Mock.cf, makeTruePredicate Mock.testSort) ) @@ -287,7 +317,7 @@ test_simplifyRule = , testCase "Does not simplify ensures predicate" $ do let rule = Pair (Mock.a, makeTruePredicate Mock.testSort) - `rewritesTo` + `rewritesToWithSort` Pair (Mock.cf, makeEqualsPredicate Mock.testSort Mock.b Mock.b) expected = [rule] @@ -296,11 +326,11 @@ test_simplifyRule = assertEqual "" expected actual , testCase "Substitution in requires predicate" $ do - let expected = [Mock.a `rewritesTo` Mock.f Mock.b] + let expected = [Mock.a `rewritesToWithSort` Mock.f Mock.b] actual <- runSimplifyRule ( Pair (Mock.a, makeEqualsPredicate Mock.testSort Mock.b x) - `rewritesTo` + `rewritesToWithSort` Pair (Mock.f x, makeTruePredicate Mock.testSort) ) @@ -308,13 +338,13 @@ test_simplifyRule = , testCase "Splits rule" $ do let expected = - [ Mock.a `rewritesTo` Mock.cf - , Mock.b `rewritesTo` Mock.cf + [ Mock.a `rewritesToWithSort` Mock.cf + , Mock.b `rewritesToWithSort` Mock.cf ] actual <- runSimplifyRule ( mkOr Mock.a Mock.b - `rewritesTo` + `rewritesToWithSort` Mock.cf ) @@ -323,25 +353,25 @@ test_simplifyRule = \ Case where it is not is simplified" $ do let expected = [ Pair (Mock.f x, makeCeilPredicate Mock.testSort (Mock.f x)) - `rewritesTo` + `rewritesToWithSort` Pair (Mock.a, makeTruePredicate Mock.testSort) ] actual <- runSimplifyRule ( Pair (Mock.f x, makeTruePredicate Mock.testSort) - `rewritesTo` + `rewritesToWithSort` Pair (Mock.a, makeTruePredicate Mock.testSort) ) assertEqual "" expected actual , testCase "f(x) is always defined" $ do let expected = - [ Mock.functional10 x `rewritesTo` Mock.a + [ Mock.functional10 x `rewritesToWithSort` Mock.a ] actual <- runSimplifyRule ( Pair (Mock.functional10 x, makeTruePredicate Mock.testSort) - `rewritesTo` + `rewritesToWithSort` Pair (Mock.a, makeTruePredicate Mock.testSort) ) @@ -361,12 +391,19 @@ test_simplifyRule = ) ) ) - `rewritesTo` + `rewritesToWithSort` Pair (Mock.a, makeTruePredicate Mock.testSort) ) assertEqual "" expected actual ] where + rewritesToWithSort + :: RuleBase base OnePathRule + => base VariableName + -> base VariableName + -> OnePathRule + rewritesToWithSort = Common.rewritesToWithSort + x = mkElemVar Mock.x runSimplifyRule From f25410b87036492aeea398179437d46c3c805634 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 28 Jul 2020 16:54:00 +0300 Subject: [PATCH 17/27] Test.Step.Rule: remove class specific to old OnePathRule --- kore/test/Test/Kore/Step/Rule/Common.hs | 23 ----------------------- kore/test/Test/Kore/Step/Rule/Expand.hs | 9 ++++++++- 2 files changed, 8 insertions(+), 24 deletions(-) diff --git a/kore/test/Test/Kore/Step/Rule/Common.hs b/kore/test/Test/Kore/Step/Rule/Common.hs index 8483c77942..95652c330c 100644 --- a/kore/test/Test/Kore/Step/Rule/Common.hs +++ b/kore/test/Test/Kore/Step/Rule/Common.hs @@ -1,7 +1,6 @@ module Test.Kore.Step.Rule.Common ( Pair (..) , RuleBase (..) - , rewritesToOLD ) where import Prelude.Kore @@ -38,28 +37,6 @@ import qualified Kore.Step.RulePattern as OLD newtype Pair variable = Pair (TermLike variable, Predicate variable) -class OnePathRuleBaseOLD base where - rewritesToOLD :: base VariableName -> base VariableName -> OLD.OnePathRule - -instance OnePathRuleBaseOLD Pair where - Pair (t1, p1) `rewritesToOLD` Pair (t2, p2) = - OLD.OnePathRule RulePattern - { OLD.left = t1 - , OLD.requires = p1 - , OLD.rhs = RHS - { OLD.existentials = [] - , OLD.right = t2 - , OLD.ensures = p2 - } - , OLD.antiLeft = Nothing - , OLD.attributes = Default.def - } - -instance OnePathRuleBaseOLD TermLike where - t1 `rewritesToOLD` t2 = - Pair (t1, makeTruePredicate_) - `rewritesToOLD` Pair (t2, makeTruePredicate_) - class RuleBase base rule where rewritesTo :: base VariableName -> base VariableName -> rule rewritesToWithSort :: base VariableName -> base VariableName -> rule diff --git a/kore/test/Test/Kore/Step/Rule/Expand.hs b/kore/test/Test/Kore/Step/Rule/Expand.hs index 27f5528b65..2757fde7b3 100644 --- a/kore/test/Test/Kore/Step/Rule/Expand.hs +++ b/kore/test/Test/Kore/Step/Rule/Expand.hs @@ -50,6 +50,7 @@ import Kore.Step.ClaimPattern ( OnePathRule ) import Kore.Step.Rule.Expand +import qualified Kore.Step.RulePattern as OLD import Kore.Syntax.Id ( Id ) @@ -62,7 +63,6 @@ import qualified Test.Kore.Step.MockSymbols as Mock import Test.Kore.Step.Rule.Common ( Pair (..) , RuleBase - , rewritesToOLD ) import qualified Test.Kore.Step.Rule.Common as Common import Test.Kore.With @@ -409,6 +409,13 @@ test_expandRule = -> OnePathRule rewritesTo = Common.rewritesTo + rewritesToOLD + :: RuleBase base OLD.OnePathRule + => base VariableName + -> base VariableName + -> OLD.OnePathRule + rewritesToOLD = Common.rewritesTo + x = mkElemVar Mock.x x0 = mkElemVar Mock.x0 From 4e27c0836558cfc3b835c79750a0814ef58b0706 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 28 Jul 2020 18:01:19 +0300 Subject: [PATCH 18/27] Test.Step.Rule.Simplify: hlint workaround --- kore/test/Test/Kore/Step/Rule/Simplify.hs | 28 +++++++++++------------ 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/kore/test/Test/Kore/Step/Rule/Simplify.hs b/kore/test/Test/Kore/Step/Rule/Simplify.hs index 3a88797ffb..3fe98426f1 100644 --- a/kore/test/Test/Kore/Step/Rule/Simplify.hs +++ b/kore/test/Test/Kore/Step/Rule/Simplify.hs @@ -105,7 +105,7 @@ import Test.Tasty.HUnit.Ext test_simplifyRule_RewriteRule :: [TestTree] test_simplifyRule_RewriteRule = [ testCase "No simplification needed" $ do - let rule = Mock.a `rewritesToWithSort` Mock.cf + let rule = Mock.a `rewritesToWithSortRewriteRule` Mock.cf expected = [rule] actual <- runSimplifyRule rule @@ -113,11 +113,11 @@ test_simplifyRule_RewriteRule = assertEqual "" expected actual , testCase "Simplify lhs term" $ do - let expected = [Mock.a `rewritesToWithSort` Mock.cf] + let expected = [Mock.a `rewritesToWithSortRewriteRule` Mock.cf] actual <- runSimplifyRule ( mkAnd Mock.a (mkEquals Mock.testSort Mock.a Mock.a) - `rewritesToWithSort` + `rewritesToWithSortRewriteRule` Mock.cf ) @@ -126,7 +126,7 @@ test_simplifyRule_RewriteRule = , testCase "Does not simplify rhs term" $ do let rule = Mock.a - `rewritesToWithSort` + `rewritesToWithSortRewriteRule` mkAnd Mock.cf (mkEquals Mock.testSort Mock.a Mock.a) expected = [rule] @@ -135,11 +135,11 @@ test_simplifyRule_RewriteRule = assertEqual "" expected actual , testCase "Substitution in lhs term" $ do - let expected = [Mock.a `rewritesToWithSort` Mock.f Mock.b] + let expected = [Mock.a `rewritesToWithSortRewriteRule` Mock.f Mock.b] actual <- runSimplifyRule ( mkAnd Mock.a (mkEquals Mock.testSort Mock.b x) - `rewritesToWithSort` Mock.f x + `rewritesToWithSortRewriteRule` Mock.f x ) assertEqual "" expected actual @@ -147,7 +147,7 @@ test_simplifyRule_RewriteRule = , testCase "Does not simplify ensures predicate" $ do let rule = Pair (Mock.a, makeTruePredicate Mock.testSort) - `rewritesToWithSort` + `rewritesToWithSortRewriteRule` Pair (Mock.cf, makeEqualsPredicate Mock.testSort Mock.b Mock.b) expected = [rule] @@ -157,37 +157,37 @@ test_simplifyRule_RewriteRule = , testCase "Splits rule" $ do let expected = - [ Mock.a `rewritesToWithSort` Mock.cf - , Mock.b `rewritesToWithSort` Mock.cf + [ Mock.a `rewritesToWithSortRewriteRule` Mock.cf + , Mock.b `rewritesToWithSortRewriteRule` Mock.cf ] actual <- runSimplifyRule ( mkOr Mock.a Mock.b - `rewritesToWithSort` + `rewritesToWithSortRewriteRule` Mock.cf ) assertEqual "" expected actual , testCase "f(x) is always defined" $ do let expected = - [ Mock.functional10 x `rewritesToWithSort` Mock.a + [ Mock.functional10 x `rewritesToWithSortRewriteRule` Mock.a ] actual <- runSimplifyRule ( Pair (Mock.functional10 x, makeTruePredicate Mock.testSort) - `rewritesToWithSort` + `rewritesToWithSortRewriteRule` Pair (Mock.a, makeTruePredicate Mock.testSort) ) assertEqual "" expected actual ] where - rewritesToWithSort + rewritesToWithSortRewriteRule :: RuleBase base (RewriteRule VariableName) => base VariableName -> base VariableName -> RewriteRule VariableName - rewritesToWithSort = Common.rewritesToWithSort + rewritesToWithSortRewriteRule = Common.rewritesToWithSort x = mkElemVar Mock.x From c263eee27e70f4683e7ab2d619e2451a76d355ca Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 28 Jul 2020 18:05:11 +0300 Subject: [PATCH 19/27] Test.Step.Rule.Simplify: hlint workaround --- kore/test/Test/Kore/Step/Rule/Simplify.hs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/kore/test/Test/Kore/Step/Rule/Simplify.hs b/kore/test/Test/Kore/Step/Rule/Simplify.hs index 3fe98426f1..a4f1f53348 100644 --- a/kore/test/Test/Kore/Step/Rule/Simplify.hs +++ b/kore/test/Test/Kore/Step/Rule/Simplify.hs @@ -208,7 +208,7 @@ test_simplifyRule_OnePathRuleOLD = ) ) ) - `rewritesToWithSort` + `rewritesToWithSortOLD` Pair (Mock.a, makeTruePredicate Mock.testSort) ) assertEqual "" expected actual @@ -217,47 +217,47 @@ test_simplifyRule_OnePathRuleOLD = \ Case where it is not is simplified" $ do let expected = [ Pair (Mock.f x, makeCeilPredicate Mock.testSort (Mock.f x)) - `rewritesToWithSort` + `rewritesToWithSortOLD` Pair (Mock.a, makeTruePredicate Mock.testSort) ] actual <- runSimplifyRule ( Pair (Mock.f x, makeTruePredicate Mock.testSort) - `rewritesToWithSort` + `rewritesToWithSortOLD` Pair (Mock.a, makeTruePredicate Mock.testSort) ) assertEqual "" expected actual , testCase "Substitution in requires predicate" $ do - let expected = [Mock.a `rewritesToWithSort` Mock.f Mock.b] + let expected = [Mock.a `rewritesToWithSortOLD` Mock.f Mock.b] actual <- runSimplifyRule ( Pair (Mock.a, makeEqualsPredicate Mock.testSort Mock.b x) - `rewritesToWithSort` + `rewritesToWithSortOLD` Pair (Mock.f x, makeTruePredicate Mock.testSort) ) assertEqual "" expected actual , testCase "Simplifies requires predicate" $ do - let expected = [Mock.a `rewritesToWithSort` Mock.cf] + let expected = [Mock.a `rewritesToWithSortOLD` Mock.cf] actual <- runSimplifyRule ( Pair (Mock.a, makeEqualsPredicate Mock.testSort Mock.b Mock.b) - `rewritesToWithSort` + `rewritesToWithSortOLD` Pair (Mock.cf, makeTruePredicate Mock.testSort) ) assertEqual "" expected actual ] where - rewritesToWithSort + rewritesToWithSortOLD :: RuleBase base OLD.OnePathRule => base VariableName -> base VariableName -> OLD.OnePathRule - rewritesToWithSort = Common.rewritesToWithSort + rewritesToWithSortOLD = Common.rewritesToWithSort x = mkElemVar Mock.x From cdfd7eedd212b8d616dd27bf051fc72370f5f30f Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 28 Jul 2020 18:24:43 +0300 Subject: [PATCH 20/27] Test.Step.Rule.Simplify: fix unit test --- kore/test/Test/Kore/Step/Rule/Simplify.hs | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/kore/test/Test/Kore/Step/Rule/Simplify.hs b/kore/test/Test/Kore/Step/Rule/Simplify.hs index a4f1f53348..a3de77b761 100644 --- a/kore/test/Test/Kore/Step/Rule/Simplify.hs +++ b/kore/test/Test/Kore/Step/Rule/Simplify.hs @@ -422,7 +422,7 @@ test_simplifyClaimRuleOLD = [ test "infers definedness" [] rule1 [rule1'] - , test "includes side condition" [(Mock.g Mock.a, Mock.f Mock.a)] + , test "TESTING includes side condition" [(Mock.g Mock.a, Mock.f Mock.a)] rule2 [rule2'] ] @@ -481,7 +481,7 @@ test_simplifyClaimRule = [ test "infers definedness" [] rule1 [rule1'] - , test "includes side condition" [(Mock.g Mock.a, Mock.f Mock.a)] + , test "TESTING includes side condition" [(Mock.g Mock.a, Mock.f Mock.a)] rule2 [rule2'] ] @@ -493,9 +493,15 @@ test_simplifyClaimRule = claimPattern (Pattern.fromTermLike (Mock.g Mock.a)) Mock.b & require aEqualsb rule2' = - claimPattern (Pattern.fromTermLike (Mock.f Mock.a)) Mock.b - & require aEqualsb + rule2 & requireDefined + & Lens.over + (field @"left") + (\patt -> + Pattern.andCondition + (Mock.f Mock.a & Pattern.fromTermLike) + (Pattern.withoutTerm patt) + ) require condition = Lens.over From 49d435cb2553e0e03e51fabab5f643c9ded3ae93 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 28 Jul 2020 18:30:07 +0300 Subject: [PATCH 21/27] HLint --- kore/test/Test/Kore/Step/Rule/Simplify.hs | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/kore/test/Test/Kore/Step/Rule/Simplify.hs b/kore/test/Test/Kore/Step/Rule/Simplify.hs index a3de77b761..b5e588d645 100644 --- a/kore/test/Test/Kore/Step/Rule/Simplify.hs +++ b/kore/test/Test/Kore/Step/Rule/Simplify.hs @@ -497,10 +497,9 @@ test_simplifyClaimRule = & requireDefined & Lens.over (field @"left") - (\patt -> - Pattern.andCondition - (Mock.f Mock.a & Pattern.fromTermLike) - (Pattern.withoutTerm patt) + ( Pattern.andCondition + (Mock.f Mock.a & Pattern.fromTermLike) + . Pattern.withoutTerm ) require condition = From 82c6c6c0c0ed47d24b53d049a996adb1d9e1eb83 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 28 Jul 2020 18:38:42 +0300 Subject: [PATCH 22/27] Clean-up --- kore/src/Kore/Step/ClaimPattern.hs | 6 +++--- kore/test/Test/Kore/Step/Rule/Simplify.hs | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs index 93a7f267b3..40aafa133a 100644 --- a/kore/src/Kore/Step/ClaimPattern.hs +++ b/kore/src/Kore/Step/ClaimPattern.hs @@ -248,7 +248,7 @@ applySubstitution substitution claim = finalClaim = substitute subst claim substitutedVariables = Substitution.variables substitution --- |Is the rule free of the given variables? +-- | Is the rule free of the given variables? isFreeOf :: ClaimPattern -> Set.Set (SomeVariable RewritingVariableName) @@ -259,7 +259,7 @@ isFreeOf rule = $ freeVariables rule -- TODO(Ana): move this to Internal.TermLike? --- | Extracts all top level existential quantifications +-- | Extracts all top level existential quantifications. termToExistentials :: TermLike RewritingVariableName -> [ElementVariable RewritingVariableName] @@ -366,7 +366,7 @@ instance From AllPathRule Attribute.RuleIndex where instance From AllPathRule Attribute.Trusted where from = Attribute.trusted . attributes . getAllPathRule --- | Converts a 'AllPathRule' into its term representation. +-- | Converts an 'AllPathRule' into its term representation. -- This is intended to be used only in unparsing situations, -- as some of the variable information related to the -- rewriting algorithm is lost. diff --git a/kore/test/Test/Kore/Step/Rule/Simplify.hs b/kore/test/Test/Kore/Step/Rule/Simplify.hs index b5e588d645..217e742df6 100644 --- a/kore/test/Test/Kore/Step/Rule/Simplify.hs +++ b/kore/test/Test/Kore/Step/Rule/Simplify.hs @@ -422,7 +422,7 @@ test_simplifyClaimRuleOLD = [ test "infers definedness" [] rule1 [rule1'] - , test "TESTING includes side condition" [(Mock.g Mock.a, Mock.f Mock.a)] + , test "includes side condition" [(Mock.g Mock.a, Mock.f Mock.a)] rule2 [rule2'] ] @@ -481,7 +481,7 @@ test_simplifyClaimRule = [ test "infers definedness" [] rule1 [rule1'] - , test "TESTING includes side condition" [(Mock.g Mock.a, Mock.f Mock.a)] + , test "includes side condition" [(Mock.g Mock.a, Mock.f Mock.a)] rule2 [rule2'] ] From 89d4a325e45376575403df8011d84226be12bc26 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Wed, 29 Jul 2020 12:08:17 +0300 Subject: [PATCH 23/27] Fix ClaimPattern right hand side free variables bug --- kore/src/Kore/Step/ClaimPattern.hs | 30 +++++++++++++++++++++++++----- kore/src/Kore/Step/Rule/Expand.hs | 5 +++-- 2 files changed, 28 insertions(+), 7 deletions(-) diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs index 40aafa133a..559c7524a7 100644 --- a/kore/src/Kore/Step/ClaimPattern.hs +++ b/kore/src/Kore/Step/ClaimPattern.hs @@ -6,6 +6,8 @@ License : NCSA module Kore.Step.ClaimPattern ( ClaimPattern (..) + , freeVariablesLeft + , freeVariablesRight , claimPattern , claimPatternInternal , OnePathRule (..) @@ -35,7 +37,8 @@ import qualified GHC.Generics as GHC import qualified Kore.Attribute.Axiom as Attribute import Kore.Attribute.Pattern.FreeVariables - ( HasFreeVariables (..) + ( FreeVariables + , HasFreeVariables (..) ) import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables import Kore.Debug @@ -137,12 +140,29 @@ instance From ClaimPattern Attribute.PriorityAttributes where instance From ClaimPattern Attribute.HeatCool where from = from @(Attribute.Axiom _ _) . attributes +freeVariablesRight + :: ClaimPattern + -> FreeVariables RewritingVariableName +freeVariablesRight claimPattern'@(ClaimPattern _ _ _ _) = + freeVariables + ( TermLike.mkExistsN existentials + (OrPattern.toTermLike right) + ) + where + ClaimPattern { right, existentials } = claimPattern' + +freeVariablesLeft + :: ClaimPattern + -> FreeVariables RewritingVariableName +freeVariablesLeft claimPattern'@(ClaimPattern _ _ _ _) = + freeVariables left + where + ClaimPattern { left } = claimPattern' + instance HasFreeVariables ClaimPattern RewritingVariableName where freeVariables claimPattern'@(ClaimPattern _ _ _ _) = - freeVariables left - <> freeVariables (OrPattern.toPattern right) - where - ClaimPattern { left, right } = claimPattern' + freeVariablesLeft claimPattern' + <> freeVariablesRight claimPattern' -- | Creates a 'ClaimPattern' from a left hand side 'Pattern' -- and a 'TermLike' representing the right hand side pattern. The diff --git a/kore/src/Kore/Step/Rule/Expand.hs b/kore/src/Kore/Step/Rule/Expand.hs index 7061a8c2e7..0e37f17cb4 100644 --- a/kore/src/Kore/Step/Rule/Expand.hs +++ b/kore/src/Kore/Step/Rule/Expand.hs @@ -81,6 +81,7 @@ import Kore.Step.ClaimPattern , ClaimPattern (..) , OnePathRule (..) , ReachabilityRule (..) + , freeVariablesLeft ) import Kore.Step.RulePattern ( RulePattern (RulePattern) @@ -193,8 +194,8 @@ instance ExpandSingleConstructors ClaimPattern where :: [ElementVariable RewritingVariableName] leftElementVariables = extractFreeElementVariables - . freeVariables - $ left + . freeVariablesLeft + $ rule freeElementVariables :: [ElementVariable RewritingVariableName] freeElementVariables = From 6eaf5c1ef564adb6d1527d94999956ecfc844861 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Wed, 29 Jul 2020 12:12:07 +0300 Subject: [PATCH 24/27] Fix ClaimPattern unparsing bug --- kore/src/Kore/Step/ClaimPattern.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs index 559c7524a7..f536516662 100644 --- a/kore/src/Kore/Step/ClaimPattern.hs +++ b/kore/src/Kore/Step/ClaimPattern.hs @@ -205,12 +205,12 @@ claimPatternToTerm modality representation@(ClaimPattern _ _ _ _) = leftPattern (TermLike.applyModality modality rightPattern) where - ClaimPattern { left, right } = representation + ClaimPattern { left, right, existentials } = representation leftPattern = Pattern.toTermLike left & TermLike.mapVariables getRewritingVariable rightPattern = - OrPattern.toTermLike right + TermLike.mkExistsN existentials (OrPattern.toTermLike right) & TermLike.mapVariables getRewritingVariable substituteRight From deb9abdf6a2d9628d4e63e1dd8dddb8cbc750667 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 29 Jul 2020 11:32:11 -0500 Subject: [PATCH 25/27] Kore.Step.Rule.Expand: Remove redundant State field --- kore/src/Kore/Step/Rule/Expand.hs | 34 ++++++++++++++----------------- 1 file changed, 15 insertions(+), 19 deletions(-) diff --git a/kore/src/Kore/Step/Rule/Expand.hs b/kore/src/Kore/Step/Rule/Expand.hs index 0e37f17cb4..4eabf70ae4 100644 --- a/kore/src/Kore/Step/Rule/Expand.hs +++ b/kore/src/Kore/Step/Rule/Expand.hs @@ -12,12 +12,12 @@ import Prelude.Kore import Control.Lens ( (%=) ) -import qualified Control.Monad as Monad import Control.Monad.State.Strict ( State - , execState + , evalState ) import qualified Control.Monad.State.Strict as State +import qualified Data.Bifunctor as Bifunctor import Data.Generics.Product ( field ) @@ -254,16 +254,8 @@ instance ExpandSingleConstructors ReachabilityRule where . getAllPathRule $ rule -data Expansion variable = - Expansion - { substitution - :: !( Map - (SomeVariable variable) - (TermLike variable) - ) - , stale - :: !(Set (ElementVariableName variable)) - } +newtype Expansion variable = + Expansion { stale :: Set (ElementVariableName variable) } deriving (GHC.Generic) type Expander variable = State (Expansion variable) @@ -276,16 +268,20 @@ expandVariables -> Set (ElementVariableName variable) -> Map (SomeVariable variable) (TermLike variable) expandVariables metadataTools variables stale = - traverse expandAddVariable variables - & flip execState Expansion { substitution = Map.empty, stale } - & substitution + wither expandAddVariable variables + & flip evalState Expansion { stale } + & (map . Bifunctor.first) inject + & Map.fromList where - expandAddVariable :: ElementVariable variable -> Expander variable () + expandAddVariable + :: ElementVariable variable + -> Expander variable + (Maybe (ElementVariable variable, TermLike variable)) expandAddVariable variable = do term <- expandVariable metadataTools variable - Monad.unless - (mkElemVar variable == term) - (field @"substitution" %= Map.insert (inject variable) term) + if mkElemVar variable == term + then return Nothing + else return $ Just (variable, term) expandVariable :: forall variable attributes From 5f866d47f06e171593729b5eff2fe6b1db96473f Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 29 Jul 2020 11:36:13 -0500 Subject: [PATCH 26/27] Test.Kore.Step.Rule.Expand: Separate old and new tests --- kore/test/Test/Kore/Step/Rule/Expand.hs | 342 ++++++++++++++++++------ 1 file changed, 262 insertions(+), 80 deletions(-) diff --git a/kore/test/Test/Kore/Step/Rule/Expand.hs b/kore/test/Test/Kore/Step/Rule/Expand.hs index 2757fde7b3..d3195acb24 100644 --- a/kore/test/Test/Kore/Step/Rule/Expand.hs +++ b/kore/test/Test/Kore/Step/Rule/Expand.hs @@ -1,5 +1,6 @@ module Test.Kore.Step.Rule.Expand ( test_expandRule + , test_expandRule_OLD ) where import Prelude.Kore @@ -70,6 +71,174 @@ import Test.Kore.With ) import Test.Tasty.HUnit.Ext +test_expandRule_OLD :: [TestTree] +test_expandRule_OLD = + [ testCase "Nothing to expand" $ + let expected = Mock.f x `rewritesToOLD` Mock.g x + actual = + expandSingleConstructors + (metadataTools []) + (Mock.f x `rewritesToOLD` Mock.g x) + in assertEqual "" expected actual + , testCase "Nothing to expand without constructors" $ + let expected = Mock.f x `rewritesToOLD` Mock.g x + actual = + expandSingleConstructors + (metadataTools + [ (Mock.testSortId, noConstructor) ] + ) + (Mock.f x `rewritesToOLD` Mock.g x) + in assertEqual "" expected actual + , testCase "Nothing to expand with multiple constructors" $ + let expected = Mock.f x `rewritesToOLD` Mock.g x + actual = + expandSingleConstructors + (metadataTools + [ ( Mock.testSortId + , noConstructor + `with` constructor Mock.aSymbol + `with` constructor Mock.bSymbol + ) + ] + ) + (Mock.f x `rewritesToOLD` Mock.g x) + in assertEqual "" expected actual + , testCase "Expands variable once to constant" $ + let expected = + Pair (Mock.f Mock.a, makeEqualsPredicate_ x Mock.a) + `rewritesToOLD` + Pair (Mock.g Mock.a, makeTruePredicate_) + actual = + expandSingleConstructors + (metadataTools + [ ( Mock.testSortId + , noConstructor `with` constructor Mock.aSymbol + ) + ] + ) + (Mock.f x `rewritesToOLD` Mock.g x) + in assertEqual "" expected actual + , testCase "Expands variable once to argument constructor" $ + let expected = + Pair + ( Mock.fSort0 (expandableConstructor1 x00TestSort) + , makeEqualsPredicate_ + x0 + (expandableConstructor1 x00TestSort) + ) + `rewritesToOLD` + Pair + ( Mock.gSort0 (expandableConstructor1 x00TestSort) + , makeTruePredicate_ + ) + actual = + expandSingleConstructors + (metadataTools + [ ( Mock.testSort0Id + , noConstructor + `with` + ( constructor expandableConstructor1Symbol + `with` Mock.testSort + ) + ) + ] + ) + (Mock.fSort0 x0 `rewritesToOLD` Mock.gSort0 x0) + in assertEqual "" expected actual + , testCase "Expands variable twice." $ + let expected = + Pair + ( Mock.fSort0 (expandableConstructor1 Mock.a) + , makeEqualsPredicate_ + x0 + (expandableConstructor1 Mock.a) + ) + `rewritesToOLD` + Pair + ( Mock.gSort0 (expandableConstructor1 Mock.a) + , makeTruePredicate_ + ) + actual = + expandSingleConstructors + (metadataTools + [ ( Mock.testSort0Id + , noConstructor + `with` + ( constructor expandableConstructor1Symbol + `with` Mock.testSort + ) + ) + , ( Mock.testSortId + , noConstructor `with` constructor Mock.aSymbol + ) + ] + ) + (Mock.fSort0 x0 `rewritesToOLD` Mock.gSort0 x0) + in assertEqual "" expected actual + , testCase "Expands multiple arguments." $ + let expected = + Pair + ( Mock.fSort0 (expandableConstructor2 Mock.a Mock.a) + , makeEqualsPredicate_ + x0 + (expandableConstructor2 Mock.a Mock.a) + ) + `rewritesToOLD` + Pair + ( Mock.gSort0 (expandableConstructor2 Mock.a Mock.a) + , makeTruePredicate_ + ) + actual = + expandSingleConstructors + (metadataTools + [ ( Mock.testSort0Id + , noConstructor + `with` + ( constructor expandableConstructor2Symbol + `with` Mock.testSort + `with` Mock.testSort + ) + ) + , ( Mock.testSortId + , noConstructor `with` constructor Mock.aSymbol + ) + ] + ) + (Mock.fSort0 x0 `rewritesToOLD` Mock.gSort0 x0) + in assertEqual "" expected actual + , testCase "Expands one of multiple arguments" $ + let expected = + Pair + ( Mock.fSort0 (expandableConstructor2a x00TestSort1 Mock.a) + , makeEqualsPredicate_ + x0 + (expandableConstructor2a x00TestSort1 Mock.a) + ) + `rewritesToOLD` + Pair + ( Mock.gSort0 (expandableConstructor2a x00TestSort1 Mock.a) + , makeTruePredicate_ + ) + actual = + expandSingleConstructors + (metadataTools + [ ( Mock.testSort0Id + , noConstructor + `with` + ( constructor expandableConstructor2aSymbol + `with` Mock.testSort1 + `with` Mock.testSort + ) + ) + , ( Mock.testSortId + , noConstructor `with` constructor Mock.aSymbol + ) + ] + ) + (Mock.fSort0 x0 `rewritesToOLD` Mock.gSort0 x0) + in assertEqual "" expected actual + ] + test_expandRule :: [TestTree] test_expandRule = [ testCase "Nothing to expand" $ @@ -401,94 +570,107 @@ test_expandRule = (Mock.fSort0 x0 `rewritesTo` Mock.gSort0 x0) in assertEqual "" expected actual ] - where - rewritesTo - :: RuleBase base OnePathRule - => base VariableName - -> base VariableName - -> OnePathRule - rewritesTo = Common.rewritesTo - rewritesToOLD - :: RuleBase base OLD.OnePathRule - => base VariableName - -> base VariableName - -> OLD.OnePathRule - rewritesToOLD = Common.rewritesTo +rewritesTo + :: RuleBase base OnePathRule + => base VariableName + -> base VariableName + -> OnePathRule +rewritesTo = Common.rewritesTo + +rewritesToOLD + :: RuleBase base OLD.OnePathRule + => base VariableName + -> base VariableName + -> OLD.OnePathRule +rewritesToOLD = Common.rewritesTo + +x, x0 :: TermLike VariableName +x = mkElemVar Mock.x +x0 = mkElemVar Mock.x0 + +x00TestSortVar :: ElementVariable VariableName +x00TestSortVar = + mkElementVariable (testId "x0") Mock.testSort + & Lens.set + (field @"variableName" . Lens.mapped . field @"counter") + (Just (Element 0)) + +x00TestSort :: TermLike VariableName +x00TestSort = mkElemVar x00TestSortVar + +x00TestSort1Var :: ElementVariable VariableName +x00TestSort1Var = + mkElementVariable (testId "x0") Mock.testSort1 + & Lens.set + (field @"variableName" . Lens.mapped . field @"counter") + (Just (Element 0)) + +x00TestSort1 :: TermLike VariableName +x00TestSort1 = mkElemVar x00TestSort1Var + +metadataTools + :: [(Id, Attribute.Constructors)] + -> SmtMetadataTools Attribute.Symbol +metadataTools sortAndConstructors = + Mock.metadataTools + { MetadataTools.sortConstructors = Map.fromList sortAndConstructors + } + +expandableConstructor1Id :: Id +expandableConstructor1Id = testId "expandableConstructor1" + +expandableConstructor1Symbol :: Symbol +expandableConstructor1Symbol = + Mock.symbol expandableConstructor1Id [Mock.testSort] Mock.testSort0 + & Symbol.functional + & Symbol.constructor - x = mkElemVar Mock.x - x0 = mkElemVar Mock.x0 +expandableConstructor1 + :: HasCallStack + => TermLike VariableName -> TermLike VariableName +expandableConstructor1 arg = + mkApplySymbol expandableConstructor1Symbol [arg] - x00TestSortVar = - mkElementVariable (testId "x0") Mock.testSort - & Lens.set - (field @"variableName" . Lens.mapped . field @"counter") - (Just (Element 0)) - x00TestSort = mkElemVar x00TestSortVar +expandableConstructor2Id :: Id +expandableConstructor2Id = testId "expandableConstructor2" - x00TestSort1Var = - mkElementVariable (testId "x0") Mock.testSort1 - & Lens.set - (field @"variableName" . Lens.mapped . field @"counter") - (Just (Element 0)) - x00TestSort1 = mkElemVar x00TestSort1Var +expandableConstructor2Symbol :: Symbol +expandableConstructor2Symbol = + Mock.symbol + expandableConstructor2Id + [Mock.testSort, Mock.testSort] + Mock.testSort0 + & Symbol.functional + & Symbol.constructor - metadataTools - :: [(Id, Attribute.Constructors)] - -> SmtMetadataTools Attribute.Symbol - metadataTools sortAndConstructors = - Mock.metadataTools - { MetadataTools.sortConstructors = Map.fromList sortAndConstructors - } +expandableConstructor2 + :: HasCallStack + => TermLike VariableName + -> TermLike VariableName + -> TermLike VariableName +expandableConstructor2 arg1 arg2 = + mkApplySymbol expandableConstructor2Symbol [arg1, arg2] - expandableConstructor1Id :: Id - expandableConstructor1Id = testId "expandableConstructor1" - expandableConstructor1Symbol :: Symbol - expandableConstructor1Symbol = - Mock.symbol expandableConstructor1Id [Mock.testSort] Mock.testSort0 - & Symbol.functional - & Symbol.constructor - expandableConstructor1 - :: HasCallStack - => TermLike VariableName -> TermLike VariableName - expandableConstructor1 arg = - mkApplySymbol expandableConstructor1Symbol [arg] +expandableConstructor2aId :: Id +expandableConstructor2aId = testId "expandableConstructor2a" - expandableConstructor2Id :: Id - expandableConstructor2Id = testId "expandableConstructor2" - expandableConstructor2Symbol :: Symbol - expandableConstructor2Symbol = - Mock.symbol - expandableConstructor2Id - [Mock.testSort, Mock.testSort] - Mock.testSort0 - & Symbol.functional - & Symbol.constructor - expandableConstructor2 - :: HasCallStack - => TermLike VariableName - -> TermLike VariableName - -> TermLike VariableName - expandableConstructor2 arg1 arg2 = - mkApplySymbol expandableConstructor2Symbol [arg1, arg2] +expandableConstructor2aSymbol :: Symbol +expandableConstructor2aSymbol = + Mock.symbol + expandableConstructor2aId + [Mock.testSort1, Mock.testSort] + Mock.testSort0 + & Symbol.functional + & Symbol.constructor - expandableConstructor2aId :: Id - expandableConstructor2aId = testId "expandableConstructor2a" - expandableConstructor2aSymbol :: Symbol - expandableConstructor2aSymbol = - Mock.symbol - expandableConstructor2aId - [Mock.testSort1, Mock.testSort] - Mock.testSort0 - & Symbol.functional - & Symbol.constructor - expandableConstructor2a - :: HasCallStack - => TermLike VariableName - -> TermLike VariableName - -> TermLike VariableName - expandableConstructor2a arg1 arg2 = - mkApplySymbol expandableConstructor2aSymbol [arg1, arg2] +expandableConstructor2a + :: HasCallStack + => TermLike VariableName + -> TermLike VariableName + -> TermLike VariableName +expandableConstructor2a arg1 arg2 = + mkApplySymbol expandableConstructor2aSymbol [arg1, arg2] noConstructor :: Attribute.Constructors noConstructor = Attribute.Constructors Nothing From 03f9f855ddd7729df2906a495c8ec9bd31a58229 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Thu, 30 Jul 2020 12:00:12 +0300 Subject: [PATCH 27/27] Address review comments --- kore/src/Kore/Internal/Conditional.hs | 3 +- kore/src/Kore/Internal/TermLike.hs | 16 ++++--- kore/src/Kore/Step/ClaimPattern.hs | 54 +++++------------------ kore/src/Kore/Step/Rule/Expand.hs | 15 ++++--- kore/test/Test/Kore/Step/Rule.hs | 4 +- kore/test/Test/Kore/Step/Rule/Common.hs | 5 +-- kore/test/Test/Kore/Step/Rule/Simplify.hs | 11 ++++- 7 files changed, 43 insertions(+), 65 deletions(-) diff --git a/kore/src/Kore/Internal/Conditional.hs b/kore/src/Kore/Internal/Conditional.hs index 7be50430aa..cd5e15fee8 100644 --- a/kore/src/Kore/Internal/Conditional.hs +++ b/kore/src/Kore/Internal/Conditional.hs @@ -253,8 +253,7 @@ instance => From (Map (SomeVariable variable) (TermLike variable)) (Conditional variable ()) where from = - from @(Predicate variable) @(Conditional variable ()) - . from @(Substitution variable) @(Predicate variable) + from @(Substitution variable) @(Conditional variable ()) . from @(Map (SomeVariable variable) (TermLike variable)) @(Substitution variable) diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index 740e31df85..4e11e90893 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -46,11 +46,9 @@ module Kore.Internal.TermLike , forceSort , fullyOverrideSort -- * Reachability modalities and application - , Modality + , Modality (..) , weakExistsFinally , weakAlwaysFinally - , wEF - , wAF , applyModality -- * Pure Kore pattern constructors , mkAnd @@ -2008,7 +2006,7 @@ refreshSetBinder -> Binder (SetVariable variable) (TermLike variable) refreshSetBinder = refreshBinder refreshSetVariable -type Modality = Sort -> Alias (TermLike VariableName) +data Modality = WEF | WAF -- | Weak exists finally modality symbol. weakExistsFinally :: Text @@ -2019,7 +2017,7 @@ weakAlwaysFinally :: Text weakAlwaysFinally = "weakAlwaysFinally" -- | 'Alias' construct for weak exist finally. -wEF :: Modality +wEF :: Sort -> Alias (TermLike VariableName) wEF sort = Alias { aliasConstructor = Id { getId = weakExistsFinally @@ -2035,7 +2033,7 @@ wEF sort = Alias } -- | 'Alias' construct for weak always finally. -wAF :: Modality +wAF :: Sort -> Alias (TermLike VariableName) wAF sort = Alias { aliasConstructor = Id { getId = weakAlwaysFinally @@ -2057,6 +2055,10 @@ applyModality -> TermLike VariableName -> TermLike VariableName applyModality modality term = - mkApplyAlias (modality sort) [term] + case modality of + WEF -> + mkApplyAlias (wEF sort) [term] + WAF -> + mkApplyAlias (wAF sort) [term] where sort = termLikeSort term diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs index f536516662..3cf69dd2bd 100644 --- a/kore/src/Kore/Step/ClaimPattern.hs +++ b/kore/src/Kore/Step/ClaimPattern.hs @@ -9,7 +9,6 @@ module Kore.Step.ClaimPattern , freeVariablesLeft , freeVariablesRight , claimPattern - , claimPatternInternal , OnePathRule (..) , AllPathRule (..) , ReachabilityRule (..) @@ -165,30 +164,16 @@ instance HasFreeVariables ClaimPattern RewritingVariableName where <> freeVariablesRight claimPattern' -- | Creates a 'ClaimPattern' from a left hand side 'Pattern' --- and a 'TermLike' representing the right hand side pattern. The --- 'TermLike' is parsed into an 'OrPattern' and a list of --- existentially quantified variables. -claimPattern - :: Pattern RewritingVariableName - -> TermLike RewritingVariableName - -> ClaimPattern -claimPattern left rightTerm = - ClaimPattern - { left - , right = OrPattern.parseFromTermLike rightTerm - , existentials = termToExistentials rightTerm - , attributes = Default.def - } +-- and an 'OrPattern', representing the right hand side pattern. +-- The list of element variables are existentially quantified +-- in the right hand side. --- | Unsafe version of 'claimPattern'. The right hand side is --- assumed to be already processed into an 'OrPattern' and --- a list of existentially quantified variables. -claimPatternInternal +claimPattern :: Pattern RewritingVariableName -> OrPattern RewritingVariableName -> [ElementVariable RewritingVariableName] -> ClaimPattern -claimPatternInternal left right existentials = +claimPattern left right existentials = ClaimPattern { left , right @@ -308,22 +293,13 @@ instance Diff OnePathRule -- rewriting algorithm is lost. onePathRuleToTerm :: OnePathRule -> TermLike VariableName onePathRuleToTerm (OnePathRule claimPattern') = - claimPatternToTerm TermLike.wEF claimPattern' + claimPatternToTerm TermLike.WEF claimPattern' instance Unparse OnePathRule where unparse claimPattern' = - "claim {}" - <> Pretty.line' - <> Pretty.nest 4 - (unparse $ onePathRuleToTerm claimPattern') - <> Pretty.line' - <> "[]" - + unparse $ onePathRuleToTerm claimPattern' unparse2 claimPattern' = - "claim {}" - Pretty.<+> - unparse2 (onePathRuleToTerm claimPattern') - Pretty.<+> "[]" + unparse2 $ onePathRuleToTerm claimPattern' instance TopBottom OnePathRule where isTop _ = False @@ -358,17 +334,9 @@ instance Diff AllPathRule instance Unparse AllPathRule where unparse claimPattern' = - "claim {}" - <> Pretty.line' - <> Pretty.nest 4 - (unparse $ allPathRuleToTerm claimPattern') - <> Pretty.line' - <> "[]" + unparse $ allPathRuleToTerm claimPattern' unparse2 claimPattern' = - "claim {}" - Pretty.<+> - unparse2 (allPathRuleToTerm claimPattern') - Pretty.<+> "[]" + unparse2 $ allPathRuleToTerm claimPattern' instance TopBottom AllPathRule where isTop _ = False @@ -392,7 +360,7 @@ instance From AllPathRule Attribute.Trusted where -- rewriting algorithm is lost. allPathRuleToTerm :: AllPathRule -> TermLike VariableName allPathRuleToTerm (AllPathRule claimPattern') = - claimPatternToTerm TermLike.wAF claimPattern' + claimPatternToTerm TermLike.WAF claimPattern' -- | Unified One-Path and All-Path claim pattern. data ReachabilityRule diff --git a/kore/src/Kore/Step/Rule/Expand.hs b/kore/src/Kore/Step/Rule/Expand.hs index 4eabf70ae4..a0725ad991 100644 --- a/kore/src/Kore/Step/Rule/Expand.hs +++ b/kore/src/Kore/Step/Rule/Expand.hs @@ -46,15 +46,16 @@ import Kore.IndexedModule.MetadataTools ( SmtMetadataTools , findSortConstructors ) -import Kore.Internal.Condition - ( Condition - ) +import qualified Kore.Internal.Condition as Condition import qualified Kore.Internal.OrPattern as OrPattern import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.Predicate ( makeAndPredicate ) import qualified Kore.Internal.Predicate as Predicate +import Kore.Internal.Substitution + ( Substitution + ) import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.TermLike ( InternalVariable @@ -216,14 +217,16 @@ instance ExpandSingleConstructors ClaimPattern where metadataTools leftElementVariables allElementVariableNames - substitutionCondition = - from @(Map _ _) @(Condition _) expansion + substitutionPredicate = + Substitution.toPredicate + . from @(Map _ _) @(Substitution _) + $ expansion subst = Map.mapKeys variableName expansion in rule { left = Pattern.andCondition (Pattern.substitute subst left) - substitutionCondition + (Condition.fromPredicate substitutionPredicate) , existentials , right = OrPattern.substitute subst right } diff --git a/kore/test/Test/Kore/Step/Rule.hs b/kore/test/Test/Kore/Step/Rule.hs index d187fe71fa..3dd29c2ef3 100644 --- a/kore/test/Test/Kore/Step/Rule.hs +++ b/kore/test/Test/Kore/Step/Rule.hs @@ -252,7 +252,7 @@ test_patternToAxiomPatternAndBack = let initialPattern = mkImplies (mkAnd (Predicate.unwrapPredicate requiresP) leftP) (applyModality - wEF + WEF (mkAnd (Predicate.unwrapPredicate ensuresP) rightP) ) in @@ -264,7 +264,7 @@ test_patternToAxiomPatternAndBack = let initialPattern = mkImplies (mkAnd (Predicate.unwrapPredicate requiresP) leftP) (applyModality - wAF + WAF (mkAnd (Predicate.unwrapPredicate ensuresP) rightP) ) in diff --git a/kore/test/Test/Kore/Step/Rule/Common.hs b/kore/test/Test/Kore/Step/Rule/Common.hs index 95652c330c..0a1e2e659c 100644 --- a/kore/test/Test/Kore/Step/Rule/Common.hs +++ b/kore/test/Test/Kore/Step/Rule/Common.hs @@ -5,7 +5,6 @@ module Test.Kore.Step.Rule.Common import Prelude.Kore - import qualified Data.Default as Default import qualified Kore.Internal.OrPattern as OrPattern @@ -26,7 +25,7 @@ import Kore.Rewriting.RewritingVariable ) import Kore.Step.ClaimPattern ( OnePathRule (..) - , claimPatternInternal + , claimPattern ) import Kore.Step.RulePattern ( RHS (RHS) @@ -44,7 +43,7 @@ class RuleBase base rule where instance RuleBase Pair OnePathRule where Pair (t1, p1) `rewritesTo` Pair (t2, p2) = OnePathRule - $ claimPatternInternal + $ claimPattern (Pattern.fromTermAndPredicate t1' p1') (Pattern.fromTermAndPredicate t2' p2' & OrPattern.fromPattern) [] diff --git a/kore/test/Test/Kore/Step/Rule/Simplify.hs b/kore/test/Test/Kore/Step/Rule/Simplify.hs index 217e742df6..b3b5184847 100644 --- a/kore/test/Test/Kore/Step/Rule/Simplify.hs +++ b/kore/test/Test/Kore/Step/Rule/Simplify.hs @@ -487,10 +487,17 @@ test_simplifyClaimRule = ] where rule1, rule2, rule2' :: ClaimPattern - rule1 = claimPattern (Pattern.fromTermLike (Mock.f Mock.a)) Mock.b + rule1 = + claimPattern + (Pattern.fromTermLike (Mock.f Mock.a)) + (OrPattern.fromPatterns [Pattern.fromTermLike Mock.b]) + [] rule1' = rule1 & requireDefined rule2 = - claimPattern (Pattern.fromTermLike (Mock.g Mock.a)) Mock.b + claimPattern + (Pattern.fromTermLike (Mock.g Mock.a)) + (OrPattern.fromPatterns [Pattern.fromTermLike Mock.b]) + [] & require aEqualsb rule2' = rule2