@@ -37,7 +37,7 @@ length (x::xs) = 1 + length xs
3737
3838||| Show that the length function on vectors in fact calculates the length
3939private lengthCorrect : (n : Nat) -> (xs : Vect n a) -> length xs = n
40−lengthCorrect Z [] = refl
40+lengthCorrect Z [] = refl
4141lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in refl
4242
4343--------------------------------------------------------------------------------
@@ -66,7 +66,7 @@ init (x::y::ys) = x :: init (y::ys)
6666index : Fin n -> Vect n a -> a
6767index fZ (x::xs) = x
6868index (fS k) (x::xs) = index k xs
69−index fZ [] impossible
69+index fZ [] impossible
7070
7171||| Insert an element at a particular index
7272insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a
@@ -79,7 +79,7 @@ deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a
7979deleteAt fZ (x::xs) = xs
8080deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs
8181deleteAt {n = Z} (fS k) (x::xs) = absurd k
82−deleteAt _ [] impossible
82+deleteAt _ [] impossible
8383
8484||| Replace an element at a particlar index with another
8585replaceAt : Fin n -> t -> Vect n t -> Vect n t
@@ -101,13 +101,13 @@ updateAt (fS k) f (x::xs) = x :: updateAt k f xs
101101||| Get the first m elements of a Vect
102102||| @ m the number of elements to take
103103take : (n : Nat) -> Vect (n + m) a -> Vect n a
104−take Z xs = []
104+take Z xs = []
105105take (S k) (x :: xs) = x :: take k xs
106106
107107||| Remove the first m elements of a Vect
108108||| @ m the number of elements to remove
109109drop : (n : Nat) -> Vect (n + m) a -> Vect m a
110−drop Z xs = xs
110+drop Z xs = xs
111111drop (S k) (x :: xs) = drop k xs
112112
113113--------------------------------------------------------------------------------
@@ -115,18 +115,12 @@ drop (S k) (x :: xs) = drop k xs
115115--------------------------------------------------------------------------------
116116
117117||| Reverse the order of the elements of a vector
118−total reverse : {n : Nat} -> Vect n a -> Vect n a
119−reverse {n} xs = reverse' [] (plusZeroRightNeutral n) xs
120− where
121− total reverse' : {m, j, l : Nat} ->
122− Vect m a -> (j + m = l) -> Vect j a -> Vect l a
123− reverse' {m} {j = Z } {l} acc prf [] ?= acc
124− reverse' {m} {j = S k} {l} acc prf (x::xs) =
125− let prf1 : (m + (S k) = l) = rewrite plusCommutative m (S k) in prf in
126− let prf2 : (S (m + k) = l) = rewrite plusSuccRightSucc m k in prf1 in
127− let prf3 : (S (k + m) = l) = rewrite plusCommutative k m in prf2 in
128− let prf4 : (k + (S m) = l) = rewrite sym $ plusSuccRightSucc k m in prf3 in
129− reverse' (x::acc) prf4 xs
118+reverse : Vect n a -> Vect n a
119+reverse xs = go [] xs
120+ where go : Vect n a -> Vect m a -> Vect (n+m) a
121+ go {n} acc [] = rewrite plusZeroRightNeutral n in acc
122+ go {n} {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m
123+ in go (x::acc) xs
130124
131125||| Alternate an element between the other elements of a vector
132126||| @ sep the element to intersperse
@@ -136,8 +130,9 @@ intersperse sep [] = []
136130intersperse sep (x::xs) = x :: intersperse' sep xs
137131 where
138132 intersperse' : a -> Vect n a -> Vect (n + n) a
139− intersperse' sep [] = []
140− intersperse' sep (x::xs) ?= sep :: x :: intersperse' sep xs
133+ intersperse' sep [] = []
134+ intersperse' {n=S n} sep (x::xs) = rewrite sym $ plusSuccRightSucc n n
135+ in sep :: x :: intersperse' sep xs
141136
142137--------------------------------------------------------------------------------
143138-- Conversion from list (toList is provided by Foldable)
@@ -147,7 +142,7 @@ intersperse sep (x::xs) = x :: intersperse' sep xs
147142fromList' : Vect n a -> (l : List a) -> Vect (length l + n) a
148143fromList' ys [] = ys
149144fromList' {n} ys (x::xs) =
150− rewrite (plusSuccRightSucc (length xs) n) ==>
145+ rewrite (plusSuccRightSucc (length xs) n) ==>
151146 Vect (plus (length xs) (S n)) a in
152147 fromList' (x::ys) xs
153148
@@ -212,7 +207,7 @@ instance (Eq a) => Eq (Vect n a) where
212207--------------------------------------------------------------------------------
213208
214209instance Ord a => Ord (Vect n a) where
215− compare [] [] = EQ
210+ compare [] [] = EQ
216211 compare (x::xs) (y::ys) =
217212 if x /= y then
218213 compare x y
@@ -228,15 +223,24 @@ instance Functor (Vect n) where
228223 map f [] = []
229224 map f (x::xs) = f x :: map f xs
230225
231−-- XXX: causes Idris to enter an infinite loop when type checking in the REPL
232−--mapMaybe : (a -> Maybe b) -> Vect n a -> (p ** Vect b p)
233−--mapMaybe f [] = (_ ** [])
234−--mapMaybe f (x::xs) = mapMaybe' (f x)
235−-- XXX: working around the type restrictions on case statements
236−-- where
237−-- mapMaybe' : (Maybe b) -> (n ** Vect b n) -> (p ** Vect b p)
238−-- mapMaybe' Nothing (n ** tail) = (n ** tail)
239−-- mapMaybe' (Just j) (n ** tail) = (S n ** j::tail)
226+
227+||| Map a partial function across a vector, returning those elements for which
228+||| the function had a value.
229+|||
230+||| The first projection of the resulting pair (ie the length) will always be
231+||| at most the length of the input vector. This is not, however, guaranteed
232+||| by the type.
233+|||
234+||| @ f the partial function (expressed by returning `Maybe`)
235+||| @ xs the vector to check for results
236+mapMaybe : (f : a -> Maybe b) -> (xs : Vect n a) -> (m : Nat ** Vect m b)
237+mapMaybe f [] = (_ ** [])
238+mapMaybe f (x::xs) =
239+ let (len ** ys) = mapMaybe f xs
240+ in case f x of
241+ Just y => (S len ** y :: ys)
242+ Nothing => ( len ** ys)
243+
240244
241245--------------------------------------------------------------------------------
242246-- Folds
@@ -451,18 +455,18 @@ catMaybes ((Just j)::xs) with (catMaybes xs)
451455 | (_ ** tail) = (_ ** j::tail)
452456
453457diag : Vect n (Vect n a) -> Vect n a
454−diag [] = []
458+diag [] = []
455459diag ((x::xs)::xss) = x :: diag (map tail xss)
456460
457461range : Vect n (Fin n)
458−range {n=Z} = []
462+range {n=Z} = []
459463range {n=S _} = fZ :: map fS range
460464
461465||| Transpose a Vect of Vects, turning rows into columns and vice versa.
462466|||
463467||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
464468transpose : Vect m (Vect n a) -> Vect n (Vect m a)
465−transpose [] = replicate _ []
469+transpose [] = replicate _ []
466470transpose (x :: xs) = zipWith (::) x (transpose xs)
467471
468472--------------------------------------------------------------------------------
@@ -483,19 +487,3 @@ vectAppendAssociative (x :: xs) ys zs =
483487 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
484488
485489
486−--------------------------------------------------------------------------------
487−-- Proofs
488−--------------------------------------------------------------------------------
489−
490−Prelude.Vect.reverse'_lemma_1 = proof {
491− intros;
492− rewrite prf;
493− rewrite sym (plusZeroRightNeutral m);
494− exact value;
495−}
496−
497−Prelude.Vect.intersperse'_lemma_1 = proof {
498− intros;
499− rewrite (plusSuccRightSucc n1 n1);
500− trivial;
501−}