@@ -9,17 +9,11 @@ module TypeFun.Data.List
99 , Drop
1010 , Take
1111 , Delete
12− , Remove
13− , (:++:)
1412 -- * Elements lookup
1513 , IndexOf
16− , IndexOfMay
17− , IndexOfMay'
18− , IndicesOfMay
14+ , IndexOf'
1915 , IndicesOf
2016 , Index
21− , IndexMay
22− , IndicesMay
2317 , Indices
2418 , Elem
2519 , NotElem
@@ -30,19 +24,13 @@ module TypeFun.Data.List
3024 , IsPrefixOf
3125 , IsNotPrefixOf
3226 , IsPrefixOfBool
33− -- * Set operations
3427 , Union
35− , UnionList
3628 , AppendUniq
3729 , Intersect
38− , Substract
3930 -- * Uniqueness checking
4031 , ElementIsUniq
4132 , UniqElements
4233 , UniqElements'
43− -- * Unsafe helpers
44− , appendId
45− , subListId
4634 ) where
4735
4836import Data.Type.Bool
@@ -51,7 +39,6 @@ import GHC.TypeLits
5139import TypeFun.Data.Eq
5240import TypeFun.Data.Maybe
5341import TypeFun.Data.Peano
54−import Unsafe.Coerce
5542
5643------------------------------------------------------------------------
5744-- NOTE: Errors type classes. These type classes are not in separate --
@@ -71,8 +58,6 @@ class ListIsPrefixOf a b
7158
7259class ElementIsNotUniqInList a s
7360
74−class IndexNotFoundInList a s
75−
7661----------------------
7762-- main module code --
7863----------------------
@@ -98,62 +83,34 @@ type family Delete (a :: k) (s :: [k]) :: [k] where
9883 Delete a (a ': as) = Delete a as
9984 Delete a (b ': as) = b ': (Delete a as)
10085
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
86+type IndexOf a s = IndexOf' Z a s
12687
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)
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
13092
131−type family IndicesOf (a :: [k]) (b :: [k]) :: [N] where
93+type family IndicesOf (a :: [k]) (b :: [k]) :: [Maybe N] where
13294 IndicesOf '[] bs = '[]
13395 IndicesOf (a ': as) bs = (IndexOf a bs) ': (IndicesOf as bs)
13496
135−type Index idx s = FromJust (IndexMay idx s)
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
136101
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)
145−
146−type family Indices (idxs :: [N]) (a :: [k]) :: [k] where
147− Indices '[] as = '[]
102+type family Indices (idxs :: [N]) (a :: [k]) :: [Maybe k] where
103+ Indices '[] as = '[]
148104 Indices (i ': idxs) as = (Index i as) ': (Indices idxs as)
149105
106+
150107-- | Generates unresolvable constraint if fists element is not
151108-- contained inside of second
152−type Elem a s = NothingToConstr (IndexOfMay a s)
109+type Elem a s = NothingToConstr (IndexOf a s)
153110 (ElementNotFoundInList a s)
154111
155112-- | Reverse of 'Elem'
156−type NotElem a s = JustToConstr (IndexOfMay a s)
113+type NotElem a s = JustToConstr (IndexOf a s)
157114 (ElementIsInList a s)
158115
159116-- | Count elements in a list
@@ -168,12 +125,6 @@ type family SubList (a :: [k]) (b :: [k]) :: Constraint where
168125 SubList '[] bs = ()
169126 SubList (a ': as) bs = (Elem a bs, SubList as bs)
170127
171−subListId
172− :: forall proxy l r
173− . proxy l
174− -> (SubList l l => r) -> r
175−subListId _ = unsafeCoerce id
176−
177128type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where
178129 NotSubList '[] bs = ()
179130 NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)
@@ -199,10 +150,6 @@ type family Union (a :: [k]) (b :: [k]) :: [k] where
199150 Union '[] bs = bs
200151 Union (a ': as) bs = Union as (AppendUniq a bs)
201152
202−type family UnionList (l :: [[k]]) :: [k] where
203− UnionList '[] = '[]
204− UnionList (a ': as) = Union a (UnionList as)
205−
206153-- | Append element to list if element is not already presented in
207154type family AppendUniq (a :: k) (s :: [k]) :: [k] where
208155 AppendUniq a (a ': bs) = a ': bs
@@ -211,13 +158,7 @@ type family AppendUniq (a :: k) (s :: [k]) :: [k] where
211158
212159-- | Calculates intersection between two lists. Order of elements is
213160-- taken from first list
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
161+type Intersect a b = (CatMaybes (Indices (CatMaybes (IndicesOf a b)) b))
221162
222163-- | Checks that element 'a' occurs in a list just once
223164type ElementIsUniq a s = If (Equal (S Z) (Count a s))