propellor

propellor config for hosts.
git clone git://git.ricketyspace.net/propellor.git
Log | Files | Refs | LICENSE

MetaTypes.hs (9187B)


      1 {-# LANGUAGE TypeOperators, PolyKinds, DataKinds, ConstraintKinds #-}
      2 {-# LANGUAGE TypeFamilies, UndecidableInstances, FlexibleInstances, GADTs #-}
      3 {-# LANGUAGE CPP #-}
      4 
      5 module Propellor.Types.MetaTypes (
      6 	MetaType(..),
      7 	UnixLike,
      8 	Linux,
      9 	DebianLike,
     10 	Debian,
     11 	Buntish,
     12 	ArchLinux,
     13 	FreeBSD,
     14 	HasInfo,
     15 	MetaTypes,
     16 	type (+),
     17 	sing,
     18 	SingI,
     19 	IncludesInfo,
     20 	Targets,
     21 	NonTargets,
     22 	PrettyPrintMetaTypes,
     23 	IsSubset,
     24 	Combine,
     25 	CheckCombinable,
     26 	CheckCombinableNote,
     27 	type (&&),
     28 	Not,
     29 	EqT,
     30 	Union,
     31 	Intersect,
     32 	Difference,
     33 	IfStuck,
     34 	DelayError,
     35 	DelayErrorFcf,
     36 ) where
     37 
     38 import Propellor.Types.Singletons
     39 import Propellor.Types.OS
     40 
     41 import GHC.TypeLits hiding (type (+))
     42 import GHC.Exts (Constraint)
     43 import Data.Type.Bool
     44 
     45 #ifdef WITH_TYPE_ERRORS
     46 import Type.Errors
     47 #else
     48 type family IfStuck (expr :: k) (b :: k1) (c :: k1) :: k1 where
     49 	IfStuck expr b c = c
     50 type family DelayError msg where
     51 	DelayError msg = TypeError msg
     52 type family DelayErrorFcf msg where
     53 	DelayErrorFcf msg = TypeError msg
     54 #endif
     55 
     56 data MetaType
     57 	= Targeting TargetOS -- ^ A target OS of a Property
     58 	| WithInfo           -- ^ Indicates that a Property has associated Info
     59 	deriving (Show, Eq, Ord)
     60 
     61 -- | Any unix-like system
     62 type UnixLike = MetaTypes
     63 	'[ 'Targeting 'OSDebian
     64 	, 'Targeting 'OSBuntish
     65 	, 'Targeting 'OSArchLinux
     66 	, 'Targeting 'OSFreeBSD
     67 	]
     68 
     69 -- | Any linux system
     70 type Linux = MetaTypes
     71 	'[ 'Targeting 'OSDebian
     72 	, 'Targeting 'OSBuntish
     73 	, 'Targeting 'OSArchLinux
     74 	]
     75 
     76 -- | Debian and derivatives.
     77 type DebianLike = MetaTypes '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish ]
     78 type Debian = MetaTypes '[ 'Targeting 'OSDebian ]
     79 type Buntish = MetaTypes '[ 'Targeting 'OSBuntish ]
     80 type FreeBSD = MetaTypes '[ 'Targeting 'OSFreeBSD ]
     81 type ArchLinux = MetaTypes '[ 'Targeting 'OSArchLinux ]
     82 
     83 -- | Used to indicate that a Property adds Info to the Host where it's used.
     84 type HasInfo = MetaTypes '[ 'WithInfo ]
     85 
     86 type family IncludesInfo t :: Bool where
     87 	IncludesInfo (MetaTypes l) = Elem 'WithInfo l
     88 
     89 type MetaTypes = Sing
     90 
     91 -- This boilerplate would not be needed if the singletons library were
     92 -- used.
     93 data instance Sing (x :: MetaType) where
     94 	OSDebianS :: Sing ('Targeting 'OSDebian)
     95 	OSBuntishS :: Sing ('Targeting 'OSBuntish)
     96 	OSFreeBSDS :: Sing ('Targeting 'OSFreeBSD)
     97 	OSArchLinuxS :: Sing ('Targeting 'OSArchLinux)
     98 	WithInfoS :: Sing 'WithInfo
     99 instance SingI ('Targeting 'OSDebian) where sing = OSDebianS
    100 instance SingI ('Targeting 'OSBuntish) where sing = OSBuntishS
    101 instance SingI ('Targeting 'OSFreeBSD) where sing = OSFreeBSDS
    102 instance SingI ('Targeting 'OSArchLinux) where sing = OSArchLinuxS
    103 instance SingI 'WithInfo where sing = WithInfoS
    104 instance SingKind ('KProxy :: KProxy MetaType) where
    105 	type DemoteRep ('KProxy :: KProxy MetaType) = MetaType
    106 	fromSing OSDebianS = Targeting OSDebian
    107 	fromSing OSBuntishS = Targeting OSBuntish
    108 	fromSing OSFreeBSDS = Targeting OSFreeBSD
    109 	fromSing OSArchLinuxS = Targeting OSArchLinux
    110 	fromSing WithInfoS = WithInfo
    111 
    112 -- | Convenience type operator to combine two `MetaTypes` lists.
    113 --
    114 -- For example:
    115 --
    116 -- > HasInfo + Debian
    117 --
    118 -- Which is shorthand for this type:
    119 --
    120 -- > MetaTypes '[WithInfo, Targeting OSDebian]
    121 type family a + b :: * where
    122 	(MetaTypes a) + (MetaTypes b) = MetaTypes (Concat a b)
    123 
    124 type family Concat (list1 :: [a]) (list2 :: [a]) :: [a] where
    125 	Concat '[] bs = bs
    126 	Concat (a ': as) bs = a ': (Concat as bs)
    127 
    128 -- | Combine two MetaTypes lists, yielding a list
    129 -- that has targets present in both, and nontargets present in either.
    130 type family Combine (list1 :: [a]) (list2 :: [a]) :: [a] where
    131 	Combine (list1 :: [a]) (list2 :: [a]) =
    132 		(Concat
    133 			(NonTargets list1 `Union` NonTargets list2)
    134 			(Targets list1 `Intersect` Targets list2)
    135 		)
    136 
    137 -- | Checks if two MetaTypes lists can be safly combined;
    138 -- eg they have at least one Target in common.
    139 type family IsCombinable (list1 :: [a]) (list2 :: [a]) :: Bool where
    140 	-- As a special case, if either list is empty or only WithInfo, 
    141 	-- let it be combined with the other. This relies on MetaTypes
    142 	-- list always containing at least one Target, so can only happen
    143 	-- if there's already been a type error. This special case lets the
    144 	-- type checker show only the original type error, and not
    145 	-- subsequent errors due to later CheckCombinable constraints.
    146 	IsCombinable '[] list2 = 'True
    147 	IsCombinable list1 '[] = 'True
    148 	IsCombinable ('WithInfo ': list1) list2 = IsCombinable list1 list2
    149 	IsCombinable list1 ('WithInfo ': list2) = IsCombinable list1 list2
    150 	IsCombinable list1 list2 =
    151 		Not (Null (Combine (Targets list1) (Targets list2)))
    152 
    153 -- | This (or CheckCombinableNote) should be used anywhere Combine is used, 
    154 -- as an additional constraint. For example:
    155 --
    156 -- > foo :: CheckCombinable x y => x -> y -> Combine x y
    157 type family CheckCombinable (list1 :: [a]) (list2 :: [a]) :: Constraint where
    158 	CheckCombinable list1 list2 =
    159 		If (IsCombinable list1 list2)
    160 			('True ~ 'True)
    161 			(CannotCombine list1 list2 'Nothing)
    162 
    163 -- | Allows providing an additional note.
    164 type family CheckCombinableNote (list1 :: [a]) (list2 :: [a]) (note :: ErrorMessage) :: Constraint where
    165 	CheckCombinableNote list1 list2 note =
    166 		If (IsCombinable list1 list2)
    167 			('True ~ 'True)
    168 			(CannotCombine list1 list2
    169 				('Just ('Text "(" ':<>: note ':<>: 'Text ")"))
    170 			)
    171 
    172 -- Checking IfStuck is to avoid massive and useless error message leaking 
    173 -- type families from this module.
    174 type family CannotCombine (list1 :: [a]) (list2 :: [a]) (note :: Maybe ErrorMessage) :: Constraint where
    175 	CannotCombine list1 list2 note = 
    176 		IfStuck list1
    177 			(IfStuck list2
    178 				(DelayError (CannotCombineMessage UnknownType UnknownType UnknownTypeNote))
    179 				(DelayErrorFcf (CannotCombineMessage UnknownType (PrettyPrintMetaTypes list2) UnknownTypeNote))
    180 			)
    181 			(IfStuck list2
    182 				(DelayError (CannotCombineMessage (PrettyPrintMetaTypes list1) UnknownType UnknownTypeNote))
    183 				(DelayErrorFcf (CannotCombineMessage (PrettyPrintMetaTypes list1) (PrettyPrintMetaTypes list2) note))
    184 			)
    185 
    186 type family UnknownType :: ErrorMessage where
    187 	UnknownType = 'Text "<unknown>"
    188 
    189 type family UnknownTypeNote :: Maybe ErrorMessage where
    190 	UnknownTypeNote = 'Just ('Text "(Property <unknown> is often caused by applying a Property constructor to the wrong number of arguments.)")
    191 
    192 type family CannotCombineMessage (a :: ErrorMessage) (b :: ErrorMessage) (note :: Maybe ErrorMessage) :: ErrorMessage where
    193 	CannotCombineMessage a b ('Just note) =
    194 		CannotCombineMessage a b 'Nothing
    195 			':$$: note
    196 	CannotCombineMessage a b 'Nothing =
    197 		'Text "Cannot combine Properties:"
    198 			':$$: ('Text "  Property " ':<>: a)
    199 			':$$: ('Text "  Property " ':<>: b)
    200 
    201 type family IsTarget (a :: t) :: Bool where
    202 	IsTarget ('Targeting a) = 'True
    203 	IsTarget 'WithInfo = 'False
    204 
    205 type family Targets (l :: [a]) :: [a] where
    206 	Targets '[] = '[]
    207 	Targets (x ': xs) =
    208 		If (IsTarget x)
    209 			(x ': Targets xs)
    210 			(Targets xs)
    211 
    212 type family NonTargets (l :: [a]) :: [a] where
    213 	NonTargets '[] = '[]
    214 	NonTargets (x ': xs) =
    215 		If (IsTarget x)
    216 			(NonTargets xs)
    217 			(x ': NonTargets xs)
    218 
    219 -- | Pretty-prints a list of MetaTypes for display in a type error message.
    220 type family PrettyPrintMetaTypes (l :: [MetaType]) :: ErrorMessage where
    221 	PrettyPrintMetaTypes '[] = 'Text "<none>"
    222 	PrettyPrintMetaTypes (t ': '[]) = PrettyPrintMetaType t
    223 	PrettyPrintMetaTypes (t ': ts) = 
    224 		PrettyPrintMetaType t ':<>: 'Text " + " ':<>: PrettyPrintMetaTypes ts
    225 
    226 type family PrettyPrintMetaType t :: ErrorMessage where
    227 	PrettyPrintMetaType 'WithInfo = 'ShowType HasInfo
    228 	PrettyPrintMetaType ('Targeting 'OSDebian) = 'ShowType Debian
    229 	PrettyPrintMetaType ('Targeting 'OSBuntish) = 'ShowType Buntish
    230 	PrettyPrintMetaType ('Targeting 'OSFreeBSD) = 'ShowType FreeBSD
    231 	PrettyPrintMetaType ('Targeting 'OSArchLinux) = 'ShowType ArchLinux
    232 	PrettyPrintMetaType ('Targeting t) = 'ShowType t
    233 
    234 -- | Type level elem
    235 type family Elem (a :: t) (list :: [t]) :: Bool where
    236 	Elem a '[] = 'False
    237 	Elem a (b ': bs) = EqT a b || Elem a bs
    238 
    239 -- | Type level union.
    240 type family Union (list1 :: [a]) (list2 :: [a]) :: [a] where
    241 	Union '[] list2 = list2
    242 	Union (a ': rest) list2 =
    243 		If (Elem a list2 || Elem a rest)
    244 			(Union rest list2)
    245 			(a ': Union rest list2)
    246 
    247 -- | Type level intersection. Duplicate list items are eliminated.
    248 type family Intersect (list1 :: [a]) (list2 :: [a]) :: [a] where
    249 	Intersect '[] list2 = '[]
    250 	Intersect (a ': rest) list2 = 
    251 		If (Elem a list2 && Not (Elem a rest))
    252 			(a ': Intersect rest list2)
    253 			(Intersect rest list2)
    254 
    255 -- | Type level difference. Items that are in the first list, but not in
    256 -- the second.
    257 type family Difference (list1 :: [a]) (list2 :: [a]) :: [a] where
    258 	Difference '[] list2 = '[]
    259 	Difference (a ': rest) list2 =
    260 		If (Elem a list2)
    261 			(Difference rest list2)
    262 			(a ': Difference rest list2)
    263 
    264 -- | Every item in the subset must be in the superset.
    265 type family IsSubset (subset :: [a]) (superset :: [a]) :: Bool where
    266 	IsSubset '[] superset = 'True
    267 	IsSubset (s ': rest) superset =
    268 		If (Elem s superset)
    269 			(IsSubset rest superset)
    270 			'False
    271 
    272 -- | Type level null.
    273 type family Null (list :: [a]) :: Bool where
    274 	Null '[] = 'True
    275 	Null l = 'False
    276 
    277 -- | Type level equality of metatypes.
    278 type family EqT (a :: MetaType) (b :: MetaType) where
    279  	EqT a a = 'True
    280  	EqT a b = 'False