git.iko.soy/type-fun
on master help sign in
add Union and intersection
7c20294Aleksey Uimanov
src/TypeFun/Data/List.hs+29−1
compare with master
unifiedsplit
@@ -12,7 +12,9 @@ module TypeFun.Data.List
12 -- * Elements lookup
12 -- * Elements lookup
13 , IndexOf
13 , IndexOf
14 , IndexOf'
14 , IndexOf'
15+ , IndicesOf
15 , Index
16 , Index
17+ , Indices
16 , Elem
18 , Elem
17 , NotElem
19 , NotElem
18 , Count
20 , Count
@@ -22,6 +24,9 @@ module TypeFun.Data.List
22 , IsPrefixOf
24 , IsPrefixOf
23 , IsNotPrefixOf
25 , IsNotPrefixOf
24 , IsPrefixOfBool
26 , IsPrefixOfBool
27+ , Union
28+ , AppendUniq
29+ , Intersect
25 -- * Uniqueness checking
30 -- * Uniqueness checking
26 , ElementIsUniq
31 , ElementIsUniq
27 , UniqElements
32 , UniqElements
@@ -85,11 +90,19 @@ type family IndexOf' (acc :: N) (a :: k) (s :: [k]) :: Maybe N where
85 IndexOf' acc a (a ': as) = 'Just acc
90 IndexOf' acc a (a ': as) = 'Just acc
86 IndexOf' acc a (b ': as) = IndexOf' (S acc) a as
91 IndexOf' acc a (b ': as) = IndexOf' (S acc) a as
87
92
93+type family IndicesOf (a :: [k]) (b :: [k]) :: [Maybe N] where
94+ IndicesOf '[] bs = '[]
95+ IndicesOf (a ': as) bs = (IndexOf a bs) ': (IndicesOf as bs)
96+
88type family Index (idx :: N) (s :: [k]) :: Maybe k where
97type family Index (idx :: N) (s :: [k]) :: Maybe k where
89 Index idx '[] = 'Nothing
98 Index idx '[] = 'Nothing
90 Index Z (a ': as) = 'Just a
99 Index Z (a ': as) = 'Just a
91 Index (S idx) (a ': as) = Index idx as
100 Index (S idx) (a ': as) = Index idx as
92
101
102+type family Indices (idxs :: [N]) (a :: [k]) :: [Maybe k] where
103+ Indices '[] as = '[]
104+ Indices (i ': idxs) as = (Index i as) ': (Indices idxs as)
105+
93
106
94-- | Generates unresolvable constraint if fists element is not
107-- | Generates unresolvable constraint if fists element is not
95-- contained inside of second
108-- contained inside of second
@@ -131,12 +144,27 @@ type family IsPrefixOfBool (a :: [k]) (b :: [k]) :: Bool where
131 IsPrefixOfBool (a ': as) (a ': bs) = IsPrefixOfBool as bs
144 IsPrefixOfBool (a ': as) (a ': bs) = IsPrefixOfBool as bs
132 IsPrefixOfBool as bs = 'False
145 IsPrefixOfBool as bs = 'False
133
146
147+-- | Appends elements from first list to second if they are not
148+-- presented in.
149+type family Union (a :: [k]) (b :: [k]) :: [k] where
150+ Union '[] bs = bs
151+ Union (a ': as) bs = Union as (AppendUniq a bs)
152+
153+-- | Append element to list if element is not already presented in
154+type family AppendUniq (a :: k) (s :: [k]) :: [k] where
155+ AppendUniq a (a ': bs) = a ': bs
156+ AppendUniq a (b ': bs) = b ': (AppendUniq a bs)
157+ AppendUniq a '[] = '[a]
158+
159+-- | Calculates intersection between two lists. Order of elements is
160+-- taken from first list
161+type Intersect a b = (CatMaybes (Indices (CatMaybes (IndicesOf a b)) b))
162+
134-- | Checks that element 'a' occurs in a list just once
163-- | Checks that element 'a' occurs in a list just once
135type ElementIsUniq a s = If (Equal (S Z) (Count a s))
164type ElementIsUniq a s = If (Equal (S Z) (Count a s))
136 (() :: Constraint)
165 (() :: Constraint)
137 (ElementIsNotUniqInList a s)
166 (ElementIsNotUniqInList a s)
138
167
139−
140-- | Checks that all elements in list are unique
168-- | Checks that all elements in list are unique
141type UniqElements a = UniqElements' a a
169type UniqElements a = UniqElements' a a
142
170
src/TypeFun/Data/Maybe.hs+5
@@ -16,3 +16,8 @@ type family NothingToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where
16type family JustToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where
16type family JustToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where
17 JustToConstr 'Nothing c = ()
17 JustToConstr 'Nothing c = ()
18 JustToConstr ('Just a) c = c
18 JustToConstr ('Just a) c = c
19+
20+type family CatMaybes (l :: [Maybe k]) :: [k] where
21+ CatMaybes '[] = '[]
22+ CatMaybes (('Just a) ': as) = a ': (CatMaybes as)
23+ CatMaybes ('Nothing ': as) = CatMaybes as