@@ -11,9 +11,13 @@ module TypeFun.Data.List
1111 , Delete
1212 -- * Elements lookup
1313 , IndexOf
14− , IndexOf'
14+ , IndexOfMay
15+ , IndexOfMay'
16+ , IndicesOfMay
1517 , IndicesOf
1618 , Index
19+ , IndexMay
20+ , IndicesMay
1721 , Indices
1822 , Elem
1923 , NotElem
@@ -26,6 +30,7 @@ module TypeFun.Data.List
2630 , IsPrefixOfBool
2731 -- * Set operations
2832 , Union
33+ , UnionList
2934 , AppendUniq
3035 , Intersect
3136 -- * Uniqueness checking
@@ -59,6 +64,8 @@ class ListIsPrefixOf a b
5964
6065class ElementIsNotUniqInList a s
6166
67+class IndexNotFoundInList a s
68+
6269----------------------
6370-- main module code --
6471----------------------
@@ -84,33 +91,45 @@ type family Delete (a :: k) (s :: [k]) :: [k] where
8491 Delete a (a ': as) = Delete a as
8592 Delete a (b ': as) = b ': (Delete a as)
8693
87−type IndexOf a s = IndexOf' Z a s
94+type IndexOf a s = FromJust (IndexOfMay a s)
95+
96+type IndexOfMay a s = IndexOfMay' Z a s
97+
98+type family IndexOfMay' (acc :: N) (a :: k) (s :: [k]) :: Maybe N where
99+ IndexOfMay' acc a '[] = 'Nothing
100+ IndexOfMay' acc a (a ': as) = 'Just acc
101+ IndexOfMay' acc a (b ': as) = IndexOfMay' (S acc) a as
88102
89−type family IndexOf' (acc :: N) (a :: k) (s :: [k]) :: Maybe N where
90− IndexOf' acc a '[] = 'Nothing
91− IndexOf' acc a (a ': as) = 'Just acc
92− IndexOf' acc a (b ': as) = IndexOf' (S acc) a as
103+type family IndicesOfMay (a :: [k]) (b :: [k]) :: [Maybe N] where
104+ IndicesOfMay '[] bs = '[]
105+ IndicesOfMay (a ': as) bs = (IndexOfMay a bs) ': (IndicesOfMay as bs)
93106
94−type family IndicesOf (a :: [k]) (b :: [k]) :: [Maybe N] where
107+type family IndicesOf (a :: [k]) (b :: [k]) :: [N] where
95108 IndicesOf '[] bs = '[]
96109 IndicesOf (a ': as) bs = (IndexOf a bs) ': (IndicesOf as bs)
97110
98−type family Index (idx :: N) (s :: [k]) :: Maybe k where
99− Index idx '[] = 'Nothing
100− Index Z (a ': as) = 'Just a
101− Index (S idx) (a ': as) = Index idx as
111+type Index idx s = FromJust (IndexMay idx s)
102112
103−type family Indices (idxs :: [N]) (a :: [k]) :: [Maybe k] where
104− Indices '[] as = '[]
113+type family IndexMay (idx :: N) (s :: [k]) :: Maybe k where
114+ IndexMay idx '[] = 'Nothing
115+ IndexMay Z (a ': as) = 'Just a
116+ IndexMay (S idx) (a ': as) = IndexMay idx as
117+
118+type family IndicesMay (idxs :: [N]) (a :: [k]) :: [Maybe k] where
119+ IndicesMay '[] as = '[]
120+ IndicesMay (i ': idxs) as = (IndexMay i as) ': (IndicesMay idxs as)
121+
122+type family Indices (idxs :: [N]) (a :: [k]) :: [k] where
123+ Indices '[] as = '[]
105124 Indices (i ': idxs) as = (Index i as) ': (Indices idxs as)
106125
107126-- | Generates unresolvable constraint if fists element is not
108127-- contained inside of second
109−type Elem a s = NothingToConstr (IndexOf a s)
128+type Elem a s = NothingToConstr (IndexOfMay a s)
110129 (ElementNotFoundInList a s)
111130
112131-- | Reverse of 'Elem'
113−type NotElem a s = JustToConstr (IndexOf a s)
132+type NotElem a s = JustToConstr (IndexOfMay a s)
114133 (ElementIsInList a s)
115134
116135-- | Count elements in a list
@@ -150,6 +169,10 @@ type family Union (a :: [k]) (b :: [k]) :: [k] where
150169 Union '[] bs = bs
151170 Union (a ': as) bs = Union as (AppendUniq a bs)
152171
172+type family UnionList (l :: [[k]]) :: [k] where
173+ UnionList '[] = '[]
174+ UnionList (a ': as) = Union a (UnionList as)
175+
153176-- | Append element to list if element is not already presented in
154177type family AppendUniq (a :: k) (s :: [k]) :: [k] where
155178 AppendUniq a (a ': bs) = a ': bs
@@ -158,7 +181,7 @@ type family AppendUniq (a :: k) (s :: [k]) :: [k] where
158181
159182-- | Calculates intersection between two lists. Order of elements is
160183-- taken from first list
161−type Intersect a b = (CatMaybes (Indices (CatMaybes (IndicesOf a b)) b))
184+type Intersect a b = (Indices (CatMaybes (IndicesOfMay a b)) b)
162185
163186-- | Checks that element 'a' occurs in a list just once
164187type ElementIsUniq a s = If (Equal (S Z) (Count a s))