diff options
| -rw-r--r-- | debian/changelog | 7 | ||||
| -rw-r--r-- | src/Propellor/EnsureProperty.hs | 8 | ||||
| -rw-r--r-- | src/Propellor/PropAccum.hs | 6 | ||||
| -rw-r--r-- | src/Propellor/Types.hs | 20 | ||||
| -rw-r--r-- | src/Propellor/Types/MetaTypes.hs | 187 |
5 files changed, 99 insertions, 129 deletions
diff --git a/debian/changelog b/debian/changelog index ae97e9db..bf4df720 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,10 @@ +propellor (5.4.1) UNRELEASED; urgency=medium + + * Modernized and simplified the MetaTypes implementation now that + compatability with ghc 7 is no longer needed. + + -- Joey Hess <id@joeyh.name> Fri, 18 May 2018 10:25:05 -0400 + propellor (5.4.0) unstable; urgency=medium [ Sean Whitton ] diff --git a/src/Propellor/EnsureProperty.hs b/src/Propellor/EnsureProperty.hs index 5a07107c..6c720e2b 100644 --- a/src/Propellor/EnsureProperty.hs +++ b/src/Propellor/EnsureProperty.hs @@ -50,10 +50,10 @@ ensureProperty ensureProperty _ = maybe (return NoChange) catchPropellor . getSatisfy -- The name of this was chosen to make type errors a bit more understandable. -type family Cannot_ensureProperty_WithInfo (l :: [a]) :: Bool -type instance Cannot_ensureProperty_WithInfo '[] = 'True -type instance Cannot_ensureProperty_WithInfo (t ': ts) = - Not (t `EqT` 'WithInfo) && Cannot_ensureProperty_WithInfo ts +type family Cannot_ensureProperty_WithInfo (l :: [a]) :: Bool where + Cannot_ensureProperty_WithInfo '[] = 'True + Cannot_ensureProperty_WithInfo (t ': ts) = + Not (t `EqT` 'WithInfo) && Cannot_ensureProperty_WithInfo ts -- | Constructs a property, like `property`, but provides its -- `OuterMetaTypesWitness`. diff --git a/src/Propellor/PropAccum.hs b/src/Propellor/PropAccum.hs index 5d1d3afb..c60ced73 100644 --- a/src/Propellor/PropAccum.hs +++ b/src/Propellor/PropAccum.hs @@ -41,9 +41,9 @@ infixl 1 & infixl 1 &^ infixl 1 ! -type family GetMetaTypes x -type instance GetMetaTypes (Property (MetaTypes t)) = MetaTypes t -type instance GetMetaTypes (RevertableProperty (MetaTypes t) undo) = MetaTypes t +type family GetMetaTypes x where + GetMetaTypes (Property (MetaTypes t)) = MetaTypes t + GetMetaTypes (RevertableProperty (MetaTypes t) undo) = MetaTypes t -- | Adds a property to a Props. -- diff --git a/src/Propellor/Types.hs b/src/Propellor/Types.hs index 7cbe9f13..e10e0f5b 100644 --- a/src/Propellor/Types.hs +++ b/src/Propellor/Types.hs @@ -154,13 +154,19 @@ instance IsProp (RevertableProperty setupmetatypes undometatypes) where -- | Type level calculation of the type that results from combining two -- types of properties. -type family CombinedType x y -type instance CombinedType (Property (MetaTypes x)) (Property (MetaTypes y)) = Property (MetaTypes (Combine x y)) -type instance CombinedType (RevertableProperty (MetaTypes x) (MetaTypes x')) (RevertableProperty (MetaTypes y) (MetaTypes y')) = RevertableProperty (MetaTypes (Combine x y)) (MetaTypes (Combine x' y')) --- When only one of the properties is revertable, the combined property is --- not fully revertable, so is not a RevertableProperty. -type instance CombinedType (RevertableProperty (MetaTypes x) (MetaTypes x')) (Property (MetaTypes y)) = Property (MetaTypes (Combine x y)) -type instance CombinedType (Property (MetaTypes x)) (RevertableProperty (MetaTypes y) (MetaTypes y')) = Property (MetaTypes (Combine x y)) +type family CombinedType x y where + CombinedType (Property (MetaTypes x)) (Property (MetaTypes y)) = + Property (MetaTypes (Combine x y)) + CombinedType + (RevertableProperty (MetaTypes x) (MetaTypes x')) + (RevertableProperty (MetaTypes y) (MetaTypes y')) = + RevertableProperty (MetaTypes (Combine x y)) (MetaTypes (Combine x' y')) + -- When only one of the properties is revertable, the combined + -- property is not fully revertable, so is not a RevertableProperty. + CombinedType (RevertableProperty (MetaTypes x) (MetaTypes x')) (Property (MetaTypes y)) = + Property (MetaTypes (Combine x y)) + CombinedType (Property (MetaTypes x)) (RevertableProperty (MetaTypes y) (MetaTypes y')) = + Property (MetaTypes (Combine x y)) type ResultCombiner = Maybe (Propellor Result) -> Maybe (Propellor Result) -> Maybe (Propellor Result) diff --git a/src/Propellor/Types/MetaTypes.hs b/src/Propellor/Types/MetaTypes.hs index 4e4472eb..0c476e87 100644 --- a/src/Propellor/Types/MetaTypes.hs +++ b/src/Propellor/Types/MetaTypes.hs @@ -30,6 +30,8 @@ module Propellor.Types.MetaTypes ( import Propellor.Types.Singletons import Propellor.Types.OS +import Data.Type.Bool + data MetaType = Targeting TargetOS -- ^ A target OS of a Property | WithInfo -- ^ Indicates that a Property has associated Info @@ -60,8 +62,8 @@ type ArchLinux = MetaTypes '[ 'Targeting 'OSArchLinux ] -- | Used to indicate that a Property adds Info to the Host where it's used. type HasInfo = MetaTypes '[ 'WithInfo ] -type family IncludesInfo t :: Bool -type instance IncludesInfo (MetaTypes l) = Elem 'WithInfo l +type family IncludesInfo t :: Bool where + IncludesInfo (MetaTypes l) = Elem 'WithInfo l type MetaTypes = Sing @@ -95,21 +97,21 @@ instance SingKind ('KProxy :: KProxy MetaType) where -- Which is shorthand for this type: -- -- > MetaTypes '[WithInfo, Targeting OSDebian] -type family a + b :: ab -type instance (MetaTypes a) + (MetaTypes b) = MetaTypes (Concat a b) +type family a + b :: * where + (MetaTypes a) + (MetaTypes b) = MetaTypes (Concat a b) -type family Concat (list1 :: [a]) (list2 :: [a]) :: [a] -type instance Concat '[] bs = bs -type instance Concat (a ': as) bs = a ': (Concat as bs) +type family Concat (list1 :: [a]) (list2 :: [a]) :: [a] where + Concat '[] bs = bs + Concat (a ': as) bs = a ': (Concat as bs) -- | Combine two MetaTypes lists, yielding a list -- that has targets present in both, and nontargets present in either. -type family Combine (list1 :: [a]) (list2 :: [a]) :: [a] -type instance Combine (list1 :: [a]) (list2 :: [a]) = - (Concat - (NonTargets list1 `Union` NonTargets list2) - (Targets list1 `Intersect` Targets list2) - ) +type family Combine (list1 :: [a]) (list2 :: [a]) :: [a] where + Combine (list1 :: [a]) (list2 :: [a]) = + (Concat + (NonTargets list1 `Union` NonTargets list2) + (Targets list1 `Intersect` Targets list2) + ) -- | Checks if two MetaTypes lists can be safely combined. -- @@ -117,121 +119,76 @@ type instance Combine (list1 :: [a]) (list2 :: [a]) = -- constraint. For example: -- -- > foo :: (CheckCombinable x y ~ 'CanCombine) => x -> y -> Combine x y -type family CheckCombinable (list1 :: [a]) (list2 :: [a]) :: CheckCombine --- As a special case, if either list is empty, let it be combined with the --- other. This relies on MetaTypes list always containing at least --- one target, so can only happen if there's already been a type error. --- This special case lets the type checker show only the original type --- error, and not an extra error due to a later CheckCombinable constraint. -type instance CheckCombinable '[] list2 = 'CanCombine -type instance CheckCombinable list1 '[] = 'CanCombine -type instance CheckCombinable (l1 ': list1) (l2 ': list2) = - CheckCombinable' (Combine (l1 ': list1) (l2 ': list2)) -type family CheckCombinable' (combinedlist :: [a]) :: CheckCombine -type instance CheckCombinable' '[] = 'CannotCombineTargets -type instance CheckCombinable' (a ': rest) - = If (IsTarget a) - 'CanCombine - (CheckCombinable' rest) +type family CheckCombinable (list1 :: [a]) (list2 :: [a]) :: CheckCombine where + -- As a special case, if either list is empty, let it be combined + -- with the other. This relies on MetaTypes list always containing + -- at least one target, so can only happen if there's already been + -- a type error. This special case lets the type checker show only + -- the original type error, and not an extra error due to a later + -- CheckCombinable constraint. + CheckCombinable '[] list2 = 'CanCombine + CheckCombinable list1 '[] = 'CanCombine + CheckCombinable (l1 ': list1) (l2 ': list2) = + CheckCombinable' (Combine (l1 ': list1) (l2 ': list2)) +type family CheckCombinable' (combinedlist :: [a]) :: CheckCombine where + CheckCombinable' '[] = 'CannotCombineTargets + CheckCombinable' (a ': rest) + = If (IsTarget a) + 'CanCombine + (CheckCombinable' rest) data CheckCombine = CannotCombineTargets | CanCombine -- | Every item in the subset must be in the superset. -- -- The name of this was chosen to make type errors more understandable. -type family NotSuperset (superset :: [a]) (subset :: [a]) :: CheckCombine -type instance NotSuperset superset '[] = 'CanCombine -type instance NotSuperset superset (s ': rest) = - If (Elem s superset) - (NotSuperset superset rest) - 'CannotCombineTargets +type family NotSuperset (superset :: [a]) (subset :: [a]) :: CheckCombine where + NotSuperset superset '[] = 'CanCombine + NotSuperset superset (s ': rest) = + If (Elem s superset) + (NotSuperset superset rest) + 'CannotCombineTargets -type family IsTarget (a :: t) :: Bool -type instance IsTarget ('Targeting a) = 'True -type instance IsTarget 'WithInfo = 'False +type family IsTarget (a :: t) :: Bool where + IsTarget ('Targeting a) = 'True + IsTarget 'WithInfo = 'False -type family Targets (l :: [a]) :: [a] -type instance Targets '[] = '[] -type instance Targets (x ': xs) = - If (IsTarget x) - (x ': Targets xs) - (Targets xs) +type family Targets (l :: [a]) :: [a] where + Targets '[] = '[] + Targets (x ': xs) = + If (IsTarget x) + (x ': Targets xs) + (Targets xs) -type family NonTargets (l :: [a]) :: [a] -type instance NonTargets '[] = '[] -type instance NonTargets (x ': xs) = - If (IsTarget x) - (NonTargets xs) - (x ': NonTargets xs) +type family NonTargets (l :: [a]) :: [a] where + NonTargets '[] = '[] + NonTargets (x ': xs) = + If (IsTarget x) + (NonTargets xs) + (x ': NonTargets xs) -- | Type level elem -type family Elem (a :: t) (list :: [t]) :: Bool -type instance Elem a '[] = 'False -type instance Elem a (b ': bs) = EqT a b || Elem a bs +type family Elem (a :: t) (list :: [t]) :: Bool where + Elem a '[] = 'False + Elem a (b ': bs) = EqT a b || Elem a bs -- | Type level union. -type family Union (list1 :: [a]) (list2 :: [a]) :: [a] -type instance Union '[] list2 = list2 -type instance Union (a ': rest) list2 = - If (Elem a list2 || Elem a rest) - (Union rest list2) - (a ': Union rest list2) +type family Union (list1 :: [a]) (list2 :: [a]) :: [a] where + Union '[] list2 = list2 + Union (a ': rest) list2 = + If (Elem a list2 || Elem a rest) + (Union rest list2) + (a ': Union rest list2) -- | Type level intersection. Duplicate list items are eliminated. -type family Intersect (list1 :: [a]) (list2 :: [a]) :: [a] -type instance Intersect '[] list2 = '[] -type instance Intersect (a ': rest) list2 = - If (Elem a list2 && Not (Elem a rest)) - (a ': Intersect rest list2) - (Intersect rest list2) - --- | Type level equality --- --- This is a very clumsy implmentation, but it works back to ghc 7.6. -type family EqT (a :: t) (b :: t) :: Bool -type instance EqT ('Targeting a) ('Targeting b) = EqT a b -type instance EqT 'WithInfo 'WithInfo = 'True -type instance EqT 'WithInfo ('Targeting b) = 'False -type instance EqT ('Targeting a) 'WithInfo = 'False -type instance EqT 'OSDebian 'OSDebian = 'True -type instance EqT 'OSBuntish 'OSBuntish = 'True -type instance EqT 'OSFreeBSD 'OSFreeBSD = 'True -type instance EqT 'OSDebian 'OSBuntish = 'False -type instance EqT 'OSDebian 'OSFreeBSD = 'False -type instance EqT 'OSBuntish 'OSDebian = 'False -type instance EqT 'OSBuntish 'OSFreeBSD = 'False -type instance EqT 'OSFreeBSD 'OSDebian = 'False -type instance EqT 'OSFreeBSD 'OSBuntish = 'False -type instance EqT 'OSArchLinux 'OSArchLinux = 'True -type instance EqT 'OSArchLinux 'OSDebian = 'False -type instance EqT 'OSArchLinux 'OSBuntish = 'False -type instance EqT 'OSArchLinux 'OSFreeBSD = 'False -type instance EqT 'OSDebian 'OSArchLinux = 'False -type instance EqT 'OSBuntish 'OSArchLinux = 'False -type instance EqT 'OSFreeBSD 'OSArchLinux = 'False - --- More modern version if the combinatiorial explosion gets too bad later: --- --- type family Eq (a :: MetaType) (b :: MetaType) where --- Eq a a = True --- Eq a b = False - --- | An equivilant to the following is in Data.Type.Bool in --- modern versions of ghc, but is included here to support ghc 7.6. -type family If (cond :: Bool) (tru :: a) (fls :: a) :: a -type instance If 'True tru fls = tru -type instance If 'False tru fls = fls -type family (a :: Bool) || (b :: Bool) :: Bool -type instance 'False || 'False = 'False -type instance 'True || 'True = 'True -type instance 'True || 'False = 'True -type instance 'False || 'True = 'True -type family (a :: Bool) && (b :: Bool) :: Bool -type instance 'False && 'False = 'False -type instance 'True && 'True = 'True -type instance 'True && 'False = 'False -type instance 'False && 'True = 'False -type family Not (a :: Bool) :: Bool -type instance Not 'False = 'True -type instance Not 'True = 'False +type family Intersect (list1 :: [a]) (list2 :: [a]) :: [a] where + Intersect '[] list2 = '[] + Intersect (a ': rest) list2 = + If (Elem a list2 && Not (Elem a rest)) + (a ': Intersect rest list2) + (Intersect rest list2) +-- | Type level equality of metatypes. +type family EqT (a :: MetaType) (b :: MetaType) where + EqT a a = 'True + EqT a b = 'False |