git.iko.soy/Idris-dev
on master help sign in
Tests for tail recursive implementations of foldr
9b28ec3Jan Bessai
test/folding001/expectednew file+4
compare with master
unifiedsplit
@@ -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