@@ -45,36 +45,64 @@ lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl
45--------------------------------------------------------------------------------
45--------------------------------------------------------------------------------
47||| All but the first element of the vector
47||| All but the first element of the vector
48tail : Vect (S len) elem -> Vect len elem
52tail : Vect (S len) elem -> Vect len elem
49tail (x::xs) = xs
53tail (x::xs) = xs
51||| Only the first element of the vector
55||| Only the first element of the vector
52head : Vect (S len) elem -> elem
60head : Vect (S len) elem -> elem
53head (x::xs) = x
61head (x::xs) = x
55||| The last element of the vector
63||| The last element of the vector
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
60||| All but the last element of the vector
72||| All but the last element of the vector
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)
65||| Extract a particular element from a vector
81||| Extract a particular element from a vector
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
71||| Insert an element at a particular index
91||| Insert an element at a particular index
94+||| insertAt 1 8 [1,2,3,4]
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
77||| Construct a new vector consisting of all but the indicated element
101||| Construct a new vector consisting of all but the indicated element
104+||| deleteAt 1 [1,2,3,4]
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
84||| Replace an element at a particlar index with another
112||| Replace an element at a particlar index with another
115+||| replaceAt 1 8 [1,2,3,4]
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
127+||| updateAt 1 (+10) [1,2,3,4]
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,20 +136,54 @@ updateAt (FS k) f (x::xs) = x :: updateAt k f xs
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
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
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
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
157+||| Take up to the first n elements of a Vect if they exist.
158+||| @ n the maximum number of elements to take
161+||| takeUpto 10 [1,2,3,4]
163+takeUpto : (x : Nat) -> Vect n elem -> Vect (minimum x n) elem
165+takeUpto x [] = rewrite minimumZeroZeroLeft x in []
166+takeUpto (S x) (y::ys) = y :: takeUpto x ys
168+||| Drop up to the first n elements of a Vect if they exist.
169+||| @ n the maximum number of elements to remove.
172+||| dropUpto 10 [1,2,3,4]
174+dropUpto : (x : Nat) -> Vect n elem -> Vect (n `minus` minimum x n) elem
175+dropUpto Z ys {n} = rewrite minusZeroRight n in ys
177+dropUpto (S x) (y :: ys) = dropUpto x ys
113||| Take the longest prefix of a Vect such that all elements satisfy some
179||| Take the longest prefix of a Vect such that all elements satisfy some
114||| Boolean predicate.
180||| Boolean predicate.
116||| @ p the predicate
182||| @ p the predicate
185+||| takeWhile (<3) [1,2,3,4]
117takeWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
187takeWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
118takeWhile p [] = (_ ** [])
188takeWhile p [] = (_ ** [])
119takeWhile p (x::xs) =
189takeWhile p (x::xs) =
@@ -127,6 +197,10 @@ takeWhile p (x::xs) =
127||| Boolean predicate.
197||| Boolean predicate.
129||| @ p the predicate
199||| @ p the predicate
202+||| dropWhile (<3) [1,2,3,4]
130dropWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
204dropWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
131dropWhile p [] = (_ ** [])
205dropWhile p [] = (_ ** [])
132dropWhile p (x::xs) =
206dropWhile p (x::xs) =
@@ -140,6 +214,10 @@ dropWhile p (x::xs) =
140--------------------------------------------------------------------------------
214--------------------------------------------------------------------------------
142||| Reverse the order of the elements of a vector
216||| Reverse the order of the elements of a vector
219+||| reverse [1,2,3,4]
143reverse : Vect len elem -> Vect len elem
221reverse : Vect len elem -> Vect len elem
144reverse xs = go [] xs
222reverse xs = go [] xs
145 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
@@ -150,6 +228,10 @@ reverse xs = go [] xs
150||| Alternate an element between the other elements of a vector
228||| Alternate an element between the other elements of a vector
151||| @ sep the element to intersperse
229||| @ sep the element to intersperse
152||| @ xs the vector to separate with `sep`
230||| @ xs the vector to separate with `sep`
233+||| intersperse 0 [1,2,3,4]
153intersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elem
235intersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elem
154intersperse sep [] = []
236intersperse sep [] = []
155intersperse sep (x::xs) = x :: intersperse' sep xs
237intersperse sep (x::xs) = x :: intersperse' sep xs
@@ -174,6 +256,10 @@ fromList' {len} ys (x::xs) =
174||| Convert a list to a vector.
256||| Convert a list to a vector.
176||| The length of the list should be statically known.
258||| The length of the list should be statically known.
261+||| fromList [1,2,3,4]
177fromList : (l : List elem) -> Vect (length l) elem
263fromList : (l : List elem) -> Vect (length l) elem
178fromList l =
264fromList l =
179 rewrite (sym $ plusZeroRightNeutral (length l)) in
265 rewrite (sym $ plusZeroRightNeutral (length l)) in
@@ -184,19 +270,31 @@ fromList l =
184--------------------------------------------------------------------------------
270--------------------------------------------------------------------------------
186||| Append two vectors
272||| Append two vectors
275+||| [1,2,3,4] ++ [5,6]
187(++) : (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
188(++) [] ys = ys
278(++) [] ys = ys
189(++) (x::xs) ys = x :: xs ++ ys
279(++) (x::xs) ys = x :: xs ++ ys
191−||| Repeate some value some number of times.
281+||| Repeat some value some number of times.
193||| @ len the number of times to repeat it
283||| @ len the number of times to repeat it
194||| @ x the value to repeat
284||| @ x the value to repeat
195replicate : (len : Nat) -> (x : elem) -> Vect len elem
289replicate : (len : Nat) -> (x : elem) -> Vect len elem
196replicate Z x = []
290replicate Z x = []
197replicate (S k) x = x :: replicate k x
291replicate (S k) x = x :: replicate k x
199||| Merge two ordered vectors
293||| Merge two ordered vectors
296+||| mergeBy compare (fromList [1,3,5]) (fromList [2,3,4,5,6])
200mergeBy : (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
201mergeBy order [] [] = []
299mergeBy order [] [] = []
202mergeBy order [] (x :: xs) = x :: xs
300mergeBy order [] (x :: xs) = x :: xs
@@ -220,30 +318,54 @@ merge = mergeBy compare
220||| @ f the function to combine elements with
318||| @ f the function to combine elements with
221||| @ xs the first vector of elements
319||| @ xs the first vector of elements
222||| @ ys the second vector of elements
320||| @ ys the second vector of elements
323+||| zipWith (+) (fromList [1,2,3,4]) (fromList [5,6,7,8])
223zipWith : (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
224zipWith f [] [] = []
326zipWith f [] [] = []
225zipWith 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
227||| Combine three equal-length vectors into a vector with some function
329||| Combine three equal-length vectors into a vector with some function
332+||| zipWith3 (\x,y,z => x+y+z) (fromList [1,2,3,4]) (fromList [5,6,7,8]) (fromList [1,1,1,1])
228zipWith3 : (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
229zipWith3 f [] [] [] = []
335zipWith3 f [] [] [] = []
230zipWith3 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
232||| Combine two equal-length vectors pairwise
338||| Combine two equal-length vectors pairwise
341+||| zip (fromList [1,2,3,4]) (fromList [1,2,3,4])
233zip : (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)
234zip = zipWith (\x,y => (x,y))
344zip = zipWith (\x,y => (x,y))
236||| Combine three equal-length vectors elementwise into a vector of tuples
346||| Combine three equal-length vectors elementwise into a vector of tuples
349+||| zip3 (fromList [1,2,3,4]) (fromList [1,2,3,4]) (fromList [1,2,3,4])
237zip3 : (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)
238zip3 = zipWith3 (\x,y,z => (x,y,z))
352zip3 = zipWith3 (\x,y,z => (x,y,z))
240||| Convert a vector of pairs to a pair of vectors
354||| Convert a vector of pairs to a pair of vectors
357+||| unzip (fromList [(1,2), (1,2)])
241unzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b)
359unzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b)
242unzip [] = ([], [])
360unzip [] = ([], [])
243unzip ((l, r)::xs) with (unzip xs)
361unzip ((l, r)::xs) with (unzip xs)
244 | (lefts, rights) = (l::lefts, r::rights)
362 | (lefts, rights) = (l::lefts, r::rights)
246||| Convert a vector of three-tuples to a triplet of vectors
364||| Convert a vector of three-tuples to a triplet of vectors
367+||| unzip3 (fromList [(1,2,3), (1,2,3)])
247unzip3 : (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)
248unzip3 [] = ([], [], [])
370unzip3 [] = ([], [], [])
249unzip3 ((l,c,r)::xs) with (unzip3 xs)
371unzip3 ((l,c,r)::xs) with (unzip3 xs)
@@ -285,6 +407,10 @@ implementation Functor (Vect n) where
286||| @ f the partial function (expressed by returning `Maybe`)
408||| @ f the partial function (expressed by returning `Maybe`)
287||| @ xs the vector to check for results
409||| @ xs the vector to check for results
412+||| mapMaybe ((find (=='a')) . unpack) (fromList ["abc","ade","bgh","xyz"])
288mapMaybe : (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)
289mapMaybe f [] = (_ ** [])
415mapMaybe f [] = (_ ** [])
290mapMaybe f (x::xs) =
416mapMaybe f (x::xs) =
@@ -293,7 +419,6 @@ mapMaybe f (x::xs) =
293 Just y => (S len ** y :: ys)
419 Just y => (S len ** y :: ys)
294 Nothing => ( len ** ys)
420 Nothing => ( len ** ys)
297--------------------------------------------------------------------------------
422--------------------------------------------------------------------------------
299--------------------------------------------------------------------------------
424--------------------------------------------------------------------------------
@@ -310,23 +435,41 @@ implementation Foldable (Vect n) where
310--------------------------------------------------------------------------------
435--------------------------------------------------------------------------------
312||| Flatten a vector of equal-length vectors
437||| Flatten a vector of equal-length vectors
440+||| concat [[1,2,3], [4,5,6]]
313concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem
442concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem
314concat [] = []
443concat [] = []
315concat (v::vs) = v ++ concat vs
444concat (v::vs) = v ++ concat vs
317||| Foldr without seeding the accumulator
446||| Foldr without seeding the accumulator
449+||| foldr1 (-) (fromList [1,2,3])
318foldr1 : (t -> t -> t) -> Vect (S n) t -> t
451foldr1 : (t -> t -> t) -> Vect (S n) t -> t
319−foldr1 f (x::xs) = foldr f x xs
452+foldr1 f [x] = x
453+foldr1 f (x::y::xs) = f x (foldr1 f (y::xs))
321||| Foldl without seeding the accumulator
455||| Foldl without seeding the accumulator
458+||| foldl1 (-) (fromList [1,2,3])
322foldl1 : (t -> t -> t) -> Vect (S n) t -> t
460foldl1 : (t -> t -> t) -> Vect (S n) t -> t
323foldl1 f (x::xs) = foldl f x xs
461foldl1 f (x::xs) = foldl f x xs
324--------------------------------------------------------------------------------
463--------------------------------------------------------------------------------
326--------------------------------------------------------------------------------
465--------------------------------------------------------------------------------
328||| 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
329||| accumulator states in the form of a vector.
468||| accumulator states in the form of a vector.
471+||| scanl (-) 0 (fromList [1,2,3])
330scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res
473scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res
331scanl f q [] = [q]
474scanl f q [] = [q]
332scanl f q (x::xs) = q :: scanl f (f q x) xs
475scanl f q (x::xs) = q :: scanl f (f q x) xs
@@ -335,6 +478,10 @@ scanl f q (x::xs) = q :: scanl f (f q x) xs
335||| starting value.
478||| starting value.
336||| 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
337||| starts the fold with the element following it.
480||| starts the fold with the element following it.
483+||| scanl1 (-) (fromList [1,2,3])
338scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem
485scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem
339scanl1 f [] = []
486scanl1 f [] = []
340scanl1 f (x::xs) = scanl f x xs
487scanl1 f (x::xs) = scanl f x xs
@@ -347,6 +494,10 @@ scanl1 f (x::xs) = scanl f x xs
347||| @ p the equality test
494||| @ p the equality test
348||| @ e the item to search for
495||| @ e the item to search for
349||| @ xs the vector to search in
496||| @ xs the vector to search in
499+||| elemBy (==) 2 [1,2,3,4]
350elemBy : (p : elem -> elem -> Bool) -> (e : elem) -> (xs : Vect len elem) -> Bool
501elemBy : (p : elem -> elem -> Bool) -> (e : elem) -> (xs : Vect len elem) -> Bool
351elemBy p e [] = False
502elemBy p e [] = False
352elemBy p e (x::xs) = p e x || elemBy p e xs
503elemBy p e (x::xs) = p e x || elemBy p e xs
@@ -354,17 +505,29 @@ elemBy p e (x::xs) = p e x || elemBy p e xs
354||| 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
355||| @ x what to search for
506||| @ x what to search for
356||| @ xs where to search
507||| @ xs where to search
357elem : Eq elem => (x : elem) -> (xs : Vect len elem) -> Bool
512elem : Eq elem => (x : elem) -> (xs : Vect len elem) -> Bool
358elem = elemBy (==)
513elem = elemBy (==)
360||| Find the association of some key with a user-provided comparison
515||| Find the association of some key with a user-provided comparison
361||| @ p the comparison operator for keys (True if they match)
516||| @ p the comparison operator for keys (True if they match)
362||| @ e the key to look for
517||| @ e the key to look for
520+||| lookupBy (==) 2 [(1, 'a'), (2, 'b'), (3, 'c')]
363lookupBy : (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
364lookupBy p e [] = Nothing
523lookupBy p e [] = Nothing
365lookupBy 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
367||| 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
529+||| lookup 3 [(1, 'a'), (2, 'b'), (3, 'c')]
368lookup : Eq key => key -> Vect n (key, val) -> Maybe val
531lookup : Eq key => key -> Vect n (key, val) -> Maybe val
369lookup = lookupBy (==)
532lookup = lookupBy (==)
@@ -372,11 +535,19 @@ lookup = lookupBy (==)
372||| @ p the comparison operator
535||| @ p the comparison operator
373||| @ elems the vector to search
536||| @ elems the vector to search
374||| @ xs what to search for
537||| @ xs what to search for
540+||| hasAnyBy (==) [2,5] [1,2,3,4]
375hasAnyBy : (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
376hasAnyBy p elems [] = False
543hasAnyBy p elems [] = False
377hasAnyBy 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
379||| 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
549+||| hasAny [2,5] [1,2,3,4]
380hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool
551hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool
381hasAny = hasAnyBy (==)
552hasAny = hasAnyBy (==)
@@ -386,30 +557,62 @@ hasAny = hasAnyBy (==)
387||| Find the first element of the vector that satisfies some test
558||| Find the first element of the vector that satisfies some test
388||| @ p the test to satisfy
559||| @ p the test to satisfy
562+||| find (== 3) [1,2,3,4]
389find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem
564find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem
390find p [] = Nothing
565find p [] = Nothing
391find 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
393||| 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
571+||| findIndex (== 3) [1,2,3,4]
394findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)
573findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)
395findIndex p [] = Nothing
574findIndex p [] = Nothing
396findIndex 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)
398||| Find the indices of all elements that satisfy some test
577||| Find the indices of all elements that satisfy some test
580+||| findIndices (< 3) [1,2,3,4]
399findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)
582findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)
400findIndices p [] = []
583findIndices p [] = []
401findIndices p (x :: xs) = let is = map FS $ findIndices p xs
584findIndices p (x :: xs) = let is = map FS $ findIndices p xs
402 in if p x then 0 :: is else is
585 in if p x then 0 :: is else is
587+||| Find the index of the first element of the vector that satisfies some test
590+||| elemIndexBy (==) 3 [1,2,3,4]
404elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)
592elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)
405elemIndexBy p e = findIndex $ p e
593elemIndexBy p e = findIndex $ p e
595+||| Find the index of the first element of the vector equal to the given one.
598+||| elemIndex 3 [1,2,3,4]
407elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)
600elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)
408elemIndex = elemIndexBy (==)
601elemIndex = elemIndexBy (==)
603+||| Find the indices of all elements that satisfy some test
606+||| elemIndicesBy (<=) 3 [1,2,3,4]
410elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)
608elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)
411elemIndicesBy p e = findIndices $ p e
609elemIndicesBy p e = findIndices $ p e
611+||| Find the indices of all elements uquals to the given one
614+||| elemIndices 3 [1,2,3,4,3]
413elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
616elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
414elemIndices = elemIndicesBy (==)
617elemIndices = elemIndicesBy (==)
@@ -418,6 +621,10 @@ elemIndices = elemIndicesBy (==)
418--------------------------------------------------------------------------------
621--------------------------------------------------------------------------------
420||| Find all elements of a vector that satisfy some test
623||| Find all elements of a vector that satisfy some test
626+||| filter (< 3) (fromList [1,2,3,4])
421filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
628filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
422filter p [] = ( _ ** [] )
629filter p [] = ( _ ** [] )
423filter p (x::xs) =
630filter p (x::xs) =
@@ -428,6 +635,10 @@ filter p (x::xs) =
428 (_ ** tail)
635 (_ ** tail)
430||| Make the elements of some vector unique by some test
637||| Make the elements of some vector unique by some test
640+||| nubBy (==) (fromList [1,2,2,3,4,4])
431nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
642nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
432nubBy = nubBy' []
643nubBy = nubBy' []
@@ -439,15 +650,29 @@ nubBy = nubBy' []
439 | (_ ** tail) = (_ ** x::tail)
650 | (_ ** tail) = (_ ** x::tail)
441||| 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
655+||| nub (fromList [1,2,2,3,4,4])
442nub : Eq elem => Vect len elem -> (p ** Vect p elem)
657nub : Eq elem => Vect len elem -> (p ** Vect p elem)
443nub = nubBy (==)
658nub = nubBy (==)
660+||| Delete first element from list according to some test
663+||| deleteBy (<) 3 (fromList [1,2,2,3,4,4])
445deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem)
665deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem)
446deleteBy _ _ [] = (_ ** [])
666deleteBy _ _ [] = (_ ** [])
447deleteBy eq x (y::ys) =
667deleteBy eq x (y::ys) =
448 let (len ** zs) = deleteBy eq x ys
668 let (len ** zs) = deleteBy eq x ys
449 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)
671+||| Delete first element from list equal to the given one
674+||| delete 2 (fromList [1,2,2,3,4,4])
451delete : (Eq elem) => elem -> Vect len elem -> (p ** Vect p elem)
676delete : (Eq elem) => elem -> Vect len elem -> (p ** Vect p elem)
452delete = deleteBy (==)
677delete = deleteBy (==)
@@ -455,14 +680,28 @@ delete = deleteBy (==)
455-- Splitting and breaking lists
680-- Splitting and breaking lists
456--------------------------------------------------------------------------------
681--------------------------------------------------------------------------------
458−||| A tuple where the first element is a Vect of the n first elements and
683+||| A tuple where the first element is a `Vect` of the `n` first elements and
459−||| the second element is a Vect of the remaining elements of the original Vect
684+||| the second element is a `Vect` of the remaining elements of the original.
460−||| It is equivalent to (take n xs, drop n xs)
685+||| It is equivalent to `(take n xs, drop n xs)` (`splitAtTakeDrop`),
686+||| but is more efficient.
461||| @ n the index to split at
688||| @ n the index to split at
462−||| @ xs the Vect to split in two
689+||| @ xs the `Vect` to split in two
692+||| splitAt 2 (fromList [1,2,3,4])
463splitAt : (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)
464−splitAt n xs = (take n xs, drop n xs)
695+splitAt Z xs = ([], xs)
696+splitAt (S k) (x :: xs) with (splitAt k xs)
697+ | (tk, dr) = (x :: tk, dr)
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.
703+||| partition (== 2) (fromList [1,2,3,2,4])
466partition : (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))
467partition p [] = ((_ ** []), (_ ** []))
706partition p [] = ((_ ** []), (_ ** []))
468partition p (x::xs) =
707partition p (x::xs) =
@@ -476,17 +715,37 @@ partition p (x::xs) =
476-- Predicates
715-- Predicates
477--------------------------------------------------------------------------------
716--------------------------------------------------------------------------------
718+||| Verify vector prefix
721+||| isPrefixOfBy (==) (fromList [1,2]) (fromList [1,2,3,4])
479isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
723isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
480isPrefixOfBy p [] right = True
724isPrefixOfBy p [] right = True
481isPrefixOfBy p left [] = False
725isPrefixOfBy p left [] = False
482isPrefixOfBy 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
728+||| Verify vector prefix
731+||| isPrefixOf (fromList [1,2]) (fromList [1,2,3,4])
484isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
733isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
485isPrefixOf = isPrefixOfBy (==)
734isPrefixOf = isPrefixOfBy (==)
736+||| Verify vector suffix
739+||| isSuffixOfBy (==) (fromList [3,4]) (fromList [1,2,3,4])
487isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
741isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
488isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
742isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
744+||| Verify vector suffix
747+||| isSuffixOf (fromList [3,4]) (fromList [1,2,3,4])
490isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
749isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
491isSuffixOf = isSuffixOfBy (==)
750isSuffixOf = isSuffixOfBy (==)
@@ -494,10 +753,20 @@ isSuffixOf = isSuffixOfBy (==)
494-- Conversions
753-- Conversions
495--------------------------------------------------------------------------------
754--------------------------------------------------------------------------------
756+||| Convert Maybe type into Vect
759+||| maybeToVect (Just 2)
497maybeToVect : Maybe elem -> (p ** Vect p elem)
761maybeToVect : Maybe elem -> (p ** Vect p elem)
498maybeToVect Nothing = (_ ** [])
762maybeToVect Nothing = (_ ** [])
499maybeToVect (Just j) = (_ ** [j])
763maybeToVect (Just j) = (_ ** [j])
765+||| Convert first element of Vect (if exists) into Maybe.
501vectToMaybe : Vect len elem -> Maybe elem
770vectToMaybe : Vect len elem -> Maybe elem
502vectToMaybe [] = Nothing
771vectToMaybe [] = Nothing
503vectToMaybe (x::xs) = Just x
772vectToMaybe (x::xs) = Just x
@@ -506,6 +775,11 @@ vectToMaybe (x::xs) = Just x
507--------------------------------------------------------------------------------
776--------------------------------------------------------------------------------
778+||| Filter out Nothings from Vect
781+||| catMaybes [Just 1, Just 2, Nothing, Nothing, Just 5]
509catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem)
783catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem)
510catMaybes [] = (_ ** [])
784catMaybes [] = (_ ** [])
511catMaybes (Nothing::xs) = catMaybes xs
785catMaybes (Nothing::xs) = catMaybes xs
@@ -513,6 +787,11 @@ catMaybes ((Just j)::xs) =
513 let (_ ** tail) = catMaybes xs
787 let (_ ** tail) = catMaybes xs
514 in (_ ** j::tail)
788 in (_ ** j::tail)
790+||| Get diagonal elements
793+||| diag [[1,2,3], [4,5,6], [7,8,9]]
516diag : Vect len (Vect len elem) -> Vect len elem
795diag : Vect len (Vect len elem) -> Vect len elem
517diag [] = []
796diag [] = []
518diag ((x::xs)::xss) = x :: diag (map tail xss)
797diag ((x::xs)::xss) = x :: diag (map tail xss)
@@ -521,12 +800,18 @@ range : {len : Nat} -> Vect len (Fin len)
521range {len=Z} = []
800range {len=Z} = []
522range {len=S _} = FZ :: map FS range
801range {len=S _} = FZ :: map FS range
524−||| Transpose a Vect of Vects, turning rows into columns and vice versa.
803+||| Transpose a `Vect` of `Vect`s, turning rows into columns and vice versa.
805+||| This is like zipping all the inner `Vect`s together and is equivalent to `traverse id` (`transposeTraverse`).
526||| 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`.
527−transpose : {n : Nat} -> Vect m (Vect n elem) -> Vect n (Vect m elem)
808+|||
528−transpose [] = replicate _ []
809+||| ```idris example
529−transpose (x :: xs) = zipWith (::) x (transpose xs)
810+||| transpose [[1,2], [3,4], [5,6], [7,8]]
812+transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)
813+transpose [] = replicate _ [] -- = [| [] |]
814+transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]
531--------------------------------------------------------------------------------
816--------------------------------------------------------------------------------
532-- Applicative/Monad/Traversable
817-- Applicative/Monad/Traversable
@@ -534,7 +819,6 @@ transpose (x :: xs) = zipWith (::) x (transpose xs)
535implementation Applicative (Vect k) where
820implementation Applicative (Vect k) where
536 pure = replicate _
821 pure = replicate _
538 fs <*> vs = zipWith apply fs vs
822 fs <*> vs = zipWith apply fs vs
540||| This monad is different from the List monad, (>>=)
824||| This monad is different from the List monad, (>>=)
@@ -543,8 +827,8 @@ implementation Monad (Vect len) where
543 m >>= f = diag (map f m)
827 m >>= f = diag (map f m)
545implementation Traversable (Vect n) where
829implementation Traversable (Vect n) where
546− traverse f [] = pure Vect.Nil
830+ traverse f [] = [| [] |]
547− traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
831+ traverse f (x :: xs) = [| f x :: traverse f xs |]
549--------------------------------------------------------------------------------
833--------------------------------------------------------------------------------
@@ -553,13 +837,29 @@ implementation Traversable (Vect n) where
553implementation Show elem => Show (Vect len elem) where
837implementation Show elem => Show (Vect len elem) where
554 show = show . toList
838 show = show . toList
840+--------------------------------------------------------------------------------
842+--------------------------------------------------------------------------------
844+Uninhabited a => Uninhabited (Vect (S n) a) where
845+ uninhabited (x :: _) = uninhabited x
556--------------------------------------------------------------------------------
847--------------------------------------------------------------------------------
557-- Properties
848-- Properties
558--------------------------------------------------------------------------------
849--------------------------------------------------------------------------------
851+vectMustBeNil : (xs : Vect Z a) -> xs = []
852+vectMustBeNil [] = Refl
560vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys)
854vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys)
561vectConsCong x xs xs Refl = Refl
855vectConsCong x xs xs Refl = Refl
857+vectInjective1 : {xs : Vect n a} -> {ys : Vect m b} -> x :: xs ~=~ y :: ys -> x ~=~ y
858+vectInjective1 Refl = Refl
860+vectInjective2 : {xs : Vect n a} -> {ys : Vect m b} -> x :: xs ~=~ y :: ys -> xs ~=~ ys
861+vectInjective2 Refl = Refl
563vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
863vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
564vectNilRightNeutral [] = Refl
864vectNilRightNeutral [] = Refl
565vectNilRightNeutral (x :: xs) =
865vectNilRightNeutral (x :: xs) =
@@ -573,16 +873,93 @@ vectAppendAssociative [] y z = Refl
573vectAppendAssociative (x :: xs) ys zs =
873vectAppendAssociative (x :: xs) ys zs =
574 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
874 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
876+||| Adding a prefix and then taking the prefix gets the prefix. Or,
877+||| adding a suffix and then dropping the suffix does nothing.
878+takePrefix : (ns : Vect n a) -> (ms : Vect m a) -> take n (ns ++ ms) = ns
879+takePrefix [] _ = Refl
880+takePrefix (n :: ns) ms = cong $ takePrefix ns ms
882+||| Adding a prefix and then dropping the prefix does nothing. Or,
883+||| adding a suffix and then taking the suffix gets the suffix.
884+dropPrefix : (ns : Vect n a) -> (ms : Vect m a) -> drop n (ns ++ ms) = ms
885+dropPrefix [] ms = Refl
886+dropPrefix (_ :: ns) ms = dropPrefix ns ms
888+||| `take n . take (n + m) = take n`
889+takeTake : (n : Nat) -> (m : Nat) ->
890+ (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->
892+ take n (take (n + m) xs) = take n ys
893+takeTake Z m _ _ _ = Refl
894+takeTake (S n) m (x :: xs) (y :: ys) prf = rewrite vectInjective1 prf in cong (takeTake n m xs ys (vectInjective2 prf))
896+||| `drop (n + m) = drop m . drop n`
897+dropDrop : (n : Nat) -> (m : Nat) ->
898+ (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->
900+ drop (n + m) xs = drop m (drop n ys)
901+dropDrop Z m xs xs Refl = Refl
902+dropDrop (S n) m (_ :: xs) (_ :: ys) prf = dropDrop n m xs ys (vectInjective2 prf)
904+||| A `Vect` may be restored from its components.
905+takeDropConcat : (n : Nat) -> (xs : Vect (n + m) a) -> take n xs ++ drop n xs = xs
906+takeDropConcat Z xs = Refl
907+takeDropConcat (S n) (x :: xs) = cong $ takeDropConcat n xs
909+||| `drop n . take (n + m) = take m . drop n`.
911+||| Or: there are two ways to extract a subsequence.
912+dropTakeTakeDrop : (n : Nat) -> (m : Nat) ->
913+ (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->
915+ drop n (take (n + m) xs) = take m (drop n ys)
916+dropTakeTakeDrop Z m xs xs Refl = Refl
917+dropTakeTakeDrop (S n) m (_ :: xs) (_ :: ys) prf = dropTakeTakeDrop n m xs ys (vectInjective2 prf)
919+splitAtTakeDrop : (n : Nat) -> (xs : Vect (n + m) a) -> splitAt n xs = (take n xs, drop n xs)
920+splitAtTakeDrop Z xs = Refl
921+splitAtTakeDrop (S k) (x :: xs) with (splitAt k xs) proof p
922+ | (tk, dr) = let prf = trans p (splitAtTakeDrop k xs)
923+ in aux (cong {f=(x ::) . fst} prf) (cong {f=snd} prf)
924+ where aux : {a, b : Type} -> {w, x : a} -> {y, z : b} -> w = x -> y = z -> (w, y) = (x, z)
925+ aux Refl Refl = Refl
927+zipWithIsLiftA2 : (f : a -> b -> c) -> (as : Vect n a) -> (bs : Vect n b) -> zipWith f as bs = [| f as bs |]
928+zipWithIsLiftA2 _ [] [] = Refl
929+zipWithIsLiftA2 f (a :: as) (b :: bs) = rewrite zipWithIsLiftA2 f as bs in Refl
930+zipWithIsLiftA3 : (f : a -> b -> c -> d) -> (as : Vect n a) -> (bs : Vect n b) -> (cs : Vect n c) -> zipWith3 f as bs cs = [| f as bs cs |]
931+zipWithIsLiftA3 _ [] [] [] = Refl
932+zipWithIsLiftA3 f (a :: as) (b :: bs) (c :: cs) = rewrite zipWithIsLiftA3 f as bs cs in Refl
934+-- Note relationship to Applicative (Morphism (Fin n))
935+indexReplicate : (x : a) -> (n : Nat) -> (i : Fin n) -> index i (replicate n x) = x
936+indexReplicate x (S n) FZ = Refl
937+indexReplicate x (S n) (FS i) = indexReplicate x n i
938+indexZipWith : (f : a -> b -> c) -> (as : Vect n a) -> (bs : Vect n b) -> (i : Fin n) -> index i (zipWith f as bs) = f (index i as) (index i bs)
939+indexZipWith f (a :: _) (b :: _) FZ = Refl
940+indexZipWith f (_ :: as) (_ :: bs) (FS i) = indexZipWith f as bs i
941+indexTranspose : (x : Fin o) -> (y : Fin i) -> (xss : Vect o (Vect i a)) -> index y (index x xss) = index x (index y (transpose xss))
942+indexTranspose x y (xs :: xss) = rewrite prf in
943+ rewrite sym $ indexZipWith Vect.(::) xs (transpose xss) y in Refl
944+ where prf : index y (index x (xs :: xss)) = index x (index y xs :: index y (transpose xss))
947+ FS k => indexTranspose k y xss
949+transposeTraverse : (xss : Vect o (Vect i a)) -> transpose xss = traverse Basics.id xss
950+transposeTraverse [] = Refl
951+transposeTraverse (xs :: xss) = rewrite zipWithIsLiftA2 Vect.(::) xs (transpose xss) in cong (transposeTraverse xss)
953+traverseIdCons : (xs : Vect o a) -> (xss : Vect o (Vect i a)) -> traverse Basics.id [| xs :: xss |] = xs :: traverse Basics.id xss
954+traverseIdCons [] [] = Refl
955+traverseIdCons (x :: xs) (ys :: xss) = rewrite traverseIdCons xs xss in Refl
956+transposeCons : (xs : Vect o a) -> (xss : Vect o (Vect i a)) -> transpose (zipWith (::) xs xss) = xs :: transpose xss
957+transposeCons xs xss = rewrite zipWithIsLiftA2 Vect.(::) xs xss in rewrite transposeTraverse (pure (::) <*> xs <*> xss) in rewrite transposeTraverse xss in traverseIdCons xs xss
576--------------------------------------------------------------------------------
959--------------------------------------------------------------------------------
578--------------------------------------------------------------------------------
961--------------------------------------------------------------------------------
580−vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y
581−vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
583−vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys
584−vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
586implementation DecEq a => DecEq (Vect n a) where
963implementation DecEq a => DecEq (Vect n a) where
587 decEq [] [] = Yes Refl
964 decEq [] [] = Yes Refl
588 decEq (x :: xs) (y :: ys) with (decEq x y)
965 decEq (x :: xs) (y :: ys) with (decEq x y)