@@ -9,13 +9,15 @@ import Language.Reflection
99infixr 7 ::
1010
1111||| Vectors: Generic lists with explicit length in the type
12+||| @ len the length of the list
13+||| @ elem the type of elements
1214%elim
13−data Vect : Nat -> Type -> Type where
15+data Vect : (len : Nat) -> (elem : Type) -> Type where
1416 ||| Empty vector
15− Nil : Vect Z a
16− ||| A non-empty vector of length `S k`, consisting of a head element and
17− ||| the rest of the list, of length `k`.
18− (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a
17+ Nil : Vect Z elem
18+ ||| A non-empty vector of length `S len`, consisting of a head element and
19+ ||| the rest of the list, of length `len`.
20+ (::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem
1921
2022-- Hints for interactive editing
2123%name Vect xs,ys,zs,ws
@@ -28,14 +30,14 @@ data Vect : Nat -> Type -> Type where
2830|||
2931||| **Note**: this is only useful if you don't already statically know the length
3032||| 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)
3234||| @ xs the vector
33−length : (xs : Vect n a) -> Nat
35+length : (xs : Vect len elem) -> Nat
3436length [] = 0
3537length (x::xs) = 1 + length xs
3638
3739||| 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
3941lengthCorrect Z [] = Refl
4042lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl
4143
@@ -44,44 +46,44 @@ lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl
4446--------------------------------------------------------------------------------
4547
4648||| 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
4850tail (x::xs) = xs
4951
5052||| Only the first element of the vector
51−head : Vect (S n) a -> a
53+head : Vect (S len) elem -> elem
5254head (x::xs) = x
5355
5456||| The last element of the vector
55−last : Vect (S n) a -> a
57+last : Vect (S len) elem -> elem
5658last (x::[]) = x
5759last (x::y::ys) = last $ y::ys
5860
5961||| 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
6163init (x::[]) = []
6264init (x::y::ys) = x :: init (y::ys)
6365
6466||| Extract a particular element from a vector
65−index : Fin n -> Vect n a -> a
67+index : Fin len -> Vect len elem -> elem
6668index FZ (x::xs) = x
6769index (FS k) (x::xs) = index k xs
6870
6971
7072||| 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
7274insertAt FZ y xs = y :: xs
7375insertAt (FS k) y (x::xs) = x :: insertAt k y xs
7476insertAt (FS k) y [] = absurd k
7577
7678||| Construct a new vector consisting of all but the indicated element
77−deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a
78−deleteAt FZ (x::xs) = xs
79−deleteAt {n = S m} (FS k) (x::xs) = x :: deleteAt k xs
80−deleteAt {n = Z} (FS k) (x::xs) = absurd k
81−deleteAt _ [] impossible
79+deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem
80+deleteAt FZ (x::xs) = xs
81+deleteAt {len = S m} (FS k) (x::xs) = x :: deleteAt k xs
82+deleteAt {len = Z} (FS k) (x::xs) = absurd k
83+deleteAt _ [] impossible
8284
8385||| 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
8587replaceAt FZ y (x::xs) = y :: xs
8688replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
8789
@@ -89,7 +91,7 @@ replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
8991||| @ i the index to replace at
9092||| @ f the update function
9193||| @ 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
9395updateAt FZ f (x::xs) = f x :: xs
9496updateAt (FS k) f (x::xs) = x :: updateAt k f xs
9597
@@ -99,13 +101,13 @@ updateAt (FS k) f (x::xs) = x :: updateAt k f xs
99101
100102||| Get the first n elements of a Vect
101103||| @ 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
103105take Z xs = []
104106take (S k) (x :: xs) = x :: take k xs
105107
106108||| Remove the first n elements of a Vect
107109||| @ 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
109111drop Z xs = xs
110112drop (S k) (x :: xs) = drop k xs
111113
@@ -113,7 +115,7 @@ drop (S k) (x :: xs) = drop k xs
113115||| Boolean predicate.
114116|||
115117||| @ 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)
117119takeWhile p [] = (_ ** [])
118120takeWhile p (x::xs) =
119121 let (len ** ys) = takeWhile p xs
@@ -126,7 +128,7 @@ takeWhile p (x::xs) =
126128||| Boolean predicate.
127129|||
128130||| @ 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)
130132dropWhile p [] = (_ ** [])
131133dropWhile p (x::xs) =
132134 if p x then
@@ -139,9 +141,9 @@ dropWhile p (x::xs) =
139141--------------------------------------------------------------------------------
140142
141143||| 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
143145reverse 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
145147 go {n} acc [] = rewrite plusZeroRightNeutral n in acc
146148 go {n} {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m
147149 in go (x::acc) xs
@@ -149,11 +151,11 @@ reverse xs = go [] xs
149151||| Alternate an element between the other elements of a vector
150152||| @ sep the element to intersperse
151153||| @ 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
153155intersperse sep [] = []
154156intersperse sep (x::xs) = x :: intersperse' sep xs
155157 where
156− intersperse' : a -> Vect n a -> Vect (n + n) a
158+ intersperse' : elem -> Vect n elem -> Vect (n + n) elem
157159 intersperse' sep [] = []
158160 intersperse' {n=S n} sep (x::xs) = rewrite sym $ plusSuccRightSucc n n
159161 in sep :: x :: intersperse' sep xs
@@ -163,17 +165,17 @@ intersperse sep (x::xs) = x :: intersperse' sep xs
163165--------------------------------------------------------------------------------
164166
165167
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
167169fromList' ys [] = ys
168−fromList' {n} ys (x::xs) =
169− rewrite (plusSuccRightSucc (length xs) n) ==>
170− Vect (plus (length xs) (S n)) a in
170+fromList' {len} ys (x::xs) =
171+ rewrite (plusSuccRightSucc (length xs) len) ==>
172+ Vect (plus (length xs) (S len)) elem in
171173 fromList' (x::ys) xs
172174
173175||| Convert a list to a vector.
174176|||
175177||| 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
177179fromList l =
178180 rewrite (sym $ plusZeroRightNeutral (length l)) in
179181 reverse $ fromList' [] l
@@ -183,30 +185,31 @@ fromList l =
183185--------------------------------------------------------------------------------
184186
185187||| 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
187189(++) [] ys = ys
188190(++) (x::xs) ys = x :: xs ++ ys
189191
190−||| Repeate some value n times
191−||| @ n the number of times to repeat it
192+||| Repeate some value some number of times.
193+|||
194+||| @ len the number of times to repeat it
192195||| @ x the value to repeat
193−replicate : (n : Nat) -> (x : a) -> Vect n a
196+replicate : (len : Nat) -> (x : elem) -> Vect len elem
194197replicate Z x = []
195198replicate (S k) x = x :: replicate k x
196199
197200||| 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
199202mergeBy order [] [] = []
200203mergeBy 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
202205 x :: xs
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)
204207 = case order x y of
205208 LT => x :: mergeBy order xs (y :: ys)
206− _ => rewrite sym (plusSuccRightSucc k k') in
209+ _ => rewrite sym (plusSuccRightSucc k k') in
207210 y :: mergeBy order (x :: xs) ys
208211
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
210213merge = mergeBy compare
211214
212215--------------------------------------------------------------------------------
@@ -223,26 +226,26 @@ zipWith f [] [] = []
223226zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
224227
225228||| 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
227230zipWith3 f [] [] [] = []
228231zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
229232
230233||| 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)
232235zip = zipWith (\x,y => (x,y))
233236
234237||| 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)
236239zip3 = zipWith3 (\x,y,z => (x,y,z))
237240
238241||| 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)
240243unzip [] = ([], [])
241244unzip ((l, r)::xs) with (unzip xs)
242245 | (lefts, rights) = (l::lefts, r::rights)
243246
244247||| 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)
246249unzip3 [] = ([], [], [])
247250unzip3 ((l,c,r)::xs) with (unzip3 xs)
248251 | (lefts, centers, rights) = (l::lefts, c::centers, r::rights)
@@ -251,7 +254,7 @@ unzip3 ((l,c,r)::xs) with (unzip3 xs)
251254-- Equality
252255--------------------------------------------------------------------------------
253256
254−implementation (Eq a) => Eq (Vect n a) where
257+implementation (Eq elem) => Eq (Vect len elem) where
255258 (==) [] [] = True
256259 (==) (x::xs) (y::ys) = x == y && xs == ys
257260
@@ -260,7 +263,7 @@ implementation (Eq a) => Eq (Vect n a) where
260263-- Order
261264--------------------------------------------------------------------------------
262265
263−implementation Ord a => Ord (Vect n a) where
266+implementation Ord elem => Ord (Vect len elem) where
264267 compare [] [] = EQ
265268 compare (x::xs) (y::ys) = compare x y `thenCompare` compare xs ys
266269
@@ -283,7 +286,7 @@ implementation Functor (Vect n) where
283286|||
284287||| @ f the partial function (expressed by returning `Maybe`)
285288||| @ 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)
287290mapMaybe f [] = (_ ** [])
288291mapMaybe f (x::xs) =
289292 let (len ** ys) = mapMaybe f xs
@@ -308,7 +311,7 @@ implementation Foldable (Vect n) where
308311--------------------------------------------------------------------------------
309312
310313||| 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
312315concat [] = []
313316concat (v::vs) = v ++ concat vs
314317
@@ -323,7 +326,7 @@ foldl1 f (x::xs) = foldl f x xs
323326-- Scans
324327--------------------------------------------------------------------------------
325328
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
327330scanl f q [] = [q]
328331scanl f q (x::xs) = q :: scanl f (f q x) xs
329332
@@ -335,37 +338,37 @@ scanl f q (x::xs) = q :: scanl f (f q x) xs
335338||| @ p the equality test
336339||| @ e the item to search for
337340||| @ 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
339342elemBy p e [] = False
340343elemBy p e (x::xs) = p e x || elemBy p e xs
341344
342345||| Use the default Boolean equality on elements to search for an item
343346||| @ x what to search for
344347||| @ 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
346349elem = elemBy (==)
347350
348351||| Find the association of some key with a user-provided comparison
349352||| @ p the comparison operator for keys (True if they match)
350353||| @ 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
352355lookupBy p e [] = Nothing
353356lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs
354357
355358||| 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
357360lookup = lookupBy (==)
358361
359362||| Check if any element of xs is found in elems by a user-provided comparison
360363||| @ p the comparison operator
361364||| @ elems the vector to search
362365||| @ 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
364367hasAnyBy p elems [] = False
365368hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs
366369
367370||| 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
369372hasAny = hasAnyBy (==)
370373
371374--------------------------------------------------------------------------------
@@ -374,31 +377,31 @@ hasAny = hasAnyBy (==)
374377
375378||| Find the first element of the vector that satisfies some test
376379||| @ 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
378381find p [] = Nothing
379382find p (x::xs) = if p x then Just x else find p xs
380383
381384||| 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)
383386findIndex p [] = Nothing
384387findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)
385388
386389||| 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)
388391findIndices p [] = []
389392findIndices p (x :: xs) = let is = map FS $ findIndices p xs
390393 in if p x then 0 :: is else is
391394
392−elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe (Fin m)
395+elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)
393396elemIndexBy p e = findIndex $ p e
394397
395−elemIndex : Eq a => a -> Vect m a -> Maybe (Fin m)
398+elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)
396399elemIndex = elemIndexBy (==)
397400
398−elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> List (Fin m)
401+elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)
399402elemIndicesBy p e = findIndices $ p e
400403
401−elemIndices : Eq a => a -> Vect m a -> List (Fin m)
404+elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
402405elemIndices = elemIndicesBy (==)
403406
404407--------------------------------------------------------------------------------
@@ -406,7 +409,7 @@ elemIndices = elemIndicesBy (==)
406409--------------------------------------------------------------------------------
407410
408411||| 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)
410413filter p [] = ( _ ** [] )
411414filter p (x::xs) =
412415 let (_ ** tail) = filter p xs
@@ -416,10 +419,10 @@ filter p (x::xs) =
416419 (_ ** tail)
417420
418421||| 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)
420423nubBy = nubBy' []
421424 where
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)
423426 nubBy' acc p [] = (_ ** [])
424427 nubBy' acc p (x::xs) with (elemBy p x acc)
425428 | True = nubBy' acc p xs
@@ -427,16 +430,16 @@ nubBy = nubBy' []
427430 | (_ ** tail) = (_ ** x::tail)
428431
429432||| 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)
431434nub = nubBy (==)
432435
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)
434437deleteBy _ _ [] = (_ ** [])
435438deleteBy eq x (y::ys) =
436439 let (len ** zs) = deleteBy eq x ys
437440 in if x `eq` y then (_ ** ys) else (S len ** y ::zs)
438441
439−delete : (Eq a) => a -> Vect n a -> (p ** Vect p a)
442+delete : (Eq elem) => elem -> Vect len elem -> (p ** Vect p elem)
440443delete = deleteBy (==)
441444
442445--------------------------------------------------------------------------------
@@ -448,10 +451,10 @@ delete = deleteBy (==)
448451||| It is equivalent to (take n xs, drop n xs)
449452||| @ n the index to split at
450453||| @ 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)
452455splitAt n xs = (take n xs, drop n xs)
453456
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))
455458partition p [] = ((_ ** []), (_ ** []))
456459partition p (x::xs) =
457460 let ((leftLen ** lefts), (rightLen ** rights)) = partition p xs in
@@ -464,29 +467,29 @@ partition p (x::xs) =
464467-- Predicates
465468--------------------------------------------------------------------------------
466469
467−isPrefixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool
470+isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
468471isPrefixOfBy p [] right = True
469472isPrefixOfBy p left [] = False
470473isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys
471474
472−isPrefixOf : Eq a => Vect m a -> Vect n a -> Bool
475+isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
473476isPrefixOf = isPrefixOfBy (==)
474477
475−isSuffixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool
478+isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
476479isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
477480
478−isSuffixOf : Eq a => Vect m a -> Vect n a -> Bool
481+isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
479482isSuffixOf = isSuffixOfBy (==)
480483
481484--------------------------------------------------------------------------------
482485-- Conversions
483486--------------------------------------------------------------------------------
484487
485−maybeToVect : Maybe a -> (p ** Vect p a)
488+maybeToVect : Maybe elem -> (p ** Vect p elem)
486489maybeToVect Nothing = (_ ** [])
487490maybeToVect (Just j) = (_ ** [j])
488491
489−vectToMaybe : Vect n a -> Maybe a
492+vectToMaybe : Vect len elem -> Maybe elem
490493vectToMaybe [] = Nothing
491494vectToMaybe (x::xs) = Just x
492495
@@ -494,25 +497,25 @@ vectToMaybe (x::xs) = Just x
494497-- Misc
495498--------------------------------------------------------------------------------
496499
497−catMaybes : Vect n (Maybe a) -> (p ** Vect p a)
500+catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem)
498501catMaybes [] = (_ ** [])
499502catMaybes (Nothing::xs) = catMaybes xs
500503catMaybes ((Just j)::xs) =
501504 let (_ ** tail) = catMaybes xs
502505 in (_ ** j::tail)
503506
504−diag : Vect n (Vect n a) -> Vect n a
507+diag : Vect len (Vect len elem) -> Vect len elem
505508diag [] = []
506509diag ((x::xs)::xss) = x :: diag (map tail xss)
507510
508−range : {n : Nat} -> Vect n (Fin n)
509−range {n=Z} = []
510−range {n=S _} = FZ :: map FS range
511+range : {len : Nat} -> Vect len (Fin len)
512+range {len=Z} = []
513+range {len=S _} = FZ :: map FS range
511514
512515||| Transpose a Vect of Vects, turning rows into columns and vice versa.
513516|||
514517||| 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)
516519transpose [] = replicate _ []
517520transpose (x :: xs) = zipWith (::) x (transpose xs)
518521
@@ -527,7 +530,7 @@ implementation Applicative (Vect k) where
527530
528531||| This monad is different from the List monad, (>>=)
529532||| uses the diagonal.
530−implementation Monad (Vect n) where
533+implementation Monad (Vect len) where
531534 m >>= f = diag (map f m)
532535
533536implementation Traversable (Vect n) where
@@ -538,14 +541,14 @@ implementation Traversable (Vect n) where
538541-- Show
539542--------------------------------------------------------------------------------
540543
541−implementation Show a => Show (Vect n a) where
544+implementation Show elem => Show (Vect len elem) where
542545 show = show . toList
543546
544547--------------------------------------------------------------------------------
545548-- Properties
546549--------------------------------------------------------------------------------
547550
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)
549552vectConsCong x xs xs Refl = Refl
550553
551554vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
@@ -553,7 +556,10 @@ vectNilRightNeutral [] = Refl
553556vectNilRightNeutral (x :: xs) =
554557 vectConsCong _ _ _ (vectNilRightNeutral xs)
555558
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
557563vectAppendAssociative [] y z = Refl
558564vectAppendAssociative (x :: xs) ys zs =
559565 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
@@ -599,7 +605,7 @@ noEmptyElem : {x : a} -> Elem x [] -> Void
599605noEmptyElem Here impossible
600606
601607Uninhabited (Elem x []) where
602− uninhabited = noEmptyElem
608+ uninhabited = noEmptyElem
603609
604610||| An item not in the head and not in the tail is not in the Vect at all
605611neitherHereNorThere : {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)
634640||| length in its type, otherwise return Nothing
635641||| @len the required length
636642||| @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
638644-- only know we don't know how to make a Vect n a, not that one can't exist.
639645exactLength : {m : Nat} -> -- expected at run-time
640646 (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)
@@ -654,4 +660,3 @@ overLength {m} n xs with (cmp m n)
654660 = Just (0 ** xs)
655661 overLength {m = plus n (S x)} n xs | (CmpGT x)
656662 = Just (S x ** rewrite plusCommutative (S x) n in xs)
657−