git.iko.soy/Idris-dev
on master help sign in
Added examples to the Vect doc
cc30a89klangner
libs/base/Data/Vect.idr+264
compare with master
unifiedsplit
@@ -45,36 +45,64 @@ lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl
45--------------------------------------------------------------------------------
45--------------------------------------------------------------------------------
46
46
47||| All but the first element of the vector
47||| All but the first element of the vector
48+|||
49+||| ```idris example
50+||| tail [1,2,3,4]
51+||| ```
48tail : Vect (S len) elem -> Vect len elem
52tail : Vect (S len) elem -> Vect len elem
49tail (x::xs) = xs
53tail (x::xs) = xs
50
54
51||| Only the first element of the vector
55||| Only the first element of the vector
56+|||
57+||| ```idris example
58+||| head [1,2,3,4]
59+||| ```
52head : Vect (S len) elem -> elem
60head : Vect (S len) elem -> elem
53head (x::xs) = x
61head (x::xs) = x
54
62
55||| The last element of the vector
63||| The last element of the vector
64+|||
65+||| ```idris example
66+||| last [1,2,3,4]
67+||| ```
56last : Vect (S len) elem -> elem
68last : Vect (S len) elem -> elem
57last (x::[]) = x
69last (x::[]) = x
58last (x::y::ys) = last $ y::ys
70last (x::y::ys) = last $ y::ys
59
71
60||| All but the last element of the vector
72||| All but the last element of the vector
73+|||
74+||| ```idris example
75+||| init [1,2,3,4]
76+||| ```
61init : Vect (S len) elem -> Vect len elem
77init : Vect (S len) elem -> Vect len elem
62init (x::[]) = []
78init (x::[]) = []
63init (x::y::ys) = x :: init (y::ys)
79init (x::y::ys) = x :: init (y::ys)
64
80
65||| Extract a particular element from a vector
81||| Extract a particular element from a vector
82+|||
83+||| ```idris example
84+||| index 1 [1,2,3,4]
85+||| ```
66index : Fin len -> Vect len elem -> elem
86index : Fin len -> Vect len elem -> elem
67index FZ (x::xs) = x
87index FZ (x::xs) = x
68index (FS k) (x::xs) = index k xs
88index (FS k) (x::xs) = index k xs
69
89
70
90
71||| Insert an element at a particular index
91||| Insert an element at a particular index
92+|||
93+||| ```idris example
94+||| insertAt 1 8 [1,2,3,4]
95+||| ```
72insertAt : Fin (S len) -> elem -> Vect len elem -> Vect (S len) elem
96insertAt : Fin (S len) -> elem -> Vect len elem -> Vect (S len) elem
73insertAt FZ y xs = y :: xs
97insertAt FZ y xs = y :: xs
74insertAt (FS k) y (x::xs) = x :: insertAt k y xs
98insertAt (FS k) y (x::xs) = x :: insertAt k y xs
75insertAt (FS k) y [] = absurd k
99insertAt (FS k) y [] = absurd k
76
100
77||| Construct a new vector consisting of all but the indicated element
101||| Construct a new vector consisting of all but the indicated element
102+|||
103+||| ```idris example
104+||| deleteAt 1 [1,2,3,4]
105+||| ```
78deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem
106deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem
79deleteAt FZ (x::xs) = xs
107deleteAt FZ (x::xs) = xs
80deleteAt {len = S m} (FS k) (x::xs) = x :: deleteAt k xs
108deleteAt {len = S m} (FS k) (x::xs) = x :: deleteAt k xs
@@ -82,6 +110,10 @@ deleteAt {len = Z} (FS k) (x::xs) = absurd k
82deleteAt _ [] impossible
110deleteAt _ [] impossible
83
111
84||| Replace an element at a particlar index with another
112||| Replace an element at a particlar index with another
113+|||
114+||| ```idris example
115+||| replaceAt 1 8 [1,2,3,4]
116+||| ```
85replaceAt : Fin len -> elem -> Vect len elem -> Vect len elem
117replaceAt : Fin len -> elem -> Vect len elem -> Vect len elem
86replaceAt FZ y (x::xs) = y :: xs
118replaceAt FZ y (x::xs) = y :: xs
87replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
119replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
@@ -90,6 +122,10 @@ replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
90||| @ i the index to replace at
122||| @ i the index to replace at
91||| @ f the update function
123||| @ f the update function
92||| @ xs the vector to replace in
124||| @ xs the vector to replace in
125+|||
126+||| ```idris example
127+||| updateAt 1 (+10) [1,2,3,4]
128+||| ```
93updateAt : (i : Fin len) -> (f : elem -> elem) -> (xs : Vect len elem) -> Vect len elem
129updateAt : (i : Fin len) -> (f : elem -> elem) -> (xs : Vect len elem) -> Vect len elem
94updateAt FZ f (x::xs) = f x :: xs
130updateAt FZ f (x::xs) = f x :: xs
95updateAt (FS k) f (x::xs) = x :: updateAt k f xs
131updateAt (FS k) f (x::xs) = x :: updateAt k f xs
@@ -100,18 +136,30 @@ updateAt (FS k) f (x::xs) = x :: updateAt k f xs
100
136
101||| Get the first n elements of a Vect
137||| Get the first n elements of a Vect
102||| @ n the number of elements to take
138||| @ n the number of elements to take
139+|||
140+||| ```idris example
141+||| take 2 [1,2,3,4]
142+||| ```
103take : (n : Nat) -> Vect (n + m) elem -> Vect n elem
143take : (n : Nat) -> Vect (n + m) elem -> Vect n elem
104take Z xs = []
144take Z xs = []
105take (S k) (x :: xs) = x :: take k xs
145take (S k) (x :: xs) = x :: take k xs
106
146
107||| Remove the first n elements of a Vect
147||| Remove the first n elements of a Vect
108||| @ n the number of elements to remove
148||| @ n the number of elements to remove
149+|||
150+||| ```idris example
151+||| drop 2 [1,2,3,4]
152+||| ```
109drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
153drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
110drop Z xs = xs
154drop Z xs = xs
111drop (S k) (x :: xs) = drop k xs
155drop (S k) (x :: xs) = drop k xs
112
156
113||| Take up to the first n elements of a Vect if they exist.
157||| Take up to the first n elements of a Vect if they exist.
114||| @ n the maximum number of elements to take
158||| @ n the maximum number of elements to take
159+|||
160+||| ```idris example
161+||| takeUpto 10 [1,2,3,4]
162+||| ```
115takeUpto : (x : Nat) -> Vect n elem -> Vect (minimum x n) elem
163takeUpto : (x : Nat) -> Vect n elem -> Vect (minimum x n) elem
116takeUpto Z ys = []
164takeUpto Z ys = []
117takeUpto x [] = rewrite minimumZeroZeroLeft x in []
165takeUpto x [] = rewrite minimumZeroZeroLeft x in []
@@ -119,6 +167,10 @@ takeUpto (S x) (y::ys) = y :: takeUpto x ys
119
167
120||| Drop up to the first n elements of a Vect if they exist.
168||| Drop up to the first n elements of a Vect if they exist.
121||| @ n the maximum number of elements to remove.
169||| @ n the maximum number of elements to remove.
170+|||
171+||| ```idris example
172+||| dropUpto 10 [1,2,3,4]
173+||| ```
122dropUpto : (x : Nat) -> Vect n elem -> Vect (n `minus` minimum x n) elem
174dropUpto : (x : Nat) -> Vect n elem -> Vect (n `minus` minimum x n) elem
123dropUpto Z ys {n} = rewrite minusZeroRight n in ys
175dropUpto Z ys {n} = rewrite minusZeroRight n in ys
124dropUpto x [] = []
176dropUpto x [] = []
@@ -128,6 +180,10 @@ dropUpto (S x) (y :: ys) = dropUpto x ys
128||| Boolean predicate.
180||| Boolean predicate.
129|||
181|||
130||| @ p the predicate
182||| @ p the predicate
183+|||
184+||| ```idris example
185+||| takeWhile (<3) [1,2,3,4]
186+||| ```
131takeWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
187takeWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
132takeWhile p [] = (_ ** [])
188takeWhile p [] = (_ ** [])
133takeWhile p (x::xs) =
189takeWhile p (x::xs) =
@@ -141,6 +197,10 @@ takeWhile p (x::xs) =
141||| Boolean predicate.
197||| Boolean predicate.
142|||
198|||
143||| @ p the predicate
199||| @ p the predicate
200+|||
201+||| ```idris example
202+||| dropWhile (<3) [1,2,3,4]
203+||| ```
144dropWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
204dropWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
145dropWhile p [] = (_ ** [])
205dropWhile p [] = (_ ** [])
146dropWhile p (x::xs) =
206dropWhile p (x::xs) =
@@ -154,6 +214,10 @@ dropWhile p (x::xs) =
154--------------------------------------------------------------------------------
214--------------------------------------------------------------------------------
155
215
156||| Reverse the order of the elements of a vector
216||| Reverse the order of the elements of a vector
217+|||
218+||| ```idris example
219+||| reverse [1,2,3,4]
220+||| ```
157reverse : Vect len elem -> Vect len elem
221reverse : Vect len elem -> Vect len elem
158reverse xs = go [] xs
222reverse xs = go [] xs
159 where go : Vect n elem -> Vect m elem -> Vect (n+m) elem
223 where go : Vect n elem -> Vect m elem -> Vect (n+m) elem
@@ -164,6 +228,10 @@ reverse xs = go [] xs
164||| Alternate an element between the other elements of a vector
228||| Alternate an element between the other elements of a vector
165||| @ sep the element to intersperse
229||| @ sep the element to intersperse
166||| @ xs the vector to separate with `sep`
230||| @ xs the vector to separate with `sep`
231+|||
232+||| ```idris example
233+||| intersperse 0 [1,2,3,4]
234+||| ```
167intersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elem
235intersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elem
168intersperse sep [] = []
236intersperse sep [] = []
169intersperse sep (x::xs) = x :: intersperse' sep xs
237intersperse sep (x::xs) = x :: intersperse' sep xs
@@ -188,6 +256,10 @@ fromList' {len} ys (x::xs) =
188||| Convert a list to a vector.
256||| Convert a list to a vector.
189|||
257|||
190||| The length of the list should be statically known.
258||| The length of the list should be statically known.
259+|||
260+||| ```idris example
261+||| fromList [1,2,3,4]
262+||| ```
191fromList : (l : List elem) -> Vect (length l) elem
263fromList : (l : List elem) -> Vect (length l) elem
192fromList l =
264fromList l =
193 rewrite (sym $ plusZeroRightNeutral (length l)) in
265 rewrite (sym $ plusZeroRightNeutral (length l)) in
@@ -198,6 +270,10 @@ fromList l =
198--------------------------------------------------------------------------------
270--------------------------------------------------------------------------------
199
271
200||| Append two vectors
272||| Append two vectors
273+|||
274+||| ```idris example
275+||| [1,2,3,4] ++ [5,6]
276+||| ```
201(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem
277(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem
202(++) [] ys = ys
278(++) [] ys = ys
203(++) (x::xs) ys = x :: xs ++ ys
279(++) (x::xs) ys = x :: xs ++ ys
@@ -206,11 +282,19 @@ fromList l =
206|||
282|||
207||| @ len the number of times to repeat it
283||| @ len the number of times to repeat it
208||| @ x the value to repeat
284||| @ x the value to repeat
285+|||
286+||| ```idris example
287+||| replicate 4 1
288+||| ```
209replicate : (len : Nat) -> (x : elem) -> Vect len elem
289replicate : (len : Nat) -> (x : elem) -> Vect len elem
210replicate Z x = []
290replicate Z x = []
211replicate (S k) x = x :: replicate k x
291replicate (S k) x = x :: replicate k x
212
292
213||| Merge two ordered vectors
293||| Merge two ordered vectors
294+|||
295+||| ```idris example
296+||| mergeBy compare (fromList [1,3,5]) (fromList [2,3,4,5,6])
297+||| ```
214mergeBy : (elem -> elem -> Ordering) -> (xs : Vect n elem) -> (ys : Vect m elem) -> Vect (n + m) elem
298mergeBy : (elem -> elem -> Ordering) -> (xs : Vect n elem) -> (ys : Vect m elem) -> Vect (n + m) elem
215mergeBy order [] [] = []
299mergeBy order [] [] = []
216mergeBy order [] (x :: xs) = x :: xs
300mergeBy order [] (x :: xs) = x :: xs
@@ -234,30 +318,54 @@ merge = mergeBy compare
234||| @ f the function to combine elements with
318||| @ f the function to combine elements with
235||| @ xs the first vector of elements
319||| @ xs the first vector of elements
236||| @ ys the second vector of elements
320||| @ ys the second vector of elements
321+|||
322+||| ```idris example
323+||| zipWith (+) (fromList [1,2,3,4]) (fromList [5,6,7,8])
324+||| ```
237zipWith : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n c
325zipWith : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n c
238zipWith f [] [] = []
326zipWith f [] [] = []
239zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
327zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
240
328
241||| Combine three equal-length vectors into a vector with some function
329||| Combine three equal-length vectors into a vector with some function
330+|||
331+||| ```idris example
332+||| zipWith3 (\x,y,z => x+y+z) (fromList [1,2,3,4]) (fromList [5,6,7,8]) (fromList [1,1,1,1])
333+||| ```
242zipWith3 : (a -> b -> c -> d) -> (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n d
334zipWith3 : (a -> b -> c -> d) -> (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n d
243zipWith3 f [] [] [] = []
335zipWith3 f [] [] [] = []
244zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
336zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
245
337
246||| Combine two equal-length vectors pairwise
338||| Combine two equal-length vectors pairwise
339+|||
340+||| ```idris example
341+||| zip (fromList [1,2,3,4]) (fromList [1,2,3,4])
342+||| ```
247zip : (xs : Vect n a) -> (ys : Vect n b) -> Vect n (a, b)
343zip : (xs : Vect n a) -> (ys : Vect n b) -> Vect n (a, b)
248zip = zipWith (\x,y => (x,y))
344zip = zipWith (\x,y => (x,y))
249
345
250||| Combine three equal-length vectors elementwise into a vector of tuples
346||| Combine three equal-length vectors elementwise into a vector of tuples
347+|||
348+||| ```idris example
349+||| zip3 (fromList [1,2,3,4]) (fromList [1,2,3,4]) (fromList [1,2,3,4])
350+||| ```
251zip3 : (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n (a, b, c)
351zip3 : (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n (a, b, c)
252zip3 = zipWith3 (\x,y,z => (x,y,z))
352zip3 = zipWith3 (\x,y,z => (x,y,z))
253
353
254||| Convert a vector of pairs to a pair of vectors
354||| Convert a vector of pairs to a pair of vectors
355+|||
356+||| ```idris example
357+||| unzip (fromList [(1,2), (1,2)])
358+||| ```
255unzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b)
359unzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b)
256unzip [] = ([], [])
360unzip [] = ([], [])
257unzip ((l, r)::xs) with (unzip xs)
361unzip ((l, r)::xs) with (unzip xs)
258 | (lefts, rights) = (l::lefts, r::rights)
362 | (lefts, rights) = (l::lefts, r::rights)
259
363
260||| Convert a vector of three-tuples to a triplet of vectors
364||| Convert a vector of three-tuples to a triplet of vectors
365+|||
366+||| ```idris example
367+||| unzip3 (fromList [(1,2,3), (1,2,3)])
368+||| ```
261unzip3 : (xs : Vect n (a, b, c)) -> (Vect n a, Vect n b, Vect n c)
369unzip3 : (xs : Vect n (a, b, c)) -> (Vect n a, Vect n b, Vect n c)
262unzip3 [] = ([], [], [])
370unzip3 [] = ([], [], [])
263unzip3 ((l,c,r)::xs) with (unzip3 xs)
371unzip3 ((l,c,r)::xs) with (unzip3 xs)
@@ -299,6 +407,10 @@ implementation Functor (Vect n) where
299|||
407|||
300||| @ f the partial function (expressed by returning `Maybe`)
408||| @ f the partial function (expressed by returning `Maybe`)
301||| @ xs the vector to check for results
409||| @ xs the vector to check for results
410+|||
411+||| ```idris example
412+||| mapMaybe ((find (=='a')) . unpack) (fromList ["abc","ade","bgh","xyz"])
413+||| ```
302mapMaybe : (f : a -> Maybe b) -> (xs : Vect len a) -> (m : Nat ** Vect m b)
414mapMaybe : (f : a -> Maybe b) -> (xs : Vect len a) -> (m : Nat ** Vect m b)
303mapMaybe f [] = (_ ** [])
415mapMaybe f [] = (_ ** [])
304mapMaybe f (x::xs) =
416mapMaybe f (x::xs) =
@@ -323,16 +435,28 @@ implementation Foldable (Vect n) where
323--------------------------------------------------------------------------------
435--------------------------------------------------------------------------------
324
436
325||| Flatten a vector of equal-length vectors
437||| Flatten a vector of equal-length vectors
438+|||
439+||| ```idris example
440+||| concat [[1,2,3], [4,5,6]]
441+||| ```
326concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem
442concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem
327concat [] = []
443concat [] = []
328concat (v::vs) = v ++ concat vs
444concat (v::vs) = v ++ concat vs
329
445
330||| Foldr without seeding the accumulator
446||| Foldr without seeding the accumulator
447+|||
448+||| ```idris example
449+||| foldr1 (-) (fromList [1,2,3])
450+||| ```
331foldr1 : (t -> t -> t) -> Vect (S n) t -> t
451foldr1 : (t -> t -> t) -> Vect (S n) t -> t
332foldr1 f [x] = x
452foldr1 f [x] = x
333foldr1 f (x::y::xs) = f x (foldr1 f (y::xs))
453foldr1 f (x::y::xs) = f x (foldr1 f (y::xs))
334
454
335||| Foldl without seeding the accumulator
455||| Foldl without seeding the accumulator
456+|||
457+||| ```idris example
458+||| foldl1 (-) (fromList [1,2,3])
459+||| ```
336foldl1 : (t -> t -> t) -> Vect (S n) t -> t
460foldl1 : (t -> t -> t) -> Vect (S n) t -> t
337foldl1 f (x::xs) = foldl f x xs
461foldl1 f (x::xs) = foldl f x xs
338
462
@@ -342,6 +466,10 @@ foldl1 f (x::xs) = foldl f x xs
342
466
343||| The scanl function is similar to foldl, but returns all the intermediate
467||| The scanl function is similar to foldl, but returns all the intermediate
344||| accumulator states in the form of a vector.
468||| accumulator states in the form of a vector.
469+|||
470+||| ```idris example
471+||| scanl (-) 0 (fromList [1,2,3])
472+||| ```
345scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res
473scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res
346scanl f q [] = [q]
474scanl f q [] = [q]
347scanl f q (x::xs) = q :: scanl f (f q x) xs
475scanl f q (x::xs) = q :: scanl f (f q x) xs
@@ -350,6 +478,10 @@ scanl f q (x::xs) = q :: scanl f (f q x) xs
350||| starting value.
478||| starting value.
351||| It assumes the first element of the vector to be the starting value and then
479||| It assumes the first element of the vector to be the starting value and then
352||| starts the fold with the element following it.
480||| starts the fold with the element following it.
481+|||
482+||| ```idris example
483+||| scanl1 (-) (fromList [1,2,3])
484+||| ```
353scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem
485scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem
354scanl1 f [] = []
486scanl1 f [] = []
355scanl1 f (x::xs) = scanl f x xs
487scanl1 f (x::xs) = scanl f x xs
@@ -362,6 +494,10 @@ scanl1 f (x::xs) = scanl f x xs
362||| @ p the equality test
494||| @ p the equality test
363||| @ e the item to search for
495||| @ e the item to search for
364||| @ xs the vector to search in
496||| @ xs the vector to search in
497+|||
498+||| ```idris example
499+||| elemBy (==) 2 [1,2,3,4]
500+||| ```
365elemBy : (p : elem -> elem -> Bool) -> (e : elem) -> (xs : Vect len elem) -> Bool
501elemBy : (p : elem -> elem -> Bool) -> (e : elem) -> (xs : Vect len elem) -> Bool
366elemBy p e [] = False
502elemBy p e [] = False
367elemBy p e (x::xs) = p e x || elemBy p e xs
503elemBy p e (x::xs) = p e x || elemBy p e xs
@@ -369,17 +505,29 @@ elemBy p e (x::xs) = p e x || elemBy p e xs
369||| Use the default Boolean equality on elements to search for an item
505||| Use the default Boolean equality on elements to search for an item
370||| @ x what to search for
506||| @ x what to search for
371||| @ xs where to search
507||| @ xs where to search
508+|||
509+||| ```idris example
510+||| elem 3 [1,2,3,4]
511+||| ```
372elem : Eq elem => (x : elem) -> (xs : Vect len elem) -> Bool
512elem : Eq elem => (x : elem) -> (xs : Vect len elem) -> Bool
373elem = elemBy (==)
513elem = elemBy (==)
374
514
375||| Find the association of some key with a user-provided comparison
515||| Find the association of some key with a user-provided comparison
376||| @ p the comparison operator for keys (True if they match)
516||| @ p the comparison operator for keys (True if they match)
377||| @ e the key to look for
517||| @ e the key to look for
518+|||
519+||| ```idris example
520+||| lookupBy (==) 2 [(1, 'a'), (2, 'b'), (3, 'c')]
521+||| ```
378lookupBy : (p : key -> key -> Bool) -> (e : key) -> (xs : Vect n (key, val)) -> Maybe val
522lookupBy : (p : key -> key -> Bool) -> (e : key) -> (xs : Vect n (key, val)) -> Maybe val
379lookupBy p e [] = Nothing
523lookupBy p e [] = Nothing
380lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs
524lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs
381
525
382||| Find the assocation of some key using the default Boolean equality test
526||| Find the assocation of some key using the default Boolean equality test
527+|||
528+||| ```idris example
529+||| lookup 3 [(1, 'a'), (2, 'b'), (3, 'c')]
530+||| ```
383lookup : Eq key => key -> Vect n (key, val) -> Maybe val
531lookup : Eq key => key -> Vect n (key, val) -> Maybe val
384lookup = lookupBy (==)
532lookup = lookupBy (==)
385
533
@@ -387,11 +535,19 @@ lookup = lookupBy (==)
387||| @ p the comparison operator
535||| @ p the comparison operator
388||| @ elems the vector to search
536||| @ elems the vector to search
389||| @ xs what to search for
537||| @ xs what to search for
538+|||
539+||| ```idris example
540+||| hasAnyBy (==) [2,5] [1,2,3,4]
541+||| ```
390hasAnyBy : (p : elem -> elem -> Bool) -> (elems : Vect m elem) -> (xs : Vect len elem) -> Bool
542hasAnyBy : (p : elem -> elem -> Bool) -> (elems : Vect m elem) -> (xs : Vect len elem) -> Bool
391hasAnyBy p elems [] = False
543hasAnyBy p elems [] = False
392hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs
544hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs
393
545
394||| Check if any element of xs is found in elems using the default Boolean equality test
546||| Check if any element of xs is found in elems using the default Boolean equality test
547+|||
548+||| ```idris example
549+||| hasAny [2,5] [1,2,3,4]
550+||| ```
395hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool
551hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool
396hasAny = hasAnyBy (==)
552hasAny = hasAnyBy (==)
397
553
@@ -401,30 +557,62 @@ hasAny = hasAnyBy (==)
401
557
402||| Find the first element of the vector that satisfies some test
558||| Find the first element of the vector that satisfies some test
403||| @ p the test to satisfy
559||| @ p the test to satisfy
560+|||
561+||| ```idris example
562+||| find (== 3) [1,2,3,4]
563+||| ```
404find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem
564find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem
405find p [] = Nothing
565find p [] = Nothing
406find p (x::xs) = if p x then Just x else find p xs
566find p (x::xs) = if p x then Just x else find p xs
407
567
408||| Find the index of the first element of the vector that satisfies some test
568||| Find the index of the first element of the vector that satisfies some test
569+|||
570+||| ```idris example
571+||| findIndex (== 3) [1,2,3,4]
572+||| ```
409findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)
573findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)
410findIndex p [] = Nothing
574findIndex p [] = Nothing
411findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)
575findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)
412
576
413||| Find the indices of all elements that satisfy some test
577||| Find the indices of all elements that satisfy some test
578+|||
579+||| ```idris example
580+||| findIndices (< 3) [1,2,3,4]
581+||| ```
414findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)
582findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)
415findIndices p [] = []
583findIndices p [] = []
416findIndices p (x :: xs) = let is = map FS $ findIndices p xs
584findIndices p (x :: xs) = let is = map FS $ findIndices p xs
417 in if p x then 0 :: is else is
585 in if p x then 0 :: is else is
418
586
587+||| Find the index of the first element of the vector that satisfies some test
588+|||
589+||| ```idris example
590+||| elemIndexBy (==) 3 [1,2,3,4]
591+||| ```
419elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)
592elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)
420elemIndexBy p e = findIndex $ p e
593elemIndexBy p e = findIndex $ p e
421
594
595+||| Find the index of the first element of the vector equal to the given one.
596+|||
597+||| ```idris example
598+||| elemIndex 3 [1,2,3,4]
599+||| ```
422elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)
600elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)
423elemIndex = elemIndexBy (==)
601elemIndex = elemIndexBy (==)
424
602
603+||| Find the indices of all elements that satisfy some test
604+|||
605+||| ```idris example
606+||| elemIndicesBy (<=) 3 [1,2,3,4]
607+||| ```
425elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)
608elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)
426elemIndicesBy p e = findIndices $ p e
609elemIndicesBy p e = findIndices $ p e
427
610
611+||| Find the indices of all elements uquals to the given one
612+|||
613+||| ```idris example
614+||| elemIndices 3 [1,2,3,4,3]
615+||| ```
428elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
616elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
429elemIndices = elemIndicesBy (==)
617elemIndices = elemIndicesBy (==)
430
618
@@ -433,6 +621,10 @@ elemIndices = elemIndicesBy (==)
433--------------------------------------------------------------------------------
621--------------------------------------------------------------------------------
434
622
435||| Find all elements of a vector that satisfy some test
623||| Find all elements of a vector that satisfy some test
624+|||
625+||| ```idris example
626+||| filter (< 3) (fromList [1,2,3,4])
627+||| ```
436filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
628filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
437filter p [] = ( _ ** [] )
629filter p [] = ( _ ** [] )
438filter p (x::xs) =
630filter p (x::xs) =
@@ -443,6 +635,10 @@ filter p (x::xs) =
443 (_ ** tail)
635 (_ ** tail)
444
636
445||| Make the elements of some vector unique by some test
637||| Make the elements of some vector unique by some test
638+|||
639+||| ```idris example
640+||| nubBy (==) (fromList [1,2,2,3,4,4])
641+||| ```
446nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
642nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
447nubBy = nubBy' []
643nubBy = nubBy' []
448 where
644 where
@@ -454,15 +650,29 @@ nubBy = nubBy' []
454 | (_ ** tail) = (_ ** x::tail)
650 | (_ ** tail) = (_ ** x::tail)
455
651
456||| Make the elements of some vector unique by the default Boolean equality
652||| Make the elements of some vector unique by the default Boolean equality
653+|||
654+||| ```idris example
655+||| nub (fromList [1,2,2,3,4,4])
656+||| ```
457nub : Eq elem => Vect len elem -> (p ** Vect p elem)
657nub : Eq elem => Vect len elem -> (p ** Vect p elem)
458nub = nubBy (==)
658nub = nubBy (==)
459
659
660+||| Delete first element from list according to some test
661+|||
662+||| ```idris example
663+||| deleteBy (<) 3 (fromList [1,2,2,3,4,4])
664+||| ```
460deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem)
665deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem)
461deleteBy _ _ [] = (_ ** [])
666deleteBy _ _ [] = (_ ** [])
462deleteBy eq x (y::ys) =
667deleteBy eq x (y::ys) =
463 let (len ** zs) = deleteBy eq x ys
668 let (len ** zs) = deleteBy eq x ys
464 in if x `eq` y then (_ ** ys) else (S len ** y ::zs)
669 in if x `eq` y then (_ ** ys) else (S len ** y ::zs)
465
670
671+||| Delete first element from list equal to the given one
672+|||
673+||| ```idris example
674+||| delete 2 (fromList [1,2,2,3,4,4])
675+||| ```
466delete : (Eq elem) => elem -> Vect len elem -> (p ** Vect p elem)
676delete : (Eq elem) => elem -> Vect len elem -> (p ** Vect p elem)
467delete = deleteBy (==)
677delete = deleteBy (==)
468
678
@@ -477,11 +687,21 @@ delete = deleteBy (==)
477|||
687|||
478||| @ n the index to split at
688||| @ n the index to split at
479||| @ xs the `Vect` to split in two
689||| @ xs the `Vect` to split in two
690+|||
691+||| ```idris example
692+||| splitAt 2 (fromList [1,2,3,4])
693+||| ```
480splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
694splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
481splitAt Z xs = ([], xs)
695splitAt Z xs = ([], xs)
482splitAt (S k) (x :: xs) with (splitAt k xs)
696splitAt (S k) (x :: xs) with (splitAt k xs)
483 | (tk, dr) = (x :: tk, dr)
697 | (tk, dr) = (x :: tk, dr)
484
698
699+||| A tuple where the first element is a `Vect` of the `n` elements passing given test
700+||| and the second element is a `Vect` of the remaining elements of the original.
701+|||
702+||| ```idris example
703+||| partition (== 2) (fromList [1,2,3,2,4])
704+||| ```
485partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
705partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
486partition p [] = ((_ ** []), (_ ** []))
706partition p [] = ((_ ** []), (_ ** []))
487partition p (x::xs) =
707partition p (x::xs) =
@@ -495,17 +715,37 @@ partition p (x::xs) =
495-- Predicates
715-- Predicates
496--------------------------------------------------------------------------------
716--------------------------------------------------------------------------------
497
717
718+||| Verify vector prefix
719+|||
720+||| ```idris example
721+||| isPrefixOfBy (==) (fromList [1,2]) (fromList [1,2,3,4])
722+||| ```
498isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
723isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
499isPrefixOfBy p [] right = True
724isPrefixOfBy p [] right = True
500isPrefixOfBy p left [] = False
725isPrefixOfBy p left [] = False
501isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys
726isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys
502
727
728+||| Verify vector prefix
729+|||
730+||| ```idris example
731+||| isPrefixOf (fromList [1,2]) (fromList [1,2,3,4])
732+||| ```
503isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
733isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
504isPrefixOf = isPrefixOfBy (==)
734isPrefixOf = isPrefixOfBy (==)
505
735
736+||| Verify vector suffix
737+|||
738+||| ```idris example
739+||| isSuffixOfBy (==) (fromList [3,4]) (fromList [1,2,3,4])
740+||| ```
506isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
741isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
507isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
742isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
508
743
744+||| Verify vector suffix
745+|||
746+||| ```idris example
747+||| isSuffixOf (fromList [3,4]) (fromList [1,2,3,4])
748+||| ```
509isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
749isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
510isSuffixOf = isSuffixOfBy (==)
750isSuffixOf = isSuffixOfBy (==)
511
751
@@ -513,10 +753,20 @@ isSuffixOf = isSuffixOfBy (==)
513-- Conversions
753-- Conversions
514--------------------------------------------------------------------------------
754--------------------------------------------------------------------------------
515
755
756+||| Convert Maybe type into Vect
757+|||
758+||| ```idris example
759+||| maybeToVect (Just 2)
760+||| ```
516maybeToVect : Maybe elem -> (p ** Vect p elem)
761maybeToVect : Maybe elem -> (p ** Vect p elem)
517maybeToVect Nothing = (_ ** [])
762maybeToVect Nothing = (_ ** [])
518maybeToVect (Just j) = (_ ** [j])
763maybeToVect (Just j) = (_ ** [j])
519
764
765+||| Convert first element of Vect (if exists) into Maybe.
766+|||
767+||| ```idris example
768+||| vectToMaybe [2]
769+||| ```
520vectToMaybe : Vect len elem -> Maybe elem
770vectToMaybe : Vect len elem -> Maybe elem
521vectToMaybe [] = Nothing
771vectToMaybe [] = Nothing
522vectToMaybe (x::xs) = Just x
772vectToMaybe (x::xs) = Just x
@@ -525,6 +775,11 @@ vectToMaybe (x::xs) = Just x
525-- Misc
775-- Misc
526--------------------------------------------------------------------------------
776--------------------------------------------------------------------------------
527
777
778+||| Filter out Nothings from Vect
779+|||
780+||| ```idris example
781+||| catMaybes [Just 1, Just 2, Nothing, Nothing, Just 5]
782+||| ```
528catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem)
783catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem)
529catMaybes [] = (_ ** [])
784catMaybes [] = (_ ** [])
530catMaybes (Nothing::xs) = catMaybes xs
785catMaybes (Nothing::xs) = catMaybes xs
@@ -532,6 +787,11 @@ catMaybes ((Just j)::xs) =
532 let (_ ** tail) = catMaybes xs
787 let (_ ** tail) = catMaybes xs
533 in (_ ** j::tail)
788 in (_ ** j::tail)
534
789
790+||| Get diagonal elements
791+|||
792+||| ```idris example
793+||| diag [[1,2,3], [4,5,6], [7,8,9]]
794+||| ```
535diag : Vect len (Vect len elem) -> Vect len elem
795diag : Vect len (Vect len elem) -> Vect len elem
536diag [] = []
796diag [] = []
537diag ((x::xs)::xss) = x :: diag (map tail xss)
797diag ((x::xs)::xss) = x :: diag (map tail xss)
@@ -545,6 +805,10 @@ range {len=S _} = FZ :: map FS range
545||| This is like zipping all the inner `Vect`s together and is equivalent to `traverse id` (`transposeTraverse`).
805||| This is like zipping all the inner `Vect`s together and is equivalent to `traverse id` (`transposeTraverse`).
546|||
806|||
547||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
807||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
808+|||
809+||| ```idris example
810+||| transpose [[1,2], [3,4], [5,6], [7,8]]
811+||| ```
548transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)
812transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)
549transpose [] = replicate _ [] -- = [| [] |]
813transpose [] = replicate _ [] -- = [| [] |]
550transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]
814transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]