@@ -11,7 +11,6 @@ infixr 7 ::
11||| Vectors: Generic lists with explicit length in the type
11||| Vectors: Generic lists with explicit length in the type
12||| @ len the length of the list
12||| @ len the length of the list
13||| @ elem the type of elements
13||| @ elem the type of elements
15data Vect : (len : Nat) -> (elem : Type) -> Type where
14data Vect : (len : Nat) -> (elem : Type) -> Type where
16 ||| Empty vector
15 ||| Empty vector
17 Nil : Vect Z elem
16 Nil : Vect Z elem
@@ -46,36 +45,64 @@ lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl
46--------------------------------------------------------------------------------
45--------------------------------------------------------------------------------
48||| All but the first element of the vector
47||| All but the first element of the vector
49tail : Vect (S len) elem -> Vect len elem
52tail : Vect (S len) elem -> Vect len elem
50tail (x::xs) = xs
53tail (x::xs) = xs
52||| Only the first element of the vector
55||| Only the first element of the vector
53head : Vect (S len) elem -> elem
60head : Vect (S len) elem -> elem
54head (x::xs) = x
61head (x::xs) = x
56||| The last element of the vector
63||| The last element of the vector
57last : Vect (S len) elem -> elem
68last : Vect (S len) elem -> elem
58last (x::[]) = x
69last (x::[]) = x
59last (x::y::ys) = last $ y::ys
70last (x::y::ys) = last $ y::ys
61||| All but the last element of the vector
72||| All but the last element of the vector
62init : Vect (S len) elem -> Vect len elem
77init : Vect (S len) elem -> Vect len elem
63init (x::[]) = []
78init (x::[]) = []
64init (x::y::ys) = x :: init (y::ys)
79init (x::y::ys) = x :: init (y::ys)
66||| Extract a particular element from a vector
81||| Extract a particular element from a vector
67index : Fin len -> Vect len elem -> elem
86index : Fin len -> Vect len elem -> elem
68index FZ (x::xs) = x
87index FZ (x::xs) = x
69index (FS k) (x::xs) = index k xs
88index (FS k) (x::xs) = index k xs
72||| Insert an element at a particular index
91||| Insert an element at a particular index
94+||| insertAt 1 8 [1,2,3,4]
73insertAt : Fin (S len) -> elem -> Vect len elem -> Vect (S len) elem
96insertAt : Fin (S len) -> elem -> Vect len elem -> Vect (S len) elem
74insertAt FZ y xs = y :: xs
97insertAt FZ y xs = y :: xs
75insertAt (FS k) y (x::xs) = x :: insertAt k y xs
98insertAt (FS k) y (x::xs) = x :: insertAt k y xs
76insertAt (FS k) y [] = absurd k
99insertAt (FS k) y [] = absurd k
78||| 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]
79deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem
106deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem
80deleteAt FZ (x::xs) = xs
107deleteAt FZ (x::xs) = xs
81deleteAt {len = S m} (FS k) (x::xs) = x :: deleteAt k xs
108deleteAt {len = S m} (FS k) (x::xs) = x :: deleteAt k xs
@@ -83,6 +110,10 @@ deleteAt {len = Z} (FS k) (x::xs) = absurd k
83deleteAt _ [] impossible
110deleteAt _ [] impossible
85||| 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]
86replaceAt : Fin len -> elem -> Vect len elem -> Vect len elem
117replaceAt : Fin len -> elem -> Vect len elem -> Vect len elem
87replaceAt FZ y (x::xs) = y :: xs
118replaceAt FZ y (x::xs) = y :: xs
88replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
119replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
@@ -91,6 +122,10 @@ replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
91||| @ i the index to replace at
122||| @ i the index to replace at
92||| @ f the update function
123||| @ f the update function
93||| @ xs the vector to replace in
124||| @ xs the vector to replace in
127+||| updateAt 1 (+10) [1,2,3,4]
94updateAt : (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
95updateAt FZ f (x::xs) = f x :: xs
130updateAt FZ f (x::xs) = f x :: xs
96updateAt (FS k) f (x::xs) = x :: updateAt k f xs
131updateAt (FS k) f (x::xs) = x :: updateAt k f xs
@@ -101,20 +136,54 @@ updateAt (FS k) f (x::xs) = x :: updateAt k f xs
102||| Get the first n elements of a Vect
137||| Get the first n elements of a Vect
103||| @ n the number of elements to take
138||| @ n the number of elements to take
104take : (n : Nat) -> Vect (n + m) elem -> Vect n elem
143take : (n : Nat) -> Vect (n + m) elem -> Vect n elem
105take Z xs = []
144take Z xs = []
106take (S k) (x :: xs) = x :: take k xs
145take (S k) (x :: xs) = x :: take k xs
108||| Remove the first n elements of a Vect
147||| Remove the first n elements of a Vect
109||| @ n the number of elements to remove
148||| @ n the number of elements to remove
110drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
153drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
111drop Z xs = xs
154drop Z xs = xs
112drop (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
114||| 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
115||| Boolean predicate.
180||| Boolean predicate.
117||| @ p the predicate
182||| @ p the predicate
185+||| takeWhile (<3) [1,2,3,4]
118takeWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
187takeWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
119takeWhile p [] = (_ ** [])
188takeWhile p [] = (_ ** [])
120takeWhile p (x::xs) =
189takeWhile p (x::xs) =
@@ -128,6 +197,10 @@ takeWhile p (x::xs) =
128||| Boolean predicate.
197||| Boolean predicate.
130||| @ p the predicate
199||| @ p the predicate
202+||| dropWhile (<3) [1,2,3,4]
131dropWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
204dropWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
132dropWhile p [] = (_ ** [])
205dropWhile p [] = (_ ** [])
133dropWhile p (x::xs) =
206dropWhile p (x::xs) =
@@ -141,6 +214,10 @@ dropWhile p (x::xs) =
141--------------------------------------------------------------------------------
214--------------------------------------------------------------------------------
143||| 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]
144reverse : Vect len elem -> Vect len elem
221reverse : Vect len elem -> Vect len elem
145reverse xs = go [] xs
222reverse xs = go [] xs
146 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
@@ -151,6 +228,10 @@ reverse xs = go [] xs
151||| Alternate an element between the other elements of a vector
228||| Alternate an element between the other elements of a vector
152||| @ sep the element to intersperse
229||| @ sep the element to intersperse
153||| @ xs the vector to separate with `sep`
230||| @ xs the vector to separate with `sep`
233+||| intersperse 0 [1,2,3,4]
154intersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elem
235intersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elem
155intersperse sep [] = []
236intersperse sep [] = []
156intersperse sep (x::xs) = x :: intersperse' sep xs
237intersperse sep (x::xs) = x :: intersperse' sep xs
@@ -175,6 +256,10 @@ fromList' {len} ys (x::xs) =
175||| Convert a list to a vector.
256||| Convert a list to a vector.
177||| 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]
178fromList : (l : List elem) -> Vect (length l) elem
263fromList : (l : List elem) -> Vect (length l) elem
179fromList l =
264fromList l =
180 rewrite (sym $ plusZeroRightNeutral (length l)) in
265 rewrite (sym $ plusZeroRightNeutral (length l)) in
@@ -185,19 +270,31 @@ fromList l =
185--------------------------------------------------------------------------------
270--------------------------------------------------------------------------------
187||| Append two vectors
272||| Append two vectors
275+||| [1,2,3,4] ++ [5,6]
188(++) : (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
189(++) [] ys = ys
278(++) [] ys = ys
190(++) (x::xs) ys = x :: xs ++ ys
279(++) (x::xs) ys = x :: xs ++ ys
192−||| Repeate some value some number of times.
281+||| Repeat some value some number of times.
194||| @ len the number of times to repeat it
283||| @ len the number of times to repeat it
195||| @ x the value to repeat
284||| @ x the value to repeat
196replicate : (len : Nat) -> (x : elem) -> Vect len elem
289replicate : (len : Nat) -> (x : elem) -> Vect len elem
197replicate Z x = []
290replicate Z x = []
198replicate (S k) x = x :: replicate k x
291replicate (S k) x = x :: replicate k x
200||| Merge two ordered vectors
293||| Merge two ordered vectors
296+||| mergeBy compare (fromList [1,3,5]) (fromList [2,3,4,5,6])
201mergeBy : (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
202mergeBy order [] [] = []
299mergeBy order [] [] = []
203mergeBy order [] (x :: xs) = x :: xs
300mergeBy order [] (x :: xs) = x :: xs
@@ -221,30 +318,54 @@ merge = mergeBy compare
221||| @ f the function to combine elements with
318||| @ f the function to combine elements with
222||| @ xs the first vector of elements
319||| @ xs the first vector of elements
223||| @ 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])
224zipWith : (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
225zipWith f [] [] = []
326zipWith f [] [] = []
226zipWith 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
228||| 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])
229zipWith3 : (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
230zipWith3 f [] [] [] = []
335zipWith3 f [] [] [] = []
231zipWith3 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
233||| 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])
234zip : (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)
235zip = zipWith (\x,y => (x,y))
344zip = zipWith (\x,y => (x,y))
237||| 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])
238zip3 : (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)
239zip3 = zipWith3 (\x,y,z => (x,y,z))
352zip3 = zipWith3 (\x,y,z => (x,y,z))
241||| 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)])
242unzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b)
359unzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b)
243unzip [] = ([], [])
360unzip [] = ([], [])
244unzip ((l, r)::xs) with (unzip xs)
361unzip ((l, r)::xs) with (unzip xs)
245 | (lefts, rights) = (l::lefts, r::rights)
362 | (lefts, rights) = (l::lefts, r::rights)
247||| 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)])
248unzip3 : (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)
249unzip3 [] = ([], [], [])
370unzip3 [] = ([], [], [])
250unzip3 ((l,c,r)::xs) with (unzip3 xs)
371unzip3 ((l,c,r)::xs) with (unzip3 xs)
@@ -286,6 +407,10 @@ implementation Functor (Vect n) where
287||| @ f the partial function (expressed by returning `Maybe`)
408||| @ f the partial function (expressed by returning `Maybe`)
288||| @ 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"])
289mapMaybe : (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)
290mapMaybe f [] = (_ ** [])
415mapMaybe f [] = (_ ** [])
291mapMaybe f (x::xs) =
416mapMaybe f (x::xs) =
@@ -294,7 +419,6 @@ mapMaybe f (x::xs) =
294 Just y => (S len ** y :: ys)
419 Just y => (S len ** y :: ys)
295 Nothing => ( len ** ys)
420 Nothing => ( len ** ys)
298--------------------------------------------------------------------------------
422--------------------------------------------------------------------------------
300--------------------------------------------------------------------------------
424--------------------------------------------------------------------------------
@@ -311,23 +435,41 @@ implementation Foldable (Vect n) where
311--------------------------------------------------------------------------------
435--------------------------------------------------------------------------------
313||| Flatten a vector of equal-length vectors
437||| Flatten a vector of equal-length vectors
440+||| concat [[1,2,3], [4,5,6]]
314concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem
442concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem
315concat [] = []
443concat [] = []
316concat (v::vs) = v ++ concat vs
444concat (v::vs) = v ++ concat vs
318||| Foldr without seeding the accumulator
446||| Foldr without seeding the accumulator
449+||| foldr1 (-) (fromList [1,2,3])
319foldr1 : (t -> t -> t) -> Vect (S n) t -> t
451foldr1 : (t -> t -> t) -> Vect (S n) t -> t
320−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))
322||| Foldl without seeding the accumulator
455||| Foldl without seeding the accumulator
458+||| foldl1 (-) (fromList [1,2,3])
323foldl1 : (t -> t -> t) -> Vect (S n) t -> t
460foldl1 : (t -> t -> t) -> Vect (S n) t -> t
324foldl1 f (x::xs) = foldl f x xs
461foldl1 f (x::xs) = foldl f x xs
325--------------------------------------------------------------------------------
463--------------------------------------------------------------------------------
327--------------------------------------------------------------------------------
465--------------------------------------------------------------------------------
329||| 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
330||| accumulator states in the form of a vector.
468||| accumulator states in the form of a vector.
471+||| scanl (-) 0 (fromList [1,2,3])
331scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res
473scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res
332scanl f q [] = [q]
474scanl f q [] = [q]
333scanl f q (x::xs) = q :: scanl f (f q x) xs
475scanl f q (x::xs) = q :: scanl f (f q x) xs
@@ -336,6 +478,10 @@ scanl f q (x::xs) = q :: scanl f (f q x) xs
336||| starting value.
478||| starting value.
337||| 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
338||| starts the fold with the element following it.
480||| starts the fold with the element following it.
483+||| scanl1 (-) (fromList [1,2,3])
339scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem
485scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem
340scanl1 f [] = []
486scanl1 f [] = []
341scanl1 f (x::xs) = scanl f x xs
487scanl1 f (x::xs) = scanl f x xs
@@ -348,6 +494,10 @@ scanl1 f (x::xs) = scanl f x xs
348||| @ p the equality test
494||| @ p the equality test
349||| @ e the item to search for
495||| @ e the item to search for
350||| @ xs the vector to search in
496||| @ xs the vector to search in
499+||| elemBy (==) 2 [1,2,3,4]
351elemBy : (p : elem -> elem -> Bool) -> (e : elem) -> (xs : Vect len elem) -> Bool
501elemBy : (p : elem -> elem -> Bool) -> (e : elem) -> (xs : Vect len elem) -> Bool
352elemBy p e [] = False
502elemBy p e [] = False
353elemBy p e (x::xs) = p e x || elemBy p e xs
503elemBy p e (x::xs) = p e x || elemBy p e xs
@@ -355,17 +505,29 @@ elemBy p e (x::xs) = p e x || elemBy p e xs
355||| 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
356||| @ x what to search for
506||| @ x what to search for
357||| @ xs where to search
507||| @ xs where to search
358elem : Eq elem => (x : elem) -> (xs : Vect len elem) -> Bool
512elem : Eq elem => (x : elem) -> (xs : Vect len elem) -> Bool
359elem = elemBy (==)
513elem = elemBy (==)
361||| Find the association of some key with a user-provided comparison
515||| Find the association of some key with a user-provided comparison
362||| @ p the comparison operator for keys (True if they match)
516||| @ p the comparison operator for keys (True if they match)
363||| @ e the key to look for
517||| @ e the key to look for
520+||| lookupBy (==) 2 [(1, 'a'), (2, 'b'), (3, 'c')]
364lookupBy : (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
365lookupBy p e [] = Nothing
523lookupBy p e [] = Nothing
366lookupBy 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
368||| 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')]
369lookup : Eq key => key -> Vect n (key, val) -> Maybe val
531lookup : Eq key => key -> Vect n (key, val) -> Maybe val
370lookup = lookupBy (==)
532lookup = lookupBy (==)
@@ -373,11 +535,19 @@ lookup = lookupBy (==)
373||| @ p the comparison operator
535||| @ p the comparison operator
374||| @ elems the vector to search
536||| @ elems the vector to search
375||| @ xs what to search for
537||| @ xs what to search for
540+||| hasAnyBy (==) [2,5] [1,2,3,4]
376hasAnyBy : (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
377hasAnyBy p elems [] = False
543hasAnyBy p elems [] = False
378hasAnyBy 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
380||| 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]
381hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool
551hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool
382hasAny = hasAnyBy (==)
552hasAny = hasAnyBy (==)
@@ -387,30 +557,62 @@ hasAny = hasAnyBy (==)
388||| Find the first element of the vector that satisfies some test
558||| Find the first element of the vector that satisfies some test
389||| @ p the test to satisfy
559||| @ p the test to satisfy
562+||| find (== 3) [1,2,3,4]
390find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem
564find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem
391find p [] = Nothing
565find p [] = Nothing
392find 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
394||| 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]
395findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)
573findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)
396findIndex p [] = Nothing
574findIndex p [] = Nothing
397findIndex 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)
399||| 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]
400findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)
582findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)
401findIndices p [] = []
583findIndices p [] = []
402findIndices p (x :: xs) = let is = map FS $ findIndices p xs
584findIndices p (x :: xs) = let is = map FS $ findIndices p xs
403 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]
405elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)
592elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)
406elemIndexBy 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]
408elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)
600elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)
409elemIndex = elemIndexBy (==)
601elemIndex = elemIndexBy (==)
603+||| Find the indices of all elements that satisfy some test
606+||| elemIndicesBy (<=) 3 [1,2,3,4]
411elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)
608elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)
412elemIndicesBy 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]
414elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
616elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
415elemIndices = elemIndicesBy (==)
617elemIndices = elemIndicesBy (==)
@@ -419,6 +621,10 @@ elemIndices = elemIndicesBy (==)
419--------------------------------------------------------------------------------
621--------------------------------------------------------------------------------
421||| 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])
422filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
628filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
423filter p [] = ( _ ** [] )
629filter p [] = ( _ ** [] )
424filter p (x::xs) =
630filter p (x::xs) =
@@ -429,6 +635,10 @@ filter p (x::xs) =
429 (_ ** tail)
635 (_ ** tail)
431||| 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])
432nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
642nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
433nubBy = nubBy' []
643nubBy = nubBy' []
@@ -440,15 +650,29 @@ nubBy = nubBy' []
440 | (_ ** tail) = (_ ** x::tail)
650 | (_ ** tail) = (_ ** x::tail)
442||| 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])
443nub : Eq elem => Vect len elem -> (p ** Vect p elem)
657nub : Eq elem => Vect len elem -> (p ** Vect p elem)
444nub = nubBy (==)
658nub = nubBy (==)
660+||| Delete first element from list according to some test
663+||| deleteBy (<) 3 (fromList [1,2,2,3,4,4])
446deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem)
665deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem)
447deleteBy _ _ [] = (_ ** [])
666deleteBy _ _ [] = (_ ** [])
448deleteBy eq x (y::ys) =
667deleteBy eq x (y::ys) =
449 let (len ** zs) = deleteBy eq x ys
668 let (len ** zs) = deleteBy eq x ys
450 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])
452delete : (Eq elem) => elem -> Vect len elem -> (p ** Vect p elem)
676delete : (Eq elem) => elem -> Vect len elem -> (p ** Vect p elem)
453delete = deleteBy (==)
677delete = deleteBy (==)
@@ -456,14 +680,28 @@ delete = deleteBy (==)
456-- Splitting and breaking lists
680-- Splitting and breaking lists
457--------------------------------------------------------------------------------
681--------------------------------------------------------------------------------
459−||| 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
460−||| 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.
461−||| 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.
462||| @ n the index to split at
688||| @ n the index to split at
463−||| @ xs the Vect to split in two
689+||| @ xs the `Vect` to split in two
692+||| splitAt 2 (fromList [1,2,3,4])
464splitAt : (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)
465−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])
467partition : (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))
468partition p [] = ((_ ** []), (_ ** []))
706partition p [] = ((_ ** []), (_ ** []))
469partition p (x::xs) =
707partition p (x::xs) =
@@ -477,17 +715,37 @@ partition p (x::xs) =
477-- Predicates
715-- Predicates
478--------------------------------------------------------------------------------
716--------------------------------------------------------------------------------
718+||| Verify vector prefix
721+||| isPrefixOfBy (==) (fromList [1,2]) (fromList [1,2,3,4])
480isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
723isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
481isPrefixOfBy p [] right = True
724isPrefixOfBy p [] right = True
482isPrefixOfBy p left [] = False
725isPrefixOfBy p left [] = False
483isPrefixOfBy 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])
485isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
733isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
486isPrefixOf = isPrefixOfBy (==)
734isPrefixOf = isPrefixOfBy (==)
736+||| Verify vector suffix
739+||| isSuffixOfBy (==) (fromList [3,4]) (fromList [1,2,3,4])
488isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
741isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
489isSuffixOfBy 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])
491isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
749isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
492isSuffixOf = isSuffixOfBy (==)
750isSuffixOf = isSuffixOfBy (==)
@@ -495,10 +753,20 @@ isSuffixOf = isSuffixOfBy (==)
495-- Conversions
753-- Conversions
496--------------------------------------------------------------------------------
754--------------------------------------------------------------------------------
756+||| Convert Maybe type into Vect
759+||| maybeToVect (Just 2)
498maybeToVect : Maybe elem -> (p ** Vect p elem)
761maybeToVect : Maybe elem -> (p ** Vect p elem)
499maybeToVect Nothing = (_ ** [])
762maybeToVect Nothing = (_ ** [])
500maybeToVect (Just j) = (_ ** [j])
763maybeToVect (Just j) = (_ ** [j])
765+||| Convert first element of Vect (if exists) into Maybe.
502vectToMaybe : Vect len elem -> Maybe elem
770vectToMaybe : Vect len elem -> Maybe elem
503vectToMaybe [] = Nothing
771vectToMaybe [] = Nothing
504vectToMaybe (x::xs) = Just x
772vectToMaybe (x::xs) = Just x
@@ -507,6 +775,11 @@ vectToMaybe (x::xs) = Just x
508--------------------------------------------------------------------------------
776--------------------------------------------------------------------------------
778+||| Filter out Nothings from Vect
781+||| catMaybes [Just 1, Just 2, Nothing, Nothing, Just 5]
510catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem)
783catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem)
511catMaybes [] = (_ ** [])
784catMaybes [] = (_ ** [])
512catMaybes (Nothing::xs) = catMaybes xs
785catMaybes (Nothing::xs) = catMaybes xs
@@ -514,6 +787,11 @@ catMaybes ((Just j)::xs) =
514 let (_ ** tail) = catMaybes xs
787 let (_ ** tail) = catMaybes xs
515 in (_ ** j::tail)
788 in (_ ** j::tail)
790+||| Get diagonal elements
793+||| diag [[1,2,3], [4,5,6], [7,8,9]]
517diag : Vect len (Vect len elem) -> Vect len elem
795diag : Vect len (Vect len elem) -> Vect len elem
518diag [] = []
796diag [] = []
519diag ((x::xs)::xss) = x :: diag (map tail xss)
797diag ((x::xs)::xss) = x :: diag (map tail xss)
@@ -522,12 +800,18 @@ range : {len : Nat} -> Vect len (Fin len)
522range {len=Z} = []
800range {len=Z} = []
523range {len=S _} = FZ :: map FS range
801range {len=S _} = FZ :: map FS range
525−||| 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`).
527||| 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`.
810+||| transpose [[1,2], [3,4], [5,6], [7,8]]
528−transpose : {n : Nat} -> Vect m (Vect n elem) -> Vect n (Vect m elem)
812+transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)
529−transpose [] = replicate _ []
813+transpose [] = replicate _ [] -- = [| [] |]
530−transpose (x :: xs) = zipWith (::) x (transpose xs)
814+transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]
532--------------------------------------------------------------------------------
816--------------------------------------------------------------------------------
533-- Applicative/Monad/Traversable
817-- Applicative/Monad/Traversable
@@ -535,7 +819,6 @@ transpose (x :: xs) = zipWith (::) x (transpose xs)
536implementation Applicative (Vect k) where
820implementation Applicative (Vect k) where
537 pure = replicate _
821 pure = replicate _
539 fs <*> vs = zipWith apply fs vs
822 fs <*> vs = zipWith apply fs vs
541||| This monad is different from the List monad, (>>=)
824||| This monad is different from the List monad, (>>=)
@@ -544,8 +827,8 @@ implementation Monad (Vect len) where
544 m >>= f = diag (map f m)
827 m >>= f = diag (map f m)
546implementation Traversable (Vect n) where
829implementation Traversable (Vect n) where
547− traverse f [] = pure Vect.Nil
830+ traverse f [] = [| [] |]
548− traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
831+ traverse f (x :: xs) = [| f x :: traverse f xs |]
550--------------------------------------------------------------------------------
833--------------------------------------------------------------------------------
@@ -554,13 +837,29 @@ implementation Traversable (Vect n) where
554implementation Show elem => Show (Vect len elem) where
837implementation Show elem => Show (Vect len elem) where
555 show = show . toList
838 show = show . toList
840+--------------------------------------------------------------------------------
842+--------------------------------------------------------------------------------
844+Uninhabited a => Uninhabited (Vect (S n) a) where
845+ uninhabited (x :: _) = uninhabited x
557--------------------------------------------------------------------------------
847--------------------------------------------------------------------------------
558-- Properties
848-- Properties
559--------------------------------------------------------------------------------
849--------------------------------------------------------------------------------
851+vectMustBeNil : (xs : Vect Z a) -> xs = []
852+vectMustBeNil [] = Refl
561vectConsCong : (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)
562vectConsCong 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
564vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
863vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
565vectNilRightNeutral [] = Refl
864vectNilRightNeutral [] = Refl
566vectNilRightNeutral (x :: xs) =
865vectNilRightNeutral (x :: xs) =
@@ -574,16 +873,93 @@ vectAppendAssociative [] y z = Refl
574vectAppendAssociative (x :: xs) ys zs =
873vectAppendAssociative (x :: xs) ys zs =
575 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
577--------------------------------------------------------------------------------
959--------------------------------------------------------------------------------
579--------------------------------------------------------------------------------
961--------------------------------------------------------------------------------
581−vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y
582−vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
584−vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys
585−vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
587implementation DecEq a => DecEq (Vect n a) where
963implementation DecEq a => DecEq (Vect n a) where
588 decEq [] [] = Yes Refl
964 decEq [] [] = Yes Refl
589 decEq (x :: xs) (y :: ys) with (decEq x y)
965 decEq (x :: xs) (y :: ys) with (decEq x y)