@@ -24,43 +24,65 @@ infixr 7 ::
2424-- Length
2525--------------------------------------------------------------------------------
2626
27−length : Vect n a -> Nat
27+||| Calculate the length of a `Vect`.
28+|||
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)
32+||| @ xs the vector
33+length : (xs : Vect n a) -> Nat
2834length [] = 0
2935length (x::xs) = 1 + length xs
3036
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
41+
3142--------------------------------------------------------------------------------
3243-- Indexing into vectors
3344--------------------------------------------------------------------------------
3445
46+||| All but the first element of the vector
3547tail : Vect (S n) a -> Vect n a
3648tail (x::xs) = xs
3749
50+||| Only the first element of the vector
3851head : Vect (S n) a -> a
3952head (x::xs) = x
4053
54+||| The last element of the vector
4155last : Vect (S n) a -> a
4256last (x::[]) = x
4357last (x::y::ys) = last $ y::ys
4458
59+||| All but the last element of the vector
4560init : Vect (S n) a -> Vect n a
4661init (x::[]) = []
4762init (x::y::ys) = x :: init (y::ys)
4863
64+||| Extract a particular element from a vector
4965index : Fin n -> Vect n a -> a
5066index fZ (x::xs) = x
5167index (fS k) (x::xs) = index k xs
5268index fZ [] impossible
5369
70+||| Construct a new vector consisting of all but the indicated element
5471deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a
5572deleteAt fZ (x::xs) = xs
5673deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs
5774deleteAt _ [] impossible
5875
76+||| Replace an element at a particlar index with another
5977replaceAt : Fin n -> t -> Vect n t -> Vect n t
6078replaceAt fZ y (x::xs) = y :: xs
6179replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs
6280
63−updateAt : Fin n -> (t -> t) -> Vect n t -> Vect n t
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
85+updateAt : (i : Fin n) -> (f : t -> t) -> (xs : Vect n t) -> Vect n t
6486updateAt fZ f (x::xs) = f x :: xs
6587updateAt (fS k) f (x::xs) = x :: updateAt k f xs
6688
@@ -68,11 +90,15 @@ updateAt (fS k) f (x::xs) = x :: updateAt k f xs
6890-- Subvectors
6991--------------------------------------------------------------------------------
7092
93+||| Get the first m elements of a Vect
94+||| @ m the number of elements to take
7195take : {n : Nat} -> (m : Fin (S n)) -> Vect n a -> Vect (cast m) a
7296take (fS k) [] = FinZElim k
7397take fZ _ = []
7498take (fS k) (x::xs) = x :: take k xs
7599
100+||| Remove the first m elements of a Vect
101+||| @ m the number of elements to remove
76102drop : (m : Fin (S n)) -> Vect n a -> Vect (n - cast m) a
77103drop (fS k) [] = FinZElim k
78104drop fZ xs ?= xs
@@ -82,10 +108,11 @@ drop (fS k) (x::xs) = drop k xs
82108-- Transformations
83109--------------------------------------------------------------------------------
84110
111+||| Reverse the order of the elements of a vector
85112total reverse : {n : Nat} -> Vect n a -> Vect n a
86113reverse {n} xs = reverse' [] (plusZeroRightNeutral n) xs
87114 where
88− total reverse' : {m, j, l : Nat} ->
115+ total reverse' : {m, j, l : Nat} ->
89116 Vect m a -> (j + m = l) -> Vect j a -> Vect l a
90117 reverse' {m} {j = Z } {l} acc prf [] ?= acc
91118 reverse' {m} {j = S k} {l} acc prf (x::xs) =
@@ -95,7 +122,10 @@ reverse {n} xs = reverse' [] (plusZeroRightNeutral n) xs
95122 let prf4 : (k + (S m) = l) = rewrite sym $ plusSuccRightSucc k m in prf3 in
96123 reverse' (x::acc) prf4 xs
97124
98−intersperse : a -> Vect n a -> Vect (n + pred n) a
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`
128+intersperse : (sep : a) -> (xs : Vect n a) -> Vect (n + pred n) a
99129intersperse sep [] = []
100130intersperse sep (x::xs) = x :: intersperse' sep xs
101131 where
@@ -115,7 +145,9 @@ fromList' {n} ys (x::xs) =
115145 Vect (plus (length xs) (S n)) a in
116146 fromList' (x::ys) xs
117147
118−
148+||| Convert a list to a vector.
149+|||
150+||| The length of the list should be statically known.
119151fromList : (l : List a) -> Vect (length l) a
120152fromList l =
121153 rewrite (sym $ plusZeroRightNeutral (length l)) in
@@ -125,11 +157,15 @@ fromList l =
125157-- Building (bigger) vectors
126158--------------------------------------------------------------------------------
127159
160+||| Append two vectors
128161(++) : Vect m a -> Vect n a -> Vect (m + n) a
129162(++) [] ys = ys
130163(++) (x::xs) ys = x :: xs ++ ys
131164
132−replicate : (n : Nat) -> a -> Vect n a
165+||| Repeate some value n times
166+||| @ n the number of times to repeat it
167+||| @ x the value to repeat
168+replicate : (n : Nat) -> (x : a) -> Vect n a
133169replicate Z x = []
134170replicate (S k) x = x :: replicate k x
135171
@@ -137,18 +173,21 @@ replicate (S k) x = x :: replicate k x
137173-- Zips and unzips
138174--------------------------------------------------------------------------------
139175
176+||| Combine two equal-length vectors pairwise with some function
140177zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
141178zipWith f [] [] = []
142179zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
143180
181+||| Combine two equal-length vectors pairwise
144182zip : Vect n a -> Vect n b -> Vect n (a, b)
145183zip = zipWith (\x => \y => (x,y))
146184
185+||| Convert a vector of pairs to a pair of vectors
147186unzip : Vect n (a, b) -> (Vect n a, Vect n b)
148187unzip [] = ([], [])
149188unzip ((l, r)::xs) with (unzip xs)
150189 | (lefts, rights) = (l::lefts, r::rights)
151−
190+
152191--------------------------------------------------------------------------------
153192-- Equality
154193--------------------------------------------------------------------------------
@@ -208,6 +247,7 @@ instance Foldable (Vect n) where
208247-- Special folds
209248--------------------------------------------------------------------------------
210249
250+||| Flatten a vector of equal-length vectors
211251concat : Vect m (Vect n a) -> Vect (m * n) a
212252concat [] = []
213253concat (v::vs) = v ++ concat vs
@@ -216,30 +256,46 @@ concat (v::vs) = v ++ concat vs
216256-- Membership tests
217257--------------------------------------------------------------------------------
218258
219−elemBy : (a -> a -> Bool) -> a -> Vect n a -> Bool
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
263+elemBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n a) -> Bool
220264elemBy p e [] = False
221265elemBy p e (x::xs) with (p e x)
222266 | True = True
223267 | False = elemBy p e xs
224268
225−elem : Eq a => a -> Vect n a -> Bool
269+||| Use the default Boolean equality on elements to search for an item
270+||| @ x what to search for
271+||| @ xs where to search
272+elem : Eq a => (x : a) -> (xs : Vect n a) -> Bool
226273elem = elemBy (==)
227274
228−lookupBy : (a -> a -> Bool) -> a -> Vect n (a, b) -> Maybe b
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
278+lookupBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n (a, b)) -> Maybe b
229279lookupBy p e [] = Nothing
230280lookupBy p e ((l, r)::xs) with (p e l)
231281 | True = Just r
232282 | False = lookupBy p e xs
233283
284+||| Find the assocation of some key using the default Boolean equality test
234285lookup : Eq a => a -> Vect n (a, b) -> Maybe b
235286lookup = lookupBy (==)
236287
237−hasAnyBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool
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
292+hasAnyBy : (p : a -> a -> Bool) -> (elems : Vect m a) -> (xs : Vect n a) -> Bool
238293hasAnyBy p elems [] = False
239294hasAnyBy p elems (x::xs) with (elemBy p x elems)
240295 | True = True
241296 | False = hasAnyBy p elems xs
242297
298+||| Check if any element of xs is found in elems using the default Boolean equality test
243299hasAny : Eq a => Vect m a -> Vect n a -> Bool
244300hasAny = hasAnyBy (==)
245301
@@ -247,12 +303,15 @@ hasAny = hasAnyBy (==)
247303-- Searching with a predicate
248304--------------------------------------------------------------------------------
249305
250−find : (a -> Bool) -> Vect n a -> Maybe a
306+||| Find the first element of the vector that satisfies some test
307+||| @ p the test to satisfy
308+find : (p : a -> Bool) -> (xs : Vect n a) -> Maybe a
251309find p [] = Nothing
252310find p (x::xs) with (p x)
253311 | True = Just x
254312 | False = find p xs
255313
314+||| Find the index of the first element of the vector that satisfies some test
256315findIndex : (a -> Bool) -> Vect n a -> Maybe Nat
257316findIndex = findIndex' 0
258317 where
@@ -262,6 +321,7 @@ findIndex = findIndex' 0
262321 | True = Just cnt
263322 | False = findIndex' (S cnt) p xs
264323
324+||| Find the indices of all elements that satisfy some test
265325total findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
266326findIndices = findIndices' 0
267327 where
@@ -290,6 +350,7 @@ elemIndices = elemIndicesBy (==)
290350-- Filters
291351--------------------------------------------------------------------------------
292352
353+||| Find all elements of a vector that satisfy some test
293354total filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
294355filter p [] = ( _ ** [] )
295356filter p (x::xs) with (filter p xs)
@@ -299,6 +360,7 @@ filter p (x::xs) with (filter p xs)
299360 else
300361 (_ ** tail)
301362
363+||| Make the elements of some vector unique by some test
302364nubBy : (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)
303365nubBy = nubBy' []
304366 where
@@ -309,6 +371,7 @@ nubBy = nubBy' []
309371 | False with (nubBy' (x::acc) p xs)
310372 | (_ ** tail) = (_ ** x::tail)
311373
374+||| Make the elements of some vector unique by the default Boolean equality
312375nub : Eq a => Vect n a -> (p ** Vect p a)
313376nub = nubBy (==)
314377