summaryrefslogtreecommitdiff
path: root/src/Propellor/Types/OS/Typelevel.hs
blob: 2b17d87b00955252060391b4057058f82c7eef1e (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, TypeFamilies, UndecidableInstances #-}

module Propellor.Types.OS.TypeLevel (
	SupportedOS(..),
	OSList(..),
	debian,
	buntish,
	freeBSD,
	unixlike,
	combineSupportedOS,
	intersectSupportedOS,
) where

import Network.BSD (HostName)
import Data.Typeable
import Data.String
import Data.Type.Bool
import Data.Type.Equality

-- | A supported operating system.
data SupportedOS = OSDebian | OSBuntish | OSFreeBSD
	deriving (Show, Eq)

-- | A type-level and value-level list of supported operating systems.
--
-- If the list is empty, no operating system is supported.
data OSList (os :: [SupportedOS]) = OSList [SupportedOS]
	deriving (Show, Eq)

-- | Any unix-like OS.
unixlike :: OSList '[OSDebian, OSBuntish, OSFreeBSD]
unixlike = OSList [OSDebian, OSBuntish, OSFreeBSD]

debian :: OSList '[OSDebian]
debian = typeOS OSDebian

buntish :: OSList '[OSBuntish]
buntish = typeOS OSBuntish

freeBSD :: OSList '[OSFreeBSD]
freeBSD = typeOS OSFreeBSD

typeOS :: SupportedOS -> OSList os
typeOS o = OSList [o]

-- FIXME, should type check
-- foo :: OSList '[OSDebian, OSFreeBSD]
-- foo = (debian `combineSupportedOS` freeBSD ) `intersectSupportedOS` unixlike 

-- | Combines two lists of supported OS's, yielding a list with the
-- contents of both.
combineSupportedOS
	:: (r ~ ConcatOSList l1 l2)
	=> OSList l1
	-> OSList l2
	-> OSList r
combineSupportedOS (OSList l1) (OSList l2) = OSList (l1 ++ l2)

-- | Type level concat for OSList.
type family ConcatOSList (list1 :: [a]) (list2 :: [a]) :: [a]
type instance ConcatOSList '[] list2 = list2
type instance ConcatOSList (a ': rest) list2 = a ': ConcatOSList rest list2

-- | The intersection between two lists of supported OS's.
intersectSupportedOS
	:: (r ~ IntersectOSList l1 l2)
	=> OSList l1
	-> OSList l2
	-> OSList r
intersectSupportedOS (OSList l1) (OSList l2) = OSList (filter (`elem` l2) l1)

-- | Type level intersection for OSList
type family IntersectOSList (list1 :: [a]) (list2 :: [a]) :: [a]
type instance IntersectOSList '[] list2 = list2
type instance IntersectOSList (a ': rest) list2 = 
	If (ElemOSList a list2)
		(a ': IntersectOSList rest list2)
		(IntersectOSList rest list2)

-- | Type level elem for OSList
type family ElemOSList a (list :: [b]) :: Bool
type instance ElemOSList a '[] = False
type instance ElemOSList a (b ': bs) = 
	If (a == b)
		True
		(ElemOSList a bs)

-- | Type level equality for SupportedOS
type family EqOS (a :: SupportedOS) (b :: SupportedOS) where
	EqOS a a = True
	EqOS a b = False
type instance a == b = EqOS a b