git.iko.soy/Idris-dev
on master help sign in
Merge pull request #969 from JanBessai/MoreTailRecursion
3a315acEdwin Brady
libs/prelude/Prelude/List.idr+5−2
compare with master
unifiedsplit
@@ -236,9 +236,12 @@ mapMaybe f (x::xs) =
236-- Folds
236-- Folds
237--------------------------------------------------------------------------------
237--------------------------------------------------------------------------------
238
238
239+total foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> List t -> acc
240+foldrImpl f e go [] = go e
241+foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
242+
239instance Foldable List where
243instance Foldable List where
240− foldr f e [] = e
244+ foldr f e xs = foldrImpl f e id xs
241− foldr f e (x::xs) = f x (foldr f e xs)
242
245
243--------------------------------------------------------------------------------
246--------------------------------------------------------------------------------
244-- Special folds
247-- Special folds
libs/prelude/Prelude/Vect.idr+43−29
@@ -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}
test/folding001/expectednew file+4
@@ -0,0 +1,4 @@
1+([], []) -> ([], [])
2+([1], [1]) -> ([1], [1])
3+([1, 2, 3], [1, 2, 3]) -> ([1, 2, 3], [1, 2, 3])
4+([3, 2, 1], [3, 2, 1]) -> ([3, 2, 1], [3, 2, 1])
test/folding001/folding001.idrnew file+23
@@ -0,0 +1,23 @@
1+module Main
2+
3+-- foldr (::) [] converts to lists
4+foldToList : (Foldable t) => t a -> List a
5+foldToList = foldr (::) []
6+
7+showTestLine : List Int -> Vect n Int -> IO ()
8+showTestLine xs ys =
9+ putStrLn $ "(" ++
10+ show xs ++ ", " ++
11+ show ys ++ ") " ++
12+ "-> (" ++
13+ show (foldToList xs) ++ ", " ++
14+ show (foldToList ys) ++ ")"
15+
16+main : IO ()
17+main = do
18+ showTestLine [] []
19+ showTestLine [1] [1]
20+ showTestLine [1, 2, 3] [1, 2, 3]
21+ showTestLine [3, 2, 1] [3, 2, 1]
22+
23+
test/folding001/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+idris $@ folding001.idr -o folding001
3+./folding001
4+rm -f folding001 *.ibc
test/folding002/expectednew file+2
@@ -0,0 +1,2 @@
1+500000500000
2+500000500000
test/folding002/folding002.idrnew file+23
@@ -0,0 +1,23 @@
1+-- perform a very large foldr to test tail recursion
2+addAll : (Foldable t, Num a) => t a -> a
3+addAll = foldr (+) 0
4+
5+n : Integer
6+n = 1000000
7+
8+numbersList : List Bits64
9+numbersList = numbersList' n []
10+ where
11+ numbersList' : Integer -> List Bits64 -> List Bits64
12+ numbersList' 0 xs = xs
13+ numbersList' k xs = numbersList' (k - 1) (fromInteger k :: xs)
14+
15+numbersVect : Vect (length numbersList) Bits64
16+numbersVect = fromList numbersList
17+
18+main : IO ()
19+main = do
20+ putStrLn . show . prim__zextB64_BigInt $ addAll numbersVect
21+ putStrLn . show . prim__zextB64_BigInt $ addAll numbersList
22+
23+
test/folding002/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+idris $@ folding002.idr -o folding002
3+./folding002
4+rm -f folding002 *.ibc