@@ -9,13 +9,15 @@ import Language.Reflection
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
13+||| @ elem the type of elements
13−data Vect : Nat -> Type -> Type where
15+data Vect : (len : Nat) -> (elem : Type) -> Type where
14 ||| Empty vector
16 ||| Empty vector
15− Nil : Vect Z a
17+ Nil : Vect Z elem
16− ||| A non-empty vector of length `S k`, consisting of a head element and
18+ ||| A non-empty vector of length `S len`, consisting of a head element and
17− ||| the rest of the list, of length `k`.
19+ ||| the rest of the list, of length `len`.
18− (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a
20+ (::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem
20-- Hints for interactive editing
22-- Hints for interactive editing
21%name Vect xs,ys,zs,ws
23%name Vect xs,ys,zs,ws
@@ -28,14 +30,14 @@ data Vect : Nat -> Type -> Type where
29||| **Note**: this is only useful if you don't already statically know the length
31||| **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.
32||| and you want to avoid matching the implicit argument for erasure reasons.
31−||| @ n the length (provably equal to the return value)
33+||| @ len the length (provably equal to the return value)
32||| @ xs the vector
34||| @ xs the vector
33−length : (xs : Vect n a) -> Nat
35+length : (xs : Vect len elem) -> Nat
34length [] = 0
36length [] = 0
35length (x::xs) = 1 + length xs
37length (x::xs) = 1 + length xs
37||| Show that the length function on vectors in fact calculates the length
39||| Show that the length function on vectors in fact calculates the length
38−private lengthCorrect : (n : Nat) -> (xs : Vect n a) -> length xs = n
40+private lengthCorrect : (len : Nat) -> (xs : Vect len elem) -> length xs = len
39lengthCorrect Z [] = Refl
41lengthCorrect Z [] = Refl
40lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl
42lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl
@@ -44,44 +46,44 @@ lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl
44--------------------------------------------------------------------------------
46--------------------------------------------------------------------------------
46||| All but the first element of the vector
48||| All but the first element of the vector
47−tail : Vect (S n) a -> Vect n a
49+tail : Vect (S len) elem -> Vect len elem
48tail (x::xs) = xs
50tail (x::xs) = xs
50||| Only the first element of the vector
52||| Only the first element of the vector
51−head : Vect (S n) a -> a
53+head : Vect (S len) elem -> elem
52head (x::xs) = x
54head (x::xs) = x
54||| The last element of the vector
56||| The last element of the vector
55−last : Vect (S n) a -> a
57+last : Vect (S len) elem -> elem
56last (x::[]) = x
58last (x::[]) = x
57last (x::y::ys) = last $ y::ys
59last (x::y::ys) = last $ y::ys
59||| All but the last element of the vector
61||| All but the last element of the vector
60−init : Vect (S n) a -> Vect n a
62+init : Vect (S len) elem -> Vect len elem
61init (x::[]) = []
63init (x::[]) = []
62init (x::y::ys) = x :: init (y::ys)
64init (x::y::ys) = x :: init (y::ys)
64||| Extract a particular element from a vector
66||| Extract a particular element from a vector
65−index : Fin n -> Vect n a -> a
67+index : Fin len -> Vect len elem -> elem
66index FZ (x::xs) = x
68index FZ (x::xs) = x
67index (FS k) (x::xs) = index k xs
69index (FS k) (x::xs) = index k xs
70||| Insert an element at a particular index
72||| Insert an element at a particular index
71−insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a
73+insertAt : Fin (S len) -> elem -> Vect len elem -> Vect (S len) elem
72insertAt FZ y xs = y :: xs
74insertAt FZ y xs = y :: xs
73insertAt (FS k) y (x::xs) = x :: insertAt k y xs
75insertAt (FS k) y (x::xs) = x :: insertAt k y xs
74insertAt (FS k) y [] = absurd k
76insertAt (FS k) y [] = absurd k
76||| Construct a new vector consisting of all but the indicated element
78||| Construct a new vector consisting of all but the indicated element
77−deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a
79+deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem
78−deleteAt FZ (x::xs) = xs
80+deleteAt FZ (x::xs) = xs
79−deleteAt {n = S m} (FS k) (x::xs) = x :: deleteAt k xs
81+deleteAt {len = S m} (FS k) (x::xs) = x :: deleteAt k xs
80−deleteAt {n = Z} (FS k) (x::xs) = absurd k
82+deleteAt {len = Z} (FS k) (x::xs) = absurd k
81−deleteAt _ [] impossible
83+deleteAt _ [] impossible
83||| Replace an element at a particlar index with another
85||| Replace an element at a particlar index with another
84−replaceAt : Fin n -> t -> Vect n t -> Vect n t
86+replaceAt : Fin len -> elem -> Vect len elem -> Vect len elem
85replaceAt FZ y (x::xs) = y :: xs
87replaceAt FZ y (x::xs) = y :: xs
86replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
88replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
@@ -89,7 +91,7 @@ replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
89||| @ i the index to replace at
91||| @ i the index to replace at
90||| @ f the update function
92||| @ f the update function
91||| @ xs the vector to replace in
93||| @ xs the vector to replace in
92−updateAt : (i : Fin n) -> (f : t -> t) -> (xs : Vect n t) -> Vect n t
94+updateAt : (i : Fin len) -> (f : elem -> elem) -> (xs : Vect len elem) -> Vect len elem
93updateAt FZ f (x::xs) = f x :: xs
95updateAt FZ f (x::xs) = f x :: xs
94updateAt (FS k) f (x::xs) = x :: updateAt k f xs
96updateAt (FS k) f (x::xs) = x :: updateAt k f xs
@@ -99,13 +101,13 @@ updateAt (FS k) f (x::xs) = x :: updateAt k f xs
100||| Get the first n elements of a Vect
102||| Get the first n elements of a Vect
101||| @ n the number of elements to take
103||| @ n the number of elements to take
102−take : (n : Nat) -> Vect (n + m) a -> Vect n a
104+take : (n : Nat) -> Vect (n + m) elem -> Vect n elem
103take Z xs = []
105take Z xs = []
104take (S k) (x :: xs) = x :: take k xs
106take (S k) (x :: xs) = x :: take k xs
106||| Remove the first n elements of a Vect
108||| Remove the first n elements of a Vect
107||| @ n the number of elements to remove
109||| @ n the number of elements to remove
108−drop : (n : Nat) -> Vect (n + m) a -> Vect m a
110+drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
109drop Z xs = xs
111drop Z xs = xs
110drop (S k) (x :: xs) = drop k xs
112drop (S k) (x :: xs) = drop k xs
@@ -113,7 +115,7 @@ drop (S k) (x :: xs) = drop k xs
113||| Boolean predicate.
115||| Boolean predicate.
115||| @ p the predicate
117||| @ p the predicate
116−takeWhile : (p : a -> Bool) -> Vect n a -> (q ** Vect q a)
118+takeWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
117takeWhile p [] = (_ ** [])
119takeWhile p [] = (_ ** [])
118takeWhile p (x::xs) =
120takeWhile p (x::xs) =
119 let (len ** ys) = takeWhile p xs
121 let (len ** ys) = takeWhile p xs
@@ -126,7 +128,7 @@ takeWhile p (x::xs) =
126||| Boolean predicate.
128||| Boolean predicate.
128||| @ p the predicate
130||| @ p the predicate
129−dropWhile : (p : a -> Bool) -> Vect n a -> (q ** Vect q a)
131+dropWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
130dropWhile p [] = (_ ** [])
132dropWhile p [] = (_ ** [])
131dropWhile p (x::xs) =
133dropWhile p (x::xs) =
132 if p x then
134 if p x then
@@ -139,9 +141,9 @@ dropWhile p (x::xs) =
139--------------------------------------------------------------------------------
141--------------------------------------------------------------------------------
141||| Reverse the order of the elements of a vector
143||| Reverse the order of the elements of a vector
142−reverse : Vect n a -> Vect n a
144+reverse : Vect len elem -> Vect len elem
143reverse xs = go [] xs
145reverse xs = go [] xs
144− where go : Vect n a -> Vect m a -> Vect (n+m) a
146+ where go : Vect n elem -> Vect m elem -> Vect (n+m) elem
145 go {n} acc [] = rewrite plusZeroRightNeutral n in acc
147 go {n} acc [] = rewrite plusZeroRightNeutral n in acc
146 go {n} {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m
148 go {n} {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m
147 in go (x::acc) xs
149 in go (x::acc) xs
@@ -149,11 +151,11 @@ reverse xs = go [] xs
149||| Alternate an element between the other elements of a vector
151||| Alternate an element between the other elements of a vector
150||| @ sep the element to intersperse
152||| @ sep the element to intersperse
151||| @ xs the vector to separate with `sep`
153||| @ xs the vector to separate with `sep`
152−intersperse : (sep : a) -> (xs : Vect n a) -> Vect (n + pred n) a
154+intersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elem
153intersperse sep [] = []
155intersperse sep [] = []
154intersperse sep (x::xs) = x :: intersperse' sep xs
156intersperse sep (x::xs) = x :: intersperse' sep xs
156− intersperse' : a -> Vect n a -> Vect (n + n) a
158+ intersperse' : elem -> Vect n elem -> Vect (n + n) elem
157 intersperse' sep [] = []
159 intersperse' sep [] = []
158 intersperse' {n=S n} sep (x::xs) = rewrite sym $ plusSuccRightSucc n n
160 intersperse' {n=S n} sep (x::xs) = rewrite sym $ plusSuccRightSucc n n
159 in sep :: x :: intersperse' sep xs
161 in sep :: x :: intersperse' sep xs
@@ -163,17 +165,17 @@ intersperse sep (x::xs) = x :: intersperse' sep xs
163--------------------------------------------------------------------------------
165--------------------------------------------------------------------------------
166−fromList' : Vect n a -> (l : List a) -> Vect (length l + n) a
168+fromList' : Vect len elem -> (l : List elem) -> Vect (length l + len) elem
167fromList' ys [] = ys
169fromList' ys [] = ys
168−fromList' {n} ys (x::xs) =
170+fromList' {len} ys (x::xs) =
169− rewrite (plusSuccRightSucc (length xs) n) ==>
171+ rewrite (plusSuccRightSucc (length xs) len) ==>
170− Vect (plus (length xs) (S n)) a in
172+ Vect (plus (length xs) (S len)) elem in
171 fromList' (x::ys) xs
173 fromList' (x::ys) xs
173||| Convert a list to a vector.
175||| Convert a list to a vector.
175||| The length of the list should be statically known.
177||| The length of the list should be statically known.
176−fromList : (l : List a) -> Vect (length l) a
178+fromList : (l : List elem) -> Vect (length l) elem
177fromList l =
179fromList l =
178 rewrite (sym $ plusZeroRightNeutral (length l)) in
180 rewrite (sym $ plusZeroRightNeutral (length l)) in
179 reverse $ fromList' [] l
181 reverse $ fromList' [] l
@@ -183,30 +185,31 @@ fromList l =
183--------------------------------------------------------------------------------
185--------------------------------------------------------------------------------
185||| Append two vectors
187||| Append two vectors
186−(++) : Vect m a -> Vect n a -> Vect (m + n) a
188+(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem
187(++) [] ys = ys
189(++) [] ys = ys
188(++) (x::xs) ys = x :: xs ++ ys
190(++) (x::xs) ys = x :: xs ++ ys
190−||| Repeate some value n times
192+||| Repeate some value some number of times.
191−||| @ n the number of times to repeat it
194+||| @ len the number of times to repeat it
192||| @ x the value to repeat
195||| @ x the value to repeat
193−replicate : (n : Nat) -> (x : a) -> Vect n a
196+replicate : (len : Nat) -> (x : elem) -> Vect len elem
194replicate Z x = []
197replicate Z x = []
195replicate (S k) x = x :: replicate k x
198replicate (S k) x = x :: replicate k x
197||| Merge two ordered vectors
200||| Merge two ordered vectors
198−mergeBy : (a -> a -> Ordering) -> Vect n a -> Vect m a -> Vect (n + m) a
201+mergeBy : (elem -> elem -> Ordering) -> (xs : Vect n elem) -> (ys : Vect m elem) -> Vect (n + m) elem
199mergeBy order [] [] = []
202mergeBy order [] [] = []
200mergeBy order [] (x :: xs) = x :: xs
203mergeBy order [] (x :: xs) = x :: xs
201−mergeBy {n = S k} order (x :: xs) [] = rewrite plusZeroRightNeutral (S k) in
204+mergeBy {n = S k} order (x :: xs) [] = rewrite plusZeroRightNeutral (S k) in
203−mergeBy {n = S k} {m = S k'} order (x :: xs) (y :: ys)
206+mergeBy {n = S k} {m = S k'} order (x :: xs) (y :: ys)
204 = case order x y of
207 = case order x y of
205 LT => x :: mergeBy order xs (y :: ys)
208 LT => x :: mergeBy order xs (y :: ys)
206− _ => rewrite sym (plusSuccRightSucc k k') in
209+ _ => rewrite sym (plusSuccRightSucc k k') in
207 y :: mergeBy order (x :: xs) ys
210 y :: mergeBy order (x :: xs) ys
209−merge : Ord a => Vect n a -> Vect m a -> Vect (n + m) a
212+merge : Ord elem => Vect n elem -> Vect m elem -> Vect (n + m) elem
210merge = mergeBy compare
213merge = mergeBy compare
212--------------------------------------------------------------------------------
215--------------------------------------------------------------------------------
@@ -223,26 +226,26 @@ zipWith f [] [] = []
223zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
226zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
225||| Combine three equal-length vectors into a vector with some function
228||| Combine three equal-length vectors into a vector with some function
226−zipWith3 : (a -> b -> c -> d) -> Vect n a -> Vect n b -> Vect n c -> Vect n d
229+zipWith3 : (a -> b -> c -> d) -> (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n d
227zipWith3 f [] [] [] = []
230zipWith3 f [] [] [] = []
228zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
231zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
230||| Combine two equal-length vectors pairwise
233||| Combine two equal-length vectors pairwise
231−zip : Vect n a -> Vect n b -> Vect n (a, b)
234+zip : (xs : Vect n a) -> (ys : Vect n b) -> Vect n (a, b)
232zip = zipWith (\x,y => (x,y))
235zip = zipWith (\x,y => (x,y))
234||| Combine three equal-length vectors elementwise into a vector of tuples
237||| Combine three equal-length vectors elementwise into a vector of tuples
235−zip3 : Vect n a -> Vect n b -> Vect n c -> Vect n (a, b, c)
238+zip3 : (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n (a, b, c)
236zip3 = zipWith3 (\x,y,z => (x,y,z))
239zip3 = zipWith3 (\x,y,z => (x,y,z))
238||| Convert a vector of pairs to a pair of vectors
241||| Convert a vector of pairs to a pair of vectors
239−unzip : Vect n (a, b) -> (Vect n a, Vect n b)
242+unzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b)
240unzip [] = ([], [])
243unzip [] = ([], [])
241unzip ((l, r)::xs) with (unzip xs)
244unzip ((l, r)::xs) with (unzip xs)
242 | (lefts, rights) = (l::lefts, r::rights)
245 | (lefts, rights) = (l::lefts, r::rights)
244||| Convert a vector of three-tuples to a triplet of vectors
247||| Convert a vector of three-tuples to a triplet of vectors
245−unzip3 : Vect n (a, b, c) -> (Vect n a, Vect n b, Vect n c)
248+unzip3 : (xs : Vect n (a, b, c)) -> (Vect n a, Vect n b, Vect n c)
246unzip3 [] = ([], [], [])
249unzip3 [] = ([], [], [])
247unzip3 ((l,c,r)::xs) with (unzip3 xs)
250unzip3 ((l,c,r)::xs) with (unzip3 xs)
248 | (lefts, centers, rights) = (l::lefts, c::centers, r::rights)
251 | (lefts, centers, rights) = (l::lefts, c::centers, r::rights)
@@ -251,7 +254,7 @@ unzip3 ((l,c,r)::xs) with (unzip3 xs)
251-- Equality
254-- Equality
252--------------------------------------------------------------------------------
255--------------------------------------------------------------------------------
254−implementation (Eq a) => Eq (Vect n a) where
257+implementation (Eq elem) => Eq (Vect len elem) where
255 (==) [] [] = True
258 (==) [] [] = True
256 (==) (x::xs) (y::ys) = x == y && xs == ys
259 (==) (x::xs) (y::ys) = x == y && xs == ys
@@ -260,7 +263,7 @@ implementation (Eq a) => Eq (Vect n a) where
261--------------------------------------------------------------------------------
264--------------------------------------------------------------------------------
263−implementation Ord a => Ord (Vect n a) where
266+implementation Ord elem => Ord (Vect len elem) where
264 compare [] [] = EQ
267 compare [] [] = EQ
265 compare (x::xs) (y::ys) = compare x y `thenCompare` compare xs ys
268 compare (x::xs) (y::ys) = compare x y `thenCompare` compare xs ys
@@ -283,7 +286,7 @@ implementation Functor (Vect n) where
284||| @ f the partial function (expressed by returning `Maybe`)
287||| @ f the partial function (expressed by returning `Maybe`)
285||| @ xs the vector to check for results
288||| @ xs the vector to check for results
286−mapMaybe : (f : a -> Maybe b) -> (xs : Vect n a) -> (m : Nat ** Vect m b)
289+mapMaybe : (f : a -> Maybe b) -> (xs : Vect len a) -> (m : Nat ** Vect m b)
287mapMaybe f [] = (_ ** [])
290mapMaybe f [] = (_ ** [])
288mapMaybe f (x::xs) =
291mapMaybe f (x::xs) =
289 let (len ** ys) = mapMaybe f xs
292 let (len ** ys) = mapMaybe f xs
@@ -308,7 +311,7 @@ implementation Foldable (Vect n) where
308--------------------------------------------------------------------------------
311--------------------------------------------------------------------------------
310||| Flatten a vector of equal-length vectors
313||| Flatten a vector of equal-length vectors
311−concat : Vect m (Vect n a) -> Vect (m * n) a
314+concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem
312concat [] = []
315concat [] = []
313concat (v::vs) = v ++ concat vs
316concat (v::vs) = v ++ concat vs
@@ -323,7 +326,7 @@ foldl1 f (x::xs) = foldl f x xs
324--------------------------------------------------------------------------------
327--------------------------------------------------------------------------------
326−scanl : (b -> a -> b) -> b -> Vect n a -> Vect (S n) b
329+scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res
327scanl f q [] = [q]
330scanl f q [] = [q]
328scanl f q (x::xs) = q :: scanl f (f q x) xs
331scanl f q (x::xs) = q :: scanl f (f q x) xs
@@ -335,37 +338,37 @@ scanl f q (x::xs) = q :: scanl f (f q x) xs
335||| @ p the equality test
338||| @ p the equality test
336||| @ e the item to search for
339||| @ e the item to search for
337||| @ xs the vector to search in
340||| @ xs the vector to search in
338−elemBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n a) -> Bool
341+elemBy : (p : elem -> elem -> Bool) -> (e : elem) -> (xs : Vect len elem) -> Bool
339elemBy p e [] = False
342elemBy p e [] = False
340elemBy p e (x::xs) = p e x || elemBy p e xs
343elemBy p e (x::xs) = p e x || elemBy p e xs
342||| Use the default Boolean equality on elements to search for an item
345||| Use the default Boolean equality on elements to search for an item
343||| @ x what to search for
346||| @ x what to search for
344||| @ xs where to search
347||| @ xs where to search
345−elem : Eq a => (x : a) -> (xs : Vect n a) -> Bool
348+elem : Eq elem => (x : elem) -> (xs : Vect len elem) -> Bool
346elem = elemBy (==)
349elem = elemBy (==)
348||| Find the association of some key with a user-provided comparison
351||| Find the association of some key with a user-provided comparison
349||| @ p the comparison operator for keys (True if they match)
352||| @ p the comparison operator for keys (True if they match)
350||| @ e the key to look for
353||| @ e the key to look for
351−lookupBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n (a, b)) -> Maybe b
354+lookupBy : (p : key -> key -> Bool) -> (e : key) -> (xs : Vect n (key, val)) -> Maybe val
352lookupBy p e [] = Nothing
355lookupBy p e [] = Nothing
353lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs
356lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs
355||| Find the assocation of some key using the default Boolean equality test
358||| Find the assocation of some key using the default Boolean equality test
356−lookup : Eq a => a -> Vect n (a, b) -> Maybe b
359+lookup : Eq key => key -> Vect n (key, val) -> Maybe val
357lookup = lookupBy (==)
360lookup = lookupBy (==)
359||| Check if any element of xs is found in elems by a user-provided comparison
362||| Check if any element of xs is found in elems by a user-provided comparison
360||| @ p the comparison operator
363||| @ p the comparison operator
361||| @ elems the vector to search
364||| @ elems the vector to search
362||| @ xs what to search for
365||| @ xs what to search for
363−hasAnyBy : (p : a -> a -> Bool) -> (elems : Vect m a) -> (xs : Vect n a) -> Bool
366+hasAnyBy : (p : elem -> elem -> Bool) -> (elems : Vect m elem) -> (xs : Vect len elem) -> Bool
364hasAnyBy p elems [] = False
367hasAnyBy p elems [] = False
365hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs
368hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs
367||| Check if any element of xs is found in elems using the default Boolean equality test
370||| Check if any element of xs is found in elems using the default Boolean equality test
368−hasAny : Eq a => Vect m a -> Vect n a -> Bool
371+hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool
369hasAny = hasAnyBy (==)
372hasAny = hasAnyBy (==)
371--------------------------------------------------------------------------------
374--------------------------------------------------------------------------------
@@ -374,31 +377,31 @@ hasAny = hasAnyBy (==)
375||| Find the first element of the vector that satisfies some test
378||| Find the first element of the vector that satisfies some test
376||| @ p the test to satisfy
379||| @ p the test to satisfy
377−find : (p : a -> Bool) -> (xs : Vect n a) -> Maybe a
380+find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem
378find p [] = Nothing
381find p [] = Nothing
379find p (x::xs) = if p x then Just x else find p xs
382find p (x::xs) = if p x then Just x else find p xs
381||| Find the index of the first element of the vector that satisfies some test
384||| Find the index of the first element of the vector that satisfies some test
382−findIndex : (a -> Bool) -> Vect n a -> Maybe (Fin n)
385+findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)
383findIndex p [] = Nothing
386findIndex p [] = Nothing
384findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)
387findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)
386||| Find the indices of all elements that satisfy some test
389||| Find the indices of all elements that satisfy some test
387−findIndices : (a -> Bool) -> Vect m a -> List (Fin m)
390+findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)
388findIndices p [] = []
391findIndices p [] = []
389findIndices p (x :: xs) = let is = map FS $ findIndices p xs
392findIndices p (x :: xs) = let is = map FS $ findIndices p xs
390 in if p x then 0 :: is else is
393 in if p x then 0 :: is else is
392−elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe (Fin m)
395+elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)
393elemIndexBy p e = findIndex $ p e
396elemIndexBy p e = findIndex $ p e
395−elemIndex : Eq a => a -> Vect m a -> Maybe (Fin m)
398+elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)
396elemIndex = elemIndexBy (==)
399elemIndex = elemIndexBy (==)
398−elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> List (Fin m)
401+elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)
399elemIndicesBy p e = findIndices $ p e
402elemIndicesBy p e = findIndices $ p e
401−elemIndices : Eq a => a -> Vect m a -> List (Fin m)
404+elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
402elemIndices = elemIndicesBy (==)
405elemIndices = elemIndicesBy (==)
404--------------------------------------------------------------------------------
407--------------------------------------------------------------------------------
@@ -406,7 +409,7 @@ elemIndices = elemIndicesBy (==)
406--------------------------------------------------------------------------------
409--------------------------------------------------------------------------------
408||| Find all elements of a vector that satisfy some test
411||| Find all elements of a vector that satisfy some test
409−filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
412+filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
410filter p [] = ( _ ** [] )
413filter p [] = ( _ ** [] )
411filter p (x::xs) =
414filter p (x::xs) =
412 let (_ ** tail) = filter p xs
415 let (_ ** tail) = filter p xs
@@ -416,10 +419,10 @@ filter p (x::xs) =
416 (_ ** tail)
419 (_ ** tail)
418||| Make the elements of some vector unique by some test
421||| Make the elements of some vector unique by some test
419−nubBy : (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)
422+nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
420nubBy = nubBy' []
423nubBy = nubBy' []
422− nubBy' : Vect m a -> (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)
425+ nubBy' : Vect m elem -> (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
423 nubBy' acc p [] = (_ ** [])
426 nubBy' acc p [] = (_ ** [])
424 nubBy' acc p (x::xs) with (elemBy p x acc)
427 nubBy' acc p (x::xs) with (elemBy p x acc)
425 | True = nubBy' acc p xs
428 | True = nubBy' acc p xs
@@ -427,16 +430,16 @@ nubBy = nubBy' []
427 | (_ ** tail) = (_ ** x::tail)
430 | (_ ** tail) = (_ ** x::tail)
429||| Make the elements of some vector unique by the default Boolean equality
432||| Make the elements of some vector unique by the default Boolean equality
430−nub : Eq a => Vect n a -> (p ** Vect p a)
433+nub : Eq elem => Vect len elem -> (p ** Vect p elem)
431nub = nubBy (==)
434nub = nubBy (==)
433−deleteBy : (a -> a -> Bool) -> a -> Vect n a -> (p ** Vect p a)
436+deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem)
434deleteBy _ _ [] = (_ ** [])
437deleteBy _ _ [] = (_ ** [])
435deleteBy eq x (y::ys) =
438deleteBy eq x (y::ys) =
436 let (len ** zs) = deleteBy eq x ys
439 let (len ** zs) = deleteBy eq x ys
437 in if x `eq` y then (_ ** ys) else (S len ** y ::zs)
440 in if x `eq` y then (_ ** ys) else (S len ** y ::zs)
439−delete : (Eq a) => a -> Vect n a -> (p ** Vect p a)
442+delete : (Eq elem) => elem -> Vect len elem -> (p ** Vect p elem)
440delete = deleteBy (==)
443delete = deleteBy (==)
442--------------------------------------------------------------------------------
445--------------------------------------------------------------------------------
@@ -448,10 +451,10 @@ delete = deleteBy (==)
448||| It is equivalent to (take n xs, drop n xs)
451||| It is equivalent to (take n xs, drop n xs)
449||| @ n the index to split at
452||| @ n the index to split at
450||| @ xs the Vect to split in two
453||| @ xs the Vect to split in two
451−splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a)
454+splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
452splitAt n xs = (take n xs, drop n xs)
455splitAt n xs = (take n xs, drop n xs)
454−partition : (a -> Bool) -> Vect n a -> ((p ** Vect p a), (q ** Vect q a))
457+partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
455partition p [] = ((_ ** []), (_ ** []))
458partition p [] = ((_ ** []), (_ ** []))
456partition p (x::xs) =
459partition p (x::xs) =
457 let ((leftLen ** lefts), (rightLen ** rights)) = partition p xs in
460 let ((leftLen ** lefts), (rightLen ** rights)) = partition p xs in
@@ -464,29 +467,29 @@ partition p (x::xs) =
464-- Predicates
467-- Predicates
465--------------------------------------------------------------------------------
468--------------------------------------------------------------------------------
467−isPrefixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool
470+isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
468isPrefixOfBy p [] right = True
471isPrefixOfBy p [] right = True
469isPrefixOfBy p left [] = False
472isPrefixOfBy p left [] = False
470isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys
473isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys
472−isPrefixOf : Eq a => Vect m a -> Vect n a -> Bool
475+isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
473isPrefixOf = isPrefixOfBy (==)
476isPrefixOf = isPrefixOfBy (==)
475−isSuffixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool
478+isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
476isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
479isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
478−isSuffixOf : Eq a => Vect m a -> Vect n a -> Bool
481+isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
479isSuffixOf = isSuffixOfBy (==)
482isSuffixOf = isSuffixOfBy (==)
481--------------------------------------------------------------------------------
484--------------------------------------------------------------------------------
482-- Conversions
485-- Conversions
483--------------------------------------------------------------------------------
486--------------------------------------------------------------------------------
485−maybeToVect : Maybe a -> (p ** Vect p a)
488+maybeToVect : Maybe elem -> (p ** Vect p elem)
486maybeToVect Nothing = (_ ** [])
489maybeToVect Nothing = (_ ** [])
487maybeToVect (Just j) = (_ ** [j])
490maybeToVect (Just j) = (_ ** [j])
489−vectToMaybe : Vect n a -> Maybe a
492+vectToMaybe : Vect len elem -> Maybe elem
490vectToMaybe [] = Nothing
493vectToMaybe [] = Nothing
491vectToMaybe (x::xs) = Just x
494vectToMaybe (x::xs) = Just x
@@ -494,25 +497,25 @@ vectToMaybe (x::xs) = Just x
495--------------------------------------------------------------------------------
498--------------------------------------------------------------------------------
497−catMaybes : Vect n (Maybe a) -> (p ** Vect p a)
500+catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem)
498catMaybes [] = (_ ** [])
501catMaybes [] = (_ ** [])
499catMaybes (Nothing::xs) = catMaybes xs
502catMaybes (Nothing::xs) = catMaybes xs
500catMaybes ((Just j)::xs) =
503catMaybes ((Just j)::xs) =
501 let (_ ** tail) = catMaybes xs
504 let (_ ** tail) = catMaybes xs
502 in (_ ** j::tail)
505 in (_ ** j::tail)
504−diag : Vect n (Vect n a) -> Vect n a
507+diag : Vect len (Vect len elem) -> Vect len elem
505diag [] = []
508diag [] = []
506diag ((x::xs)::xss) = x :: diag (map tail xss)
509diag ((x::xs)::xss) = x :: diag (map tail xss)
508−range : {n : Nat} -> Vect n (Fin n)
511+range : {len : Nat} -> Vect len (Fin len)
509−range {n=Z} = []
512+range {len=Z} = []
510−range {n=S _} = FZ :: map FS range
513+range {len=S _} = FZ :: map FS range
512||| Transpose a Vect of Vects, turning rows into columns and vice versa.
515||| Transpose a Vect of Vects, turning rows into columns and vice versa.
514||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
517||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
515−transpose : {n : Nat} -> Vect m (Vect n a) -> Vect n (Vect m a)
518+transpose : {n : Nat} -> Vect m (Vect n elem) -> Vect n (Vect m elem)
516transpose [] = replicate _ []
519transpose [] = replicate _ []
517transpose (x :: xs) = zipWith (::) x (transpose xs)
520transpose (x :: xs) = zipWith (::) x (transpose xs)
@@ -527,7 +530,7 @@ implementation Applicative (Vect k) where
528||| This monad is different from the List monad, (>>=)
531||| This monad is different from the List monad, (>>=)
529||| uses the diagonal.
532||| uses the diagonal.
530−implementation Monad (Vect n) where
533+implementation Monad (Vect len) where
531 m >>= f = diag (map f m)
534 m >>= f = diag (map f m)
533implementation Traversable (Vect n) where
536implementation Traversable (Vect n) where
@@ -538,14 +541,14 @@ implementation Traversable (Vect n) where
539--------------------------------------------------------------------------------
542--------------------------------------------------------------------------------
541−implementation Show a => Show (Vect n a) where
544+implementation Show elem => Show (Vect len elem) where
542 show = show . toList
545 show = show . toList
544--------------------------------------------------------------------------------
547--------------------------------------------------------------------------------
545-- Properties
548-- Properties
546--------------------------------------------------------------------------------
549--------------------------------------------------------------------------------
548−vectConsCong : (x : a) -> (xs : Vect n a) -> (ys : Vect m a) -> (xs = ys) -> (x :: xs = x :: ys)
551+vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys)
549vectConsCong x xs xs Refl = Refl
552vectConsCong x xs xs Refl = Refl
551vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
554vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
@@ -553,7 +556,10 @@ vectNilRightNeutral [] = Refl
553vectNilRightNeutral (x :: xs) =
556vectNilRightNeutral (x :: xs) =
554 vectConsCong _ _ _ (vectNilRightNeutral xs)
557 vectConsCong _ _ _ (vectNilRightNeutral xs)
556−vectAppendAssociative : (x : Vect xLen a) -> (y : Vect yLen a) -> (z : Vect zLen a) -> x ++ (y ++ z) = (x ++ y) ++ z
559+vectAppendAssociative : (xs : Vect xLen elem) ->
560+ (ys : Vect yLen elem) ->
561+ (zs : Vect zLen elem) ->
562+ xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
557vectAppendAssociative [] y z = Refl
563vectAppendAssociative [] y z = Refl
558vectAppendAssociative (x :: xs) ys zs =
564vectAppendAssociative (x :: xs) ys zs =
559 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
565 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
@@ -599,7 +605,7 @@ noEmptyElem : {x : a} -> Elem x [] -> Void
599noEmptyElem Here impossible
605noEmptyElem Here impossible
601Uninhabited (Elem x []) where
607Uninhabited (Elem x []) where
602− uninhabited = noEmptyElem
608+ uninhabited = noEmptyElem
604||| An item not in the head and not in the tail is not in the Vect at all
610||| An item not in the head and not in the tail is not in the Vect at all
605neitherHereNorThere : {x, y : a} -> {xs : Vect n a} -> Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
611neitherHereNorThere : {x, y : a} -> {xs : Vect n a} -> Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
@@ -634,7 +640,7 @@ mapElem (There e) = There (mapElem e)
634||| length in its type, otherwise return Nothing
640||| length in its type, otherwise return Nothing
635||| @len the required length
641||| @len the required length
636||| @xs the vector with the desired length
642||| @xs the vector with the desired length
637−-- Needs to be Maybe rather than Dec, because if 'n' is unequal to m, we
643+-- Needs to be Maybe rather than Dec, because if 'n' is unequal to m, we
638-- only know we don't know how to make a Vect n a, not that one can't exist.
644-- only know we don't know how to make a Vect n a, not that one can't exist.
639exactLength : {m : Nat} -> -- expected at run-time
645exactLength : {m : Nat} -> -- expected at run-time
640 (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)
646 (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)
@@ -654,4 +660,3 @@ overLength {m} n xs with (cmp m n)
654 = Just (0 ** xs)
660 = Just (0 ** xs)
655 overLength {m = plus n (S x)} n xs | (CmpGT x)
661 overLength {m = plus n (S x)} n xs | (CmpGT x)
656 = Just (S x ** rewrite plusCommutative (S x) n in xs)
662 = Just (S x ** rewrite plusCommutative (S x) n in xs)