{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, ConstraintKinds #-}
{-# LANGUAGE TypeFamilies, UndecidableInstances, FlexibleInstances, GADTs #-}
{-# LANGUAGE CPP #-}
module Propellor.Types.MetaTypes (
MetaType(..),
UnixLike,
Linux,
DebianLike,
Debian,
Buntish,
ArchLinux,
FreeBSD,
HasInfo,
MetaTypes,
type (+),
sing,
SingI,
IncludesInfo,
Targets,
NonTargets,
PrettyPrintMetaTypes,
IsSubset,
Combine,
CheckCombinable,
CheckCombinableNote,
type (&&),
Not,
EqT,
Union,
Intersect,
Difference,
IfStuck,
DelayError,
DelayErrorFcf,
) where
import Propellor.Types.Singletons
import Propellor.Types.OS
import GHC.TypeLits hiding (type (+))
import GHC.Exts (Constraint)
import Data.Type.Bool
import Data.Kind (Type)
#ifdef WITH_TYPE_ERRORS
import Type.Errors
#else
type family IfStuck (expr :: k) (b :: k1) (c :: k1) :: k1 where
IfStuck expr b c = c
type family DelayError msg where
DelayError msg = TypeError msg
type family DelayErrorFcf msg where
DelayErrorFcf msg = TypeError msg
#endif
data MetaType
= Targeting TargetOS
| WithInfo
deriving (Int -> MetaType -> ShowS
[MetaType] -> ShowS
MetaType -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MetaType] -> ShowS
$cshowList :: [MetaType] -> ShowS
show :: MetaType -> String
$cshow :: MetaType -> String
showsPrec :: Int -> MetaType -> ShowS
$cshowsPrec :: Int -> MetaType -> ShowS
Show, MetaType -> MetaType -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MetaType -> MetaType -> Bool
$c/= :: MetaType -> MetaType -> Bool
== :: MetaType -> MetaType -> Bool
$c== :: MetaType -> MetaType -> Bool
Eq, Eq MetaType
MetaType -> MetaType -> Bool
MetaType -> MetaType -> Ordering
MetaType -> MetaType -> MetaType
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: MetaType -> MetaType -> MetaType
$cmin :: MetaType -> MetaType -> MetaType
max :: MetaType -> MetaType -> MetaType
$cmax :: MetaType -> MetaType -> MetaType
>= :: MetaType -> MetaType -> Bool
$c>= :: MetaType -> MetaType -> Bool
> :: MetaType -> MetaType -> Bool
$c> :: MetaType -> MetaType -> Bool
<= :: MetaType -> MetaType -> Bool
$c<= :: MetaType -> MetaType -> Bool
< :: MetaType -> MetaType -> Bool
$c< :: MetaType -> MetaType -> Bool
compare :: MetaType -> MetaType -> Ordering
$ccompare :: MetaType -> MetaType -> Ordering
Ord)
type UnixLike = MetaTypes
'[ 'Targeting 'OSDebian
, 'Targeting 'OSBuntish
, 'Targeting 'OSArchLinux
, 'Targeting 'OSFreeBSD
]
type Linux = MetaTypes
'[ 'Targeting 'OSDebian
, 'Targeting 'OSBuntish
, 'Targeting 'OSArchLinux
]
type DebianLike = MetaTypes '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish ]
type Debian = MetaTypes '[ 'Targeting 'OSDebian ]
type Buntish = MetaTypes '[ 'Targeting 'OSBuntish ]
type FreeBSD = MetaTypes '[ 'Targeting 'OSFreeBSD ]
type ArchLinux = MetaTypes '[ 'Targeting 'OSArchLinux ]
type HasInfo = MetaTypes '[ 'WithInfo ]
type family IncludesInfo t :: Bool where
IncludesInfo (MetaTypes l) = Elem 'WithInfo l
type MetaTypes = Sing
data instance Sing (x :: MetaType) where
OSDebianS :: Sing ('Targeting 'OSDebian)
OSBuntishS :: Sing ('Targeting 'OSBuntish)
OSFreeBSDS :: Sing ('Targeting 'OSFreeBSD)
OSArchLinuxS :: Sing ('Targeting 'OSArchLinux)
WithInfoS :: Sing 'WithInfo
instance SingI ('Targeting 'OSDebian) where sing :: Sing ('Targeting 'OSDebian)
sing = Sing ('Targeting 'OSDebian)
OSDebianS
instance SingI ('Targeting 'OSBuntish) where sing :: Sing ('Targeting 'OSBuntish)
sing = Sing ('Targeting 'OSBuntish)
OSBuntishS
instance SingI ('Targeting 'OSFreeBSD) where sing :: Sing ('Targeting 'OSFreeBSD)
sing = Sing ('Targeting 'OSFreeBSD)
OSFreeBSDS
instance SingI ('Targeting 'OSArchLinux) where sing :: Sing ('Targeting 'OSArchLinux)
sing = Sing ('Targeting 'OSArchLinux)
OSArchLinuxS
instance SingI 'WithInfo where sing :: Sing 'WithInfo
sing = Sing 'WithInfo
WithInfoS
instance SingKind ('KProxy :: KProxy MetaType) where
type DemoteRep ('KProxy :: KProxy MetaType) = MetaType
fromSing :: forall (a :: MetaType). Sing a -> DemoteRep 'KProxy
fromSing Sing a
R:SingMetaTypex a
OSDebianS = TargetOS -> MetaType
Targeting TargetOS
OSDebian
fromSing Sing a
R:SingMetaTypex a
OSBuntishS = TargetOS -> MetaType
Targeting TargetOS
OSBuntish
fromSing Sing a
R:SingMetaTypex a
OSFreeBSDS = TargetOS -> MetaType
Targeting TargetOS
OSFreeBSD
fromSing Sing a
R:SingMetaTypex a
OSArchLinuxS = TargetOS -> MetaType
Targeting TargetOS
OSArchLinux
fromSing Sing a
R:SingMetaTypex a
WithInfoS = MetaType
WithInfo
type family a + b :: Type where
(MetaTypes a) + (MetaTypes b) = MetaTypes (Concat a b)
type family Concat (list1 :: [a]) (list2 :: [a]) :: [a] where
Concat '[] bs = bs
Concat (a ': as) bs = a ': (Concat as bs)
type family Combine (list1 :: [a]) (list2 :: [a]) :: [a] where
Combine ('WithInfo : list1) ('WithInfo : list2) = 'WithInfo ':
list1 `Intersect` list2
Combine ('WithInfo : list1) list2 = 'WithInfo ':
list1 `Intersect` list2
Combine list1 ('WithInfo : list2) = 'WithInfo ':
list1 `Intersect` list2
Combine list1 list2 =
list1 `Intersect` list2
type family IsCombinable (list1 :: [a]) (list2 :: [a]) :: Bool where
IsCombinable '[] list2 = 'True
IsCombinable list1 '[] = 'True
IsCombinable ('WithInfo ': list1) list2 = IsCombinable list1 list2
IsCombinable list1 ('WithInfo ': list2) = IsCombinable list1 list2
IsCombinable list1 list2 =
Not (Null (Combine (Targets list1) (Targets list2)))
type family CheckCombinable (list1 :: [a]) (list2 :: [a]) :: Constraint where
CheckCombinable list1 list2 =
If (IsCombinable list1 list2)
('True ~ 'True)
(CannotCombine list1 list2 'Nothing)
type family CheckCombinableNote (list1 :: [a]) (list2 :: [a]) (note :: ErrorMessage) :: Constraint where
CheckCombinableNote list1 list2 note =
If (IsCombinable list1 list2)
('True ~ 'True)
(CannotCombine list1 list2
('Just ('Text "(" ':<>: note ':<>: 'Text ")"))
)
type family CannotCombine (list1 :: [a]) (list2 :: [a]) (note :: Maybe ErrorMessage) :: Constraint where
CannotCombine list1 list2 note =
IfStuck list1
(IfStuck list2
(DelayError (CannotCombineMessage UnknownType UnknownType UnknownTypeNote))
(DelayErrorFcf (CannotCombineMessage UnknownType (PrettyPrintMetaTypes list2) UnknownTypeNote))
)
(IfStuck list2
(DelayError (CannotCombineMessage (PrettyPrintMetaTypes list1) UnknownType UnknownTypeNote))
(DelayErrorFcf (CannotCombineMessage (PrettyPrintMetaTypes list1) (PrettyPrintMetaTypes list2) note))
)
type family UnknownType :: ErrorMessage where
UnknownType = 'Text "<unknown>"
type family UnknownTypeNote :: Maybe ErrorMessage where
UnknownTypeNote = 'Just ('Text "(Property <unknown> is often caused by applying a Property constructor to the wrong number of arguments.)")
type family CannotCombineMessage (a :: ErrorMessage) (b :: ErrorMessage) (note :: Maybe ErrorMessage) :: ErrorMessage where
CannotCombineMessage a b ('Just note) =
CannotCombineMessage a b 'Nothing
':$$: note
CannotCombineMessage a b 'Nothing =
'Text "Cannot combine Properties:"
':$$: ('Text " Property " ':<>: a)
':$$: ('Text " Property " ':<>: b)
type family IsTarget (a :: t) :: Bool where
IsTarget ('Targeting a) = 'True
IsTarget 'WithInfo = 'False
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] where
NonTargets '[] = '[]
NonTargets (x ': xs) =
If (IsTarget x)
(NonTargets xs)
(x ': NonTargets xs)
type family PrettyPrintMetaTypes (l :: [MetaType]) :: ErrorMessage where
PrettyPrintMetaTypes '[] = 'Text "<none>"
PrettyPrintMetaTypes (t ': '[]) = PrettyPrintMetaType t
PrettyPrintMetaTypes (t ': ts) =
PrettyPrintMetaType t ':<>: 'Text " + " ':<>: PrettyPrintMetaTypes ts
type family PrettyPrintMetaType t :: ErrorMessage where
PrettyPrintMetaType 'WithInfo = 'ShowType HasInfo
PrettyPrintMetaType ('Targeting 'OSDebian) = 'ShowType Debian
PrettyPrintMetaType ('Targeting 'OSBuntish) = 'ShowType Buntish
PrettyPrintMetaType ('Targeting 'OSFreeBSD) = 'ShowType FreeBSD
PrettyPrintMetaType ('Targeting 'OSArchLinux) = 'ShowType ArchLinux
PrettyPrintMetaType ('Targeting t) = 'ShowType t
type family Elem (a :: t) (list :: [t]) :: Bool where
Elem a '[] = 'False
Elem a (b ': bs) = EqT a b || Elem a bs
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 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 family Difference (list1 :: [a]) (list2 :: [a]) :: [a] where
Difference '[] list2 = '[]
Difference (a ': rest) list2 =
If (Elem a list2)
(Difference rest list2)
(a ': Difference rest list2)
type family IsSubset (subset :: [a]) (superset :: [a]) :: Bool where
IsSubset '[] superset = 'True
IsSubset (s ': rest) superset =
If (Elem s superset)
(IsSubset rest superset)
'False
type family Null (list :: [a]) :: Bool where
Null '[] = 'True
Null l = 'False
type family EqT (a :: MetaType) (b :: MetaType) where
EqT a a = 'True
EqT a b = 'False