@@ -9,11 +9,17 @@ module TypeFun.Data.List
99 , Drop
1010 , Take
1111 , Delete
12+ , Remove
13+ , (:++:)
1214 -- * Elements lookup
1315 , IndexOf
14− , IndexOf'
16+ , IndexOfMay
17+ , IndexOfMay'
18+ , IndicesOfMay
1519 , IndicesOf
1620 , Index
21+ , IndexMay
22+ , IndicesMay
1723 , Indices
1824 , Elem
1925 , NotElem
@@ -24,13 +30,19 @@ module TypeFun.Data.List
2430 , IsPrefixOf
2531 , IsNotPrefixOf
2632 , IsPrefixOfBool
33+ -- * Set operations
2734 , Union
35+ , UnionList
2836 , AppendUniq
2937 , Intersect
38+ , Substract
3039 -- * Uniqueness checking
3140 , ElementIsUniq
3241 , UniqElements
3342 , UniqElements'
43+ -- * Unsafe helpers
44+ , appendId
45+ , subListId
3446 ) where
3547
3648import Data.Type.Bool
@@ -39,6 +51,7 @@ import GHC.TypeLits
3951import TypeFun.Data.Eq
4052import TypeFun.Data.Maybe
4153import TypeFun.Data.Peano
54+import Unsafe.Coerce
4255
4356------------------------------------------------------------------------
4457-- NOTE: Errors type classes. These type classes are not in separate --
@@ -58,6 +71,8 @@ class ListIsPrefixOf a b
5871
5972class ElementIsNotUniqInList a s
6073
74+class IndexNotFoundInList a s
75+
6176----------------------
6277-- main module code --
6378----------------------
@@ -83,34 +98,62 @@ type family Delete (a :: k) (s :: [k]) :: [k] where
8398 Delete a (a ': as) = Delete a as
8499 Delete a (b ': as) = b ': (Delete a as)
85100
86−type IndexOf a s = IndexOf' Z a s
101+-- | Remove index from the list
102+type family Remove (i :: N) (a :: [k]) :: [k] where
103+ Remove i '[] = '[]
104+ Remove 'Z (a ': as) = as
105+ Remove ('S i) (a ': as) = a ': (Remove i as)
106+
107+type family (:++:) (a :: [k]) (b :: [k]) :: [k] where
108+ '[] :++: b = b
109+ (a ': as) :++: b = a ': (as :++: b)
110+
111+appendId
112+ :: forall proxy l r
113+ . proxy l
114+ -> (l ~ (l :++: '[]) => r)
115+ -> r
116+appendId = unsafeCoerce id
117+
118+type IndexOf a s = FromJust (IndexOfMay a s)
119+
120+type IndexOfMay a s = IndexOfMay' Z a s
121+
122+type family IndexOfMay' (acc :: N) (a :: k) (s :: [k]) :: Maybe N where
123+ IndexOfMay' acc a '[] = 'Nothing
124+ IndexOfMay' acc a (a ': as) = 'Just acc
125+ IndexOfMay' acc a (b ': as) = IndexOfMay' (S acc) a as
87126
88−type family IndexOf' (acc :: N) (a :: k) (s :: [k]) :: Maybe N where
89− IndexOf' acc a '[] = 'Nothing
90− IndexOf' acc a (a ': as) = 'Just acc
91− IndexOf' acc a (b ': as) = IndexOf' (S acc) a as
127+type family IndicesOfMay (a :: [k]) (b :: [k]) :: [Maybe N] where
128+ IndicesOfMay '[] bs = '[]
129+ IndicesOfMay (a ': as) bs = (IndexOfMay a bs) ': (IndicesOfMay as bs)
92130
93−type family IndicesOf (a :: [k]) (b :: [k]) :: [Maybe N] where
131+type family IndicesOf (a :: [k]) (b :: [k]) :: [N] where
94132 IndicesOf '[] bs = '[]
95133 IndicesOf (a ': as) bs = (IndexOf a bs) ': (IndicesOf as bs)
96134
97−type family Index (idx :: N) (s :: [k]) :: Maybe k where
98− Index idx '[] = 'Nothing
99− Index Z (a ': as) = 'Just a
100− Index (S idx) (a ': as) = Index idx as
135+type Index idx s = FromJust (IndexMay idx s)
101136
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)
137+type family IndexMay (idx :: N) (s :: [k]) :: Maybe k where
138+ IndexMay idx '[] = 'Nothing
139+ IndexMay Z (a ': as) = 'Just a
140+ IndexMay (S idx) (a ': as) = IndexMay idx as
141+
142+type family IndicesMay (idxs :: [N]) (a :: [k]) :: [Maybe k] where
143+ IndicesMay '[] as = '[]
144+ IndicesMay (i ': idxs) as = (IndexMay i as) ': (IndicesMay idxs as)
105145
146+type family Indices (idxs :: [N]) (a :: [k]) :: [k] where
147+ Indices '[] as = '[]
148+ Indices (i ': idxs) as = (Index i as) ': (Indices idxs as)
106149
107150-- | Generates unresolvable constraint if fists element is not
108151-- contained inside of second
109−type Elem a s = NothingToConstr (IndexOf a s)
152+type Elem a s = NothingToConstr (IndexOfMay a s)
110153 (ElementNotFoundInList a s)
111154
112155-- | Reverse of 'Elem'
113−type NotElem a s = JustToConstr (IndexOf a s)
156+type NotElem a s = JustToConstr (IndexOfMay a s)
114157 (ElementIsInList a s)
115158
116159-- | Count elements in a list
@@ -125,6 +168,12 @@ type family SubList (a :: [k]) (b :: [k]) :: Constraint where
125168 SubList '[] bs = ()
126169 SubList (a ': as) bs = (Elem a bs, SubList as bs)
127170
171+subListId
172+ :: forall proxy l r
173+ . proxy l
174+ -> (SubList l l => r) -> r
175+subListId _ = unsafeCoerce id
176+
128177type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where
129178 NotSubList '[] bs = ()
130179 NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)
@@ -150,6 +199,10 @@ type family Union (a :: [k]) (b :: [k]) :: [k] where
150199 Union '[] bs = bs
151200 Union (a ': as) bs = Union as (AppendUniq a bs)
152201
202+type family UnionList (l :: [[k]]) :: [k] where
203+ UnionList '[] = '[]
204+ UnionList (a ': as) = Union a (UnionList as)
205+
153206-- | Append element to list if element is not already presented in
154207type family AppendUniq (a :: k) (s :: [k]) :: [k] where
155208 AppendUniq a (a ': bs) = a ': bs
@@ -158,7 +211,13 @@ type family AppendUniq (a :: k) (s :: [k]) :: [k] where
158211
159212-- | Calculates intersection between two lists. Order of elements is
160213-- taken from first list
161−type Intersect a b = (CatMaybes (Indices (CatMaybes (IndicesOf a b)) b))
214+type Intersect a b = (Indices (CatMaybes (IndicesOfMay a b)) b)
215+
216+-- | Removes from first list all elements occured in second
217+type family Substract (a :: [k]) (b :: [k]) :: [k] where
218+ Substract '[] b = '[]
219+ Substract a '[] = a
220+ Substract a (b ': bs) = Substract (Delete b a) bs
162221
163222-- | Checks that element 'a' occurs in a list just once
164223type ElementIsUniq a s = If (Equal (S Z) (Count a s))