summaryrefslogtreecommitdiff
path: root/src/Propellor/Types
diff options
context:
space:
mode:
authorJoey Hess2016-03-19 16:49:48 -0400
committerJoey Hess2016-03-19 16:49:48 -0400
commit72005752b3a86303217cb67add37ca5d515da8ae (patch)
treeb6e1b163961154e60614a5d983210d9c821d31bd /src/Propellor/Types
parent368eaf569846199f4a68fe52d74ff50e19cc3820 (diff)
wip
Diffstat (limited to 'src/Propellor/Types')
-rw-r--r--src/Propellor/Types/Target.hs103
1 files changed, 44 insertions, 59 deletions
diff --git a/src/Propellor/Types/Target.hs b/src/Propellor/Types/Target.hs
index 549cf99b..3b21d1f8 100644
--- a/src/Propellor/Types/Target.hs
+++ b/src/Propellor/Types/Target.hs
@@ -135,7 +135,9 @@ outerPropTypes (Property proptypes _) = OuterPropTypes proptypes
-- with HasInfo in its PropTypes. Doing so would cause the info associated
-- with the property to be lost.
ensureProperty
- :: ((Targets inner `NotSuperset` Targets outer) ~ CanCombine, CannotUseEnsurePropertyWithInfo inner ~ True)
+ :: ((Targets inner `NotSuperset` Targets outer) ~ CanCombineTargets
+ , CannotUseEnsurePropertyWithInfo inner ~ True
+ )
=> OuterPropTypes outer
-> Property (WithTypes inner)
-> IO ()
@@ -146,15 +148,17 @@ type family CannotUseEnsurePropertyWithInfo (l :: [a]) :: Bool
type instance CannotUseEnsurePropertyWithInfo '[] = 'True
type instance CannotUseEnsurePropertyWithInfo (t ': ts) = Not (t `EqT` WithInfo) && CannotUseEnsurePropertyWithInfo ts
--- | Changes the target of a property.
+-- | Tightens the PropType list of a Property, to contain fewer targets.
--
--- This can only tighten the target list to contain fewer targets.
-target
- :: (combined ~ IntersectTarget old new, CannotCombineTargets old new combined ~ CanCombineTargets)
- => Targeting newtarget
+-- Anything else in the PropType list is passed through unchanged.
+tightenTargets
+ :: ( combined ~ Concat (NonTargets old) (Intersect (Targets old) newtargets)
+ , CannotCombineTargets old new combined ~ CanCombineTargets
+ )
+ => Targeting newtargets
-> Property (WithTypes old)
- -> Property (WithTypes new)
-target newtarget (Property old a) = Property (intersectTarget old new) a
+ -> Property (WithTypes combined)
+tightenTargets _ (Property old a) = Property sing a
{-
@@ -167,54 +171,44 @@ orProperty
:: Property (Targeting a)
-> Property (Targeting b)
-> Property (Targeting (UnionTarget a b))
-orProperty a@(Property ta ioa) b@(Property tb iob) =
- Property (unionTargets ta tb) io
+orProperty a@(Property ta ioa) b@(Property tb iob) = Property sing io
where
-- TODO pick with of ioa or iob to use based on final OS of
-- system being run on.
io = undefined
--- | The union of two lists of Targets.
-unionTargets
- :: Targeting l1
- -> Targeting l2
- -> Targeting (UnionTarget l1 l2)
-unionTargets (Targeting l1) (Targeting l2) =
- Targeting $ nub $ l1 ++ l2
+-- | Type level union of lists of Targets
+type family UnionTarget (list1 :: [a]) (list2 :: [a]) :: [a]
+type instance UnionTarget '[] list2 = list2
+type instance UnionTarget (a ': rest) list2 =
+ If (ElemTarget a list2 || ElemTarget a rest)
+ (UnionTarget rest list2)
+ (a ': UnionTarget rest list2)
-}
--- | The intersection between two lists of Targets.
-intersectTarget
- :: (r ~ IntersectTarget l1 l2, CannotCombineTargets l1 l2 r ~ CanCombineTargets)
- => Targeting l1
- -> Targeting l2
- -> Targeting r
-intersectTarget (Targeting l1) (Targeting l2) =
- Targeting $ nub $ filter (`elem` l2) l1
-
-data CheckCombine = CannotCombine | CanCombine
-
-{-
+data CheckCombineTargets = CannotCombineTargets | CanCombineTargets
--- | Detect intersection of two lists that don't have any common OS.
+-- | 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.
-type family CannotCombineTargets (list1 :: [a]) (list2 :: [a]) (listr :: [a]) :: CheckCombine
+type family CannotCombineTargets (list1 :: [a]) (list2 :: [a]) (listr :: [a]) :: CheckCombineTargets
type instance CannotCombineTargets l1 l2 '[] = 'CannotCombineTargets
type instance CannotCombineTargets l1 l2 (a ': rest) = 'CanCombineTargets
--}
-
-- | Every item in the subset must be in the superset.
--
-- The name of this was chosen to make type errors a more understandable.
-type family NotSuperset (superset :: [a]) (subset :: [a]) :: CheckCombine
-type instance NotSuperset superset '[] = 'CanCombine
+type family NotSuperset (superset :: [a]) (subset :: [a]) :: CheckCombineTargets
+type instance NotSuperset superset '[] = 'CanCombineTargets
type instance NotSuperset superset (s ': rest) =
If (Elem s superset)
(NotSuperset superset rest)
- 'CannotCombine
+ 'CannotCombineTargets
+
+type family IsTarget (a :: t) :: Bool
+type instance IsTarget (Targeting a) = True
+type instance IsTarget WithInfo = False
type family Targets (l :: [a]) :: [a]
type instance Targets '[] = '[]
@@ -223,35 +217,26 @@ type instance Targets (x ': xs) =
(x ': Targets xs)
(Targets xs)
-type family IsTarget (a :: t) :: Bool
-type instance IsTarget (Targeting a) = True
-type instance IsTarget WithInfo = False
-
-{-
-
--- | Type level intersection of lists of Targets
-type family IntersectTarget (list1 :: [a]) (list2 :: [a]) :: [a]
-type instance IntersectTarget '[] list2 = '[]
-type instance IntersectTarget (a ': rest) list2 =
- If (ElemTarget a list2 && Not (ElemTarget a rest))
- (a ': IntersectTarget rest list2)
- (IntersectTarget rest list2)
-
--- | Type level union of lists of Targets
-type family UnionTarget (list1 :: [a]) (list2 :: [a]) :: [a]
-type instance UnionTarget '[] list2 = list2
-type instance UnionTarget (a ': rest) list2 =
- If (ElemTarget a list2 || ElemTarget a rest)
- (UnionTarget rest list2)
- (a ': UnionTarget rest list2)
-
--}
+type family NonTargets (l :: [a]) :: [a]
+type instance NonTargets '[] = '[]
+type instance NonTargets (x ': xs) =
+ If (IsTarget x)
+ (Targets xs)
+ (x ': Targets 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 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.