1a7d24e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #3400 from enolan/purify-benchmarks

Fix deprecation warnings in benchmarks

commit1a7d24e76501e11cb4bab7471d04718f84e3fc60 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateFri 2 Sep 2016, 09:05 (10 years ago) parent5b2711f 938e861

5 files changed+15−17

compare with master

unifiedsplit

benchmarks/fasta/fasta.idr+3−3 benchmarks/pidigits/pidigits.idr+1−1 benchmarks/quasigroups/Parser.idr+7−7 benchmarks/quasigroups/Solver.idr+2−4 benchmarks/trivial/sortvec.idr+2−2

benchmarks/fasta/fasta.idr+3−3

@@ -31,7 +31,7 @@ splitAt' n s = let s' = unpack s in (pack $ take n s', pack $ drop n s')

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

3232writeAlu name s0 = putStrLn name *> go s0

3333 where

34− go "" = return ()

34+ go "" = pure ()

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

3636

3737replicate : Int -> Char -> String

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

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

6565

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

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

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

6868 make' n col seed buf = do

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

7070 let nextchar = strIndex lookupTable newseed

@@ -80,4 +80,4 @@ main = do

8080 writeAlu ">ONE Homo sapiens alu" (takeRepeat (fromInteger (cast n)*2) alu)

8181 nseed <- make ">TWO IUB ambiguity codes" (fromInteger (cast n)*3) iub 42

8282 make ">THREE Homo sapiens frequency" (fromInteger (cast n)*5) homosapiens nseed

83− return ()

83+ pure ()

benchmarks/pidigits/pidigits.idr+1−1

@@ -46,7 +46,7 @@ pidigit = do

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

4747 let l = str (MkF 1 0 1) 1 n

4848 loop 10 0 l

49− return ()

49+ pure ()

5050

5151main : IO ()

5252main = pidigit

benchmarks/quasigroups/Parser.idr+7−7

@@ -14,24 +14,24 @@ Parser : Nat -> Type

1414Parser n = Either ParseErr (b : Board n ** LegalBoard b)

1515

1616mapM : Monad m => (a -> m b) -> Vect n a -> m (Vect n b)

17−mapM _ Nil = return Vect.Nil

17+mapM _ Nil = pure Vect.Nil

1818mapM f (x::xs) = do

1919 x' <- f x

2020 xs' <- mapM f xs

21− return (Vect.(::) x' xs')

21+ pure (Vect.(::) x' xs')

2222

2323parseToken : String -> Either String (Cell n)

24−parseToken "." = return Nothing

24+parseToken "." = pure Nothing

2525parseToken "0" = Left "Got cell 0, expected 1-based numbering"

2626parseToken x = map Just (tryParseFin ((cast x) - 1))

2727 where

2828 tryParseFin : Int -> Either String (Fin n)

2929 tryParseFin {n=Z} _ = Left ("Given cell " ++ x ++ " out of range")

30− tryParseFin {n=S k} 0 = return FZ

30+ tryParseFin {n=S k} 0 = pure FZ

3131 tryParseFin {n=S k} x =

3232 case tryParseFin {n=k} (x-1) of

3333 Left err => Left err

34− Right fin => return (FS fin)

34+ Right fin => pure (FS fin)

3535

3636length : Vect n a -> Nat

3737length {n=n} _ = n

@@ -45,7 +45,7 @@ parseCols {n=S k} row l cs = helper last l

4545 let here = (x, row) -- TODO: Determine why naming this makes idris smarter

4646 tok <- parseToken {n=S k} (index x cs)

4747 case tok of

48− Nothing => return (_ ** l)

48+ Nothing => pure (_ ** l)

4949 Just t =>

5050 case legalVal b here t of

5151 Yes prf => Right (_ ** Step prf l)

@@ -79,4 +79,4 @@ parse str =

7979 let rows = fromList (lines str) in

8080 case parseRows {n=length rows} emptyBoard Base rows of

8181 Left msg => Left msg

82− Right board => return (_ ** board)

82+ Right board => pure (_ ** board)

benchmarks/quasigroups/Solver.idr+2−4

@@ -184,9 +184,8 @@ fillBoard {n=(S n)} b l with (emptyCell b)

184184 | Left full = Just (b ** (l, full))

185185 | Right (coords ** p) = recurse last

186186 where

187− %assert_total

188187 tryAll : (v : Fin (S n)) -> (Fin (S n), Maybe (b' : Board (S n) ** LegalBoard b'))

189− tryAll v = --trace ("Trying " ++ show (the Int (cast v))) $

188+ tryAll v = assert_total $ --trace ("Trying " ++ show (the Int (cast v))) $

190189 case tryValue l coords p v of

191190 Right success => (v, Just success)

192191 Left _ => -- TODO: Prove unsolvable

@@ -194,9 +193,8 @@ fillBoard {n=(S n)} b l with (emptyCell b)

194193 FS k => tryAll (weaken k)

195194 FZ => (v, Nothing)

196195

197− %assert_total

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

199− recurse start =

197+ recurse start = assert_total $

200198 case tryAll start of

201199 (_, Nothing) => Nothing

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

benchmarks/trivial/sortvec.idr+2−2

@@ -15,8 +15,8 @@ vsort [] = []

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

1616

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

18−mkSortVec Z = return []

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

18+mkSortVec Z = pure []

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

2020

2121main : IO ()

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