git.iko.soy/type-fun
on master help sign in
Add 'Index' versions without Maybe output
4819b04Aleksey Uimanov
example/Main.hs+4−3
compare with master
unifiedsplit
@@ -18,9 +18,10 @@ sublistConstr p = elemConstr p + 1
18prefixConstr :: (IsPrefixOf '[Int, Bool] l) => proxy l -> Int
18prefixConstr :: (IsPrefixOf '[Int, Bool] l) => proxy l -> Int
19prefixConstr p = sublistConstr p + 1
19prefixConstr p = sublistConstr p + 1
20
20
21−-- | This function has narrower constraint __Int is inside of l and it
21+-- | This function has narrower constraint
22+-- __Int is inside of l and it is a first argument__
22−-- is a first argument__ and uses inside more wide function
23+-- and uses inside more wide function
23−indexConstr :: (('Just 'Z) ~ (IndexOf Int l)) => proxy l -> Int
24+indexConstr :: (('Just 'Z) ~ (IndexOfMay Int l)) => proxy l -> Int
24indexConstr p = elemConstr p + 1
25indexConstr p = elemConstr p + 1
25
26
26uniqConstr :: (UniqElements l) => proxy l -> Int
27uniqConstr :: (UniqElements l) => proxy l -> Int
src/TypeFun/Data/List.hs+39−16
@@ -11,9 +11,13 @@ module TypeFun.Data.List
11 , Delete
11 , Delete
12 -- * Elements lookup
12 -- * Elements lookup
13 , IndexOf
13 , IndexOf
14− , IndexOf'
14+ , IndexOfMay
15+ , IndexOfMay'
16+ , IndicesOfMay
15 , IndicesOf
17 , IndicesOf
16 , Index
18 , Index
19+ , IndexMay
20+ , IndicesMay
17 , Indices
21 , Indices
18 , Elem
22 , Elem
19 , NotElem
23 , NotElem
@@ -26,6 +30,7 @@ module TypeFun.Data.List
26 , IsPrefixOfBool
30 , IsPrefixOfBool
27 -- * Set operations
31 -- * Set operations
28 , Union
32 , Union
33+ , UnionList
29 , AppendUniq
34 , AppendUniq
30 , Intersect
35 , Intersect
31 -- * Uniqueness checking
36 -- * Uniqueness checking
@@ -59,6 +64,8 @@ class ListIsPrefixOf a b
59
64
60class ElementIsNotUniqInList a s
65class ElementIsNotUniqInList a s
61
66
67+class IndexNotFoundInList a s
68+
62----------------------
69----------------------
63-- main module code --
70-- main module code --
64----------------------
71----------------------
@@ -84,33 +91,45 @@ type family Delete (a :: k) (s :: [k]) :: [k] where
84 Delete a (a ': as) = Delete a as
91 Delete a (a ': as) = Delete a as
85 Delete a (b ': as) = b ': (Delete a as)
92 Delete a (b ': as) = b ': (Delete a as)
86
93
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
88
102
89−type family IndexOf' (acc :: N) (a :: k) (s :: [k]) :: Maybe N where
103+type family IndicesOfMay (a :: [k]) (b :: [k]) :: [Maybe N] where
90− IndexOf' acc a '[] = 'Nothing
104+ IndicesOfMay '[] bs = '[]
91− IndexOf' acc a (a ': as) = 'Just acc
105+ IndicesOfMay (a ': as) bs = (IndexOfMay a bs) ': (IndicesOfMay as bs)
92− IndexOf' acc a (b ': as) = IndexOf' (S acc) a as
93
106
94−type family IndicesOf (a :: [k]) (b :: [k]) :: [Maybe N] where
107+type family IndicesOf (a :: [k]) (b :: [k]) :: [N] where
95 IndicesOf '[] bs = '[]
108 IndicesOf '[] bs = '[]
96 IndicesOf (a ': as) bs = (IndexOf a bs) ': (IndicesOf as bs)
109 IndicesOf (a ': as) bs = (IndexOf a bs) ': (IndicesOf as bs)
97
110
98−type family Index (idx :: N) (s :: [k]) :: Maybe k where
111+type Index idx s = FromJust (IndexMay idx s)
99− Index idx '[] = 'Nothing
100− Index Z (a ': as) = 'Just a
101− Index (S idx) (a ': as) = Index idx as
102
112
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+
103−type family Indices (idxs :: [N]) (a :: [k]) :: [Maybe k] where
118+type family IndicesMay (idxs :: [N]) (a :: [k]) :: [Maybe k] where
104− Indices '[] as = '[]
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 = '[]
105 Indices (i ': idxs) as = (Index i as) ': (Indices idxs as)
124 Indices (i ': idxs) as = (Index i as) ': (Indices idxs as)
106
125
107-- | Generates unresolvable constraint if fists element is not
126-- | Generates unresolvable constraint if fists element is not
108-- contained inside of second
127-- contained inside of second
109−type Elem a s = NothingToConstr (IndexOf a s)
128+type Elem a s = NothingToConstr (IndexOfMay a s)
110 (ElementNotFoundInList a s)
129 (ElementNotFoundInList a s)
111
130
112-- | Reverse of 'Elem'
131-- | Reverse of 'Elem'
113−type NotElem a s = JustToConstr (IndexOf a s)
132+type NotElem a s = JustToConstr (IndexOfMay a s)
114 (ElementIsInList a s)
133 (ElementIsInList a s)
115
134
116-- | Count elements in a list
135-- | Count elements in a list
@@ -150,6 +169,10 @@ type family Union (a :: [k]) (b :: [k]) :: [k] where
150 Union '[] bs = bs
169 Union '[] bs = bs
151 Union (a ': as) bs = Union as (AppendUniq a bs)
170 Union (a ': as) bs = Union as (AppendUniq a bs)
152
171
172+type family UnionList (l :: [[k]]) :: [k] where
173+ UnionList '[] = '[]
174+ UnionList (a ': as) = Union a (UnionList as)
175+
153-- | Append element to list if element is not already presented in
176-- | Append element to list if element is not already presented in
154type family AppendUniq (a :: k) (s :: [k]) :: [k] where
177type family AppendUniq (a :: k) (s :: [k]) :: [k] where
155 AppendUniq a (a ': bs) = a ': bs
178 AppendUniq a (a ': bs) = a ': bs
@@ -158,7 +181,7 @@ type family AppendUniq (a :: k) (s :: [k]) :: [k] where
158
181
159-- | Calculates intersection between two lists. Order of elements is
182-- | Calculates intersection between two lists. Order of elements is
160-- taken from first list
183-- 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)
162
185
163-- | Checks that element 'a' occurs in a list just once
186-- | Checks that element 'a' occurs in a list just once
164type ElementIsUniq a s = If (Equal (S Z) (Count a s))
187type ElementIsUniq a s = If (Equal (S Z) (Count a s))
src/TypeFun/Data/Maybe.hs+3
@@ -21,3 +21,6 @@ type family CatMaybes (l :: [Maybe k]) :: [k] where
21 CatMaybes '[] = '[]
21 CatMaybes '[] = '[]
22 CatMaybes (('Just a) ': as) = a ': (CatMaybes as)
22 CatMaybes (('Just a) ': as) = a ': (CatMaybes as)
23 CatMaybes ('Nothing ': as) = CatMaybes as
23 CatMaybes ('Nothing ': as) = CatMaybes as
24+
25+type family FromJust (a :: Maybe k) :: k where
26+ FromJust ('Just a) = a