git.iko.soy/Idris-dev
on master help sign in
Ported the majority of the list API to the vector data type.
02ef050Dominic Mulligan
lib/prelude/vect.idr+164−26
compare with master
unifiedsplit
@@ -18,19 +18,15 @@ data Vect : Set -> Nat -> Set where
18
18
19tail : Vect a (S n) -> Vect a n
19tail : Vect a (S n) -> Vect a n
20tail (x::xs) = xs
20tail (x::xs) = xs
21−tail [] impossible
22
21
23head : Vect a (S n) -> a
22head : Vect a (S n) -> a
24head (x::xs) = x
23head (x::xs) = x
25−head [] impossible
26
24
27last : Vect a (S n) -> a
25last : Vect a (S n) -> a
28−last [] impossible
29last (x::[]) = x
26last (x::[]) = x
30last (x::y::ys) = last $ y::ys
27last (x::y::ys) = last $ y::ys
31
28
32init : Vect a (S n) -> Vect a n
29init : Vect a (S n) -> Vect a n
33−init [] impossible
34init (x::[]) = []
30init (x::[]) = []
35init (x::y::ys) = x :: init (y::ys)
31init (x::y::ys) = x :: init (y::ys)
36
32
@@ -44,11 +40,11 @@ index (fS _) [] impossible
44-- Conversions to and from list
40-- Conversions to and from list
45--------------------------------------------------------------------------------
41--------------------------------------------------------------------------------
46
42
47−toList : Vect a n -> List a
43+total toList : Vect a n -> List a
48toList [] = []
44toList [] = []
49toList (x::xs) = x :: toList xs
45toList (x::xs) = x :: toList xs
50
46
51−fromList : (l : List a) -> Vect a (length l)
47+total fromList : (l : List a) -> Vect a (length l)
52fromList [] = []
48fromList [] = []
53fromList (x::xs) = x :: fromList xs
49fromList (x::xs) = x :: fromList xs
54
50
@@ -61,36 +57,61 @@ fromList (x::xs) = x :: fromList xs
61(++) (x::xs) ys = x :: xs ++ ys
57(++) (x::xs) ys = x :: xs ++ ys
62
58
63--------------------------------------------------------------------------------
59--------------------------------------------------------------------------------
64−-- Transformations
60+-- Maps
65--------------------------------------------------------------------------------
61--------------------------------------------------------------------------------
66
62
67−reverse : Vect a n -> Vect a n
68−reverse = reverse' []
69− where
70− reverse' : Vect a m -> Vect a n -> Vect a (m + n)
63+total map : (a -> b) -> Vect a n -> Vect b n
71− reverse' acc [] ?= acc
64+map f [] = []
72− reverse' acc (x::xs) ?= reverse' (x::acc) xs
65+map f (x::xs) = f x :: map f xs
73
66
74--------------------------------------------------------------------------------
67--------------------------------------------------------------------------------
75−-- Maps
68+-- Folds
76--------------------------------------------------------------------------------
69--------------------------------------------------------------------------------
77
70
78−map : (a -> b) -> Vect a n -> Vect b n
71+total foldl : (a -> b -> a) -> a -> Vect b m -> a
79−map f [] = []
72+foldl f e [] = e
80−map f (x::xs) = f x :: map f xs
73+foldl f e (x::xs) = foldl f (f e x) xs
74+
75+total foldr : (a -> b -> b) -> b -> Vect a m -> b
76+foldr f e [] = e
77+foldr f e (x::xs) = f x (foldr f e xs)
81
78
82--------------------------------------------------------------------------------
79--------------------------------------------------------------------------------
83−-- Filters
80+-- Special folds
84--------------------------------------------------------------------------------
81--------------------------------------------------------------------------------
85
82
83+total and : Vect Bool m -> Bool
84+and = foldr (&&) True
85+
86+total or : Vect Bool m -> Bool
87+or = foldr (||) False
88+
89+total any : (a -> Bool) -> Vect a m -> Bool
90+any p = or . map p
91+
86−filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)
92+total all : (a -> Bool) -> Vect a m -> Bool
87−filter p [] = ( _ ** [] )
93+all p = and . map p
88−filter p (x::xs) with (filter p xs)
94+
95+--------------------------------------------------------------------------------
96+-- Transformations
97+--------------------------------------------------------------------------------
98+
99+total reverse : Vect a n -> Vect a n
100+reverse = reverse' []
101+ where
102+ total reverse' : Vect a m -> Vect a n -> Vect a (m + n)
103+ reverse' acc [] ?= acc
104+ reverse' acc (x::xs) ?= reverse' (x::acc) xs
105+
106+total intersperse' : a -> Vect a m -> (p ** Vect a p)
107+intersperse' sep [] = (_ ** [])
108+intersperse' sep (y::ys) with (intersperse' sep ys)
89− | (_ ** tail) =
109+ | (_ ** tail) = (_ ** sep::y::tail)
90− if p x then
110+
91− (_ ** x::tail)
111+total intersperse : a -> Vect a m -> (p ** Vect a p)
92− else
112+intersperse sep [] = (_ ** [])
113+intersperse sep (x::xs) with (intersperse' sep xs)
93− (_ ** tail)
114+ | (_ ** tail) = (_ ** x::tail)
94
115
95--------------------------------------------------------------------------------
116--------------------------------------------------------------------------------
96-- Membership tests
117-- Membership tests
@@ -123,6 +144,123 @@ hasAnyBy p elems (x::xs) with (elemBy p x elems)
123hasAny : Eq a => Vect a m -> Vect a n -> Bool
144hasAny : Eq a => Vect a m -> Vect a n -> Bool
124hasAny = hasAnyBy (==)
145hasAny = hasAnyBy (==)
125
146
147+--------------------------------------------------------------------------------
148+-- Searching with a predicate
149+--------------------------------------------------------------------------------
150+
151+find : (a -> Bool) -> Vect a n -> Maybe a
152+find p [] = Nothing
153+find p (x::xs) with (p x)
154+ | True = Just x
155+ | False = find p xs
156+
157+findIndex : (a -> Bool) -> Vect a n -> Maybe Nat
158+findIndex = findIndex' 0
159+ where
160+ findIndex' : Nat -> (a -> Bool) -> Vect a n -> Maybe Nat
161+ findIndex' cnt p [] = Nothing
162+ findIndex' cnt p (x::xs) with (p x)
163+ | True = Just cnt
164+ | False = findIndex' (S cnt) p xs
165+
166+total findIndices : (a -> Bool) -> Vect a m -> (p ** Vect Nat p)
167+findIndices = findIndices' 0
168+ where
169+ total findIndices' : Nat -> (a -> Bool) -> Vect a m -> (p ** Vect Nat p)
170+ findIndices' cnt p [] = (_ ** [])
171+ findIndices' cnt p (x::xs) with (findIndices' (S cnt) p xs)
172+ | (_ ** tail) =
173+ if p x then
174+ (_ ** cnt::tail)
175+ else
176+ (_ ** tail)
177+
178+elemIndexBy : (a -> a -> Bool) -> a -> Vect a m -> Maybe Nat
179+elemIndexBy p e = findIndex $ p e
180+
181+elemIndex : Eq a => a -> Vect a m -> Maybe Nat
182+elemIndex = elemIndexBy (==)
183+
184+total elemIndicesBy : (a -> a -> Bool) -> a -> Vect a m -> (p ** Vect Nat p)
185+elemIndicesBy p e = findIndices $ p e
186+
187+total elemIndices : Eq a => a -> Vect a m -> (p ** Vect Nat p)
188+elemIndices = elemIndicesBy (==)
189+
190+--------------------------------------------------------------------------------
191+-- Filters
192+--------------------------------------------------------------------------------
193+
194+total filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)
195+filter p [] = ( _ ** [] )
196+filter p (x::xs) with (filter p xs)
197+ | (_ ** tail) =
198+ if p x then
199+ (_ ** x::tail)
200+ else
201+ (_ ** tail)
202+
203+nubBy : (a -> a -> Bool) -> Vect a n -> (p ** Vect a p)
204+nubBy = nubBy' []
205+ where
206+ nubBy' : Vect a m -> (a -> a -> Bool) -> Vect a n -> (p ** Vect a p)
207+ nubBy' acc p [] = (_ ** [])
208+ nubBy' acc p (x::xs) with (elemBy p x acc)
209+ | True = nubBy' acc p xs
210+ | False with (nubBy' (x::acc) p xs)
211+ | (_ ** tail) = (_ ** x::tail)
212+
213+nub : Eq a => Vect a n -> (p ** Vect a p)
214+nub = nubBy (==)
215+
216+--------------------------------------------------------------------------------
217+-- Splitting and breaking lists
218+--------------------------------------------------------------------------------
219+
220+-- XXX: todo
221+
222+--------------------------------------------------------------------------------
223+-- Predicates
224+--------------------------------------------------------------------------------
225+
226+isPrefixOfBy : (a -> a -> Bool) -> Vect a m -> Vect a n -> Bool
227+isPrefixOfBy p [] right = True
228+isPrefixOfBy p left [] = False
229+isPrefixOfBy p (x::xs) (y::ys) with (p x y)
230+ | True = isPrefixOfBy p xs ys
231+ | False = False
232+
233+isPrefixOf : Eq a => Vect a m -> Vect a n -> Bool
234+isPrefixOf = isPrefixOfBy (==)
235+
236+isSuffixOfBy : (a -> a -> Bool) -> Vect a m -> Vect a n -> Bool
237+isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
238+
239+isSuffixOf : Eq a => Vect a m -> Vect a n -> Bool
240+isSuffixOf = isSuffixOfBy (==)
241+
242+--------------------------------------------------------------------------------
243+-- Conversions
244+--------------------------------------------------------------------------------
245+
246+total maybeToVect : Maybe a -> (p ** Vect a p)
247+maybeToVect Nothing = (_ ** [])
248+maybeToVect (Just j) = (_ ** [j])
249+
250+total vectToMaybe : Vect a n -> Maybe a
251+vectToMaybe [] = Nothing
252+vectToMaybe (x::xs) = Just x
253+
254+--------------------------------------------------------------------------------
255+-- Misc
256+--------------------------------------------------------------------------------
257+
258+catMaybes : Vect (Maybe a) n -> (p ** Vect a p)
259+catMaybes [] = (_ ** [])
260+catMaybes (Nothing::xs) = catMaybes xs
261+catMaybes ((Just j)::xs) with (catMaybes xs)
262+ | (_ ** tail) = (_ ** j::tail)
263+
126--------------------------------------------------------------------------------
264--------------------------------------------------------------------------------
127-- Proofs
265-- Proofs
128--------------------------------------------------------------------------------
266--------------------------------------------------------------------------------