From 03b453af1d577406f9bf127a9ff1291953b09bb0 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 13 Feb 2020 12:47:47 -0600 Subject: [PATCH 01/21] unsafeWrap: HasCallStack HasCallStack adds call stack information to the assertions, which is important for diagnosing test failures. --- kore/src/Kore/Internal/Substitution.hs | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/kore/src/Kore/Internal/Substitution.hs b/kore/src/Kore/Internal/Substitution.hs index 311d9b34c2..fc52368c0b 100644 --- a/kore/src/Kore/Internal/Substitution.hs +++ b/kore/src/Kore/Internal/Substitution.hs @@ -314,24 +314,25 @@ wrap xs = Substitution xs -- | Wrap the list of substitutions to a normalized substitution. Do not use -- this unless you are sure you need it. unsafeWrap - :: Ord variable + :: HasCallStack + => Ord variable => [(UnifiedVariable variable, TermLike variable)] -> Substitution variable unsafeWrap = NormalizedSubstitution . List.foldl' insertNormalized Map.empty where insertNormalized subst (var, termLike) = + Map.insert var termLike subst -- The variable must not occur in the substitution - assert (Map.notMember var subst) + & assert (Map.notMember var subst) -- or in the right-hand side of this or any other substitution, - $ assert (not $ occurs termLike) - $ assert (not $ any occurs subst) + & assert (not $ occurs termLike) + & assert (not $ any occurs subst) -- this substitution must not depend on any substitution variable, - $ assert (not $ any depends $ Map.keys subst) + & assert (not $ any depends $ Map.keys subst) -- and if this is an element variable substitution, the substitution -- must be defined. - $ assert (not $ isElemVar var && isBottom termLike) - $ Map.insert var termLike subst + & assert (not $ isElemVar var && isBottom termLike) where occurs = TermLike.hasFreeVariable var depends var' = TermLike.hasFreeVariable var' termLike From 3f1fead8816d32cefd9024c1fb6a23c8863315b1 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 13 Feb 2020 12:48:11 -0600 Subject: [PATCH 02/21] test_matcherVariableFunction: Fix inconsistent variable naming The variables x and xSub were given the same name, but different sorts. --- kore/test/Test/Kore/Step/Axiom/Matcher.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/test/Test/Kore/Step/Axiom/Matcher.hs b/kore/test/Test/Kore/Step/Axiom/Matcher.hs index af8ed3fbcf..76f93cdea3 100644 --- a/kore/test/Test/Kore/Step/Axiom/Matcher.hs +++ b/kore/test/Test/Kore/Step/Axiom/Matcher.hs @@ -384,7 +384,7 @@ test_matcherVariableFunction = ] where aSubSub = Mock.functional00SubSubSort - xSub = ElementVariable $ Variable (testId "x") mempty Mock.subSort + xSub = ElementVariable $ Variable (testId "xSub") mempty Mock.subSort test_matcherNonVarToPattern :: [TestTree] test_matcherNonVarToPattern = From 51ead8ad8b16c545765a80fcef61313e1cd42ae1 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Sun, 9 Feb 2020 11:26:48 -0600 Subject: [PATCH 03/21] Kore.Variables.Fresh.refreshVariables: Documentation bug --- kore/src/Kore/Variables/Fresh.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kore/src/Kore/Variables/Fresh.hs b/kore/src/Kore/Variables/Fresh.hs index c99becf219..5fc9f0f51e 100644 --- a/kore/src/Kore/Variables/Fresh.hs +++ b/kore/src/Kore/Variables/Fresh.hs @@ -82,8 +82,8 @@ result with 'Kore.Internal.TermLike.mkVar': @ 'Kore.Internal.TermLike.substitute' ('Kore.Internal.TermLike.mkVar' \<$\> refreshVariables avoid rename) - :: 'Kore.Internal.TermLike TermLike' Variable - -> 'Kore.Internal.TermLike TermLike' Variable + :: 'Kore.Internal.TermLike.TermLike' Variable + -> 'Kore.Internal.TermLike.TermLike' Variable @ -} From 95a901dad2108f3ca3eb380ab39a6b94f1e56f4c Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Sun, 9 Feb 2020 11:32:25 -0600 Subject: [PATCH 04/21] Add class FreshPartialOrd --- kore/src/Kore/Internal/TermLike/TermLike.hs | 4 +- kore/src/Kore/Variables/Fresh.hs | 117 +++++++++++++++----- kore/test/Test/Kore/Step/RewriteStep.hs | 5 +- 3 files changed, 94 insertions(+), 32 deletions(-) diff --git a/kore/src/Kore/Internal/TermLike/TermLike.hs b/kore/src/Kore/Internal/TermLike/TermLike.hs index 563d5e0596..2b2ce4c634 100644 --- a/kore/src/Kore/Internal/TermLike/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike/TermLike.hs @@ -899,7 +899,7 @@ externalizeFreshVariables termLike = <$> iterate nextVariable variable where wouldCapture var = isFreeVariable (ElemVar var) avoiding - nextVariable = fmap Fresh.nextVariable + nextVariable = Fresh.nextVariable variable externalize = fmap Variable.externalizeFreshVariable safeSetVariable @@ -913,7 +913,7 @@ externalizeFreshVariables termLike = <$> iterate nextVariable variable where wouldCapture var = isFreeVariable (SetVar var) avoiding - nextVariable = fmap Fresh.nextVariable + nextVariable = Fresh.nextVariable variable externalize = fmap Variable.externalizeFreshVariable underElementBinder freeVariables' variable child = do diff --git a/kore/src/Kore/Variables/Fresh.hs b/kore/src/Kore/Variables/Fresh.hs index 5fc9f0f51e..932b4bf7c0 100644 --- a/kore/src/Kore/Variables/Fresh.hs +++ b/kore/src/Kore/Variables/Fresh.hs @@ -3,9 +3,9 @@ Copyright : (c) Runtime Verification, 2018 License : UIUC/NCSA -} module Kore.Variables.Fresh - ( FreshVariable (..) + ( FreshPartialOrd (..) + , FreshVariable (..) , refreshVariables - , nextVariable -- * Re-exports , module Kore.Syntax.Variable ) where @@ -13,6 +13,12 @@ module Kore.Variables.Fresh import Prelude.Kore import qualified Data.Foldable as Foldable +import Data.Function + ( on + ) +import Data.Functor + ( ($>) + ) import Data.Map.Strict ( Map ) @@ -28,6 +34,78 @@ import Kore.Syntax.Id import Kore.Syntax.SetVariable import Kore.Syntax.Variable +{- | @FreshPartialOrder@ defines a partial order for renaming variables. + +Agreement: + +prop> maybe True (== compare a b) (compareFresh a b) + +Dominance: + +prop> maybe False (\/= GT) (compareFresh a (supVariable a)) + +Increment: + +prop> compareFresh a (nextVariable a x) == Just LT + + -} +class Ord variable => FreshPartialOrd variable where + compareFresh :: variable -> variable -> Maybe Ordering + supVariable :: variable -> variable + nextVariable + :: variable -- ^ original variable + -> variable -- ^ lower bound + -> variable + +instance FreshPartialOrd Variable where + compareFresh x y + | variableName x == variableName y = Just $ compare x y + | otherwise = Nothing + + supVariable variable = variable { variableCounter = Just Sup } + + nextVariable variable Variable { variableName, variableCounter } = + variable + { variableName = variableName' + , variableCounter = variableCounter' + } + where + variableName' = + variableName { idLocation = AstLocationGeneratedVariable } + variableCounter' = + case variableCounter of + Nothing -> Just (Element 0) + Just (Element a) -> Just (Element (succ a)) + Just Sup -> illegalVariableCounter + +instance + FreshPartialOrd variable + => FreshPartialOrd (ElementVariable variable) + where + compareFresh = on compareFresh getElementVariable + {-# INLINE compareFresh #-} + + supVariable = ElementVariable . supVariable . getElementVariable + {-# INLINE supVariable #-} + + nextVariable (ElementVariable variable) (ElementVariable bound) = + ElementVariable (nextVariable variable bound) + {-# INLINE nextVariable #-} + +instance + FreshPartialOrd variable + => FreshPartialOrd (SetVariable variable) + where + compareFresh = on compareFresh getSetVariable + {-# INLINE compareFresh #-} + + supVariable = SetVariable . supVariable . getSetVariable + {-# INLINE supVariable #-} + + nextVariable (SetVariable variable) (SetVariable bound) = + SetVariable (nextVariable variable bound) + {-# INLINE nextVariable #-} + {- | A @FreshVariable@ can be renamed to avoid colliding with a set of names. -} class Ord variable => FreshVariable variable where @@ -43,6 +121,14 @@ class Ord variable => FreshVariable variable where :: Set variable -- ^ variables to avoid -> variable -- ^ variable to rename -> Maybe variable + default refreshVariable + :: FreshPartialOrd variable + => Set variable + -> variable + -> Maybe variable + refreshVariable avoiding variable = do + largest <- Set.lookupLT (supVariable variable) avoiding + compareFresh variable largest $> nextVariable variable largest instance FreshVariable variable => FreshVariable (ElementVariable variable) where @@ -56,16 +142,7 @@ instance FreshVariable variable => FreshVariable (SetVariable variable) where avoid' = Set.map getSetVariable avoid -instance FreshVariable Variable where - refreshVariable avoiding variable = do - fixedLargest <- fixSort <$> Set.lookupLT pivotMax avoiding - if fixedLargest >= pivotMin - then Just (nextVariable fixedLargest) - else Nothing - where - pivotMax = variable { variableCounter = Just Sup } - pivotMin = variable { variableCounter = Nothing } - fixSort var = var { variableSort = variableSort variable } +instance FreshVariable Variable instance FreshVariable Concrete where refreshVariable _ = \case {} @@ -109,19 +186,3 @@ refreshVariables avoid0 = -- The variable does not collide with any others, so renaming is not -- necessary. (Set.insert var avoid, rename) - -{- | Increase the 'variableCounter' of a 'Variable' - -} -nextVariable :: Variable -> Variable -nextVariable variable@Variable { variableName, variableCounter } = - variable - { variableName = variableName' - , variableCounter = variableCounter' - } - where - variableName' = variableName { idLocation = AstLocationGeneratedVariable } - variableCounter' = - case variableCounter of - Nothing -> Just (Element 0) - Just (Element a) -> Just (Element (succ a)) - Just Sup -> illegalVariableCounter diff --git a/kore/test/Test/Kore/Step/RewriteStep.hs b/kore/test/Test/Kore/Step/RewriteStep.hs index 96b0618c0f..1c1024a4bb 100644 --- a/kore/test/Test/Kore/Step/RewriteStep.hs +++ b/kore/test/Test/Kore/Step/RewriteStep.hs @@ -351,7 +351,8 @@ test_applyRewriteRule_ = , testCase "quantified rhs: non-clashing" $ do let expect = Right [ OrPattern.fromPatterns [Pattern.fromTermLike final] ] - final = mkElemVar (nextVariable . nextVariable <$> Mock.x) + x'' = nextVariable Mock.x . nextVariable Mock.x $ Mock.x + final = mkElemVar x'' initial = pure (mkElemVar Mock.y) axiom = RewriteRule $ rulePattern @@ -467,7 +468,7 @@ test_applyRewriteRule_ = , testCase "non-function substitution error" $ do let expect = Left $ UnificationError $ unsupportedPatterns "Unknown unification case." - (mkElemVar (nextVariable <$> Mock.x)) + (mkElemVar (nextVariable Mock.x Mock.x)) (Mock.plain10 (mkElemVar Mock.y)) initial = pure $ Mock.sigma (mkElemVar Mock.x) (Mock.plain10 (mkElemVar Mock.y)) From a56892761d30170e0862095d55eb12ff29a7ffdf Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Sun, 9 Feb 2020 11:50:39 -0600 Subject: [PATCH 05/21] Use FreshPartialOrd to optimize variable renaming --- kore/src/Kore/Builtin/Int/Int.hs | 5 +- kore/src/Kore/Builtin/String/String.hs | 5 +- kore/src/Kore/Internal/Condition.hs | 4 +- kore/src/Kore/Internal/Conditional.hs | 4 +- kore/src/Kore/Internal/Pattern.hs | 4 +- kore/src/Kore/Internal/Predicate.hs | 4 +- kore/src/Kore/Internal/Substitution.hs | 4 +- kore/src/Kore/Internal/TermLike.hs | 5 +- kore/src/Kore/Internal/TermLike/TermLike.hs | 10 +- kore/src/Kore/Internal/Variable.hs | 8 +- kore/src/Kore/Step/Axiom/Matcher.hs | 4 +- kore/src/Kore/Step/Step.hs | 10 +- kore/src/Kore/Variables/Fresh.hs | 17 +-- kore/src/Kore/Variables/Target.hs | 14 +- kore/src/Kore/Variables/UnifiedVariable.hs | 27 ++-- kore/test/Test/Kore/Builtin.hs | 4 +- kore/test/Test/Kore/Builtin/Int.hs | 2 +- kore/test/Test/Kore/Builtin/Map.hs | 2 +- kore/test/Test/Kore/Internal/Pattern.hs | 139 +++--------------- .../Test/Kore/Step/Function/Integration.hs | 2 +- kore/test/Test/Kore/Step/MockSymbols.hs | 7 +- kore/test/Test/Kore/Step/Simplifier.hs | 4 +- kore/test/Test/Kore/Unification/Unifier.hs | 96 +----------- kore/test/Test/Kore/Variables/V.hs | 72 +++++++++ kore/test/Test/Kore/Variables/W.hs | 73 +++++++++ 25 files changed, 254 insertions(+), 272 deletions(-) create mode 100644 kore/test/Test/Kore/Variables/V.hs create mode 100644 kore/test/Test/Kore/Variables/W.hs diff --git a/kore/src/Kore/Builtin/Int/Int.hs b/kore/src/Kore/Builtin/Int/Int.hs index fffe09cbf8..d3d22edb31 100644 --- a/kore/src/Kore/Builtin/Int/Int.hs +++ b/kore/src/Kore/Builtin/Int/Int.hs @@ -54,9 +54,6 @@ import qualified Data.Text as Text import qualified Kore.Domain.Builtin as Domain import Kore.Internal.Pattern as Pattern import Kore.Internal.TermLike as TermLike -import Kore.Variables.Fresh - ( FreshVariable - ) {- | Builtin name of the @Int@ sort. -} @@ -72,7 +69,7 @@ See also: 'sort' -} asInternal - :: FreshVariable variable + :: InternalVariable variable => Sort -- ^ resulting sort -> Integer -- ^ builtin value to render -> TermLike variable diff --git a/kore/src/Kore/Builtin/String/String.hs b/kore/src/Kore/Builtin/String/String.hs index f97d3fe687..75dc0470e1 100644 --- a/kore/src/Kore/Builtin/String/String.hs +++ b/kore/src/Kore/Builtin/String/String.hs @@ -41,9 +41,6 @@ import Kore.Internal.Pattern ) import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.TermLike as TermLike -import Kore.Variables.Fresh - ( FreshVariable - ) {- | Builtin name of the @String@ sort. -} @@ -59,7 +56,7 @@ See also: 'sort' -} asInternal - :: FreshVariable variable + :: InternalVariable variable => Sort -- ^ resulting sort -> Text -- ^ builtin value to render -> TermLike variable diff --git a/kore/src/Kore/Internal/Condition.hs b/kore/src/Kore/Internal/Condition.hs index 5a57fbb078..7e68f1edf0 100644 --- a/kore/src/Kore/Internal/Condition.hs +++ b/kore/src/Kore/Internal/Condition.hs @@ -64,7 +64,7 @@ import qualified Kore.Internal.TermLike as TermLike import Kore.Internal.Variable import Kore.Syntax import Kore.Variables.Fresh - ( FreshVariable + ( FreshPartialOrd ) import Kore.Variables.UnifiedVariable ( UnifiedVariable @@ -148,7 +148,7 @@ toPredicate toPredicate = from mapVariables - :: (Ord variable1, FreshVariable variable2) + :: (Ord variable1, FreshPartialOrd variable2) => (ElementVariable variable1 -> ElementVariable variable2) -> (SetVariable variable1 -> SetVariable variable2) -> Condition variable1 diff --git a/kore/src/Kore/Internal/Conditional.hs b/kore/src/Kore/Internal/Conditional.hs index 7b62de2e21..51f8a75c5b 100644 --- a/kore/src/Kore/Internal/Conditional.hs +++ b/kore/src/Kore/Internal/Conditional.hs @@ -78,7 +78,7 @@ import Kore.TopBottom ) import Kore.Unparser import Kore.Variables.Fresh - ( FreshVariable + ( FreshPartialOrd ) import Kore.Variables.UnifiedVariable ( ElementVariable @@ -413,7 +413,7 @@ isPredicate Conditional {term} = isTop term -} mapVariables - :: (Ord variableFrom, FreshVariable variableTo) + :: (Ord variableFrom, FreshPartialOrd variableTo) => ((ElementVariable variableFrom -> ElementVariable variableTo) -> (SetVariable variableFrom -> SetVariable variableTo) -> termFrom -> termTo) -> (ElementVariable variableFrom -> ElementVariable variableTo) -> (SetVariable variableFrom -> SetVariable variableTo) diff --git a/kore/src/Kore/Internal/Pattern.hs b/kore/src/Kore/Internal/Pattern.hs index 829de76e66..2caa9dabcb 100644 --- a/kore/src/Kore/Internal/Pattern.hs +++ b/kore/src/Kore/Internal/Pattern.hs @@ -79,7 +79,7 @@ import Kore.TopBottom ( TopBottom (..) ) import Kore.Variables.Fresh - ( FreshVariable + ( FreshPartialOrd ) {- | The conjunction of a pattern, predicate, and substitution. @@ -123,7 +123,7 @@ freeElementVariables = in an Pattern. -} mapVariables - :: (Ord variableFrom, FreshVariable variableTo) + :: (Ord variableFrom, FreshPartialOrd variableTo) => (ElementVariable variableFrom -> ElementVariable variableTo) -> (SetVariable variableFrom -> SetVariable variableTo) -> Pattern variableFrom diff --git a/kore/src/Kore/Internal/Predicate.hs b/kore/src/Kore/Internal/Predicate.hs index c68133fc06..79b79e1900 100644 --- a/kore/src/Kore/Internal/Predicate.hs +++ b/kore/src/Kore/Internal/Predicate.hs @@ -121,7 +121,7 @@ import Kore.TopBottom ) import Kore.Unparser import Kore.Variables.Fresh - ( FreshVariable + ( FreshPartialOrd ) import Kore.Variables.UnifiedVariable ( UnifiedVariable (..) @@ -706,7 +706,7 @@ isPredicate = Either.isRight . makePredicate {- | Replace all variables in a @Predicate@ using the provided mapping. -} mapVariables - :: (Ord from, FreshVariable to) + :: (Ord from, FreshPartialOrd to) => (ElementVariable from -> ElementVariable to) -> (SetVariable from -> SetVariable to) -> Predicate from diff --git a/kore/src/Kore/Internal/Substitution.hs b/kore/src/Kore/Internal/Substitution.hs index fc52368c0b..144ee01add 100644 --- a/kore/src/Kore/Internal/Substitution.hs +++ b/kore/src/Kore/Internal/Substitution.hs @@ -86,7 +86,7 @@ import Kore.Unparser ( unparseToString ) import Kore.Variables.Fresh - ( FreshVariable + ( FreshPartialOrd ) import Kore.Variables.UnifiedVariable import qualified SQL @@ -351,7 +351,7 @@ modify f = wrap . f . unwrap -- with the given function. mapVariables :: forall variableFrom variableTo - . (Ord variableFrom, FreshVariable variableTo) + . (Ord variableFrom, FreshPartialOrd variableTo) => (ElementVariable variableFrom -> ElementVariable variableTo) -> (SetVariable variableFrom -> SetVariable variableTo) -> Substitution variableFrom diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index 2da03762f0..a5dbc56579 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -271,7 +271,8 @@ import Kore.Unparser import qualified Kore.Unparser as Unparser import Kore.Variables.Binding import Kore.Variables.Fresh - ( FreshVariable + ( FreshPartialOrd + , FreshVariable ) import qualified Kore.Variables.Fresh as Fresh import Kore.Variables.UnifiedVariable @@ -391,7 +392,7 @@ composes with other tree transformations without allocating intermediates. -} fromConcrete - :: FreshVariable variable + :: FreshPartialOrd variable => TermLike Concrete -> TermLike variable fromConcrete = mapVariables (\case {}) (\case {}) diff --git a/kore/src/Kore/Internal/TermLike/TermLike.hs b/kore/src/Kore/Internal/TermLike/TermLike.hs index 2b2ce4c634..b1a038978f 100644 --- a/kore/src/Kore/Internal/TermLike/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike/TermLike.hs @@ -125,7 +125,7 @@ import Kore.Unparser import qualified Kore.Unparser as Unparser import Kore.Variables.Binding import Kore.Variables.Fresh - ( FreshVariable + ( FreshPartialOrd ) import qualified Kore.Variables.Fresh as Fresh import qualified Pretty @@ -593,7 +593,7 @@ See also: 'traverseVariables' -} mapVariables :: forall variable1 variable2 - . (Ord variable1, FreshVariable variable2) + . (Ord variable1, FreshPartialOrd variable2) => (ElementVariable variable1 -> ElementVariable variable2) -> (SetVariable variable1 -> SetVariable variable2) -> TermLike variable1 @@ -669,7 +669,7 @@ See also: 'mapVariables' -} traverseVariables :: forall variable1 variable2 m - . (Ord variable1, FreshVariable variable2) + . (Ord variable1, FreshPartialOrd variable2) => Monad m => (ElementVariable variable1 -> m (ElementVariable variable2)) -> (SetVariable variable1 -> m (SetVariable variable2)) @@ -762,7 +762,7 @@ sequenceAdjunct gsequence = renameElementBinder :: Monad m - => (Ord variable1, FreshVariable variable2) + => (Ord variable1, FreshPartialOrd variable2) => (ElementVariable variable1 -> m (ElementVariable variable2)) -> Set.Set (UnifiedVariable variable2) -> Binder (ElementVariable variable1) @@ -788,7 +788,7 @@ renameElementBinder trElemVar avoiding binder = do renameSetBinder :: Monad m - => (Ord variable1, FreshVariable variable2) + => (Ord variable1, FreshPartialOrd variable2) => (SetVariable variable1 -> m (SetVariable variable2)) -> Set.Set (UnifiedVariable variable2) -> Binder (SetVariable variable1) diff --git a/kore/src/Kore/Internal/Variable.hs b/kore/src/Kore/Internal/Variable.hs index 79bc39390b..ecefdcfae7 100644 --- a/kore/src/Kore/Internal/Variable.hs +++ b/kore/src/Kore/Internal/Variable.hs @@ -7,6 +7,8 @@ License : NCSA module Kore.Internal.Variable ( SubstitutionOrd (..) , InternalVariable + , FreshVariable + , FreshPartialOrd , module Kore.Syntax.ElementVariable , module Kore.Syntax.SetVariable , module Kore.Syntax.Variable @@ -24,7 +26,8 @@ import Kore.Unparser ( Unparse ) import Kore.Variables.Fresh - ( FreshVariable + ( FreshPartialOrd + , FreshVariable ) {- | @SubstitutionOrd@ orders variables for substitution. @@ -81,5 +84,6 @@ these constraints. type InternalVariable variable = ( Ord variable, SubstitutionOrd variable , Debug variable, Show variable, Unparse variable - , VariableName variable, SortedVariable variable, FreshVariable variable + , VariableName variable, SortedVariable variable + , FreshPartialOrd variable, FreshVariable variable ) diff --git a/kore/src/Kore/Step/Axiom/Matcher.hs b/kore/src/Kore/Step/Axiom/Matcher.hs index 29d73e2dbc..1a120cc3bb 100644 --- a/kore/src/Kore/Step/Axiom/Matcher.hs +++ b/kore/src/Kore/Step/Axiom/Matcher.hs @@ -94,7 +94,7 @@ import Kore.Step.Simplification.Simplify import qualified Kore.Step.Simplification.Simplify as Simplifier import Kore.Variables.Binding import Kore.Variables.Fresh - ( FreshVariable + ( FreshPartialOrd ) import qualified Kore.Variables.Fresh as Variables import Kore.Variables.UnifiedVariable @@ -607,7 +607,7 @@ Returns 'Nothing' if the variable name is already globally-unique. -} liftVariable - :: FreshVariable variable + :: FreshPartialOrd variable => MonadState (MatcherState variable) matcher => UnifiedVariable variable -> matcher (Maybe (UnifiedVariable variable)) diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index 4013c5de26..6df4f28af3 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -80,7 +80,6 @@ import qualified Kore.Internal.SideCondition as SideCondition import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.TermLike ( ElementVariable - , FreshVariable , InternalVariable , SetVariable , TermLike @@ -100,6 +99,9 @@ import qualified Kore.Unification.Unify as Monad.Unify , scatter ) import Kore.Unparser +import Kore.Variables.Fresh + ( FreshPartialOrd + ) import Kore.Variables.Target ( Target ) @@ -159,7 +161,7 @@ class UnifyingRule rule where distinguishing rule variables from configuration variables. -} mapRuleVariables - :: (Ord variable1, FreshVariable variable2) + :: (Ord variable1, FreshPartialOrd variable2) => (ElementVariable variable1 -> ElementVariable variable2) -> (SetVariable variable1 -> SetVariable variable2) -> rule variable1 @@ -272,7 +274,7 @@ targetRuleVariables sideCondition initial = {- | Unwrap the variables in a 'RulePattern'. Inverse of 'targetRuleVariables'. -} unTargetRule - :: FreshVariable variable + :: FreshPartialOrd variable => UnifyingRule rule => rule (Target variable) -> rule variable unTargetRule = mapRuleVariables Target.unTargetElement Target.unTargetSet @@ -417,7 +419,7 @@ applyInitialConditions sideCondition initial unification = do -- |Renames configuration variables to distinguish them from those in the rule. toConfigurationVariables - :: FreshVariable variable + :: InternalVariable variable => Pattern variable -> Pattern (Target variable) toConfigurationVariables = diff --git a/kore/src/Kore/Variables/Fresh.hs b/kore/src/Kore/Variables/Fresh.hs index 932b4bf7c0..6a670857ea 100644 --- a/kore/src/Kore/Variables/Fresh.hs +++ b/kore/src/Kore/Variables/Fresh.hs @@ -78,6 +78,11 @@ instance FreshPartialOrd Variable where Just (Element a) -> Just (Element (succ a)) Just Sup -> illegalVariableCounter +instance FreshPartialOrd Concrete where + compareFresh = \case {} + supVariable = \case {} + nextVariable = \case {} + instance FreshPartialOrd variable => FreshPartialOrd (ElementVariable variable) @@ -130,17 +135,9 @@ class Ord variable => FreshVariable variable where largest <- Set.lookupLT (supVariable variable) avoiding compareFresh variable largest $> nextVariable variable largest -instance FreshVariable variable => FreshVariable (ElementVariable variable) - where - refreshVariable avoid = traverse (refreshVariable avoid') - where - avoid' = Set.map getElementVariable avoid +instance FreshPartialOrd variable => FreshVariable (ElementVariable variable) -instance FreshVariable variable => FreshVariable (SetVariable variable) - where - refreshVariable avoid = traverse (refreshVariable avoid') - where - avoid' = Set.map getSetVariable avoid +instance FreshPartialOrd variable => FreshVariable (SetVariable variable) instance FreshVariable Variable diff --git a/kore/src/Kore/Variables/Target.hs b/kore/src/Kore/Variables/Target.hs index 9d902c2db6..82008c72db 100644 --- a/kore/src/Kore/Variables/Target.hs +++ b/kore/src/Kore/Variables/Target.hs @@ -37,7 +37,8 @@ import Kore.Unparser ( Unparse (..) ) import Kore.Variables.Fresh - ( FreshVariable (..) + ( FreshPartialOrd (..) + , FreshVariable (..) ) import Kore.Variables.UnifiedVariable ( ElementVariable @@ -140,6 +141,17 @@ instance From variable1 variable2 => From (Target variable1) variable2 where from = from @variable1 @variable2 . unTarget {-# INLINE from #-} +instance FreshPartialOrd variable => FreshPartialOrd (Target variable) where + compareFresh = on compareFresh unTarget + {-# INLINE compareFresh #-} + + supVariable = fmap supVariable + {-# INLINE supVariable #-} + + nextVariable variable bound = + fmap (flip nextVariable (unTarget bound)) variable + {-# INLINE nextVariable #-} + {- | Ensures that fresh variables are unique under 'unwrapStepperVariable'. -} instance FreshVariable variable => FreshVariable (Target variable) where diff --git a/kore/src/Kore/Variables/UnifiedVariable.hs b/kore/src/Kore/Variables/UnifiedVariable.hs index 5b15e7c4fe..f3744be7cb 100644 --- a/kore/src/Kore/Variables/UnifiedVariable.hs +++ b/kore/src/Kore/Variables/UnifiedVariable.hs @@ -42,7 +42,6 @@ import qualified Data.Map.Strict as Map import Data.Set ( Set ) -import qualified Data.Set as Set import qualified Generics.SOP as SOP import GHC.Generics ( Generic @@ -83,15 +82,25 @@ instance Unparse variable => Unparse (UnifiedVariable variable) where unparse = foldMapVariable unparse unparse2 = foldMapVariable unparse2 -instance FreshVariable variable => FreshVariable (UnifiedVariable variable) +instance + FreshPartialOrd variable => FreshPartialOrd (UnifiedVariable variable) where - refreshVariable avoid = \case - SetVar v -> SetVar <$> refreshVariable setVars v - ElemVar v -> ElemVar <$> refreshVariable elemVars v - where - avoid' = Set.toList avoid - setVars = Set.fromList [v | SetVar v <- avoid'] - elemVars = Set.fromList [v | ElemVar v <- avoid'] + compareFresh (ElemVar elemVar1) (ElemVar elemVar2) = + compareFresh elemVar1 elemVar2 + compareFresh (SetVar elemVar1) (SetVar elemVar2) = + compareFresh elemVar1 elemVar2 + compareFresh _ _ = Nothing + + supVariable (ElemVar elemVar) = ElemVar (supVariable elemVar) + supVariable (SetVar setVar) = SetVar (supVariable setVar) + + nextVariable (ElemVar elemVar1) (ElemVar elemVar2) = + ElemVar (nextVariable elemVar1 elemVar2) + nextVariable (SetVar setVar1) (SetVar setVar2) = + SetVar (nextVariable setVar1 setVar2) + nextVariable _ _ = error "The impossible happened!" + +instance FreshPartialOrd variable => FreshVariable (UnifiedVariable variable) isElemVar :: UnifiedVariable variable -> Bool isElemVar (ElemVar _) = True diff --git a/kore/test/Test/Kore/Builtin.hs b/kore/test/Test/Kore/Builtin.hs index dfc7c5805a..1b77012fd2 100644 --- a/kore/test/Test/Kore/Builtin.hs +++ b/kore/test/Test/Kore/Builtin.hs @@ -115,10 +115,10 @@ test_internalize = mkSet = Set.asInternal . Data.Set.fromList s = mkElemVar (elemVarS "s" setSort) - mkInt :: FreshVariable variable => Integer -> TermLike variable + mkInt :: InternalVariable variable => Integer -> TermLike variable mkInt = Int.asInternal intSort = Builtin.intSort - zero, one :: FreshVariable variable => TermLike variable + zero, one :: InternalVariable variable => TermLike variable zero = mkInt 0 one = mkInt 1 x = mkElemVar (elemVarS "x" intSort) diff --git a/kore/test/Test/Kore/Builtin/Int.hs b/kore/test/Test/Kore/Builtin/Int.hs index 93ecb89e8d..58abcc1cb9 100644 --- a/kore/test/Test/Kore/Builtin/Int.hs +++ b/kore/test/Test/Kore/Builtin/Int.hs @@ -363,7 +363,7 @@ intLiteral :: Integer -> TermLike Variable intLiteral = asInternal -- | Specialize 'Int.asInternal' to the builtin sort 'intSort'. -asInternal :: FreshVariable variable => Integer -> TermLike variable +asInternal :: InternalVariable variable => Integer -> TermLike variable asInternal = Int.asInternal intSort -- | Specialize 'asInternal' to the builtin sort 'intSort'. diff --git a/kore/test/Test/Kore/Builtin/Map.hs b/kore/test/Test/Kore/Builtin/Map.hs index 7ebec196aa..6ed8e6db57 100644 --- a/kore/test/Test/Kore/Builtin/Map.hs +++ b/kore/test/Test/Kore/Builtin/Map.hs @@ -1184,7 +1184,7 @@ test_renormalize = x = mkIntVar (testId "x") v = mkIntVar (testId "v") - k1, k2 :: FreshVariable variable => TermLike variable + k1, k2 :: InternalVariable variable => TermLike variable k1 = Test.Int.asInternal 1 k2 = Test.Int.asInternal 2 diff --git a/kore/test/Test/Kore/Internal/Pattern.hs b/kore/test/Test/Kore/Internal/Pattern.hs index e83dad7a13..e100967a0b 100644 --- a/kore/test/Test/Kore/Internal/Pattern.hs +++ b/kore/test/Test/Kore/Internal/Pattern.hs @@ -7,14 +7,6 @@ import Prelude.Kore import Test.Tasty -import qualified Data.Set as Set -import Data.Text.Prettyprint.Doc -import qualified Generics.SOP as SOP -import qualified GHC.Generics as GHC - -import Kore.Debug - ( Debug - ) import Kore.Internal.Pattern as Pattern ( Conditional (..) , mapVariables @@ -32,7 +24,6 @@ import Kore.Internal.Predicate ) import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.TermLike -import Kore.Unparser import Kore.Variables.UnifiedVariable ( UnifiedVariable (..) ) @@ -44,6 +35,8 @@ import Test.Kore import Test.Kore.Internal.TermLike ( termLikeChildGen ) +import Test.Kore.Variables.V +import Test.Kore.Variables.W import Test.Tasty.HUnit.Ext internalPatternGen :: Gen (Internal.Pattern Variable) @@ -55,17 +48,17 @@ test_expandedPattern = [ testCase "Mapping variables" (assertEqual "" Conditional - { term = war "1" - , predicate = makeEquals (war "2") (war "3") + { term = war' "1" + , predicate = makeEquals (war' "2") (war' "3") , substitution = Substitution.wrap - [(ElemVar . ElementVariable $ W "4", war "5")] + [(ElemVar . ElementVariable $ mkW "4", war' "5")] } (Pattern.mapVariables (fmap showVar) (fmap showVar) Conditional - { term = var 1 - , predicate = makeEquals (var 2) (var 3) + { term = var' 1 + , predicate = makeEquals (var' 2) (var' 3) , substitution = Substitution.wrap - [(ElemVar . ElementVariable $ V 4, var 5)] + [(ElemVar . ElementVariable $ mkV 4, var' 5)] } ) ) @@ -73,41 +66,41 @@ test_expandedPattern = (assertEqual "" (makeAnd (makeAnd - (var 1) - (makeEq (var 2) (var 3)) + (var' 1) + (makeEq (var' 2) (var' 3)) ) - (makeEq (var 4) (var 5)) + (makeEq (var' 4) (var' 5)) ) (Pattern.toTermLike Conditional - { term = var 1 - , predicate = makeEquals (var 2) (var 3) + { term = var' 1 + , predicate = makeEquals (var' 2) (var' 3) , substitution = Substitution.wrap - [(ElemVar . ElementVariable $ V 4, var 5)] + [(ElemVar . ElementVariable $ mkV 4, var' 5)] } ) ) , testCase "Converting to a ML pattern - top pattern" (assertEqual "" (makeAnd - (makeEq (var 2) (var 3)) - (makeEq (var 4) (var 5)) + (makeEq (var' 2) (var' 3)) + (makeEq (var' 4) (var' 5)) ) (Pattern.toTermLike Conditional { term = mkTop sortVariable - , predicate = makeEquals (var 2) (var 3) + , predicate = makeEquals (var' 2) (var' 3) , substitution = Substitution.wrap - [(ElemVar . ElementVariable $ V 4, var 5)] + [(ElemVar . ElementVariable $ mkV 4, var' 5)] } ) ) , testCase "Converting to a ML pattern - top predicate" (assertEqual "" - (var 1) + (var' 1) (Pattern.toTermLike Conditional - { term = var 1 + { term = var' 1 , predicate = makeTruePredicate_ , substitution = mempty } @@ -119,9 +112,9 @@ test_expandedPattern = (Pattern.toTermLike Conditional { term = mkBottom sortVariable - , predicate = makeEquals (var 2) (var 3) + , predicate = makeEquals (var' 2) (var' 3) , substitution = Substitution.wrap - [(ElemVar . ElementVariable $ V 4, var 5)] + [(ElemVar . ElementVariable $ mkV 4, var' 5)] } ) ) @@ -130,7 +123,7 @@ test_expandedPattern = (mkBottom sortVariable) (Pattern.toTermLike Conditional - { term = var 1 + { term = var' 1 , predicate = makeFalsePredicate_ , substitution = mempty } @@ -138,89 +131,6 @@ test_expandedPattern = ) ] -newtype V = V Integer - deriving (Show, Eq, Ord, GHC.Generic) - -instance SOP.Generic V - -instance SOP.HasDatatypeInfo V - -instance Debug V - -instance Diff V - -instance Unparse V where - unparse (V n) = "V" <> pretty n <> ":" <> unparse sortVariable - unparse2 = undefined - -instance SortedVariable V where - sortedVariableSort _ = sortVariable - -instance From Variable V where - from = error "Not implemented" - -instance From V Variable where - from = error "Not implemented" - -instance VariableName V - -instance FreshVariable V where - refreshVariable avoiding v@(V name) - | Set.notMember v avoiding = Nothing - | otherwise = - Just ((head . dropWhile (flip Set.member avoiding)) (V <$> names' )) - where - names' = iterate (+ 1) name - -instance SubstitutionOrd V where - compareSubstitution = compare - -newtype W = W String - deriving (Show, Eq, Ord, GHC.Generic) - -instance SOP.Generic W - -instance SOP.HasDatatypeInfo W - -instance Debug W - -instance Diff W - -instance Unparse W where - unparse (W name) = "W" <> pretty name <> ":" <> unparse sortVariable - unparse2 = undefined - -instance SortedVariable W where - sortedVariableSort _ = sortVariable - -instance From Variable W where - from = error "Not implemented" - -instance From W Variable where - from = error "Not implemented" - -instance VariableName W - -instance FreshVariable W where - refreshVariable avoiding w@(W name) - | Set.notMember w avoiding = Nothing - | otherwise = - Just ((head . dropWhile (flip Set.member avoiding)) (W <$> names' )) - where - names' = iterate (<> "\'") name - -instance SubstitutionOrd W where - compareSubstitution = compare - -showVar :: V -> W -showVar (V i) = W (show i) - -var :: Integer -> TermLike V -var = mkElemVar . ElementVariable . V - -war :: String -> TermLike W -war = mkElemVar . ElementVariable . W - makeEq :: InternalVariable var => TermLike var @@ -235,6 +145,3 @@ makeEquals :: InternalVariable var => TermLike var -> TermLike var -> Predicate var makeEquals p1 p2 = makeEqualsPredicate_ p1 p2 - -sortVariable :: Sort -sortVariable = SortVariableSort (SortVariable (Id "#a" AstLocationTest)) diff --git a/kore/test/Test/Kore/Step/Function/Integration.hs b/kore/test/Test/Kore/Step/Function/Integration.hs index 020e35ae55..3763368432 100644 --- a/kore/test/Test/Kore/Step/Function/Integration.hs +++ b/kore/test/Test/Kore/Step/Function/Integration.hs @@ -1348,7 +1348,7 @@ appliedMockEvaluator result = mapVariables :: forall variable - . (FreshVariable variable, VariableName variable) + . InternalVariable variable => Pattern Variable -> Pattern variable mapVariables = diff --git a/kore/test/Test/Kore/Step/MockSymbols.hs b/kore/test/Test/Kore/Step/MockSymbols.hs index 124e733bf1..3b57560cb4 100644 --- a/kore/test/Test/Kore/Step/MockSymbols.hs +++ b/kore/test/Test/Kore/Step/MockSymbols.hs @@ -73,8 +73,7 @@ import Kore.Internal.Symbol hiding ( sortInjection ) import Kore.Internal.TermLike - ( FreshVariable - , InternalVariable + ( InternalVariable , TermLike ) import qualified Kore.Internal.TermLike as Internal @@ -1710,7 +1709,7 @@ builtinSet child = } builtinInt - :: FreshVariable variable + :: InternalVariable variable => Integer -> TermLike variable builtinInt = Builtin.Int.asInternal intSort @@ -1722,7 +1721,7 @@ builtinBool builtinBool = Builtin.Bool.asInternal boolSort builtinString - :: FreshVariable variable + :: InternalVariable variable => Text -> TermLike variable builtinString = Builtin.String.asInternal stringSort diff --git a/kore/test/Test/Kore/Step/Simplifier.hs b/kore/test/Test/Kore/Step/Simplifier.hs index 482c56960a..f559ff2cbf 100644 --- a/kore/test/Test/Kore/Step/Simplifier.hs +++ b/kore/test/Test/Kore/Step/Simplifier.hs @@ -75,7 +75,7 @@ mockSimplifierHelper convertTermLikeVariables :: ( VariableName variable , VariableName variable0 - , FreshVariable variable0 + , FreshPartialOrd variable0 ) => TermLike variable -> TermLike variable0 @@ -87,7 +87,7 @@ convertTermLikeVariables = convertPatternVariables :: ( VariableName variable , VariableName variable0 - , FreshVariable variable0 + , FreshPartialOrd variable0 ) => Pattern variable -> Pattern variable0 diff --git a/kore/test/Test/Kore/Unification/Unifier.hs b/kore/test/Test/Kore/Unification/Unifier.hs index bd2c324f0d..1e8bad4d16 100644 --- a/kore/test/Test/Kore/Unification/Unifier.hs +++ b/kore/test/Test/Kore/Unification/Unifier.hs @@ -19,15 +19,11 @@ import Data.List.NonEmpty ( NonEmpty ((:|)) ) import qualified Data.Map.Strict as Map -import qualified Data.Set as Set import Data.Text ( Text ) import qualified Data.Text.Prettyprint.Doc as Pretty -import qualified Generics.SOP as SOP -import qualified GHC.Generics as GHC -import Kore.Debug import qualified Kore.Internal.Condition as Condition import qualified Kore.Internal.MultiOr as MultiOr import Kore.Internal.Pattern as Pattern @@ -66,6 +62,8 @@ import qualified SMT import Test.Kore import qualified Test.Kore.Step.MockSymbols as Mock +import Test.Kore.Variables.V +import Test.Kore.Variables.W import Test.Tasty.HUnit.Ext var :: Text -> Sort -> ElementVariable Variable @@ -532,13 +530,13 @@ test_unification = -} , testCase "Maps substitution variables" (assertEqual "" - [(ElemVar $ ElementVariable $ W "1", war' "2")] + [(ElemVar $ ElementVariable $ mkW "1", war' "2")] (Substitution.unwrap . Substitution.mapVariables (fmap showVar) (fmap showVar) . Substitution.wrap - $ [(ElemVar $ ElementVariable $ V 1, var' 2)] + $ [(ElemVar $ ElementVariable $ mkV 1, var' 2)] ) ) , testCase "framed Map with concrete Map" $ @@ -670,92 +668,6 @@ test_unsupportedConstructs = (mkImplies a (mkNext a1)) ) -newtype V = V Integer - deriving (Eq, GHC.Generic, Ord, Show) - -instance SOP.Generic V - -instance SOP.HasDatatypeInfo V - -instance Debug V - -instance Diff V - -instance SortedVariable V where - sortedVariableSort _ = sortVar - -instance From Variable V where - from = error "Not implemented" - -instance From V Variable where - from = error "Not implemented" - -instance VariableName V - -instance Unparse V where - unparse = error "Not implemented" - unparse2 = error "Not implemented" - -instance FreshVariable V where - refreshVariable avoiding v@(V name) - | Set.notMember v avoiding = Nothing - | otherwise = - Just ((head . dropWhile (flip Set.member avoiding)) (V <$> names' )) - where - names' = iterate (+ 1) name - -instance SubstitutionOrd V where - compareSubstitution = compare - -newtype W = W String - deriving (Eq, GHC.Generic, Ord, Show) - -instance SOP.Generic W - -instance SOP.HasDatatypeInfo W - -instance Debug W - -instance Diff W - -instance SortedVariable W where - sortedVariableSort _ = sortVar - -instance From Variable W where - from = error "Not implemented" - -instance From W Variable where - from = error "Not implemented" - -instance VariableName W - -instance Unparse W where - unparse = error "Not implemented" - unparse2 = error "Not implemented" - -instance FreshVariable W where - refreshVariable avoiding w@(W name) - | Set.notMember w avoiding = Nothing - | otherwise = - Just ((head . dropWhile (flip Set.member avoiding)) (W <$> names' )) - where - names' = iterate (<> "\'") name - -instance SubstitutionOrd W where - compareSubstitution = compare - -showVar :: V -> W -showVar (V i) = W (show i) - -var' :: Integer -> TermLike V -var' = mkElemVar . ElementVariable . V - -war' :: String -> TermLike W -war' = mkElemVar . ElementVariable . W - -sortVar :: Sort -sortVar = SortVariableSort (SortVariable (Id "#a" AstLocationTest)) - injUnificationTests :: [TestTree] injUnificationTests = [ testCase "Injected Variable" $ diff --git a/kore/test/Test/Kore/Variables/V.hs b/kore/test/Test/Kore/Variables/V.hs new file mode 100644 index 0000000000..feba093d36 --- /dev/null +++ b/kore/test/Test/Kore/Variables/V.hs @@ -0,0 +1,72 @@ +module Test.Kore.Variables.V + ( V (..), mkV, var' + , sortVariable + ) where + +import Prelude.Kore + +import qualified Generics.SOP as SOP +import qualified GHC.Generics as GHC +import Numeric.Natural + +import Data.Sup +import Debug +import Kore.Internal.TermLike +import Kore.Unparser +import Kore.Variables.Fresh +import Pretty + +data V = + V { value :: Integer, counter :: Maybe (Sup Natural) } + deriving (Show, Eq, Ord, GHC.Generic) + +mkV :: Integer -> V +mkV value = V { value, counter = Nothing } + +instance SOP.Generic V + +instance SOP.HasDatatypeInfo V + +instance Debug V + +instance Diff V + +instance Unparse V where + unparse (V n _) = "V" <> pretty n <> ":" <> unparse sortVariable + unparse2 = undefined + +instance SortedVariable V where + sortedVariableSort _ = sortVariable + +instance From Variable V where + from = error "Not implemented" + +instance From V Variable where + from = error "Not implemented" + +instance VariableName V + +instance FreshPartialOrd V where + compareFresh (V a an) (V b bn) + | a == b = Just (compare an bn) + | otherwise = Nothing + supVariable v = v { counter = Just Sup } + nextVariable v V { counter } = + v { counter = counter' } + where + counter' = + case counter of + Nothing -> Just (Element 0) + Just (Element a) -> Just (Element (succ a)) + Just Sup -> illegalVariableCounter + +instance FreshVariable V + +instance SubstitutionOrd V where + compareSubstitution = compare + +var' :: Integer -> TermLike V +var' = mkElemVar . ElementVariable . mkV + +sortVariable :: Sort +sortVariable = SortVariableSort (SortVariable (Id "#a" AstLocationTest)) diff --git a/kore/test/Test/Kore/Variables/W.hs b/kore/test/Test/Kore/Variables/W.hs new file mode 100644 index 0000000000..fe20eb71f5 --- /dev/null +++ b/kore/test/Test/Kore/Variables/W.hs @@ -0,0 +1,73 @@ +module Test.Kore.Variables.W + ( W, mkW, war' + , showVar + ) where + +import Prelude.Kore + +import qualified Generics.SOP as SOP +import qualified GHC.Generics as GHC +import Numeric.Natural + +import Data.Sup +import Debug +import Kore.Internal.TermLike +import Kore.Unparser +import Kore.Variables.Fresh +import Pretty + +import Test.Kore.Variables.V + +data W = W { value :: String, counter :: Maybe (Sup Natural) } + deriving (Show, Eq, Ord, GHC.Generic) + +mkW :: String -> W +mkW value = W { value, counter = Nothing } + +instance SOP.Generic W + +instance SOP.HasDatatypeInfo W + +instance Debug W + +instance Diff W + +instance Unparse W where + unparse (W name _) = "W" <> pretty name <> ":" <> unparse sortVariable + unparse2 = undefined + +instance SortedVariable W where + sortedVariableSort _ = sortVariable + +instance From Variable W where + from = error "Not implemented" + +instance From W Variable where + from = error "Not implemented" + +instance VariableName W + +instance FreshPartialOrd W where + compareFresh (W a an) (W b bn) + | a == b = Just (compare an bn) + | otherwise = Nothing + supVariable w = w { counter = Just Sup } + nextVariable w W { counter } = + w { counter = counter' } + where + counter' = + case counter of + Nothing -> Just (Element 0) + Just (Element a) -> Just (Element (succ a)) + Just Sup -> illegalVariableCounter + +instance FreshVariable W + +instance SubstitutionOrd W where + compareSubstitution = compare + +showVar :: V -> W +showVar (V i n) = W (show i) n + +war' :: String -> TermLike W +war' = mkElemVar . ElementVariable . mkW From cbedf142de3ccea006ae7fe48a2c40b7c4db69fc Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 12 Feb 2020 12:13:04 -0600 Subject: [PATCH 06/21] FreshVariable: Precise property tests --- kore/src/Kore/Variables/Fresh.hs | 42 +++++++++---- kore/test/Test/Kore/Variables/Fresh.hs | 83 ++++++++++++++++++++++++++ 2 files changed, 114 insertions(+), 11 deletions(-) diff --git a/kore/src/Kore/Variables/Fresh.hs b/kore/src/Kore/Variables/Fresh.hs index 6a670857ea..b302e6501a 100644 --- a/kore/src/Kore/Variables/Fresh.hs +++ b/kore/src/Kore/Variables/Fresh.hs @@ -12,6 +12,7 @@ module Kore.Variables.Fresh import Prelude.Kore +import qualified Control.Lens as Lens import qualified Data.Foldable as Foldable import Data.Function ( on @@ -19,6 +20,9 @@ import Data.Function import Data.Functor ( ($>) ) +import Data.Generics.Product + ( field + ) import Data.Map.Strict ( Map ) @@ -40,13 +44,28 @@ Agreement: prop> maybe True (== compare a b) (compareFresh a b) +Relevance: + +prop> compareFresh a (supVariable a) \/= Nothing + +prop> a \/= supVariable a && x \/= supVariable x ==> compareFresh a (nextVariable a x) \/= Nothing + +Idempotence: + +prop> supVariable a == supVariable (supVariable a) + Dominance: -prop> maybe False (\/= GT) (compareFresh a (supVariable a)) +prop> a \/= supVariable a ==> compareFresh a (supVariable a) == Just LT -Increment: +Monotonicity: -prop> compareFresh a (nextVariable a x) == Just LT +prop> a \/= supVariable a && x \/= supVariable x ==> compareFresh a (nextVariable a x) == Just LT + +Note: The monotonicity property of 'nextVariable' implies the relevance +property. + +prop> a \/= supVariable a && x \/= supVariable x ==> maybe True (== LT) (compareFresh x (nextVariable a x)) -} class Ord variable => FreshPartialOrd variable where @@ -61,22 +80,23 @@ instance FreshPartialOrd Variable where compareFresh x y | variableName x == variableName y = Just $ compare x y | otherwise = Nothing + {-# INLINE compareFresh #-} supVariable variable = variable { variableCounter = Just Sup } + {-# INLINE supVariable #-} - nextVariable variable Variable { variableName, variableCounter } = + nextVariable variable Variable { variableCounter = boundary } = variable - { variableName = variableName' - , variableCounter = variableCounter' - } + & Lens.set (field @"variableName" . field @"idLocation") generated + & Lens.over (field @"variableCounter") (increment . max boundary) where - variableName' = - variableName { idLocation = AstLocationGeneratedVariable } - variableCounter' = - case variableCounter of + generated = AstLocationGeneratedVariable + increment = + \case Nothing -> Just (Element 0) Just (Element a) -> Just (Element (succ a)) Just Sup -> illegalVariableCounter + {-# INLINE nextVariable #-} instance FreshPartialOrd Concrete where compareFresh = \case {} diff --git a/kore/test/Test/Kore/Variables/Fresh.hs b/kore/test/Test/Kore/Variables/Fresh.hs index b49759c7f9..43bdb10cf5 100644 --- a/kore/test/Test/Kore/Variables/Fresh.hs +++ b/kore/test/Test/Kore/Variables/Fresh.hs @@ -2,13 +2,27 @@ module Test.Kore.Variables.Fresh ( test_refreshVariable + , test_FreshPartialOrd_Variable + -- * Test patterns + , testFreshPartialOrd + , variableGen + , counterGen + , sortGen + , idGen ) where import Prelude.Kore +import Hedgehog +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range import Test.Tasty +import Test.Tasty.Hedgehog import Test.Tasty.HUnit +import Control.Monad + ( when + ) import Data.Maybe ( fromJust ) @@ -16,7 +30,9 @@ import Data.Set ( Set ) import qualified Data.Set as Set +import Numeric.Natural +import Data.Sup import Kore.Sort import Kore.Syntax.ElementVariable ( ElementVariable (..) @@ -32,6 +48,14 @@ import Kore.Variables.UnifiedVariable ) import Test.Kore + ( idGen + , testId + ) +import Test.Kore.Step.MockSymbols + ( subSort + , testSort + , topSort + ) metaVariable :: Variable metaVariable = Variable @@ -296,3 +320,62 @@ test_refreshVariable = unifiedSetNonTargetOriginal = unifiedNonTarget unifiedSetOriginal avoidUET = Set.singleton unifiedElemNonTargetOriginal avoidUST = Set.singleton unifiedSetTargetOriginal + +-- | Property tests of a 'FreshPartialOrd' instance using the given generator. +testFreshPartialOrd + :: (Show variable, FreshPartialOrd variable) + => Gen variable + -> [TestTree] +testFreshPartialOrd gen = + [ testProperty "supVariable is relevant" $ property $ do + x <- forAll gen + compareFresh x (supVariable x) /== Nothing + , testProperty "supVariable is idempotent" $ property $ do + x <- forAll gen + let xSup = supVariable x + xSupSup = supVariable xSup + xSup === xSupSup + , testProperty "supVariable dominates other variables" $ property $ do + x <- forAll gen + let sup = supVariable x + when (x == sup) discard + compareFresh x (supVariable x) === Just LT + , testProperty "nextVariable is relevant" $ property $ do + x <- forAll gen + y <- forAll gen + when (x == supVariable x) discard + when (y == supVariable y) discard + let x' = nextVariable x y + annotateShow x' + compareFresh x x' /== Nothing + , testProperty "nextVariable is monotonic" $ property $ do + x <- forAll gen + y <- forAll gen + when (x == supVariable x) discard + when (y == supVariable y) discard + let x' = nextVariable x y + annotateShow x' + compareFresh x x' === Just LT + case compareFresh y x' of + Nothing -> return () + Just ordering -> ordering === LT + ] + +test_FreshPartialOrd_Variable :: TestTree +test_FreshPartialOrd_Variable = + testGroup "instance FreshPartialOrd Variable" + $ testFreshPartialOrd variableGen + +variableGen :: MonadGen gen => gen Variable +variableGen = Variable <$> idGen <*> counterGen <*> sortGen + +counterGen :: MonadGen gen => gen (Maybe (Sup Natural)) +counterGen = + Gen.frequency + [ (2, pure Nothing) + , (4, Just . Element <$> Gen.integral (Range.linear 0 256)) + , (1, pure $ Just Sup) + ] + +sortGen :: MonadGen gen => gen Sort +sortGen = Gen.element [testSort, topSort, subSort] From 2ee928ffd2fd6becca065f630488cd1d8a410547 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 12 Feb 2020 12:55:28 -0600 Subject: [PATCH 07/21] Test.Kore.Variables.Fresh: FreshPartialOrd instance tests --- kore/test/Test/Kore/Variables/Fresh.hs | 37 +++++++++++++++++++++----- 1 file changed, 31 insertions(+), 6 deletions(-) diff --git a/kore/test/Test/Kore/Variables/Fresh.hs b/kore/test/Test/Kore/Variables/Fresh.hs index 43bdb10cf5..e5e134e143 100644 --- a/kore/test/Test/Kore/Variables/Fresh.hs +++ b/kore/test/Test/Kore/Variables/Fresh.hs @@ -3,12 +3,9 @@ module Test.Kore.Variables.Fresh ( test_refreshVariable , test_FreshPartialOrd_Variable - -- * Test patterns - , testFreshPartialOrd - , variableGen - , counterGen - , sortGen - , idGen + , test_FreshPartialOrd_ElementVariable + , test_FreshPartialOrd_SetVariable + , test_FreshPartialOrd_UnifiedVariable ) where import Prelude.Kore @@ -366,6 +363,21 @@ test_FreshPartialOrd_Variable = testGroup "instance FreshPartialOrd Variable" $ testFreshPartialOrd variableGen +test_FreshPartialOrd_ElementVariable :: TestTree +test_FreshPartialOrd_ElementVariable = + testGroup "instance FreshPartialOrd (ElementVariable Variable)" + $ testFreshPartialOrd elementVariableGen + +test_FreshPartialOrd_SetVariable :: TestTree +test_FreshPartialOrd_SetVariable = + testGroup "instance FreshPartialOrd (SetVariable Variable)" + $ testFreshPartialOrd setVariableGen + +test_FreshPartialOrd_UnifiedVariable :: TestTree +test_FreshPartialOrd_UnifiedVariable = + testGroup "instance FreshPartialOrd (UnifiedVariable Variable)" + $ testFreshPartialOrd unifiedVariableGen + variableGen :: MonadGen gen => gen Variable variableGen = Variable <$> idGen <*> counterGen <*> sortGen @@ -379,3 +391,16 @@ counterGen = sortGen :: MonadGen gen => gen Sort sortGen = Gen.element [testSort, topSort, subSort] + +elementVariableGen :: MonadGen gen => gen (ElementVariable Variable) +elementVariableGen = ElementVariable <$> variableGen + +setVariableGen :: MonadGen gen => gen (SetVariable Variable) +setVariableGen = SetVariable <$> variableGen + +unifiedVariableGen :: MonadGen gen => gen (UnifiedVariable Variable) +unifiedVariableGen = + Gen.choice + [ ElemVar <$> elementVariableGen + , SetVar <$> setVariableGen + ] From 910f2b4046124ddd18f02fc159396b06df4cf22e Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 13 Feb 2020 10:09:31 -0600 Subject: [PATCH 08/21] FreshPartialOrd: Simplify algebra --- kore/src/Kore/Internal/TermLike/TermLike.hs | 35 ++++--- kore/src/Kore/Variables/Fresh.hs | 105 ++++++++++++++------ kore/src/Kore/Variables/Target.hs | 6 +- kore/src/Kore/Variables/UnifiedVariable.hs | 13 ++- kore/test/Test/Kore/Step/RewriteStep.hs | 9 +- kore/test/Test/Kore/Variables/Fresh.hs | 22 ++-- kore/test/Test/Kore/Variables/V.hs | 17 ++-- kore/test/Test/Kore/Variables/W.hs | 17 ++-- 8 files changed, 143 insertions(+), 81 deletions(-) diff --git a/kore/src/Kore/Internal/TermLike/TermLike.hs b/kore/src/Kore/Internal/TermLike/TermLike.hs index b1a038978f..383966e5e3 100644 --- a/kore/src/Kore/Internal/TermLike/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike/TermLike.hs @@ -888,33 +888,32 @@ externalizeFreshVariables termLike = among the set of avoided variables. The externalized form is returned. -} - safeElementVariable - :: FreeVariables Variable - -> ElementVariable Variable - -> ElementVariable Variable - safeElementVariable avoiding variable = - head -- 'head' is safe because 'iterate' creates an infinite list + safeVariable + :: (Functor f, FreshPartialOrd (f Variable)) + => (f Variable -> UnifiedVariable Variable) + -> FreeVariables Variable + -> f Variable + -> f Variable + safeVariable mk avoiding variable = + head $ dropWhile wouldCapture $ externalize - <$> iterate nextVariable variable + <$> iterate Fresh.incrementVariable variable where - wouldCapture var = isFreeVariable (ElemVar var) avoiding - nextVariable = Fresh.nextVariable variable + wouldCapture var = isFreeVariable (mk var) avoiding externalize = fmap Variable.externalizeFreshVariable + safeElementVariable + :: FreeVariables Variable + -> ElementVariable Variable + -> ElementVariable Variable + safeElementVariable = safeVariable ElemVar + safeSetVariable :: FreeVariables Variable -> SetVariable Variable -> SetVariable Variable - safeSetVariable avoiding variable = - head -- 'head' is safe because 'iterate' creates an infinite list - $ dropWhile wouldCapture - $ externalize - <$> iterate nextVariable variable - where - wouldCapture var = isFreeVariable (SetVar var) avoiding - nextVariable = Fresh.nextVariable variable - externalize = fmap Variable.externalizeFreshVariable + safeSetVariable = safeVariable SetVar underElementBinder freeVariables' variable child = do let variable' = safeElementVariable freeVariables' variable diff --git a/kore/src/Kore/Variables/Fresh.hs b/kore/src/Kore/Variables/Fresh.hs index b302e6501a..8e356e4e7c 100644 --- a/kore/src/Kore/Variables/Fresh.hs +++ b/kore/src/Kore/Variables/Fresh.hs @@ -5,6 +5,7 @@ License : UIUC/NCSA module Kore.Variables.Fresh ( FreshPartialOrd (..) , FreshVariable (..) + , incrementVariable , refreshVariables -- * Re-exports , module Kore.Syntax.Variable @@ -17,9 +18,6 @@ import qualified Data.Foldable as Foldable import Data.Function ( on ) -import Data.Functor - ( ($>) - ) import Data.Generics.Product ( field ) @@ -40,6 +38,9 @@ import Kore.Syntax.Variable {- | @FreshPartialOrder@ defines a partial order for renaming variables. +Two variables are related under this partial order when @compareFresh@ returns +@'Just' _@. + Agreement: prop> maybe True (== compare a b) (compareFresh a b) @@ -48,7 +49,9 @@ Relevance: prop> compareFresh a (supVariable a) \/= Nothing -prop> a \/= supVariable a && x \/= supVariable x ==> compareFresh a (nextVariable a x) \/= Nothing +prop> isJust (nextVariable x a) ==> isJust (compareFresh a (nextVariable x a)) + +prop> isJust (nextVariable x a) ==> isJust (compareFresh x (nextVariable x a)) Idempotence: @@ -60,21 +63,58 @@ prop> a \/= supVariable a ==> compareFresh a (supVariable a) == Just LT Monotonicity: -prop> a \/= supVariable a && x \/= supVariable x ==> compareFresh a (nextVariable a x) == Just LT +prop> isJust (nextVariable x a) ==> compareFresh a (nextVariable x a) == Just LT + +prop> isJust (nextVariable x a) ==> compareFresh x (nextVariable x a) == Just LT Note: The monotonicity property of 'nextVariable' implies the relevance property. -prop> a \/= supVariable a && x \/= supVariable x ==> maybe True (== LT) (compareFresh x (nextVariable a x)) - -} class Ord variable => FreshPartialOrd variable where + {- | @compareFresh@ defines a partial order on variables. + + In the typical implementation of fresh name generation, the variable name + consists of a string (the base name) and a counter. Then, all variables with + the same base name are related, and their ordering is given by the counter. + + -} compareFresh :: variable -> variable -> Maybe Ordering + + {- | @supVariable x@ is the greatest variable related to @x@. + + In the typical implementation, the counter has type + @'Maybe' ('Sup' 'Natural')@ + so that @supVariable x@ has a counter @'Just' 'Sup'@. + + -} supVariable :: variable -> variable + + {- | @nextVariable@ generates a fresh variable greater than a given bound. + + The resulting variable, if defined, is /related/ to the /original variable/. + @nextVariable@ returns @'Nothing'@ unless: + + * the /lower bound/ is related to the /original variable/, and + * the /original variable/ is not greater than the /lower bound/. + + When @nextVariable@ returns a value (@'Just' _@), then the result is + strictly greater than both arguments. + + -} nextVariable - :: variable -- ^ original variable - -> variable -- ^ lower bound - -> variable + :: variable -- ^ lower bound + -> variable -- ^ original variable + -> Maybe variable + +incrementVariable :: FreshPartialOrd variable => variable -> variable +incrementVariable original = + case nextVariable original original of + Just incremented -> incremented + Nothing -> + -- This is impossible for any law-abiding instance of + -- FreshPartialOrd. + undefined instance FreshPartialOrd Variable where compareFresh x y @@ -85,17 +125,24 @@ instance FreshPartialOrd Variable where supVariable variable = variable { variableCounter = Just Sup } {-# INLINE supVariable #-} - nextVariable variable Variable { variableCounter = boundary } = - variable - & Lens.set (field @"variableName" . field @"idLocation") generated - & Lens.over (field @"variableCounter") (increment . max boundary) + nextVariable bound original = do + ordering <- compareFresh bound original + case ordering of { LT -> empty; _ -> pure () } + incrementCounter . resetIdLocation $ original where - generated = AstLocationGeneratedVariable - increment = - \case - Nothing -> Just (Element 0) - Just (Element a) -> Just (Element (succ a)) - Just Sup -> illegalVariableCounter + resetIdLocation = + Lens.set + (field @"variableName" . field @"idLocation") + AstLocationGeneratedVariable + incrementCounter = + field @"variableCounter" $ \_ -> + case variableCounter bound of + Nothing -> pure $ Just (Element 0) + Just (Element a) -> pure $ Just (Element (succ a)) + Just Sup -> + -- Never rename (supVariable _) because it does not + -- occur in any pattern. + empty {-# INLINE nextVariable #-} instance FreshPartialOrd Concrete where @@ -113,8 +160,8 @@ instance supVariable = ElementVariable . supVariable . getElementVariable {-# INLINE supVariable #-} - nextVariable (ElementVariable variable) (ElementVariable bound) = - ElementVariable (nextVariable variable bound) + nextVariable (ElementVariable bound) (ElementVariable original) = + ElementVariable <$> nextVariable bound original {-# INLINE nextVariable #-} instance @@ -127,8 +174,8 @@ instance supVariable = SetVariable . supVariable . getSetVariable {-# INLINE supVariable #-} - nextVariable (SetVariable variable) (SetVariable bound) = - SetVariable (nextVariable variable bound) + nextVariable (SetVariable bound) (SetVariable original) = + SetVariable <$> nextVariable bound original {-# INLINE nextVariable #-} {- | A @FreshVariable@ can be renamed to avoid colliding with a set of names. @@ -144,16 +191,18 @@ class Ord variable => FreshVariable variable where -} refreshVariable :: Set variable -- ^ variables to avoid - -> variable -- ^ variable to rename + -> variable -- ^ variable to rename -> Maybe variable default refreshVariable :: FreshPartialOrd variable => Set variable -> variable -> Maybe variable - refreshVariable avoiding variable = do - largest <- Set.lookupLT (supVariable variable) avoiding - compareFresh variable largest $> nextVariable variable largest + refreshVariable avoiding original = do + largest <- Set.lookupLT (supVariable original) avoiding + _ <- compareFresh original largest + nextVariable largest original + {-# INLINE refreshVariable #-} instance FreshPartialOrd variable => FreshVariable (ElementVariable variable) diff --git a/kore/src/Kore/Variables/Target.hs b/kore/src/Kore/Variables/Target.hs index 82008c72db..2d41ae16fb 100644 --- a/kore/src/Kore/Variables/Target.hs +++ b/kore/src/Kore/Variables/Target.hs @@ -55,7 +55,8 @@ instead of 'NonTarget' variables. data Target variable = Target !variable | NonTarget !variable - deriving (GHC.Generic, Show, Functor) + deriving (GHC.Generic, Show) + deriving (Functor, Foldable, Traversable) instance Eq variable => Eq (Target variable) where (==) = on (==) unTarget @@ -148,8 +149,7 @@ instance FreshPartialOrd variable => FreshPartialOrd (Target variable) where supVariable = fmap supVariable {-# INLINE supVariable #-} - nextVariable variable bound = - fmap (flip nextVariable (unTarget bound)) variable + nextVariable (unTarget -> bound) = traverse (nextVariable bound) {-# INLINE nextVariable #-} {- | Ensures that fresh variables are unique under 'unwrapStepperVariable'. diff --git a/kore/src/Kore/Variables/UnifiedVariable.hs b/kore/src/Kore/Variables/UnifiedVariable.hs index f3744be7cb..816a9290f9 100644 --- a/kore/src/Kore/Variables/UnifiedVariable.hs +++ b/kore/src/Kore/Variables/UnifiedVariable.hs @@ -94,11 +94,14 @@ instance supVariable (ElemVar elemVar) = ElemVar (supVariable elemVar) supVariable (SetVar setVar) = SetVar (supVariable setVar) - nextVariable (ElemVar elemVar1) (ElemVar elemVar2) = - ElemVar (nextVariable elemVar1 elemVar2) - nextVariable (SetVar setVar1) (SetVar setVar2) = - SetVar (nextVariable setVar1 setVar2) - nextVariable _ _ = error "The impossible happened!" + nextVariable (ElemVar bound) (ElemVar original) = + ElemVar <$> nextVariable bound original + nextVariable (SetVar bound) (SetVar original) = + SetVar <$> nextVariable bound original + nextVariable _ _ = + -- There is never a need to rename a SetVariable to avoid an + -- ElementVariable, and vice versa. + empty instance FreshPartialOrd variable => FreshVariable (UnifiedVariable variable) diff --git a/kore/test/Test/Kore/Step/RewriteStep.hs b/kore/test/Test/Kore/Step/RewriteStep.hs index 1c1024a4bb..0057d47e37 100644 --- a/kore/test/Test/Kore/Step/RewriteStep.hs +++ b/kore/test/Test/Kore/Step/RewriteStep.hs @@ -82,7 +82,7 @@ import Kore.Unification.UnifierT , runUnifierT ) import Kore.Variables.Fresh - ( nextVariable + ( incrementVariable ) import Kore.Variables.Target ( Target @@ -351,7 +351,7 @@ test_applyRewriteRule_ = , testCase "quantified rhs: non-clashing" $ do let expect = Right [ OrPattern.fromPatterns [Pattern.fromTermLike final] ] - x'' = nextVariable Mock.x . nextVariable Mock.x $ Mock.x + x'' = incrementVariable . incrementVariable $ Mock.x final = mkElemVar x'' initial = pure (mkElemVar Mock.y) axiom = @@ -466,9 +466,10 @@ test_applyRewriteRule_ = -- vs -- sigma(a, i(b)) with substitution b=a , testCase "non-function substitution error" $ do - let expect = Left $ UnificationError $ unsupportedPatterns + let x' = incrementVariable Mock.x + expect = Left $ UnificationError $ unsupportedPatterns "Unknown unification case." - (mkElemVar (nextVariable Mock.x Mock.x)) + (mkElemVar x') (Mock.plain10 (mkElemVar Mock.y)) initial = pure $ Mock.sigma (mkElemVar Mock.x) (Mock.plain10 (mkElemVar Mock.y)) diff --git a/kore/test/Test/Kore/Variables/Fresh.hs b/kore/test/Test/Kore/Variables/Fresh.hs index e5e134e143..bb35df72f9 100644 --- a/kore/test/Test/Kore/Variables/Fresh.hs +++ b/kore/test/Test/Kore/Variables/Fresh.hs @@ -342,20 +342,24 @@ testFreshPartialOrd gen = y <- forAll gen when (x == supVariable x) discard when (y == supVariable y) discard - let x' = nextVariable x y - annotateShow x' - compareFresh x x' /== Nothing + case nextVariable y x of + Nothing -> discard + Just x' -> do + annotateShow x' + compareFresh x x' /== Nothing , testProperty "nextVariable is monotonic" $ property $ do x <- forAll gen y <- forAll gen when (x == supVariable x) discard when (y == supVariable y) discard - let x' = nextVariable x y - annotateShow x' - compareFresh x x' === Just LT - case compareFresh y x' of - Nothing -> return () - Just ordering -> ordering === LT + case nextVariable y x of + Nothing -> discard + Just x' -> do + annotateShow x' + compareFresh x x' === Just LT + case compareFresh y x' of + Nothing -> return () + Just ordering -> ordering === LT ] test_FreshPartialOrd_Variable :: TestTree diff --git a/kore/test/Test/Kore/Variables/V.hs b/kore/test/Test/Kore/Variables/V.hs index feba093d36..9e5a1330d0 100644 --- a/kore/test/Test/Kore/Variables/V.hs +++ b/kore/test/Test/Kore/Variables/V.hs @@ -5,6 +5,9 @@ module Test.Kore.Variables.V import Prelude.Kore +import Data.Generics.Product + ( field + ) import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC import Numeric.Natural @@ -51,14 +54,14 @@ instance FreshPartialOrd V where | a == b = Just (compare an bn) | otherwise = Nothing supVariable v = v { counter = Just Sup } - nextVariable v V { counter } = - v { counter = counter' } + nextVariable V { counter = bound } = + field @"counter" (increment . max bound) where - counter' = - case counter of - Nothing -> Just (Element 0) - Just (Element a) -> Just (Element (succ a)) - Just Sup -> illegalVariableCounter + increment = + \case + Nothing -> pure $ Just (Element 0) + Just (Element a) -> pure $ Just (Element (succ a)) + Just Sup -> empty instance FreshVariable V diff --git a/kore/test/Test/Kore/Variables/W.hs b/kore/test/Test/Kore/Variables/W.hs index fe20eb71f5..a3ef1413a9 100644 --- a/kore/test/Test/Kore/Variables/W.hs +++ b/kore/test/Test/Kore/Variables/W.hs @@ -5,6 +5,9 @@ module Test.Kore.Variables.W import Prelude.Kore +import Data.Generics.Product + ( field + ) import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC import Numeric.Natural @@ -52,14 +55,14 @@ instance FreshPartialOrd W where | a == b = Just (compare an bn) | otherwise = Nothing supVariable w = w { counter = Just Sup } - nextVariable w W { counter } = - w { counter = counter' } + nextVariable W { counter = bound } = + field @"counter" (increment . max bound) where - counter' = - case counter of - Nothing -> Just (Element 0) - Just (Element a) -> Just (Element (succ a)) - Just Sup -> illegalVariableCounter + increment = + \case + Nothing -> pure $ Just (Element 0) + Just (Element a) -> pure $ Just (Element (succ a)) + Just Sup -> empty instance FreshVariable W From 145a53670ff0340933b632513487beeab5005e4e Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 13 Feb 2020 10:41:58 -0600 Subject: [PATCH 09/21] Debug: Better indentation for Set, Map, and Seq --- kore/src/Debug.hs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/kore/src/Debug.hs b/kore/src/Debug.hs index 7e0d1051ad..13c9b134e5 100644 --- a/kore/src/Debug.hs +++ b/kore/src/Debug.hs @@ -338,16 +338,18 @@ fromCofreeT (CofreeT x) = SOP (Z (I x :* Nil)) instance (Debug k, Debug a) => Debug (Map.Map k a) where debugPrec as precOut = - parens (precOut >= 10) ("Data.Map.fromList" <+> debug (Map.toList as)) + (parens (precOut >= 10) . Pretty.sep) + ["Data.Map.fromList", debug (Map.toList as)] instance Debug a => Debug (Set a) where debugPrec as precOut = - parens (precOut >= 10) ("Data.Set.fromList" <+> debug (Set.toList as)) + (parens (precOut >= 10) . Pretty.sep) + ["Data.Set.fromList", debug (Set.toList as)] instance Debug a => Debug (Seq a) where debugPrec as precOut = - parens (precOut >= 10) - $ "Data.Sequence.fromList" <+> debug (Foldable.toList as) + (parens (precOut >= 10) . Pretty.sep) + ["Data.Sequence.fromList", debug (Foldable.toList as)] instance Debug a => Debug (Const a b) From 6ba2de26f544a818ee104316fa9521236efc1a8f Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 13 Feb 2020 11:34:51 -0600 Subject: [PATCH 10/21] Kore.Step.Rule.Expand: Clearer error when variable generation fails --- kore/src/Kore/Step/Rule/Expand.hs | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/kore/src/Kore/Step/Rule/Expand.hs b/kore/src/Kore/Step/Rule/Expand.hs index d36a82ab75..ba2c296d08 100644 --- a/kore/src/Kore/Step/Rule/Expand.hs +++ b/kore/src/Kore/Step/Rule/Expand.hs @@ -19,6 +19,7 @@ import Data.List.NonEmpty import qualified Data.Map.Strict as Map import qualified Data.Set as Set +import qualified Debug import Kore.Attribute.Pattern.FreeVariables ( FreeVariables (getFreeVariables) , freeVariables @@ -71,6 +72,7 @@ import Kore.Variables.UnifiedVariable ( UnifiedVariable (ElemVar) , extractElementVariable ) +import qualified Pretty -- | Instantiate variables on sorts with a single constructor {- TODO(ttuegel): make this a strategy step, so that we expand any @@ -299,17 +301,18 @@ maybeNewVariable then error "Unmatching sort for direct use variable." else (usedVariables, mkElemVar variable) maybeNewVariable usedVariables variable sort UseAsPrototype = - case refreshVariable usedVariables (resort variable) of + case refreshVariable usedVariables variable' of Just newVariable -> ( Set.insert newVariable usedVariables , mkElemVar newVariable ) Nothing -> - (error . unlines) - [ "Expecting a variable refresh for" - , show variable - , "but got nothing. Used variables:" - , show usedVariables + (error . show . Pretty.hang 4 . Pretty.vsep) + [ "Failed to generate a new name for:" + , Pretty.indent 4 $ Debug.debug variable' + , "while avoiding:" + , Pretty.indent 4 $ Debug.debug usedVariables ] where + variable' = resort variable resort (ElementVariable var) = ElementVariable var { variableSort = sort } From e60901cd8ec2ffc08838b50589d4175be0acdb80 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 13 Feb 2020 11:35:35 -0600 Subject: [PATCH 11/21] Test.Kore.Variables.Fresh: New test for refreshVariable --- kore/test/Test/Kore/Variables/Fresh.hs | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/kore/test/Test/Kore/Variables/Fresh.hs b/kore/test/Test/Kore/Variables/Fresh.hs index bb35df72f9..2e4b94e7c0 100644 --- a/kore/test/Test/Kore/Variables/Fresh.hs +++ b/kore/test/Test/Kore/Variables/Fresh.hs @@ -51,6 +51,8 @@ import Test.Kore import Test.Kore.Step.MockSymbols ( subSort , testSort + , testSort0 + , testSort1 , topSort ) @@ -70,7 +72,16 @@ metaVariableDifferentSort = Variable test_refreshVariable :: [TestTree] test_refreshVariable = - [ testGroup "instance FreshVariable Variable" + [ testCase "same name, different sort" $ do + let x0 = Variable (testId "x0") Nothing testSort0 + x1 = x0 { variableSort = testSort1 } + x1' = x1 { variableCounter = Just (Element 0) } + let avoiding = Set.singleton x0 + assertEqual "Expected fresh variable" + (Just x1') + (refreshVariable avoiding x1) + + , testGroup "instance FreshVariable Variable" [ testCase "refreshVariable - avoid empty set" $ assertEqual "Expected no new variable" Nothing From 2444552f9aba7da113a05d6dd40c7eaf4c449717 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 13 Feb 2020 11:35:50 -0600 Subject: [PATCH 12/21] testFreshPartialOrd: Generate related variables --- kore/test/Test/Kore/Variables/Fresh.hs | 71 +++++++++++++++----------- 1 file changed, 41 insertions(+), 30 deletions(-) diff --git a/kore/test/Test/Kore/Variables/Fresh.hs b/kore/test/Test/Kore/Variables/Fresh.hs index 2e4b94e7c0..695d08b19b 100644 --- a/kore/test/Test/Kore/Variables/Fresh.hs +++ b/kore/test/Test/Kore/Variables/Fresh.hs @@ -43,6 +43,7 @@ import Kore.Variables.UnifiedVariable ( UnifiedVariable (..) , mapUnifiedVariable ) +import Pair import Test.Kore ( idGen @@ -329,72 +330,82 @@ test_refreshVariable = avoidUET = Set.singleton unifiedElemNonTargetOriginal avoidUST = Set.singleton unifiedSetTargetOriginal --- | Property tests of a 'FreshPartialOrd' instance using the given generator. +{- | Property tests of a 'FreshPartialOrd' instance using the given generator. + +The generator should produce a 'Pair' of related variables. + + -} testFreshPartialOrd :: (Show variable, FreshPartialOrd variable) - => Gen variable + => Gen (Pair variable) -> [TestTree] testFreshPartialOrd gen = - [ testProperty "supVariable is relevant" $ property $ do - x <- forAll gen + [ testProperty "compareFresh agrees with compare" $ property $ do + Pair x y <- forAll gen + compareFresh x y === Just (compare x y) + compareFresh y x === Just (compare y x) + , testProperty "supVariable is relevant" $ property $ do + Pair x _ <- forAll gen compareFresh x (supVariable x) /== Nothing , testProperty "supVariable is idempotent" $ property $ do - x <- forAll gen + Pair x _ <- forAll gen let xSup = supVariable x xSupSup = supVariable xSup xSup === xSupSup , testProperty "supVariable dominates other variables" $ property $ do - x <- forAll gen + Pair x _ <- forAll gen let sup = supVariable x when (x == sup) discard - compareFresh x (supVariable x) === Just LT + compareFresh x sup === Just LT , testProperty "nextVariable is relevant" $ property $ do - x <- forAll gen - y <- forAll gen + Pair x y <- forAll gen when (x == supVariable x) discard when (y == supVariable y) discard case nextVariable y x of - Nothing -> discard + Nothing -> + compareFresh y x === Just LT Just x' -> do annotateShow x' compareFresh x x' /== Nothing , testProperty "nextVariable is monotonic" $ property $ do - x <- forAll gen - y <- forAll gen + Pair x y <- forAll gen when (x == supVariable x) discard when (y == supVariable y) discard case nextVariable y x of - Nothing -> discard + Nothing -> + compareFresh y x === Just LT Just x' -> do annotateShow x' compareFresh x x' === Just LT - case compareFresh y x' of - Nothing -> return () - Just ordering -> ordering === LT + compareFresh y x' === Just LT ] test_FreshPartialOrd_Variable :: TestTree test_FreshPartialOrd_Variable = testGroup "instance FreshPartialOrd Variable" - $ testFreshPartialOrd variableGen + $ testFreshPartialOrd relatedVariableGen test_FreshPartialOrd_ElementVariable :: TestTree test_FreshPartialOrd_ElementVariable = testGroup "instance FreshPartialOrd (ElementVariable Variable)" - $ testFreshPartialOrd elementVariableGen + $ testFreshPartialOrd relatedElementVariableGen test_FreshPartialOrd_SetVariable :: TestTree test_FreshPartialOrd_SetVariable = testGroup "instance FreshPartialOrd (SetVariable Variable)" - $ testFreshPartialOrd setVariableGen + $ testFreshPartialOrd relatedSetVariableGen test_FreshPartialOrd_UnifiedVariable :: TestTree test_FreshPartialOrd_UnifiedVariable = testGroup "instance FreshPartialOrd (UnifiedVariable Variable)" - $ testFreshPartialOrd unifiedVariableGen + $ testFreshPartialOrd relatedUnifiedVariableGen -variableGen :: MonadGen gen => gen Variable -variableGen = Variable <$> idGen <*> counterGen <*> sortGen +relatedVariableGen :: Gen (Pair Variable) +relatedVariableGen = do + name <- idGen + Pair + <$> (Variable name <$> counterGen <*> sortGen) + <*> (Variable name <$> counterGen <*> sortGen) counterGen :: MonadGen gen => gen (Maybe (Sup Natural)) counterGen = @@ -407,15 +418,15 @@ counterGen = sortGen :: MonadGen gen => gen Sort sortGen = Gen.element [testSort, topSort, subSort] -elementVariableGen :: MonadGen gen => gen (ElementVariable Variable) -elementVariableGen = ElementVariable <$> variableGen +relatedElementVariableGen :: Gen (Pair (ElementVariable Variable)) +relatedElementVariableGen = (fmap . fmap) ElementVariable relatedVariableGen -setVariableGen :: MonadGen gen => gen (SetVariable Variable) -setVariableGen = SetVariable <$> variableGen +relatedSetVariableGen :: Gen (Pair (SetVariable Variable)) +relatedSetVariableGen = (fmap . fmap) SetVariable relatedVariableGen -unifiedVariableGen :: MonadGen gen => gen (UnifiedVariable Variable) -unifiedVariableGen = +relatedUnifiedVariableGen :: Gen (Pair (UnifiedVariable Variable)) +relatedUnifiedVariableGen = Gen.choice - [ ElemVar <$> elementVariableGen - , SetVar <$> setVariableGen + [ (fmap . fmap) ElemVar relatedElementVariableGen + , (fmap . fmap) SetVar relatedSetVariableGen ] From 07d456b9cadcb893686101aa7ba5d613547b3f42 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 13 Feb 2020 11:44:25 -0600 Subject: [PATCH 13/21] refreshVariable: Remove redundant comparison --- kore/src/Kore/Variables/Fresh.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/kore/src/Kore/Variables/Fresh.hs b/kore/src/Kore/Variables/Fresh.hs index 8e356e4e7c..5dac751183 100644 --- a/kore/src/Kore/Variables/Fresh.hs +++ b/kore/src/Kore/Variables/Fresh.hs @@ -200,7 +200,6 @@ class Ord variable => FreshVariable variable where -> Maybe variable refreshVariable avoiding original = do largest <- Set.lookupLT (supVariable original) avoiding - _ <- compareFresh original largest nextVariable largest original {-# INLINE refreshVariable #-} From d13e3db3eb540b412b1ca605048b25ab419724ec Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Fri, 14 Feb 2020 09:48:02 -0600 Subject: [PATCH 14/21] SortedVariable: lensVariableSort --- kore/src/Kore/Syntax/Variable.hs | 24 ++++++++++++++++++---- kore/src/Kore/Variables/Target.hs | 7 +++++-- kore/src/Kore/Variables/UnifiedVariable.hs | 1 + kore/test/Test/Kore/Variables/V.hs | 4 +++- kore/test/Test/Kore/Variables/W.hs | 4 +++- 5 files changed, 32 insertions(+), 8 deletions(-) diff --git a/kore/src/Kore/Syntax/Variable.hs b/kore/src/Kore/Syntax/Variable.hs index d5ff59fa61..57ac6d62f5 100644 --- a/kore/src/Kore/Syntax/Variable.hs +++ b/kore/src/Kore/Syntax/Variable.hs @@ -13,11 +13,15 @@ module Kore.Syntax.Variable , isOriginalVariable , illegalVariableCounter , externalizeFreshVariable + -- * Variable names , VariableName , toVariable , fromVariable + -- * Variable sorts , SortedVariable (..) + , sortedVariableSort , unparse2SortedVariable + -- * Concrete , Concrete ) where @@ -26,6 +30,13 @@ import Prelude.Kore import Control.DeepSeq ( NFData (..) ) +import Control.Lens + ( Lens' + ) +import qualified Control.Lens as Lens +import Data.Generics.Product + ( field + ) import Data.Hashable import qualified Data.Text as Text import qualified Data.Text.Prettyprint.Doc as Pretty @@ -151,11 +162,15 @@ toVariable = from @variable @Variable -} class SortedVariable variable where - -- | The known 'Sort' of the given variable. - sortedVariableSort :: variable -> Sort + lensVariableSort :: Lens' variable Sort + +-- | The known 'Sort' of the given variable. +sortedVariableSort :: SortedVariable variable => variable -> Sort +sortedVariableSort = Lens.view lensVariableSort instance SortedVariable Variable where - sortedVariableSort = variableSort + lensVariableSort = field @"variableSort" + {-# INLINE lensVariableSort #-} {- | Unparse any 'SortedVariable' in an Applicative Kore binder. @@ -200,7 +215,8 @@ instance Unparse Concrete where unparse2 = \case {} instance SortedVariable Concrete where - sortedVariableSort = \case {} + lensVariableSort _ = \case {} + {-# INLINE lensVariableSort #-} instance VariableName Concrete diff --git a/kore/src/Kore/Variables/Target.hs b/kore/src/Kore/Variables/Target.hs index 2d41ae16fb..3a7d73627f 100644 --- a/kore/src/Kore/Variables/Target.hs +++ b/kore/src/Kore/Variables/Target.hs @@ -129,8 +129,11 @@ instance SortedVariable variable => SortedVariable (Target variable) where - sortedVariableSort (Target variable) = sortedVariableSort variable - sortedVariableSort (NonTarget variable) = sortedVariableSort variable + lensVariableSort f = + \case + Target variable -> Target <$> lensVariableSort f variable + NonTarget variable -> Target <$> lensVariableSort f variable + {-# INLINE lensVariableSort #-} instance VariableName variable => VariableName (Target variable) diff --git a/kore/src/Kore/Variables/UnifiedVariable.hs b/kore/src/Kore/Variables/UnifiedVariable.hs index 816a9290f9..12d50825b3 100644 --- a/kore/src/Kore/Variables/UnifiedVariable.hs +++ b/kore/src/Kore/Variables/UnifiedVariable.hs @@ -54,6 +54,7 @@ import Kore.Syntax.ElementVariable import Kore.Syntax.SetVariable import Kore.Syntax.Variable ( SortedVariable (..) + , sortedVariableSort ) import Kore.Unparser import Kore.Variables.Fresh diff --git a/kore/test/Test/Kore/Variables/V.hs b/kore/test/Test/Kore/Variables/V.hs index 9e5a1330d0..fd3117e1c1 100644 --- a/kore/test/Test/Kore/Variables/V.hs +++ b/kore/test/Test/Kore/Variables/V.hs @@ -5,6 +5,7 @@ module Test.Kore.Variables.V import Prelude.Kore +import qualified Control.Lens as Lens import Data.Generics.Product ( field ) @@ -39,7 +40,8 @@ instance Unparse V where unparse2 = undefined instance SortedVariable V where - sortedVariableSort _ = sortVariable + lensVariableSort = Lens.lens (const sortVariable) (\v _ -> v) + {-# INLINE lensVariableSort #-} instance From Variable V where from = error "Not implemented" diff --git a/kore/test/Test/Kore/Variables/W.hs b/kore/test/Test/Kore/Variables/W.hs index a3ef1413a9..cfa408ec4f 100644 --- a/kore/test/Test/Kore/Variables/W.hs +++ b/kore/test/Test/Kore/Variables/W.hs @@ -5,6 +5,7 @@ module Test.Kore.Variables.W import Prelude.Kore +import qualified Control.Lens as Lens import Data.Generics.Product ( field ) @@ -40,7 +41,8 @@ instance Unparse W where unparse2 = undefined instance SortedVariable W where - sortedVariableSort _ = sortVariable + lensVariableSort = Lens.lens (const sortVariable) (\w _ -> w) + {-# INLINE lensVariableSort #-} instance From Variable W where from = error "Not implemented" From 4f36de6d03aa7961facf561930908a7345166c84 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Fri, 14 Feb 2020 10:40:02 -0600 Subject: [PATCH 15/21] FreshPartialOrd: Return to the original plan --- kore/src/Kore/Internal/Condition.hs | 2 +- kore/src/Kore/Internal/Conditional.hs | 3 +- kore/src/Kore/Internal/Pattern.hs | 3 +- kore/src/Kore/Internal/Predicate.hs | 2 +- kore/src/Kore/Internal/Substitution.hs | 2 +- kore/src/Kore/Internal/TermLike.hs | 2 +- kore/src/Kore/Internal/TermLike/TermLike.hs | 10 +- kore/src/Kore/Step/Axiom/Matcher.hs | 2 +- kore/src/Kore/Step/Step.hs | 5 +- kore/src/Kore/Syntax/ElementVariable.hs | 12 ++ kore/src/Kore/Syntax/SetVariable.hs | 12 ++ kore/src/Kore/Variables/Fresh.hs | 146 ++++++++------------ kore/src/Kore/Variables/Target.hs | 17 ++- kore/src/Kore/Variables/UnifiedVariable.hs | 50 ++++--- kore/test/Test/Kore/Step/RewriteStep.hs | 6 +- kore/test/Test/Kore/Step/Simplifier.hs | 2 + kore/test/Test/Kore/Variables/Fresh.hs | 96 +++++++------ kore/test/Test/Kore/Variables/V.hs | 14 +- kore/test/Test/Kore/Variables/W.hs | 14 +- 19 files changed, 215 insertions(+), 185 deletions(-) diff --git a/kore/src/Kore/Internal/Condition.hs b/kore/src/Kore/Internal/Condition.hs index 7e68f1edf0..d68cc80725 100644 --- a/kore/src/Kore/Internal/Condition.hs +++ b/kore/src/Kore/Internal/Condition.hs @@ -148,7 +148,7 @@ toPredicate toPredicate = from mapVariables - :: (Ord variable1, FreshPartialOrd variable2) + :: (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2) => (ElementVariable variable1 -> ElementVariable variable2) -> (SetVariable variable1 -> SetVariable variable2) -> Condition variable1 diff --git a/kore/src/Kore/Internal/Conditional.hs b/kore/src/Kore/Internal/Conditional.hs index 51f8a75c5b..4484abf32a 100644 --- a/kore/src/Kore/Internal/Conditional.hs +++ b/kore/src/Kore/Internal/Conditional.hs @@ -69,6 +69,7 @@ import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.TermLike ( InternalVariable , Sort + , SortedVariable , TermLike , termLikeSort ) @@ -413,7 +414,7 @@ isPredicate Conditional {term} = isTop term -} mapVariables - :: (Ord variableFrom, FreshPartialOrd variableTo) + :: (Ord variableFrom, FreshPartialOrd variableTo, SortedVariable variableTo) => ((ElementVariable variableFrom -> ElementVariable variableTo) -> (SetVariable variableFrom -> SetVariable variableTo) -> termFrom -> termTo) -> (ElementVariable variableFrom -> ElementVariable variableTo) -> (SetVariable variableFrom -> SetVariable variableTo) diff --git a/kore/src/Kore/Internal/Pattern.hs b/kore/src/Kore/Internal/Pattern.hs index 2caa9dabcb..23c73245c7 100644 --- a/kore/src/Kore/Internal/Pattern.hs +++ b/kore/src/Kore/Internal/Pattern.hs @@ -63,6 +63,7 @@ import Kore.Internal.TermLike , InternalVariable , SetVariable , Sort + , SortedVariable , TermLike , mkAnd , mkBottom @@ -123,7 +124,7 @@ freeElementVariables = in an Pattern. -} mapVariables - :: (Ord variableFrom, FreshPartialOrd variableTo) + :: (Ord variableFrom, FreshPartialOrd variableTo, SortedVariable variableTo) => (ElementVariable variableFrom -> ElementVariable variableTo) -> (SetVariable variableFrom -> SetVariable variableTo) -> Pattern variableFrom diff --git a/kore/src/Kore/Internal/Predicate.hs b/kore/src/Kore/Internal/Predicate.hs index 79b79e1900..c651d10dd3 100644 --- a/kore/src/Kore/Internal/Predicate.hs +++ b/kore/src/Kore/Internal/Predicate.hs @@ -706,7 +706,7 @@ isPredicate = Either.isRight . makePredicate {- | Replace all variables in a @Predicate@ using the provided mapping. -} mapVariables - :: (Ord from, FreshPartialOrd to) + :: (Ord from, FreshPartialOrd to, SortedVariable to) => (ElementVariable from -> ElementVariable to) -> (SetVariable from -> SetVariable to) -> Predicate from diff --git a/kore/src/Kore/Internal/Substitution.hs b/kore/src/Kore/Internal/Substitution.hs index 144ee01add..ac80046f64 100644 --- a/kore/src/Kore/Internal/Substitution.hs +++ b/kore/src/Kore/Internal/Substitution.hs @@ -351,7 +351,7 @@ modify f = wrap . f . unwrap -- with the given function. mapVariables :: forall variableFrom variableTo - . (Ord variableFrom, FreshPartialOrd variableTo) + . (Ord variableFrom, FreshPartialOrd variableTo, SortedVariable variableTo) => (ElementVariable variableFrom -> ElementVariable variableTo) -> (SetVariable variableFrom -> SetVariable variableTo) -> Substitution variableFrom diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index a5dbc56579..866c53cf45 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -392,7 +392,7 @@ composes with other tree transformations without allocating intermediates. -} fromConcrete - :: FreshPartialOrd variable + :: (FreshPartialOrd variable, SortedVariable variable) => TermLike Concrete -> TermLike variable fromConcrete = mapVariables (\case {}) (\case {}) diff --git a/kore/src/Kore/Internal/TermLike/TermLike.hs b/kore/src/Kore/Internal/TermLike/TermLike.hs index 383966e5e3..76f97c1681 100644 --- a/kore/src/Kore/Internal/TermLike/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike/TermLike.hs @@ -593,7 +593,7 @@ See also: 'traverseVariables' -} mapVariables :: forall variable1 variable2 - . (Ord variable1, FreshPartialOrd variable2) + . (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2) => (ElementVariable variable1 -> ElementVariable variable2) -> (SetVariable variable1 -> SetVariable variable2) -> TermLike variable1 @@ -669,7 +669,7 @@ See also: 'mapVariables' -} traverseVariables :: forall variable1 variable2 m - . (Ord variable1, FreshPartialOrd variable2) + . (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2) => Monad m => (ElementVariable variable1 -> m (ElementVariable variable2)) -> (SetVariable variable1 -> m (SetVariable variable2)) @@ -762,7 +762,7 @@ sequenceAdjunct gsequence = renameElementBinder :: Monad m - => (Ord variable1, FreshPartialOrd variable2) + => (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2) => (ElementVariable variable1 -> m (ElementVariable variable2)) -> Set.Set (UnifiedVariable variable2) -> Binder (ElementVariable variable1) @@ -788,7 +788,7 @@ renameElementBinder trElemVar avoiding binder = do renameSetBinder :: Monad m - => (Ord variable1, FreshPartialOrd variable2) + => (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2) => (SetVariable variable1 -> m (SetVariable variable2)) -> Set.Set (UnifiedVariable variable2) -> Binder (SetVariable variable1) @@ -898,7 +898,7 @@ externalizeFreshVariables termLike = head $ dropWhile wouldCapture $ externalize - <$> iterate Fresh.incrementVariable variable + <$> iterate Fresh.nextVariable variable where wouldCapture var = isFreeVariable (mk var) avoiding externalize = fmap Variable.externalizeFreshVariable diff --git a/kore/src/Kore/Step/Axiom/Matcher.hs b/kore/src/Kore/Step/Axiom/Matcher.hs index 1a120cc3bb..d1c8b803b0 100644 --- a/kore/src/Kore/Step/Axiom/Matcher.hs +++ b/kore/src/Kore/Step/Axiom/Matcher.hs @@ -607,7 +607,7 @@ Returns 'Nothing' if the variable name is already globally-unique. -} liftVariable - :: FreshPartialOrd variable + :: (FreshPartialOrd variable, SortedVariable variable) => MonadState (MatcherState variable) matcher => UnifiedVariable variable -> matcher (Maybe (UnifiedVariable variable)) diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index 6df4f28af3..60774c34e5 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -82,6 +82,7 @@ import Kore.Internal.TermLike ( ElementVariable , InternalVariable , SetVariable + , SortedVariable , TermLike ) import qualified Kore.Internal.TermLike as TermLike @@ -161,7 +162,7 @@ class UnifyingRule rule where distinguishing rule variables from configuration variables. -} mapRuleVariables - :: (Ord variable1, FreshPartialOrd variable2) + :: (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2) => (ElementVariable variable1 -> ElementVariable variable2) -> (SetVariable variable1 -> SetVariable variable2) -> rule variable1 @@ -274,7 +275,7 @@ targetRuleVariables sideCondition initial = {- | Unwrap the variables in a 'RulePattern'. Inverse of 'targetRuleVariables'. -} unTargetRule - :: FreshPartialOrd variable + :: (FreshPartialOrd variable, SortedVariable variable) => UnifyingRule rule => rule (Target variable) -> rule variable unTargetRule = mapRuleVariables Target.unTargetElement Target.unTargetSet diff --git a/kore/src/Kore/Syntax/ElementVariable.hs b/kore/src/Kore/Syntax/ElementVariable.hs index 8011b7c6d6..30bb4e31f5 100644 --- a/kore/src/Kore/Syntax/ElementVariable.hs +++ b/kore/src/Kore/Syntax/ElementVariable.hs @@ -13,11 +13,17 @@ import Prelude.Kore import Control.DeepSeq ( NFData (..) ) +import Data.Generics.Wrapped + ( _Unwrapped + ) import Data.Hashable import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC import Kore.Debug +import Kore.Syntax.Variable + ( SortedVariable (..) + ) import Kore.Unparser -- | Element (singleton) Kore variables @@ -40,3 +46,9 @@ instance (Debug variable, Diff variable) => Diff (ElementVariable variable) instance Unparse variable => Unparse (ElementVariable variable) where unparse = unparse . getElementVariable unparse2 = unparse2 . getElementVariable + +instance + SortedVariable variable => SortedVariable (ElementVariable variable) + where + lensVariableSort = _Unwrapped . lensVariableSort + {-# INLINE lensVariableSort #-} diff --git a/kore/src/Kore/Syntax/SetVariable.hs b/kore/src/Kore/Syntax/SetVariable.hs index 6dc7a7d26d..bb850625af 100644 --- a/kore/src/Kore/Syntax/SetVariable.hs +++ b/kore/src/Kore/Syntax/SetVariable.hs @@ -13,11 +13,17 @@ import Prelude.Kore import Control.DeepSeq ( NFData (..) ) +import Data.Generics.Wrapped + ( _Unwrapped + ) import Data.Hashable import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC import Kore.Debug +import Kore.Syntax.Variable + ( SortedVariable (..) + ) import Kore.Unparser -- | Applicative-Kore set variables @@ -40,3 +46,9 @@ instance (Debug variable, Diff variable) => Diff (SetVariable variable) instance Unparse variable => Unparse (SetVariable variable) where unparse = unparse . getSetVariable unparse2 = unparse2 . getSetVariable + +instance + SortedVariable variable => SortedVariable (SetVariable variable) + where + lensVariableSort = _Unwrapped . lensVariableSort + {-# INLINE lensVariableSort #-} diff --git a/kore/src/Kore/Variables/Fresh.hs b/kore/src/Kore/Variables/Fresh.hs index 5dac751183..647c2e789e 100644 --- a/kore/src/Kore/Variables/Fresh.hs +++ b/kore/src/Kore/Variables/Fresh.hs @@ -5,7 +5,6 @@ License : UIUC/NCSA module Kore.Variables.Fresh ( FreshPartialOrd (..) , FreshVariable (..) - , incrementVariable , refreshVariables -- * Re-exports , module Kore.Syntax.Variable @@ -14,13 +13,14 @@ module Kore.Variables.Fresh import Prelude.Kore import qualified Control.Lens as Lens +import qualified Control.Monad as Monad import qualified Data.Foldable as Foldable -import Data.Function - ( on - ) import Data.Generics.Product ( field ) +import Data.Generics.Wrapped + ( _Unwrapped + ) import Data.Map.Strict ( Map ) @@ -38,48 +38,42 @@ import Kore.Syntax.Variable {- | @FreshPartialOrder@ defines a partial order for renaming variables. -Two variables are related under this partial order when @compareFresh@ returns -@'Just' _@. +Two variables @x@ and @y@ are related under the partial order if @infVariable@ +and @supVariable@ give the same value on @x@ and @y@. -Agreement: +Disjoint: -prop> maybe True (== compare a b) (compareFresh a b) +prop> infVariable x /= supVariable y -Relevance: +prop> (infVariable x == infVariable y) == (supVariable x == supVariable y) -prop> compareFresh a (supVariable a) \/= Nothing +Order: -prop> isJust (nextVariable x a) ==> isJust (compareFresh a (nextVariable x a)) +prop> infVariable x <= x -prop> isJust (nextVariable x a) ==> isJust (compareFresh x (nextVariable x a)) +prop> x <= supVariable x -Idempotence: +prop> infVariable x < supVariable x -prop> supVariable a == supVariable (supVariable a) +Idempotence: -Dominance: +prop> infVariable x == infVariable (infVariable x) -prop> a \/= supVariable a ==> compareFresh a (supVariable a) == Just LT +prop> supVariable x == supVariable (supVariable x) Monotonicity: -prop> isJust (nextVariable x a) ==> compareFresh a (nextVariable x a) == Just LT +prop> x < supVariable x ==> x < nextVariable x + +Bounding: -prop> isJust (nextVariable x a) ==> compareFresh x (nextVariable x a) == Just LT +prop> x < supVariable x ==> infVariable x < nextVariable x -Note: The monotonicity property of 'nextVariable' implies the relevance -property. +prop> x < supVariable x ==> nextVariable x < supVariable x -} class Ord variable => FreshPartialOrd variable where - {- | @compareFresh@ defines a partial order on variables. - - In the typical implementation of fresh name generation, the variable name - consists of a string (the base name) and a counter. Then, all variables with - the same base name are related, and their ordering is given by the counter. - - -} - compareFresh :: variable -> variable -> Maybe Ordering + infVariable :: variable -> variable {- | @supVariable x@ is the greatest variable related to @x@. @@ -90,63 +84,31 @@ class Ord variable => FreshPartialOrd variable where -} supVariable :: variable -> variable - {- | @nextVariable@ generates a fresh variable greater than a given bound. - - The resulting variable, if defined, is /related/ to the /original variable/. - @nextVariable@ returns @'Nothing'@ unless: - - * the /lower bound/ is related to the /original variable/, and - * the /original variable/ is not greater than the /lower bound/. - - When @nextVariable@ returns a value (@'Just' _@), then the result is - strictly greater than both arguments. - + {- | @nextVariable@ increments the counter attached to a variable. -} - nextVariable - :: variable -- ^ lower bound - -> variable -- ^ original variable - -> Maybe variable - -incrementVariable :: FreshPartialOrd variable => variable -> variable -incrementVariable original = - case nextVariable original original of - Just incremented -> incremented - Nothing -> - -- This is impossible for any law-abiding instance of - -- FreshPartialOrd. - undefined + nextVariable :: variable -> variable instance FreshPartialOrd Variable where - compareFresh x y - | variableName x == variableName y = Just $ compare x y - | otherwise = Nothing - {-# INLINE compareFresh #-} + infVariable variable = variable { variableCounter = Nothing } + {-# INLINE infVariable #-} supVariable variable = variable { variableCounter = Just Sup } {-# INLINE supVariable #-} - nextVariable bound original = do - ordering <- compareFresh bound original - case ordering of { LT -> empty; _ -> pure () } - incrementCounter . resetIdLocation $ original + nextVariable = + Lens.over (field @"variableCounter") incrementCounter + . Lens.set (field @"variableName" . field @"idLocation") generated where - resetIdLocation = - Lens.set - (field @"variableName" . field @"idLocation") - AstLocationGeneratedVariable - incrementCounter = - field @"variableCounter" $ \_ -> - case variableCounter bound of - Nothing -> pure $ Just (Element 0) - Just (Element a) -> pure $ Just (Element (succ a)) - Just Sup -> - -- Never rename (supVariable _) because it does not - -- occur in any pattern. - empty + generated = AstLocationGeneratedVariable + incrementCounter counter = + case counter of + Nothing -> Just (Element 0) + Just (Element n) -> Just (Element (succ n)) + Just Sup -> illegalVariableCounter {-# INLINE nextVariable #-} instance FreshPartialOrd Concrete where - compareFresh = \case {} + infVariable = \case {} supVariable = \case {} nextVariable = \case {} @@ -154,28 +116,26 @@ instance FreshPartialOrd variable => FreshPartialOrd (ElementVariable variable) where - compareFresh = on compareFresh getElementVariable - {-# INLINE compareFresh #-} + infVariable = Lens.over _Unwrapped infVariable + {-# INLINE infVariable #-} - supVariable = ElementVariable . supVariable . getElementVariable + supVariable = Lens.over _Unwrapped supVariable {-# INLINE supVariable #-} - nextVariable (ElementVariable bound) (ElementVariable original) = - ElementVariable <$> nextVariable bound original + nextVariable = Lens.over _Unwrapped nextVariable {-# INLINE nextVariable #-} instance FreshPartialOrd variable => FreshPartialOrd (SetVariable variable) where - compareFresh = on compareFresh getSetVariable - {-# INLINE compareFresh #-} + infVariable = Lens.over _Unwrapped infVariable + {-# INLINE infVariable #-} - supVariable = SetVariable . supVariable . getSetVariable + supVariable = Lens.over _Unwrapped supVariable {-# INLINE supVariable #-} - nextVariable (SetVariable bound) (SetVariable original) = - SetVariable <$> nextVariable bound original + nextVariable = Lens.over _Unwrapped nextVariable {-# INLINE nextVariable #-} {- | A @FreshVariable@ can be renamed to avoid colliding with a set of names. @@ -194,18 +154,26 @@ class Ord variable => FreshVariable variable where -> variable -- ^ variable to rename -> Maybe variable default refreshVariable - :: FreshPartialOrd variable + :: (FreshPartialOrd variable, SortedVariable variable) => Set variable -> variable -> Maybe variable refreshVariable avoiding original = do - largest <- Set.lookupLT (supVariable original) avoiding - nextVariable largest original + largest <- assignSort <$> Set.lookupLT (supVariable original) avoiding + Monad.guard (largest >= infVariable original) + pure (nextVariable largest) + where + originalSort = Lens.view lensVariableSort original + assignSort = Lens.set lensVariableSort originalSort {-# INLINE refreshVariable #-} -instance FreshPartialOrd variable => FreshVariable (ElementVariable variable) +instance + (FreshPartialOrd variable, SortedVariable variable) + => FreshVariable (ElementVariable variable) -instance FreshPartialOrd variable => FreshVariable (SetVariable variable) +instance + (FreshPartialOrd variable, SortedVariable variable) + => FreshVariable (SetVariable variable) instance FreshVariable Variable diff --git a/kore/src/Kore/Variables/Target.hs b/kore/src/Kore/Variables/Target.hs index 3a7d73627f..fb3b81d19e 100644 --- a/kore/src/Kore/Variables/Target.hs +++ b/kore/src/Kore/Variables/Target.hs @@ -146,13 +146,22 @@ instance From variable1 variable2 => From (Target variable1) variable2 where {-# INLINE from #-} instance FreshPartialOrd variable => FreshPartialOrd (Target variable) where - compareFresh = on compareFresh unTarget - {-# INLINE compareFresh #-} + infVariable = + \case + Target var -> Target (infVariable var) + NonTarget var -> NonTarget (infVariable var) + {-# INLINE infVariable #-} - supVariable = fmap supVariable + supVariable = + \case + Target var -> Target (supVariable var) + NonTarget var -> NonTarget (supVariable var) {-# INLINE supVariable #-} - nextVariable (unTarget -> bound) = traverse (nextVariable bound) + nextVariable = + \case + Target var -> Target (nextVariable var) + NonTarget var -> NonTarget (nextVariable var) {-# INLINE nextVariable #-} {- | Ensures that fresh variables are unique under 'unwrapStepperVariable'. diff --git a/kore/src/Kore/Variables/UnifiedVariable.hs b/kore/src/Kore/Variables/UnifiedVariable.hs index 12d50825b3..32b1f69451 100644 --- a/kore/src/Kore/Variables/UnifiedVariable.hs +++ b/kore/src/Kore/Variables/UnifiedVariable.hs @@ -83,28 +83,40 @@ instance Unparse variable => Unparse (UnifiedVariable variable) where unparse = foldMapVariable unparse unparse2 = foldMapVariable unparse2 +instance + SortedVariable variable + => SortedVariable (UnifiedVariable variable) + where + lensVariableSort f = + \case + ElemVar elemVar -> ElemVar <$> lensVariableSort f elemVar + SetVar setVar -> SetVar <$> lensVariableSort f setVar + {-# INLINE lensVariableSort #-} + instance FreshPartialOrd variable => FreshPartialOrd (UnifiedVariable variable) where - compareFresh (ElemVar elemVar1) (ElemVar elemVar2) = - compareFresh elemVar1 elemVar2 - compareFresh (SetVar elemVar1) (SetVar elemVar2) = - compareFresh elemVar1 elemVar2 - compareFresh _ _ = Nothing - - supVariable (ElemVar elemVar) = ElemVar (supVariable elemVar) - supVariable (SetVar setVar) = SetVar (supVariable setVar) - - nextVariable (ElemVar bound) (ElemVar original) = - ElemVar <$> nextVariable bound original - nextVariable (SetVar bound) (SetVar original) = - SetVar <$> nextVariable bound original - nextVariable _ _ = - -- There is never a need to rename a SetVariable to avoid an - -- ElementVariable, and vice versa. - empty - -instance FreshPartialOrd variable => FreshVariable (UnifiedVariable variable) + infVariable = + \case + ElemVar elemVar -> ElemVar (infVariable elemVar) + SetVar setVar -> SetVar (infVariable setVar) + {-# INLINE infVariable #-} + + supVariable = + \case + ElemVar elemVar -> ElemVar (supVariable elemVar) + SetVar setVar -> SetVar (supVariable setVar) + {-# INLINE supVariable #-} + + nextVariable = + \case + ElemVar elemVar -> ElemVar (nextVariable elemVar) + SetVar setVar -> SetVar (nextVariable setVar) + {-# INLINE nextVariable #-} + +instance + (FreshPartialOrd variable, SortedVariable variable) + => FreshVariable (UnifiedVariable variable) isElemVar :: UnifiedVariable variable -> Bool isElemVar (ElemVar _) = True diff --git a/kore/test/Test/Kore/Step/RewriteStep.hs b/kore/test/Test/Kore/Step/RewriteStep.hs index 0057d47e37..fa4d6317b8 100644 --- a/kore/test/Test/Kore/Step/RewriteStep.hs +++ b/kore/test/Test/Kore/Step/RewriteStep.hs @@ -82,7 +82,7 @@ import Kore.Unification.UnifierT , runUnifierT ) import Kore.Variables.Fresh - ( incrementVariable + ( nextVariable ) import Kore.Variables.Target ( Target @@ -351,7 +351,7 @@ test_applyRewriteRule_ = , testCase "quantified rhs: non-clashing" $ do let expect = Right [ OrPattern.fromPatterns [Pattern.fromTermLike final] ] - x'' = incrementVariable . incrementVariable $ Mock.x + x'' = nextVariable . nextVariable $ Mock.x final = mkElemVar x'' initial = pure (mkElemVar Mock.y) axiom = @@ -466,7 +466,7 @@ test_applyRewriteRule_ = -- vs -- sigma(a, i(b)) with substitution b=a , testCase "non-function substitution error" $ do - let x' = incrementVariable Mock.x + let x' = nextVariable Mock.x expect = Left $ UnificationError $ unsupportedPatterns "Unknown unification case." (mkElemVar x') diff --git a/kore/test/Test/Kore/Step/Simplifier.hs b/kore/test/Test/Kore/Step/Simplifier.hs index f559ff2cbf..794de3510b 100644 --- a/kore/test/Test/Kore/Step/Simplifier.hs +++ b/kore/test/Test/Kore/Step/Simplifier.hs @@ -76,6 +76,7 @@ convertTermLikeVariables :: ( VariableName variable , VariableName variable0 , FreshPartialOrd variable0 + , SortedVariable variable0 ) => TermLike variable -> TermLike variable0 @@ -88,6 +89,7 @@ convertPatternVariables :: ( VariableName variable , VariableName variable0 , FreshPartialOrd variable0 + , SortedVariable variable0 ) => Pattern variable -> Pattern variable0 diff --git a/kore/test/Test/Kore/Variables/Fresh.hs b/kore/test/Test/Kore/Variables/Fresh.hs index 695d08b19b..0b1b513041 100644 --- a/kore/test/Test/Kore/Variables/Fresh.hs +++ b/kore/test/Test/Kore/Variables/Fresh.hs @@ -18,7 +18,7 @@ import Test.Tasty.Hedgehog import Test.Tasty.HUnit import Control.Monad - ( when + ( unless ) import Data.Maybe ( fromJust @@ -340,44 +340,46 @@ testFreshPartialOrd => Gen (Pair variable) -> [TestTree] testFreshPartialOrd gen = - [ testProperty "compareFresh agrees with compare" $ property $ do - Pair x y <- forAll gen - compareFresh x y === Just (compare x y) - compareFresh y x === Just (compare y x) - , testProperty "supVariable is relevant" $ property $ do + [ testProperty "exclusive bounds" $ property $ do + xy <- forAll gen + let Pair infX infY = infVariable <$> xy + Pair supX supY = supVariable <$> xy + annotateShow infX + annotateShow supX + annotateShow infY + annotateShow supY + (infX == infY) === (supX == supY) + infX /== supY + infY /== supX + , testProperty "lower and upper bound" $ property $ do Pair x _ <- forAll gen - compareFresh x (supVariable x) /== Nothing - , testProperty "supVariable is idempotent" $ property $ do + let inf = infVariable x + sup = supVariable x + annotateShow inf + annotateShow sup + Hedgehog.assert (inf <= x) + Hedgehog.assert (x <= sup) + Hedgehog.assert (inf < sup) + , testProperty "idempotence" $ property $ do Pair x _ <- forAll gen - let xSup = supVariable x - xSupSup = supVariable xSup - xSup === xSupSup - , testProperty "supVariable dominates other variables" $ property $ do + let inf1 = infVariable x + inf2 = infVariable inf1 + sup1 = supVariable x + sup2 = supVariable sup1 + inf1 === inf2 + sup1 === sup2 + , testProperty "nextVariable" $ property $ do Pair x _ <- forAll gen - let sup = supVariable x - when (x == sup) discard - compareFresh x sup === Just LT - , testProperty "nextVariable is relevant" $ property $ do - Pair x y <- forAll gen - when (x == supVariable x) discard - when (y == supVariable y) discard - case nextVariable y x of - Nothing -> - compareFresh y x === Just LT - Just x' -> do - annotateShow x' - compareFresh x x' /== Nothing - , testProperty "nextVariable is monotonic" $ property $ do - Pair x y <- forAll gen - when (x == supVariable x) discard - when (y == supVariable y) discard - case nextVariable y x of - Nothing -> - compareFresh y x === Just LT - Just x' -> do - annotateShow x' - compareFresh x x' === Just LT - compareFresh y x' === Just LT + let inf = infVariable x + sup = supVariable x + next = nextVariable x + unless (x < sup) discard + annotateShow inf + annotateShow sup + annotateShow next + Hedgehog.assert (inf < next) + Hedgehog.assert (x < next) + Hedgehog.assert (next < sup) ] test_FreshPartialOrd_Variable :: TestTree @@ -402,10 +404,24 @@ test_FreshPartialOrd_UnifiedVariable = relatedVariableGen :: Gen (Pair Variable) relatedVariableGen = do - name <- idGen - Pair - <$> (Variable name <$> counterGen <*> sortGen) - <*> (Variable name <$> counterGen <*> sortGen) + Pair name1 name2 <- + Gen.choice + [ do { name <- idGen; return (Pair name name) } + , Pair <$> idGen <*> idGen + ] + Pair counter1 counter2 <- + Gen.choice + [ do { counter <- counterGen; return (Pair counter counter) } + , Pair <$> counterGen <*> counterGen + ] + Pair sort1 sort2 <- + Gen.choice + [ do { sort <- sortGen; return (Pair sort sort) } + , Pair <$> sortGen <*> sortGen + ] + let variable1 = Variable name1 counter1 sort1 + variable2 = Variable name2 counter2 sort2 + return (Pair variable1 variable2) counterGen :: MonadGen gen => gen (Maybe (Sup Natural)) counterGen = diff --git a/kore/test/Test/Kore/Variables/V.hs b/kore/test/Test/Kore/Variables/V.hs index fd3117e1c1..8e9df64ce2 100644 --- a/kore/test/Test/Kore/Variables/V.hs +++ b/kore/test/Test/Kore/Variables/V.hs @@ -52,18 +52,16 @@ instance From V Variable where instance VariableName V instance FreshPartialOrd V where - compareFresh (V a an) (V b bn) - | a == b = Just (compare an bn) - | otherwise = Nothing + infVariable v = v { counter = Nothing } supVariable v = v { counter = Just Sup } - nextVariable V { counter = bound } = - field @"counter" (increment . max bound) + nextVariable = + Lens.over (field @"counter") increment where increment = \case - Nothing -> pure $ Just (Element 0) - Just (Element a) -> pure $ Just (Element (succ a)) - Just Sup -> empty + Nothing -> Just (Element 0) + Just (Element a) -> Just (Element (succ a)) + Just Sup -> illegalVariableCounter instance FreshVariable V diff --git a/kore/test/Test/Kore/Variables/W.hs b/kore/test/Test/Kore/Variables/W.hs index cfa408ec4f..7b857aa955 100644 --- a/kore/test/Test/Kore/Variables/W.hs +++ b/kore/test/Test/Kore/Variables/W.hs @@ -53,18 +53,16 @@ instance From W Variable where instance VariableName W instance FreshPartialOrd W where - compareFresh (W a an) (W b bn) - | a == b = Just (compare an bn) - | otherwise = Nothing + infVariable w = w { counter = Nothing } supVariable w = w { counter = Just Sup } - nextVariable W { counter = bound } = - field @"counter" (increment . max bound) + nextVariable = + Lens.over (field @"counter") increment where increment = \case - Nothing -> pure $ Just (Element 0) - Just (Element a) -> pure $ Just (Element (succ a)) - Just Sup -> empty + Nothing -> Just (Element 0) + Just (Element a) -> Just (Element (succ a)) + Just Sup -> illegalVariableCounter instance FreshVariable W From 038269e47f902c54705526148b5505e6d27fcad7 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Fri, 14 Feb 2020 10:42:42 -0600 Subject: [PATCH 16/21] Target: Use FreshPartialOrd for FreshVariable --- kore/src/Kore/Variables/Target.hs | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/kore/src/Kore/Variables/Target.hs b/kore/src/Kore/Variables/Target.hs index fb3b81d19e..1d57383f60 100644 --- a/kore/src/Kore/Variables/Target.hs +++ b/kore/src/Kore/Variables/Target.hs @@ -24,7 +24,6 @@ import Prelude.Kore import Data.Hashable ( Hashable (hashWithSalt) ) -import qualified Data.Set as Set import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC @@ -166,13 +165,9 @@ instance FreshPartialOrd variable => FreshPartialOrd (Target variable) where {- | Ensures that fresh variables are unique under 'unwrapStepperVariable'. -} -instance FreshVariable variable => FreshVariable (Target variable) where - refreshVariable (Set.map unTarget -> avoiding) = - \case - Target variable -> - Target <$> refreshVariable avoiding variable - NonTarget variable -> - NonTarget <$> refreshVariable avoiding variable +instance + (FreshPartialOrd variable, SortedVariable variable) + => FreshVariable (Target variable) instance Unparse variable => From e7057edf5528bf87df8b651e10bc1aaf0ed1de86 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Fri, 14 Feb 2020 10:43:07 -0600 Subject: [PATCH 17/21] Target: Fix documentation --- kore/src/Kore/Variables/Target.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kore/src/Kore/Variables/Target.hs b/kore/src/Kore/Variables/Target.hs index 1d57383f60..ee75a708c8 100644 --- a/kore/src/Kore/Variables/Target.hs +++ b/kore/src/Kore/Variables/Target.hs @@ -46,9 +46,9 @@ import Kore.Variables.UnifiedVariable {- | Distinguish variables by their source. -'Target' variables always compare 'LT' 'NonTarget' variables, so that the -unification procedure prefers to generate substitutions for 'Target' variables -instead of 'NonTarget' variables. +'Target' variables always compare 'LT' 'NonTarget' variables under +'SubstitutionOrd', so that the unification procedure prefers to generate +substitutions for 'Target' variables instead of 'NonTarget' variables. -} data Target variable From 0489cc35ac80c0eb6eba882093a78356e116eae2 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Fri, 14 Feb 2020 13:29:04 -0600 Subject: [PATCH 18/21] Target: Cleaner Eq and Ord instances --- kore/src/Kore/Variables/Target.hs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/kore/src/Kore/Variables/Target.hs b/kore/src/Kore/Variables/Target.hs index ee75a708c8..b07209d997 100644 --- a/kore/src/Kore/Variables/Target.hs +++ b/kore/src/Kore/Variables/Target.hs @@ -58,11 +58,11 @@ data Target variable deriving (Functor, Foldable, Traversable) instance Eq variable => Eq (Target variable) where - (==) = on (==) unTarget + (==) a b = unTarget a == unTarget b {-# INLINE (==) #-} instance Ord variable => Ord (Target variable) where - compare = on compare unTarget + compare a b = compare (unTarget a) (unTarget b) {-# INLINE compare #-} instance Hashable variable => Hashable (Target variable) where @@ -90,6 +90,7 @@ instance unTarget :: Target variable -> variable unTarget (Target variable) = variable unTarget (NonTarget variable) = variable +{-# INLINE unTarget #-} unTargetElement :: ElementVariable (Target variable) -> ElementVariable variable unTargetElement = fmap unTarget From 3f8474327a56c0820c87b70a6ee98509664dd2c8 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Fri, 14 Feb 2020 13:29:28 -0600 Subject: [PATCH 19/21] INLINE for variable renaming --- kore/src/Kore/Internal/TermLike/Renaming.hs | 1 + kore/src/Kore/Variables/UnifiedVariable.hs | 6 ++++++ 2 files changed, 7 insertions(+) diff --git a/kore/src/Kore/Internal/TermLike/Renaming.hs b/kore/src/Kore/Internal/TermLike/Renaming.hs index 73b2b73691..a78a84862b 100644 --- a/kore/src/Kore/Internal/TermLike/Renaming.hs +++ b/kore/src/Kore/Internal/TermLike/Renaming.hs @@ -56,6 +56,7 @@ renameFreeVariables trElemVar trSetVar = renameSetVariable setVar <$> trSetVar setVar <*> pure renaming +{-# INLINE renameFreeVariables #-} askUnifiedVariable :: Monad m diff --git a/kore/src/Kore/Variables/UnifiedVariable.hs b/kore/src/Kore/Variables/UnifiedVariable.hs index 32b1f69451..53b5621885 100644 --- a/kore/src/Kore/Variables/UnifiedVariable.hs +++ b/kore/src/Kore/Variables/UnifiedVariable.hs @@ -241,9 +241,11 @@ instance { setVariables = on (<>) setVariables a b , elementVariables = on (<>) elementVariables a b } + {-# INLINE (<>) #-} instance Ord variable1 => Monoid (UnifiedVariableMap variable1 variable2) where mempty = UnifiedVariableMap mempty mempty + {-# INLINE mempty #-} renameSetVariable :: Ord variable1 @@ -255,6 +257,7 @@ renameSetVariable variable1 variable2 = Lens.over (field @"setVariables") (Map.insert variable1 variable2) +{-# INLINE renameSetVariable #-} renameElementVariable :: Ord variable1 @@ -266,6 +269,7 @@ renameElementVariable variable1 variable2 = Lens.over (field @"elementVariables") (Map.insert variable1 variable2) +{-# INLINE renameElementVariable #-} lookupRenamedElementVariable :: Ord variable1 @@ -274,6 +278,7 @@ lookupRenamedElementVariable -> Maybe (ElementVariable variable2) lookupRenamedElementVariable variable = Map.lookup variable . elementVariables +{-# INLINE lookupRenamedElementVariable #-} lookupRenamedSetVariable :: Ord variable1 @@ -282,3 +287,4 @@ lookupRenamedSetVariable -> Maybe (SetVariable variable2) lookupRenamedSetVariable variable = Map.lookup variable . setVariables +{-# INLINE lookupRenamedSetVariable #-} From 002255d0247aed1361e2d5526d326bedc40fa1c8 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Sun, 16 Feb 2020 20:59:03 -0600 Subject: [PATCH 20/21] hlint suggestions --- kore/test/Test/Kore/Variables/V.hs | 2 +- kore/test/Test/Kore/Variables/W.hs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kore/test/Test/Kore/Variables/V.hs b/kore/test/Test/Kore/Variables/V.hs index 8e9df64ce2..a226216e02 100644 --- a/kore/test/Test/Kore/Variables/V.hs +++ b/kore/test/Test/Kore/Variables/V.hs @@ -40,7 +40,7 @@ instance Unparse V where unparse2 = undefined instance SortedVariable V where - lensVariableSort = Lens.lens (const sortVariable) (\v _ -> v) + lensVariableSort = Lens.lens (const sortVariable) const {-# INLINE lensVariableSort #-} instance From Variable V where diff --git a/kore/test/Test/Kore/Variables/W.hs b/kore/test/Test/Kore/Variables/W.hs index 7b857aa955..d587109cf2 100644 --- a/kore/test/Test/Kore/Variables/W.hs +++ b/kore/test/Test/Kore/Variables/W.hs @@ -41,7 +41,7 @@ instance Unparse W where unparse2 = undefined instance SortedVariable W where - lensVariableSort = Lens.lens (const sortVariable) (\w _ -> w) + lensVariableSort = Lens.lens (const sortVariable) const {-# INLINE lensVariableSort #-} instance From Variable W where From 69390f1083d6b3d7b7ad2c9d75547a9809066cc3 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 18 Feb 2020 11:08:04 -0600 Subject: [PATCH 21/21] MapVariables type synonym --- kore/src/Kore/Internal/Conditional.hs | 15 +++++++-------- kore/src/Kore/Variables/UnifiedVariable.hs | 12 +++++++++--- 2 files changed, 16 insertions(+), 11 deletions(-) diff --git a/kore/src/Kore/Internal/Conditional.hs b/kore/src/Kore/Internal/Conditional.hs index 4484abf32a..e47f4cb48d 100644 --- a/kore/src/Kore/Internal/Conditional.hs +++ b/kore/src/Kore/Internal/Conditional.hs @@ -82,8 +82,7 @@ import Kore.Variables.Fresh ( FreshPartialOrd ) import Kore.Variables.UnifiedVariable - ( ElementVariable - , SetVariable + ( MapVariables , UnifiedVariable ) import qualified SQL @@ -414,12 +413,12 @@ isPredicate Conditional {term} = isTop term -} mapVariables - :: (Ord variableFrom, FreshPartialOrd variableTo, SortedVariable variableTo) - => ((ElementVariable variableFrom -> ElementVariable variableTo) -> (SetVariable variableFrom -> SetVariable variableTo) -> termFrom -> termTo) - -> (ElementVariable variableFrom -> ElementVariable variableTo) - -> (SetVariable variableFrom -> SetVariable variableTo) - -> Conditional variableFrom termFrom - -> Conditional variableTo termTo + :: Ord variableFrom + => (FreshPartialOrd variableTo, SortedVariable variableTo) + => MapVariables variableFrom variableTo termFrom termTo + -> MapVariables variableFrom variableTo + (Conditional variableFrom termFrom) + (Conditional variableTo termTo) mapVariables mapTermVariables mapElemVar diff --git a/kore/src/Kore/Variables/UnifiedVariable.hs b/kore/src/Kore/Variables/UnifiedVariable.hs index 53b5621885..7b77c0ecdd 100644 --- a/kore/src/Kore/Variables/UnifiedVariable.hs +++ b/kore/src/Kore/Variables/UnifiedVariable.hs @@ -15,6 +15,7 @@ module Kore.Variables.UnifiedVariable , unifiedVariableSort , refreshElementVariable , refreshSetVariable + , MapVariables , mapUnifiedVariable , traverseUnifiedVariable -- * UnifiedVariableMap @@ -202,10 +203,15 @@ refreshSetVariable avoiding = -- UnifiedVariable (above) conserves the SetVar constructor. fmap expectSetVar . refreshVariable avoiding . SetVar +type MapVariables variable1 variable2 term1 term2 = + (ElementVariable variable1 -> ElementVariable variable2) + -> (SetVariable variable1 -> SetVariable variable2) + -> term1 -> term2 + mapUnifiedVariable - :: (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) - -> UnifiedVariable variable1 -> UnifiedVariable variable2 + :: MapVariables variable1 variable2 + (UnifiedVariable variable1) + (UnifiedVariable variable2) mapUnifiedVariable mapElemVar mapSetVar = \case ElemVar elemVar -> ElemVar (mapElemVar elemVar)