@@ -45,64 +45,36 @@ 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
52tail : Vect (S len) elem -> Vect len elem
48tail : Vect (S len) elem -> Vect len elem
53tail (x::xs) = xs
49tail (x::xs) = xs
55||| Only the first element of the vector
51||| Only the first element of the vector
60head : Vect (S len) elem -> elem
52head : Vect (S len) elem -> elem
61head (x::xs) = x
53head (x::xs) = x
63||| The last element of the vector
55||| The last element of the vector
68last : Vect (S len) elem -> elem
56last : Vect (S len) elem -> elem
69last (x::[]) = x
57last (x::[]) = x
70last (x::y::ys) = last $ y::ys
58last (x::y::ys) = last $ y::ys
72||| All but the last element of the vector
60||| All but the last element of the vector
77init : Vect (S len) elem -> Vect len elem
61init : Vect (S len) elem -> Vect len elem
78init (x::[]) = []
62init (x::[]) = []
79init (x::y::ys) = x :: init (y::ys)
63init (x::y::ys) = x :: init (y::ys)
81||| Extract a particular element from a vector
65||| Extract a particular element from a vector
86index : Fin len -> Vect len elem -> elem
66index : Fin len -> Vect len elem -> elem
87index FZ (x::xs) = x
67index FZ (x::xs) = x
88index (FS k) (x::xs) = index k xs
68index (FS k) (x::xs) = index k xs
91||| Insert an element at a particular index
71||| Insert an element at a particular index
94−||| insertAt 1 8 [1,2,3,4]
96insertAt : Fin (S len) -> elem -> Vect len elem -> Vect (S len) elem
72insertAt : Fin (S len) -> elem -> Vect len elem -> Vect (S len) elem
97insertAt FZ y xs = y :: xs
73insertAt FZ y xs = y :: xs
98insertAt (FS k) y (x::xs) = x :: insertAt k y xs
74insertAt (FS k) y (x::xs) = x :: insertAt k y xs
99insertAt (FS k) y [] = absurd k
75insertAt (FS k) y [] = absurd k
101||| Construct a new vector consisting of all but the indicated element
77||| Construct a new vector consisting of all but the indicated element
104−||| deleteAt 1 [1,2,3,4]
106deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem
78deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem
107deleteAt FZ (x::xs) = xs
79deleteAt FZ (x::xs) = xs
108deleteAt {len = S m} (FS k) (x::xs) = x :: deleteAt k xs
80deleteAt {len = S m} (FS k) (x::xs) = x :: deleteAt k xs
@@ -110,10 +82,6 @@ deleteAt {len = Z} (FS k) (x::xs) = absurd k
110deleteAt _ [] impossible
82deleteAt _ [] impossible
112||| Replace an element at a particlar index with another
84||| Replace an element at a particlar index with another
115−||| replaceAt 1 8 [1,2,3,4]
117replaceAt : Fin len -> elem -> Vect len elem -> Vect len elem
85replaceAt : Fin len -> elem -> Vect len elem -> Vect len elem
118replaceAt FZ y (x::xs) = y :: xs
86replaceAt FZ y (x::xs) = y :: xs
119replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
87replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
@@ -122,10 +90,6 @@ replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
122||| @ i the index to replace at
90||| @ i the index to replace at
123||| @ f the update function
91||| @ f the update function
124||| @ xs the vector to replace in
92||| @ xs the vector to replace in
127−||| updateAt 1 (+10) [1,2,3,4]
129updateAt : (i : Fin len) -> (f : elem -> elem) -> (xs : Vect len elem) -> Vect len elem
93updateAt : (i : Fin len) -> (f : elem -> elem) -> (xs : Vect len elem) -> Vect len elem
130updateAt FZ f (x::xs) = f x :: xs
94updateAt FZ f (x::xs) = f x :: xs
131updateAt (FS k) f (x::xs) = x :: updateAt k f xs
95updateAt (FS k) f (x::xs) = x :: updateAt k f xs
@@ -136,54 +100,20 @@ updateAt (FS k) f (x::xs) = x :: updateAt k f xs
137||| Get the first n elements of a Vect
101||| Get the first n elements of a Vect
138||| @ n the number of elements to take
102||| @ n the number of elements to take
143take : (n : Nat) -> Vect (n + m) elem -> Vect n elem
103take : (n : Nat) -> Vect (n + m) elem -> Vect n elem
144take Z xs = []
104take Z xs = []
145take (S k) (x :: xs) = x :: take k xs
105take (S k) (x :: xs) = x :: take k xs
147||| Remove the first n elements of a Vect
107||| Remove the first n elements of a Vect
148||| @ n the number of elements to remove
108||| @ n the number of elements to remove
153drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
109drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
154drop Z xs = xs
110drop Z xs = xs
155drop (S k) (x :: xs) = drop k xs
111drop (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
179||| Take the longest prefix of a Vect such that all elements satisfy some
113||| Take the longest prefix of a Vect such that all elements satisfy some
180||| Boolean predicate.
114||| Boolean predicate.
182||| @ p the predicate
116||| @ p the predicate
185−||| takeWhile (<3) [1,2,3,4]
187takeWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
117takeWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
188takeWhile p [] = (_ ** [])
118takeWhile p [] = (_ ** [])
189takeWhile p (x::xs) =
119takeWhile p (x::xs) =
@@ -197,10 +127,6 @@ takeWhile p (x::xs) =
197||| Boolean predicate.
127||| Boolean predicate.
199||| @ p the predicate
129||| @ p the predicate
202−||| dropWhile (<3) [1,2,3,4]
204dropWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
130dropWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
205dropWhile p [] = (_ ** [])
131dropWhile p [] = (_ ** [])
206dropWhile p (x::xs) =
132dropWhile p (x::xs) =
@@ -214,10 +140,6 @@ dropWhile p (x::xs) =
214--------------------------------------------------------------------------------
140--------------------------------------------------------------------------------
216||| Reverse the order of the elements of a vector
142||| Reverse the order of the elements of a vector
219−||| reverse [1,2,3,4]
221reverse : Vect len elem -> Vect len elem
143reverse : Vect len elem -> Vect len elem
222reverse xs = go [] xs
144reverse xs = go [] xs
223 where go : Vect n elem -> Vect m elem -> Vect (n+m) elem
145 where go : Vect n elem -> Vect m elem -> Vect (n+m) elem
@@ -228,10 +150,6 @@ reverse xs = go [] xs
228||| Alternate an element between the other elements of a vector
150||| Alternate an element between the other elements of a vector
229||| @ sep the element to intersperse
151||| @ sep the element to intersperse
230||| @ xs the vector to separate with `sep`
152||| @ xs the vector to separate with `sep`
233−||| intersperse 0 [1,2,3,4]
235intersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elem
153intersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elem
236intersperse sep [] = []
154intersperse sep [] = []
237intersperse sep (x::xs) = x :: intersperse' sep xs
155intersperse sep (x::xs) = x :: intersperse' sep xs
@@ -256,10 +174,6 @@ fromList' {len} ys (x::xs) =
256||| Convert a list to a vector.
174||| Convert a list to a vector.
258||| The length of the list should be statically known.
176||| The length of the list should be statically known.
261−||| fromList [1,2,3,4]
263fromList : (l : List elem) -> Vect (length l) elem
177fromList : (l : List elem) -> Vect (length l) elem
264fromList l =
178fromList l =
265 rewrite (sym $ plusZeroRightNeutral (length l)) in
179 rewrite (sym $ plusZeroRightNeutral (length l)) in
@@ -270,31 +184,19 @@ fromList l =
270--------------------------------------------------------------------------------
184--------------------------------------------------------------------------------
272||| Append two vectors
186||| Append two vectors
275−||| [1,2,3,4] ++ [5,6]
277(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem
187(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem
278(++) [] ys = ys
188(++) [] ys = ys
279(++) (x::xs) ys = x :: xs ++ ys
189(++) (x::xs) ys = x :: xs ++ ys
281−||| Repeat some value some number of times.
191+||| Repeate some value some number of times.
283||| @ len the number of times to repeat it
193||| @ len the number of times to repeat it
284||| @ x the value to repeat
194||| @ x the value to repeat
289replicate : (len : Nat) -> (x : elem) -> Vect len elem
195replicate : (len : Nat) -> (x : elem) -> Vect len elem
290replicate Z x = []
196replicate Z x = []
291replicate (S k) x = x :: replicate k x
197replicate (S k) x = x :: replicate k x
293||| Merge two ordered vectors
199||| Merge two ordered vectors
296−||| mergeBy compare (fromList [1,3,5]) (fromList [2,3,4,5,6])
298mergeBy : (elem -> elem -> Ordering) -> (xs : Vect n elem) -> (ys : Vect m elem) -> Vect (n + m) elem
200mergeBy : (elem -> elem -> Ordering) -> (xs : Vect n elem) -> (ys : Vect m elem) -> Vect (n + m) elem
299mergeBy order [] [] = []
201mergeBy order [] [] = []
300mergeBy order [] (x :: xs) = x :: xs
202mergeBy order [] (x :: xs) = x :: xs
@@ -318,54 +220,30 @@ merge = mergeBy compare
318||| @ f the function to combine elements with
220||| @ f the function to combine elements with
319||| @ xs the first vector of elements
221||| @ xs the first vector of elements
320||| @ ys the second vector of elements
222||| @ ys the second vector of elements
323−||| zipWith (+) (fromList [1,2,3,4]) (fromList [5,6,7,8])
325zipWith : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n c
223zipWith : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n c
326zipWith f [] [] = []
224zipWith f [] [] = []
327zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
225zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
329||| Combine three equal-length vectors into a vector with some function
227||| 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])
334zipWith3 : (a -> b -> c -> d) -> (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n d
228zipWith3 : (a -> b -> c -> d) -> (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n d
335zipWith3 f [] [] [] = []
229zipWith3 f [] [] [] = []
336zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
230zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
338||| Combine two equal-length vectors pairwise
232||| Combine two equal-length vectors pairwise
341−||| zip (fromList [1,2,3,4]) (fromList [1,2,3,4])
343zip : (xs : Vect n a) -> (ys : Vect n b) -> Vect n (a, b)
233zip : (xs : Vect n a) -> (ys : Vect n b) -> Vect n (a, b)
344zip = zipWith (\x,y => (x,y))
234zip = zipWith (\x,y => (x,y))
346||| Combine three equal-length vectors elementwise into a vector of tuples
236||| 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])
351zip3 : (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n (a, b, c)
237zip3 : (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n (a, b, c)
352zip3 = zipWith3 (\x,y,z => (x,y,z))
238zip3 = zipWith3 (\x,y,z => (x,y,z))
354||| Convert a vector of pairs to a pair of vectors
240||| Convert a vector of pairs to a pair of vectors
357−||| unzip (fromList [(1,2), (1,2)])
359unzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b)
241unzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b)
360unzip [] = ([], [])
242unzip [] = ([], [])
361unzip ((l, r)::xs) with (unzip xs)
243unzip ((l, r)::xs) with (unzip xs)
362 | (lefts, rights) = (l::lefts, r::rights)
244 | (lefts, rights) = (l::lefts, r::rights)
364||| Convert a vector of three-tuples to a triplet of vectors
246||| Convert a vector of three-tuples to a triplet of vectors
367−||| unzip3 (fromList [(1,2,3), (1,2,3)])
369unzip3 : (xs : Vect n (a, b, c)) -> (Vect n a, Vect n b, Vect n c)
247unzip3 : (xs : Vect n (a, b, c)) -> (Vect n a, Vect n b, Vect n c)
370unzip3 [] = ([], [], [])
248unzip3 [] = ([], [], [])
371unzip3 ((l,c,r)::xs) with (unzip3 xs)
249unzip3 ((l,c,r)::xs) with (unzip3 xs)
@@ -407,10 +285,6 @@ implementation Functor (Vect n) where
408||| @ f the partial function (expressed by returning `Maybe`)
286||| @ f the partial function (expressed by returning `Maybe`)
409||| @ xs the vector to check for results
287||| @ xs the vector to check for results
412−||| mapMaybe ((find (=='a')) . unpack) (fromList ["abc","ade","bgh","xyz"])
414mapMaybe : (f : a -> Maybe b) -> (xs : Vect len a) -> (m : Nat ** Vect m b)
288mapMaybe : (f : a -> Maybe b) -> (xs : Vect len a) -> (m : Nat ** Vect m b)
415mapMaybe f [] = (_ ** [])
289mapMaybe f [] = (_ ** [])
416mapMaybe f (x::xs) =
290mapMaybe f (x::xs) =
@@ -419,6 +293,7 @@ mapMaybe f (x::xs) =
419 Just y => (S len ** y :: ys)
293 Just y => (S len ** y :: ys)
420 Nothing => ( len ** ys)
294 Nothing => ( len ** ys)
422--------------------------------------------------------------------------------
297--------------------------------------------------------------------------------
424--------------------------------------------------------------------------------
299--------------------------------------------------------------------------------
@@ -435,41 +310,23 @@ implementation Foldable (Vect n) where
435--------------------------------------------------------------------------------
310--------------------------------------------------------------------------------
437||| Flatten a vector of equal-length vectors
312||| Flatten a vector of equal-length vectors
440−||| concat [[1,2,3], [4,5,6]]
442concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem
313concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem
443concat [] = []
314concat [] = []
444concat (v::vs) = v ++ concat vs
315concat (v::vs) = v ++ concat vs
446||| Foldr without seeding the accumulator
317||| Foldr without seeding the accumulator
449−||| foldr1 (-) (fromList [1,2,3])
451foldr1 : (t -> t -> t) -> Vect (S n) t -> t
318foldr1 : (t -> t -> t) -> Vect (S n) t -> t
452−foldr1 f [x] = x
319+foldr1 f (x::xs) = foldr f x xs
453−foldr1 f (x::y::xs) = f x (foldr1 f (y::xs))
455||| Foldl without seeding the accumulator
321||| Foldl without seeding the accumulator
458−||| foldl1 (-) (fromList [1,2,3])
460foldl1 : (t -> t -> t) -> Vect (S n) t -> t
322foldl1 : (t -> t -> t) -> Vect (S n) t -> t
461foldl1 f (x::xs) = foldl f x xs
323foldl1 f (x::xs) = foldl f x xs
463--------------------------------------------------------------------------------
324--------------------------------------------------------------------------------
465--------------------------------------------------------------------------------
326--------------------------------------------------------------------------------
467||| The scanl function is similar to foldl, but returns all the intermediate
328||| The scanl function is similar to foldl, but returns all the intermediate
468||| accumulator states in the form of a vector.
329||| accumulator states in the form of a vector.
471−||| scanl (-) 0 (fromList [1,2,3])
473scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res
330scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res
474scanl f q [] = [q]
331scanl f q [] = [q]
475scanl f q (x::xs) = q :: scanl f (f q x) xs
332scanl f q (x::xs) = q :: scanl f (f q x) xs
@@ -478,10 +335,6 @@ scanl f q (x::xs) = q :: scanl f (f q x) xs
478||| starting value.
335||| starting value.
479||| It assumes the first element of the vector to be the starting value and then
336||| It assumes the first element of the vector to be the starting value and then
480||| starts the fold with the element following it.
337||| starts the fold with the element following it.
483−||| scanl1 (-) (fromList [1,2,3])
485scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem
338scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem
486scanl1 f [] = []
339scanl1 f [] = []
487scanl1 f (x::xs) = scanl f x xs
340scanl1 f (x::xs) = scanl f x xs
@@ -494,10 +347,6 @@ scanl1 f (x::xs) = scanl f x xs
494||| @ p the equality test
347||| @ p the equality test
495||| @ e the item to search for
348||| @ e the item to search for
496||| @ xs the vector to search in
349||| @ xs the vector to search in
499−||| elemBy (==) 2 [1,2,3,4]
501elemBy : (p : elem -> elem -> Bool) -> (e : elem) -> (xs : Vect len elem) -> Bool
350elemBy : (p : elem -> elem -> Bool) -> (e : elem) -> (xs : Vect len elem) -> Bool
502elemBy p e [] = False
351elemBy p e [] = False
503elemBy p e (x::xs) = p e x || elemBy p e xs
352elemBy p e (x::xs) = p e x || elemBy p e xs
@@ -505,29 +354,17 @@ elemBy p e (x::xs) = p e x || elemBy p e xs
505||| Use the default Boolean equality on elements to search for an item
354||| Use the default Boolean equality on elements to search for an item
506||| @ x what to search for
355||| @ x what to search for
507||| @ xs where to search
356||| @ xs where to search
512elem : Eq elem => (x : elem) -> (xs : Vect len elem) -> Bool
357elem : Eq elem => (x : elem) -> (xs : Vect len elem) -> Bool
513elem = elemBy (==)
358elem = elemBy (==)
515||| Find the association of some key with a user-provided comparison
360||| Find the association of some key with a user-provided comparison
516||| @ p the comparison operator for keys (True if they match)
361||| @ p the comparison operator for keys (True if they match)
517||| @ e the key to look for
362||| @ e the key to look for
520−||| lookupBy (==) 2 [(1, 'a'), (2, 'b'), (3, 'c')]
522lookupBy : (p : key -> key -> Bool) -> (e : key) -> (xs : Vect n (key, val)) -> Maybe val
363lookupBy : (p : key -> key -> Bool) -> (e : key) -> (xs : Vect n (key, val)) -> Maybe val
523lookupBy p e [] = Nothing
364lookupBy p e [] = Nothing
524lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs
365lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs
526||| Find the assocation of some key using the default Boolean equality test
367||| Find the assocation of some key using the default Boolean equality test
529−||| lookup 3 [(1, 'a'), (2, 'b'), (3, 'c')]
531lookup : Eq key => key -> Vect n (key, val) -> Maybe val
368lookup : Eq key => key -> Vect n (key, val) -> Maybe val
532lookup = lookupBy (==)
369lookup = lookupBy (==)
@@ -535,19 +372,11 @@ lookup = lookupBy (==)
535||| @ p the comparison operator
372||| @ p the comparison operator
536||| @ elems the vector to search
373||| @ elems the vector to search
537||| @ xs what to search for
374||| @ xs what to search for
540−||| hasAnyBy (==) [2,5] [1,2,3,4]
542hasAnyBy : (p : elem -> elem -> Bool) -> (elems : Vect m elem) -> (xs : Vect len elem) -> Bool
375hasAnyBy : (p : elem -> elem -> Bool) -> (elems : Vect m elem) -> (xs : Vect len elem) -> Bool
543hasAnyBy p elems [] = False
376hasAnyBy p elems [] = False
544hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs
377hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs
546||| Check if any element of xs is found in elems using the default Boolean equality test
379||| Check if any element of xs is found in elems using the default Boolean equality test
549−||| hasAny [2,5] [1,2,3,4]
551hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool
380hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool
552hasAny = hasAnyBy (==)
381hasAny = hasAnyBy (==)
@@ -557,62 +386,30 @@ hasAny = hasAnyBy (==)
558||| Find the first element of the vector that satisfies some test
387||| Find the first element of the vector that satisfies some test
559||| @ p the test to satisfy
388||| @ p the test to satisfy
562−||| find (== 3) [1,2,3,4]
564find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem
389find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem
565find p [] = Nothing
390find p [] = Nothing
566find p (x::xs) = if p x then Just x else find p xs
391find p (x::xs) = if p x then Just x else find p xs
568||| Find the index of the first element of the vector that satisfies some test
393||| Find the index of the first element of the vector that satisfies some test
571−||| findIndex (== 3) [1,2,3,4]
573findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)
394findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)
574findIndex p [] = Nothing
395findIndex p [] = Nothing
575findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)
396findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)
577||| Find the indices of all elements that satisfy some test
398||| Find the indices of all elements that satisfy some test
580−||| findIndices (< 3) [1,2,3,4]
582findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)
399findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)
583findIndices p [] = []
400findIndices p [] = []
584findIndices p (x :: xs) = let is = map FS $ findIndices p xs
401findIndices p (x :: xs) = let is = map FS $ findIndices p xs
585 in if p x then 0 :: is else is
402 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]
592elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)
404elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)
593elemIndexBy p e = findIndex $ p e
405elemIndexBy 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]
600elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)
407elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)
601elemIndex = elemIndexBy (==)
408elemIndex = elemIndexBy (==)
603−||| Find the indices of all elements that satisfy some test
606−||| elemIndicesBy (<=) 3 [1,2,3,4]
608elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)
410elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)
609elemIndicesBy p e = findIndices $ p e
411elemIndicesBy 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]
616elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
413elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
617elemIndices = elemIndicesBy (==)
414elemIndices = elemIndicesBy (==)
@@ -621,10 +418,6 @@ elemIndices = elemIndicesBy (==)
621--------------------------------------------------------------------------------
418--------------------------------------------------------------------------------
623||| Find all elements of a vector that satisfy some test
420||| Find all elements of a vector that satisfy some test
626−||| filter (< 3) (fromList [1,2,3,4])
628filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
421filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
629filter p [] = ( _ ** [] )
422filter p [] = ( _ ** [] )
630filter p (x::xs) =
423filter p (x::xs) =
@@ -635,10 +428,6 @@ filter p (x::xs) =
635 (_ ** tail)
428 (_ ** tail)
637||| Make the elements of some vector unique by some test
430||| Make the elements of some vector unique by some test
640−||| nubBy (==) (fromList [1,2,2,3,4,4])
642nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
431nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
643nubBy = nubBy' []
432nubBy = nubBy' []
@@ -650,29 +439,15 @@ nubBy = nubBy' []
650 | (_ ** tail) = (_ ** x::tail)
439 | (_ ** tail) = (_ ** x::tail)
652||| Make the elements of some vector unique by the default Boolean equality
441||| Make the elements of some vector unique by the default Boolean equality
655−||| nub (fromList [1,2,2,3,4,4])
657nub : Eq elem => Vect len elem -> (p ** Vect p elem)
442nub : Eq elem => Vect len elem -> (p ** Vect p elem)
658nub = nubBy (==)
443nub = nubBy (==)
660−||| Delete first element from list according to some test
663−||| deleteBy (<) 3 (fromList [1,2,2,3,4,4])
665deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem)
445deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem)
666deleteBy _ _ [] = (_ ** [])
446deleteBy _ _ [] = (_ ** [])
667deleteBy eq x (y::ys) =
447deleteBy eq x (y::ys) =
668 let (len ** zs) = deleteBy eq x ys
448 let (len ** zs) = deleteBy eq x ys
669 in if x `eq` y then (_ ** ys) else (S len ** y ::zs)
449 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])
676delete : (Eq elem) => elem -> Vect len elem -> (p ** Vect p elem)
451delete : (Eq elem) => elem -> Vect len elem -> (p ** Vect p elem)
677delete = deleteBy (==)
452delete = deleteBy (==)
@@ -680,28 +455,14 @@ delete = deleteBy (==)
680-- Splitting and breaking lists
455-- Splitting and breaking lists
681--------------------------------------------------------------------------------
456--------------------------------------------------------------------------------
683−||| A tuple where the first element is a `Vect` of the `n` first elements and
458+||| A tuple where the first element is a Vect of the n first elements and
684−||| the second element is a `Vect` of the remaining elements of the original.
459+||| the second element is a Vect of the remaining elements of the original Vect
685−||| It is equivalent to `(take n xs, drop n xs)` (`splitAtTakeDrop`),
460+||| It is equivalent to (take n xs, drop n xs)
686−||| but is more efficient.
688||| @ n the index to split at
461||| @ n the index to split at
689−||| @ xs the `Vect` to split in two
462+||| @ xs the Vect to split in two
692−||| splitAt 2 (fromList [1,2,3,4])
694splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
463splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
695−splitAt Z xs = ([], xs)
464+splitAt n xs = (take n xs, drop n 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])
705partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
466partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
706partition p [] = ((_ ** []), (_ ** []))
467partition p [] = ((_ ** []), (_ ** []))
707partition p (x::xs) =
468partition p (x::xs) =
@@ -715,37 +476,17 @@ partition p (x::xs) =
715-- Predicates
476-- Predicates
716--------------------------------------------------------------------------------
477--------------------------------------------------------------------------------
718−||| Verify vector prefix
721−||| isPrefixOfBy (==) (fromList [1,2]) (fromList [1,2,3,4])
723isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
479isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
724isPrefixOfBy p [] right = True
480isPrefixOfBy p [] right = True
725isPrefixOfBy p left [] = False
481isPrefixOfBy p left [] = False
726isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys
482isPrefixOfBy 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])
733isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
484isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
734isPrefixOf = isPrefixOfBy (==)
485isPrefixOf = isPrefixOfBy (==)
736−||| Verify vector suffix
739−||| isSuffixOfBy (==) (fromList [3,4]) (fromList [1,2,3,4])
741isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
487isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
742isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
488isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
744−||| Verify vector suffix
747−||| isSuffixOf (fromList [3,4]) (fromList [1,2,3,4])
749isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
490isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
750isSuffixOf = isSuffixOfBy (==)
491isSuffixOf = isSuffixOfBy (==)
@@ -753,20 +494,10 @@ isSuffixOf = isSuffixOfBy (==)
753-- Conversions
494-- Conversions
754--------------------------------------------------------------------------------
495--------------------------------------------------------------------------------
756−||| Convert Maybe type into Vect
759−||| maybeToVect (Just 2)
761maybeToVect : Maybe elem -> (p ** Vect p elem)
497maybeToVect : Maybe elem -> (p ** Vect p elem)
762maybeToVect Nothing = (_ ** [])
498maybeToVect Nothing = (_ ** [])
763maybeToVect (Just j) = (_ ** [j])
499maybeToVect (Just j) = (_ ** [j])
765−||| Convert first element of Vect (if exists) into Maybe.
770vectToMaybe : Vect len elem -> Maybe elem
501vectToMaybe : Vect len elem -> Maybe elem
771vectToMaybe [] = Nothing
502vectToMaybe [] = Nothing
772vectToMaybe (x::xs) = Just x
503vectToMaybe (x::xs) = Just x
@@ -775,11 +506,6 @@ vectToMaybe (x::xs) = Just x
776--------------------------------------------------------------------------------
507--------------------------------------------------------------------------------
778−||| Filter out Nothings from Vect
781−||| catMaybes [Just 1, Just 2, Nothing, Nothing, Just 5]
783catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem)
509catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem)
784catMaybes [] = (_ ** [])
510catMaybes [] = (_ ** [])
785catMaybes (Nothing::xs) = catMaybes xs
511catMaybes (Nothing::xs) = catMaybes xs
@@ -787,11 +513,6 @@ catMaybes ((Just j)::xs) =
787 let (_ ** tail) = catMaybes xs
513 let (_ ** tail) = catMaybes xs
788 in (_ ** j::tail)
514 in (_ ** j::tail)
790−||| Get diagonal elements
793−||| diag [[1,2,3], [4,5,6], [7,8,9]]
795diag : Vect len (Vect len elem) -> Vect len elem
516diag : Vect len (Vect len elem) -> Vect len elem
796diag [] = []
517diag [] = []
797diag ((x::xs)::xss) = x :: diag (map tail xss)
518diag ((x::xs)::xss) = x :: diag (map tail xss)
@@ -800,18 +521,12 @@ range : {len : Nat} -> Vect len (Fin len)
800range {len=Z} = []
521range {len=Z} = []
801range {len=S _} = FZ :: map FS range
522range {len=S _} = FZ :: map FS range
803−||| Transpose a `Vect` of `Vect`s, turning rows into columns and vice versa.
524+||| Transpose a Vect of Vects, 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`).
807||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
526||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
810−||| transpose [[1,2], [3,4], [5,6], [7,8]]
812−transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)
527+transpose : {n : Nat} -> Vect m (Vect n elem) -> Vect n (Vect m elem)
813−transpose [] = replicate _ [] -- = [| [] |]
528+transpose [] = replicate _ []
814−transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]
529+transpose (x :: xs) = zipWith (::) x (transpose xs)
816--------------------------------------------------------------------------------
531--------------------------------------------------------------------------------
817-- Applicative/Monad/Traversable
532-- Applicative/Monad/Traversable
@@ -819,6 +534,7 @@ transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]
820implementation Applicative (Vect k) where
535implementation Applicative (Vect k) where
821 pure = replicate _
536 pure = replicate _
822 fs <*> vs = zipWith apply fs vs
538 fs <*> vs = zipWith apply fs vs
824||| This monad is different from the List monad, (>>=)
540||| This monad is different from the List monad, (>>=)
@@ -827,8 +543,8 @@ implementation Monad (Vect len) where
827 m >>= f = diag (map f m)
543 m >>= f = diag (map f m)
829implementation Traversable (Vect n) where
545implementation Traversable (Vect n) where
830− traverse f [] = [| [] |]
546+ traverse f [] = pure Vect.Nil
831− traverse f (x :: xs) = [| f x :: traverse f xs |]
547+ traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
833--------------------------------------------------------------------------------
549--------------------------------------------------------------------------------
@@ -837,29 +553,13 @@ implementation Traversable (Vect n) where
837implementation Show elem => Show (Vect len elem) where
553implementation Show elem => Show (Vect len elem) where
838 show = show . toList
554 show = show . toList
840−--------------------------------------------------------------------------------
842−--------------------------------------------------------------------------------
844−Uninhabited a => Uninhabited (Vect (S n) a) where
845− uninhabited (x :: _) = uninhabited x
847--------------------------------------------------------------------------------
556--------------------------------------------------------------------------------
848-- Properties
557-- Properties
849--------------------------------------------------------------------------------
558--------------------------------------------------------------------------------
851−vectMustBeNil : (xs : Vect Z a) -> xs = []
852−vectMustBeNil [] = Refl
854vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys)
560vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys)
855vectConsCong x xs xs Refl = Refl
561vectConsCong 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
863vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
563vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
864vectNilRightNeutral [] = Refl
564vectNilRightNeutral [] = Refl
865vectNilRightNeutral (x :: xs) =
565vectNilRightNeutral (x :: xs) =
@@ -873,93 +573,16 @@ vectAppendAssociative [] y z = Refl
873vectAppendAssociative (x :: xs) ys zs =
573vectAppendAssociative (x :: xs) ys zs =
874 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
574 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
959--------------------------------------------------------------------------------
576--------------------------------------------------------------------------------
961--------------------------------------------------------------------------------
578--------------------------------------------------------------------------------
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
963implementation DecEq a => DecEq (Vect n a) where
586implementation DecEq a => DecEq (Vect n a) where
964 decEq [] [] = Yes Refl
587 decEq [] [] = Yes Refl
965 decEq (x :: xs) (y :: ys) with (decEq x y)
588 decEq (x :: xs) (y :: ys) with (decEq x y)