79ff02f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2883 from paulkoerbitz/2819-fix-benchmarks

2819 fix benchmarks

commit79ff02f1a7fe94b665c09afcebe757ab4d8ffe24 authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateTue 5 Jan 2016, 09:50 (11 years ago) parentf6f97eb 665c467

7 files changed+44−38

compare with master

unifiedsplit

.travis.yml+1 benchmarks/fasta/fasta.idr+9−10 benchmarks/pidigits/pidigits.idr+10−10 benchmarks/quasigroups/Main.idr+14−11 benchmarks/quasigroups/Parser.idr+3−2 benchmarks/quasigroups/Solver.idr+3−2 benchmarks/trivial/sortvec.idr+4−3

.travis.yml+1

@@ -107,3 +107,4 @@ script:

107107 echo "make -j2 $test";

108108 make -j2 $test;

109109 done

110+ - cd benchmarks && ./build.pl && ./run.pl && cd ..

benchmarks/fasta/fasta.idr+9−10

@@ -1,7 +1,6 @@

11module Main

33import System

4−import Data.Floats

65alu : String

76alu = "GGCCGGGCGCGGTGGCTCACGCCTGTAATCCCAGCACTTTGGGAGGCCGAGGCGGGCGGATCACCTGAGG\

@@ -9,12 +8,12 @@ alu = "GGCCGGGCGCGGTGGCTCACGCCTGTAATCCCAGCACTTTGGGAGGCCGAGGCGGGCGGATCACCTGAGG\

98 \CGTGGTGGCGCGCGCCTGTAATCCCAGCTACTCGGGAGGCTGAGGCAGGAGAATCGCTTGAACCCGGGAGGC\

109 \GGAGGTTGCAGTGAGCCGAGATCGCGCCACTGCACTCCAGCCTGGGCGACAGAGCGAGACTCCGTCTCAAAAA"

1110

12−iub : List (Char, Float)

11+iub : List (Char, Double)

1312iub = [('a',0.27),('c',0.12),('g',0.12),('t',0.27),('B',0.02)

1413 ,('D',0.02),('H',0.02),('K',0.02),('M',0.02),('N',0.02)

1514 ,('R',0.02),('S',0.02),('V',0.02),('W',0.02),('Y',0.02)]

1615

17−homosapiens : List (Char, Float)

16+homosapiens : List (Char, Double)

1817homosapiens = [('a',0.3029549426680),('c',0.1979883004921)

1918 ,('g',0.1975473066391),('t',0.3015094502008)]

2019

@@ -30,10 +29,10 @@ splitAt' : Nat -> String -> (String, String)

3029splitAt' n s = let s' = unpack s in (pack $ take n s', pack $ drop n s')

3130

3231writeAlu : String -> String -> IO ()

33−writeAlu name s0 = putStrLn name $> go s0

32+writeAlu name s0 = putStrLn name *> go s0

3433 where

3534 go "" = return ()

36− go s = let (h,t) = splitAt' 60 s in putStrLn h $> go t

35+ go s = let (h,t) = splitAt' 60 s in putStrLn h *> go t

3736

3837replicate : Int -> Char -> String

3938replicate 0 c = ""

@@ -44,10 +43,10 @@ scanl f q ls = q :: (case ls of

4443 [] => []

4544 x::xs => scanl f (f q x) xs)

4645

47−accum : (Char,Float) -> (Char,Float) -> (Char,Float)

46+accum : (Char,Double) -> (Char,Double) -> (Char,Double)

4847accum (_,p) (c,q) = (c,p+q)

4948

50−make : String -> Int -> List (Char, Float) -> Int -> IO Int

49+make : String -> Int -> List (Char, Double) -> Int -> IO Int

5150make name n0 tbl seed0 = do

5251 putStrLn name

5352 make' n0 0 seed0 ""

@@ -55,7 +54,7 @@ make name n0 tbl seed0 = do

5554 modulus : Int

5655 modulus = 139968

5756

58− fill : List (Char,Float) -> Int -> List String

57+ fill : List (Char,Double) -> Int -> List String

5958 fill ((c,p) :: cps) j =

6059 let k = min modulus (cast (cast modulus * p + 1))

6160 in replicate (k - j) c :: fill cps k

@@ -65,13 +64,13 @@ make name n0 tbl seed0 = do

6564 lookupTable = Foldable.concat (fill (scanl accum ('a',0) tbl) 0)

6665

6766 make' : Int -> Int -> Int -> String -> IO Int

68− make' 0 col seed buf = when (col > 0) (putStrLn buf) $> return seed

67+ make' 0 col seed buf = when (col > 0) (putStrLn buf) *> return seed

6968 make' n col seed buf = do

7069 let newseed = modInt (seed * 3877 + 29573) modulus

7170 let nextchar = strIndex lookupTable newseed

7271 let newbuf = buf <+> singleton nextchar

7372 if col+1 >= 60

74− then putStrLn newbuf $> make' (n-1) 0 newseed ""

73+ then putStrLn newbuf *> make' (n-1) 0 newseed ""

7574 else make' (n-1) (col+1) newseed newbuf

7675

7776

benchmarks/pidigits/pidigits.idr+10−10

@@ -1,18 +1,19 @@

11import System

2+import Data.Vect

34{- Toy program that outputs the n first digits of Pi.

5− Inspired from http://www.haskell.org/haskellwiki/Shootout/Pidigits.

6+ Inspired from http://www.haskell.org/haskellwiki/Shootout/Pidigits.

67 The original ns and str lazy lists have been replaced by strict functions.

8− Memory usage seems to be excessive. One of the branches of str is tail recursive, and

9+ Memory usage seems to be excessive. One of the branches of str is tail recursive, and

910 the other one only needs to cons an extra Integer.

1011

11− For reference, the Haskell version runs in 0m0.230s when printing to /dev/null.

12+ For reference, the Haskell version runs in 0m0.230s when printing to /dev/null.

1213 It almost runs in constant space.

1314-}

1415

15−data F = mkF Integer Integer Integer

16+data F = MkF Integer Integer Integer

1617

1718-- Prints the list of digits by groups of 10

1819loop : Nat -> Nat -> List Integer -> IO()

@@ -23,19 +24,19 @@ loop (S k) k' (x::xs) = do putStr (show x)

2324 loop k (S k') xs

2425

2526fn : Integer -> F

26−fn k = mkF k (4*k+2) (2*k+1)

27+fn k = MkF k (4*k+2) (2*k+1)

2728

2829flr : Integer -> F -> Integer

29−flr x (mkF q r t) = (q*x + r) `div` t

30+flr x (MkF q r t) = (q*x + r) `div` t

3031

3132comp : F -> F -> F

32−comp (mkF q r t) (mkF u v x) = mkF (q*u) (q*v+r*x) (t*x)

33+comp (MkF q r t) (MkF u v x) = MkF (q*u) (q*v+r*x) (t*x)

3334

3435-- Returns the list of digits of pi. Memory hungry.

3536str : F -> Integer -> Nat -> List Integer

3637str _ _ Z = Nil

3738str z k (S n) = if(y == flr 4 z)

38− then y :: str (comp (mkF 10 (-10*y) 1) z ) k n

39+ then y :: str (comp (MkF 10 (-10*y) 1) z ) k n

3940 else str (comp z (fn k)) (k+1) (S n)

4041 where y = flr 3 z

4142

@@ -43,10 +44,9 @@ pidigit : IO()

4344pidigit = do

4445 [_,a] <- getArgs

4546 let n = fromIntegerNat (the Integer (cast a))

46− let l = str (mkF 1 0 1) 1 n

47+ let l = str (MkF 1 0 1) 1 n

4748 loop 10 0 l

4849 return ()

4950

5051main : IO ()

5152main = pidigit

52−

benchmarks/quasigroups/Main.idr+14−11

@@ -10,15 +10,18 @@ main = do

1010 case args of

1111 [_, path] => do

1212 f <- readFile path

13− case parse f of

14− Left err => putStrLn err

15− Right (_ ** (board ** legal)) => do

16− putStrLn "Got board:"

17− printLn board

18− putStrLn "Solving..."

19− case fillBoard board legal of

20− Nothing => putStrLn "No solution found"

21− Just (solved ** _) => do

22− putStrLn "Solution found:"

23− printLn solved

13+ case f of

14+ Left _err => putStrLn $ "Error reading file: " ++ path

15+ Right f' =>

16+ case parse f' of

17+ Left err => putStrLn err

18+ Right (_ ** (board ** legal)) => do

19+ putStrLn "Got board:"

20+ printLn board

21+ putStrLn "Solving..."

22+ case fillBoard board legal of

23+ Nothing => putStrLn "No solution found"

24+ Just (solved ** _) => do

25+ putStrLn "Solution found:"

26+ printLn solved

2427 [self] => putStrLn ("Usage: " ++ self ++ " <board file>")

benchmarks/quasigroups/Parser.idr+3−2

@@ -1,6 +1,7 @@

11module Parser

33import Decidable.Equality

4+import Data.Vect

56import Solver

@@ -61,9 +62,9 @@ parseRows {n=S k} _ l rs = helper last l

6162 step : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)

6263 step i l =

6364 let cs = fromList (words (index i rs)) in

64− case decEq (length cs) (S k) of

65+ case decEq (Parser.length cs) (S k) of

6566 No _ => Left "Row length not equal to column height"

66− Yes prf => let foo = (replace {P=\n => Vect n String} prf cs) in parseCols i l foo -- TODO: foo shouldn't be needed

67+ Yes prf => parseCols i l (replace {P=\n => Vect n String} prf cs)

6768

6869 helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)

6970 helper FZ l = step FZ l

benchmarks/quasigroups/Solver.idr+3−2

@@ -2,6 +2,7 @@ module Solver

33import Decidable.Equality

44import Control.Monad.State

5+import Data.Vect

56import Data.Vect.Quantifiers

78%default total

@@ -95,7 +96,7 @@ legalVal b (x, y) v =

9596 case colSafe b x v of

9697 No prf' => No (\(_, cf, _) => prf' cf)

9798 Yes prf' =>

98− case empty (getCell b (x, y)) of

99+ case Solver.empty (getCell b (x, y)) of

99100 No prf'' => No (\(ef, _, _) => prf'' ef)

100101 Yes prf'' => Yes (prf'', prf', prf)

101102

@@ -194,7 +195,7 @@ fillBoard {n=(S n)} b l with (emptyCell b)

194195

195196 %assert_total

196197 recurse : Fin (S n) -> Maybe (b' : Board (S n) ** CompleteBoard b')

197− recurse start =

198+ recurse start =

198199 case tryAll start of

199200 (_, Nothing) => Nothing

200201 (FZ, Just (b' ** l')) => fillBoard b' l'

benchmarks/trivial/sortvec.idr+4−3

@@ -1,7 +1,9 @@

11module Main

33import System

4+import Effects

45import Effect.Random

6+import Data.Vect

68total

79insert : Ord a => a -> Vect n a -> Vect (S n) a

@@ -12,13 +14,12 @@ vsort : Ord a => Vect n a -> Vect n a

1214vsort [] = []

1315vsort (x :: xs) = insert x (vsort xs)

1416

15−mkSortVec : (n : Nat) -> Eff m [RND] (Vect n Int)

17+mkSortVec : (n : Nat) -> Eff (Vect n Int) [RND]

1618mkSortVec Z = return []

1719mkSortVec (S k) = return (fromInteger !(rndInt 0 10000) :: !(mkSortVec k))

1820

1921main : IO ()

2022main = do (_ :: arg :: _) <- getArgs

21−-- let arg = "2000"

22− let vec = runPure [123456789] (mkSortVec (fromInteger (cast arg)))

23+ let vec = runPure $ (srand 123456789 *> mkSortVec (fromInteger (cast arg)))

2324 putStrLn "Made vector"

2425 printLn (vsort vec)