From bf318157142194e5dfdab732212b11d0a2068365 Mon Sep 17 00:00:00 2001 From: Joey Hess Date: Wed, 9 Mar 2016 11:44:22 -0400 Subject: rename to Target --- src/Propellor/Types/Target.hs | 136 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 136 insertions(+) create mode 100644 src/Propellor/Types/Target.hs (limited to 'src/Propellor/Types/Target.hs') diff --git a/src/Propellor/Types/Target.hs b/src/Propellor/Types/Target.hs new file mode 100644 index 00000000..c9739ad4 --- /dev/null +++ b/src/Propellor/Types/Target.hs @@ -0,0 +1,136 @@ +{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, TypeFamilies, UndecidableInstances #-} + +module Propellor.Types.Target ( + Target(..), + Targeting(..), + debian, + buntish, + freeBSD, + unixlike, + includeTarget, + intersectTarget, +) where + +import Network.BSD (HostName) +import Data.Typeable +import Data.String + +----- DEMO ---------- +data Property os = Property os (IO ()) + +mkProperty :: os -> IO () -> Property os +mkProperty os a = Property os a + +-- Intentionally a type error! :) +--foo :: Property (Targeting '[OSDebian, OSFreeBSD]) +--foo = mkProperty supportedos $ do +-- ensureProperty supportedos jail +-- where supportedos = includeTarget debian + +jail :: Property (Targeting '[OSFreeBSD]) +jail = Property freeBSD $ do + return () +----- END DEMO ---------- + +-- | A Target system, where a Property is indended to be used. +data Target = OSDebian | OSBuntish | OSFreeBSD + deriving (Show, Eq) + +-- | A type-level and value-level list of targets. +data Targeting (os :: [Target]) = Targeting [Target] + deriving (Show, Eq) + +-- | Any unix-like OS. +unixlike :: Targeting '[OSDebian, OSBuntish, OSFreeBSD] +unixlike = Targeting [OSDebian, OSBuntish, OSFreeBSD] + +debian :: Targeting '[OSDebian] +debian = typeOS OSDebian + +buntish :: Targeting '[OSBuntish] +buntish = typeOS OSBuntish + +freeBSD :: Targeting '[OSFreeBSD] +freeBSD = typeOS OSFreeBSD + +typeOS :: Target -> Targeting os +typeOS o = Targeting [o] + +ensureProperty + :: (CannotCombineTargets outertarget innertarget (IntersectTargeting outertarget innertarget) ~ CanCombineTargets) + => Targeting outertarget + -> Property (Targeting innertarget) + -> IO () +ensureProperty outeros (Property inneros a) = a + +-- | Adds to a list of targets. +includeTarget + :: (r ~ ConcatTargeting l1 l2) + => Targeting l1 + -> Targeting l2 + -> Targeting r +includeTarget (Targeting l1) (Targeting l2) = Targeting (l1 ++ l2) + +-- | Type level concat for Targeting. +type family ConcatTargeting (list1 :: [a]) (list2 :: [a]) :: [a] +type instance ConcatTargeting '[] list2 = list2 +type instance ConcatTargeting (a ': rest) list2 = a ': ConcatTargeting rest list2 + +-- | The intersection between two lists of Targets. +intersectTarget + :: (r ~ IntersectTargeting l1 l2, CannotCombineTargets l1 l2 r ~ CanCombineTargets) + => Targeting l1 + -> Targeting l2 + -> Targeting r +intersectTarget (Targeting l1) (Targeting l2) = Targeting (filter (`elem` l2) l1) + +-- | Detect intersection of two lists that don't have any common OS. +-- +-- The name of this was chosen to make type errors a more understandable. +type family CannotCombineTargets (list1 :: [a]) (list2 :: [a]) (listr :: [a]) :: CheckIntersection +type instance CannotCombineTargets l1 l2 '[] = 'CannotCombineTargets +type instance CannotCombineTargets l1 l2 (a ': rest) = 'CanCombineTargets +data CheckIntersection = CannotCombineTargets | CanCombineTargets + +-- | Type level intersection for Targeting +type family IntersectTargeting (list1 :: [a]) (list2 :: [a]) :: [a] +type instance IntersectTargeting '[] list2 = '[] +type instance IntersectTargeting (a ': rest) list2 = + If (ElemTargeting a list2) + (a ': IntersectTargeting rest list2) + (IntersectTargeting rest list2) + +-- | Type level elem for Targeting +type family ElemTargeting (a :: Target) (list :: [Target]) :: Bool +type instance ElemTargeting a '[] = 'False +type instance ElemTargeting a (b ': bs) = EqTarget a b || ElemTargeting a bs + +-- | Type level equality for Target +-- +-- This is a very clumsy implmentation, but it works back to ghc 7.6. +type family EqTarget (a :: Target) (b :: Target) :: Bool +type instance EqTarget OSDebian OSDebian = 'True +type instance EqTarget OSBuntish OSBuntish = 'True +type instance EqTarget OSFreeBSD OSFreeBSD = 'True +type instance EqTarget OSDebian OSBuntish = 'False +type instance EqTarget OSDebian OSFreeBSD = 'False +type instance EqTarget OSBuntish OSDebian = 'False +type instance EqTarget OSBuntish OSFreeBSD = 'False +type instance EqTarget OSFreeBSD OSDebian = 'False +type instance EqTarget OSFreeBSD OSBuntish = 'False +-- More modern version if the combinatiorial explosion gets too bad later: +-- +-- type family EqTarget (a :: Target) (b :: Target) where +-- EqTarget a a = True +-- EqTarget a b = False + +-- | This is in Data.Type.Bool with 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 -- cgit v1.2.3