@@ -24,43 +24,65 @@ infixr 7 ::
25--------------------------------------------------------------------------------
25--------------------------------------------------------------------------------
27+||| Calculate the length of a `Vect`.
29+||| **Note**: this is only useful if you don't already statically know the length
30+||| and you want to avoid matching the implicit argument for erasure reasons.
31+||| @ n the length (provably equal to the return value)
27−length : Vect n a -> Nat
33+length : (xs : Vect n a) -> Nat
28length [] = 0
34length [] = 0
29length (x::xs) = 1 + length xs
35length (x::xs) = 1 + length xs
37+||| Show that the length function on vectors in fact calculates the length
38+private lengthCorrect : (n : Nat) -> (xs : Vect n a) -> length xs = n
39+lengthCorrect Z [] = refl
40+lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in refl
31--------------------------------------------------------------------------------
42--------------------------------------------------------------------------------
32-- Indexing into vectors
43-- Indexing into vectors
33--------------------------------------------------------------------------------
44--------------------------------------------------------------------------------
46+||| All but the first element of the vector
35tail : Vect (S n) a -> Vect n a
47tail : Vect (S n) a -> Vect n a
36tail (x::xs) = xs
48tail (x::xs) = xs
50+||| Only the first element of the vector
38head : Vect (S n) a -> a
51head : Vect (S n) a -> a
39head (x::xs) = x
52head (x::xs) = x
54+||| The last element of the vector
41last : Vect (S n) a -> a
55last : Vect (S n) a -> a
42last (x::[]) = x
56last (x::[]) = x
43last (x::y::ys) = last $ y::ys
57last (x::y::ys) = last $ y::ys
59+||| All but the last element of the vector
45init : Vect (S n) a -> Vect n a
60init : Vect (S n) a -> Vect n a
46init (x::[]) = []
61init (x::[]) = []
47init (x::y::ys) = x :: init (y::ys)
62init (x::y::ys) = x :: init (y::ys)
64+||| Extract a particular element from a vector
49index : Fin n -> Vect n a -> a
65index : Fin n -> Vect n a -> a
50index fZ (x::xs) = x
66index fZ (x::xs) = x
51index (fS k) (x::xs) = index k xs
67index (fS k) (x::xs) = index k xs
52index fZ [] impossible
68index fZ [] impossible
70+||| Construct a new vector consisting of all but the indicated element
54deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a
71deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a
55deleteAt fZ (x::xs) = xs
72deleteAt fZ (x::xs) = xs
56deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs
73deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs
57deleteAt _ [] impossible
74deleteAt _ [] impossible
76+||| Replace an element at a particlar index with another
59replaceAt : Fin n -> t -> Vect n t -> Vect n t
77replaceAt : Fin n -> t -> Vect n t -> Vect n t
60replaceAt fZ y (x::xs) = y :: xs
78replaceAt fZ y (x::xs) = y :: xs
61replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs
79replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs
81+||| Replace the element at a particular index with the result of applying a function to it
82+||| @ i the index to replace at
83+||| @ f the update function
84+||| @ xs the vector to replace in
63−updateAt : Fin n -> (t -> t) -> Vect n t -> Vect n t
85+updateAt : (i : Fin n) -> (f : t -> t) -> (xs : Vect n t) -> Vect n t
64updateAt fZ f (x::xs) = f x :: xs
86updateAt fZ f (x::xs) = f x :: xs
65updateAt (fS k) f (x::xs) = x :: updateAt k f xs
87updateAt (fS k) f (x::xs) = x :: updateAt k f xs
@@ -68,11 +90,15 @@ updateAt (fS k) f (x::xs) = x :: updateAt k f xs
68-- Subvectors
90-- Subvectors
69--------------------------------------------------------------------------------
91--------------------------------------------------------------------------------
93+||| Get the first m elements of a Vect
94+||| @ m the number of elements to take
71take : {n : Nat} -> (m : Fin (S n)) -> Vect n a -> Vect (cast m) a
95take : {n : Nat} -> (m : Fin (S n)) -> Vect n a -> Vect (cast m) a
72take (fS k) [] = FinZElim k
96take (fS k) [] = FinZElim k
73take fZ _ = []
97take fZ _ = []
74take (fS k) (x::xs) = x :: take k xs
98take (fS k) (x::xs) = x :: take k xs
100+||| Remove the first m elements of a Vect
101+||| @ m the number of elements to remove
76drop : (m : Fin (S n)) -> Vect n a -> Vect (n - cast m) a
102drop : (m : Fin (S n)) -> Vect n a -> Vect (n - cast m) a
77drop (fS k) [] = FinZElim k
103drop (fS k) [] = FinZElim k
78drop fZ xs ?= xs
104drop fZ xs ?= xs
@@ -82,10 +108,11 @@ drop (fS k) (x::xs) = drop k xs
82-- Transformations
108-- Transformations
83--------------------------------------------------------------------------------
109--------------------------------------------------------------------------------
111+||| Reverse the order of the elements of a vector
85total reverse : {n : Nat} -> Vect n a -> Vect n a
112total reverse : {n : Nat} -> Vect n a -> Vect n a
86reverse {n} xs = reverse' [] (plusZeroRightNeutral n) xs
113reverse {n} xs = reverse' [] (plusZeroRightNeutral n) xs
88− total reverse' : {m, j, l : Nat} ->
115+ total reverse' : {m, j, l : Nat} ->
89 Vect m a -> (j + m = l) -> Vect j a -> Vect l a
116 Vect m a -> (j + m = l) -> Vect j a -> Vect l a
90 reverse' {m} {j = Z } {l} acc prf [] ?= acc
117 reverse' {m} {j = Z } {l} acc prf [] ?= acc
91 reverse' {m} {j = S k} {l} acc prf (x::xs) =
118 reverse' {m} {j = S k} {l} acc prf (x::xs) =
@@ -95,7 +122,10 @@ reverse {n} xs = reverse' [] (plusZeroRightNeutral n) xs
95 let prf4 : (k + (S m) = l) = rewrite sym $ plusSuccRightSucc k m in prf3 in
122 let prf4 : (k + (S m) = l) = rewrite sym $ plusSuccRightSucc k m in prf3 in
96 reverse' (x::acc) prf4 xs
123 reverse' (x::acc) prf4 xs
125+||| Alternate an element between the other elements of a vector
126+||| @ sep the element to intersperse
127+||| @ xs the vector to separate with `sep`
98−intersperse : a -> Vect n a -> Vect (n + pred n) a
128+intersperse : (sep : a) -> (xs : Vect n a) -> Vect (n + pred n) a
99intersperse sep [] = []
129intersperse sep [] = []
100intersperse sep (x::xs) = x :: intersperse' sep xs
130intersperse sep (x::xs) = x :: intersperse' sep xs
@@ -115,7 +145,9 @@ fromList' {n} ys (x::xs) =
115 Vect (plus (length xs) (S n)) a in
145 Vect (plus (length xs) (S n)) a in
116 fromList' (x::ys) xs
146 fromList' (x::ys) xs
118−
148+||| Convert a list to a vector.
150+||| The length of the list should be statically known.
119fromList : (l : List a) -> Vect (length l) a
151fromList : (l : List a) -> Vect (length l) a
120fromList l =
152fromList l =
121 rewrite (sym $ plusZeroRightNeutral (length l)) in
153 rewrite (sym $ plusZeroRightNeutral (length l)) in
@@ -125,11 +157,15 @@ fromList l =
125-- Building (bigger) vectors
157-- Building (bigger) vectors
126--------------------------------------------------------------------------------
158--------------------------------------------------------------------------------
160+||| Append two vectors
128(++) : Vect m a -> Vect n a -> Vect (m + n) a
161(++) : Vect m a -> Vect n a -> Vect (m + n) a
129(++) [] ys = ys
162(++) [] ys = ys
130(++) (x::xs) ys = x :: xs ++ ys
163(++) (x::xs) ys = x :: xs ++ ys
165+||| Repeate some value n times
166+||| @ n the number of times to repeat it
167+||| @ x the value to repeat
132−replicate : (n : Nat) -> a -> Vect n a
168+replicate : (n : Nat) -> (x : a) -> Vect n a
133replicate Z x = []
169replicate Z x = []
134replicate (S k) x = x :: replicate k x
170replicate (S k) x = x :: replicate k x
@@ -137,18 +173,21 @@ replicate (S k) x = x :: replicate k x
137-- Zips and unzips
173-- Zips and unzips
138--------------------------------------------------------------------------------
174--------------------------------------------------------------------------------
176+||| Combine two equal-length vectors pairwise with some function
140zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
177zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
141zipWith f [] [] = []
178zipWith f [] [] = []
142zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
179zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
181+||| Combine two equal-length vectors pairwise
144zip : Vect n a -> Vect n b -> Vect n (a, b)
182zip : Vect n a -> Vect n b -> Vect n (a, b)
145zip = zipWith (\x => \y => (x,y))
183zip = zipWith (\x => \y => (x,y))
185+||| Convert a vector of pairs to a pair of vectors
147unzip : Vect n (a, b) -> (Vect n a, Vect n b)
186unzip : Vect n (a, b) -> (Vect n a, Vect n b)
148unzip [] = ([], [])
187unzip [] = ([], [])
149unzip ((l, r)::xs) with (unzip xs)
188unzip ((l, r)::xs) with (unzip xs)
150 | (lefts, rights) = (l::lefts, r::rights)
189 | (lefts, rights) = (l::lefts, r::rights)
152--------------------------------------------------------------------------------
191--------------------------------------------------------------------------------
153-- Equality
192-- Equality
154--------------------------------------------------------------------------------
193--------------------------------------------------------------------------------
@@ -208,6 +247,7 @@ instance Foldable (Vect n) where
208-- Special folds
247-- Special folds
209--------------------------------------------------------------------------------
248--------------------------------------------------------------------------------
250+||| Flatten a vector of equal-length vectors
211concat : Vect m (Vect n a) -> Vect (m * n) a
251concat : Vect m (Vect n a) -> Vect (m * n) a
212concat [] = []
252concat [] = []
213concat (v::vs) = v ++ concat vs
253concat (v::vs) = v ++ concat vs
@@ -216,30 +256,46 @@ concat (v::vs) = v ++ concat vs
216-- Membership tests
256-- Membership tests
217--------------------------------------------------------------------------------
257--------------------------------------------------------------------------------
259+||| Search for an item using a user-provided test
260+||| @ p the equality test
261+||| @ e the item to search for
262+||| @ xs the vector to search in
219−elemBy : (a -> a -> Bool) -> a -> Vect n a -> Bool
263+elemBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n a) -> Bool
220elemBy p e [] = False
264elemBy p e [] = False
221elemBy p e (x::xs) with (p e x)
265elemBy p e (x::xs) with (p e x)
222 | True = True
266 | True = True
223 | False = elemBy p e xs
267 | False = elemBy p e xs
269+||| Use the default Boolean equality on elements to search for an item
270+||| @ x what to search for
271+||| @ xs where to search
225−elem : Eq a => a -> Vect n a -> Bool
272+elem : Eq a => (x : a) -> (xs : Vect n a) -> Bool
226elem = elemBy (==)
273elem = elemBy (==)
275+||| Find the association of some key with a user-provided comparison
276+||| @ p the comparison operator for keys (True if they match)
277+||| @ e the key to look for
228−lookupBy : (a -> a -> Bool) -> a -> Vect n (a, b) -> Maybe b
278+lookupBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n (a, b)) -> Maybe b
229lookupBy p e [] = Nothing
279lookupBy p e [] = Nothing
230lookupBy p e ((l, r)::xs) with (p e l)
280lookupBy p e ((l, r)::xs) with (p e l)
231 | True = Just r
281 | True = Just r
232 | False = lookupBy p e xs
282 | False = lookupBy p e xs
284+||| Find the assocation of some key using the default Boolean equality test
234lookup : Eq a => a -> Vect n (a, b) -> Maybe b
285lookup : Eq a => a -> Vect n (a, b) -> Maybe b
235lookup = lookupBy (==)
286lookup = lookupBy (==)
288+||| Check if any element of xs is found in elems by a user-provided comparison
289+||| @ p the comparison operator
290+||| @ elems the vector to search
291+||| @ xs what to search for
237−hasAnyBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool
292+hasAnyBy : (p : a -> a -> Bool) -> (elems : Vect m a) -> (xs : Vect n a) -> Bool
238hasAnyBy p elems [] = False
293hasAnyBy p elems [] = False
239hasAnyBy p elems (x::xs) with (elemBy p x elems)
294hasAnyBy p elems (x::xs) with (elemBy p x elems)
240 | True = True
295 | True = True
241 | False = hasAnyBy p elems xs
296 | False = hasAnyBy p elems xs
298+||| Check if any element of xs is found in elems using the default Boolean equality test
243hasAny : Eq a => Vect m a -> Vect n a -> Bool
299hasAny : Eq a => Vect m a -> Vect n a -> Bool
244hasAny = hasAnyBy (==)
300hasAny = hasAnyBy (==)
@@ -247,12 +303,15 @@ hasAny = hasAnyBy (==)
247-- Searching with a predicate
303-- Searching with a predicate
248--------------------------------------------------------------------------------
304--------------------------------------------------------------------------------
306+||| Find the first element of the vector that satisfies some test
307+||| @ p the test to satisfy
250−find : (a -> Bool) -> Vect n a -> Maybe a
308+find : (p : a -> Bool) -> (xs : Vect n a) -> Maybe a
251find p [] = Nothing
309find p [] = Nothing
252find p (x::xs) with (p x)
310find p (x::xs) with (p x)
253 | True = Just x
311 | True = Just x
254 | False = find p xs
312 | False = find p xs
314+||| Find the index of the first element of the vector that satisfies some test
256findIndex : (a -> Bool) -> Vect n a -> Maybe Nat
315findIndex : (a -> Bool) -> Vect n a -> Maybe Nat
257findIndex = findIndex' 0
316findIndex = findIndex' 0
@@ -262,6 +321,7 @@ findIndex = findIndex' 0
262 | True = Just cnt
321 | True = Just cnt
263 | False = findIndex' (S cnt) p xs
322 | False = findIndex' (S cnt) p xs
324+||| Find the indices of all elements that satisfy some test
265total findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
325total findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
266findIndices = findIndices' 0
326findIndices = findIndices' 0
@@ -290,6 +350,7 @@ elemIndices = elemIndicesBy (==)
290-- Filters
350-- Filters
291--------------------------------------------------------------------------------
351--------------------------------------------------------------------------------
353+||| Find all elements of a vector that satisfy some test
293total filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
354total filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
294filter p [] = ( _ ** [] )
355filter p [] = ( _ ** [] )
295filter p (x::xs) with (filter p xs)
356filter p (x::xs) with (filter p xs)
@@ -299,6 +360,7 @@ filter p (x::xs) with (filter p xs)
300 (_ ** tail)
361 (_ ** tail)
363+||| Make the elements of some vector unique by some test
302nubBy : (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)
364nubBy : (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)
303nubBy = nubBy' []
365nubBy = nubBy' []
@@ -309,6 +371,7 @@ nubBy = nubBy' []
309 | False with (nubBy' (x::acc) p xs)
371 | False with (nubBy' (x::acc) p xs)
310 | (_ ** tail) = (_ ** x::tail)
372 | (_ ** tail) = (_ ** x::tail)
374+||| Make the elements of some vector unique by the default Boolean equality
312nub : Eq a => Vect n a -> (p ** Vect p a)
375nub : Eq a => Vect n a -> (p ** Vect p a)
313nub = nubBy (==)
376nub = nubBy (==)