From 2a3530695c90f889df91f6a3a38a8989091f65a3 Mon Sep 17 00:00:00 2001 From: Joey Hess Date: Thu, 24 Mar 2016 22:01:30 -0400 Subject: fix combineWith to only accept properties that have common targets --- src/Propellor/Types.hs | 17 +++++++++-------- src/Propellor/Types/MetaTypes.hs | 17 ++++++++++++----- 2 files changed, 21 insertions(+), 13 deletions(-) (limited to 'src') diff --git a/src/Propellor/Types.hs b/src/Propellor/Types.hs index 743787cc..3cd5a368 100644 --- a/src/Propellor/Types.hs +++ b/src/Propellor/Types.hs @@ -5,6 +5,7 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE DataKinds #-} module Propellor.Types ( Host(..) @@ -244,12 +245,12 @@ 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 (Sing x)) (Property (Sing y)) = Property (Sing (Union x y)) -type instance CombinedType (RevertableProperty (Sing x) (Sing x')) (RevertableProperty (Sing y) (Sing y')) = RevertableProperty (Sing (Union x y)) (Sing (Union x' y')) +type instance CombinedType (Property (Sing x)) (Property (Sing y)) = Property (Sing (Combine x y)) +type instance CombinedType (RevertableProperty (Sing x) (Sing x')) (RevertableProperty (Sing y) (Sing y')) = RevertableProperty (Sing (Combine x y)) (Sing (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 (Sing x) (Sing x')) (Property (Sing y)) = Property (Sing (Union x y)) -type instance CombinedType (Property (Sing x)) (RevertableProperty (Sing y) (Sing y')) = Property (Sing (Union x y)) +type instance CombinedType (RevertableProperty (Sing x) (Sing x')) (Property (Sing y)) = Property (Sing (Combine x y)) +type instance CombinedType (Property (Sing x)) (RevertableProperty (Sing y) (Sing y')) = Property (Sing (Combine x y)) type ResultCombiner = Propellor Result -> Propellor Result -> Propellor Result @@ -267,15 +268,15 @@ class Combines x y where -> y -> CombinedType x y -instance (CombinedType (Property (Sing x)) (Property (Sing y)) ~ Property (Sing (Union x y)), SingI (Union x y)) => Combines (Property (Sing x)) (Property (Sing y)) where +instance (CannotCombineTargets x y (Combine x y) ~ 'CanCombineTargets, SingI (Combine x y)) => Combines (Property (Sing x)) (Property (Sing y)) where combineWith f _ (Property t1 d1 a1 i1 c1) (Property _t2 d2 a2 i2 c2) = Property sing d1 (f a1 a2) i1 (ChildProperty d2 a2 i2 c2 : c1) -instance (CombinedType (RevertableProperty (Sing x) (Sing x')) (RevertableProperty (Sing y) (Sing y')) ~ RevertableProperty (Sing (Union x y)) (Sing (Union x' y')), SingI (Union x y), SingI (Union x' y')) => Combines (RevertableProperty (Sing x) (Sing x')) (RevertableProperty (Sing y) (Sing y')) where +instance (CannotCombineTargets x y (Combine x y) ~ 'CanCombineTargets, CannotCombineTargets x' y' (Combine x' y') ~ 'CanCombineTargets, SingI (Combine x y), SingI (Combine x' y')) => Combines (RevertableProperty (Sing x) (Sing x')) (RevertableProperty (Sing y) (Sing y')) where combineWith sf tf (RevertableProperty s1 t1) (RevertableProperty s2 t2) = RevertableProperty (combineWith sf tf s1 s2) (combineWith tf sf t1 t2) -instance (CombinedType (RevertableProperty (Sing x) (Sing x')) (Property (Sing y)) ~ Property (Sing (Union x y)), SingI (Union x y)) => Combines (RevertableProperty (Sing x) (Sing x')) (Property (Sing y)) where +instance (CannotCombineTargets x y (Combine x y) ~ 'CanCombineTargets, SingI (Combine x y)) => Combines (RevertableProperty (Sing x) (Sing x')) (Property (Sing y)) where combineWith sf tf (RevertableProperty x _) y = combineWith sf tf x y -instance (CombinedType (Property (Sing x)) (RevertableProperty (Sing y) (Sing y')) ~ Property (Sing (Union x y)), SingI (Union x y)) => Combines (Property (Sing x)) (RevertableProperty (Sing y) (Sing y')) where +instance (CannotCombineTargets x y (Combine x y) ~ 'CanCombineTargets, SingI (Combine x y)) => Combines (Property (Sing x)) (RevertableProperty (Sing y) (Sing y')) where combineWith sf tf x (RevertableProperty y _) = combineWith sf tf x y diff --git a/src/Propellor/Types/MetaTypes.hs b/src/Propellor/Types/MetaTypes.hs index 60af33ef..6edea291 100644 --- a/src/Propellor/Types/MetaTypes.hs +++ b/src/Propellor/Types/MetaTypes.hs @@ -13,14 +13,12 @@ module Propellor.Types.MetaTypes ( Sing, sing, SingI, - Union, - Intersect, - Concat, IncludesInfo, Targets, NonTargets, NotSuperset, CheckCombineTargets(..), + Combine, CannotCombineTargets, type (&&), Not, @@ -89,6 +87,15 @@ type family Concat (list1 :: [a]) (list2 :: [a]) :: [a] type instance Concat '[] bs = bs type instance 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 IncludesInfo t :: Bool type instance IncludesInfo (Sing l) = Elem 'WithInfo l @@ -97,8 +104,6 @@ type family CannotUseEnsurePropertyWithInfo (l :: [a]) :: Bool type instance CannotUseEnsurePropertyWithInfo '[] = 'True type instance CannotUseEnsurePropertyWithInfo (t ': ts) = Not (t `EqT` 'WithInfo) && CannotUseEnsurePropertyWithInfo ts -data CheckCombineTargets = CannotCombineTargets | CanCombineTargets - -- | Detect intersection of two lists that don't have any common targets. -- -- The name of this was chosen to make type errors a more understandable. @@ -106,6 +111,8 @@ type family CannotCombineTargets (list1 :: [a]) (list2 :: [a]) (listr :: [a]) :: type instance CannotCombineTargets l1 l2 '[] = 'CannotCombineTargets type instance CannotCombineTargets l1 l2 (a ': rest) = 'CanCombineTargets +data CheckCombineTargets = CannotCombineTargets | CanCombineTargets + -- | Every item in the subset must be in the superset. -- -- The name of this was chosen to make type errors more understandable. -- cgit v1.2.3