From ae7098e83f1c158e40fdc1e5ec5ba5dd74f6055e Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 11 Feb 2020 13:41:54 -0600 Subject: [PATCH 1/6] class VariableName --- kore/src/Kore/Internal/Variable.hs | 2 +- .../Kore/Step/Simplification/ExpandAlias.hs | 2 +- kore/src/Kore/Syntax/Variable.hs | 63 ++++++++++++------- kore/src/Kore/Variables/Target.hs | 13 +++- .../Kore/ASTVerifier/DefinitionVerifier.hs | 1 + kore/test/Test/Kore/Internal/Pattern.hs | 20 ++++-- .../Test/Kore/Step/Function/Integration.hs | 2 +- kore/test/Test/Kore/Step/Simplifier.hs | 13 ++-- kore/test/Test/Kore/Unification/Unifier.hs | 20 ++++-- 9 files changed, 92 insertions(+), 44 deletions(-) diff --git a/kore/src/Kore/Internal/Variable.hs b/kore/src/Kore/Internal/Variable.hs index e16b08a706..79bc39390b 100644 --- a/kore/src/Kore/Internal/Variable.hs +++ b/kore/src/Kore/Internal/Variable.hs @@ -81,5 +81,5 @@ these constraints. type InternalVariable variable = ( Ord variable, SubstitutionOrd variable , Debug variable, Show variable, Unparse variable - , SortedVariable variable, FreshVariable variable + , VariableName variable, SortedVariable variable, FreshVariable variable ) diff --git a/kore/src/Kore/Step/Simplification/ExpandAlias.hs b/kore/src/Kore/Step/Simplification/ExpandAlias.hs index 719eff65bf..37a1229901 100644 --- a/kore/src/Kore/Step/Simplification/ExpandAlias.hs +++ b/kore/src/Kore/Step/Simplification/ExpandAlias.hs @@ -33,7 +33,7 @@ import Kore.Internal.TermLike , substitute ) import Kore.Syntax.Variable - ( SortedVariable (..) + ( fromVariable ) import Kore.Unification.Unify ( MonadUnify diff --git a/kore/src/Kore/Syntax/Variable.hs b/kore/src/Kore/Syntax/Variable.hs index a0b4960812..d5ff59fa61 100644 --- a/kore/src/Kore/Syntax/Variable.hs +++ b/kore/src/Kore/Syntax/Variable.hs @@ -13,6 +13,9 @@ module Kore.Syntax.Variable , isOriginalVariable , illegalVariableCounter , externalizeFreshVariable + , VariableName + , toVariable + , fromVariable , SortedVariable (..) , unparse2SortedVariable , Concrete @@ -78,6 +81,12 @@ instance Unparse Variable where unparse2 variableName <> Pretty.pretty variableCounter +instance From Variable Variable where + from = id + {-# INLINE from #-} + +instance VariableName Variable + {- | Is the variable original (as opposed to generated)? -} isOriginalVariable :: Variable -> Bool @@ -112,37 +121,41 @@ externalizeFreshVariable variable@Variable { variableName, variableCounter } = , idLocation = AstLocationGeneratedVariable } -{- | 'SortedVariable' is a Kore variable with a known sort. +{- | 'VariableName' is the name of a Kore variable. + +A 'VariableName' has instances: + +* @'From' variable 'Variable'@ +* @'From' 'Variable' variable@ + +such that both implementations of 'from' are injective, + +prop> (==) (fromVariable x) (fromVariable y) === (==) x y -The instances of @SortedVariable@ must encompass the 'Variable' type by -implementing 'fromVariable', i.e. we must be able to construct a -@SortedVariable@ given a parsed 'Variable'. +prop> (==) x y === (==) (toVariable x) (toVariable y) -'toVariable' may delete information so that + -} +class + (Ord variable, From variable Variable, From Variable variable) + => VariableName variable + +-- | An injection from 'Variable' to any 'VariableName'. +fromVariable :: forall variable. VariableName variable => Variable -> variable +fromVariable = from @Variable @variable -> toVariable . fromVariable === id :: Variable -> Variable +-- | An injection from any 'VariableName' to 'Variable'. +toVariable :: forall variable. VariableName variable => variable -> Variable +toVariable = from @variable @Variable -but the reverse is not required. +{- | 'SortedVariable' is a Kore variable with a known sort. -} class SortedVariable variable where -- | The known 'Sort' of the given variable. sortedVariableSort :: variable -> Sort - sortedVariableSort variable = - variableSort - where - Variable { variableSort } = toVariable variable - - -- | Convert a variable from the parsed syntax of Kore. - fromVariable :: Variable -> variable - -- | Extract the parsed syntax of a Kore variable. - toVariable :: variable -> Variable --- TODO(traiansf): the 'SortedVariable' class mixes different concerns. instance SortedVariable Variable where sortedVariableSort = variableSort - fromVariable = id - toVariable = id {- | Unparse any 'SortedVariable' in an Applicative Kore binder. @@ -188,5 +201,13 @@ instance Unparse Concrete where instance SortedVariable Concrete where sortedVariableSort = \case {} - toVariable = \case {} - fromVariable = error "Cannot construct a variable in a concrete term!" + +instance VariableName Concrete + +instance From Variable Concrete where + from = error "Cannot construct a variable in a concrete term!" + {-# INLINE from #-} + +instance From Concrete Variable where + from = \case {} + {-# INLINE from #-} diff --git a/kore/src/Kore/Variables/Target.hs b/kore/src/Kore/Variables/Target.hs index d9080dd71e..9d902c2db6 100644 --- a/kore/src/Kore/Variables/Target.hs +++ b/kore/src/Kore/Variables/Target.hs @@ -129,9 +129,16 @@ instance where sortedVariableSort (Target variable) = sortedVariableSort variable sortedVariableSort (NonTarget variable) = sortedVariableSort variable - fromVariable = Target . fromVariable - toVariable (Target var) = toVariable var - toVariable (NonTarget var) = toVariable var + +instance VariableName variable => VariableName (Target variable) + +instance From variable1 variable2 => From variable1 (Target variable2) where + from = Target . from @variable1 @variable2 + {-# INLINE from #-} + +instance From variable1 variable2 => From (Target variable1) variable2 where + from = from @variable1 @variable2 . unTarget + {-# INLINE from #-} {- | Ensures that fresh variables are unique under 'unwrapStepperVariable'. -} diff --git a/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier.hs b/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier.hs index 49bf46329d..48ad9804f8 100644 --- a/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier.hs +++ b/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier.hs @@ -85,6 +85,7 @@ import qualified Kore.Internal.TermLike as Internal import Kore.Sort import Kore.Syntax hiding ( PatternF (..) + , VariableName ) import Kore.Syntax.Definition import qualified Kore.Syntax.PatternF as Syntax diff --git a/kore/test/Test/Kore/Internal/Pattern.hs b/kore/test/Test/Kore/Internal/Pattern.hs index 6253e83976..e83dad7a13 100644 --- a/kore/test/Test/Kore/Internal/Pattern.hs +++ b/kore/test/Test/Kore/Internal/Pattern.hs @@ -155,8 +155,14 @@ instance Unparse V where instance SortedVariable V where sortedVariableSort _ = sortVariable - fromVariable = undefined - toVariable = undefined + +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) @@ -186,8 +192,14 @@ instance Unparse W where instance SortedVariable W where sortedVariableSort _ = sortVariable - fromVariable = undefined - toVariable = undefined + +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) diff --git a/kore/test/Test/Kore/Step/Function/Integration.hs b/kore/test/Test/Kore/Step/Function/Integration.hs index f38d016008..020e35ae55 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, SortedVariable variable) + . (FreshVariable variable, VariableName variable) => Pattern Variable -> Pattern variable mapVariables = diff --git a/kore/test/Test/Kore/Step/Simplifier.hs b/kore/test/Test/Kore/Step/Simplifier.hs index 4d4255d176..482c56960a 100644 --- a/kore/test/Test/Kore/Step/Simplifier.hs +++ b/kore/test/Test/Kore/Step/Simplifier.hs @@ -19,9 +19,6 @@ import Kore.Internal.Predicate ) import Kore.Internal.TermLike as TermLike import Kore.Step.Simplification.Simplify -import Kore.Syntax.Variable - ( SortedVariable (..) - ) mockSimplifier :: InternalVariable variable @@ -76,9 +73,8 @@ mockSimplifierHelper unevaluatedPatt convertTermLikeVariables - :: ( Ord variable - , SortedVariable variable - , SortedVariable variable0 + :: ( VariableName variable + , VariableName variable0 , FreshVariable variable0 ) => TermLike variable @@ -89,9 +85,8 @@ convertTermLikeVariables = (fmap $ fromVariable . toVariable) convertPatternVariables - :: ( Ord variable - , SortedVariable variable - , SortedVariable variable0 + :: ( VariableName variable + , VariableName variable0 , FreshVariable variable0 ) => Pattern variable diff --git a/kore/test/Test/Kore/Unification/Unifier.hs b/kore/test/Test/Kore/Unification/Unifier.hs index eaec948667..bd2c324f0d 100644 --- a/kore/test/Test/Kore/Unification/Unifier.hs +++ b/kore/test/Test/Kore/Unification/Unifier.hs @@ -683,8 +683,14 @@ instance Diff V instance SortedVariable V where sortedVariableSort _ = sortVar - fromVariable = error "Not implemented" - toVariable = error "Not implemented" + +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" @@ -714,8 +720,14 @@ instance Diff W instance SortedVariable W where sortedVariableSort _ = sortVar - fromVariable = error "Not implemented" - toVariable = error "Not implemented" + +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" From a9913eca0d1cf5d1dac330c173506608e1ffa327 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 11 Feb 2020 14:58:03 -0600 Subject: [PATCH 2/6] SideCondition.Representation: Use a dynamic representation --- .../Internal/SideCondition/SideCondition.hs | 76 ++++++++++++++----- 1 file changed, 57 insertions(+), 19 deletions(-) diff --git a/kore/src/Kore/Internal/SideCondition/SideCondition.hs b/kore/src/Kore/Internal/SideCondition/SideCondition.hs index fd43c0c108..390d4a17ae 100644 --- a/kore/src/Kore/Internal/SideCondition/SideCondition.hs +++ b/kore/src/Kore/Internal/SideCondition/SideCondition.hs @@ -11,43 +11,81 @@ module Kore.Internal.SideCondition.SideCondition import Prelude.Kore import Control.DeepSeq - ( NFData + ( NFData (..) ) import Data.Hashable - ( Hashable + ( Hashable (..) , Hashed , hashed ) import Data.Text ( Text ) -import qualified Generics.SOP as SOP - ( Generic - , HasDatatypeInfo - ) -import qualified GHC.Generics as GHC +import Data.Type.Equality + ( (:~:) (..) + , testEquality + ) import Kore.Debug - ( Debug + ( Debug (..) , Diff (..) ) +import Type.Reflection + ( SomeTypeRep (..) + , TypeRep + , Typeable + , typeRep + ) + +data Representation where + Representation :: Ord a => !(TypeRep a) -> !(Hashed a) -> Representation + +instance Eq Representation where + (==) (Representation typeRep1 hashed1) (Representation typeRep2 hashed2) = + case testEquality typeRep1 typeRep2 of + Nothing -> False + Just Refl -> hashed1 == hashed2 + {-# INLINE (==) #-} + +instance Ord Representation where + compare + (Representation typeRep1 hashed1) + (Representation typeRep2 hashed2) + = + case testEquality typeRep1 typeRep2 of + Nothing -> compare (SomeTypeRep typeRep1) (SomeTypeRep typeRep2) + Just Refl -> compare hashed1 hashed2 + {-# INLINE compare #-} + +instance Show Representation where + showsPrec prec (Representation typeRep1 _) = + showParen (prec >= 10) + $ showString "Representation " . shows typeRep1 . showString " _" + {-# INLINE showsPrec #-} -newtype Representation = - Representation - { getRepresentation :: Hashed Text - } - deriving (Eq, GHC.Generic, Hashable, NFData, Ord, Show) +instance Hashable Representation where + hashWithSalt salt (Representation typeRep1 hashed1) = + salt `hashWithSalt` typeRep1 `hashWithSalt` hashed1 + {-# INLINE hashWithSalt #-} -instance SOP.Generic Representation +instance NFData Representation where + rnf (Representation typeRep1 hashed1) = typeRep1 `seq` hashed1 `seq` () + {-# INLINE rnf #-} -instance SOP.HasDatatypeInfo Representation +mkRepresentation :: (Ord a, Hashable a, Typeable a) => a -> Representation +mkRepresentation = Representation typeRep . hashed -instance Debug Representation +instance Debug Representation where + debugPrec _ _ = "_" + {-# INLINE debugPrec #-} -instance Diff Representation +instance Diff Representation where + diffPrec _ _ = Nothing + {-# INLINE diffPrec #-} -instance From Text Representation where - from = Representation . hashed +instance (Ord a, Hashable a, Typeable a) => From a Representation where + from = mkRepresentation + {-# INLINE from #-} fromText :: Text -> Representation fromText = from From cf895ef96b327ae219a7ed96aea8c02a38ba85ac Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 11 Feb 2020 15:13:30 -0600 Subject: [PATCH 3/6] toRepresentationCondition: Store a (Condition Variable) Store the Condition (with its variable names mapped down to Variable) instead of the unparsed Condition. Using the dynamic representation in this way is Slightly Evil, but 50% faster. --- kore/src/Kore/Attribute/Pattern.hs | 3 +++ kore/src/Kore/Internal/SideCondition.hs | 9 ++++----- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/kore/src/Kore/Attribute/Pattern.hs b/kore/src/Kore/Attribute/Pattern.hs index 32b78ce9ff..b463391729 100644 --- a/kore/src/Kore/Attribute/Pattern.hs +++ b/kore/src/Kore/Attribute/Pattern.hs @@ -89,6 +89,9 @@ data Pattern variable = } deriving (Eq, GHC.Generic, Show) +-- TODO (thomas.tuegel): Lift 'simplified' to the 'Conditional' level once we +-- treat the latter as an aggregate root. + instance NFData variable => NFData (Pattern variable) instance Hashable variable => Hashable (Pattern variable) diff --git a/kore/src/Kore/Internal/SideCondition.hs b/kore/src/Kore/Internal/SideCondition.hs index f447dc98ae..7a66a59701 100644 --- a/kore/src/Kore/Internal/SideCondition.hs +++ b/kore/src/Kore/Internal/SideCondition.hs @@ -36,9 +36,6 @@ import qualified Kore.Internal.Condition as Condition import Kore.Internal.Predicate ( Predicate ) -import qualified Kore.Internal.SideCondition.SideCondition as SideCondition.Representation - ( fromText - ) import qualified Kore.Internal.SideCondition.SideCondition as SideCondition ( Representation ) @@ -46,13 +43,14 @@ import Kore.Internal.Variable ( ElementVariable , InternalVariable , SetVariable + , Variable + , toVariable ) import Kore.TopBottom ( TopBottom (..) ) import Kore.Unparser ( Unparse (..) - , unparseToText ) import qualified Pretty import qualified SQL @@ -175,4 +173,5 @@ toRepresentationCondition => Condition variable -> SideCondition.Representation toRepresentationCondition condition = - SideCondition.Representation.fromText $ unparseToText condition + from @(Condition Variable) + $ Condition.mapVariables (fmap toVariable) (fmap toVariable) condition From 612d10247da6df126925a5f4ebb0813d703fdbce Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 11 Feb 2020 15:25:09 -0600 Subject: [PATCH 4/6] Kore.Step.EquationalStep: Avoid side condition's free variables --- kore/src/Kore/Step/EquationalStep.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/kore/src/Kore/Step/EquationalStep.hs b/kore/src/Kore/Step/EquationalStep.hs index f480de776e..cd8a0fe239 100644 --- a/kore/src/Kore/Step/EquationalStep.hs +++ b/kore/src/Kore/Step/EquationalStep.hs @@ -385,8 +385,7 @@ applyRulesSequence sideCondition initial rules = matchRules sideCondition initial rules' >>= finalizeRulesSequence sideCondition initial where - -- TODO (thomas.tuegel): Include freeVariables sideCondition - avoidConfigVars = freeVariables initial + avoidConfigVars = freeVariables sideCondition <> freeVariables initial rules' = EqualityPattern.targetRuleVariables avoidConfigVars <$> rules -- | Matches a list a rules against a configuration. See 'matchRule'. From 2ed61364ea40a3a00a066b6ccb946c5629bee33f Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 11 Feb 2020 15:36:11 -0600 Subject: [PATCH 5/6] targetRuleVariables: Take side condition and configuration as arguments Taking both the side condition and the configuration as arguments, instead of only a set of free variables, helps ensure that the rule variables are renamed to avoid both the configuration AND the side condition. --- kore/src/Kore/Step/EquationalStep.hs | 3 +-- kore/src/Kore/Step/RewriteStep.hs | 3 +-- kore/src/Kore/Step/Step.hs | 8 ++++++-- kore/test/Test/Kore/Step/RewriteStep.hs | 9 ++++++++- 4 files changed, 16 insertions(+), 7 deletions(-) diff --git a/kore/src/Kore/Step/EquationalStep.hs b/kore/src/Kore/Step/EquationalStep.hs index cd8a0fe239..21489d2065 100644 --- a/kore/src/Kore/Step/EquationalStep.hs +++ b/kore/src/Kore/Step/EquationalStep.hs @@ -385,8 +385,7 @@ applyRulesSequence sideCondition initial rules = matchRules sideCondition initial rules' >>= finalizeRulesSequence sideCondition initial where - avoidConfigVars = freeVariables sideCondition <> freeVariables initial - rules' = EqualityPattern.targetRuleVariables avoidConfigVars <$> rules + rules' = EqualityPattern.targetRuleVariables sideCondition initial <$> rules -- | Matches a list a rules against a configuration. See 'matchRule'. matchRules diff --git a/kore/src/Kore/Step/RewriteStep.hs b/kore/src/Kore/Step/RewriteStep.hs index 5e49d40866..4fac09db60 100644 --- a/kore/src/Kore/Step/RewriteStep.hs +++ b/kore/src/Kore/Step/RewriteStep.hs @@ -251,8 +251,7 @@ applyRulesWithFinalizer -> unifier (Results RulePattern variable) applyRulesWithFinalizer finalize unificationProcedure rules initial = do let sideCondition = SideCondition.topTODO - configurationVariables = freeVariables initial - rules' = targetRuleVariables configurationVariables <$> rules + rules' = targetRuleVariables sideCondition initial <$> rules results <- unifyRules unificationProcedure sideCondition initial rules' debugAppliedRewriteRules initial results finalize initial results diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index 0f816b9f51..4013c5de26 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -48,6 +48,7 @@ import qualified Data.Text.Prettyprint.Doc as Pretty import qualified Branch import Kore.Attribute.Pattern.FreeVariables ( FreeVariables (..) + , HasFreeVariables (freeVariables) ) import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables import Kore.Internal.Condition @@ -257,13 +258,16 @@ The rule's variables are: targetRuleVariables :: InternalVariable variable => UnifyingRule rule - => FreeVariables (Target variable) + => SideCondition (Target variable) + -> Pattern (Target variable) -> rule variable -> rule (Target variable) -targetRuleVariables avoiding = +targetRuleVariables sideCondition initial = snd . refreshRule avoiding . mapRuleVariables Target.mkElementTarget Target.mkSetTarget + where + avoiding = freeVariables sideCondition <> freeVariables initial {- | Unwrap the variables in a 'RulePattern'. Inverse of 'targetRuleVariables'. -} diff --git a/kore/test/Test/Kore/Step/RewriteStep.hs b/kore/test/Test/Kore/Step/RewriteStep.hs index 690b169065..96b0618c0f 100644 --- a/kore/test/Test/Kore/Step/RewriteStep.hs +++ b/kore/test/Test/Kore/Step/RewriteStep.hs @@ -21,6 +21,9 @@ import Data.Function ) import qualified Data.Set as Set +import Kore.Attribute.Pattern.FreeVariables + ( FreeVariables + ) import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables import qualified Kore.Internal.Condition as Condition import qualified Kore.Internal.Conditional as Conditional @@ -81,6 +84,9 @@ import Kore.Unification.UnifierT import Kore.Variables.Fresh ( nextVariable ) +import Kore.Variables.Target + ( Target + ) import Kore.Variables.UnifiedVariable ( UnifiedVariable (..) ) @@ -186,7 +192,8 @@ test_renameRuleVariables = , rhs = injectTermIntoRHS (Mock.g (mkElemVar Mock.x)) , attributes = Default.def } - actual = Step.targetRuleVariables initialFreeVariables axiom + actual = Step.targetRuleVariables SideCondition.top initial axiom + initialFreeVariables :: FreeVariables (Target Variable) initialFreeVariables = freeVariables initial actualFreeVariables = freeVariables actual assertEqual "Expected no common free variables" From 4536334b099589588a4442a4ebbb3a6bf4fce2b8 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 12 Feb 2020 10:47:26 -0600 Subject: [PATCH 6/6] SideCondition: Remove fromText --- kore/src/Kore/Internal/SideCondition/SideCondition.hs | 7 ------- 1 file changed, 7 deletions(-) diff --git a/kore/src/Kore/Internal/SideCondition/SideCondition.hs b/kore/src/Kore/Internal/SideCondition/SideCondition.hs index 390d4a17ae..d0be912e7b 100644 --- a/kore/src/Kore/Internal/SideCondition/SideCondition.hs +++ b/kore/src/Kore/Internal/SideCondition/SideCondition.hs @@ -5,7 +5,6 @@ License : NCSA module Kore.Internal.SideCondition.SideCondition ( Representation - , fromText ) where import Prelude.Kore @@ -18,9 +17,6 @@ import Data.Hashable , Hashed , hashed ) -import Data.Text - ( Text - ) import Data.Type.Equality ( (:~:) (..) @@ -86,6 +82,3 @@ instance Diff Representation where instance (Ord a, Hashable a, Typeable a) => From a Representation where from = mkRepresentation {-# INLINE from #-} - -fromText :: Text -> Representation -fromText = from