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

.travis.yml+1

compare with master

unifiedsplit

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

107 echo "make -j2 $test";

108 make -j2 $test;

109 done

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

benchmarks/fasta/fasta.idr+9−10

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

1module Main

2

3import System

4−import Data.Floats

5

4

6alu : String

5alu : String

7alu = "GGCCGGGCGCGGTGGCTCACGCCTGTAATCCCAGCACTTTGGGAGGCCGAGGCGGGCGGATCACCTGAGG\

6alu = "GGCCGGGCGCGGTGGCTCACGCCTGTAATCCCAGCACTTTGGGAGGCCGAGGCGGGCGGATCACCTGAGG\

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

9 \CGTGGTGGCGCGCGCCTGTAATCCCAGCTACTCGGGAGGCTGAGGCAGGAGAATCGCTTGAACCCGGGAGGC\

8 \CGTGGTGGCGCGCGCCTGTAATCCCAGCTACTCGGGAGGCTGAGGCAGGAGAATCGCTTGAACCCGGGAGGC\

10 \GGAGGTTGCAGTGAGCCGAGATCGCGCCACTGCACTCCAGCCTGGGCGACAGAGCGAGACTCCGTCTCAAAAA"

9 \GGAGGTTGCAGTGAGCCGAGATCGCGCCACTGCACTCCAGCCTGGGCGACAGAGCGAGACTCCGTCTCAAAAA"

11

10

12−iub : List (Char, Float)

11+iub : List (Char, Double)

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

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

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

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

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

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

16

15

17−homosapiens : List (Char, Float)

16+homosapiens : List (Char, Double)

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

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

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

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

20

19

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

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

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

31

30

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

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

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

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

34 where

33 where

35 go "" = return ()

34 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

37

36

38replicate : Int -> Char -> String

37replicate : Int -> Char -> String

39replicate 0 c = ""

38replicate 0 c = ""

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

44 [] => []

43 [] => []

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

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

46

45

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

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

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

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

49

48

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

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

51make name n0 tbl seed0 = do

50make name n0 tbl seed0 = do

52 putStrLn name

51 putStrLn name

53 make' n0 0 seed0 ""

52 make' n0 0 seed0 ""

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

55 modulus : Int

54 modulus : Int

56 modulus = 139968

55 modulus = 139968

57

56

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

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

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

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

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

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

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

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

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

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

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

66

65

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

66 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

69 make' n col seed buf = do

68 make' n col seed buf = do

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

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

71 let nextchar = strIndex lookupTable newseed

70 let nextchar = strIndex lookupTable newseed

72 let newbuf = buf <+> singleton nextchar

71 let newbuf = buf <+> singleton nextchar

73 if col+1 >= 60

72 if col+1 >= 60

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

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

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

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

76

75

77

76

benchmarks/pidigits/pidigits.idr+10−10

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

1import System

2+import Data.Vect

2

3

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

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

4

5

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

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

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

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

7

8

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

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

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

10

11

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.

12 It almost runs in constant space.

13 It almost runs in constant space.

13-}

14-}

14

15

15−data F = mkF Integer Integer Integer

16+data F = MkF Integer Integer Integer

16

17

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

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

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

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

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

23 loop k (S k') xs

24 loop k (S k') xs

24

25

25fn : Integer -> F

26fn : Integer -> F

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

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

27

28

28flr : Integer -> F -> Integer

29flr : 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

30

31

31comp : F -> F -> F

32comp : 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)

33

34

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

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

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

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

36str _ _ Z = Nil

37str _ _ Z = Nil

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

38str 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

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

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

40 where y = flr 3 z

41 where y = flr 3 z

41

42

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

43pidigit = do

44pidigit = do

44 [_,a] <- getArgs

45 [_,a] <- getArgs

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

46 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

47 loop 10 0 l

48 loop 10 0 l

48 return ()

49 return ()

49

50

50main : IO ()

51main : IO ()

51main = pidigit

52main = pidigit

52−

benchmarks/quasigroups/Main.idr+14−11

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

10 case args of

11 [_, path] => do

12 f <- readFile path

13+ case f of

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

15+ Right f' =>

13− case parse f of

16+ case parse f' of

14− Left err => putStrLn err

17+ Left err => putStrLn err

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

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

16− putStrLn "Got board:"

19+ putStrLn "Got board:"

17− printLn board

20+ printLn board

18− putStrLn "Solving..."

21+ putStrLn "Solving..."

19− case fillBoard board legal of

22+ case fillBoard board legal of

20− Nothing => putStrLn "No solution found"

23+ Nothing => putStrLn "No solution found"

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

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

22− putStrLn "Solution found:"

25+ putStrLn "Solution found:"

23− printLn solved

26+ printLn solved

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

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

benchmarks/quasigroups/Parser.idr+3−2

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

1module Parser

2

3import Decidable.Equality

4+import Data.Vect

4

5

5import Solver

6import Solver

6

7

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

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

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

62 step i l =

63 step i l =

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

64 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

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

66 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)

67

68

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

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

69 helper FZ l = step FZ l

70 helper FZ l = step FZ l

benchmarks/quasigroups/Solver.idr+3−2

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

2

3import Decidable.Equality

4import Control.Monad.State

5+import Data.Vect

5import Data.Vect.Quantifiers

6import Data.Vect.Quantifiers

6

7

7%default total

8%default total

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

95 case colSafe b x v of

96 case colSafe b x v of

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

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

97 Yes prf' =>

98 Yes prf' =>

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

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

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

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

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

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

101

102

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

194

195

195 %assert_total

196 %assert_total

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

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

197− recurse start =

198+ recurse start =

198 case tryAll start of

199 case tryAll start of

199 (_, Nothing) => Nothing

200 (_, Nothing) => Nothing

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

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

benchmarks/trivial/sortvec.idr+4−3

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

1module Main

2

3import System

4+import Effects

4import Effect.Random

5import Effect.Random

6+import Data.Vect

5

7

6total

8total

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

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

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

12vsort [] = []

14vsort [] = []

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

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

14

16

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

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

16mkSortVec Z = return []

18mkSortVec Z = return []

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

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

18

20

19main : IO ()

21main : IO ()

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

22main = 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)))

23 putStrLn "Made vector"

24 putStrLn "Made vector"

24 printLn (vsort vec)

25 printLn (vsort vec)