git.iko.soy/Idris-dev
on master help sign in
Tail recursive foldr, reverse and fromList for Vect
49b4066Jan Bessai
libs/prelude/Prelude/Vect.idr+43−29
compare with master
unifiedsplit
@@ -70,13 +70,48 @@ drop (fS k) [] = FinZElim k
70drop fZ xs ?= xs
70drop fZ xs ?= xs
71drop (fS k) (x::xs) = drop k xs
71drop (fS k) (x::xs) = drop k xs
72
72
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+
73--------------------------------------------------------------------------------
98--------------------------------------------------------------------------------
74-- Conversion from list (toList is provided by Foldable)
99-- Conversion from list (toList is provided by Foldable)
75--------------------------------------------------------------------------------
100--------------------------------------------------------------------------------
76
101
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+
77fromList : (l : List a) -> Vect (length l) a
111fromList : (l : List a) -> Vect (length l) a
78−fromList [] = []
112+fromList l =
79−fromList (x::xs) = x :: fromList xs
113+ rewrite (sym $ plusZeroRightNeutral (length l)) in
114+ reverse $ fromList' [] l
80
115
81--------------------------------------------------------------------------------
116--------------------------------------------------------------------------------
82-- Building (bigger) vectors
117-- Building (bigger) vectors
@@ -154,9 +189,12 @@ instance Functor (Vect n) where
154-- Folds
189-- Folds
155--------------------------------------------------------------------------------
190--------------------------------------------------------------------------------
156
191
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+
157instance Foldable (Vect n) where
196instance Foldable (Vect n) where
158− foldr f e [] = e
197+ foldr f e xs = foldrImpl f e id xs
159− foldr f e (x::xs) = f x (foldr f e xs)
160
198
161--------------------------------------------------------------------------------
199--------------------------------------------------------------------------------
162-- Special folds
200-- Special folds
@@ -166,25 +204,6 @@ concat : Vect m (Vect n a) -> Vect (m * n) a
166concat [] = []
204concat [] = []
167concat (v::vs) = v ++ concat vs
205concat (v::vs) = v ++ concat vs
168
206
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−
188--------------------------------------------------------------------------------
207--------------------------------------------------------------------------------
189-- Membership tests
208-- Membership tests
190--------------------------------------------------------------------------------
209--------------------------------------------------------------------------------
@@ -349,14 +368,9 @@ Prelude.Vect.drop_lemma_1 = proof {
349 trivial;
368 trivial;
350}
369}
351
370
352−Prelude.Vect.reverse'_lemma_2 = proof {
353− intros;
354− rewrite (plusSuccRightSucc m n1);
355− exact value;
356−}
357−
358Prelude.Vect.reverse'_lemma_1 = proof {
371Prelude.Vect.reverse'_lemma_1 = proof {
359 intros;
372 intros;
373+ rewrite prf;
360 rewrite sym (plusZeroRightNeutral m);
374 rewrite sym (plusZeroRightNeutral m);
361 exact value;
375 exact value;
362}
376}