@@ -70,13 +70,48 @@ drop (fS k) [] = FinZElim k
7070drop fZ xs ?= xs
7171drop (fS k) (x::xs) = drop k xs
7272
73+--------------------------------------------------------------------------------
74+-- Transformations
75+--------------------------------------------------------------------------------
76+
77+total reverse : {n : Nat} -> Vect n a -> Vect n a
78+reverse {n} xs = reverse' [] (plusZeroRightNeutral n) xs
79+ where
80+ total reverse' : {m, j, l : Nat} ->
81+ Vect m a -> (j + m = l) -> Vect j a -> Vect l a
82+ reverse' {m} {j = Z } {l} acc prf [] ?= acc
83+ reverse' {m} {j = S k} {l} acc prf (x::xs) =
84+ let prf1 : (m + (S k) = l) = rewrite plusCommutative m (S k) in prf in
85+ let prf2 : (S (m + k) = l) = rewrite plusSuccRightSucc m k in prf1 in
86+ let prf3 : (S (k + m) = l) = rewrite plusCommutative k m in prf2 in
87+ let prf4 : (k + (S m) = l) = rewrite sym $ plusSuccRightSucc k m in prf3 in
88+ reverse' (x::acc) prf4 xs
89+
90+intersperse : a -> Vect n a -> Vect (n + pred n) a
91+intersperse sep [] = []
92+intersperse sep (x::xs) = x :: intersperse' sep xs
93+ where
94+ intersperse' : a -> Vect n a -> Vect (n + n) a
95+ intersperse' sep [] = []
96+ intersperse' sep (x::xs) ?= sep :: x :: intersperse' sep xs
97+
7398--------------------------------------------------------------------------------
7499-- Conversion from list (toList is provided by Foldable)
75100--------------------------------------------------------------------------------
76101
102+
103+fromList' : Vect n a -> (l : List a) -> Vect (length l + n) a
104+fromList' ys [] = ys
105+fromList' {n} ys (x::xs) =
106+ rewrite (plusSuccRightSucc (length xs) n) ==>
107+ Vect (plus (length xs) (S n)) a in
108+ fromList' (x::ys) xs
109+
110+
77111fromList : (l : List a) -> Vect (length l) a
78−fromList [] = []
79−fromList (x::xs) = x :: fromList xs
112+fromList l =
113+ rewrite (sym $ plusZeroRightNeutral (length l)) in
114+ reverse $ fromList' [] l
80115
81116--------------------------------------------------------------------------------
82117-- Building (bigger) vectors
@@ -154,9 +189,12 @@ instance Functor (Vect n) where
154189-- Folds
155190--------------------------------------------------------------------------------
156191
192+total foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc
193+foldrImpl f e go [] = go e
194+foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
195+
157196instance Foldable (Vect n) where
158− foldr f e [] = e
159− foldr f e (x::xs) = f x (foldr f e xs)
197+ foldr f e xs = foldrImpl f e id xs
160198
161199--------------------------------------------------------------------------------
162200-- Special folds
@@ -166,25 +204,6 @@ concat : Vect m (Vect n a) -> Vect (m * n) a
166204concat [] = []
167205concat (v::vs) = v ++ concat vs
168206
169−--------------------------------------------------------------------------------
170−-- Transformations
171−--------------------------------------------------------------------------------
172−
173−total reverse : Vect n a -> Vect n a
174−reverse = reverse' []
175− where
176− total reverse' : Vect m a -> Vect n a -> Vect (m + n) a
177− reverse' acc [] ?= acc
178− reverse' acc (x::xs) ?= reverse' (x::acc) xs
179−
180−intersperse : a -> Vect n a -> Vect (n + pred n) a
181−intersperse sep [] = []
182−intersperse sep (x::xs) = x :: intersperse' sep xs
183− where
184− intersperse' : a -> Vect n a -> Vect (n + n) a
185− intersperse' sep [] = []
186− intersperse' sep (x::xs) ?= sep :: x :: intersperse' sep xs
187−
188207--------------------------------------------------------------------------------
189208-- Membership tests
190209--------------------------------------------------------------------------------
@@ -349,14 +368,9 @@ Prelude.Vect.drop_lemma_1 = proof {
349368 trivial;
350369}
351370
352−Prelude.Vect.reverse'_lemma_2 = proof {
353− intros;
354− rewrite (plusSuccRightSucc m n1);
355− exact value;
356−}
357−
358371Prelude.Vect.reverse'_lemma_1 = proof {
359372 intros;
373+ rewrite prf;
360374 rewrite sym (plusZeroRightNeutral m);
361375 exact value;
362376}