From 63f6a3b5e47849095e256491f4b73d643490f78f Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 21 May 2020 20:18:52 -0500 Subject: [PATCH 01/16] Add AdjUnifiedVariable --- kore/src/Kore/Attribute/Axiom.hs | 12 +- kore/src/Kore/Attribute/Axiom/Concrete.hs | 13 +- kore/src/Kore/Attribute/Axiom/Symbolic.hs | 13 +- kore/src/Kore/Attribute/Pattern.hs | 22 ++-- .../Kore/Attribute/Pattern/FreeVariables.hs | 15 +-- kore/src/Kore/Equation/Application.hs | 122 ++++++------------ kore/src/Kore/Equation/Equation.hs | 46 +++---- kore/src/Kore/Internal/Condition.hs | 7 +- kore/src/Kore/Internal/Conditional.hs | 10 +- kore/src/Kore/Internal/OrPattern.hs | 13 +- kore/src/Kore/Internal/Pattern.hs | 25 ++-- kore/src/Kore/Internal/Predicate.hs | 16 +-- kore/src/Kore/Internal/SideCondition.hs | 15 +-- kore/src/Kore/Internal/Substitution.hs | 30 ++--- kore/src/Kore/Internal/TermLike.hs | 4 +- kore/src/Kore/Internal/TermLike/Renaming.hs | 7 +- kore/src/Kore/Internal/TermLike/TermLike.hs | 100 +++++++------- kore/src/Kore/Log/DebugAppliedRewriteRules.hs | 7 +- .../Kore/Log/ErrorRewritesInstantiation.hs | 6 +- kore/src/Kore/Log/InfoAttemptUnification.hs | 4 +- kore/src/Kore/Log/WarnBottomTotalFunction.hs | 3 +- .../Kore/Log/WarnDecidePredicateUnknown.hs | 7 +- kore/src/Kore/Rewriting/RewritingVariable.hs | 39 ++---- kore/src/Kore/Rewriting/UnifyingRule.hs | 9 +- .../src/Kore/Step/Axiom/EvaluationStrategy.hs | 31 +---- kore/src/Kore/Step/RulePattern.hs | 16 +-- .../Kore/Step/Simplification/ExpandAlias.hs | 14 +- kore/src/Kore/Step/Simplification/TermLike.hs | 18 ++- kore/src/Kore/Step/Step.hs | 2 +- kore/src/Kore/Syntax/ElementVariable.hs | 12 +- kore/src/Kore/Syntax/Pattern.hs | 26 ++-- kore/src/Kore/Syntax/PatternF.hs | 25 ++-- kore/src/Kore/Syntax/SetVariable.hs | 12 +- kore/src/Kore/Unification/Error.hs | 3 +- kore/src/Kore/Variables/Target.hs | 15 ++- kore/src/Kore/Variables/UnifiedVariable.hs | 85 +++++++++--- kore/test/Test/Kore/Equation/Application.hs | 9 +- kore/test/Test/Kore/Internal/Pattern.hs | 2 +- kore/test/Test/Kore/Internal/Substitution.hs | 8 +- kore/test/Test/Kore/Internal/TermLike.hs | 20 +-- .../Test/Kore/Step/Function/Integration.hs | 9 +- kore/test/Test/Kore/Step/Rule/Simplify.hs | 8 +- .../Test/Kore/Step/Simplification/Ceil.hs | 9 +- kore/test/Test/Kore/Unification/Unifier.hs | 6 +- kore/test/Test/Kore/Variables/Fresh.hs | 4 +- kore/test/Test/Kore/Variables/W.hs | 5 + 46 files changed, 415 insertions(+), 469 deletions(-) diff --git a/kore/src/Kore/Attribute/Axiom.hs b/kore/src/Kore/Attribute/Axiom.hs index b28d53b395..efbb04e3a1 100644 --- a/kore/src/Kore/Attribute/Axiom.hs +++ b/kore/src/Kore/Attribute/Axiom.hs @@ -86,11 +86,10 @@ import Kore.Internal.Symbol ( Symbol (..) , toSymbolOrAlias ) -import Kore.Syntax.ElementVariable -import Kore.Syntax.SetVariable import Kore.Syntax.Variable ( Variable (..) ) +import Kore.Variables.UnifiedVariable import qualified SQL {- | Attributes specific to Kore axiom sentences. @@ -267,13 +266,12 @@ parseAxiomAttributes freeVariables (Attributes attrs) = mapAxiomVariables :: Ord variable2 - => (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) -> Axiom symbol variable1 -> Axiom symbol variable2 -mapAxiomVariables e s axiom@Axiom { concrete, symbolic } = +mapAxiomVariables mapping axiom@Axiom { concrete, symbolic } = axiom - { concrete = mapConcreteVariables e s concrete - , symbolic = mapSymbolicVariables e s symbolic + { concrete = mapConcreteVariables mapping concrete + , symbolic = mapSymbolicVariables mapping symbolic } getPriorityOfAxiom diff --git a/kore/src/Kore/Attribute/Axiom/Concrete.hs b/kore/src/Kore/Attribute/Axiom/Concrete.hs index 1933f1e84b..bf60682c38 100644 --- a/kore/src/Kore/Attribute/Axiom/Concrete.hs +++ b/kore/src/Kore/Attribute/Axiom/Concrete.hs @@ -35,14 +35,10 @@ import Kore.Attribute.Pattern.FreeVariables import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables import Kore.Debug import qualified Kore.Error -import Kore.Syntax.ElementVariable -import Kore.Syntax.SetVariable import Kore.Syntax.Variable ( Variable ) import Kore.Variables.UnifiedVariable - ( UnifiedVariable - ) {- | @Concrete@ represents the @concrete@ attribute for axioms. -} @@ -134,11 +130,10 @@ instance From (Concrete Variable) Attributes where mapConcreteVariables :: Ord variable2 - => (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) - -> Concrete variable1 -> Concrete variable2 -mapConcreteVariables mapElemVar mapSetVar (Concrete freeVariables) = - Concrete (mapFreeVariables mapElemVar mapSetVar freeVariables) + => AdjUnifiedVariable (variable1 -> variable2) + -> Concrete variable1 -> Concrete variable2 +mapConcreteVariables morphism (Concrete freeVariables) = + Concrete (mapFreeVariables morphism freeVariables) isConcrete :: Ord variable => Concrete variable -> UnifiedVariable variable -> Bool diff --git a/kore/src/Kore/Attribute/Axiom/Symbolic.hs b/kore/src/Kore/Attribute/Axiom/Symbolic.hs index 82c4905615..2ef2a72b8a 100644 --- a/kore/src/Kore/Attribute/Axiom/Symbolic.hs +++ b/kore/src/Kore/Attribute/Axiom/Symbolic.hs @@ -30,14 +30,10 @@ import Kore.Attribute.Pattern.FreeVariables ) import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables import Kore.Debug -import Kore.Syntax.ElementVariable -import Kore.Syntax.SetVariable import Kore.Syntax.Variable ( Variable ) import Kore.Variables.UnifiedVariable - ( UnifiedVariable - ) {- | @Symbolic@ represents the @symbolic@ attribute for axioms. -} @@ -98,11 +94,10 @@ instance From (Symbolic Variable) Attributes where mapSymbolicVariables :: Ord variable2 - => (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) - -> Symbolic variable1 -> Symbolic variable2 -mapSymbolicVariables mapElemVar mapSetVar (Symbolic freeVariables) = - Symbolic (mapFreeVariables mapElemVar mapSetVar freeVariables) + => AdjUnifiedVariable (variable1 -> variable2) + -> Symbolic variable1 -> Symbolic variable2 +mapSymbolicVariables morphism (Symbolic freeVariables) = + Symbolic (mapFreeVariables morphism freeVariables) isSymbolic :: Ord variable => Symbolic variable -> UnifiedVariable variable -> Bool diff --git a/kore/src/Kore/Attribute/Pattern.hs b/kore/src/Kore/Attribute/Pattern.hs index ee45d77313..baeff8cec8 100644 --- a/kore/src/Kore/Attribute/Pattern.hs +++ b/kore/src/Kore/Attribute/Pattern.hs @@ -64,10 +64,6 @@ import Kore.Sort ( Sort ) import Kore.Variables.UnifiedVariable - ( ElementVariable - , SetVariable - , UnifiedVariable (..) - ) {- | @Pattern@ are the attributes of a pattern collected during verification. -} @@ -177,12 +173,11 @@ See also: 'traverseVariables' -} mapVariables :: Ord variable2 - => (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) -> Pattern variable1 -> Pattern variable2 -mapVariables mapElemVar mapSetVar = +mapVariables morphism = Lens.over (field @"freeVariables") - (mapFreeVariables mapElemVar mapSetVar) + (mapFreeVariables morphism) {- | Use the provided traversal to replace the free variables in a 'Pattern'. @@ -190,14 +185,13 @@ See also: 'mapVariables' -} traverseVariables - :: forall m variable1 variable2. - (Monad m, Ord variable2) - => (ElementVariable variable1 -> m (ElementVariable variable2)) - -> (SetVariable variable1 -> m (SetVariable variable2)) + :: forall m variable1 variable2 + . (Monad m, Ord variable2) + => AdjUnifiedVariable (variable1 -> m variable2) -> Pattern variable1 -> m (Pattern variable2) -traverseVariables trElemVar trSetVar = - field @"freeVariables" (traverseFreeVariables trElemVar trSetVar) +traverseVariables morphism = + field @"freeVariables" (traverseFreeVariables morphism) {- | Delete the given variable from the set of free variables. -} diff --git a/kore/src/Kore/Attribute/Pattern/FreeVariables.hs b/kore/src/Kore/Attribute/Pattern/FreeVariables.hs index e16b040186..f89e031906 100644 --- a/kore/src/Kore/Attribute/Pattern/FreeVariables.hs +++ b/kore/src/Kore/Attribute/Pattern/FreeVariables.hs @@ -35,7 +35,6 @@ import qualified GHC.Generics as GHC import Kore.Attribute.Synthetic import Kore.Debug import Kore.Syntax.ElementVariable -import Kore.Syntax.SetVariable import Kore.Variables.UnifiedVariable newtype FreeVariables variable = @@ -115,23 +114,21 @@ freeVariable variable = FreeVariables (Set.singleton variable) mapFreeVariables :: Ord variable2 - => (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) -> FreeVariables variable1 -> FreeVariables variable2 -mapFreeVariables mapElemVar mapSetVar (FreeVariables freeVars) = - FreeVariables (Set.map (mapUnifiedVariable mapElemVar mapSetVar) freeVars) +mapFreeVariables morphism (FreeVariables freeVars) = + FreeVariables (Set.map (mapUnifiedVariable morphism) freeVars) {-# INLINE mapFreeVariables #-} traverseFreeVariables :: (Applicative f, Ord variable2) - => (ElementVariable variable1 -> f (ElementVariable variable2)) - -> (SetVariable variable1 -> f (SetVariable variable2)) + => AdjUnifiedVariable (variable1 -> f variable2) -> FreeVariables variable1 -> f (FreeVariables variable2) -traverseFreeVariables traverseElemVar traverseSetVar (FreeVariables freeVars) = +traverseFreeVariables morphism (FreeVariables freeVars) = FreeVariables . Set.fromList <$> Traversable.traverse traversal (Set.toList freeVars) where - traversal = traverseUnifiedVariable traverseElemVar traverseSetVar + traversal = traverseUnifiedVariable morphism {-# INLINE traverseFreeVariables #-} {- | Extracts the list of free element variables diff --git a/kore/src/Kore/Equation/Application.hs b/kore/src/Kore/Equation/Application.hs index 4035993f44..f50445a761 100644 --- a/kore/src/Kore/Equation/Application.hs +++ b/kore/src/Kore/Equation/Application.hs @@ -81,9 +81,7 @@ import Kore.Internal.SideCondition ) import qualified Kore.Internal.SideCondition as SideCondition import Kore.Internal.TermLike - ( ElementVariable (..) - , InternalVariable - , SetVariable (..) + ( InternalVariable , TermLike ) import qualified Kore.Internal.TermLike as TermLike @@ -102,7 +100,6 @@ import Kore.Syntax.Id ) import Kore.Syntax.Variable ( Variable - , toVariable ) import Kore.TopBottom import Kore.Unparser @@ -113,9 +110,6 @@ import Kore.Variables.Target ) import qualified Kore.Variables.Target as Target import Kore.Variables.UnifiedVariable - ( UnifiedVariable - , mapUnifiedVariable - ) import Log ( Entry (..) , MonadLog @@ -228,10 +222,10 @@ applyMatchResult equation matchResult@(predicate, substitution) = do _ -> return () let predicate' = Predicate.substitute substitution predicate - & Predicate.mapVariables Target.unTargetElement Target.unTargetSet + & Predicate.mapVariables Target.unTargetUnified equation' = Equation.substitute substitution equation - & Equation.mapVariables Target.unTargetElement Target.unTargetSet + & Equation.mapVariables Target.unTargetUnified return (equation', predicate') where equationVariables = freeVariables equation & FreeVariables.toList @@ -308,8 +302,7 @@ checkRequires sideCondition predicate requires = -- TODO (thomas.tuegel): Do not unwrap sideCondition. sideCondition' = SideCondition.mapVariables - Target.unTargetElement - Target.unTargetSet + Target.unTargetUnified sideCondition assertBottom orCondition @@ -346,7 +339,7 @@ targetEquationVariables targetEquationVariables sideCondition initial = snd . Equation.refreshVariables avoiding - . Equation.mapVariables Target.mkElementTarget Target.mkSetTarget + . Equation.mapVariables Target.mkUnifiedTarget where avoiding = freeVariables sideCondition <> freeVariables initial @@ -363,36 +356,23 @@ data AttemptEquationError variable mapAttemptEquationErrorVariables :: (InternalVariable variable1, InternalVariable variable2) - => (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) -> AttemptEquationError variable1 -> AttemptEquationError variable2 -mapAttemptEquationErrorVariables mapElemVar mapSetVar = +mapAttemptEquationErrorVariables adj = \case WhileMatch matchError -> - WhileMatch - $ mapMatchErrorVariables - mapElemTargetVar mapSetTargetVar - matchError + WhileMatch $ mapMatchErrorVariables adjTarget matchError WhileApplyMatchResult applyMatchResultErrors -> WhileApplyMatchResult $ mapApplyMatchResultErrorsVariables - mapElemTargetVar mapSetTargetVar + adjTarget applyMatchResultErrors WhileCheckRequires checkRequiresError -> WhileCheckRequires - $ mapCheckRequiresErrorVariables - mapElemVar mapSetVar - checkRequiresError + $ mapCheckRequiresErrorVariables adj checkRequiresError where - mapElemTargetVar = - ElementVariable - . fmap (getElementVariable . mapElemVar . ElementVariable) - . getElementVariable - mapSetTargetVar = - SetVariable - . fmap (getSetVariable . mapSetVar . SetVariable) - . getSetVariable + adjTarget = fmap <$> adj whileMatch :: Functor monad @@ -454,16 +434,14 @@ instance InternalVariable variable => Pretty (MatchError variable) where mapMatchErrorVariables :: (InternalVariable variable1, InternalVariable variable2) - => (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) -> MatchError variable1 -> MatchError variable2 -mapMatchErrorVariables mapElemVar mapSetVar = +mapMatchErrorVariables mapping = \MatchError { matchTerm, matchEquation } -> MatchError - { matchTerm = TermLike.mapVariables mapElemVar mapSetVar matchTerm - , matchEquation = - Equation.mapVariables mapElemVar mapSetVar matchEquation + { matchTerm = TermLike.mapVariables mapping matchTerm + , matchEquation = Equation.mapVariables mapping matchEquation } {- | Errors that can occur during 'applyMatchResult'. @@ -503,17 +481,14 @@ instance mapApplyMatchResultErrorsVariables :: (InternalVariable variable1, InternalVariable variable2) - => (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) -> ApplyMatchResultErrors variable1 -> ApplyMatchResultErrors variable2 -mapApplyMatchResultErrorsVariables mapElemVar mapSetVar applyMatchResultErrors = +mapApplyMatchResultErrorsVariables mapping applyMatchResultErrors = ApplyMatchResultErrors - { matchResult = mapMatchResultVariables mapElemVar mapSetVar matchResult + { matchResult = mapMatchResultVariables mapping matchResult , applyMatchErrors = - fmap - (mapApplyMatchResultErrorVariables mapElemVar mapSetVar) - applyMatchErrors + mapApplyMatchResultErrorVariables mapping <$> applyMatchErrors } where ApplyMatchResultErrors { matchResult, applyMatchErrors } = @@ -521,18 +496,17 @@ mapApplyMatchResultErrorsVariables mapElemVar mapSetVar applyMatchResultErrors = mapMatchResultVariables :: (InternalVariable variable1, InternalVariable variable2) - => (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) -> MatchResult variable1 -> MatchResult variable2 -mapMatchResultVariables mapElemVar mapSetVar (predicate, substitution) = - ( Predicate.mapVariables mapElemVar mapSetVar predicate +mapMatchResultVariables mapping (predicate, substitution) = + ( Predicate.mapVariables mapping predicate , mapSubstitutionVariables substitution ) where mapSubstitutionVariables = - Map.mapKeys (mapUnifiedVariable mapElemVar mapSetVar) - . Map.map (TermLike.mapVariables mapElemVar mapSetVar) + Map.mapKeys (mapUnifiedVariable mapping) + . Map.map (TermLike.mapVariables mapping) {- | @ApplyMatchResultError@ represents a reason the match could not be applied. -} @@ -579,11 +553,10 @@ instance mapApplyMatchResultErrorVariables :: (InternalVariable variable1, InternalVariable variable2) - => (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) -> ApplyMatchResultError variable1 -> ApplyMatchResultError variable2 -mapApplyMatchResultErrorVariables mapElemVar mapSetVar applyMatchResultError = +mapApplyMatchResultErrorVariables mapping applyMatchResultError = case applyMatchResultError of NotConcrete variable termLike -> NotConcrete @@ -595,8 +568,8 @@ mapApplyMatchResultErrorVariables mapElemVar mapSetVar applyMatchResultError = (mapTermLikeVariables termLike) NotMatched variable -> NotMatched (mapUnifiedVariable' variable) where - mapUnifiedVariable' = mapUnifiedVariable mapElemVar mapSetVar - mapTermLikeVariables = TermLike.mapVariables mapElemVar mapSetVar + mapUnifiedVariable' = mapUnifiedVariable mapping + mapTermLikeVariables = TermLike.mapVariables mapping {- | Errors that can occur during 'checkRequires'. -} @@ -627,17 +600,16 @@ instance InternalVariable variable => Pretty (CheckRequiresError variable) where mapCheckRequiresErrorVariables :: (InternalVariable variable1, InternalVariable variable2) - => (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) -> CheckRequiresError variable1 -> CheckRequiresError variable2 -mapCheckRequiresErrorVariables mapElemVar mapSetVar checkRequiresError = +mapCheckRequiresErrorVariables mapping checkRequiresError = CheckRequiresError { matchPredicate = mapPredicateVariables matchPredicate , equationRequires = mapPredicateVariables equationRequires } where - mapPredicateVariables = Predicate.mapVariables mapElemVar mapSetVar + mapPredicateVariables = Predicate.mapVariables mapping CheckRequiresError { matchPredicate, equationRequires } = checkRequiresError -- * Logging @@ -693,26 +665,18 @@ debugAttemptEquationResult -> log () debugAttemptEquationResult equation result = logEntry $ DebugAttemptEquationResult - (Equation.mapVariables toElementVariable toSetVariable equation) - (mapAttemptEquationResultVariables - toElementVariable - toSetVariable - result - ) - where - toElementVariable = fmap toVariable - toSetVariable = fmap toVariable + (Equation.mapVariables toUnifiedVariable equation) + (mapAttemptEquationResultVariables toUnifiedVariable result) mapAttemptEquationResultVariables :: (InternalVariable variable1, InternalVariable variable2) - => (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) -> AttemptEquationResult variable1 -> AttemptEquationResult variable2 -mapAttemptEquationResultVariables mapElemVar mapSetVar = +mapAttemptEquationResultVariables mapping = Bifunctor.bimap - (mapAttemptEquationErrorVariables mapElemVar mapSetVar) - (Pattern.mapVariables mapElemVar mapSetVar) + (mapAttemptEquationErrorVariables mapping) + (Pattern.mapVariables mapping) whileDebugAttemptEquation :: MonadLog log @@ -724,10 +688,8 @@ whileDebugAttemptEquation whileDebugAttemptEquation termLike equation = logWhile (DebugAttemptEquation equation' termLike') where - toElementVariable = fmap toVariable - toSetVariable = fmap toVariable - termLike' = TermLike.mapVariables toElementVariable toSetVariable termLike - equation' = Equation.mapVariables toElementVariable toSetVariable equation + termLike' = TermLike.mapVariables toUnifiedVariable termLike + equation' = Equation.mapVariables toUnifiedVariable equation {- | Log when an 'Equation' is actually applied. -} @@ -783,7 +745,5 @@ debugApplyEquation debugApplyEquation equation result = logEntry $ DebugApplyEquation equation' result' where - toElementVariable = fmap toVariable - toSetVariable = fmap toVariable - equation' = Equation.mapVariables toElementVariable toSetVariable equation - result' = Pattern.mapVariables toElementVariable toSetVariable result + equation' = Equation.mapVariables toUnifiedVariable equation + result' = Pattern.mapVariables toUnifiedVariable result diff --git a/kore/src/Kore/Equation/Equation.hs b/kore/src/Kore/Equation/Equation.hs index 075fa1c575..ab59e00a7d 100644 --- a/kore/src/Kore/Equation/Equation.hs +++ b/kore/src/Kore/Equation/Equation.hs @@ -20,9 +20,13 @@ import Prelude.Kore import Control.DeepSeq ( NFData ) +import qualified Control.Lens as Lens import qualified Data.Default as Default import qualified Data.Foldable as Foldable import qualified Data.Functor.Foldable as Recursive +import Data.Generics.Wrapped + ( _Wrapped + ) import Data.Map.Strict ( Map ) @@ -53,10 +57,8 @@ import Kore.Internal.Symbol ( Symbol (..) ) import Kore.Internal.TermLike - ( ElementVariable - , Id (..) + ( Id (..) , InternalVariable - , SetVariable , Sort , TermLike , Variable @@ -75,8 +77,6 @@ import Kore.Unparser ) import qualified Kore.Variables.Fresh as Fresh import Kore.Variables.UnifiedVariable - ( UnifiedVariable (..) - ) import Pretty ( Pretty (..) ) @@ -199,22 +199,20 @@ instance AstWithLocation variable => AstWithLocation (Equation variable) where mapVariables :: (Ord variable1, InternalVariable variable2) - => (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) -> Equation variable1 -> Equation variable2 -mapVariables mapElemVar mapSetVar equation@(Equation _ _ _ _ _) = +mapVariables mapping equation@(Equation _ _ _ _ _) = equation { requires = mapPredicateVariables requires , left = mapTermLikeVariables left , right = mapTermLikeVariables right , ensures = mapPredicateVariables ensures - , attributes = - Attribute.mapAxiomVariables mapElemVar mapSetVar attributes + , attributes = Attribute.mapAxiomVariables mapping attributes } where Equation { requires, left, right, ensures, attributes } = equation - mapTermLikeVariables = TermLike.mapVariables mapElemVar mapSetVar - mapPredicateVariables = Predicate.mapVariables mapElemVar mapSetVar + mapTermLikeVariables = TermLike.mapVariables mapping + mapPredicateVariables = Predicate.mapVariables mapping refreshVariables :: forall variable @@ -227,21 +225,25 @@ refreshVariables equation@(Equation _ _ _ _ _) = let rename = Fresh.refreshVariables avoid originalFreeVariables - mapElemVars elemVar = - case Map.lookup (ElemVar elemVar) rename of - Just (ElemVar elemVar') -> elemVar' - _ -> elemVar - mapSetVars setVar = - case Map.lookup (SetVar setVar) rename of - Just (SetVar setVar') -> setVar' - _ -> setVar + adj = + AdjUnifiedVariable + { elemVar = + ElementVariable . Lens.over _Wrapped $ \var -> + case Map.lookup (ElemVar var) rename of + Just (ElemVar var') -> var' + _ -> var + , setVar = + SetVariable . Lens.over _Wrapped $ \var -> + case Map.lookup (SetVar var) rename of + Just (SetVar var') -> var' + _ -> var + } subst = TermLike.mkVar <$> rename left' = TermLike.substitute subst left requires' = Predicate.substitute subst requires right' = TermLike.substitute subst right ensures' = Predicate.substitute subst ensures - attributes' = - Attribute.mapAxiomVariables mapElemVars mapSetVars attributes + attributes' = Attribute.mapAxiomVariables adj attributes equation' = equation { left = left' diff --git a/kore/src/Kore/Internal/Condition.hs b/kore/src/Kore/Internal/Condition.hs index 14b2105fcc..b9a294f303 100644 --- a/kore/src/Kore/Internal/Condition.hs +++ b/kore/src/Kore/Internal/Condition.hs @@ -64,8 +64,6 @@ import qualified Kore.Internal.TermLike as TermLike import Kore.Internal.Variable import Kore.Syntax import Kore.Variables.UnifiedVariable - ( UnifiedVariable - ) -- | A predicate and substitution without an accompanying term. type Condition variable = Conditional variable () @@ -162,11 +160,10 @@ toPredicate = from mapVariables :: (InternalVariable variable1, InternalVariable variable2) - => (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) -> Condition variable1 -> Condition variable2 -mapVariables = Conditional.mapVariables (\_ _ () -> ()) +mapVariables = Conditional.mapVariables (\_ () -> ()) {- | Create a new 'Condition' from the 'Normalization' of a substitution. diff --git a/kore/src/Kore/Internal/Conditional.hs b/kore/src/Kore/Internal/Conditional.hs index bd51dc9884..3a15100fbe 100644 --- a/kore/src/Kore/Internal/Conditional.hs +++ b/kore/src/Kore/Internal/Conditional.hs @@ -436,15 +436,13 @@ mapVariables (Conditional variableTo termTo) mapVariables mapTermVariables - mapElemVar - mapSetVar + mapping Conditional { term, predicate, substitution } = Conditional - { term = mapTermVariables mapElemVar mapSetVar term - , predicate = Predicate.mapVariables mapElemVar mapSetVar predicate - , substitution = - Substitution.mapVariables mapElemVar mapSetVar substitution + { term = mapTermVariables mapping term + , predicate = Predicate.mapVariables mapping predicate + , substitution = Substitution.mapVariables mapping substitution } splitTerm :: Conditional variable term -> (term, Conditional variable ()) diff --git a/kore/src/Kore/Internal/OrPattern.hs b/kore/src/Kore/Internal/OrPattern.hs index e8b1edb5d9..d6c796cc3d 100644 --- a/kore/src/Kore/Internal/OrPattern.hs +++ b/kore/src/Kore/Internal/OrPattern.hs @@ -27,7 +27,11 @@ module Kore.Internal.OrPattern import Prelude.Kore +import qualified Control.Lens as Lens import qualified Data.Foldable as Foldable +import Data.Generics.Wrapped + ( _Wrapped + ) import Branch ( BranchT @@ -69,9 +73,9 @@ import Kore.Variables.Binding import Kore.Variables.Target ( Target (..) , mkElementTarget - , mkSetNonTarget , targetIfEqual ) +import Kore.Variables.UnifiedVariable {-| The disjunction of 'Pattern'. -} @@ -216,8 +220,11 @@ targetBinder Binder { binderVariable, binderChild } = targetIfEqual binderVariable newChild = Pattern.mapVariables - targetBoundVariables - mkSetNonTarget + AdjUnifiedVariable + { elemVar = + (ElementVariable . Lens.over _Wrapped) targetBoundVariables + , setVar = SetVariable NonTarget + } <$> binderChild in Binder { binderVariable = newVar diff --git a/kore/src/Kore/Internal/Pattern.hs b/kore/src/Kore/Internal/Pattern.hs index 09c5572d51..2ad142a556 100644 --- a/kore/src/Kore/Internal/Pattern.hs +++ b/kore/src/Kore/Internal/Pattern.hs @@ -64,7 +64,6 @@ import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.TermLike ( ElementVariable , InternalVariable - , SetVariable , Sort , TermLike , mkAnd @@ -82,8 +81,6 @@ import Kore.TopBottom ( TopBottom (..) ) import Kore.Variables.UnifiedVariable - ( UnifiedVariable - ) {- | The conjunction of a pattern, predicate, and substitution. @@ -134,21 +131,15 @@ freeElementVariables = in an Pattern. -} mapVariables - :: (InternalVariable variableFrom, InternalVariable variableTo) - => (ElementVariable variableFrom -> ElementVariable variableTo) - -> (SetVariable variableFrom -> SetVariable variableTo) - -> Pattern variableFrom - -> Pattern variableTo -mapVariables - mapElemVar - mapSetVar - Conditional { term, predicate, substitution } - = + :: (InternalVariable variable1, InternalVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) + -> Pattern variable1 + -> Pattern variable2 +mapVariables adj Conditional { term, predicate, substitution } = Conditional - { term = TermLike.mapVariables mapElemVar mapSetVar term - , predicate = Predicate.mapVariables mapElemVar mapSetVar predicate - , substitution = - Substitution.mapVariables mapElemVar mapSetVar substitution + { term = TermLike.mapVariables adj term + , predicate = Predicate.mapVariables adj predicate + , substitution = Substitution.mapVariables adj substitution } {- | Convert an 'Pattern' to an ordinary 'TermLike'. diff --git a/kore/src/Kore/Internal/Predicate.hs b/kore/src/Kore/Internal/Predicate.hs index d8a900875a..4b03369585 100644 --- a/kore/src/Kore/Internal/Predicate.hs +++ b/kore/src/Kore/Internal/Predicate.hs @@ -126,8 +126,6 @@ import Kore.Variables.Fresh ( FreshPartialOrd ) import Kore.Variables.UnifiedVariable - ( UnifiedVariable (..) - ) import Pretty ( Pretty (..) ) @@ -734,13 +732,11 @@ isPredicate = Either.isRight . makePredicate {- | Replace all variables in a @Predicate@ using the provided mapping. -} mapVariables - :: (Ord from, FreshPartialOrd to, SortedVariable to) - => (ElementVariable from -> ElementVariable to) - -> (SetVariable from -> SetVariable to) - -> Predicate from - -> Predicate to -mapVariables mapElemVar mapSetVar = - fmap (TermLike.mapVariables mapElemVar mapSetVar) + :: (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) + -> Predicate variable1 + -> Predicate variable2 +mapVariables mapping = fmap (TermLike.mapVariables mapping) instance HasFreeVariables (Predicate variable) variable where freeVariables = freeVariables . unwrapPredicate @@ -842,7 +838,7 @@ externalizeFreshVariables -> Predicate Variable externalizeFreshVariables predicate = TermLike.externalizeFreshVariables - . TermLike.mapVariables (fmap toVariable) (fmap toVariable) + . TermLike.mapVariables toUnifiedVariable <$> predicate depth :: Predicate variable -> Int diff --git a/kore/src/Kore/Internal/SideCondition.hs b/kore/src/Kore/Internal/SideCondition.hs index a4ea6bc931..71d52e33aa 100644 --- a/kore/src/Kore/Internal/SideCondition.hs +++ b/kore/src/Kore/Internal/SideCondition.hs @@ -45,11 +45,8 @@ import qualified Kore.Internal.SideCondition.SideCondition as SideCondition ( Representation ) import Kore.Internal.Variable - ( ElementVariable - , InternalVariable - , SetVariable + ( InternalVariable , Variable - , toVariable ) import Kore.TopBottom ( TopBottom (..) @@ -57,6 +54,7 @@ import Kore.TopBottom import Kore.Unparser ( Unparse (..) ) +import Kore.Variables.UnifiedVariable import qualified Pretty import qualified SQL @@ -193,12 +191,11 @@ toRepresentation SideCondition { representation } = representation mapVariables :: (InternalVariable variable1, InternalVariable variable2) - => (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) -> SideCondition variable1 -> SideCondition variable2 -mapVariables mapElemVar mapSetVar condition@(SideCondition _ _) = - fromCondition (Condition.mapVariables mapElemVar mapSetVar assumedTrue) +mapVariables mapping condition@(SideCondition _ _) = + fromCondition (Condition.mapVariables mapping assumedTrue) where SideCondition { assumedTrue } = condition @@ -216,7 +213,7 @@ toRepresentationCondition -> SideCondition.Representation toRepresentationCondition condition = from @(Condition Variable) - $ Condition.mapVariables (fmap toVariable) (fmap toVariable) condition + $ Condition.mapVariables toUnifiedVariable condition isNormalized :: forall variable. Ord variable => SideCondition variable -> Bool isNormalized = Conditional.isNormalized . from @_ @(Condition variable) diff --git a/kore/src/Kore/Internal/Substitution.hs b/kore/src/Kore/Internal/Substitution.hs index cef16e777a..0a969df343 100644 --- a/kore/src/Kore/Internal/Substitution.hs +++ b/kore/src/Kore/Internal/Substitution.hs @@ -440,29 +440,25 @@ modify modify f = wrap . f . unwrap mapAssignmentVariables - :: (InternalVariable variableFrom, InternalVariable variableTo) - => (ElementVariable variableFrom -> ElementVariable variableTo) - -> (SetVariable variableFrom -> SetVariable variableTo) - -> Assignment variableFrom - -> Assignment variableTo -mapAssignmentVariables mapElemVar mapSetVar (Assignment variable term) = + :: (InternalVariable variable1, InternalVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) + -> Assignment variable1 + -> Assignment variable2 +mapAssignmentVariables adj (Assignment variable term) = assign mappedVariable mappedTerm where - mappedVariable = mapUnifiedVariable mapElemVar mapSetVar variable - mappedTerm = TermLike.mapVariables mapElemVar mapSetVar term + mappedVariable = mapUnifiedVariable adj variable + mappedTerm = TermLike.mapVariables adj term -- | 'mapVariables' changes all the variables in the substitution -- with the given function. mapVariables - :: forall variableFrom variableTo - . (InternalVariable variableFrom, InternalVariable variableTo) - => (ElementVariable variableFrom -> ElementVariable variableTo) - -> (SetVariable variableFrom -> SetVariable variableTo) - -> Substitution variableFrom - -> Substitution variableTo -mapVariables mapElemVar mapSetVar = - modify . fmap - $ mapAssignmentVariables mapElemVar mapSetVar + :: forall variable1 variable2 + . (InternalVariable variable1, InternalVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) + -> Substitution variable1 + -> Substitution variable2 +mapVariables adj = modify . fmap $ mapAssignmentVariables adj mapTerms :: InternalVariable variable diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index 329d35ddf6..1adbea3157 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -402,7 +402,7 @@ asConcrete :: Ord variable => TermLike variable -> Maybe (TermLike Concrete) -asConcrete = traverseVariables (\case { _ -> Nothing }) (\case { _ -> Nothing }) +asConcrete = traverseVariables asConcreteUnifiedVariable isConcrete :: Ord variable => TermLike variable -> Bool isConcrete = isJust . asConcrete @@ -420,7 +420,7 @@ fromConcrete :: (FreshPartialOrd variable, SortedVariable variable) => TermLike Concrete -> TermLike variable -fromConcrete = mapVariables (\case {}) (\case {}) +fromConcrete = mapVariables fromConcreteUnifiedVariable isSimplified :: SideCondition.Representation -> TermLike variable -> Bool isSimplified sideCondition = diff --git a/kore/src/Kore/Internal/TermLike/Renaming.hs b/kore/src/Kore/Internal/TermLike/Renaming.hs index 85fc1b6783..d0103b7e53 100644 --- a/kore/src/Kore/Internal/TermLike/Renaming.hs +++ b/kore/src/Kore/Internal/TermLike/Renaming.hs @@ -43,13 +43,14 @@ renameFreeVariables :: forall m variable1 variable2 . Ord variable1 => Monad m - => (ElementVariable variable1 -> m (ElementVariable variable2)) - -> (SetVariable variable1 -> m (SetVariable variable2)) + => AdjUnifiedVariable (variable1 -> m variable2) -> FreeVariables variable1 -> m (UnifiedVariableMap variable1 variable2) -renameFreeVariables trElemVar trSetVar = +renameFreeVariables adj = Monad.foldM worker mempty . FreeVariables.toSet where + trElemVar = sequenceA . (<*>) (elemVar adj) + trSetVar = sequenceA . (<*>) (setVar adj) worker renaming = \case ElemVar elemVar -> diff --git a/kore/src/Kore/Internal/TermLike/TermLike.hs b/kore/src/Kore/Internal/TermLike/TermLike.hs index 1aa1286b5c..3c088a4ebf 100644 --- a/kore/src/Kore/Internal/TermLike/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike/TermLike.hs @@ -59,6 +59,9 @@ import Data.Functor.Identity ( Identity (..) ) import qualified Data.Generics.Product as Lens.Product +import Data.Generics.Wrapped + ( _Wrapped + ) import Data.List ( foldl' ) @@ -348,7 +351,7 @@ instance InternalVariable variable => Unparse (TermLike variable) where where freshVarTerm = externalizeFreshVariables - $ mapVariables (fmap toVariable) (fmap toVariable) term + $ mapVariables toUnifiedVariable term unparse2 term = case Recursive.project freshVarTerm of @@ -356,7 +359,7 @@ instance InternalVariable variable => Unparse (TermLike variable) where where freshVarTerm = externalizeFreshVariables - $ mapVariables (fmap toVariable) (fmap toVariable) term + $ mapVariables toUnifiedVariable term type instance Base (TermLike variable) = CofreeF (TermLikeF variable) (Attribute.Pattern variable) @@ -504,10 +507,7 @@ instance (FreshPartialOrd variable, SortedVariable variable) => From (TermLike Concrete) (TermLike variable) where - from = - mapVariables - (from @(ElementVariable Concrete)) - (from @(SetVariable Concrete)) + from = mapVariables fromConcreteUnifiedVariable {-# INLINE from #-} -- | The type of internal domain values. @@ -573,15 +573,13 @@ not injective! -} mapVariablesF - :: (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) + :: AdjUnifiedVariable (variable1 -> variable2) -> TermLikeF variable1 child -> TermLikeF variable2 child -mapVariablesF mapElemVar mapSetVar = - runIdentity . traverseVariablesF trElemVar trSetVar +mapVariablesF adj = + runIdentity . traverseVariablesF adj' where - trElemVar = Identity . mapElemVar - trSetVar = Identity . mapSetVar + adj' = (\f x -> Identity (f x)) <$> adj {- | Use the provided traversal to replace all variables in a 'TermLikeF' head. @@ -591,11 +589,10 @@ traversal is not injective! -} traverseVariablesF :: Applicative f - => (ElementVariable variable1 -> f (ElementVariable variable2)) - -> (SetVariable variable1 -> f (SetVariable variable2)) + => AdjUnifiedVariable (variable1 -> f variable2) -> TermLikeF variable1 child -> f (TermLikeF variable2 child) -traverseVariablesF trElemVar trSetVar = +traverseVariablesF adj = \case -- Non-trivial cases ExistsF any0 -> ExistsF <$> traverseVariablesExists any0 @@ -629,8 +626,10 @@ traverseVariablesF trElemVar trSetVar = SignednessF signedness -> pure (SignednessF signedness) InjF inj -> pure (InjF inj) where + trElemVar = sequenceA . (<*>) (elemVar adj) + trSetVar = sequenceA . (<*>) (setVar adj) traverseConstVariable (Const variable) = - Const <$> traverseUnifiedVariable trElemVar trSetVar variable + Const <$> traverseUnifiedVariable adj variable traverseVariablesExists Exists { existsSort, existsVariable, existsChild } = Exists existsSort <$> trElemVar existsVariable @@ -662,21 +661,21 @@ See also: 'traverseVariables' mapVariables :: forall variable1 variable2 . (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2) - => (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) -> TermLike variable1 -> TermLike variable2 -mapVariables mapElemVar mapSetVar termLike = +mapVariables adj termLike = Recursive.unfold worker (Env.env freeVariables0 termLike) where - trElemVar = Identity . mapElemVar - trSetVar = Identity . mapSetVar + adj' = (\f x -> Identity (f x)) <$> adj + trElemVar + :: ElementVariable variable1 + -> Identity (ElementVariable variable2) + trElemVar = sequenceA . (<*>) (elemVar adj') + trSetVar = sequenceA . (<*>) (setVar adj') Identity freeVariables0 = - renameFreeVariables - trElemVar - trSetVar - (freeVariables termLike) + renameFreeVariables adj' (freeVariables termLike) mapExists avoiding = sequenceAdjunct $ existsBinder $ renameElementBinder trElemVar avoiding @@ -693,8 +692,14 @@ mapVariables mapElemVar mapSetVar termLike = renameAttrs renaming = Attribute.mapVariables + AdjUnifiedVariable + { elemVar = + (ElementVariable . Lens.over _Wrapped) (askElementVariable' . Env.env renaming) + , setVar = + (SetVariable . Lens.over _Wrapped) (askSetVariable' . Env.env renaming) + } worker :: Renaming variable1 variable2 (TermLike variable1) @@ -721,8 +726,7 @@ mapVariables mapElemVar mapSetVar termLike = -- mapVariablesF will not actually call the mapping -- function because all the cases with variables are -- handled above. - mapVariablesF mapElemVar mapSetVar - $ Env.env renaming <$> termLikeF + mapVariablesF adj $ Env.env renaming <$> termLikeF in attrs' :< termLikeF' {- | Use the provided traversal to replace all variables in a 'TermLike'. @@ -739,14 +743,15 @@ traverseVariables :: forall variable1 variable2 m . (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2) => Monad m - => (ElementVariable variable1 -> m (ElementVariable variable2)) - -> (SetVariable variable1 -> m (SetVariable variable2)) + => AdjUnifiedVariable (variable1 -> m variable2) -> TermLike variable1 -> m (TermLike variable2) -traverseVariables trElemVar trSetVar termLike = - renameFreeVariables trElemVar trSetVar (freeVariables termLike) +traverseVariables adj termLike = + renameFreeVariables adj (freeVariables termLike) >>= Reader.runReaderT (Recursive.fold worker termLike) where + trElemVar = sequenceA . (<*>) (elemVar adj) + trSetVar = sequenceA . (<*>) (setVar adj) traverseExists avoiding = existsBinder (renameElementBinder trElemVar avoiding) traverseForall avoiding = @@ -756,17 +761,19 @@ traverseVariables trElemVar trSetVar termLike = traverseNu avoiding = nuBinder (renameSetBinder trSetVar avoiding) + askVariable = + AdjUnifiedVariable + { elemVar = ElementVariable (_Wrapped askElementVariable) + , setVar = SetVariable (_Wrapped askSetVariable) + } + worker :: Base (TermLike variable1) (RenamingT variable1 variable2 m (TermLike variable2)) -> RenamingT variable1 variable2 m (TermLike variable2) worker (attrs :< termLikeF) = do - attrs' <- - Attribute.traverseVariables - askElementVariable - askSetVariable - attrs + attrs' <- Attribute.traverseVariables askVariable attrs let avoiding = FreeVariables.toSet $ freeVariables attrs' termLikeF' <- case termLikeF of VariableF (Const unifiedVariable) -> do @@ -780,7 +787,7 @@ traverseVariables trElemVar trSetVar termLike = sequence termLikeF >>= -- traverseVariablesF will not actually call the traversals -- because all the cases with variables are handled above. - traverseVariablesF askElementVariable askSetVariable + traverseVariablesF askVariable (pure . Recursive.embed) (attrs' :< termLikeF') {- | Transform a 'sequence'-like function into its dual with an 'Adjunction'. @@ -952,6 +959,12 @@ externalizeFreshVariables termLike = $ fromMaybe setVariable . lookupRenamedSetVariable setVariable + lookupVariable = + AdjUnifiedVariable + { elemVar = ElementVariable (_Wrapped lookupElementVariable) + , setVar = SetVariable (_Wrapped lookupSetVariable) + } + {- | Externalize a variable safely. The variable's counter is incremented until its externalized form is unique @@ -1006,11 +1019,7 @@ externalizeFreshVariables termLike = (UnifiedVariableMap Variable Variable) (TermLike Variable) externalizeFreshVariablesWorker (attrs :< patt) = do - attrs' <- - Attribute.traverseVariables - lookupElementVariable - lookupSetVariable - attrs + attrs' <- Attribute.traverseVariables lookupVariable attrs let freeVariables' = Attribute.freeVariables attrs' patt' <- case patt of @@ -1066,12 +1075,7 @@ externalizeFreshVariables termLike = , nuChild = nuChild' } return (NuF nu') - _ -> - traverseVariablesF - lookupElementVariable - lookupSetVariable - patt - >>= sequence + _ -> traverseVariablesF lookupVariable patt >>= sequence (return . Recursive.embed) (attrs' :< patt') updateCallStack diff --git a/kore/src/Kore/Log/DebugAppliedRewriteRules.hs b/kore/src/Kore/Log/DebugAppliedRewriteRules.hs index 0a420914ed..2819997978 100644 --- a/kore/src/Kore/Log/DebugAppliedRewriteRules.hs +++ b/kore/src/Kore/Log/DebugAppliedRewriteRules.hs @@ -27,7 +27,6 @@ import Kore.Internal.Pattern import qualified Kore.Internal.TermLike as TermLike import Kore.Internal.Variable ( Variable (..) - , toVariable ) import Kore.Rewriting.RewritingVariable import Kore.Step.RulePattern @@ -41,6 +40,7 @@ import Kore.Step.Step import Kore.Unparser ( unparse ) +import Kore.Variables.UnifiedVariable import Log import Pretty ( Pretty (..) @@ -93,7 +93,4 @@ debugAppliedRewriteRules initial rules = appliedRewriteRules = coerce (mapConditionalVariables mapRuleVariables <$> rules) mapConditionalVariables mapTermVariables = - Conditional.mapVariables - mapTermVariables - (fmap toVariable) - (fmap toVariable) + Conditional.mapVariables mapTermVariables toUnifiedVariable diff --git a/kore/src/Kore/Log/ErrorRewritesInstantiation.hs b/kore/src/Kore/Log/ErrorRewritesInstantiation.hs index bead6941f8..b7ac4051d1 100644 --- a/kore/src/Kore/Log/ErrorRewritesInstantiation.hs +++ b/kore/src/Kore/Log/ErrorRewritesInstantiation.hs @@ -45,7 +45,6 @@ import qualified Kore.Internal.Pattern as Pattern import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.Variable ( InternalVariable - , toVariable ) import Kore.Rewriting.RewritingVariable import Kore.Step.RulePattern @@ -62,9 +61,6 @@ import Kore.Unparser ( unparse ) import Kore.Variables.UnifiedVariable - ( UnifiedVariable - , foldMapVariable - ) import Log import Pretty ( Pretty @@ -155,7 +151,7 @@ errorRewritesInstantiation configuration' unificationError = , errorCallStack = callStack } where - mapVariables = Pattern.mapVariables (fmap toVariable) (fmap toVariable) + mapVariables = Pattern.mapVariables toUnifiedVariable configuration = mkRewritingPattern $ mapVariables configuration' {- | Check that the final substitution covers the applied rule appropriately. diff --git a/kore/src/Kore/Log/InfoAttemptUnification.hs b/kore/src/Kore/Log/InfoAttemptUnification.hs index a6c2343caa..4746ac0171 100644 --- a/kore/src/Kore/Log/InfoAttemptUnification.hs +++ b/kore/src/Kore/Log/InfoAttemptUnification.hs @@ -18,12 +18,12 @@ import Kore.Internal.TermLike ( InternalVariable , TermLike , Variable - , toVariable ) import qualified Kore.Internal.TermLike as TermLike import Kore.Unparser ( unparse ) +import Kore.Variables.UnifiedVariable import Log import Pretty ( Pretty @@ -63,6 +63,6 @@ infoAttemptUnification infoAttemptUnification term1' term2' = logWhile InfoAttemptUnification { term1, term2 } where - mapVariables = TermLike.mapVariables (fmap toVariable) (fmap toVariable) + mapVariables = TermLike.mapVariables toUnifiedVariable term1 = mapVariables term1' term2 = mapVariables term2' diff --git a/kore/src/Kore/Log/WarnBottomTotalFunction.hs b/kore/src/Kore/Log/WarnBottomTotalFunction.hs index b193b25275..f74485b3c3 100644 --- a/kore/src/Kore/Log/WarnBottomTotalFunction.hs +++ b/kore/src/Kore/Log/WarnBottomTotalFunction.hs @@ -21,6 +21,7 @@ import Kore.Step.Simplification.Simplify import Kore.Unparser ( unparse ) +import Kore.Variables.UnifiedVariable import Pretty ( Pretty ) @@ -59,5 +60,5 @@ warnBottomTotalFunction => InternalVariable variable => TermLike variable -> logger () -warnBottomTotalFunction (mapVariables (fmap toVariable) (fmap toVariable) -> term) = +warnBottomTotalFunction (mapVariables toUnifiedVariable -> term) = logEntry WarnBottomTotalFunction { term } diff --git a/kore/src/Kore/Log/WarnDecidePredicateUnknown.hs b/kore/src/Kore/Log/WarnDecidePredicateUnknown.hs index a33982ad47..f6a84b80c1 100644 --- a/kore/src/Kore/Log/WarnDecidePredicateUnknown.hs +++ b/kore/src/Kore/Log/WarnDecidePredicateUnknown.hs @@ -21,6 +21,7 @@ import Kore.Internal.Predicate import qualified Kore.Internal.Predicate as Predicate import Kore.Internal.Variable import Kore.Unparser +import Kore.Variables.UnifiedVariable import Log import Pretty ( Pretty (..) @@ -56,8 +57,4 @@ warnDecidePredicateUnknown warnDecidePredicateUnknown predicates' = logEntry WarnDecidePredicateUnknown { predicates } where - predicates = - Predicate.mapVariables - (fmap toVariable) - (fmap toVariable) - <$> predicates' + predicates = Predicate.mapVariables toUnifiedVariable <$> predicates' diff --git a/kore/src/Kore/Rewriting/RewritingVariable.hs b/kore/src/Kore/Rewriting/RewritingVariable.hs index c68451b25b..2fa1b67c52 100644 --- a/kore/src/Kore/Rewriting/RewritingVariable.hs +++ b/kore/src/Kore/Rewriting/RewritingVariable.hs @@ -52,9 +52,6 @@ import Kore.Rewriting.UnifyingRule import Kore.Unparser import Kore.Variables.Fresh import Kore.Variables.UnifiedVariable - ( UnifiedVariable (..) - , foldMapVariable - ) data RewritingVariable = ConfigVariable !Variable @@ -156,14 +153,6 @@ getUnifiedRuleVariable getUnifiedRuleVariable (ElemVar var) = ElemVar <$> traverse getRuleVariable var getUnifiedRuleVariable (SetVar var) = SetVar <$> traverse getRuleVariable var -getElementRewritingVariable - :: ElementVariable RewritingVariable -> ElementVariable Variable -getElementRewritingVariable = fmap (from @_ @Variable) - -getSetRewritingVariable - :: SetVariable RewritingVariable -> SetVariable Variable -getSetRewritingVariable = fmap (from @_ @Variable) - getPattern :: HasCallStack => Pattern RewritingVariable @@ -174,14 +163,11 @@ getPattern pattern' = where freeVars = freeVariables pattern' & FreeVariables.toList -getPatternAux - :: Pattern RewritingVariable - -> Pattern Variable -getPatternAux pattern' = - Pattern.mapVariables - getElementRewritingVariable - getSetRewritingVariable - pattern' +getRewritingVariable :: AdjUnifiedVariable (RewritingVariable -> Variable) +getRewritingVariable = pure (from @RewritingVariable @Variable) + +getPatternAux :: Pattern RewritingVariable -> Pattern Variable +getPatternAux = Pattern.mapVariables getRewritingVariable mkConfigVariable :: Variable -> RewritingVariable mkConfigVariable = ConfigVariable @@ -245,27 +231,20 @@ mkRewritingRule :: UnifyingRule rule => rule Variable -> rule RewritingVariable -mkRewritingRule = mapRuleVariables (fmap RuleVariable) (fmap RuleVariable) +mkRewritingRule = mapRuleVariables (pure RuleVariable) {- | Unwrap the variables in a 'RulePattern'. Inverse of 'targetRuleVariables'. -} unRewritingRule :: UnifyingRule rule => rule RewritingVariable -> rule Variable -unRewritingRule = - mapRuleVariables getElementRewritingVariable getSetRewritingVariable +unRewritingRule = mapRuleVariables getRewritingVariable -- |Renames configuration variables to distinguish them from those in the rule. mkRewritingPattern :: Pattern Variable -> Pattern RewritingVariable -mkRewritingPattern = - Pattern.mapVariables - (fmap ConfigVariable) - (fmap ConfigVariable) +mkRewritingPattern = Pattern.mapVariables (pure ConfigVariable) getRemainderPredicate :: Predicate RewritingVariable -> Predicate Variable getRemainderPredicate predicate = - Predicate.mapVariables - getElementRewritingVariable - getSetRewritingVariable - predicate + Predicate.mapVariables getRewritingVariable predicate & assert (all isUnifiedConfigVariable freeVars) where freeVars = freeVariables predicate & FreeVariables.toList diff --git a/kore/src/Kore/Rewriting/UnifyingRule.hs b/kore/src/Kore/Rewriting/UnifyingRule.hs index 8ae8645613..1f6cc39097 100644 --- a/kore/src/Kore/Rewriting/UnifyingRule.hs +++ b/kore/src/Kore/Rewriting/UnifyingRule.hs @@ -24,9 +24,7 @@ import Kore.Internal.Predicate ( Predicate ) import Kore.Internal.TermLike - ( ElementVariable - , InternalVariable - , SetVariable + ( InternalVariable , SortedVariable , TermLike ) @@ -35,8 +33,6 @@ import Kore.Variables.Fresh ( FreshPartialOrd ) import Kore.Variables.UnifiedVariable - ( UnifiedVariable - ) import qualified Pretty type Renaming variable = @@ -101,8 +97,7 @@ class UnifyingRule rule where -} mapRuleVariables :: (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2) - => (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) + => AdjUnifiedVariable (variable1 -> variable2) -> rule variable1 -> rule variable2 diff --git a/kore/src/Kore/Step/Axiom/EvaluationStrategy.hs b/kore/src/Kore/Step/Axiom/EvaluationStrategy.hs index 3970caa2ef..585c1c99be 100644 --- a/kore/src/Kore/Step/Axiom/EvaluationStrategy.hs +++ b/kore/src/Kore/Step/Axiom/EvaluationStrategy.hs @@ -54,6 +54,7 @@ import Kore.Unparser ( unparse ) import qualified Kore.Variables.Target as Target +import Kore.Variables.UnifiedVariable import qualified Pretty {-|Describes whether simplifiers are allowed to return multiple results or not. @@ -75,20 +76,11 @@ definitionEvaluation -> BuiltinAndAxiomSimplifier definitionEvaluation equations = BuiltinAndAxiomSimplifier $ \term condition -> do - let equations' = - Equation.mapVariables - (fmap $ from @Variable) - (fmap $ from @Variable) - <$> equations - term' = - TermLike.mapVariables - Target.mkElementNonTarget - Target.mkSetNonTarget - term + let equations' = Equation.mapVariables fromUnifiedVariable <$> equations + term' = TermLike.mapVariables Target.mkUnifiedNonTarget term condition' = SideCondition.mapVariables - Target.mkElementNonTarget - Target.mkSetNonTarget + Target.mkUnifiedNonTarget condition let -- Attempt an equation, pairing it with its result, if applicable. attemptEquation equation = @@ -122,20 +114,11 @@ simplificationEvaluation -> BuiltinAndAxiomSimplifier simplificationEvaluation equation = BuiltinAndAxiomSimplifier $ \term condition -> do - let equation' = - Equation.mapVariables - (fmap $ from @Variable) - (fmap $ from @Variable) - equation - term' = - TermLike.mapVariables - Target.mkElementNonTarget - Target.mkSetNonTarget - term + let equation' = Equation.mapVariables fromUnifiedVariable equation + term' = TermLike.mapVariables Target.mkUnifiedNonTarget term condition' = SideCondition.mapVariables - Target.mkElementNonTarget - Target.mkSetNonTarget + Target.mkUnifiedNonTarget condition result <- Equation.attemptEquation condition' term' equation' let apply = Equation.applyEquation condition equation' diff --git a/kore/src/Kore/Step/RulePattern.hs b/kore/src/Kore/Step/RulePattern.hs index 8b36a09028..ac98e7ff0c 100644 --- a/kore/src/Kore/Step/RulePattern.hs +++ b/kore/src/Kore/Step/RulePattern.hs @@ -133,8 +133,6 @@ import Kore.Unparser ) import Kore.Variables.Fresh import Kore.Variables.UnifiedVariable - ( UnifiedVariable (..) - ) import qualified Kore.Verified as Verified import Pretty ( Pretty @@ -892,18 +890,18 @@ instance UnifyingRule RulePattern where exVars = Set.fromList $ ElemVar <$> existentials rhs originalFreeVariables = freeVariables rule1 & FreeVariables.toSet - mapRuleVariables mapElemVar mapSetVar rule1@(RulePattern _ _ _ _ _) = + mapRuleVariables adj rule1@(RulePattern _ _ _ _ _) = rule1 { left = mapTermLikeVariables left , antiLeft = mapTermLikeVariables <$> antiLeft , requires = mapPredicateVariables requires , rhs = RHS - { existentials = mapElemVar <$> existentials + { existentials = (<*>) (elemVar adj) <$> existentials , right = mapTermLikeVariables right , ensures = mapPredicateVariables ensures } , attributes = - Attribute.mapAxiomVariables mapElemVar mapSetVar attributes + Attribute.mapAxiomVariables adj attributes } where RulePattern @@ -911,8 +909,8 @@ instance UnifyingRule RulePattern where , rhs = RHS { existentials, right, ensures } , attributes } = rule1 - mapTermLikeVariables = TermLike.mapVariables mapElemVar mapSetVar - mapPredicateVariables = Predicate.mapVariables mapElemVar mapSetVar + mapTermLikeVariables = TermLike.mapVariables adj + mapPredicateVariables = Predicate.mapVariables adj instance UnifyingRule RewriteRule where matchingPattern (RewriteRule rule) = matchingPattern rule @@ -925,8 +923,8 @@ instance UnifyingRule RewriteRule where RewriteRule <$> refreshRule avoiding rule {-# INLINE refreshRule #-} - mapRuleVariables mapElemVar mapSetVar (RewriteRule rule) = - RewriteRule (mapRuleVariables mapElemVar mapSetVar rule) + mapRuleVariables mapping (RewriteRule rule) = + RewriteRule (mapRuleVariables mapping rule) {-# INLINE mapRuleVariables #-} lhsEqualsRhs diff --git a/kore/src/Kore/Step/Simplification/ExpandAlias.hs b/kore/src/Kore/Step/Simplification/ExpandAlias.hs index 37a1229901..304cf28b5d 100644 --- a/kore/src/Kore/Step/Simplification/ExpandAlias.hs +++ b/kore/src/Kore/Step/Simplification/ExpandAlias.hs @@ -32,14 +32,12 @@ import Kore.Internal.TermLike , mapVariables , substitute ) -import Kore.Syntax.Variable - ( fromVariable - ) import Kore.Unification.Unify ( MonadUnify ) import Kore.Variables.UnifiedVariable - ( mapUnifiedVariable + ( fromUnifiedVariable + , mapUnifiedVariable ) expandAlias @@ -78,9 +76,7 @@ substituteInAlias substituteInAlias Alias { aliasLeft, aliasRight } children = assert (length aliasLeft == length children) $ substitute substitutionMap - $ mapVariables (fmap fromVariable) (fmap fromVariable) aliasRight + $ mapVariables fromUnifiedVariable aliasRight where - aliasLeft' = - mapUnifiedVariable (fmap fromVariable) (fmap fromVariable) <$> aliasLeft - substitutionMap = - Map.fromList $ zip aliasLeft' children + aliasLeft' = mapUnifiedVariable fromUnifiedVariable <$> aliasLeft + substitutionMap = Map.fromList $ zip aliasLeft' children diff --git a/kore/src/Kore/Step/Simplification/TermLike.hs b/kore/src/Kore/Step/Simplification/TermLike.hs index 0732840b51..e747f5f7d3 100644 --- a/kore/src/Kore/Step/Simplification/TermLike.hs +++ b/kore/src/Kore/Step/Simplification/TermLike.hs @@ -14,6 +14,9 @@ import Prelude.Kore import qualified Control.Lens.Combinators as Lens import Data.Functor.Const import qualified Data.Functor.Foldable as Recursive +import Data.Generics.Wrapped + ( _Wrapped + ) import qualified Branch as BranchT ( gather @@ -146,11 +149,10 @@ import Kore.Unparser import qualified Kore.Variables.Binding as Binding import Kore.Variables.Target ( Target (..) - , mkSetNonTarget , targetIfEqual - , unTargetElement - , unTargetSet + , unTargetUnified ) +import Kore.Variables.UnifiedVariable import qualified Pretty -- TODO(virgil): Add a Simplifiable class and make all pattern types @@ -404,7 +406,7 @@ simplifyInternal term sideCondition = do (targetSideCondition sideCondition) (targetSimplifiedChildren simplifiedChildren) let unTargetedResults = - Pattern.mapVariables unTargetElement unTargetSet + Pattern.mapVariables unTargetUnified <$> targetedResults return unTargetedResults where @@ -414,8 +416,12 @@ simplifyInternal term sideCondition = do -> SideCondition (Target variable) targetSideCondition = SideCondition.mapVariables - (targetIfEqual . ElementVariable $ boundVar) - mkSetNonTarget + AdjUnifiedVariable + { elemVar = + (ElementVariable . Lens.over _Wrapped) + (targetIfEqual (ElementVariable boundVar)) + , setVar = SetVariable NonTarget + } targetSimplifiedChildren :: TermLike.Exists TermLike.Sort diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index c1aa8e55ed..a5b899c903 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -268,7 +268,7 @@ toConfigurationVariablesCondition => SideCondition variable -> SideCondition (Target variable) toConfigurationVariablesCondition = - SideCondition.mapVariables Target.mkElementNonTarget Target.mkSetNonTarget + SideCondition.mapVariables Target.mkUnifiedNonTarget {- | Apply the remainder predicate to the given initial configuration. diff --git a/kore/src/Kore/Syntax/ElementVariable.hs b/kore/src/Kore/Syntax/ElementVariable.hs index 6572ac00a2..24c1f1056c 100644 --- a/kore/src/Kore/Syntax/ElementVariable.hs +++ b/kore/src/Kore/Syntax/ElementVariable.hs @@ -28,7 +28,17 @@ import Kore.Unparser -- | Element (singleton) Kore variables newtype ElementVariable variable = ElementVariable { getElementVariable :: variable } - deriving (Eq, GHC.Generic, Ord, Show, Functor, Foldable, Traversable) + deriving (Eq, Ord, Show) + deriving (Functor) + deriving (Foldable, Traversable) + deriving (GHC.Generic) + +instance Applicative ElementVariable where + pure = ElementVariable + {-# INLINE pure #-} + + (<*>) (ElementVariable f) (ElementVariable a) = ElementVariable (f a) + {-# INLINE (<*>) #-} instance Hashable variable => Hashable (ElementVariable variable) diff --git a/kore/src/Kore/Syntax/Pattern.hs b/kore/src/Kore/Syntax/Pattern.hs index c870062636..a8fa9a837c 100644 --- a/kore/src/Kore/Syntax/Pattern.hs +++ b/kore/src/Kore/Syntax/Pattern.hs @@ -51,18 +51,17 @@ import qualified GHC.Generics as GHC import qualified Kore.Attribute.Null as Attribute import Kore.Debug -import Kore.Syntax.ElementVariable import Kore.Syntax.PatternF ( Const (..) , PatternF (..) ) import qualified Kore.Syntax.PatternF as PatternF -import Kore.Syntax.SetVariable import Kore.Syntax.Variable import Kore.TopBottom ( TopBottom (..) ) import Kore.Unparser +import Kore.Variables.UnifiedVariable import qualified Pretty import qualified SQL @@ -287,16 +286,15 @@ See also: 'mapVariables' -} traverseVariables - :: forall m variable1 variable2 annotation. - Monad m - => (ElementVariable variable1 -> m (ElementVariable variable2)) - -> (SetVariable variable1 -> m (SetVariable variable2)) + :: forall m variable1 variable2 annotation + . Monad m + => AdjUnifiedVariable (variable1 -> m variable2) -> Pattern variable1 annotation -> m (Pattern variable2 annotation) -traverseVariables trElemVar trSetVar = +traverseVariables morphism = Recursive.fold traverseVariablesWorker where - traverseF = PatternF.traverseVariables trElemVar trSetVar + traverseF = PatternF.traverseVariables morphism traverseVariablesWorker :: Base @@ -318,14 +316,13 @@ See also: 'traverseVariables' -} mapVariables - :: (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) + :: AdjUnifiedVariable (variable1 -> variable2) -> Pattern variable1 annotation -> Pattern variable2 annotation -mapVariables mapElemVar mapSetVar = +mapVariables morphism = Recursive.ana (mapVariablesWorker . Recursive.project) where - mapF = PatternF.mapVariables mapElemVar mapSetVar + mapF = PatternF.mapVariables morphism mapVariablesWorker (a :< pat) = a :< mapF pat {- | Construct a 'ConcretePattern' from a 'Pattern'. @@ -342,8 +339,7 @@ deciding if the result is @Nothing@ or @Just _@. asConcretePattern :: Pattern variable annotation -> Maybe (Pattern Concrete annotation) -asConcretePattern = - traverseVariables (\case { _ -> Nothing }) (\case { _ -> Nothing }) +asConcretePattern = traverseVariables asConcreteUnifiedVariable isConcrete :: Pattern variable annotation -> Bool isConcrete = isJust . asConcretePattern @@ -360,4 +356,4 @@ composes with other tree transformations without allocating intermediates. fromConcretePattern :: Pattern Concrete annotation -> Pattern variable annotation -fromConcretePattern = mapVariables (\case {}) (\case {}) +fromConcretePattern = mapVariables fromConcreteUnifiedVariable diff --git a/kore/src/Kore/Syntax/PatternF.hs b/kore/src/Kore/Syntax/PatternF.hs index a8c35420b3..574d4c28e1 100644 --- a/kore/src/Kore/Syntax/PatternF.hs +++ b/kore/src/Kore/Syntax/PatternF.hs @@ -37,7 +37,6 @@ import Kore.Syntax.Application import Kore.Syntax.Bottom import Kore.Syntax.Ceil import Kore.Syntax.DomainValue -import Kore.Syntax.ElementVariable import Kore.Syntax.Equals import Kore.Syntax.Exists import Kore.Syntax.Floor @@ -52,7 +51,6 @@ import Kore.Syntax.Not import Kore.Syntax.Nu import Kore.Syntax.Or import Kore.Syntax.Rewrites -import Kore.Syntax.SetVariable import Kore.Syntax.StringLiteral import Kore.Syntax.Top import Kore.Syntax.Variable @@ -117,13 +115,13 @@ not injective! -} mapVariables - :: (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) + :: AdjUnifiedVariable (variable1 -> variable2) -> PatternF variable1 child -> PatternF variable2 child -mapVariables mapElemVar mapSetVar = - runIdentity - . traverseVariables (Identity . mapElemVar) (Identity . mapSetVar) +mapVariables adj = + runIdentity . traverseVariables adj' + where + adj' = (Identity .) <$> adj {-# INLINE mapVariables #-} {- | Use the provided traversal to replace all variables in a 'PatternF' head. @@ -134,11 +132,9 @@ traversal is not injective! -} traverseVariables :: Applicative f - => (ElementVariable variable1 -> f (ElementVariable variable2)) - -> (SetVariable variable1 -> f (SetVariable variable2)) - -> PatternF variable1 child - -> f (PatternF variable2 child) -traverseVariables trElemVar trSetVar = + => AdjUnifiedVariable (variable1 -> f variable2) + -> PatternF variable1 child -> f (PatternF variable2 child) +traverseVariables adj = \case -- Non-trivial cases ExistsF any0 -> ExistsF <$> traverseVariablesExists any0 @@ -165,9 +161,10 @@ traverseVariables trElemVar trSetVar = TopF topP -> pure (TopF topP) InhabitantF s -> pure (InhabitantF s) where + trElemVar = sequenceA . (<*>) (elemVar adj) + trSetVar = sequenceA . (<*>) (setVar adj) traverseVariable (Const variable) = - VariableF . Const - <$> traverseUnifiedVariable trElemVar trSetVar variable + VariableF . Const <$> traverseUnifiedVariable adj variable traverseVariablesExists Exists { existsSort, existsVariable, existsChild } = Exists existsSort <$> trElemVar existsVariable diff --git a/kore/src/Kore/Syntax/SetVariable.hs b/kore/src/Kore/Syntax/SetVariable.hs index cd864ca36f..f3ccc2ef53 100644 --- a/kore/src/Kore/Syntax/SetVariable.hs +++ b/kore/src/Kore/Syntax/SetVariable.hs @@ -28,7 +28,17 @@ import Kore.Unparser -- | Applicative-Kore set variables newtype SetVariable variable = SetVariable { getSetVariable :: variable } - deriving (Eq, GHC.Generic, Ord, Show, Functor, Foldable, Traversable) + deriving (Eq, Ord, Show) + deriving (Functor) + deriving (Foldable, Traversable) + deriving (GHC.Generic) + +instance Applicative SetVariable where + pure = SetVariable + {-# INLINE pure #-} + + (<*>) (SetVariable f) (SetVariable a) = SetVariable (f a) + {-# INLINE (<*>) #-} instance Hashable variable => Hashable (SetVariable variable) diff --git a/kore/src/Kore/Unification/Error.hs b/kore/src/Kore/Unification/Error.hs index 9232061728..8bb119f9a1 100644 --- a/kore/src/Kore/Unification/Error.hs +++ b/kore/src/Kore/Unification/Error.hs @@ -27,6 +27,7 @@ import Kore.Sort import Kore.Syntax.Application import Kore.Syntax.Variable import Kore.Unparser +import Kore.Variables.UnifiedVariable import Pretty ( Pretty ) @@ -54,7 +55,7 @@ unsupportedPatterns => String -> TermLike variable -> TermLike variable -> UnificationError unsupportedPatterns message = on (UnsupportedPatterns message) - $ mapVariables (fmap toVariable) (fmap toVariable) + $ mapVariables toUnifiedVariable instance Pretty UnificationError where pretty UnsupportedPatterns { message, first, second } = diff --git a/kore/src/Kore/Variables/Target.hs b/kore/src/Kore/Variables/Target.hs index 2b1c3e57c2..816a922f66 100644 --- a/kore/src/Kore/Variables/Target.hs +++ b/kore/src/Kore/Variables/Target.hs @@ -11,11 +11,14 @@ module Kore.Variables.Target , unTarget , unTargetElement , unTargetSet + , unTargetUnified , mkElementTarget , mkSetTarget + , mkUnifiedTarget , isTarget , mkElementNonTarget , mkSetNonTarget + , mkUnifiedNonTarget , isNonTarget , targetIfEqual ) where @@ -38,9 +41,6 @@ import Kore.Variables.Fresh , FreshVariable (..) ) import Kore.Variables.UnifiedVariable - ( ElementVariable - , SetVariable - ) {- | Distinguish variables by their source. @@ -96,6 +96,9 @@ unTargetElement = fmap unTarget unTargetSet :: SetVariable (Target variable) -> SetVariable variable unTargetSet = fmap unTarget +unTargetUnified :: AdjUnifiedVariable (Target variable -> variable) +unTargetUnified = pure unTarget + mkElementTarget :: ElementVariable variable -> ElementVariable (Target variable) @@ -106,6 +109,9 @@ mkSetTarget -> SetVariable (Target variable) mkSetTarget = fmap Target +mkUnifiedTarget :: AdjUnifiedVariable (variable -> Target variable) +mkUnifiedTarget = pure Target + isTarget :: Target variable -> Bool isTarget (Target _) = True isTarget (NonTarget _) = False @@ -120,6 +126,9 @@ mkSetNonTarget -> SetVariable (Target variable) mkSetNonTarget = fmap NonTarget +mkUnifiedNonTarget :: AdjUnifiedVariable (variable -> Target variable) +mkUnifiedNonTarget = pure NonTarget + isNonTarget :: Target variable -> Bool isNonTarget = not . isTarget diff --git a/kore/src/Kore/Variables/UnifiedVariable.hs b/kore/src/Kore/Variables/UnifiedVariable.hs index 805f43a56d..ccb9ac55ce 100644 --- a/kore/src/Kore/Variables/UnifiedVariable.hs +++ b/kore/src/Kore/Variables/UnifiedVariable.hs @@ -15,7 +15,13 @@ module Kore.Variables.UnifiedVariable , unifiedVariableSort , refreshElementVariable , refreshSetVariable + -- * AdjUnifiedVariable , MapVariables + , AdjUnifiedVariable (..) + , asConcreteUnifiedVariable + , fromConcreteUnifiedVariable + , toUnifiedVariable + , fromUnifiedVariable , mapUnifiedVariable , traverseUnifiedVariable -- * UnifiedVariableMap @@ -23,10 +29,15 @@ module Kore.Variables.UnifiedVariable , UnifiedVariableMap , renameElementVariable, renameSetVariable , lookupRenamedElementVariable, lookupRenamedSetVariable + -- * Re-exports + , Kleisli (..) ) where import Prelude.Kore +import Control.Arrow + ( Kleisli (..) + ) import Control.DeepSeq ( NFData ) @@ -207,28 +218,72 @@ refreshSetVariable avoiding = fmap expectSetVar . refreshVariable avoiding . SetVar type MapVariables variable1 variable2 term1 term2 = - (ElementVariable variable1 -> ElementVariable variable2) - -> (SetVariable variable1 -> SetVariable variable2) - -> term1 -> term2 + AdjUnifiedVariable (variable1 -> variable2) -> term1 -> term2 + +{- | 'AdjUnifiedVariable' is the right adjoint of 'UnifiedVariable'. + +Where 'UnifiedVariable' is a sum type, 'AdjUnifiedVariable' is a product type +with one field for each constructor. A 'UnifiedVariable' can be used to select +one field from the 'AdjUnifiedVariable'. + +In practice, 'AdjUnifiedVariable' are used to represent morphisms that transform +'ElementVariable' and 'SetVariable' separately while preserving each kind of +variable; that is, the type @'AdjUnifiedVariable' (a -> b)@ is a restriction of +the type @'UnifiedVariable' a -> 'UnifiedVariable' b@ + + -} +data AdjUnifiedVariable a = + AdjUnifiedVariable + { elemVar :: ElementVariable a + , setVar :: SetVariable a + } + deriving (Functor) + +instance Applicative AdjUnifiedVariable where + pure a = AdjUnifiedVariable (ElementVariable a) (SetVariable a) + {-# INLINE pure #-} + + (<*>) fs as = + AdjUnifiedVariable + { elemVar = elemVar fs <*> elemVar as + , setVar = setVar fs <*> setVar as + } + {-# INLINE (<*>) #-} + +asConcreteUnifiedVariable :: AdjUnifiedVariable (variable -> Maybe Concrete) +asConcreteUnifiedVariable = pure (const Nothing) + +fromConcreteUnifiedVariable :: AdjUnifiedVariable (Concrete -> variable) +fromConcreteUnifiedVariable = pure (\case {}) mapUnifiedVariable - :: MapVariables variable1 variable2 - (UnifiedVariable variable1) - (UnifiedVariable variable2) -mapUnifiedVariable mapElemVar mapSetVar = + :: AdjUnifiedVariable (variable1 -> variable2) + -> UnifiedVariable variable1 -> UnifiedVariable variable2 +mapUnifiedVariable AdjUnifiedVariable { elemVar, setVar } = \case - ElemVar elemVar -> ElemVar (mapElemVar elemVar) - SetVar setVar -> SetVar (mapSetVar setVar) + ElemVar elementVariable -> ElemVar $ elemVar <*> elementVariable + SetVar setVariable -> SetVar $ setVar <*> setVariable traverseUnifiedVariable - :: Functor f - => (ElementVariable variable1 -> f (ElementVariable variable2)) - -> (SetVariable variable1 -> f (SetVariable variable2)) + :: Applicative f + => AdjUnifiedVariable (variable1 -> f variable2) -> UnifiedVariable variable1 -> f (UnifiedVariable variable2) -traverseUnifiedVariable traverseElemVar traverseSetVar = +traverseUnifiedVariable AdjUnifiedVariable { elemVar, setVar } = \case - ElemVar elemVar -> ElemVar <$> traverseElemVar elemVar - SetVar setVar -> SetVar <$> traverseSetVar setVar + ElemVar elementVariable -> + ElemVar <$> sequenceA (elemVar <*> elementVariable) + SetVar setVariable -> + SetVar <$> sequenceA (setVar <*> setVariable) + +toUnifiedVariable + :: VariableName variable + => AdjUnifiedVariable (variable -> Variable) +toUnifiedVariable = pure toVariable + +fromUnifiedVariable + :: VariableName variable + => AdjUnifiedVariable (Variable -> variable) +fromUnifiedVariable = pure fromVariable type VariableMap meta variable1 variable2 = Map (meta variable1) (meta variable2) diff --git a/kore/test/Test/Kore/Equation/Application.hs b/kore/test/Test/Kore/Equation/Application.hs index a3d6950880..8cb838cf2f 100644 --- a/kore/test/Test/Kore/Equation/Application.hs +++ b/kore/test/Test/Kore/Equation/Application.hs @@ -76,15 +76,10 @@ attemptEquation sideCondition termLike equation = where sideCondition' = SideCondition.mapVariables - Target.mkElementNonTarget - Target.mkSetNonTarget + Target.mkUnifiedNonTarget sideCondition - termLike' = - TermLike.mapVariables - Target.mkElementNonTarget - Target.mkSetNonTarget - termLike + termLike' = TermLike.mapVariables Target.mkUnifiedNonTarget termLike assertNotMatched :: AttemptEquationError Variable -> Assertion assertNotMatched (WhileMatch _) = return () diff --git a/kore/test/Test/Kore/Internal/Pattern.hs b/kore/test/Test/Kore/Internal/Pattern.hs index 2aa56783f1..05bf53e557 100644 --- a/kore/test/Test/Kore/Internal/Pattern.hs +++ b/kore/test/Test/Kore/Internal/Pattern.hs @@ -54,7 +54,7 @@ test_expandedPattern = $ Substitution.mkUnwrappedSubstitution [(ElemVar . ElementVariable $ mkW "4", war' "5")] } - (Pattern.mapVariables (fmap showVar) (fmap showVar) + (Pattern.mapVariables showUnifiedVar Conditional { term = var' 1 , predicate = makeEquals (var' 2) (var' 3) diff --git a/kore/test/Test/Kore/Internal/Substitution.hs b/kore/test/Test/Kore/Internal/Substitution.hs index 8d3ceaf0f3..267f88b067 100644 --- a/kore/test/Test/Kore/Internal/Substitution.hs +++ b/kore/test/Test/Kore/Internal/Substitution.hs @@ -136,19 +136,19 @@ mapVariablesTests = [ testCase "map id over empty is empty" $ assertEqual "" (wrap mempty) - . mapVariables id id $ emptySubst + . mapVariables (pure id) $ emptySubst , testCase "map id over wrap empty is normalized empty" $ assertEqual "" (wrap mempty) - . mapVariables id id $ wrap emptyRawSubst + . mapVariables (pure id) $ wrap emptyRawSubst , testCase "map id over singleton == id" $ assertEqual "" (wrap singletonSubst) - . mapVariables id id $ wrap singletonSubst + . mapVariables (pure id) $ wrap singletonSubst , testCase "map id over normalized singletonSubst" $ assertEqual "" (wrap singletonSubst) - . mapVariables id id $ unsafeWrapFromAssignments singletonSubst + . mapVariables (pure id) $ unsafeWrapFromAssignments singletonSubst ] isNormalizedTests :: TestTree diff --git a/kore/test/Test/Kore/Internal/TermLike.hs b/kore/test/Test/Kore/Internal/TermLike.hs index 006ccadfbc..2f4581c986 100644 --- a/kore/test/Test/Kore/Internal/TermLike.hs +++ b/kore/test/Test/Kore/Internal/TermLike.hs @@ -42,8 +42,6 @@ import Kore.Variables.Fresh ( refreshVariable ) import Kore.Variables.UnifiedVariable - ( UnifiedVariable (..) - ) import Test.Kore hiding ( symbolGen @@ -375,13 +373,19 @@ test_renaming = , testSet "\\nu" mkNu ] where - mapElementVariables' v = mapVariables (const v) id - mapSetVariables' v = mapVariables id (const v) + mapElementVariables' (getElementVariable -> v) = + mapVariables (pure id) { elemVar = ElementVariable (const v) } + mapSetVariables' (getSetVariable -> v) = + mapVariables (pure id) { setVar = SetVariable (const v) } - traverseElementVariables' v = - runIdentity . traverseVariables (const $ return v) pure - traverseSetVariables' v = - runIdentity . traverseVariables pure (const $ return v) + traverseElementVariables' (getElementVariable -> v) = + runIdentity + . traverseVariables (pure return) + { elemVar = ElementVariable (const $ return v) } + traverseSetVariables' (getSetVariable -> v) = + runIdentity + . traverseVariables (pure return) + { setVar = SetVariable (const $ return v) } doesNotCapture :: HasCallStack diff --git a/kore/test/Test/Kore/Step/Function/Integration.hs b/kore/test/Test/Kore/Step/Function/Integration.hs index 3931f0b88b..54cdc804c5 100644 --- a/kore/test/Test/Kore/Step/Function/Integration.hs +++ b/kore/test/Test/Kore/Step/Function/Integration.hs @@ -96,8 +96,6 @@ import Kore.Syntax.Definition hiding ) import Kore.Unparser import Kore.Variables.UnifiedVariable - ( UnifiedVariable (..) - ) import qualified Pretty import Test.Kore @@ -1330,11 +1328,10 @@ mapVariables => Pattern Variable -> Pattern variable mapVariables = - Pattern.mapVariables worker worker + Pattern.mapVariables (pure worker) where - worker :: Functor f => f Variable -> f variable - worker = fmap $ \v -> - fromVariable v { variableCounter = Just (Element 1) } + worker :: Variable -> variable + worker v = fromVariable v { variableCounter = Just (Element 1) } mockEvaluator :: Monad simplifier diff --git a/kore/test/Test/Kore/Step/Rule/Simplify.hs b/kore/test/Test/Kore/Step/Rule/Simplify.hs index fa81df3095..74eaffff58 100644 --- a/kore/test/Test/Kore/Step/Rule/Simplify.hs +++ b/kore/test/Test/Kore/Step/Rule/Simplify.hs @@ -64,8 +64,8 @@ import Kore.Step.Simplification.Simplify import qualified Kore.Step.SMT.Declaration.All as SMT.All import Kore.Syntax.Variable ( Variable - , fromVariable ) +import Kore.Variables.UnifiedVariable import qualified Test.Kore.Step.MockSymbols as Mock import Test.SMT @@ -332,15 +332,13 @@ test_simplifyClaimRule = :: InternalVariable variable => Predicate Variable -> Predicate variable - liftPredicate = - Predicate.mapVariables (fmap fromVariable) (fmap fromVariable) + liftPredicate = Predicate.mapVariables fromUnifiedVariable liftTermLike :: InternalVariable variable => TermLike Variable -> TermLike variable - liftTermLike = - TermLike.mapVariables (fmap fromVariable) (fmap fromVariable) + liftTermLike = TermLike.mapVariables fromUnifiedVariable liftReplacement :: InternalVariable variable diff --git a/kore/test/Test/Kore/Step/Simplification/Ceil.hs b/kore/test/Test/Kore/Step/Simplification/Ceil.hs index d65ad9c755..8107ffd15a 100644 --- a/kore/test/Test/Kore/Step/Simplification/Ceil.hs +++ b/kore/test/Test/Kore/Step/Simplification/Ceil.hs @@ -48,8 +48,6 @@ import qualified Kore.Step.Simplification.Simplify as AttemptedAxiom ( AttemptedAxiom (..) ) import Kore.Variables.UnifiedVariable - ( UnifiedVariable (..) - ) import Test.Kore.Step.MockSymbols ( testSort @@ -490,11 +488,10 @@ mapVariables => Pattern Variable -> Pattern variable mapVariables = - Pattern.mapVariables worker worker + Pattern.mapVariables (pure worker) where - worker :: Functor f => f Variable -> f variable - worker = fmap $ \v -> - fromVariable v { variableCounter = Just (Sup.Element 1) } + worker :: Variable -> variable + worker v = fromVariable v { variableCounter = Just (Sup.Element 1) } makeCeil :: InternalVariable variable diff --git a/kore/test/Test/Kore/Unification/Unifier.hs b/kore/test/Test/Kore/Unification/Unifier.hs index 7f292cfe8c..142377603e 100644 --- a/kore/test/Test/Kore/Unification/Unifier.hs +++ b/kore/test/Test/Kore/Unification/Unifier.hs @@ -57,8 +57,6 @@ import qualified Kore.Unification.SubstitutionSimplifier as Unification import qualified Kore.Unification.UnifierT as Monad.Unify import Kore.Unparser import Kore.Variables.UnifiedVariable - ( UnifiedVariable (..) - ) import qualified Pretty import Test.Kore @@ -541,9 +539,7 @@ test_unification = [(ElemVar $ ElementVariable $ mkW "1", war' "2")] ) (Substitution.unwrap - . Substitution.mapVariables - (fmap showVar) - (fmap showVar) + . Substitution.mapVariables showUnifiedVar . Substitution.wrap . Substitution.mkUnwrappedSubstitution $ [(ElemVar $ ElementVariable $ mkV 1, var' 2)] diff --git a/kore/test/Test/Kore/Variables/Fresh.hs b/kore/test/Test/Kore/Variables/Fresh.hs index 53ed61d96c..8a7185d771 100644 --- a/kore/test/Test/Kore/Variables/Fresh.hs +++ b/kore/test/Test/Kore/Variables/Fresh.hs @@ -319,9 +319,9 @@ test_refreshVariable = setNonTargetOriginal = mkSetNonTarget setOriginal avoidST = Set.singleton setTargetOriginal - unifiedTarget = mapUnifiedVariable mkElementTarget mkSetTarget + unifiedTarget = mapUnifiedVariable mkUnifiedTarget - unifiedNonTarget = mapUnifiedVariable mkElementNonTarget mkSetNonTarget + unifiedNonTarget = mapUnifiedVariable mkUnifiedTarget -- UnifiedVariable (Target Variable) unifiedElemTargetOriginal = unifiedTarget unifiedElemOriginal diff --git a/kore/test/Test/Kore/Variables/W.hs b/kore/test/Test/Kore/Variables/W.hs index e02284d732..e763d8cd2c 100644 --- a/kore/test/Test/Kore/Variables/W.hs +++ b/kore/test/Test/Kore/Variables/W.hs @@ -1,6 +1,7 @@ module Test.Kore.Variables.W ( W, mkW, war' , showVar + , showUnifiedVar ) where import Prelude.Kore @@ -18,6 +19,7 @@ import Debug import Kore.Internal.TermLike import Kore.Unparser import Kore.Variables.Fresh +import Kore.Variables.UnifiedVariable import Pretty import Test.Kore.Variables.V @@ -74,5 +76,8 @@ instance SubstitutionOrd W where showVar :: V -> W showVar (V i n) = W (show i) n +showUnifiedVar :: AdjUnifiedVariable (V -> W) +showUnifiedVar = pure showVar + war' :: String -> TermLike W war' = mkElemVar . ElementVariable . mkW From fd7bd9f3f4050e57953b6242b1fc1468a17a77ce Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 11 May 2020 21:51:02 -0500 Subject: [PATCH 02/16] Rename class VariableName to NamedVariable --- kore/src/Kore/Internal/Variable.hs | 2 +- kore/src/Kore/Rewriting/RewritingVariable.hs | 2 +- kore/src/Kore/Syntax/Variable.hs | 20 +++++++++---------- kore/src/Kore/Variables/Target.hs | 2 +- kore/src/Kore/Variables/UnifiedVariable.hs | 4 ++-- .../Kore/ASTVerifier/DefinitionVerifier.hs | 1 - kore/test/Test/Kore/Variables/V.hs | 2 +- kore/test/Test/Kore/Variables/W.hs | 2 +- 8 files changed, 17 insertions(+), 18 deletions(-) diff --git a/kore/src/Kore/Internal/Variable.hs b/kore/src/Kore/Internal/Variable.hs index 8e897ad9f2..d3af6714b2 100644 --- a/kore/src/Kore/Internal/Variable.hs +++ b/kore/src/Kore/Internal/Variable.hs @@ -84,6 +84,6 @@ these constraints. type InternalVariable variable = ( Hashable variable, Ord variable, SubstitutionOrd variable , Debug variable, Show variable, Unparse variable - , VariableName variable, SortedVariable variable + , NamedVariable variable, SortedVariable variable , FreshPartialOrd variable, FreshVariable variable ) diff --git a/kore/src/Kore/Rewriting/RewritingVariable.hs b/kore/src/Kore/Rewriting/RewritingVariable.hs index 2fa1b67c52..3d71a00004 100644 --- a/kore/src/Kore/Rewriting/RewritingVariable.hs +++ b/kore/src/Kore/Rewriting/RewritingVariable.hs @@ -80,7 +80,7 @@ instance FreshPartialOrd RewritingVariable where ConfigVariable var -> ConfigVariable (nextVariable var) {-# INLINE nextVariable #-} -instance VariableName RewritingVariable +instance NamedVariable RewritingVariable instance SubstitutionOrd RewritingVariable where compareSubstitution (RuleVariable _) (ConfigVariable _) = LT diff --git a/kore/src/Kore/Syntax/Variable.hs b/kore/src/Kore/Syntax/Variable.hs index fc28b87b63..fad18f2af9 100644 --- a/kore/src/Kore/Syntax/Variable.hs +++ b/kore/src/Kore/Syntax/Variable.hs @@ -14,7 +14,7 @@ module Kore.Syntax.Variable , illegalVariableCounter , externalizeFreshVariable -- * Variable names - , VariableName + , NamedVariable , toVariable , fromVariable -- * Variable sorts @@ -95,7 +95,7 @@ instance From Variable Variable where from = id {-# INLINE from #-} -instance VariableName Variable +instance NamedVariable Variable {- | Is the variable original (as opposed to generated)? -} @@ -131,9 +131,9 @@ externalizeFreshVariable variable@Variable { variableName, variableCounter } = , idLocation = AstLocationGeneratedVariable } -{- | 'VariableName' is the name of a Kore variable. +{- | 'NamedVariable' is the name of a Kore variable. -A 'VariableName' has instances: +A 'NamedVariable' has instances: * @'From' variable 'Variable'@ * @'From' 'Variable' variable@ @@ -147,14 +147,14 @@ prop> (==) x y === (==) (toVariable x) (toVariable y) -} class (Ord variable, From variable Variable, From Variable variable) - => VariableName variable + => NamedVariable variable --- | An injection from 'Variable' to any 'VariableName'. -fromVariable :: forall variable. VariableName variable => Variable -> variable +-- | An injection from 'Variable' to any 'NamedVariable'. +fromVariable :: forall variable. NamedVariable variable => Variable -> variable fromVariable = from @Variable @variable --- | An injection from any 'VariableName' to 'Variable'. -toVariable :: forall variable. VariableName variable => variable -> Variable +-- | An injection from any 'NamedVariable' to 'Variable'. +toVariable :: forall variable. NamedVariable variable => variable -> Variable toVariable = from @variable @Variable {- | 'SortedVariable' is a Kore variable with a known sort. @@ -217,7 +217,7 @@ instance SortedVariable Concrete where lensVariableSort _ = \case {} {-# INLINE lensVariableSort #-} -instance VariableName Concrete +instance NamedVariable Concrete instance From Variable Concrete where from = error "Cannot construct a variable in a concrete term!" diff --git a/kore/src/Kore/Variables/Target.hs b/kore/src/Kore/Variables/Target.hs index 816a922f66..e4870ad25b 100644 --- a/kore/src/Kore/Variables/Target.hs +++ b/kore/src/Kore/Variables/Target.hs @@ -142,7 +142,7 @@ instance NonTarget variable -> Target <$> lensVariableSort f variable {-# INLINE lensVariableSort #-} -instance VariableName variable => VariableName (Target variable) +instance NamedVariable variable => NamedVariable (Target variable) instance From variable1 variable2 => From variable1 (Target variable2) where from = Target . from @variable1 @variable2 diff --git a/kore/src/Kore/Variables/UnifiedVariable.hs b/kore/src/Kore/Variables/UnifiedVariable.hs index ccb9ac55ce..eb7b2dde8f 100644 --- a/kore/src/Kore/Variables/UnifiedVariable.hs +++ b/kore/src/Kore/Variables/UnifiedVariable.hs @@ -276,12 +276,12 @@ traverseUnifiedVariable AdjUnifiedVariable { elemVar, setVar } = SetVar <$> sequenceA (setVar <*> setVariable) toUnifiedVariable - :: VariableName variable + :: NamedVariable variable => AdjUnifiedVariable (variable -> Variable) toUnifiedVariable = pure toVariable fromUnifiedVariable - :: VariableName variable + :: NamedVariable variable => AdjUnifiedVariable (Variable -> variable) fromUnifiedVariable = pure fromVariable diff --git a/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier.hs b/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier.hs index 39d6eddd82..e411763161 100644 --- a/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier.hs +++ b/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier.hs @@ -86,7 +86,6 @@ 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/Variables/V.hs b/kore/test/Test/Kore/Variables/V.hs index fa9c8e11bd..84381f28a8 100644 --- a/kore/test/Test/Kore/Variables/V.hs +++ b/kore/test/Test/Kore/Variables/V.hs @@ -51,7 +51,7 @@ instance From Variable V where instance From V Variable where from = error "Not implemented" -instance VariableName V +instance NamedVariable V instance FreshPartialOrd V where infVariable v = v { counter = Nothing } diff --git a/kore/test/Test/Kore/Variables/W.hs b/kore/test/Test/Kore/Variables/W.hs index e763d8cd2c..ddd700c09e 100644 --- a/kore/test/Test/Kore/Variables/W.hs +++ b/kore/test/Test/Kore/Variables/W.hs @@ -54,7 +54,7 @@ instance From Variable W where instance From W Variable where from = error "Not implemented" -instance VariableName W +instance NamedVariable W instance FreshPartialOrd W where infVariable w = w { counter = Nothing } From e373a9ee331b5ce9d637e5cddbaf48463438c3f2 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 20 May 2020 05:50:21 -0500 Subject: [PATCH 03/16] Add data type Variable1 The goal of refactoring is to replace type Variable and the wrappers around it with type Variable1, and rename the latter. Note that this will make the SortedVariable class obsolete because all variables will carry a sort field at the top level; therefore, we will modify the SortedVariable class to carry the intermediate definitions we need for refactoring, and remove the class in the end. --- kore/src/Kore/Syntax/Variable.hs | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/kore/src/Kore/Syntax/Variable.hs b/kore/src/Kore/Syntax/Variable.hs index fad18f2af9..be519a3704 100644 --- a/kore/src/Kore/Syntax/Variable.hs +++ b/kore/src/Kore/Syntax/Variable.hs @@ -226,3 +226,31 @@ instance From Variable Concrete where instance From Concrete variable where from = \case {} {-# INLINE from #-} + +data Variable1 variable = + Variable1 + { variableName1 :: !variable + , variableSort1 :: !Sort + } + deriving (Eq, Ord, Show) + deriving (GHC.Generic) + +instance Hashable variable => Hashable (Variable1 variable) + +instance NFData variable => NFData (Variable1 variable) + +instance SOP.Generic (Variable1 variable) + +instance SOP.HasDatatypeInfo (Variable1 variable) + +instance Debug variable => Debug (Variable1 variable) + +instance (Debug variable, Diff variable) => Diff (Variable1 variable) + +instance Unparse variable => Unparse (Variable1 variable) where + unparse Variable1 { variableName1, variableSort1 } = + unparse variableName1 + <> Pretty.colon + <> unparse variableSort1 + + unparse2 Variable1 { variableName1 } = unparse2 variableName1 From 12294eae4ed45c67af453325669215920a8ad77a Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 12 May 2020 06:15:27 -0500 Subject: [PATCH 04/16] Kore.Syntax.Variable: Variable names --- kore/src/Kore/Syntax/Variable.hs | 97 +++++++++++++++++++ .../Kore/ASTVerifier/DefinitionVerifier.hs | 1 + .../DefinitionVerifier/PatternVerifier.hs | 4 +- .../DefinitionVerifier/SortUsage.hs | 4 +- .../DefinitionVerifier/UniqueNames.hs | 4 +- 5 files changed, 107 insertions(+), 3 deletions(-) diff --git a/kore/src/Kore/Syntax/Variable.hs b/kore/src/Kore/Syntax/Variable.hs index be519a3704..1c2c4a229b 100644 --- a/kore/src/Kore/Syntax/Variable.hs +++ b/kore/src/Kore/Syntax/Variable.hs @@ -14,6 +14,10 @@ module Kore.Syntax.Variable , illegalVariableCounter , externalizeFreshVariable -- * Variable names + , VariableName (..) + , ElementVariableName (..) + , SetVariableName (..) + , SomeVariableName (..) , NamedVariable , toVariable , fromVariable @@ -37,6 +41,9 @@ import qualified Control.Lens as Lens import Data.Generics.Product ( field ) +import Data.Generics.Sum + ( _Ctor + ) import qualified Data.Text as Text import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC @@ -48,6 +55,96 @@ import Kore.Sort import Kore.Unparser import qualified Pretty +data VariableName = + VariableName + { base :: !Id + , counter :: !(Maybe (Sup Natural)) + } + deriving (Eq, Ord, Show) + deriving (GHC.Generic) + +instance Hashable VariableName + +instance NFData VariableName + +instance SOP.Generic VariableName + +instance SOP.HasDatatypeInfo VariableName + +instance Debug VariableName + +instance Diff VariableName + +newtype ElementVariableName variable = + ElementVariableName { unElementVariableName :: variable } + deriving (Eq, Ord, Show) + deriving (Functor) + deriving (Foldable, Traversable) + deriving (GHC.Generic) + +instance Hashable variable => Hashable (ElementVariableName variable) + +instance NFData variable => NFData (ElementVariableName variable) + +instance SOP.Generic (ElementVariableName variable) + +instance SOP.HasDatatypeInfo (ElementVariableName variable) + +instance Debug variable => Debug (ElementVariableName variable) + +instance (Debug variable, Diff variable) => Diff (ElementVariableName variable) + +newtype SetVariableName variable = + SetVariableName { unSetVariableName :: variable } + deriving (Eq, Ord, Show) + deriving (Functor) + deriving (Foldable, Traversable) + deriving (GHC.Generic) + +instance Hashable variable => Hashable (SetVariableName variable) + +instance NFData variable => NFData (SetVariableName variable) + +instance SOP.Generic (SetVariableName variable) + +instance SOP.HasDatatypeInfo (SetVariableName variable) + +instance Debug variable => Debug (SetVariableName variable) + +instance (Debug variable, Diff variable) => Diff (SetVariableName variable) + +data SomeVariableName variable + = SomeVariableNameElement !(ElementVariableName variable) + | SomeVariableNameSet !(SetVariableName variable) + deriving (Eq, Ord, Show) + deriving (Functor) + deriving (Foldable, Traversable) + deriving (GHC.Generic) + +instance Hashable variable => Hashable (SomeVariableName variable) + +instance NFData variable => NFData (SomeVariableName variable) + +instance SOP.Generic (SomeVariableName variable) + +instance SOP.HasDatatypeInfo (SomeVariableName variable) + +instance Debug variable => Debug (SomeVariableName variable) + +instance (Debug variable, Diff variable) => Diff (SomeVariableName variable) + +instance + Injection (SomeVariableName variable) (ElementVariableName variable) + where + injection = _Ctor @"SomeVariableNameElement" + {-# INLINE injection #-} + +instance + Injection (SomeVariableName variable) (SetVariableName variable) + where + injection = _Ctor @"SomeVariableNameSet" + {-# INLINE injection #-} + {-|'Variable' corresponds to the @variable@ syntactic category from the Semantics of K, Section 9.1.4 (Patterns). diff --git a/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier.hs b/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier.hs index e411763161..01508546f2 100644 --- a/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier.hs +++ b/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier.hs @@ -86,6 +86,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/ASTVerifier/DefinitionVerifier/PatternVerifier.hs b/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier/PatternVerifier.hs index a24972f74c..690f917877 100644 --- a/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier/PatternVerifier.hs +++ b/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier/PatternVerifier.hs @@ -25,7 +25,9 @@ import Kore.IndexedModule.Error ( noSort ) import qualified Kore.Internal.TermLike as Internal -import Kore.Syntax +import Kore.Syntax hiding + ( VariableName (..) + ) import Kore.Syntax.Definition import Kore.Variables.UnifiedVariable diff --git a/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier/SortUsage.hs b/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier/SortUsage.hs index 701977c776..e1f1d81017 100644 --- a/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier/SortUsage.hs +++ b/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier/SortUsage.hs @@ -23,7 +23,9 @@ import Kore.Error import Kore.IndexedModule.Error ( noSort ) -import Kore.Internal.TermLike +import Kore.Internal.TermLike hiding + ( VariableName (..) + ) import Kore.Syntax.Definition ( AsSentence (..) , Attributes (..) diff --git a/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier/UniqueNames.hs b/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier/UniqueNames.hs index b6389e2c61..ba43238686 100644 --- a/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier/UniqueNames.hs +++ b/kore/test/Test/Kore/ASTVerifier/DefinitionVerifier/UniqueNames.hs @@ -9,7 +9,9 @@ import Test.Tasty ) import Kore.Error -import Kore.Syntax +import Kore.Syntax hiding + ( VariableName (..) + ) import Kore.Syntax.Definition import Test.Kore.ASTVerifier.DefinitionVerifier From 44e979891a8de8ab781718c78fd05a65d4ee5edf Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Sun, 17 May 2020 07:03:50 -0500 Subject: [PATCH 05/16] Add type family VariableNameOf --- kore/src/Kore/Internal/Variable.hs | 1 + kore/src/Kore/Rewriting/RewritingVariable.hs | 29 ++++++++++++- kore/src/Kore/Syntax/ElementVariable.hs | 20 ++++++++- kore/src/Kore/Syntax/SetVariable.hs | 14 +++++- kore/src/Kore/Syntax/Variable.hs | 41 +++++++++++++++--- kore/src/Kore/Variables/Target.hs | 9 +++- kore/src/Kore/Variables/UnifiedVariable.hs | 45 +++++++++++++++++--- kore/test/Test/Kore/Variables/V.hs | 7 ++- kore/test/Test/Kore/Variables/W.hs | 7 ++- 9 files changed, 154 insertions(+), 19 deletions(-) diff --git a/kore/src/Kore/Internal/Variable.hs b/kore/src/Kore/Internal/Variable.hs index d3af6714b2..0d441fe37e 100644 --- a/kore/src/Kore/Internal/Variable.hs +++ b/kore/src/Kore/Internal/Variable.hs @@ -85,5 +85,6 @@ type InternalVariable variable = ( Hashable variable, Ord variable, SubstitutionOrd variable , Debug variable, Show variable, Unparse variable , NamedVariable variable, SortedVariable variable + , VariableBase variable , FreshPartialOrd variable, FreshVariable variable ) diff --git a/kore/src/Kore/Rewriting/RewritingVariable.hs b/kore/src/Kore/Rewriting/RewritingVariable.hs index 3d71a00004..e23d6b7981 100644 --- a/kore/src/Kore/Rewriting/RewritingVariable.hs +++ b/kore/src/Kore/Rewriting/RewritingVariable.hs @@ -24,6 +24,7 @@ module Kore.Rewriting.RewritingVariable import Prelude.Kore +import qualified Control.Lens as Lens import qualified Data.Map.Strict as Map import qualified Data.Set as Set import qualified Generics.SOP as SOP @@ -80,7 +81,33 @@ instance FreshPartialOrd RewritingVariable where ConfigVariable var -> ConfigVariable (nextVariable var) {-# INLINE nextVariable #-} -instance NamedVariable RewritingVariable +data RewritingVariableName + = ConfigVariableName !VariableName + | RuleVariableName !VariableName + deriving (Eq, Ord, Show) + deriving (GHC.Generic) + +instance NamedVariable RewritingVariable where + type VariableNameOf RewritingVariable = RewritingVariableName + lensVariableName = + Lens.lens get set + where + get (ConfigVariable variable) = + ConfigVariableName (Lens.view lensVariableName variable) + get (RuleVariable variable) = + RuleVariableName (Lens.view lensVariableName variable) + set rewritingVariable rewritingVariableName = + case rewritingVariableName of + ConfigVariableName variableName -> + Lens.set lensVariableName variableName variable + & ConfigVariable + RuleVariableName variableName -> + Lens.set lensVariableName variableName variable + & RuleVariable + where + variable = from @_ @Variable rewritingVariable + +instance VariableBase RewritingVariable instance SubstitutionOrd RewritingVariable where compareSubstitution (RuleVariable _) (ConfigVariable _) = LT diff --git a/kore/src/Kore/Syntax/ElementVariable.hs b/kore/src/Kore/Syntax/ElementVariable.hs index 24c1f1056c..1474fa18c5 100644 --- a/kore/src/Kore/Syntax/ElementVariable.hs +++ b/kore/src/Kore/Syntax/ElementVariable.hs @@ -15,14 +15,13 @@ import Control.DeepSeq ) import Data.Generics.Wrapped ( _Unwrapped + , _Wrapped ) 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 @@ -68,3 +67,20 @@ instance where from = fmap (from @variable1 @variable2) {-# INLINE from #-} + +instance + From variable Variable => From (ElementVariable variable) Variable + where + from = from . getElementVariable + +instance + From Variable variable => From Variable (ElementVariable variable) + where + from = ElementVariable . from + +instance + NamedVariable variable => NamedVariable (ElementVariable variable) + where + type VariableNameOf (ElementVariable variable) = + ElementVariableName (VariableNameOf variable) + lensVariableName = _Unwrapped . lensVariableName . _Wrapped diff --git a/kore/src/Kore/Syntax/SetVariable.hs b/kore/src/Kore/Syntax/SetVariable.hs index f3ccc2ef53..f5bc050fd5 100644 --- a/kore/src/Kore/Syntax/SetVariable.hs +++ b/kore/src/Kore/Syntax/SetVariable.hs @@ -15,14 +15,13 @@ import Control.DeepSeq ) import Data.Generics.Wrapped ( _Unwrapped + , _Wrapped ) 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 @@ -68,3 +67,14 @@ instance where from = fmap (from @variable1 @variable2) {-# INLINE from #-} + +instance From variable Variable => From (SetVariable variable) Variable where + from = from . getSetVariable + +instance From Variable variable => From Variable (SetVariable variable) where + from = SetVariable . from + +instance NamedVariable variable => NamedVariable (SetVariable variable) where + type VariableNameOf (SetVariable variable) = + SetVariableName (VariableNameOf variable) + lensVariableName = _Unwrapped . lensVariableName . _Wrapped diff --git a/kore/src/Kore/Syntax/Variable.hs b/kore/src/Kore/Syntax/Variable.hs index 1c2c4a229b..12be3bd942 100644 --- a/kore/src/Kore/Syntax/Variable.hs +++ b/kore/src/Kore/Syntax/Variable.hs @@ -18,7 +18,8 @@ module Kore.Syntax.Variable , ElementVariableName (..) , SetVariableName (..) , SomeVariableName (..) - , NamedVariable + , NamedVariable (..) + , VariableBase , toVariable , fromVariable -- * Variable sorts @@ -45,6 +46,7 @@ import Data.Generics.Sum ( _Ctor ) import qualified Data.Text as Text +import Data.Void import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC import Numeric.Natural @@ -192,7 +194,24 @@ instance From Variable Variable where from = id {-# INLINE from #-} -instance NamedVariable Variable +instance NamedVariable Variable where + type VariableNameOf Variable = VariableName + lensVariableName = + Lens.lens get set + where + get Variable { variableName, variableCounter } = + VariableName + { base = variableName + , counter = variableCounter + } + set Variable { variableSort } VariableName { base, counter } = + Variable + { variableName = base + , variableCounter = counter + , variableSort + } + +instance VariableBase Variable {- | Is the variable original (as opposed to generated)? -} @@ -243,15 +262,21 @@ prop> (==) x y === (==) (toVariable x) (toVariable y) -} class - (Ord variable, From variable Variable, From Variable variable) + (Ord variable, From variable Variable) => NamedVariable variable + where + type VariableNameOf variable + lensVariableName :: Lens' variable (VariableNameOf variable) + +class + (From Variable variable, From variable Variable) => VariableBase variable -- | An injection from 'Variable' to any 'NamedVariable'. -fromVariable :: forall variable. NamedVariable variable => Variable -> variable +fromVariable :: forall variable. From Variable variable => Variable -> variable fromVariable = from @Variable @variable -- | An injection from any 'NamedVariable' to 'Variable'. -toVariable :: forall variable. NamedVariable variable => variable -> Variable +toVariable :: forall variable. From variable Variable => variable -> Variable toVariable = from @variable @Variable {- | 'SortedVariable' is a Kore variable with a known sort. @@ -314,7 +339,11 @@ instance SortedVariable Concrete where lensVariableSort _ = \case {} {-# INLINE lensVariableSort #-} -instance NamedVariable Concrete +instance NamedVariable Concrete where + type VariableNameOf Concrete = Void + lensVariableName = Lens.lens (\case {}) (\case {}) + +instance VariableBase Concrete instance From Variable Concrete where from = error "Cannot construct a variable in a concrete term!" diff --git a/kore/src/Kore/Variables/Target.hs b/kore/src/Kore/Variables/Target.hs index e4870ad25b..2be50ade42 100644 --- a/kore/src/Kore/Variables/Target.hs +++ b/kore/src/Kore/Variables/Target.hs @@ -142,7 +142,14 @@ instance NonTarget variable -> Target <$> lensVariableSort f variable {-# INLINE lensVariableSort #-} -instance NamedVariable variable => NamedVariable (Target variable) +instance NamedVariable variable => NamedVariable (Target variable) where + type VariableNameOf (Target variable) = VariableNameOf variable + lensVariableName f = + \case + Target variable -> Target <$> lensVariableName f variable + NonTarget variable -> NonTarget <$> lensVariableName f variable + +instance VariableBase variable => VariableBase (Target variable) instance From variable1 variable2 => From variable1 (Target variable2) where from = Target . from @variable1 @variable2 diff --git a/kore/src/Kore/Variables/UnifiedVariable.hs b/kore/src/Kore/Variables/UnifiedVariable.hs index eb7b2dde8f..a567be5fd8 100644 --- a/kore/src/Kore/Variables/UnifiedVariable.hs +++ b/kore/src/Kore/Variables/UnifiedVariable.hs @@ -64,9 +64,6 @@ import Kore.Sort import Kore.Syntax.ElementVariable import Kore.Syntax.SetVariable import Kore.Syntax.Variable - ( SortedVariable (..) - , sortedVariableSort - ) import Kore.Unparser import Kore.Variables.Fresh @@ -76,7 +73,8 @@ from element variables (introduced by 'ElemVar'). data UnifiedVariable variable = ElemVar !(ElementVariable variable) | SetVar !(SetVariable variable) - deriving (Generic, Eq, Ord, Show) + deriving (Eq, Ord, Show) + deriving (Generic) instance NFData variable => NFData (UnifiedVariable variable) @@ -104,6 +102,43 @@ instance SetVar setVar -> SetVar <$> lensVariableSort f setVar {-# INLINE lensVariableSort #-} +instance From (UnifiedVariable variable) variable where + from (ElemVar elementVariable) = getElementVariable elementVariable + from (SetVar setVariable) = getSetVariable setVariable + {-# INLINE from #-} + +instance + From variable Variable => From (UnifiedVariable variable) Variable + where + from (ElemVar elementVariable) = from elementVariable + from (SetVar setVariable) = from setVariable + {-# INLINE from #-} + +instance + NamedVariable variable => NamedVariable (UnifiedVariable variable) + where + type VariableNameOf (UnifiedVariable variable) = + SomeVariableName (VariableNameOf variable) + lensVariableName = + Lens.lens get set + where + get (ElemVar elementVariable) = + SomeVariableNameElement (Lens.view lensVariableName elementVariable) + get (SetVar setVariable) = + SomeVariableNameSet (Lens.view lensVariableName setVariable) + set unifiedVariable someVariableName = + case someVariableName of + SomeVariableNameElement elementVariableName -> + ElementVariable variable + & Lens.set lensVariableName elementVariableName + & ElemVar + SomeVariableNameSet setVariableName -> + SetVariable variable + & Lens.set lensVariableName setVariableName + & SetVar + where + variable = from @_ @variable unifiedVariable + instance FreshPartialOrd variable => FreshPartialOrd (UnifiedVariable variable) where @@ -281,7 +316,7 @@ toUnifiedVariable toUnifiedVariable = pure toVariable fromUnifiedVariable - :: NamedVariable variable + :: From Variable variable => AdjUnifiedVariable (Variable -> variable) fromUnifiedVariable = pure fromVariable diff --git a/kore/test/Test/Kore/Variables/V.hs b/kore/test/Test/Kore/Variables/V.hs index 84381f28a8..93553c5d0e 100644 --- a/kore/test/Test/Kore/Variables/V.hs +++ b/kore/test/Test/Kore/Variables/V.hs @@ -51,7 +51,10 @@ instance From Variable V where instance From V Variable where from = error "Not implemented" -instance NamedVariable V +instance NamedVariable V where + type VariableNameOf V = V + lensVariableName f = f + {-# INLINE lensVariableName #-} instance FreshPartialOrd V where infVariable v = v { counter = Nothing } @@ -70,6 +73,8 @@ instance FreshVariable V instance SubstitutionOrd V where compareSubstitution = compare +instance VariableBase V + var' :: Integer -> TermLike V var' = mkElemVar . ElementVariable . mkV diff --git a/kore/test/Test/Kore/Variables/W.hs b/kore/test/Test/Kore/Variables/W.hs index ddd700c09e..ef07413771 100644 --- a/kore/test/Test/Kore/Variables/W.hs +++ b/kore/test/Test/Kore/Variables/W.hs @@ -54,7 +54,10 @@ instance From Variable W where instance From W Variable where from = error "Not implemented" -instance NamedVariable W +instance NamedVariable W where + type VariableNameOf W = W + lensVariableName f = f + {-# INLINE lensVariableName #-} instance FreshPartialOrd W where infVariable w = w { counter = Nothing } @@ -73,6 +76,8 @@ instance FreshVariable W instance SubstitutionOrd W where compareSubstitution = compare +instance VariableBase W + showVar :: V -> W showVar (V i n) = W (show i) n From c2b1155c7e1ecac500184ab7b73cd2b4a40dd17e Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 18 May 2020 20:13:21 -0500 Subject: [PATCH 06/16] NamedVariable: Add isoVariable1 method --- kore/src/Kore/AST/AstWithLocation.hs | 2 +- kore/src/Kore/Rewriting/RewritingVariable.hs | 35 +++++++------ kore/src/Kore/Syntax/ElementVariable.hs | 15 +++++- kore/src/Kore/Syntax/SetVariable.hs | 15 +++++- kore/src/Kore/Syntax/Variable.hs | 52 ++++++++++++++++---- kore/src/Kore/Variables/Target.hs | 31 +++++++++--- kore/src/Kore/Variables/UnifiedVariable.hs | 25 ++++++++++ kore/test/Test/Kore/Variables/V.hs | 6 +++ kore/test/Test/Kore/Variables/W.hs | 6 +++ 9 files changed, 152 insertions(+), 35 deletions(-) diff --git a/kore/src/Kore/AST/AstWithLocation.hs b/kore/src/Kore/AST/AstWithLocation.hs index 3ca5f3c654..28a8caaee6 100644 --- a/kore/src/Kore/AST/AstWithLocation.hs +++ b/kore/src/Kore/AST/AstWithLocation.hs @@ -57,7 +57,7 @@ instance AstWithLocation Sort where locationFromAst sortActual instance AstWithLocation Variable where - locationFromAst = locationFromAst . variableName + locationFromAst Variable { variableName } = locationFromAst variableName instance AstWithLocation variable => AstWithLocation (ElementVariable variable) diff --git a/kore/src/Kore/Rewriting/RewritingVariable.hs b/kore/src/Kore/Rewriting/RewritingVariable.hs index e23d6b7981..9d0d21c9e8 100644 --- a/kore/src/Kore/Rewriting/RewritingVariable.hs +++ b/kore/src/Kore/Rewriting/RewritingVariable.hs @@ -89,23 +89,30 @@ data RewritingVariableName instance NamedVariable RewritingVariable where type VariableNameOf RewritingVariable = RewritingVariableName - lensVariableName = - Lens.lens get set + + isoVariable1 = + Lens.iso to fr where - get (ConfigVariable variable) = - ConfigVariableName (Lens.view lensVariableName variable) - get (RuleVariable variable) = - RuleVariableName (Lens.view lensVariableName variable) - set rewritingVariable rewritingVariableName = - case rewritingVariableName of - ConfigVariableName variableName -> - Lens.set lensVariableName variableName variable + to (ConfigVariable variable) = + ConfigVariableName <$> Lens.view isoVariable1 variable + to (RuleVariable variable) = + RuleVariableName <$> Lens.view isoVariable1 variable + fr Variable1 { variableName1, variableSort1 } = + case variableName1 of + ConfigVariableName variableName1' -> + Variable1 + { variableName1 = variableName1' + , variableSort1 + } + & Lens.review isoVariable1 & ConfigVariable - RuleVariableName variableName -> - Lens.set lensVariableName variableName variable + RuleVariableName variableName1' -> + Variable1 + { variableName1 = variableName1' + , variableSort1 + } + & Lens.review isoVariable1 & RuleVariable - where - variable = from @_ @Variable rewritingVariable instance VariableBase RewritingVariable diff --git a/kore/src/Kore/Syntax/ElementVariable.hs b/kore/src/Kore/Syntax/ElementVariable.hs index 1474fa18c5..a2bd64d8a3 100644 --- a/kore/src/Kore/Syntax/ElementVariable.hs +++ b/kore/src/Kore/Syntax/ElementVariable.hs @@ -13,9 +13,9 @@ import Prelude.Kore import Control.DeepSeq ( NFData (..) ) +import qualified Control.Lens as Lens import Data.Generics.Wrapped ( _Unwrapped - , _Wrapped ) import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC @@ -83,4 +83,15 @@ instance where type VariableNameOf (ElementVariable variable) = ElementVariableName (VariableNameOf variable) - lensVariableName = _Unwrapped . lensVariableName . _Wrapped + + isoVariable1 = + Lens.iso to fr + where + to = + getElementVariable + >>> Lens.view isoVariable1 + >>> fmap ElementVariableName + fr = + fmap unElementVariableName + >>> Lens.review isoVariable1 + >>> ElementVariable diff --git a/kore/src/Kore/Syntax/SetVariable.hs b/kore/src/Kore/Syntax/SetVariable.hs index f5bc050fd5..ddd291a411 100644 --- a/kore/src/Kore/Syntax/SetVariable.hs +++ b/kore/src/Kore/Syntax/SetVariable.hs @@ -13,9 +13,9 @@ import Prelude.Kore import Control.DeepSeq ( NFData (..) ) +import qualified Control.Lens as Lens import Data.Generics.Wrapped ( _Unwrapped - , _Wrapped ) import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC @@ -77,4 +77,15 @@ instance From Variable variable => From Variable (SetVariable variable) where instance NamedVariable variable => NamedVariable (SetVariable variable) where type VariableNameOf (SetVariable variable) = SetVariableName (VariableNameOf variable) - lensVariableName = _Unwrapped . lensVariableName . _Wrapped + + isoVariable1 = + Lens.iso to fr + where + to = + getSetVariable + >>> Lens.view isoVariable1 + >>> fmap SetVariableName + fr = + fmap unSetVariableName + >>> Lens.review isoVariable1 + >>> SetVariable diff --git a/kore/src/Kore/Syntax/Variable.hs b/kore/src/Kore/Syntax/Variable.hs index 12be3bd942..baf2c89dbd 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 + , Variable1 (..) + , fromVariable1 + , toVariable1 -- * Variable names , VariableName (..) , ElementVariableName (..) @@ -36,7 +39,8 @@ import Control.DeepSeq ( NFData (..) ) import Control.Lens - ( Lens' + ( Iso' + , Lens' ) import qualified Control.Lens as Lens import Data.Generics.Product @@ -196,20 +200,27 @@ instance From Variable Variable where instance NamedVariable Variable where type VariableNameOf Variable = VariableName - lensVariableName = - Lens.lens get set + + isoVariable1 = + Lens.iso to fr where - get Variable { variableName, variableCounter } = - VariableName - { base = variableName - , counter = variableCounter + to Variable { variableName, variableCounter, variableSort } = + Variable1 + { variableName1 = + VariableName + { base = variableName + , counter = variableCounter + } + , variableSort1 = variableSort } - set Variable { variableSort } VariableName { base, counter } = + fr Variable1 { variableName1, variableSort1 } = Variable { variableName = base , variableCounter = counter - , variableSort + , variableSort = variableSort1 } + where + VariableName { base, counter } = variableName1 instance VariableBase Variable @@ -266,7 +277,23 @@ class => NamedVariable variable where type VariableNameOf variable + lensVariableName :: Lens' variable (VariableNameOf variable) + lensVariableName = isoVariable1 . field @"variableName1" + + isoVariable1 :: Iso' variable (Variable1 (VariableNameOf variable)) + +fromVariable1 + :: NamedVariable variable + => Variable1 (VariableNameOf variable) + -> variable +fromVariable1 = Lens.review isoVariable1 + +toVariable1 + :: NamedVariable variable + => variable + -> Variable1 (VariableNameOf variable) +toVariable1 = Lens.view isoVariable1 class (From Variable variable, From variable Variable) => VariableBase variable @@ -341,7 +368,10 @@ instance SortedVariable Concrete where instance NamedVariable Concrete where type VariableNameOf Concrete = Void - lensVariableName = Lens.lens (\case {}) (\case {}) + isoVariable1 = + Lens.iso + (\case {}) + (\Variable1 { variableName1 } -> case variableName1 of {}) instance VariableBase Concrete @@ -359,6 +389,8 @@ data Variable1 variable = , variableSort1 :: !Sort } deriving (Eq, Ord, Show) + deriving (Functor) + deriving (Foldable, Traversable) deriving (GHC.Generic) instance Hashable variable => Hashable (Variable1 variable) diff --git a/kore/src/Kore/Variables/Target.hs b/kore/src/Kore/Variables/Target.hs index 2be50ade42..85e08eb082 100644 --- a/kore/src/Kore/Variables/Target.hs +++ b/kore/src/Kore/Variables/Target.hs @@ -25,13 +25,15 @@ module Kore.Variables.Target import Prelude.Kore +import qualified Control.Lens as Lens import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC import Kore.Debug import Kore.Internal.Variable import Kore.Syntax.Variable - ( SortedVariable (..) + ( NamedVariable (..) + , SortedVariable (..) ) import Kore.Unparser ( Unparse (..) @@ -143,11 +145,28 @@ instance {-# INLINE lensVariableSort #-} instance NamedVariable variable => NamedVariable (Target variable) where - type VariableNameOf (Target variable) = VariableNameOf variable - lensVariableName f = - \case - Target variable -> Target <$> lensVariableName f variable - NonTarget variable -> NonTarget <$> lensVariableName f variable + type VariableNameOf (Target variable) = Target (VariableNameOf variable) + + lensVariableName = + Lens.lens get set + where + get = fmap (Lens.view lensVariableName) + set (unTarget -> variable) = + fmap $ \variableName -> + Lens.set lensVariableName variableName variable + + isoVariable1 = + Lens.iso to fr + where + to (Target variable) = Target <$> Lens.view isoVariable1 variable + to (NonTarget variable) = NonTarget <$> Lens.view isoVariable1 variable + fr Variable1 { variableName1, variableSort1 } = + flip fmap variableName1 $ \variableName1' -> + Variable1 + { variableName1 = variableName1' + , variableSort1 + } + & Lens.review isoVariable1 instance VariableBase variable => VariableBase (Target variable) diff --git a/kore/src/Kore/Variables/UnifiedVariable.hs b/kore/src/Kore/Variables/UnifiedVariable.hs index a567be5fd8..433eab50fc 100644 --- a/kore/src/Kore/Variables/UnifiedVariable.hs +++ b/kore/src/Kore/Variables/UnifiedVariable.hs @@ -119,6 +119,7 @@ instance where type VariableNameOf (UnifiedVariable variable) = SomeVariableName (VariableNameOf variable) + lensVariableName = Lens.lens get set where @@ -139,6 +140,30 @@ instance where variable = from @_ @variable unifiedVariable + isoVariable1 = + Lens.iso to fr + where + to (ElemVar elementVariable) = + SomeVariableNameElement <$> Lens.view isoVariable1 elementVariable + to (SetVar setVariable) = + SomeVariableNameSet <$> Lens.view isoVariable1 setVariable + fr Variable1 { variableName1, variableSort1 } = + case variableName1 of + SomeVariableNameElement elementVariableName -> + Variable1 + { variableName1 = elementVariableName + , variableSort1 + } + & Lens.review isoVariable1 + & ElemVar + SomeVariableNameSet setVariableName -> + Variable1 + { variableName1 = setVariableName + , variableSort1 + } + & Lens.review isoVariable1 + & SetVar + instance FreshPartialOrd variable => FreshPartialOrd (UnifiedVariable variable) where diff --git a/kore/test/Test/Kore/Variables/V.hs b/kore/test/Test/Kore/Variables/V.hs index 93553c5d0e..593d85caf5 100644 --- a/kore/test/Test/Kore/Variables/V.hs +++ b/kore/test/Test/Kore/Variables/V.hs @@ -55,6 +55,12 @@ instance NamedVariable V where type VariableNameOf V = V lensVariableName f = f {-# INLINE lensVariableName #-} + isoVariable1 = + Lens.iso to fr + where + to variableName1 = + Variable1 { variableName1, variableSort1 = sortVariable } + fr Variable1 { variableName1 } = variableName1 instance FreshPartialOrd V where infVariable v = v { counter = Nothing } diff --git a/kore/test/Test/Kore/Variables/W.hs b/kore/test/Test/Kore/Variables/W.hs index ef07413771..5225c23d66 100644 --- a/kore/test/Test/Kore/Variables/W.hs +++ b/kore/test/Test/Kore/Variables/W.hs @@ -58,6 +58,12 @@ instance NamedVariable W where type VariableNameOf W = W lensVariableName f = f {-# INLINE lensVariableName #-} + isoVariable1 = + Lens.iso to fr + where + to variableName1 = + Variable1 { variableName1, variableSort1 = sortVariable } + fr Variable1 { variableName1 } = variableName1 instance FreshPartialOrd W where infVariable w = w { counter = Nothing } From 7768643f5bc707860f4f3dfc54c7ac87f8dfd9db Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 20 May 2020 06:59:21 -0500 Subject: [PATCH 07/16] Add SortedVariable as a superclass of NamedVariable --- kore/src/Kore/Internal/Predicate.hs | 4 ++-- kore/src/Kore/Internal/TermLike.hs | 2 +- kore/src/Kore/Internal/TermLike/TermLike.hs | 6 +++--- kore/src/Kore/Rewriting/UnifyingRule.hs | 4 ++-- kore/src/Kore/Syntax/Variable.hs | 2 +- 5 files changed, 9 insertions(+), 9 deletions(-) diff --git a/kore/src/Kore/Internal/Predicate.hs b/kore/src/Kore/Internal/Predicate.hs index 4b03369585..9795ec6b52 100644 --- a/kore/src/Kore/Internal/Predicate.hs +++ b/kore/src/Kore/Internal/Predicate.hs @@ -732,11 +732,11 @@ isPredicate = Either.isRight . makePredicate {- | Replace all variables in a @Predicate@ using the provided mapping. -} mapVariables - :: (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2) + :: (Ord variable1, FreshPartialOrd variable2, NamedVariable variable2) => AdjUnifiedVariable (variable1 -> variable2) -> Predicate variable1 -> Predicate variable2 -mapVariables mapping = fmap (TermLike.mapVariables mapping) +mapVariables adj = fmap (TermLike.mapVariables adj) instance HasFreeVariables (Predicate variable) variable where freeVariables = freeVariables . unwrapPredicate diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index 1adbea3157..8141301846 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -417,7 +417,7 @@ composes with other tree transformations without allocating intermediates. -} fromConcrete - :: (FreshPartialOrd variable, SortedVariable variable) + :: (FreshPartialOrd variable, NamedVariable variable) => TermLike Concrete -> TermLike variable fromConcrete = mapVariables fromConcreteUnifiedVariable diff --git a/kore/src/Kore/Internal/TermLike/TermLike.hs b/kore/src/Kore/Internal/TermLike/TermLike.hs index 3c088a4ebf..28cd69ae98 100644 --- a/kore/src/Kore/Internal/TermLike/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike/TermLike.hs @@ -504,7 +504,7 @@ instance Unparse (TermLike variable) => SQL.Column (TermLike variable) where toColumn = SQL.toColumn . Pretty.renderText . Pretty.layoutOneLine . unparse instance - (FreshPartialOrd variable, SortedVariable variable) + (FreshPartialOrd variable, NamedVariable variable) => From (TermLike Concrete) (TermLike variable) where from = mapVariables fromConcreteUnifiedVariable @@ -660,7 +660,7 @@ See also: 'traverseVariables' -} mapVariables :: forall variable1 variable2 - . (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2) + . (Ord variable1, FreshPartialOrd variable2, NamedVariable variable2) => AdjUnifiedVariable (variable1 -> variable2) -> TermLike variable1 -> TermLike variable2 @@ -741,7 +741,7 @@ See also: 'mapVariables' -} traverseVariables :: forall variable1 variable2 m - . (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2) + . (Ord variable1, FreshPartialOrd variable2, NamedVariable variable2) => Monad m => AdjUnifiedVariable (variable1 -> m variable2) -> TermLike variable1 diff --git a/kore/src/Kore/Rewriting/UnifyingRule.hs b/kore/src/Kore/Rewriting/UnifyingRule.hs index 1f6cc39097..9cd17ba044 100644 --- a/kore/src/Kore/Rewriting/UnifyingRule.hs +++ b/kore/src/Kore/Rewriting/UnifyingRule.hs @@ -25,7 +25,7 @@ import Kore.Internal.Predicate ) import Kore.Internal.TermLike ( InternalVariable - , SortedVariable + , NamedVariable , TermLike ) import Kore.Unparser @@ -96,7 +96,7 @@ class UnifyingRule rule where distinguishing rule variables from configuration variables. -} mapRuleVariables - :: (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2) + :: (Ord variable1, FreshPartialOrd variable2, NamedVariable variable2) => AdjUnifiedVariable (variable1 -> variable2) -> rule variable1 -> rule variable2 diff --git a/kore/src/Kore/Syntax/Variable.hs b/kore/src/Kore/Syntax/Variable.hs index baf2c89dbd..3c4ede8195 100644 --- a/kore/src/Kore/Syntax/Variable.hs +++ b/kore/src/Kore/Syntax/Variable.hs @@ -273,7 +273,7 @@ prop> (==) x y === (==) (toVariable x) (toVariable y) -} class - (Ord variable, From variable Variable) + (Ord variable, From variable Variable, SortedVariable variable) => NamedVariable variable where type VariableNameOf variable From ab4d8578ef52b80157b8127ba0befb8b0fc56a41 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Sat, 23 May 2020 14:49:44 -0500 Subject: [PATCH 08/16] Generalize type of lensVariableName --- kore/src/Kore/Syntax/Variable.hs | 17 ++++++++++++----- kore/src/Kore/Variables/Target.hs | 8 -------- kore/src/Kore/Variables/UnifiedVariable.hs | 20 -------------------- kore/test/Test/Kore/Variables/V.hs | 3 +-- kore/test/Test/Kore/Variables/W.hs | 3 +-- 5 files changed, 14 insertions(+), 37 deletions(-) diff --git a/kore/src/Kore/Syntax/Variable.hs b/kore/src/Kore/Syntax/Variable.hs index 3c4ede8195..50643f958e 100644 --- a/kore/src/Kore/Syntax/Variable.hs +++ b/kore/src/Kore/Syntax/Variable.hs @@ -14,14 +14,15 @@ module Kore.Syntax.Variable , illegalVariableCounter , externalizeFreshVariable , Variable1 (..) - , fromVariable1 - , toVariable1 -- * Variable names , VariableName (..) , ElementVariableName (..) , SetVariableName (..) , SomeVariableName (..) , NamedVariable (..) + , lensVariableName + , fromVariable1 + , toVariable1 , VariableBase , toVariable , fromVariable @@ -40,6 +41,7 @@ import Control.DeepSeq ) import Control.Lens ( Iso' + , Lens , Lens' ) import qualified Control.Lens as Lens @@ -278,11 +280,16 @@ class where type VariableNameOf variable - lensVariableName :: Lens' variable (VariableNameOf variable) - lensVariableName = isoVariable1 . field @"variableName1" - isoVariable1 :: Iso' variable (Variable1 (VariableNameOf variable)) +lensVariableName + :: (NamedVariable variable1, NamedVariable variable2) + => Lens + variable1 variable2 + (VariableNameOf variable1) (VariableNameOf variable2) +lensVariableName f = + fmap fromVariable1 . field @"variableName1" f . toVariable1 + fromVariable1 :: NamedVariable variable => Variable1 (VariableNameOf variable) diff --git a/kore/src/Kore/Variables/Target.hs b/kore/src/Kore/Variables/Target.hs index 85e08eb082..fbb8323072 100644 --- a/kore/src/Kore/Variables/Target.hs +++ b/kore/src/Kore/Variables/Target.hs @@ -147,14 +147,6 @@ instance instance NamedVariable variable => NamedVariable (Target variable) where type VariableNameOf (Target variable) = Target (VariableNameOf variable) - lensVariableName = - Lens.lens get set - where - get = fmap (Lens.view lensVariableName) - set (unTarget -> variable) = - fmap $ \variableName -> - Lens.set lensVariableName variableName variable - isoVariable1 = Lens.iso to fr where diff --git a/kore/src/Kore/Variables/UnifiedVariable.hs b/kore/src/Kore/Variables/UnifiedVariable.hs index 433eab50fc..03787e8c78 100644 --- a/kore/src/Kore/Variables/UnifiedVariable.hs +++ b/kore/src/Kore/Variables/UnifiedVariable.hs @@ -120,26 +120,6 @@ instance type VariableNameOf (UnifiedVariable variable) = SomeVariableName (VariableNameOf variable) - lensVariableName = - Lens.lens get set - where - get (ElemVar elementVariable) = - SomeVariableNameElement (Lens.view lensVariableName elementVariable) - get (SetVar setVariable) = - SomeVariableNameSet (Lens.view lensVariableName setVariable) - set unifiedVariable someVariableName = - case someVariableName of - SomeVariableNameElement elementVariableName -> - ElementVariable variable - & Lens.set lensVariableName elementVariableName - & ElemVar - SomeVariableNameSet setVariableName -> - SetVariable variable - & Lens.set lensVariableName setVariableName - & SetVar - where - variable = from @_ @variable unifiedVariable - isoVariable1 = Lens.iso to fr where diff --git a/kore/test/Test/Kore/Variables/V.hs b/kore/test/Test/Kore/Variables/V.hs index 593d85caf5..2eee354486 100644 --- a/kore/test/Test/Kore/Variables/V.hs +++ b/kore/test/Test/Kore/Variables/V.hs @@ -53,8 +53,7 @@ instance From V Variable where instance NamedVariable V where type VariableNameOf V = V - lensVariableName f = f - {-# INLINE lensVariableName #-} + isoVariable1 = Lens.iso to fr where diff --git a/kore/test/Test/Kore/Variables/W.hs b/kore/test/Test/Kore/Variables/W.hs index 5225c23d66..404bbd6763 100644 --- a/kore/test/Test/Kore/Variables/W.hs +++ b/kore/test/Test/Kore/Variables/W.hs @@ -56,8 +56,7 @@ instance From W Variable where instance NamedVariable W where type VariableNameOf W = W - lensVariableName f = f - {-# INLINE lensVariableName #-} + isoVariable1 = Lens.iso to fr where From 8a5a3915e7f7926f40699a079d1610b799459b2e Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Sat, 23 May 2020 15:10:13 -0500 Subject: [PATCH 09/16] Add instance From Void _ --- kore/src/From.hs | 6 ++++++ kore/src/Kore/Internal/SideCondition.hs | 10 +++------- kore/src/Kore/Internal/SideCondition/SideCondition.hs | 5 +---- 3 files changed, 10 insertions(+), 11 deletions(-) diff --git a/kore/src/From.hs b/kore/src/From.hs index be562b513d..193843c0d4 100644 --- a/kore/src/From.hs +++ b/kore/src/From.hs @@ -8,6 +8,8 @@ module From ( From (..) ) where +import Data.Void + {- | Convert type @from@ into @to@. Valid instances are /total/. @from@ should be a homomorphism @@ -40,3 +42,7 @@ let b = let a :: A = _ in from @_ @B a -} class From from to where from :: from -> to + +instance From Void any where + from = absurd + {-# INLINE from #-} diff --git a/kore/src/Kore/Internal/SideCondition.hs b/kore/src/Kore/Internal/SideCondition.hs index 71d52e33aa..1274fd9314 100644 --- a/kore/src/Kore/Internal/SideCondition.hs +++ b/kore/src/Kore/Internal/SideCondition.hs @@ -41,12 +41,9 @@ import qualified Kore.Internal.Conditional as Conditional import Kore.Internal.Predicate ( Predicate ) -import qualified Kore.Internal.SideCondition.SideCondition as SideCondition - ( Representation - ) +import Kore.Internal.SideCondition.SideCondition as SideCondition import Kore.Internal.Variable ( InternalVariable - , Variable ) import Kore.TopBottom ( TopBottom (..) @@ -211,9 +208,8 @@ toRepresentationCondition :: InternalVariable variable => Condition variable -> SideCondition.Representation -toRepresentationCondition condition = - from @(Condition Variable) - $ Condition.mapVariables toUnifiedVariable condition +toRepresentationCondition = + mkRepresentation . Condition.mapVariables toUnifiedVariable isNormalized :: forall variable. Ord variable => SideCondition variable -> Bool isNormalized = Conditional.isNormalized . from @_ @(Condition variable) diff --git a/kore/src/Kore/Internal/SideCondition/SideCondition.hs b/kore/src/Kore/Internal/SideCondition/SideCondition.hs index 1ce0b913b6..362971317a 100644 --- a/kore/src/Kore/Internal/SideCondition/SideCondition.hs +++ b/kore/src/Kore/Internal/SideCondition/SideCondition.hs @@ -5,6 +5,7 @@ License : NCSA module Kore.Internal.SideCondition.SideCondition ( Representation + , mkRepresentation ) where import Prelude.Kore @@ -77,7 +78,3 @@ instance Debug Representation where instance Diff Representation where diffPrec _ _ = Nothing {-# INLINE diffPrec #-} - -instance (Ord a, Hashable a, Typeable a) => From a Representation where - from = mkRepresentation - {-# INLINE from #-} From 116f45d9e4c3ef416c0ac4bfbc2375be652c3220 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 26 May 2020 10:45:36 -0500 Subject: [PATCH 10/16] Add instance Injection _ Void --- kore/src/Injection.hs | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/kore/src/Injection.hs b/kore/src/Injection.hs index 88e5e36c7c..d3e5922043 100644 --- a/kore/src/Injection.hs +++ b/kore/src/Injection.hs @@ -20,6 +20,7 @@ import Data.Dynamic , fromDynamic , toDyn ) +import Data.Void {- | The canonical injection or inclusion of @from ↪ into@. @@ -80,3 +81,14 @@ instance Typeable a => Injection Dynamic a where retract = fromDynamic {-# INLINE retract #-} + +{- | 'Void' can be 'inject'ed into any type by the principle of /ex falso +quodlibet/. Because 'Void' contains no data, it can likewise be 'retract'ed +from any type. + -} +instance Injection a Void where + inject = \case {} + {-# INLINE inject #-} + + retract = const Nothing + {-# INLINE retract #-} From 9c3dc0b369d0b214a17384b6e9823410b060800b Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 26 May 2020 09:53:37 -0500 Subject: [PATCH 11/16] Add AdjSomeVariableName --- kore/package.yaml | 2 + kore/src/Kore/Attribute/Axiom.hs | 19 +- kore/src/Kore/Attribute/Axiom/Concrete.hs | 16 +- kore/src/Kore/Attribute/Axiom/Symbolic.hs | 14 +- kore/src/Kore/Attribute/Pattern.hs | 29 +- .../Kore/Attribute/Pattern/FreeVariables.hs | 31 +- .../Kore/Builtin/AssociativeCommutative.hs | 19 +- kore/src/Kore/Builtin/Builtin.hs | 4 +- kore/src/Kore/Builtin/List.hs | 3 +- kore/src/Kore/Equation/Application.hs | 95 ++-- kore/src/Kore/Equation/Equation.hs | 47 +- kore/src/Kore/Internal/Condition.hs | 9 +- kore/src/Kore/Internal/Conditional.hs | 14 +- kore/src/Kore/Internal/OrPattern.hs | 17 +- kore/src/Kore/Internal/Pattern.hs | 10 +- kore/src/Kore/Internal/Predicate.hs | 12 +- kore/src/Kore/Internal/SideCondition.hs | 18 +- kore/src/Kore/Internal/Substitution.hs | 38 +- kore/src/Kore/Internal/TermLike.hs | 8 +- kore/src/Kore/Internal/TermLike/Renaming.hs | 225 +++++++-- kore/src/Kore/Internal/TermLike/TermLike.hs | 242 +++++----- kore/src/Kore/Internal/Variable.hs | 2 +- kore/src/Kore/Log/DebugAppliedRewriteRules.hs | 4 +- .../Kore/Log/ErrorRewritesInstantiation.hs | 3 +- kore/src/Kore/Log/InfoAttemptUnification.hs | 4 +- kore/src/Kore/Log/WarnBottomTotalFunction.hs | 5 +- .../Kore/Log/WarnDecidePredicateUnknown.hs | 3 +- kore/src/Kore/Rewriting/RewritingVariable.hs | 22 +- kore/src/Kore/Rewriting/UnifyingRule.hs | 11 +- .../src/Kore/Step/Axiom/EvaluationStrategy.hs | 7 +- kore/src/Kore/Step/RulePattern.hs | 5 +- kore/src/Kore/Step/Simplification/Builtin.hs | 4 +- .../Kore/Step/Simplification/ExpandAlias.hs | 8 +- kore/src/Kore/Step/Simplification/TermLike.hs | 17 +- kore/src/Kore/Syntax/ElementVariable.hs | 7 - kore/src/Kore/Syntax/Pattern.hs | 41 +- kore/src/Kore/Syntax/PatternF.hs | 31 +- kore/src/Kore/Syntax/SetVariable.hs | 7 - kore/src/Kore/Syntax/Variable.hs | 445 ++++++++++++++---- kore/src/Kore/Unification/Error.hs | 3 +- kore/src/Kore/Variables/Target.hs | 25 +- kore/src/Kore/Variables/UnifiedVariable.hs | 82 +--- kore/test/Test/Kore/Internal/Substitution.hs | 4 +- kore/test/Test/Kore/Internal/TermLike.hs | 38 +- .../Test/Kore/Step/Function/Integration.hs | 4 +- kore/test/Test/Kore/Step/Rule/Simplify.hs | 6 +- .../Test/Kore/Step/Simplification/Ceil.hs | 4 +- kore/test/Test/Kore/Variables/Fresh.hs | 7 +- kore/test/Test/Kore/Variables/V.hs | 6 + kore/test/Test/Kore/Variables/W.hs | 9 +- 50 files changed, 1062 insertions(+), 624 deletions(-) diff --git a/kore/package.yaml b/kore/package.yaml index 99a1cb1e37..10245b919e 100644 --- a/kore/package.yaml +++ b/kore/package.yaml @@ -50,6 +50,7 @@ dependencies: - data-default >=0.7 - deepseq >=1.4 - directory >=1.3 + - distributive >=0.6 - errors >=2.3 - exceptions >=0.10 - extra >=1.6 @@ -127,6 +128,7 @@ default-extensions: - TypeFamilies - TypeOperators - TypeSynonymInstances + - UndecidableInstances - ViewPatterns ghc-options: diff --git a/kore/src/Kore/Attribute/Axiom.hs b/kore/src/Kore/Attribute/Axiom.hs index efbb04e3a1..0dbb1f0843 100644 --- a/kore/src/Kore/Attribute/Axiom.hs +++ b/kore/src/Kore/Attribute/Axiom.hs @@ -86,10 +86,9 @@ import Kore.Internal.Symbol ( Symbol (..) , toSymbolOrAlias ) -import Kore.Syntax.Variable - ( Variable (..) +import Kore.Syntax.Variable hiding + ( Concrete ) -import Kore.Variables.UnifiedVariable import qualified SQL {- | Attributes specific to Kore axiom sentences. @@ -265,13 +264,15 @@ parseAxiomAttributes freeVariables (Attributes attrs) = Foldable.foldlM (flip $ parseAxiomAttribute freeVariables) Default.def attrs mapAxiomVariables - :: Ord variable2 - => AdjUnifiedVariable (variable1 -> variable2) - -> Axiom symbol variable1 -> Axiom symbol variable2 -mapAxiomVariables mapping axiom@Axiom { concrete, symbolic } = + :: (NamedVariable variable1, NamedVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> Axiom symbol variable1 + -> Axiom symbol variable2 +mapAxiomVariables adj axiom@Axiom { concrete, symbolic } = axiom - { concrete = mapConcreteVariables mapping concrete - , symbolic = mapSymbolicVariables mapping symbolic + { concrete = mapConcreteVariables adj concrete + , symbolic = mapSymbolicVariables adj symbolic } getPriorityOfAxiom diff --git a/kore/src/Kore/Attribute/Axiom/Concrete.hs b/kore/src/Kore/Attribute/Axiom/Concrete.hs index bf60682c38..58238e2ac7 100644 --- a/kore/src/Kore/Attribute/Axiom/Concrete.hs +++ b/kore/src/Kore/Attribute/Axiom/Concrete.hs @@ -35,8 +35,8 @@ import Kore.Attribute.Pattern.FreeVariables import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables import Kore.Debug import qualified Kore.Error -import Kore.Syntax.Variable - ( Variable +import Kore.Syntax.Variable hiding + ( Concrete ) import Kore.Variables.UnifiedVariable @@ -129,11 +129,13 @@ instance From (Concrete Variable) Attributes where . unConcrete mapConcreteVariables - :: Ord variable2 - => AdjUnifiedVariable (variable1 -> variable2) - -> Concrete variable1 -> Concrete variable2 -mapConcreteVariables morphism (Concrete freeVariables) = - Concrete (mapFreeVariables morphism freeVariables) + :: (NamedVariable variable1, NamedVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> Concrete variable1 + -> Concrete variable2 +mapConcreteVariables adj (Concrete freeVariables) = + Concrete (mapFreeVariables adj freeVariables) isConcrete :: Ord variable => Concrete variable -> UnifiedVariable variable -> Bool diff --git a/kore/src/Kore/Attribute/Axiom/Symbolic.hs b/kore/src/Kore/Attribute/Axiom/Symbolic.hs index 2ef2a72b8a..c7abc59a66 100644 --- a/kore/src/Kore/Attribute/Axiom/Symbolic.hs +++ b/kore/src/Kore/Attribute/Axiom/Symbolic.hs @@ -31,8 +31,6 @@ import Kore.Attribute.Pattern.FreeVariables import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables import Kore.Debug import Kore.Syntax.Variable - ( Variable - ) import Kore.Variables.UnifiedVariable {- | @Symbolic@ represents the @symbolic@ attribute for axioms. @@ -93,11 +91,13 @@ instance From (Symbolic Variable) Attributes where . unSymbolic mapSymbolicVariables - :: Ord variable2 - => AdjUnifiedVariable (variable1 -> variable2) - -> Symbolic variable1 -> Symbolic variable2 -mapSymbolicVariables morphism (Symbolic freeVariables) = - Symbolic (mapFreeVariables morphism freeVariables) + :: (NamedVariable variable1, NamedVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> Symbolic variable1 + -> Symbolic variable2 +mapSymbolicVariables adj (Symbolic freeVariables) = + Symbolic (mapFreeVariables adj freeVariables) isSymbolic :: Ord variable => Symbolic variable -> UnifiedVariable variable -> Bool diff --git a/kore/src/Kore/Attribute/Pattern.hs b/kore/src/Kore/Attribute/Pattern.hs index baeff8cec8..4448bed7bb 100644 --- a/kore/src/Kore/Attribute/Pattern.hs +++ b/kore/src/Kore/Attribute/Pattern.hs @@ -63,6 +63,7 @@ import qualified Kore.Internal.SideCondition.SideCondition as SideCondition import Kore.Sort ( Sort ) +import Kore.Syntax.Variable import Kore.Variables.UnifiedVariable {- | @Pattern@ are the attributes of a pattern collected during verification. @@ -172,12 +173,14 @@ See also: 'traverseVariables' -} mapVariables - :: Ord variable2 - => AdjUnifiedVariable (variable1 -> variable2) - -> Pattern variable1 -> Pattern variable2 -mapVariables morphism = + :: (NamedVariable variable1, NamedVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> Pattern variable1 + -> Pattern variable2 +mapVariables adj = Lens.over (field @"freeVariables") - (mapFreeVariables morphism) + (mapFreeVariables adj) {- | Use the provided traversal to replace the free variables in a 'Pattern'. @@ -185,13 +188,15 @@ See also: 'mapVariables' -} traverseVariables - :: forall m variable1 variable2 - . (Monad m, Ord variable2) - => AdjUnifiedVariable (variable1 -> m variable2) - -> Pattern variable1 - -> m (Pattern variable2) -traverseVariables morphism = - field @"freeVariables" (traverseFreeVariables morphism) + :: forall m variable1 variable2 + . Monad m + => (NamedVariable variable1, NamedVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> m (VariableNameOf variable2)) + -> Pattern variable1 + -> m (Pattern variable2) +traverseVariables adj = + field @"freeVariables" (traverseFreeVariables adj) {- | Delete the given variable from the set of free variables. -} diff --git a/kore/src/Kore/Attribute/Pattern/FreeVariables.hs b/kore/src/Kore/Attribute/Pattern/FreeVariables.hs index f89e031906..20fe05712a 100644 --- a/kore/src/Kore/Attribute/Pattern/FreeVariables.hs +++ b/kore/src/Kore/Attribute/Pattern/FreeVariables.hs @@ -28,13 +28,13 @@ import Data.Set ( Set ) import qualified Data.Set as Set -import qualified Data.Traversable as Traversable import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC import Kore.Attribute.Synthetic import Kore.Debug import Kore.Syntax.ElementVariable +import Kore.Syntax.Variable import Kore.Variables.UnifiedVariable newtype FreeVariables variable = @@ -74,6 +74,10 @@ toList :: FreeVariables variable -> [UnifiedVariable variable] toList = Set.toList . getFreeVariables {-# INLINE toList #-} +fromList :: Ord variable => [UnifiedVariable variable] -> FreeVariables variable +fromList = foldMap freeVariable +{-# INLINE fromList #-} + toSet :: FreeVariables variable -> Set (UnifiedVariable variable) toSet = getFreeVariables {-# INLINE toSet #-} @@ -113,22 +117,21 @@ freeVariable variable = FreeVariables (Set.singleton variable) {-# INLINE freeVariable #-} mapFreeVariables - :: Ord variable2 - => AdjUnifiedVariable (variable1 -> variable2) - -> FreeVariables variable1 -> FreeVariables variable2 -mapFreeVariables morphism (FreeVariables freeVars) = - FreeVariables (Set.map (mapUnifiedVariable morphism) freeVars) + :: (NamedVariable variable1, NamedVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> FreeVariables variable1 -> FreeVariables variable2 +mapFreeVariables adj = fromList . map (mapUnifiedVariable adj) . toList {-# INLINE mapFreeVariables #-} traverseFreeVariables - :: (Applicative f, Ord variable2) - => AdjUnifiedVariable (variable1 -> f variable2) - -> FreeVariables variable1 -> f (FreeVariables variable2) -traverseFreeVariables morphism (FreeVariables freeVars) = - FreeVariables . Set.fromList - <$> Traversable.traverse traversal (Set.toList freeVars) - where - traversal = traverseUnifiedVariable morphism + :: Applicative f + => (NamedVariable variable1, NamedVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> f (VariableNameOf variable2)) + -> FreeVariables variable1 -> f (FreeVariables variable2) +traverseFreeVariables adj = + fmap fromList . traverse (traverseUnifiedVariable adj) . toList {-# INLINE traverseFreeVariables #-} {- | Extracts the list of free element variables diff --git a/kore/src/Kore/Builtin/AssociativeCommutative.hs b/kore/src/Kore/Builtin/AssociativeCommutative.hs index 940c95252e..538808e938 100644 --- a/kore/src/Kore/Builtin/AssociativeCommutative.hs +++ b/kore/src/Kore/Builtin/AssociativeCommutative.hs @@ -99,6 +99,7 @@ import Kore.Internal.TermLike , Concrete , pattern ElemVar_ , InternalVariable + , NamedVariable , TermLike , mkApplySymbol , mkBuiltin @@ -158,7 +159,7 @@ class @ -} toNormalized - :: Ord variable + :: NamedVariable variable => TermLike variable -> NormalizedOrBottom normalized variable @@ -355,7 +356,7 @@ deriving instance {- | The semigroup defined by the `concat` operation. -} instance - (Ord variable, TermWrapper normalized) + (NamedVariable variable, TermWrapper normalized) => Semigroup (NormalizedOrBottom normalized variable) where Bottom <> _ = Bottom @@ -365,7 +366,7 @@ instance concatNormalized :: forall normalized variable - . (TermWrapper normalized, Ord variable) + . (TermWrapper normalized, NamedVariable variable) => normalized (TermLike Concrete) (TermLike variable) -> normalized (TermLike Concrete) (TermLike variable) -> Maybe (normalized (TermLike Concrete) (TermLike variable)) @@ -406,7 +407,7 @@ internal representations themselves; this "flattening" step also recurses to -} renormalize - :: (TermWrapper normalized, Ord variable) + :: (TermWrapper normalized, NamedVariable variable) => normalized (TermLike Concrete) (TermLike variable) -> Maybe (normalized (TermLike Concrete) (TermLike variable)) renormalize = normalizeAbstractElements >=> flattenOpaque @@ -457,7 +458,7 @@ Return 'Nothing' if there are any duplicate (concrete or abstract) keys. -} normalizeAbstractElements - :: (TermWrapper normalized, Ord variable) + :: (TermWrapper normalized, NamedVariable variable) => normalized (TermLike Concrete) (TermLike variable) -> Maybe (normalized (TermLike Concrete) (TermLike variable)) normalizeAbstractElements (Domain.unwrapAc -> normalized) = do @@ -478,7 +479,7 @@ normalizeAbstractElements (Domain.unwrapAc -> normalized) = do -- remains abstract. extractConcreteElement :: Domain.AcWrapper collection - => Ord variable + => NamedVariable variable => Domain.Element collection (TermLike variable) -> Either (TermLike Concrete, Domain.Value collection (TermLike variable)) @@ -494,7 +495,7 @@ extractConcreteElement element = -} flattenOpaque - :: (TermWrapper normalized, Ord variable) + :: (TermWrapper normalized, NamedVariable variable) => normalized (TermLike Concrete) (TermLike variable) -> Maybe (normalized (TermLike Concrete) (TermLike variable)) flattenOpaque (Domain.unwrapAc -> normalized) = do @@ -509,7 +510,7 @@ flattenOpaque (Domain.unwrapAc -> normalized) = do {- | The monoid defined by the `concat` and `unit` operations. -} instance - (Ord variable, TermWrapper normalized) + (NamedVariable variable, TermWrapper normalized) => Monoid (NormalizedOrBottom normalized variable) where mempty = Normalized $ Domain.wrapAc Domain.emptyNormalizedAc @@ -680,7 +681,7 @@ disjointMap input = splitVariableConcrete :: forall variable a - . Ord variable + . NamedVariable variable => [(TermLike variable, a)] -> ([(TermLike variable, a)], [(TermLike Concrete, a)]) splitVariableConcrete terms = diff --git a/kore/src/Kore/Builtin/Builtin.hs b/kore/src/Kore/Builtin/Builtin.hs index 429d358db4..3227298e05 100644 --- a/kore/src/Kore/Builtin/Builtin.hs +++ b/kore/src/Kore/Builtin/Builtin.hs @@ -463,7 +463,9 @@ If the pattern is not concrete and normalized, the function is See also: 'Kore.Proof.Value.Value' -} -toKey :: Ord variable => TermLike variable -> Maybe (TermLike Concrete) +toKey + :: NamedVariable variable + => TermLike variable -> Maybe (TermLike Concrete) toKey purePattern = do p <- TermLike.asConcrete purePattern -- TODO (thomas.tuegel): Use the return value as the term. diff --git a/kore/src/Kore/Builtin/List.hs b/kore/src/Kore/Builtin/List.hs index 094ddcbc94..cacd590d45 100644 --- a/kore/src/Kore/Builtin/List.hs +++ b/kore/src/Kore/Builtin/List.hs @@ -95,6 +95,7 @@ import Kore.Internal.TermLike , Concrete , pattern ElemVar_ , InternalVariable + , NamedVariable , Sort , TermLike , pattern Var_ @@ -225,7 +226,7 @@ expectBuiltinList ctx = _ -> empty expectConcreteBuiltinList - :: Ord variable + :: NamedVariable variable => Monad m => Text -- ^ Context for error message -> TermLike variable -- ^ Operand pattern diff --git a/kore/src/Kore/Equation/Application.hs b/kore/src/Kore/Equation/Application.hs index f50445a761..3c73f2f541 100644 --- a/kore/src/Kore/Equation/Application.hs +++ b/kore/src/Kore/Equation/Application.hs @@ -99,7 +99,10 @@ import Kore.Syntax.Id , FileLocation (..) ) import Kore.Syntax.Variable - ( Variable + ( AdjSomeVariableName + , NamedVariable (..) + , Variable + , toVariableName ) import Kore.TopBottom import Kore.Unparser @@ -355,10 +358,11 @@ data AttemptEquationError variable deriving (GHC.Generic) mapAttemptEquationErrorVariables - :: (InternalVariable variable1, InternalVariable variable2) - => AdjUnifiedVariable (variable1 -> variable2) - -> AttemptEquationError variable1 - -> AttemptEquationError variable2 + :: (InternalVariable variable1, InternalVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> AttemptEquationError variable1 + -> AttemptEquationError variable2 mapAttemptEquationErrorVariables adj = \case WhileMatch matchError -> @@ -433,15 +437,16 @@ instance InternalVariable variable => Pretty (MatchError variable) where pretty _ = "equation did not match term" mapMatchErrorVariables - :: (InternalVariable variable1, InternalVariable variable2) - => AdjUnifiedVariable (variable1 -> variable2) - -> MatchError variable1 - -> MatchError variable2 -mapMatchErrorVariables mapping = + :: (InternalVariable variable1, InternalVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> MatchError variable1 + -> MatchError variable2 +mapMatchErrorVariables adj = \MatchError { matchTerm, matchEquation } -> MatchError - { matchTerm = TermLike.mapVariables mapping matchTerm - , matchEquation = Equation.mapVariables mapping matchEquation + { matchTerm = TermLike.mapVariables adj matchTerm + , matchEquation = Equation.mapVariables adj matchEquation } {- | Errors that can occur during 'applyMatchResult'. @@ -481,14 +486,14 @@ instance mapApplyMatchResultErrorsVariables :: (InternalVariable variable1, InternalVariable variable2) - => AdjUnifiedVariable (variable1 -> variable2) + => AdjSomeVariableName (VariableNameOf variable1 -> VariableNameOf variable2) -> ApplyMatchResultErrors variable1 -> ApplyMatchResultErrors variable2 -mapApplyMatchResultErrorsVariables mapping applyMatchResultErrors = +mapApplyMatchResultErrorsVariables adj applyMatchResultErrors = ApplyMatchResultErrors - { matchResult = mapMatchResultVariables mapping matchResult + { matchResult = mapMatchResultVariables adj matchResult , applyMatchErrors = - mapApplyMatchResultErrorVariables mapping <$> applyMatchErrors + mapApplyMatchResultErrorVariables adj <$> applyMatchErrors } where ApplyMatchResultErrors { matchResult, applyMatchErrors } = @@ -496,17 +501,17 @@ mapApplyMatchResultErrorsVariables mapping applyMatchResultErrors = mapMatchResultVariables :: (InternalVariable variable1, InternalVariable variable2) - => AdjUnifiedVariable (variable1 -> variable2) + => AdjSomeVariableName (VariableNameOf variable1 -> VariableNameOf variable2) -> MatchResult variable1 -> MatchResult variable2 -mapMatchResultVariables mapping (predicate, substitution) = - ( Predicate.mapVariables mapping predicate +mapMatchResultVariables adj (predicate, substitution) = + ( Predicate.mapVariables adj predicate , mapSubstitutionVariables substitution ) where mapSubstitutionVariables = - Map.mapKeys (mapUnifiedVariable mapping) - . Map.map (TermLike.mapVariables mapping) + Map.mapKeys (mapUnifiedVariable adj) + . Map.map (TermLike.mapVariables adj) {- | @ApplyMatchResultError@ represents a reason the match could not be applied. -} @@ -553,10 +558,10 @@ instance mapApplyMatchResultErrorVariables :: (InternalVariable variable1, InternalVariable variable2) - => AdjUnifiedVariable (variable1 -> variable2) + => AdjSomeVariableName (VariableNameOf variable1 -> VariableNameOf variable2) -> ApplyMatchResultError variable1 -> ApplyMatchResultError variable2 -mapApplyMatchResultErrorVariables mapping applyMatchResultError = +mapApplyMatchResultErrorVariables adj applyMatchResultError = case applyMatchResultError of NotConcrete variable termLike -> NotConcrete @@ -568,8 +573,8 @@ mapApplyMatchResultErrorVariables mapping applyMatchResultError = (mapTermLikeVariables termLike) NotMatched variable -> NotMatched (mapUnifiedVariable' variable) where - mapUnifiedVariable' = mapUnifiedVariable mapping - mapTermLikeVariables = TermLike.mapVariables mapping + mapUnifiedVariable' = mapUnifiedVariable adj + mapTermLikeVariables = TermLike.mapVariables adj {- | Errors that can occur during 'checkRequires'. -} @@ -599,17 +604,18 @@ instance InternalVariable variable => Pretty (CheckRequiresError variable) where ] mapCheckRequiresErrorVariables - :: (InternalVariable variable1, InternalVariable variable2) - => AdjUnifiedVariable (variable1 -> variable2) - -> CheckRequiresError variable1 - -> CheckRequiresError variable2 -mapCheckRequiresErrorVariables mapping checkRequiresError = + :: (InternalVariable variable1, InternalVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> CheckRequiresError variable1 + -> CheckRequiresError variable2 +mapCheckRequiresErrorVariables adj checkRequiresError = CheckRequiresError { matchPredicate = mapPredicateVariables matchPredicate , equationRequires = mapPredicateVariables equationRequires } where - mapPredicateVariables = Predicate.mapVariables mapping + mapPredicateVariables = Predicate.mapVariables adj CheckRequiresError { matchPredicate, equationRequires } = checkRequiresError -- * Logging @@ -665,18 +671,19 @@ debugAttemptEquationResult -> log () debugAttemptEquationResult equation result = logEntry $ DebugAttemptEquationResult - (Equation.mapVariables toUnifiedVariable equation) - (mapAttemptEquationResultVariables toUnifiedVariable result) + (Equation.mapVariables (pure toVariableName) equation) + (mapAttemptEquationResultVariables (pure toVariableName) result) mapAttemptEquationResultVariables - :: (InternalVariable variable1, InternalVariable variable2) - => AdjUnifiedVariable (variable1 -> variable2) - -> AttemptEquationResult variable1 - -> AttemptEquationResult variable2 -mapAttemptEquationResultVariables mapping = + :: (InternalVariable variable1, InternalVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> AttemptEquationResult variable1 + -> AttemptEquationResult variable2 +mapAttemptEquationResultVariables adj = Bifunctor.bimap - (mapAttemptEquationErrorVariables mapping) - (Pattern.mapVariables mapping) + (mapAttemptEquationErrorVariables adj) + (Pattern.mapVariables adj) whileDebugAttemptEquation :: MonadLog log @@ -688,8 +695,8 @@ whileDebugAttemptEquation whileDebugAttemptEquation termLike equation = logWhile (DebugAttemptEquation equation' termLike') where - termLike' = TermLike.mapVariables toUnifiedVariable termLike - equation' = Equation.mapVariables toUnifiedVariable equation + termLike' = TermLike.mapVariables (pure toVariableName) termLike + equation' = Equation.mapVariables (pure toVariableName) equation {- | Log when an 'Equation' is actually applied. -} @@ -745,5 +752,5 @@ debugApplyEquation debugApplyEquation equation result = logEntry $ DebugApplyEquation equation' result' where - equation' = Equation.mapVariables toUnifiedVariable equation - result' = Pattern.mapVariables toUnifiedVariable result + equation' = Equation.mapVariables (pure toVariableName) equation + result' = Pattern.mapVariables (pure toVariableName) result diff --git a/kore/src/Kore/Equation/Equation.hs b/kore/src/Kore/Equation/Equation.hs index ab59e00a7d..1bd164b1e0 100644 --- a/kore/src/Kore/Equation/Equation.hs +++ b/kore/src/Kore/Equation/Equation.hs @@ -34,6 +34,7 @@ import qualified Data.Map.Strict as Map import Data.Set ( Set ) +import qualified Data.Set as Set import Data.Text ( Text ) @@ -71,6 +72,7 @@ import Kore.Step.Step import Kore.Syntax.Application ( Application (..) ) +import Kore.Syntax.Variable import Kore.TopBottom import Kore.Unparser ( Unparse (..) @@ -198,9 +200,11 @@ instance AstWithLocation variable => AstWithLocation (Equation variable) where locationFromAst = locationFromAst . left mapVariables - :: (Ord variable1, InternalVariable variable2) - => AdjUnifiedVariable (variable1 -> variable2) - -> Equation variable1 -> Equation variable2 + :: (NamedVariable variable1, InternalVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> Equation variable1 + -> Equation variable2 mapVariables mapping equation@(Equation _ _ _ _ _) = equation { requires = mapPredicateVariables requires @@ -224,21 +228,32 @@ refreshVariables (from @_ @(Set (UnifiedVariable _)) -> avoid) equation@(Equation _ _ _ _ _) = - let rename = Fresh.refreshVariables avoid originalFreeVariables + let rename = + Fresh.refreshVariables avoid originalFreeVariables + rename' = + rename + & Map.map (Lens.view lensVariableName) + & Map.mapKeys (Lens.view lensVariableName) adj = - AdjUnifiedVariable - { elemVar = - ElementVariable . Lens.over _Wrapped $ \var -> - case Map.lookup (ElemVar var) rename of - Just (ElemVar var') -> var' - _ -> var - , setVar = - SetVariable . Lens.over _Wrapped $ \var -> - case Map.lookup (SetVar var) rename of - Just (SetVar var') -> var' - _ -> var + AdjSomeVariableName + { adjSomeVariableNameElement = + ElementVariableName . Lens.over _Wrapped $ \variable -> + case Map.lookup (inject @(SomeVariableName _) variable) rename' of + Just (SomeVariableNameElement variable') -> variable' + _ -> variable + , adjSomeVariableNameSet = + SetVariableName . Lens.over _Wrapped $ \variable -> + case Map.lookup (inject @(SomeVariableName _) variable) rename' of + Just (SomeVariableNameSet variable') -> variable' + _ -> variable + } - subst = TermLike.mkVar <$> rename + subst = + Set.toList originalFreeVariables + & map mkSubst + & Map.fromList + mkSubst variable = + (variable, TermLike.mkVar (mapUnifiedVariable adj variable)) left' = TermLike.substitute subst left requires' = Predicate.substitute subst requires right' = TermLike.substitute subst right diff --git a/kore/src/Kore/Internal/Condition.hs b/kore/src/Kore/Internal/Condition.hs index b9a294f303..463e25e768 100644 --- a/kore/src/Kore/Internal/Condition.hs +++ b/kore/src/Kore/Internal/Condition.hs @@ -159,10 +159,11 @@ toPredicate toPredicate = from mapVariables - :: (InternalVariable variable1, InternalVariable variable2) - => AdjUnifiedVariable (variable1 -> variable2) - -> Condition variable1 - -> Condition variable2 + :: (InternalVariable variable1, InternalVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> Condition variable1 + -> Condition variable2 mapVariables = Conditional.mapVariables (\_ () -> ()) {- | Create a new 'Condition' from the 'Normalization' of a substitution. diff --git a/kore/src/Kore/Internal/Conditional.hs b/kore/src/Kore/Internal/Conditional.hs index 3a15100fbe..387881f26d 100644 --- a/kore/src/Kore/Internal/Conditional.hs +++ b/kore/src/Kore/Internal/Conditional.hs @@ -62,7 +62,9 @@ import Kore.Internal.Substitution import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.TermLike ( InternalVariable + , NamedVariable , Sort + , SubstitutionOrd , TermLike , termLikeSort ) @@ -103,11 +105,11 @@ data Conditional variable child = deriving (Foldable, Functor, GHC.Generic, Traversable) deriving instance - (Eq child, InternalVariable variable) => + (Eq child, NamedVariable variable, SubstitutionOrd variable) => Eq (Conditional variable child) deriving instance - (Ord child, InternalVariable variable) => + (Ord child, NamedVariable variable, SubstitutionOrd variable) => Ord (Conditional variable child) deriving instance @@ -436,13 +438,13 @@ mapVariables (Conditional variableTo termTo) mapVariables mapTermVariables - mapping + adj Conditional { term, predicate, substitution } = Conditional - { term = mapTermVariables mapping term - , predicate = Predicate.mapVariables mapping predicate - , substitution = Substitution.mapVariables mapping substitution + { term = mapTermVariables adj term + , predicate = Predicate.mapVariables adj predicate + , substitution = Substitution.mapVariables adj substitution } splitTerm :: Conditional variable term -> (term, Conditional variable ()) diff --git a/kore/src/Kore/Internal/OrPattern.hs b/kore/src/Kore/Internal/OrPattern.hs index d6c796cc3d..6d676361ca 100644 --- a/kore/src/Kore/Internal/OrPattern.hs +++ b/kore/src/Kore/Internal/OrPattern.hs @@ -27,11 +27,7 @@ module Kore.Internal.OrPattern import Prelude.Kore -import qualified Control.Lens as Lens import qualified Data.Foldable as Foldable -import Data.Generics.Wrapped - ( _Wrapped - ) import Branch ( BranchT @@ -64,6 +60,7 @@ import Kore.Internal.TermLike , mkBottom_ , mkOr ) +import Kore.Syntax.Variable import Kore.TopBottom ( TopBottom (..) ) @@ -75,7 +72,6 @@ import Kore.Variables.Target , mkElementTarget , targetIfEqual ) -import Kore.Variables.UnifiedVariable {-| The disjunction of 'Pattern'. -} @@ -216,14 +212,13 @@ targetBinder -> Binder (ElementVariable (Target variable)) (OrPattern (Target variable)) targetBinder Binder { binderVariable, binderChild } = let newVar = mkElementTarget binderVariable - targetBoundVariables = - targetIfEqual binderVariable + targetBoundVariables = targetIfEqual binderVariable newChild = Pattern.mapVariables - AdjUnifiedVariable - { elemVar = - (ElementVariable . Lens.over _Wrapped) targetBoundVariables - , setVar = SetVariable NonTarget + AdjSomeVariableName + { adjSomeVariableNameElement = + ElementVariableName targetBoundVariables + , adjSomeVariableNameSet = SetVariableName NonTarget } <$> binderChild in Binder diff --git a/kore/src/Kore/Internal/Pattern.hs b/kore/src/Kore/Internal/Pattern.hs index 2ad142a556..e7fdd26977 100644 --- a/kore/src/Kore/Internal/Pattern.hs +++ b/kore/src/Kore/Internal/Pattern.hs @@ -77,6 +77,7 @@ import qualified Kore.Internal.TermLike as TermLike import qualified Kore.Sort as Sort ( predicateSort ) +import Kore.Syntax.Variable import Kore.TopBottom ( TopBottom (..) ) @@ -131,10 +132,11 @@ freeElementVariables = in an Pattern. -} mapVariables - :: (InternalVariable variable1, InternalVariable variable2) - => AdjUnifiedVariable (variable1 -> variable2) - -> Pattern variable1 - -> Pattern variable2 + :: (InternalVariable variable1, InternalVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> Pattern variable1 + -> Pattern variable2 mapVariables adj Conditional { term, predicate, substitution } = Conditional { term = TermLike.mapVariables adj term diff --git a/kore/src/Kore/Internal/Predicate.hs b/kore/src/Kore/Internal/Predicate.hs index 9795ec6b52..ef8a77f64a 100644 --- a/kore/src/Kore/Internal/Predicate.hs +++ b/kore/src/Kore/Internal/Predicate.hs @@ -732,10 +732,12 @@ isPredicate = Either.isRight . makePredicate {- | Replace all variables in a @Predicate@ using the provided mapping. -} mapVariables - :: (Ord variable1, FreshPartialOrd variable2, NamedVariable variable2) - => AdjUnifiedVariable (variable1 -> variable2) - -> Predicate variable1 - -> Predicate variable2 + :: (NamedVariable variable1, NamedVariable variable2) + => FreshPartialOrd variable2 + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> Predicate variable1 + -> Predicate variable2 mapVariables adj = fmap (TermLike.mapVariables adj) instance HasFreeVariables (Predicate variable) variable where @@ -838,7 +840,7 @@ externalizeFreshVariables -> Predicate Variable externalizeFreshVariables predicate = TermLike.externalizeFreshVariables - . TermLike.mapVariables toUnifiedVariable + . TermLike.mapVariables (pure toVariableName) <$> predicate depth :: Predicate variable -> Int diff --git a/kore/src/Kore/Internal/SideCondition.hs b/kore/src/Kore/Internal/SideCondition.hs index 1274fd9314..bbaee63558 100644 --- a/kore/src/Kore/Internal/SideCondition.hs +++ b/kore/src/Kore/Internal/SideCondition.hs @@ -45,13 +45,13 @@ import Kore.Internal.SideCondition.SideCondition as SideCondition import Kore.Internal.Variable ( InternalVariable ) +import Kore.Syntax.Variable import Kore.TopBottom ( TopBottom (..) ) import Kore.Unparser ( Unparse (..) ) -import Kore.Variables.UnifiedVariable import qualified Pretty import qualified SQL @@ -187,12 +187,13 @@ toRepresentation :: SideCondition variable -> SideCondition.Representation toRepresentation SideCondition { representation } = representation mapVariables - :: (InternalVariable variable1, InternalVariable variable2) - => AdjUnifiedVariable (variable1 -> variable2) - -> SideCondition variable1 - -> SideCondition variable2 -mapVariables mapping condition@(SideCondition _ _) = - fromCondition (Condition.mapVariables mapping assumedTrue) + :: (InternalVariable variable1, InternalVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> SideCondition variable1 + -> SideCondition variable2 +mapVariables adj condition@(SideCondition _ _) = + fromCondition (Condition.mapVariables adj assumedTrue) where SideCondition { assumedTrue } = condition @@ -209,7 +210,8 @@ toRepresentationCondition => Condition variable -> SideCondition.Representation toRepresentationCondition = - mkRepresentation . Condition.mapVariables toUnifiedVariable + mkRepresentation + . Condition.mapVariables @_ @Variable (pure toVariableName) isNormalized :: forall variable. Ord variable => SideCondition variable -> Bool isNormalized = Conditional.isNormalized . from @_ @(Condition variable) diff --git a/kore/src/Kore/Internal/Substitution.hs b/kore/src/Kore/Internal/Substitution.hs index 0a969df343..ae149b2e27 100644 --- a/kore/src/Kore/Internal/Substitution.hs +++ b/kore/src/Kore/Internal/Substitution.hs @@ -124,7 +124,7 @@ instance Hashable variable => Hashable (Assignment variable) -- that for variable renaming, the smaller variable will be on the -- left of the substitution. assign - :: InternalVariable variable + :: (NamedVariable variable, SubstitutionOrd variable) => UnifiedVariable variable -> TermLike variable -> Assignment variable @@ -154,7 +154,7 @@ mapAssignedTerm f (Assignment variable term) = assign variable (f term) mkUnwrappedSubstitution - :: InternalVariable variable + :: (NamedVariable variable, SubstitutionOrd variable) => [(UnifiedVariable variable, TermLike variable)] -> [Assignment variable] mkUnwrappedSubstitution = fmap (uncurry assign) @@ -183,11 +183,17 @@ data Substitution variable deriving GHC.Generic -- | 'Eq' does not differentiate normalized and denormalized 'Substitution's. -instance InternalVariable variable => Eq (Substitution variable) where +instance + (NamedVariable variable, SubstitutionOrd variable) + => Eq (Substitution variable) + where (==) = on (==) unwrap -- | 'Ord' does not differentiate normalized and denormalized 'Substitution's. -instance InternalVariable variable => Ord (Substitution variable) where +instance + (NamedVariable variable, SubstitutionOrd variable) + => Ord (Substitution variable) + where compare = on compare unwrap instance SOP.Generic (Substitution variable) @@ -285,7 +291,7 @@ type UnwrappedSubstitution variable = [Assignment variable] -- | Unwrap the 'Substitution' to its inner list of substitutions. unwrap - :: InternalVariable variable + :: (NamedVariable variable, SubstitutionOrd variable) => Substitution variable -> [Assignment variable] unwrap (Substitution xs) = @@ -352,7 +358,7 @@ cycles. -} normalOrder - :: InternalVariable variable + :: (NamedVariable variable, SubstitutionOrd variable) => (UnifiedVariable variable, TermLike variable) -> (UnifiedVariable variable, TermLike variable) normalOrder (uVar1, Var_ uVar2) @@ -440,10 +446,11 @@ modify modify f = wrap . f . unwrap mapAssignmentVariables - :: (InternalVariable variable1, InternalVariable variable2) - => AdjUnifiedVariable (variable1 -> variable2) - -> Assignment variable1 - -> Assignment variable2 + :: (InternalVariable variable1, InternalVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> Assignment variable1 + -> Assignment variable2 mapAssignmentVariables adj (Assignment variable term) = assign mappedVariable mappedTerm where @@ -453,11 +460,12 @@ mapAssignmentVariables adj (Assignment variable term) = -- | 'mapVariables' changes all the variables in the substitution -- with the given function. mapVariables - :: forall variable1 variable2 - . (InternalVariable variable1, InternalVariable variable2) - => AdjUnifiedVariable (variable1 -> variable2) - -> Substitution variable1 - -> Substitution variable2 + :: forall variable1 variable2 + . (InternalVariable variable1, InternalVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> Substitution variable1 + -> Substitution variable2 mapVariables adj = modify . fmap $ mapAssignmentVariables adj mapTerms diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index 8141301846..eb0adc7b6a 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -399,12 +399,12 @@ deciding if the result is @Nothing@ or @Just _@. -} asConcrete - :: Ord variable + :: NamedVariable variable => TermLike variable -> Maybe (TermLike Concrete) -asConcrete = traverseVariables asConcreteUnifiedVariable +asConcrete = traverseVariables (pure toVoid) -isConcrete :: Ord variable => TermLike variable -> Bool +isConcrete :: NamedVariable variable => TermLike variable -> Bool isConcrete = isJust . asConcrete {- | Construct any 'TermLike' from a @'TermLike' 'Concrete'@. @@ -420,7 +420,7 @@ fromConcrete :: (FreshPartialOrd variable, NamedVariable variable) => TermLike Concrete -> TermLike variable -fromConcrete = mapVariables fromConcreteUnifiedVariable +fromConcrete = mapVariables (pure $ from @Void) isSimplified :: SideCondition.Representation -> TermLike variable -> Bool isSimplified sideCondition = diff --git a/kore/src/Kore/Internal/TermLike/Renaming.hs b/kore/src/Kore/Internal/TermLike/Renaming.hs index d0103b7e53..ab4b03f12f 100644 --- a/kore/src/Kore/Internal/TermLike/Renaming.hs +++ b/kore/src/Kore/Internal/TermLike/Renaming.hs @@ -7,11 +7,18 @@ License : NCSA module Kore.Internal.TermLike.Renaming ( RenamingT , Renaming + , VariableNameMap , renameFreeVariables + , renameElementBinder + , renameSetBinder + , renameElementVariable + , renameSetVariable + , askSomeVariableName + , askElementVariableName + , askSetVariableName , askUnifiedVariable , askElementVariable , askSetVariable - , module Kore.Variables.UnifiedVariable ) where import Prelude.Kore @@ -19,77 +26,207 @@ import Prelude.Kore import Control.Comonad.Trans.Env ( Env ) +import qualified Control.Lens as Lens import qualified Control.Monad as Monad import Control.Monad.Reader - ( ReaderT + ( MonadReader + , ReaderT ) import qualified Control.Monad.Reader as Reader -import qualified Data.Maybe as Maybe +import Data.Functor.Adjunction + ( splitL + ) +import Data.Functor.Rep + ( Representable (..) + ) +import Data.Map.Strict + ( Map + ) +import qualified Data.Map.Strict as Map import Kore.Attribute.Pattern.FreeVariables ( FreeVariables ) import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables import Kore.Internal.Variable +import Kore.Variables.Binding import Kore.Variables.UnifiedVariable + ( UnifiedVariable + , refreshElementVariable + , refreshSetVariable + ) + +type VariableNameMap' variable1 variable2 = + AdjSomeVariableName (Map variable1 variable2) + +type VariableNameMap variable1 variable2 = + VariableNameMap' (VariableNameOf variable1) (VariableNameOf variable2) + +type RenamingT' variable1 variable2 = + ReaderT (VariableNameMap' variable1 variable2) + +type Renaming' variable1 variable2 = + Env (VariableNameMap' variable1 variable2) type RenamingT variable1 variable2 = - ReaderT (UnifiedVariableMap variable1 variable2) + RenamingT' (VariableNameOf variable1) (VariableNameOf variable2) type Renaming variable1 variable2 = - Env (UnifiedVariableMap variable1 variable2) + Renaming' (VariableNameOf variable1) (VariableNameOf variable2) renameFreeVariables :: forall m variable1 variable2 - . Ord variable1 + . NamedVariable variable1 => Monad m - => AdjUnifiedVariable (variable1 -> m variable2) + => AdjSomeVariableName (VariableNameOf variable1 -> m variable2) -> FreeVariables variable1 - -> m (UnifiedVariableMap variable1 variable2) + -> m (VariableNameMap' (VariableNameOf variable1) variable2) renameFreeVariables adj = Monad.foldM worker mempty . FreeVariables.toSet where - trElemVar = sequenceA . (<*>) (elemVar adj) - trSetVar = sequenceA . (<*>) (setVar adj) - worker renaming = - \case - ElemVar elemVar -> - renameElementVariable elemVar - <$> trElemVar elemVar - <*> pure renaming - SetVar setVar -> - renameSetVariable setVar - <$> trSetVar setVar - <*> pure renaming + adj' = fmap mkVariableNameMap adj + mkVariableNameMap rename variable1 = do + variable2 <- rename variable1 + pure (Map.singleton variable1 variable2) + worker + :: VariableNameMap' (VariableNameOf variable1) variable2 + -> UnifiedVariable variable1 + -> m (VariableNameMap' (VariableNameOf variable1) variable2) + worker renaming unifiedVariable = do + let someVariableName1 :: SomeVariableName (VariableNameOf variable1) + someVariableName1 = Lens.view lensVariableName unifiedVariable + idx :: SomeVariableName () + (variable1, idx) = splitL someVariableName1 + renaming1 <- index adj' idx variable1 + let renaming' = tabulate $ \idx' -> if idx == idx' then renaming1 else mempty + pure (renaming <> renaming') {-# INLINE renameFreeVariables #-} -askUnifiedVariable - :: Monad m +askSomeVariableName + :: HasCallStack => Ord variable1 - => UnifiedVariable variable1 - -> RenamingT variable1 variable2 m (UnifiedVariable variable2) + => MonadReader (VariableNameMap' variable1 variable2) m + => AdjSomeVariableName (variable1 -> m variable2) +askSomeVariableName = + tabulate $ \idx -> \variable1 -> + Reader.asks $ maybe (error "undefined") id . Map.lookup variable1 . flip index idx +{-# INLINE askSomeVariableName #-} + +askElementVariableName + :: Ord variable1 + => MonadReader (VariableNameMap' variable1 variable2) m + => ElementVariableName variable1 -> m (ElementVariableName variable2) +askElementVariableName = traverseElementVariableName askSomeVariableName + +askSetVariableName + :: Ord variable1 + => MonadReader (VariableNameMap' variable1 variable2) m + => SetVariableName variable1 -> m (SetVariableName variable2) +askSetVariableName = traverseSetVariableName askSomeVariableName + +askUnifiedVariable + :: (NamedVariable variable1, NamedVariable variable2) + => MonadReader (VariableNameMap variable1 variable2) m + => UnifiedVariable variable1 -> m (UnifiedVariable variable2) askUnifiedVariable = - \case - SetVar setVar -> SetVar <$> askSetVariable setVar - ElemVar elemVar -> ElemVar <$> askElementVariable elemVar -{-# INLINE askUnifiedVariable #-} + lensVariableName $ traverseSomeVariableName askSomeVariableName askElementVariable - :: Monad m - => Ord variable1 - => ElementVariable variable1 - -> RenamingT variable1 variable2 m (ElementVariable variable2) -askElementVariable elementVariable = - -- fromJust is safe because the variable must be renamed - Reader.asks $ Maybe.fromJust . lookupRenamedElementVariable elementVariable -{-# INLINE askElementVariable #-} + :: (NamedVariable variable1, NamedVariable variable2) + => MonadReader (VariableNameMap variable1 variable2) m + => ElementVariable variable1 -> m (ElementVariable variable2) +askElementVariable = lensVariableName askElementVariableName askSetVariable - :: Monad m - => Ord variable1 - => SetVariable variable1 - -> RenamingT variable1 variable2 m (SetVariable variable2) -askSetVariable setVariable = - -- fromJust is safe because the variable must be renamed - Reader.asks $ Maybe.fromJust . lookupRenamedSetVariable setVariable -{-# INLINE askSetVariable #-} + :: (NamedVariable variable1, NamedVariable variable2) + => MonadReader (VariableNameMap variable1 variable2) m + => SetVariable variable1 -> m (SetVariable variable2) +askSetVariable = lensVariableName askSetVariableName + +renameElementBinder + :: MonadReader (VariableNameMap variable1 variable2) m + => (NamedVariable variable1, NamedVariable variable2) + => FreshPartialOrd variable2 + => (ElementVariable variable1 -> m (ElementVariable variable2)) + -> FreeVariables variable2 + -> Binder (ElementVariable variable1) (m any) + -> m (Binder (ElementVariable variable2) any) +renameElementBinder trElemVar avoiding binder = do + let Binder { binderVariable, binderChild } = binder + elementVariable2 <- trElemVar binderVariable + let binderVariable' = + refreshElementVariable + (FreeVariables.toSet avoiding) + elementVariable2 + & fromMaybe elementVariable2 + withRenaming = + renameElementVariable + ((,) + <$> Lens.view lensVariableName binderVariable + <*> Lens.view lensVariableName binderVariable' + ) + binderChild' <- Reader.local withRenaming binderChild + let binder' = Binder + { binderVariable = binderVariable' + , binderChild = binderChild' + } + pure binder' +{-# INLINE renameElementBinder #-} + +renameSomeVariable + :: Ord variable1 + => SomeVariableName (variable1, variable2) + -> VariableNameMap' variable1 variable2 + -> VariableNameMap' variable1 variable2 +renameSomeVariable someVariableNames variableNameMap = + let ((variable1, variable2), idx) = splitL someVariableNames + worker idx' + | idx' == idx = Map.insert variable1 variable2 + | otherwise = id + in tabulate worker <*> variableNameMap + +renameElementVariable + :: Ord variable1 + => ElementVariableName (variable1, variable2) + -> VariableNameMap' variable1 variable2 + -> VariableNameMap' variable1 variable2 +renameElementVariable elementVariableNames = + renameSomeVariable (inject elementVariableNames) + +renameSetVariable + :: Ord variable1 + => SetVariableName (variable1, variable2) + -> VariableNameMap' variable1 variable2 + -> VariableNameMap' variable1 variable2 +renameSetVariable setVariableNames = + renameSomeVariable (inject setVariableNames) + +renameSetBinder + :: MonadReader (VariableNameMap variable1 variable2) m + => (NamedVariable variable1, NamedVariable variable2) + => FreshPartialOrd variable2 + => (SetVariable variable1 -> m (SetVariable variable2)) + -> FreeVariables variable2 + -> Binder (SetVariable variable1) (m any) + -> m (Binder (SetVariable variable2) any) +renameSetBinder trSetVar avoiding binder = do + let Binder { binderVariable, binderChild } = binder + setVariable2 <- trSetVar binderVariable + let binderVariable' = + refreshSetVariable + (FreeVariables.toSet avoiding) + setVariable2 + & fromMaybe setVariable2 + withRenaming = + renameSetVariable + ((,) + <$> Lens.view lensVariableName binderVariable + <*> Lens.view lensVariableName binderVariable' + ) + binderChild' <- Reader.local withRenaming binderChild + let binder' = Binder + { binderVariable = binderVariable' + , binderChild = binderChild' + } + pure binder' +{-# INLINE renameSetBinder #-} diff --git a/kore/src/Kore/Internal/TermLike/TermLike.hs b/kore/src/Kore/Internal/TermLike/TermLike.hs index 28cd69ae98..3ae53e4661 100644 --- a/kore/src/Kore/Internal/TermLike/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike/TermLike.hs @@ -59,12 +59,13 @@ import Data.Functor.Identity ( Identity (..) ) import qualified Data.Generics.Product as Lens.Product -import Data.Generics.Wrapped - ( _Wrapped - ) import Data.List ( foldl' ) +import qualified Data.Map.Strict as Map +import Data.Set + ( Set + ) import qualified Data.Set as Set import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC @@ -136,6 +137,10 @@ import Kore.Variables.Fresh ( FreshPartialOrd ) import qualified Kore.Variables.Fresh as Fresh +import Kore.Variables.UnifiedVariable hiding + ( renameElementVariable + , renameSetVariable + ) import qualified Pretty import qualified SQL @@ -294,7 +299,7 @@ instance NFData variable => NFData (TermLike variable) where rnf (Recursive.project -> annotation :< pat) = rnf annotation `seq` rnf pat -instance InternalVariable variable => Unparse (TermLike variable) where +instance NamedVariable variable => Unparse (TermLike variable) where unparse term = case Recursive.project freshVarTerm of (attrs :< termLikeF) @@ -351,7 +356,7 @@ instance InternalVariable variable => Unparse (TermLike variable) where where freshVarTerm = externalizeFreshVariables - $ mapVariables toUnifiedVariable term + $ mapVariables (pure toVariableName) term unparse2 term = case Recursive.project freshVarTerm of @@ -359,7 +364,7 @@ instance InternalVariable variable => Unparse (TermLike variable) where where freshVarTerm = externalizeFreshVariables - $ mapVariables toUnifiedVariable term + $ mapVariables (pure toVariableName) term type instance Base (TermLike variable) = CofreeF (TermLikeF variable) (Attribute.Pattern variable) @@ -507,7 +512,7 @@ instance (FreshPartialOrd variable, NamedVariable variable) => From (TermLike Concrete) (TermLike variable) where - from = mapVariables fromConcreteUnifiedVariable + from = mapVariables (pure $ from @Void) {-# INLINE from #-} -- | The type of internal domain values. @@ -573,13 +578,15 @@ not injective! -} mapVariablesF - :: AdjUnifiedVariable (variable1 -> variable2) - -> TermLikeF variable1 child - -> TermLikeF variable2 child + :: (NamedVariable variable1, NamedVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> TermLikeF variable1 child + -> TermLikeF variable2 child mapVariablesF adj = runIdentity . traverseVariablesF adj' where - adj' = (\f x -> Identity (f x)) <$> adj + adj' = (.) pure <$> adj {- | Use the provided traversal to replace all variables in a 'TermLikeF' head. @@ -588,10 +595,12 @@ traversal is not injective! -} traverseVariablesF - :: Applicative f - => AdjUnifiedVariable (variable1 -> f variable2) - -> TermLikeF variable1 child - -> f (TermLikeF variable2 child) + :: Applicative f + => (NamedVariable variable1, NamedVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> f (VariableNameOf variable2)) + -> TermLikeF variable1 child + -> f (TermLikeF variable2 child) traverseVariablesF adj = \case -- Non-trivial cases @@ -626,8 +635,8 @@ traverseVariablesF adj = SignednessF signedness -> pure (SignednessF signedness) InjF inj -> pure (InjF inj) where - trElemVar = sequenceA . (<*>) (elemVar adj) - trSetVar = sequenceA . (<*>) (setVar adj) + trElemVar = lensVariableName $ traverseElementVariableName adj + trSetVar = lensVariableName $ traverseSetVariableName adj traverseConstVariable (Const variable) = Const <$> traverseUnifiedVariable adj variable traverseVariablesExists Exists { existsSort, existsVariable, existsChild } = @@ -659,23 +668,26 @@ See also: 'traverseVariables' -} mapVariables - :: forall variable1 variable2 - . (Ord variable1, FreshPartialOrd variable2, NamedVariable variable2) - => AdjUnifiedVariable (variable1 -> variable2) - -> TermLike variable1 - -> TermLike variable2 + :: forall variable1 variable2 + . (NamedVariable variable1, NamedVariable variable2) + => FreshPartialOrd variable2 + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> TermLike variable1 + -> TermLike variable2 mapVariables adj termLike = Recursive.unfold worker (Env.env freeVariables0 termLike) where - adj' = (\f x -> Identity (f x)) <$> adj - trElemVar - :: ElementVariable variable1 - -> Identity (ElementVariable variable2) - trElemVar = sequenceA . (<*>) (elemVar adj') - trSetVar = sequenceA . (<*>) (setVar adj') + adjIdentity = (.) pure <$> adj + adjReader = (.) pure <$> adj + trElemVar = lensVariableName $ traverseElementVariableName adjReader + trSetVar = lensVariableName $ traverseSetVariableName adjReader + + freeVariables0 :: VariableNameMap variable1 variable2 Identity freeVariables0 = - renameFreeVariables adj' (freeVariables termLike) + freeVariables @(TermLike variable1) @variable1 termLike + & renameFreeVariables adjIdentity mapExists avoiding = sequenceAdjunct $ existsBinder $ renameElementBinder trElemVar avoiding @@ -686,20 +698,12 @@ mapVariables adj termLike = mapNu avoiding = sequenceAdjunct $ nuBinder $ renameSetBinder trSetVar avoiding + askSomeVariableName' = rightAdjunct <$> askSomeVariableName askUnifiedVariable' = rightAdjunct askUnifiedVariable - askElementVariable' = rightAdjunct askElementVariable - askSetVariable' = rightAdjunct askSetVariable renameAttrs renaming = Attribute.mapVariables - AdjUnifiedVariable - { elemVar = - (ElementVariable . Lens.over _Wrapped) - (askElementVariable' . Env.env renaming) - , setVar = - (SetVariable . Lens.over _Wrapped) - (askSetVariable' . Env.env renaming) - } + (fmap (. Env.env renaming) askSomeVariableName') worker :: Renaming variable1 variable2 (TermLike variable1) @@ -710,7 +714,7 @@ mapVariables adj termLike = let attrs :< termLikeF = Recursive.project (extract env) renaming = Env.ask env attrs' = renameAttrs renaming attrs - avoiding = FreeVariables.toSet $ freeVariables attrs' + avoiding = freeVariables attrs' termLikeF' = case termLikeF of VariableF (Const unifiedVariable1) -> @@ -741,17 +745,20 @@ See also: 'mapVariables' -} traverseVariables :: forall variable1 variable2 m - . (Ord variable1, FreshPartialOrd variable2, NamedVariable variable2) + . (NamedVariable variable1, NamedVariable variable2) + => FreshPartialOrd variable2 => Monad m - => AdjUnifiedVariable (variable1 -> m variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> m (VariableNameOf variable2)) -> TermLike variable1 -> m (TermLike variable2) traverseVariables adj termLike = - renameFreeVariables adj (freeVariables termLike) + renameFreeVariables adj (freeVariables @_ @variable1 termLike) >>= Reader.runReaderT (Recursive.fold worker termLike) where - trElemVar = sequenceA . (<*>) (elemVar adj) - trSetVar = sequenceA . (<*>) (setVar adj) + adjReader = (.) lift <$> adj + trElemVar = lensVariableName $ traverseElementVariableName adjReader + trSetVar = lensVariableName $ traverseSetVariableName adjReader traverseExists avoiding = existsBinder (renameElementBinder trElemVar avoiding) traverseForall avoiding = @@ -761,20 +768,14 @@ traverseVariables adj termLike = traverseNu avoiding = nuBinder (renameSetBinder trSetVar avoiding) - askVariable = - AdjUnifiedVariable - { elemVar = ElementVariable (_Wrapped askElementVariable) - , setVar = SetVariable (_Wrapped askSetVariable) - } - worker :: Base (TermLike variable1) (RenamingT variable1 variable2 m (TermLike variable2)) -> RenamingT variable1 variable2 m (TermLike variable2) worker (attrs :< termLikeF) = do - attrs' <- Attribute.traverseVariables askVariable attrs - let avoiding = FreeVariables.toSet $ freeVariables attrs' + attrs' <- Attribute.traverseVariables askSomeVariableName attrs + let avoiding = freeVariables attrs' termLikeF' <- case termLikeF of VariableF (Const unifiedVariable) -> do unifiedVariable' <- askUnifiedVariable unifiedVariable @@ -787,7 +788,7 @@ traverseVariables adj termLike = sequence termLikeF >>= -- traverseVariablesF will not actually call the traversals -- because all the cases with variables are handled above. - traverseVariablesF askVariable + traverseVariablesF askSomeVariableName (pure . Recursive.embed) (attrs' :< termLikeF') {- | Transform a 'sequence'-like function into its dual with an 'Adjunction'. @@ -835,58 +836,6 @@ sequenceAdjunct gsequence = contract = counit {-# INLINE sequenceAdjunct #-} -renameElementBinder - :: Monad m - => (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2) - => (ElementVariable variable1 -> m (ElementVariable variable2)) - -> Set.Set (UnifiedVariable variable2) - -> Binder (ElementVariable variable1) - (RenamingT variable1 variable2 m any) - -> RenamingT variable1 variable2 m - (Binder (ElementVariable variable2) any) -renameElementBinder trElemVar avoiding binder = do - let Binder { binderVariable, binderChild } = binder - elementVariable2 <- lift $ trElemVar binderVariable - let binderVariable' = - refreshElementVariable avoiding elementVariable2 - & fromMaybe elementVariable2 - binderChild' <- - Reader.local - (renameElementVariable binderVariable binderVariable') - binderChild - let binder' = Binder - { binderVariable = binderVariable' - , binderChild = binderChild' - } - pure binder' -{-# INLINE renameElementBinder #-} - -renameSetBinder - :: Monad m - => (Ord variable1, FreshPartialOrd variable2, SortedVariable variable2) - => (SetVariable variable1 -> m (SetVariable variable2)) - -> Set.Set (UnifiedVariable variable2) - -> Binder (SetVariable variable1) - (RenamingT variable1 variable2 m any) - -> RenamingT variable1 variable2 m - (Binder (SetVariable variable2) any) -renameSetBinder trSetVar avoiding binder = do - let Binder { binderVariable, binderChild } = binder - setVariable2 <- lift $ trSetVar binderVariable - let binderVariable' = - refreshSetVariable avoiding setVariable2 - & fromMaybe setVariable2 - binderChild' <- - Reader.local - (renameSetVariable binderVariable binderVariable') - binderChild - let binder' = Binder - { binderVariable = binderVariable' - , binderChild = binderChild' - } - pure binder' -{-# INLINE renameSetBinder #-} - {- | Reset the 'variableCounter' of all 'Variables'. @externalizeFreshVariables@ resets the 'variableCounter' of all variables, while @@ -903,18 +852,26 @@ externalizeFreshVariables termLike = -- not have a generated counter. 'generatedFreeVariables' have a generated -- counter, usually because they were introduced by applying some axiom. originalFreeVariables, generatedFreeVariables - :: Set.Set (UnifiedVariable Variable) + :: Set (UnifiedVariable Variable) (originalFreeVariables, generatedFreeVariables) = Set.partition (foldMapVariable Variable.isOriginalVariable) $ FreeVariables.toSet $ freeVariables termLike -- | The map of generated free variables, renamed to be unique from the -- original free variables. - renamedFreeVariables :: UnifiedVariableMap Variable Variable + renamedFreeVariables :: VariableNameMap Variable Variable (renamedFreeVariables, _) = Foldable.foldl' rename initial generatedFreeVariables where initial = (mempty, foldMap freeVariable originalFreeVariables) + rename + :: ( VariableNameMap Variable Variable + , FreeVariables Variable + ) + -> UnifiedVariable Variable + -> ( VariableNameMap Variable Variable + , FreeVariables Variable + ) rename (renaming, avoiding) variable = let (variable', renaming') = @@ -922,21 +879,31 @@ externalizeFreshVariables termLike = ElemVar elementVariable -> ( ElemVar elementVariable' , renameElementVariable - elementVariable - elementVariable' + (pure (name, name')) renaming ) where + name = + Lens.view lensVariableName elementVariable + & unElementVariableName + name' = + Lens.view lensVariableName elementVariable' + & unElementVariableName elementVariable' = safeElementVariable avoiding elementVariable SetVar setVariable -> ( SetVar setVariable' , renameSetVariable - setVariable - setVariable' + (pure (name, name')) renaming ) where + name = + Lens.view lensVariableName setVariable + & unSetVariableName + name' = + Lens.view lensVariableName setVariable' + & unSetVariableName setVariable' = safeSetVariable avoiding setVariable avoiding' = freeVariable variable' <> avoiding @@ -944,25 +911,29 @@ externalizeFreshVariables termLike = (renaming', avoiding') lookupElementVariable - :: ElementVariable Variable - -> Reader (UnifiedVariableMap Variable Variable) (ElementVariable Variable) - lookupElementVariable elementVariable = + :: VariableName + -> Reader (VariableNameMap Variable Variable) VariableName + lookupElementVariable elementVariableName = Reader.asks - $ fromMaybe elementVariable - . lookupRenamedElementVariable elementVariable + $ fromMaybe elementVariableName + . Map.lookup elementVariableName + . unElementVariableName + . adjSomeVariableNameElement lookupSetVariable - :: SetVariable Variable - -> Reader (UnifiedVariableMap Variable Variable) (SetVariable Variable) - lookupSetVariable setVariable = + :: VariableName + -> Reader (VariableNameMap Variable Variable) VariableName + lookupSetVariable setVariableName = Reader.asks - $ fromMaybe setVariable - . lookupRenamedSetVariable setVariable + $ fromMaybe setVariableName + . Map.lookup setVariableName + . unSetVariableName + . adjSomeVariableNameSet lookupVariable = - AdjUnifiedVariable - { elemVar = ElementVariable (_Wrapped lookupElementVariable) - , setVar = SetVariable (_Wrapped lookupSetVariable) + AdjSomeVariableName + { adjSomeVariableNameElement = ElementVariableName lookupElementVariable + , adjSomeVariableNameSet = SetVariableName lookupSetVariable } {- | Externalize a variable safely. @@ -1000,24 +971,25 @@ externalizeFreshVariables termLike = underElementBinder freeVariables' variable child = do let variable' = safeElementVariable freeVariables' variable - child' <- Reader.local (renameElementVariable variable variable') child + name = Lens.view lensVariableName variable & unElementVariableName + name' = Lens.view lensVariableName variable' & unElementVariableName + names = ElementVariableName (name, name') + child' <- Reader.local (renameElementVariable names) child return (variable', child') underSetBinder freeVariables' variable child = do let variable' = safeSetVariable freeVariables' variable - child' <- Reader.local (renameSetVariable variable variable') child + name = Lens.view lensVariableName variable & unSetVariableName + name' = Lens.view lensVariableName variable' & unSetVariableName + names = SetVariableName (name, name') + child' <- Reader.local (renameSetVariable names) child return (variable', child') externalizeFreshVariablesWorker :: Base (TermLike Variable) - (Reader - (UnifiedVariableMap Variable Variable) - (TermLike Variable) - ) - -> Reader - (UnifiedVariableMap Variable Variable) - (TermLike Variable) + (RenamingT Variable Variable Identity (TermLike Variable)) + -> RenamingT Variable Variable Identity (TermLike Variable) externalizeFreshVariablesWorker (attrs :< patt) = do attrs' <- Attribute.traverseVariables lookupVariable attrs let freeVariables' = Attribute.freeVariables attrs' @@ -1101,7 +1073,7 @@ updateCallStack = Lens.set created callstack -} mkVar :: HasCallStack - => InternalVariable variable + => NamedVariable variable => UnifiedVariable variable -> TermLike variable mkVar = updateCallStack . synthesize . VariableF . Const diff --git a/kore/src/Kore/Internal/Variable.hs b/kore/src/Kore/Internal/Variable.hs index 0d441fe37e..3bf4871f53 100644 --- a/kore/src/Kore/Internal/Variable.hs +++ b/kore/src/Kore/Internal/Variable.hs @@ -85,6 +85,6 @@ type InternalVariable variable = ( Hashable variable, Ord variable, SubstitutionOrd variable , Debug variable, Show variable, Unparse variable , NamedVariable variable, SortedVariable variable - , VariableBase variable + , VariableBase variable, From VariableName (VariableNameOf variable) , FreshPartialOrd variable, FreshVariable variable ) diff --git a/kore/src/Kore/Log/DebugAppliedRewriteRules.hs b/kore/src/Kore/Log/DebugAppliedRewriteRules.hs index 2819997978..f823a48dca 100644 --- a/kore/src/Kore/Log/DebugAppliedRewriteRules.hs +++ b/kore/src/Kore/Log/DebugAppliedRewriteRules.hs @@ -27,6 +27,7 @@ import Kore.Internal.Pattern import qualified Kore.Internal.TermLike as TermLike import Kore.Internal.Variable ( Variable (..) + , toVariableName ) import Kore.Rewriting.RewritingVariable import Kore.Step.RulePattern @@ -40,7 +41,6 @@ import Kore.Step.Step import Kore.Unparser ( unparse ) -import Kore.Variables.UnifiedVariable import Log import Pretty ( Pretty (..) @@ -93,4 +93,4 @@ debugAppliedRewriteRules initial rules = appliedRewriteRules = coerce (mapConditionalVariables mapRuleVariables <$> rules) mapConditionalVariables mapTermVariables = - Conditional.mapVariables mapTermVariables toUnifiedVariable + Conditional.mapVariables mapTermVariables (pure toVariableName) diff --git a/kore/src/Kore/Log/ErrorRewritesInstantiation.hs b/kore/src/Kore/Log/ErrorRewritesInstantiation.hs index b7ac4051d1..a8fd5fad13 100644 --- a/kore/src/Kore/Log/ErrorRewritesInstantiation.hs +++ b/kore/src/Kore/Log/ErrorRewritesInstantiation.hs @@ -45,6 +45,7 @@ import qualified Kore.Internal.Pattern as Pattern import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.Variable ( InternalVariable + , toVariableName ) import Kore.Rewriting.RewritingVariable import Kore.Step.RulePattern @@ -151,7 +152,7 @@ errorRewritesInstantiation configuration' unificationError = , errorCallStack = callStack } where - mapVariables = Pattern.mapVariables toUnifiedVariable + mapVariables = Pattern.mapVariables (pure toVariableName) configuration = mkRewritingPattern $ mapVariables configuration' {- | Check that the final substitution covers the applied rule appropriately. diff --git a/kore/src/Kore/Log/InfoAttemptUnification.hs b/kore/src/Kore/Log/InfoAttemptUnification.hs index 4746ac0171..abdec0bcb7 100644 --- a/kore/src/Kore/Log/InfoAttemptUnification.hs +++ b/kore/src/Kore/Log/InfoAttemptUnification.hs @@ -18,12 +18,12 @@ import Kore.Internal.TermLike ( InternalVariable , TermLike , Variable + , toVariableName ) import qualified Kore.Internal.TermLike as TermLike import Kore.Unparser ( unparse ) -import Kore.Variables.UnifiedVariable import Log import Pretty ( Pretty @@ -63,6 +63,6 @@ infoAttemptUnification infoAttemptUnification term1' term2' = logWhile InfoAttemptUnification { term1, term2 } where - mapVariables = TermLike.mapVariables toUnifiedVariable + mapVariables = TermLike.mapVariables (pure toVariableName) term1 = mapVariables term1' term2 = mapVariables term2' diff --git a/kore/src/Kore/Log/WarnBottomTotalFunction.hs b/kore/src/Kore/Log/WarnBottomTotalFunction.hs index f74485b3c3..887ac284d1 100644 --- a/kore/src/Kore/Log/WarnBottomTotalFunction.hs +++ b/kore/src/Kore/Log/WarnBottomTotalFunction.hs @@ -12,7 +12,7 @@ module Kore.Log.WarnBottomTotalFunction import Prelude.Kore import qualified Generics.SOP as SOP -import GHC.Generics as GHC +import qualified GHC.Generics as GHC import Kore.Internal.TermLike import Kore.Step.Simplification.Simplify @@ -21,7 +21,6 @@ import Kore.Step.Simplification.Simplify import Kore.Unparser ( unparse ) -import Kore.Variables.UnifiedVariable import Pretty ( Pretty ) @@ -60,5 +59,5 @@ warnBottomTotalFunction => InternalVariable variable => TermLike variable -> logger () -warnBottomTotalFunction (mapVariables toUnifiedVariable -> term) = +warnBottomTotalFunction (mapVariables (pure toVariableName) -> term) = logEntry WarnBottomTotalFunction { term } diff --git a/kore/src/Kore/Log/WarnDecidePredicateUnknown.hs b/kore/src/Kore/Log/WarnDecidePredicateUnknown.hs index f6a84b80c1..28a32c5613 100644 --- a/kore/src/Kore/Log/WarnDecidePredicateUnknown.hs +++ b/kore/src/Kore/Log/WarnDecidePredicateUnknown.hs @@ -21,7 +21,6 @@ import Kore.Internal.Predicate import qualified Kore.Internal.Predicate as Predicate import Kore.Internal.Variable import Kore.Unparser -import Kore.Variables.UnifiedVariable import Log import Pretty ( Pretty (..) @@ -57,4 +56,4 @@ warnDecidePredicateUnknown warnDecidePredicateUnknown predicates' = logEntry WarnDecidePredicateUnknown { predicates } where - predicates = Predicate.mapVariables toUnifiedVariable <$> predicates' + predicates = Predicate.mapVariables (pure toVariableName) <$> predicates' diff --git a/kore/src/Kore/Rewriting/RewritingVariable.hs b/kore/src/Kore/Rewriting/RewritingVariable.hs index 9d0d21c9e8..03e352d8a6 100644 --- a/kore/src/Kore/Rewriting/RewritingVariable.hs +++ b/kore/src/Kore/Rewriting/RewritingVariable.hs @@ -54,6 +54,10 @@ import Kore.Unparser import Kore.Variables.Fresh import Kore.Variables.UnifiedVariable +-- TODO (thomas.tuegel): Replace +-- > data RewritingVariable +-- with +-- > type RewritingVariable = Variable1 RewritingVariableName data RewritingVariable = ConfigVariable !Variable | RuleVariable !Variable @@ -81,6 +85,8 @@ instance FreshPartialOrd RewritingVariable where ConfigVariable var -> ConfigVariable (nextVariable var) {-# INLINE nextVariable #-} +{- | The name of a 'RewritingVariable'. + -} data RewritingVariableName = ConfigVariableName !VariableName | RuleVariableName !VariableName @@ -141,9 +147,16 @@ instance From RewritingVariable Variable where from (ConfigVariable variable) = variable from (RuleVariable variable) = variable +instance From RewritingVariableName VariableName where + from (ConfigVariableName variable) = variable + from (RuleVariableName variable) = variable + instance From Variable RewritingVariable where from = RuleVariable +instance From VariableName RewritingVariableName where + from = RuleVariableName + instance SortedVariable RewritingVariable where lensVariableSort f = \case @@ -197,8 +210,9 @@ getPattern pattern' = where freeVars = freeVariables pattern' & FreeVariables.toList -getRewritingVariable :: AdjUnifiedVariable (RewritingVariable -> Variable) -getRewritingVariable = pure (from @RewritingVariable @Variable) +getRewritingVariable + :: AdjSomeVariableName (RewritingVariableName -> VariableName) +getRewritingVariable = pure (from @RewritingVariableName @VariableName) getPatternAux :: Pattern RewritingVariable -> Pattern Variable getPatternAux = Pattern.mapVariables getRewritingVariable @@ -265,7 +279,7 @@ mkRewritingRule :: UnifyingRule rule => rule Variable -> rule RewritingVariable -mkRewritingRule = mapRuleVariables (pure RuleVariable) +mkRewritingRule = mapRuleVariables (pure RuleVariableName) {- | Unwrap the variables in a 'RulePattern'. Inverse of 'targetRuleVariables'. -} @@ -274,7 +288,7 @@ unRewritingRule = mapRuleVariables getRewritingVariable -- |Renames configuration variables to distinguish them from those in the rule. mkRewritingPattern :: Pattern Variable -> Pattern RewritingVariable -mkRewritingPattern = Pattern.mapVariables (pure ConfigVariable) +mkRewritingPattern = Pattern.mapVariables (pure ConfigVariableName) getRemainderPredicate :: Predicate RewritingVariable -> Predicate Variable getRemainderPredicate predicate = diff --git a/kore/src/Kore/Rewriting/UnifyingRule.hs b/kore/src/Kore/Rewriting/UnifyingRule.hs index 9cd17ba044..5e52d39a0a 100644 --- a/kore/src/Kore/Rewriting/UnifyingRule.hs +++ b/kore/src/Kore/Rewriting/UnifyingRule.hs @@ -28,6 +28,7 @@ import Kore.Internal.TermLike , NamedVariable , TermLike ) +import Kore.Syntax.Variable import Kore.Unparser import Kore.Variables.Fresh ( FreshPartialOrd @@ -96,10 +97,12 @@ class UnifyingRule rule where distinguishing rule variables from configuration variables. -} mapRuleVariables - :: (Ord variable1, FreshPartialOrd variable2, NamedVariable variable2) - => AdjUnifiedVariable (variable1 -> variable2) - -> rule variable1 - -> rule variable2 + :: (NamedVariable variable1, NamedVariable variable2) + => FreshPartialOrd variable2 + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> rule variable1 + -> rule variable2 -- | Checks whether a given substitution is acceptable for a rule checkInstantiation diff --git a/kore/src/Kore/Step/Axiom/EvaluationStrategy.hs b/kore/src/Kore/Step/Axiom/EvaluationStrategy.hs index 585c1c99be..9b02cfc3b3 100644 --- a/kore/src/Kore/Step/Axiom/EvaluationStrategy.hs +++ b/kore/src/Kore/Step/Axiom/EvaluationStrategy.hs @@ -54,7 +54,6 @@ import Kore.Unparser ( unparse ) import qualified Kore.Variables.Target as Target -import Kore.Variables.UnifiedVariable import qualified Pretty {-|Describes whether simplifiers are allowed to return multiple results or not. @@ -76,7 +75,9 @@ definitionEvaluation -> BuiltinAndAxiomSimplifier definitionEvaluation equations = BuiltinAndAxiomSimplifier $ \term condition -> do - let equations' = Equation.mapVariables fromUnifiedVariable <$> equations + let equations' = + Equation.mapVariables (pure fromVariableName) + <$> equations term' = TermLike.mapVariables Target.mkUnifiedNonTarget term condition' = SideCondition.mapVariables @@ -114,7 +115,7 @@ simplificationEvaluation -> BuiltinAndAxiomSimplifier simplificationEvaluation equation = BuiltinAndAxiomSimplifier $ \term condition -> do - let equation' = Equation.mapVariables fromUnifiedVariable equation + let equation' = Equation.mapVariables (pure fromVariableName) equation term' = TermLike.mapVariables Target.mkUnifiedNonTarget term condition' = SideCondition.mapVariables diff --git a/kore/src/Kore/Step/RulePattern.hs b/kore/src/Kore/Step/RulePattern.hs index ac98e7ff0c..4ab18d21fa 100644 --- a/kore/src/Kore/Step/RulePattern.hs +++ b/kore/src/Kore/Step/RulePattern.hs @@ -896,7 +896,10 @@ instance UnifyingRule RulePattern where , antiLeft = mapTermLikeVariables <$> antiLeft , requires = mapPredicateVariables requires , rhs = RHS - { existentials = (<*>) (elemVar adj) <$> existentials + { existentials = + Lens.over lensVariableName + (mapElementVariableName adj) + <$> existentials , right = mapTermLikeVariables right , ensures = mapPredicateVariables ensures } diff --git a/kore/src/Kore/Step/Simplification/Builtin.hs b/kore/src/Kore/Step/Simplification/Builtin.hs index a05813dd75..362ca926ec 100644 --- a/kore/src/Kore/Step/Simplification/Builtin.hs +++ b/kore/src/Kore/Step/Simplification/Builtin.hs @@ -103,7 +103,7 @@ normalizedMapResultToTerm BottomResult = mkBottom_ normalizeInternalMap - :: Ord variable + :: NamedVariable variable => InternalMap (TermLike Concrete) (TermLike variable) -> NormalizedMapResult variable normalizeInternalMap map' = @@ -128,7 +128,7 @@ simplifyInternalSet = . simplifyInternal normalizeInternalSet normalizeInternalSet - :: Ord variable + :: NamedVariable variable => InternalSet (TermLike Concrete) (TermLike variable) -> Maybe (InternalSet (TermLike Concrete) (TermLike variable)) normalizeInternalSet = diff --git a/kore/src/Kore/Step/Simplification/ExpandAlias.hs b/kore/src/Kore/Step/Simplification/ExpandAlias.hs index 304cf28b5d..17869342a9 100644 --- a/kore/src/Kore/Step/Simplification/ExpandAlias.hs +++ b/kore/src/Kore/Step/Simplification/ExpandAlias.hs @@ -29,6 +29,7 @@ import Kore.Internal.TermLike , InternalVariable , TermLike , Variable + , fromVariableName , mapVariables , substitute ) @@ -36,8 +37,7 @@ import Kore.Unification.Unify ( MonadUnify ) import Kore.Variables.UnifiedVariable - ( fromUnifiedVariable - , mapUnifiedVariable + ( mapUnifiedVariable ) expandAlias @@ -76,7 +76,7 @@ substituteInAlias substituteInAlias Alias { aliasLeft, aliasRight } children = assert (length aliasLeft == length children) $ substitute substitutionMap - $ mapVariables fromUnifiedVariable aliasRight + $ mapVariables (pure fromVariableName) aliasRight where - aliasLeft' = mapUnifiedVariable fromUnifiedVariable <$> aliasLeft + aliasLeft' = mapUnifiedVariable (pure fromVariableName) <$> aliasLeft substitutionMap = Map.fromList $ zip aliasLeft' children diff --git a/kore/src/Kore/Step/Simplification/TermLike.hs b/kore/src/Kore/Step/Simplification/TermLike.hs index e747f5f7d3..61c3dfc172 100644 --- a/kore/src/Kore/Step/Simplification/TermLike.hs +++ b/kore/src/Kore/Step/Simplification/TermLike.hs @@ -14,9 +14,6 @@ import Prelude.Kore import qualified Control.Lens.Combinators as Lens import Data.Functor.Const import qualified Data.Functor.Foldable as Recursive -import Data.Generics.Wrapped - ( _Wrapped - ) import qualified Branch as BranchT ( gather @@ -139,6 +136,11 @@ import qualified Kore.Step.Simplification.Top as Top import qualified Kore.Step.Simplification.Variable as Variable ( simplify ) +import Kore.Syntax.Variable + ( AdjSomeVariableName (..) + , ElementVariableName (..) + , SetVariableName (..) + ) import Kore.TopBottom ( TopBottom (..) ) @@ -152,7 +154,6 @@ import Kore.Variables.Target , targetIfEqual , unTargetUnified ) -import Kore.Variables.UnifiedVariable import qualified Pretty -- TODO(virgil): Add a Simplifiable class and make all pattern types @@ -416,11 +417,11 @@ simplifyInternal term sideCondition = do -> SideCondition (Target variable) targetSideCondition = SideCondition.mapVariables - AdjUnifiedVariable - { elemVar = - (ElementVariable . Lens.over _Wrapped) + AdjSomeVariableName + { adjSomeVariableNameElement = + ElementVariableName (targetIfEqual (ElementVariable boundVar)) - , setVar = SetVariable NonTarget + , adjSomeVariableNameSet = SetVariableName NonTarget } targetSimplifiedChildren :: TermLike.Exists diff --git a/kore/src/Kore/Syntax/ElementVariable.hs b/kore/src/Kore/Syntax/ElementVariable.hs index a2bd64d8a3..fad92be56b 100644 --- a/kore/src/Kore/Syntax/ElementVariable.hs +++ b/kore/src/Kore/Syntax/ElementVariable.hs @@ -32,13 +32,6 @@ newtype ElementVariable variable deriving (Foldable, Traversable) deriving (GHC.Generic) -instance Applicative ElementVariable where - pure = ElementVariable - {-# INLINE pure #-} - - (<*>) (ElementVariable f) (ElementVariable a) = ElementVariable (f a) - {-# INLINE (<*>) #-} - instance Hashable variable => Hashable (ElementVariable variable) instance NFData variable => NFData (ElementVariable variable) diff --git a/kore/src/Kore/Syntax/Pattern.hs b/kore/src/Kore/Syntax/Pattern.hs index a8fa9a837c..ea85c4452f 100644 --- a/kore/src/Kore/Syntax/Pattern.hs +++ b/kore/src/Kore/Syntax/Pattern.hs @@ -61,7 +61,6 @@ import Kore.TopBottom ( TopBottom (..) ) import Kore.Unparser -import Kore.Variables.UnifiedVariable import qualified Pretty import qualified SQL @@ -286,15 +285,17 @@ See also: 'mapVariables' -} traverseVariables - :: forall m variable1 variable2 annotation - . Monad m - => AdjUnifiedVariable (variable1 -> m variable2) - -> Pattern variable1 annotation - -> m (Pattern variable2 annotation) -traverseVariables morphism = + :: forall m variable1 variable2 annotation + . Monad m + => (NamedVariable variable1, NamedVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> m (VariableNameOf variable2)) + -> Pattern variable1 annotation + -> m (Pattern variable2 annotation) +traverseVariables adj = Recursive.fold traverseVariablesWorker where - traverseF = PatternF.traverseVariables morphism + traverseF = PatternF.traverseVariables adj traverseVariablesWorker :: Base @@ -316,13 +317,15 @@ See also: 'traverseVariables' -} mapVariables - :: AdjUnifiedVariable (variable1 -> variable2) - -> Pattern variable1 annotation - -> Pattern variable2 annotation -mapVariables morphism = + :: (NamedVariable variable1, NamedVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> Pattern variable1 annotation + -> Pattern variable2 annotation +mapVariables adj = Recursive.ana (mapVariablesWorker . Recursive.project) where - mapF = PatternF.mapVariables morphism + mapF = PatternF.mapVariables adj mapVariablesWorker (a :< pat) = a :< mapF pat {- | Construct a 'ConcretePattern' from a 'Pattern'. @@ -337,11 +340,12 @@ deciding if the result is @Nothing@ or @Just _@. -} asConcretePattern - :: Pattern variable annotation + :: NamedVariable variable + => Pattern variable annotation -> Maybe (Pattern Concrete annotation) -asConcretePattern = traverseVariables asConcreteUnifiedVariable +asConcretePattern = traverseVariables (pure toVoid) -isConcrete :: Pattern variable annotation -> Bool +isConcrete :: NamedVariable variable => Pattern variable annotation -> Bool isConcrete = isJust . asConcretePattern {- | Construct a 'Pattern' from a 'ConcretePattern'. @@ -354,6 +358,7 @@ composes with other tree transformations without allocating intermediates. -} fromConcretePattern - :: Pattern Concrete annotation + :: NamedVariable variable + => Pattern Concrete annotation -> Pattern variable annotation -fromConcretePattern = mapVariables fromConcreteUnifiedVariable +fromConcretePattern = mapVariables (pure $ from @Void) diff --git a/kore/src/Kore/Syntax/PatternF.hs b/kore/src/Kore/Syntax/PatternF.hs index 574d4c28e1..2fd3290494 100644 --- a/kore/src/Kore/Syntax/PatternF.hs +++ b/kore/src/Kore/Syntax/PatternF.hs @@ -20,10 +20,14 @@ import Prelude.Kore import Control.DeepSeq ( NFData (..) ) +import qualified Control.Lens as Lens import Data.Functor.Const import Data.Functor.Identity ( Identity (..) ) +import Data.Generics.Wrapped + ( _Unwrapped + ) import Data.Text ( Text ) @@ -115,13 +119,15 @@ not injective! -} mapVariables - :: AdjUnifiedVariable (variable1 -> variable2) - -> PatternF variable1 child - -> PatternF variable2 child + :: (NamedVariable variable1, NamedVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> PatternF variable1 child + -> PatternF variable2 child mapVariables adj = runIdentity . traverseVariables adj' where - adj' = (Identity .) <$> adj + adj' = (.) pure <$> adj {-# INLINE mapVariables #-} {- | Use the provided traversal to replace all variables in a 'PatternF' head. @@ -131,9 +137,11 @@ traversal is not injective! -} traverseVariables - :: Applicative f - => AdjUnifiedVariable (variable1 -> f variable2) - -> PatternF variable1 child -> f (PatternF variable2 child) + :: Applicative f + => (NamedVariable variable1, NamedVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> f (VariableNameOf variable2)) + -> PatternF variable1 child -> f (PatternF variable2 child) traverseVariables adj = \case -- Non-trivial cases @@ -161,10 +169,11 @@ traverseVariables adj = TopF topP -> pure (TopF topP) InhabitantF s -> pure (InhabitantF s) where - trElemVar = sequenceA . (<*>) (elemVar adj) - trSetVar = sequenceA . (<*>) (setVar adj) - traverseVariable (Const variable) = - VariableF . Const <$> traverseUnifiedVariable adj variable + trElemVar = lensVariableName $ traverseElementVariableName adj + trSetVar = lensVariableName $ traverseSetVariableName adj + traverseVariable = + fmap VariableF + . Lens.traverseOf _Unwrapped (traverseUnifiedVariable adj) traverseVariablesExists Exists { existsSort, existsVariable, existsChild } = Exists existsSort <$> trElemVar existsVariable diff --git a/kore/src/Kore/Syntax/SetVariable.hs b/kore/src/Kore/Syntax/SetVariable.hs index ddd291a411..037ee1c375 100644 --- a/kore/src/Kore/Syntax/SetVariable.hs +++ b/kore/src/Kore/Syntax/SetVariable.hs @@ -32,13 +32,6 @@ newtype SetVariable variable deriving (Foldable, Traversable) deriving (GHC.Generic) -instance Applicative SetVariable where - pure = SetVariable - {-# INLINE pure #-} - - (<*>) (SetVariable f) (SetVariable a) = SetVariable (f a) - {-# INLINE (<*>) #-} - instance Hashable variable => Hashable (SetVariable variable) instance NFData variable => NFData (SetVariable variable) diff --git a/kore/src/Kore/Syntax/Variable.hs b/kore/src/Kore/Syntax/Variable.hs index 50643f958e..411097dd96 100644 --- a/kore/src/Kore/Syntax/Variable.hs +++ b/kore/src/Kore/Syntax/Variable.hs @@ -19,6 +19,13 @@ module Kore.Syntax.Variable , ElementVariableName (..) , SetVariableName (..) , SomeVariableName (..) + , AdjSomeVariableName (..) + , mapSomeVariableName + , mapElementVariableName + , mapSetVariableName + , traverseSomeVariableName + , traverseElementVariableName + , traverseSetVariableName , NamedVariable (..) , lensVariableName , fromVariable1 @@ -26,12 +33,16 @@ module Kore.Syntax.Variable , VariableBase , toVariable , fromVariable + , toVariableName + , fromVariableName -- * Variable sorts , SortedVariable (..) , sortedVariableSort , unparse2SortedVariable -- * Concrete , Concrete + , Void + , toVoid ) where import Prelude.Kore @@ -45,6 +56,18 @@ import Control.Lens , Lens' ) import qualified Control.Lens as Lens +import Data.Distributive + ( Distributive (..) + ) +import Data.Functor.Adjunction + ( Adjunction (..) + , extractL + , indexAdjunction + , tabulateAdjunction + ) +import Data.Functor.Rep + ( Representable (..) + ) import Data.Generics.Product ( field ) @@ -63,96 +86,6 @@ import Kore.Sort import Kore.Unparser import qualified Pretty -data VariableName = - VariableName - { base :: !Id - , counter :: !(Maybe (Sup Natural)) - } - deriving (Eq, Ord, Show) - deriving (GHC.Generic) - -instance Hashable VariableName - -instance NFData VariableName - -instance SOP.Generic VariableName - -instance SOP.HasDatatypeInfo VariableName - -instance Debug VariableName - -instance Diff VariableName - -newtype ElementVariableName variable = - ElementVariableName { unElementVariableName :: variable } - deriving (Eq, Ord, Show) - deriving (Functor) - deriving (Foldable, Traversable) - deriving (GHC.Generic) - -instance Hashable variable => Hashable (ElementVariableName variable) - -instance NFData variable => NFData (ElementVariableName variable) - -instance SOP.Generic (ElementVariableName variable) - -instance SOP.HasDatatypeInfo (ElementVariableName variable) - -instance Debug variable => Debug (ElementVariableName variable) - -instance (Debug variable, Diff variable) => Diff (ElementVariableName variable) - -newtype SetVariableName variable = - SetVariableName { unSetVariableName :: variable } - deriving (Eq, Ord, Show) - deriving (Functor) - deriving (Foldable, Traversable) - deriving (GHC.Generic) - -instance Hashable variable => Hashable (SetVariableName variable) - -instance NFData variable => NFData (SetVariableName variable) - -instance SOP.Generic (SetVariableName variable) - -instance SOP.HasDatatypeInfo (SetVariableName variable) - -instance Debug variable => Debug (SetVariableName variable) - -instance (Debug variable, Diff variable) => Diff (SetVariableName variable) - -data SomeVariableName variable - = SomeVariableNameElement !(ElementVariableName variable) - | SomeVariableNameSet !(SetVariableName variable) - deriving (Eq, Ord, Show) - deriving (Functor) - deriving (Foldable, Traversable) - deriving (GHC.Generic) - -instance Hashable variable => Hashable (SomeVariableName variable) - -instance NFData variable => NFData (SomeVariableName variable) - -instance SOP.Generic (SomeVariableName variable) - -instance SOP.HasDatatypeInfo (SomeVariableName variable) - -instance Debug variable => Debug (SomeVariableName variable) - -instance (Debug variable, Diff variable) => Diff (SomeVariableName variable) - -instance - Injection (SomeVariableName variable) (ElementVariableName variable) - where - injection = _Ctor @"SomeVariableNameElement" - {-# INLINE injection #-} - -instance - Injection (SomeVariableName variable) (SetVariableName variable) - where - injection = _Ctor @"SomeVariableNameSet" - {-# INLINE injection #-} - {-|'Variable' corresponds to the @variable@ syntactic category from the Semantics of K, Section 9.1.4 (Patterns). @@ -200,6 +133,10 @@ instance From Variable Variable where from = id {-# INLINE from #-} +instance From VariableName VariableName where + from = id + {-# INLINE from #-} + instance NamedVariable Variable where type VariableNameOf Variable = VariableName @@ -275,7 +212,7 @@ prop> (==) x y === (==) (toVariable x) (toVariable y) -} class - (Ord variable, From variable Variable, SortedVariable variable) + (Ord variable, Ord (VariableNameOf variable), From (VariableNameOf variable) VariableName, From variable Variable, SortedVariable variable) => NamedVariable variable where type VariableNameOf variable @@ -283,7 +220,8 @@ class isoVariable1 :: Iso' variable (Variable1 (VariableNameOf variable)) lensVariableName - :: (NamedVariable variable1, NamedVariable variable2) + :: forall variable1 variable2 + . (NamedVariable variable1, NamedVariable variable2) => Lens variable1 variable2 (VariableNameOf variable1) (VariableNameOf variable2) @@ -313,6 +251,14 @@ fromVariable = from @Variable @variable toVariable :: forall variable. From variable Variable => variable -> Variable toVariable = from @variable @Variable +fromVariableName + :: forall variable. From VariableName variable => VariableName -> variable +fromVariableName = from @VariableName @variable + +toVariableName + :: forall variable. From variable VariableName => variable -> VariableName +toVariableName = from @variable @VariableName + {- | 'SortedVariable' is a Kore variable with a known sort. -} @@ -382,6 +328,10 @@ instance NamedVariable Concrete where instance VariableBase Concrete +instance From VariableName Void where + from = error "Cannot construct a variable in a concrete term!" + {-# INLINE from #-} + instance From Variable Concrete where from = error "Cannot construct a variable in a concrete term!" {-# INLINE from #-} @@ -390,6 +340,129 @@ instance From Concrete variable where from = \case {} {-# INLINE from #-} +-- * Variable names + +data VariableName = + VariableName + { base :: !Id + , counter :: !(Maybe (Sup Natural)) + } + deriving (Eq, Ord, Show) + deriving (GHC.Generic) + +instance Hashable VariableName + +instance NFData VariableName + +instance SOP.Generic VariableName + +instance SOP.HasDatatypeInfo VariableName + +instance Debug VariableName + +instance Diff VariableName + +-- * Element variables + +newtype ElementVariableName variable = + ElementVariableName { unElementVariableName :: variable } + deriving (Eq, Ord, Show) + deriving (Functor) + deriving (Foldable, Traversable) + deriving (GHC.Generic, GHC.Generic1) + +instance Semigroup a => Semigroup (ElementVariableName a) where + (<>) a b = ElementVariableName (on (<>) unElementVariableName a b) + {-# INLINE (<>) #-} + +instance Monoid a => Monoid (ElementVariableName a) where + mempty = ElementVariableName mempty + {-# INLINE mempty #-} + +instance Applicative ElementVariableName where + pure = ElementVariableName + {-# INLINE pure #-} + + (<*>) (ElementVariableName f) (ElementVariableName a) = + ElementVariableName (f a) + {-# INLINE (<*>) #-} + +instance Distributive ElementVariableName where + distribute = ElementVariableName . fmap unElementVariableName + {-# INLINE distribute #-} + +instance Hashable variable => Hashable (ElementVariableName variable) + +instance NFData variable => NFData (ElementVariableName variable) + +instance SOP.Generic (ElementVariableName variable) + +instance SOP.HasDatatypeInfo (ElementVariableName variable) + +instance Debug variable => Debug (ElementVariableName variable) + +instance (Debug variable, Diff variable) => Diff (ElementVariableName variable) + +-- * Set variables + +instance + From variable VariableName + => From (ElementVariableName variable) VariableName + where + from = from . unElementVariableName + +newtype SetVariableName variable = + SetVariableName { unSetVariableName :: variable } + deriving (Eq, Ord, Show) + deriving (Functor) + deriving (Foldable, Traversable) + deriving (GHC.Generic, GHC.Generic1) + +instance Semigroup a => Semigroup (SetVariableName a) where + (<>) a b = SetVariableName (on (<>) unSetVariableName a b) + +instance Monoid a => Monoid (SetVariableName a) where + mempty = SetVariableName mempty + {-# INLINE mempty #-} + +instance Applicative SetVariableName where + pure = SetVariableName + {-# INLINE pure #-} + + (<*>) (SetVariableName f) (SetVariableName a) = + SetVariableName (f a) + {-# INLINE (<*>) #-} + +instance Distributive SetVariableName where + distribute = SetVariableName . fmap unSetVariableName + {-# INLINE distribute #-} + +instance Hashable variable => Hashable (SetVariableName variable) + +instance NFData variable => NFData (SetVariableName variable) + +instance SOP.Generic (SetVariableName variable) + +instance SOP.HasDatatypeInfo (SetVariableName variable) + +instance Debug variable => Debug (SetVariableName variable) + +instance (Debug variable, Diff variable) => Diff (SetVariableName variable) + +instance + From variable VariableName => From (SetVariableName variable) VariableName + where + from = from . unSetVariableName + +-- * Variable occurrences + +{- | @Variable1@ is an occurrence of a variable in a Kore pattern. + +The @variable@ parameter is the type of variable names. + +Every occurrence of a variable carries the 'Sort' of the variable. + + -} data Variable1 variable = Variable1 { variableName1 :: !variable @@ -419,3 +492,191 @@ instance Unparse variable => Unparse (Variable1 variable) where <> unparse variableSort1 unparse2 Variable1 { variableName1 } = unparse2 variableName1 + +{- | @SomeVariableName@ is the name of a variable in a pattern. + +@SomeVariableName@ may be an 'ElementVariableName' or a 'SetVariableName'. + + -} +data SomeVariableName variable + = SomeVariableNameElement !(ElementVariableName variable) + | SomeVariableNameSet !(SetVariableName variable) + deriving (Eq, Ord, Show) + deriving (Functor) + deriving (Foldable, Traversable) + deriving (GHC.Generic) + +instance Hashable variable => Hashable (SomeVariableName variable) + +instance NFData variable => NFData (SomeVariableName variable) + +instance SOP.Generic (SomeVariableName variable) + +instance SOP.HasDatatypeInfo (SomeVariableName variable) + +instance Debug variable => Debug (SomeVariableName variable) + +instance (Debug variable, Diff variable) => Diff (SomeVariableName variable) + +instance + Injection (SomeVariableName variable) (ElementVariableName variable) + where + injection = _Ctor @"SomeVariableNameElement" + {-# INLINE injection #-} + +instance + Injection (SomeVariableName variable) (SetVariableName variable) + where + injection = _Ctor @"SomeVariableNameSet" + {-# INLINE injection #-} + +instance + From variable VariableName => From (SomeVariableName variable) VariableName + where + from = extractL . fmap from + +{- | 'AdjSomeVariableName' is the right adjoint of 'SomeVariableName'. + +The fields of product type 'AdjSomeVariableName' align with the constructors of +sum type 'SomeVariableName'. + +In practice, 'AdjSomeVariableName' are used to represent mappings that +transform 'ElementVariableName' and 'SetVariableName' separately while +preserving each kind of variable. For example, the type +@ + 'AdjSomeVariableName' (a -> b) +@ +is a restriction of the type +@ + 'SomeVariableName' a -> 'SomeVariableName' b +@ +where the former ensures that (element, set) variables are mapped to (element, +set) variables respectively. + +'AdjSomeVariableName' may be constructed and composed through its 'Applicative' +instance. @'pure' x@ constructs an 'AdjSomeVariableName' with the same value @x@ +in both fields. @f '<*>' a@ composes two 'AdjSomeVariableName' by applying the +function in each field of @f@ to the value in the corresponding field of @a@. + + -} +data AdjSomeVariableName a = + AdjSomeVariableName + { adjSomeVariableNameElement :: ElementVariableName a + -- ^ compare to: 'SomeVariableNameElement' + , adjSomeVariableNameSet :: SetVariableName a + -- ^ compare to: 'SomeVariableNameSet' + } + deriving (Functor) + deriving (GHC.Generic1) + +instance Semigroup a => Semigroup (AdjSomeVariableName a) where + (<>) a b = + AdjSomeVariableName + { adjSomeVariableNameElement = on (<>) adjSomeVariableNameElement a b + , adjSomeVariableNameSet = on (<>) adjSomeVariableNameSet a b + } + {-# INLINE (<>) #-} + +instance Monoid a => Monoid (AdjSomeVariableName a) where + mempty = + AdjSomeVariableName + { adjSomeVariableNameElement = mempty + , adjSomeVariableNameSet = mempty + } + {-# INLINE mempty #-} + +instance Applicative AdjSomeVariableName where + pure a = AdjSomeVariableName (ElementVariableName a) (SetVariableName a) + {-# INLINE pure #-} + + (<*>) fs as = + AdjSomeVariableName + { adjSomeVariableNameElement = + adjSomeVariableNameElement fs <*> adjSomeVariableNameElement as + , adjSomeVariableNameSet = + adjSomeVariableNameSet fs <*> adjSomeVariableNameSet as + } + {-# INLINE (<*>) #-} + +instance Distributive AdjSomeVariableName where + distribute f = + AdjSomeVariableName + { adjSomeVariableNameElement = collect adjSomeVariableNameElement f + , adjSomeVariableNameSet = collect adjSomeVariableNameSet f + } + {-# INLINE distribute #-} + +instance Representable AdjSomeVariableName where + type Rep AdjSomeVariableName = SomeVariableName () + tabulate = tabulateAdjunction + index = indexAdjunction + +instance Adjunction SomeVariableName AdjSomeVariableName where + unit a = + AdjSomeVariableName + (pure . SomeVariableNameElement . pure $ a) + (pure . SomeVariableNameSet . pure $ a) + {-# INLINE unit #-} + + counit (SomeVariableNameElement adj) = + unElementVariableName + . adjSomeVariableNameElement + . unElementVariableName + $ adj + counit (SomeVariableNameSet adj) = + unSetVariableName + . adjSomeVariableNameSet + . unSetVariableName + $ adj + {-# INLINE counit #-} + +mapSomeVariableName + :: AdjSomeVariableName (variable1 -> variable2) + -> SomeVariableName variable1 -> SomeVariableName variable2 +mapSomeVariableName adj variable1 = + fmap (index adj idx) variable1 + where + idx = () <$ variable1 + +mapElementVariableName + :: AdjSomeVariableName (variable1 -> variable2) + -> ElementVariableName variable1 + -> ElementVariableName variable2 +mapElementVariableName adj = + (<*>) (adjSomeVariableNameElement adj) + +mapSetVariableName + :: AdjSomeVariableName (variable1 -> variable2) + -> SetVariableName variable1 + -> SetVariableName variable2 +mapSetVariableName adj = + (<*>) (adjSomeVariableNameSet adj) + +traverseSomeVariableName + :: Applicative f + => AdjSomeVariableName (variable1 -> f variable2) + -> SomeVariableName variable1 -> f (SomeVariableName variable2) +traverseSomeVariableName adj variable1 = + traverse (index adj idx) variable1 + where + idx = () <$ variable1 + +traverseElementVariableName + :: forall variable1 variable2 f + . Applicative f + => AdjSomeVariableName (variable1 -> f variable2) + -> ElementVariableName variable1 + -> f (ElementVariableName variable2) +traverseElementVariableName adj = + sequenceA . (<*>) (adjSomeVariableNameElement adj) + +traverseSetVariableName + :: Applicative f + => AdjSomeVariableName (variable1 -> f variable2) + -> SetVariableName variable1 + -> f (SetVariableName variable2) +traverseSetVariableName adj = + sequenceA . (<*>) (adjSomeVariableNameSet adj) + +toVoid :: any -> Maybe Void +toVoid = const Nothing diff --git a/kore/src/Kore/Unification/Error.hs b/kore/src/Kore/Unification/Error.hs index 8bb119f9a1..dce211b2c3 100644 --- a/kore/src/Kore/Unification/Error.hs +++ b/kore/src/Kore/Unification/Error.hs @@ -27,7 +27,6 @@ import Kore.Sort import Kore.Syntax.Application import Kore.Syntax.Variable import Kore.Unparser -import Kore.Variables.UnifiedVariable import Pretty ( Pretty ) @@ -55,7 +54,7 @@ unsupportedPatterns => String -> TermLike variable -> TermLike variable -> UnificationError unsupportedPatterns message = on (UnsupportedPatterns message) - $ mapVariables toUnifiedVariable + $ mapVariables (pure toVariableName) instance Pretty UnificationError where pretty UnsupportedPatterns { message, first, second } = diff --git a/kore/src/Kore/Variables/Target.hs b/kore/src/Kore/Variables/Target.hs index fbb8323072..1bd1f65a82 100644 --- a/kore/src/Kore/Variables/Target.hs +++ b/kore/src/Kore/Variables/Target.hs @@ -42,7 +42,6 @@ import Kore.Variables.Fresh ( FreshPartialOrd (..) , FreshVariable (..) ) -import Kore.Variables.UnifiedVariable {- | Distinguish variables by their source. @@ -98,7 +97,7 @@ unTargetElement = fmap unTarget unTargetSet :: SetVariable (Target variable) -> SetVariable variable unTargetSet = fmap unTarget -unTargetUnified :: AdjUnifiedVariable (Target variable -> variable) +unTargetUnified :: AdjSomeVariableName (Target variable -> variable) unTargetUnified = pure unTarget mkElementTarget @@ -111,7 +110,7 @@ mkSetTarget -> SetVariable (Target variable) mkSetTarget = fmap Target -mkUnifiedTarget :: AdjUnifiedVariable (variable -> Target variable) +mkUnifiedTarget :: AdjSomeVariableName (variable -> Target variable) mkUnifiedTarget = pure Target isTarget :: Target variable -> Bool @@ -128,7 +127,7 @@ mkSetNonTarget -> SetVariable (Target variable) mkSetNonTarget = fmap NonTarget -mkUnifiedNonTarget :: AdjUnifiedVariable (variable -> Target variable) +mkUnifiedNonTarget :: AdjSomeVariableName (variable -> Target variable) mkUnifiedNonTarget = pure NonTarget isNonTarget :: Target variable -> Bool @@ -205,11 +204,15 @@ instance unparse2 (NonTarget var) = unparse2 var targetIfEqual - :: Eq variable + :: NamedVariable variable => ElementVariable variable - -> ElementVariable variable - -> ElementVariable (Target variable) -targetIfEqual boundVariable variable = - if boundVariable == variable - then mkElementTarget variable - else mkElementNonTarget variable + -> VariableNameOf variable + -> VariableNameOf (Target variable) +targetIfEqual boundVariable variableName = + if boundVariableName == variableName + then Target variableName + else NonTarget variableName + where + boundVariableName = + Lens.view lensVariableName boundVariable + & unElementVariableName diff --git a/kore/src/Kore/Variables/UnifiedVariable.hs b/kore/src/Kore/Variables/UnifiedVariable.hs index 03787e8c78..5d6073ec61 100644 --- a/kore/src/Kore/Variables/UnifiedVariable.hs +++ b/kore/src/Kore/Variables/UnifiedVariable.hs @@ -15,13 +15,10 @@ module Kore.Variables.UnifiedVariable , unifiedVariableSort , refreshElementVariable , refreshSetVariable - -- * AdjUnifiedVariable + -- * AdjSomeVariableName , MapVariables - , AdjUnifiedVariable (..) , asConcreteUnifiedVariable , fromConcreteUnifiedVariable - , toUnifiedVariable - , fromUnifiedVariable , mapUnifiedVariable , traverseUnifiedVariable -- * UnifiedVariableMap @@ -258,72 +255,33 @@ refreshSetVariable avoiding = fmap expectSetVar . refreshVariable avoiding . SetVar type MapVariables variable1 variable2 term1 term2 = - AdjUnifiedVariable (variable1 -> variable2) -> term1 -> term2 + AdjSomeVariableName (VariableNameOf variable1 -> VariableNameOf variable2) + -> term1 -> term2 -{- | 'AdjUnifiedVariable' is the right adjoint of 'UnifiedVariable'. - -Where 'UnifiedVariable' is a sum type, 'AdjUnifiedVariable' is a product type -with one field for each constructor. A 'UnifiedVariable' can be used to select -one field from the 'AdjUnifiedVariable'. - -In practice, 'AdjUnifiedVariable' are used to represent morphisms that transform -'ElementVariable' and 'SetVariable' separately while preserving each kind of -variable; that is, the type @'AdjUnifiedVariable' (a -> b)@ is a restriction of -the type @'UnifiedVariable' a -> 'UnifiedVariable' b@ - - -} -data AdjUnifiedVariable a = - AdjUnifiedVariable - { elemVar :: ElementVariable a - , setVar :: SetVariable a - } - deriving (Functor) - -instance Applicative AdjUnifiedVariable where - pure a = AdjUnifiedVariable (ElementVariable a) (SetVariable a) - {-# INLINE pure #-} - - (<*>) fs as = - AdjUnifiedVariable - { elemVar = elemVar fs <*> elemVar as - , setVar = setVar fs <*> setVar as - } - {-# INLINE (<*>) #-} - -asConcreteUnifiedVariable :: AdjUnifiedVariable (variable -> Maybe Concrete) +asConcreteUnifiedVariable + :: AdjSomeVariableName (any -> Maybe Void) asConcreteUnifiedVariable = pure (const Nothing) -fromConcreteUnifiedVariable :: AdjUnifiedVariable (Concrete -> variable) +fromConcreteUnifiedVariable + :: AdjSomeVariableName (Void -> any) fromConcreteUnifiedVariable = pure (\case {}) mapUnifiedVariable - :: AdjUnifiedVariable (variable1 -> variable2) - -> UnifiedVariable variable1 -> UnifiedVariable variable2 -mapUnifiedVariable AdjUnifiedVariable { elemVar, setVar } = - \case - ElemVar elementVariable -> ElemVar $ elemVar <*> elementVariable - SetVar setVariable -> SetVar $ setVar <*> setVariable + :: (NamedVariable variable1, NamedVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> VariableNameOf variable2) + -> UnifiedVariable variable1 -> UnifiedVariable variable2 +mapUnifiedVariable adj = + Lens.over lensVariableName (mapSomeVariableName adj) traverseUnifiedVariable - :: Applicative f - => AdjUnifiedVariable (variable1 -> f variable2) - -> UnifiedVariable variable1 -> f (UnifiedVariable variable2) -traverseUnifiedVariable AdjUnifiedVariable { elemVar, setVar } = - \case - ElemVar elementVariable -> - ElemVar <$> sequenceA (elemVar <*> elementVariable) - SetVar setVariable -> - SetVar <$> sequenceA (setVar <*> setVariable) - -toUnifiedVariable - :: NamedVariable variable - => AdjUnifiedVariable (variable -> Variable) -toUnifiedVariable = pure toVariable - -fromUnifiedVariable - :: From Variable variable - => AdjUnifiedVariable (Variable -> variable) -fromUnifiedVariable = pure fromVariable + :: Applicative f + => (NamedVariable variable1, NamedVariable variable2) + => AdjSomeVariableName + (VariableNameOf variable1 -> f (VariableNameOf variable2)) + -> UnifiedVariable variable1 -> f (UnifiedVariable variable2) +traverseUnifiedVariable adj = + Lens.traverseOf lensVariableName (traverseSomeVariableName adj) type VariableMap meta variable1 variable2 = Map (meta variable1) (meta variable2) diff --git a/kore/test/Test/Kore/Internal/Substitution.hs b/kore/test/Test/Kore/Internal/Substitution.hs index 267f88b067..49ce01dcbb 100644 --- a/kore/test/Test/Kore/Internal/Substitution.hs +++ b/kore/test/Test/Kore/Internal/Substitution.hs @@ -136,11 +136,11 @@ mapVariablesTests = [ testCase "map id over empty is empty" $ assertEqual "" (wrap mempty) - . mapVariables (pure id) $ emptySubst + . mapVariables @Variable @Variable (pure id) $ emptySubst , testCase "map id over wrap empty is normalized empty" $ assertEqual "" (wrap mempty) - . mapVariables (pure id) $ wrap emptyRawSubst + . mapVariables @Variable @Variable (pure id) $ wrap emptyRawSubst , testCase "map id over singleton == id" $ assertEqual "" (wrap singletonSubst) diff --git a/kore/test/Test/Kore/Internal/TermLike.hs b/kore/test/Test/Kore/Internal/TermLike.hs index 2f4581c986..f9deb86d13 100644 --- a/kore/test/Test/Kore/Internal/TermLike.hs +++ b/kore/test/Test/Kore/Internal/TermLike.hs @@ -373,19 +373,41 @@ test_renaming = , testSet "\\nu" mkNu ] where - mapElementVariables' (getElementVariable -> v) = - mapVariables (pure id) { elemVar = ElementVariable (const v) } - mapSetVariables' (getSetVariable -> v) = - mapVariables (pure id) { setVar = SetVariable (const v) } + mapElementVariables' variable = + mapVariables (pure id) + { adjSomeVariableNameElement = + ElementVariableName . const + $ unElementVariableName variableName1 + } + where + Variable1 { variableName1 } = toVariable1 variable + mapSetVariables' variable = + mapVariables (pure id) + { adjSomeVariableNameSet = + SetVariableName . const + $ unSetVariableName variableName1 + } + where + Variable1 { variableName1 } = toVariable1 variable - traverseElementVariables' (getElementVariable -> v) = + traverseElementVariables' variable = runIdentity . traverseVariables (pure return) - { elemVar = ElementVariable (const $ return v) } - traverseSetVariables' (getSetVariable -> v) = + { adjSomeVariableNameElement = + ElementVariableName . const + $ return $ unElementVariableName variableName1 + } + where + Variable1 { variableName1 } = toVariable1 variable + traverseSetVariables' variable = runIdentity . traverseVariables (pure return) - { setVar = SetVariable (const $ return v) } + { adjSomeVariableNameSet = + SetVariableName . const + $ return $ unSetVariableName variableName1 + } + where + Variable1 { variableName1 } = toVariable1 variable doesNotCapture :: HasCallStack diff --git a/kore/test/Test/Kore/Step/Function/Integration.hs b/kore/test/Test/Kore/Step/Function/Integration.hs index 54cdc804c5..8647b9a0b7 100644 --- a/kore/test/Test/Kore/Step/Function/Integration.hs +++ b/kore/test/Test/Kore/Step/Function/Integration.hs @@ -1330,8 +1330,8 @@ mapVariables mapVariables = Pattern.mapVariables (pure worker) where - worker :: Variable -> variable - worker v = fromVariable v { variableCounter = Just (Element 1) } + worker :: VariableName -> (VariableNameOf variable) + worker v = fromVariableName v { counter = Just (Element 1) } mockEvaluator :: Monad simplifier diff --git a/kore/test/Test/Kore/Step/Rule/Simplify.hs b/kore/test/Test/Kore/Step/Rule/Simplify.hs index 74eaffff58..5791a3632f 100644 --- a/kore/test/Test/Kore/Step/Rule/Simplify.hs +++ b/kore/test/Test/Kore/Step/Rule/Simplify.hs @@ -64,8 +64,8 @@ import Kore.Step.Simplification.Simplify import qualified Kore.Step.SMT.Declaration.All as SMT.All import Kore.Syntax.Variable ( Variable + , fromVariableName ) -import Kore.Variables.UnifiedVariable import qualified Test.Kore.Step.MockSymbols as Mock import Test.SMT @@ -332,13 +332,13 @@ test_simplifyClaimRule = :: InternalVariable variable => Predicate Variable -> Predicate variable - liftPredicate = Predicate.mapVariables fromUnifiedVariable + liftPredicate = Predicate.mapVariables (pure fromVariableName) liftTermLike :: InternalVariable variable => TermLike Variable -> TermLike variable - liftTermLike = TermLike.mapVariables fromUnifiedVariable + liftTermLike = TermLike.mapVariables (pure fromVariableName) liftReplacement :: InternalVariable variable diff --git a/kore/test/Test/Kore/Step/Simplification/Ceil.hs b/kore/test/Test/Kore/Step/Simplification/Ceil.hs index 8107ffd15a..6b054c3c5f 100644 --- a/kore/test/Test/Kore/Step/Simplification/Ceil.hs +++ b/kore/test/Test/Kore/Step/Simplification/Ceil.hs @@ -490,8 +490,8 @@ mapVariables mapVariables = Pattern.mapVariables (pure worker) where - worker :: Variable -> variable - worker v = fromVariable v { variableCounter = Just (Sup.Element 1) } + worker :: VariableName -> (VariableNameOf variable) + worker v = fromVariableName v { counter = Just (Sup.Element 1) } makeCeil :: InternalVariable variable diff --git a/kore/test/Test/Kore/Variables/Fresh.hs b/kore/test/Test/Kore/Variables/Fresh.hs index 8a7185d771..606eaf6a2a 100644 --- a/kore/test/Test/Kore/Variables/Fresh.hs +++ b/kore/test/Test/Kore/Variables/Fresh.hs @@ -319,11 +319,14 @@ test_refreshVariable = setNonTargetOriginal = mkSetNonTarget setOriginal avoidST = Set.singleton setTargetOriginal - unifiedTarget = mapUnifiedVariable mkUnifiedTarget + unifiedTarget = mapUnifiedVariable (pure Target) - unifiedNonTarget = mapUnifiedVariable mkUnifiedTarget + unifiedNonTarget = mapUnifiedVariable (pure Target) -- UnifiedVariable (Target Variable) + unifiedElemTargetOriginal, unifiedElemNonTargetOriginal, + unifiedSetTargetOriginal, unifiedSetNonTargetOriginal + :: UnifiedVariable (Target Variable) unifiedElemTargetOriginal = unifiedTarget unifiedElemOriginal unifiedElemNonTargetOriginal = unifiedNonTarget unifiedElemOriginal unifiedSetTargetOriginal = unifiedTarget unifiedSetOriginal diff --git a/kore/test/Test/Kore/Variables/V.hs b/kore/test/Test/Kore/Variables/V.hs index 2eee354486..f0d8ab44c7 100644 --- a/kore/test/Test/Kore/Variables/V.hs +++ b/kore/test/Test/Kore/Variables/V.hs @@ -48,9 +48,15 @@ instance SortedVariable V where instance From Variable V where from = error "Not implemented" +instance From VariableName V where + from = error "Not implemented" + instance From V Variable where from = error "Not implemented" +instance From V VariableName where + from = error "Not implemented" + instance NamedVariable V where type VariableNameOf V = V diff --git a/kore/test/Test/Kore/Variables/W.hs b/kore/test/Test/Kore/Variables/W.hs index 404bbd6763..2994b4622f 100644 --- a/kore/test/Test/Kore/Variables/W.hs +++ b/kore/test/Test/Kore/Variables/W.hs @@ -19,7 +19,6 @@ import Debug import Kore.Internal.TermLike import Kore.Unparser import Kore.Variables.Fresh -import Kore.Variables.UnifiedVariable import Pretty import Test.Kore.Variables.V @@ -51,9 +50,15 @@ instance SortedVariable W where instance From Variable W where from = error "Not implemented" +instance From VariableName W where + from = error "Not implemented" + instance From W Variable where from = error "Not implemented" +instance From W VariableName where + from = error "Not implemented" + instance NamedVariable W where type VariableNameOf W = W @@ -86,7 +91,7 @@ instance VariableBase W showVar :: V -> W showVar (V i n) = W (show i) n -showUnifiedVar :: AdjUnifiedVariable (V -> W) +showUnifiedVar :: AdjSomeVariableName (V -> W) showUnifiedVar = pure showVar war' :: String -> TermLike W From d5113dd3ee45128e632ca6640a8c08aab6d95fb7 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 26 May 2020 09:55:25 -0500 Subject: [PATCH 12/16] Remove UnifiedVariableMap --- kore/src/Kore/Internal/TermLike/TermLike.hs | 5 +- kore/src/Kore/Variables/UnifiedVariable.hs | 96 --------------------- 2 files changed, 1 insertion(+), 100 deletions(-) diff --git a/kore/src/Kore/Internal/TermLike/TermLike.hs b/kore/src/Kore/Internal/TermLike/TermLike.hs index 3ae53e4661..fc9d6e829b 100644 --- a/kore/src/Kore/Internal/TermLike/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike/TermLike.hs @@ -137,10 +137,7 @@ import Kore.Variables.Fresh ( FreshPartialOrd ) import qualified Kore.Variables.Fresh as Fresh -import Kore.Variables.UnifiedVariable hiding - ( renameElementVariable - , renameSetVariable - ) +import Kore.Variables.UnifiedVariable import qualified Pretty import qualified SQL diff --git a/kore/src/Kore/Variables/UnifiedVariable.hs b/kore/src/Kore/Variables/UnifiedVariable.hs index 5d6073ec61..633b993388 100644 --- a/kore/src/Kore/Variables/UnifiedVariable.hs +++ b/kore/src/Kore/Variables/UnifiedVariable.hs @@ -15,38 +15,18 @@ module Kore.Variables.UnifiedVariable , unifiedVariableSort , refreshElementVariable , refreshSetVariable - -- * AdjSomeVariableName , MapVariables - , asConcreteUnifiedVariable - , fromConcreteUnifiedVariable , mapUnifiedVariable , traverseUnifiedVariable - -- * UnifiedVariableMap - , VariableMap - , UnifiedVariableMap - , renameElementVariable, renameSetVariable - , lookupRenamedElementVariable, lookupRenamedSetVariable - -- * Re-exports - , Kleisli (..) ) where import Prelude.Kore -import Control.Arrow - ( Kleisli (..) - ) import Control.DeepSeq ( NFData ) import qualified Control.Lens as Lens import Data.Functor.Const -import Data.Generics.Product - ( field - ) -import Data.Map.Strict - ( Map - ) -import qualified Data.Map.Strict as Map import Data.Set ( Set ) @@ -258,14 +238,6 @@ type MapVariables variable1 variable2 term1 term2 = AdjSomeVariableName (VariableNameOf variable1 -> VariableNameOf variable2) -> term1 -> term2 -asConcreteUnifiedVariable - :: AdjSomeVariableName (any -> Maybe Void) -asConcreteUnifiedVariable = pure (const Nothing) - -fromConcreteUnifiedVariable - :: AdjSomeVariableName (Void -> any) -fromConcreteUnifiedVariable = pure (\case {}) - mapUnifiedVariable :: (NamedVariable variable1, NamedVariable variable2) => AdjSomeVariableName @@ -282,71 +254,3 @@ traverseUnifiedVariable -> UnifiedVariable variable1 -> f (UnifiedVariable variable2) traverseUnifiedVariable adj = Lens.traverseOf lensVariableName (traverseSomeVariableName adj) - -type VariableMap meta variable1 variable2 = - Map (meta variable1) (meta variable2) - -data UnifiedVariableMap variable1 variable2 = - UnifiedVariableMap - { setVariables - :: !(VariableMap SetVariable variable1 variable2) - , elementVariables - :: !(VariableMap ElementVariable variable1 variable2) - } - deriving (Generic) - -instance - Ord variable1 => Semigroup (UnifiedVariableMap variable1 variable2) - where - (<>) a b = - UnifiedVariableMap - { 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 - => SetVariable variable1 - -> SetVariable variable2 - -> UnifiedVariableMap variable1 variable2 - -> UnifiedVariableMap variable1 variable2 -renameSetVariable variable1 variable2 = - Lens.over - (field @"setVariables") - (Map.insert variable1 variable2) -{-# INLINE renameSetVariable #-} - -renameElementVariable - :: Ord variable1 - => ElementVariable variable1 - -> ElementVariable variable2 - -> UnifiedVariableMap variable1 variable2 - -> UnifiedVariableMap variable1 variable2 -renameElementVariable variable1 variable2 = - Lens.over - (field @"elementVariables") - (Map.insert variable1 variable2) -{-# INLINE renameElementVariable #-} - -lookupRenamedElementVariable - :: Ord variable1 - => ElementVariable variable1 - -> UnifiedVariableMap variable1 variable2 - -> Maybe (ElementVariable variable2) -lookupRenamedElementVariable variable = - Map.lookup variable . elementVariables -{-# INLINE lookupRenamedElementVariable #-} - -lookupRenamedSetVariable - :: Ord variable1 - => SetVariable variable1 - -> UnifiedVariableMap variable1 variable2 - -> Maybe (SetVariable variable2) -lookupRenamedSetVariable variable = - Map.lookup variable . setVariables -{-# INLINE lookupRenamedSetVariable #-} From 6cf5f4e1498560ce6db09a97b9d08d3b4ed6fe7f Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 26 May 2020 10:24:30 -0500 Subject: [PATCH 13/16] Add documentation for instance From Void _ --- kore/src/From.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/kore/src/From.hs b/kore/src/From.hs index 193843c0d4..cd8258c728 100644 --- a/kore/src/From.hs +++ b/kore/src/From.hs @@ -43,6 +43,8 @@ let b = let a :: A = _ in from @_ @B a class From from to where from :: from -> to +{- | This instance implements the principle /ex falso quodlibet/. + -} instance From Void any where from = absurd {-# INLINE from #-} From b30b7ffc4358754b43566ca070b455c1dceedaff Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 26 May 2020 10:31:52 -0500 Subject: [PATCH 14/16] Remove Kore.Variables.Target.unTargetUnified --- kore/src/Kore/Equation/Application.hs | 6 +++--- kore/src/Kore/Step/Simplification/TermLike.hs | 5 ++--- kore/src/Kore/Variables/Target.hs | 4 ---- 3 files changed, 5 insertions(+), 10 deletions(-) diff --git a/kore/src/Kore/Equation/Application.hs b/kore/src/Kore/Equation/Application.hs index 3c73f2f541..32692d0d33 100644 --- a/kore/src/Kore/Equation/Application.hs +++ b/kore/src/Kore/Equation/Application.hs @@ -225,10 +225,10 @@ applyMatchResult equation matchResult@(predicate, substitution) = do _ -> return () let predicate' = Predicate.substitute substitution predicate - & Predicate.mapVariables Target.unTargetUnified + & Predicate.mapVariables (pure Target.unTarget) equation' = Equation.substitute substitution equation - & Equation.mapVariables Target.unTargetUnified + & Equation.mapVariables (pure Target.unTarget) return (equation', predicate') where equationVariables = freeVariables equation & FreeVariables.toList @@ -305,7 +305,7 @@ checkRequires sideCondition predicate requires = -- TODO (thomas.tuegel): Do not unwrap sideCondition. sideCondition' = SideCondition.mapVariables - Target.unTargetUnified + (pure Target.unTarget) sideCondition assertBottom orCondition diff --git a/kore/src/Kore/Step/Simplification/TermLike.hs b/kore/src/Kore/Step/Simplification/TermLike.hs index 61c3dfc172..1fd7f77d5a 100644 --- a/kore/src/Kore/Step/Simplification/TermLike.hs +++ b/kore/src/Kore/Step/Simplification/TermLike.hs @@ -152,7 +152,7 @@ import qualified Kore.Variables.Binding as Binding import Kore.Variables.Target ( Target (..) , targetIfEqual - , unTargetUnified + , unTarget ) import qualified Pretty @@ -407,8 +407,7 @@ simplifyInternal term sideCondition = do (targetSideCondition sideCondition) (targetSimplifiedChildren simplifiedChildren) let unTargetedResults = - Pattern.mapVariables unTargetUnified - <$> targetedResults + Pattern.mapVariables (pure unTarget) <$> targetedResults return unTargetedResults where refresh = Lens.over Binding.existsBinder refreshElementBinder diff --git a/kore/src/Kore/Variables/Target.hs b/kore/src/Kore/Variables/Target.hs index 1bd1f65a82..32605dffd1 100644 --- a/kore/src/Kore/Variables/Target.hs +++ b/kore/src/Kore/Variables/Target.hs @@ -11,7 +11,6 @@ module Kore.Variables.Target , unTarget , unTargetElement , unTargetSet - , unTargetUnified , mkElementTarget , mkSetTarget , mkUnifiedTarget @@ -97,9 +96,6 @@ unTargetElement = fmap unTarget unTargetSet :: SetVariable (Target variable) -> SetVariable variable unTargetSet = fmap unTarget -unTargetUnified :: AdjSomeVariableName (Target variable -> variable) -unTargetUnified = pure unTarget - mkElementTarget :: ElementVariable variable -> ElementVariable (Target variable) From 2ed119518295fdc9c3bb35434635258ba1cefa94 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 26 May 2020 10:38:17 -0500 Subject: [PATCH 15/16] Refactor Kore.Equation.Equation.refreshVariables --- kore/src/Kore/Equation/Equation.hs | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/kore/src/Kore/Equation/Equation.hs b/kore/src/Kore/Equation/Equation.hs index 1bd164b1e0..3ac57aa05e 100644 --- a/kore/src/Kore/Equation/Equation.hs +++ b/kore/src/Kore/Equation/Equation.hs @@ -234,18 +234,25 @@ refreshVariables rename & Map.map (Lens.view lensVariableName) & Map.mapKeys (Lens.view lensVariableName) + lookupSomeVariableName + :: forall variable' + . Injection (SomeVariableName (VariableNameOf variable)) variable' + => variable' + -> variable' + lookupSomeVariableName variable = + do + let injected = inject @(SomeVariableName _) variable + someVariableName <- Map.lookup injected rename' + retract someVariableName + & fromMaybe variable adj = AdjSomeVariableName { adjSomeVariableNameElement = - ElementVariableName . Lens.over _Wrapped $ \variable -> - case Map.lookup (inject @(SomeVariableName _) variable) rename' of - Just (SomeVariableNameElement variable') -> variable' - _ -> variable + ElementVariableName . Lens.over _Wrapped + $ lookupSomeVariableName @(ElementVariableName _) , adjSomeVariableNameSet = - SetVariableName . Lens.over _Wrapped $ \variable -> - case Map.lookup (inject @(SomeVariableName _) variable) rename' of - Just (SomeVariableNameSet variable') -> variable' - _ -> variable + SetVariableName . Lens.over _Wrapped + $ lookupSomeVariableName @(SetVariableName _) } subst = From 6aaf313a7ddd4630685748924b38a4d5ba09a80a Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 26 May 2020 14:29:29 -0500 Subject: [PATCH 16/16] Linting --- kore/src/Kore/Internal/TermLike/Renaming.hs | 42 +++++++++---------- .../Test/Kore/Step/Function/Integration.hs | 2 +- .../Test/Kore/Step/Simplification/Ceil.hs | 2 +- 3 files changed, 23 insertions(+), 23 deletions(-) diff --git a/kore/src/Kore/Internal/TermLike/Renaming.hs b/kore/src/Kore/Internal/TermLike/Renaming.hs index ab4b03f12f..c34a7079ea 100644 --- a/kore/src/Kore/Internal/TermLike/Renaming.hs +++ b/kore/src/Kore/Internal/TermLike/Renaming.hs @@ -43,6 +43,7 @@ import Data.Map.Strict ( Map ) import qualified Data.Map.Strict as Map +import qualified Data.Maybe as Maybe import Kore.Attribute.Pattern.FreeVariables ( FreeVariables @@ -98,18 +99,23 @@ renameFreeVariables adj = idx :: SomeVariableName () (variable1, idx) = splitL someVariableName1 renaming1 <- index adj' idx variable1 - let renaming' = tabulate $ \idx' -> if idx == idx' then renaming1 else mempty + let renaming' = + tabulate renamer + where + renamer idx' + | idx' == idx = renaming1 + | otherwise = mempty pure (renaming <> renaming') {-# INLINE renameFreeVariables #-} askSomeVariableName - :: HasCallStack - => Ord variable1 + :: Ord variable1 => MonadReader (VariableNameMap' variable1 variable2) m => AdjSomeVariableName (variable1 -> m variable2) askSomeVariableName = - tabulate $ \idx -> \variable1 -> - Reader.asks $ maybe (error "undefined") id . Map.lookup variable1 . flip index idx + tabulate $ \idx variable1 -> + -- Maybe.fromJust is safe because the variable must be renamed + Reader.asks $ Maybe.fromJust . Map.lookup variable1 . flip index idx {-# INLINE askSomeVariableName #-} askElementVariableName @@ -152,7 +158,7 @@ renameElementBinder -> Binder (ElementVariable variable1) (m any) -> m (Binder (ElementVariable variable2) any) renameElementBinder trElemVar avoiding binder = do - let Binder { binderVariable, binderChild } = binder + let Binder { binderVariable } = binder elementVariable2 <- trElemVar binderVariable let binderVariable' = refreshElementVariable @@ -160,17 +166,14 @@ renameElementBinder trElemVar avoiding binder = do elementVariable2 & fromMaybe elementVariable2 withRenaming = - renameElementVariable + (renameSomeVariable . inject) ((,) <$> Lens.view lensVariableName binderVariable <*> Lens.view lensVariableName binderVariable' ) - binderChild' <- Reader.local withRenaming binderChild - let binder' = Binder - { binderVariable = binderVariable' - , binderChild = binderChild' - } - pure binder' + binder { binderVariable = binderVariable' } + & sequenceA + & Reader.local withRenaming {-# INLINE renameElementBinder #-} renameSomeVariable @@ -210,7 +213,7 @@ renameSetBinder -> Binder (SetVariable variable1) (m any) -> m (Binder (SetVariable variable2) any) renameSetBinder trSetVar avoiding binder = do - let Binder { binderVariable, binderChild } = binder + let Binder { binderVariable } = binder setVariable2 <- trSetVar binderVariable let binderVariable' = refreshSetVariable @@ -218,15 +221,12 @@ renameSetBinder trSetVar avoiding binder = do setVariable2 & fromMaybe setVariable2 withRenaming = - renameSetVariable + (renameSomeVariable . inject) ((,) <$> Lens.view lensVariableName binderVariable <*> Lens.view lensVariableName binderVariable' ) - binderChild' <- Reader.local withRenaming binderChild - let binder' = Binder - { binderVariable = binderVariable' - , binderChild = binderChild' - } - pure binder' + binder { binderVariable = binderVariable' } + & sequenceA + & Reader.local withRenaming {-# INLINE renameSetBinder #-} diff --git a/kore/test/Test/Kore/Step/Function/Integration.hs b/kore/test/Test/Kore/Step/Function/Integration.hs index 8647b9a0b7..94e96c853a 100644 --- a/kore/test/Test/Kore/Step/Function/Integration.hs +++ b/kore/test/Test/Kore/Step/Function/Integration.hs @@ -1330,7 +1330,7 @@ mapVariables mapVariables = Pattern.mapVariables (pure worker) where - worker :: VariableName -> (VariableNameOf variable) + worker :: VariableName -> VariableNameOf variable worker v = fromVariableName v { counter = Just (Element 1) } mockEvaluator diff --git a/kore/test/Test/Kore/Step/Simplification/Ceil.hs b/kore/test/Test/Kore/Step/Simplification/Ceil.hs index 6b054c3c5f..0370c72f15 100644 --- a/kore/test/Test/Kore/Step/Simplification/Ceil.hs +++ b/kore/test/Test/Kore/Step/Simplification/Ceil.hs @@ -490,7 +490,7 @@ mapVariables mapVariables = Pattern.mapVariables (pure worker) where - worker :: VariableName -> (VariableNameOf variable) + worker :: VariableName -> VariableNameOf variable worker v = fromVariableName v { counter = Just (Sup.Element 1) } makeCeil