git.iko.soy/Idris-dev
on master help sign in
Fix deprecation warnings in benchmarks
938e861Echo Nolan
benchmarks/fasta/fasta.idr+3−3
compare with master
unifiedsplit
@@ -31,7 +31,7 @@ splitAt' n s = let s' = unpack s in (pack $ take n s', pack $ drop n s')
31writeAlu : String -> String -> IO ()
31writeAlu : String -> String -> IO ()
32writeAlu name s0 = putStrLn name *> go s0
32writeAlu name s0 = putStrLn name *> go s0
33 where
33 where
34− go "" = return ()
34+ go "" = pure ()
35 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
36
36
37replicate : Int -> Char -> String
37replicate : Int -> Char -> String
@@ -64,7 +64,7 @@ make name n0 tbl seed0 = do
64 lookupTable = Foldable.concat (fill (scanl accum ('a',0) tbl) 0)
64 lookupTable = Foldable.concat (fill (scanl accum ('a',0) tbl) 0)
65
65
66 make' : Int -> Int -> Int -> String -> IO Int
66 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
68 make' n col seed buf = do
68 make' n col seed buf = do
69 let newseed = modInt (seed * 3877 + 29573) modulus
69 let newseed = modInt (seed * 3877 + 29573) modulus
70 let nextchar = strIndex lookupTable newseed
70 let nextchar = strIndex lookupTable newseed
@@ -80,4 +80,4 @@ main = do
80 writeAlu ">ONE Homo sapiens alu" (takeRepeat (fromInteger (cast n)*2) alu)
80 writeAlu ">ONE Homo sapiens alu" (takeRepeat (fromInteger (cast n)*2) alu)
81 nseed <- make ">TWO IUB ambiguity codes" (fromInteger (cast n)*3) iub 42
81 nseed <- make ">TWO IUB ambiguity codes" (fromInteger (cast n)*3) iub 42
82 make ">THREE Homo sapiens frequency" (fromInteger (cast n)*5) homosapiens nseed
82 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
46 let n = fromIntegerNat (the Integer (cast a))
46 let n = fromIntegerNat (the Integer (cast a))
47 let l = str (MkF 1 0 1) 1 n
47 let l = str (MkF 1 0 1) 1 n
48 loop 10 0 l
48 loop 10 0 l
49− return ()
49+ pure ()
50
50
51main : IO ()
51main : IO ()
52main = pidigit
52main = pidigit
benchmarks/quasigroups/Parser.idr+7−7
@@ -14,24 +14,24 @@ Parser : Nat -> Type
14Parser n = Either ParseErr (b : Board n ** LegalBoard b)
14Parser n = Either ParseErr (b : Board n ** LegalBoard b)
15
15
16mapM : Monad m => (a -> m b) -> Vect n a -> m (Vect n b)
16mapM : Monad m => (a -> m b) -> Vect n a -> m (Vect n b)
17−mapM _ Nil = return Vect.Nil
17+mapM _ Nil = pure Vect.Nil
18mapM f (x::xs) = do
18mapM f (x::xs) = do
19 x' <- f x
19 x' <- f x
20 xs' <- mapM f xs
20 xs' <- mapM f xs
21− return (Vect.(::) x' xs')
21+ pure (Vect.(::) x' xs')
22
22
23parseToken : String -> Either String (Cell n)
23parseToken : String -> Either String (Cell n)
24−parseToken "." = return Nothing
24+parseToken "." = pure Nothing
25parseToken "0" = Left "Got cell 0, expected 1-based numbering"
25parseToken "0" = Left "Got cell 0, expected 1-based numbering"
26parseToken x = map Just (tryParseFin ((cast x) - 1))
26parseToken x = map Just (tryParseFin ((cast x) - 1))
27 where
27 where
28 tryParseFin : Int -> Either String (Fin n)
28 tryParseFin : Int -> Either String (Fin n)
29 tryParseFin {n=Z} _ = Left ("Given cell " ++ x ++ " out of range")
29 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
31 tryParseFin {n=S k} x =
31 tryParseFin {n=S k} x =
32 case tryParseFin {n=k} (x-1) of
32 case tryParseFin {n=k} (x-1) of
33 Left err => Left err
33 Left err => Left err
34− Right fin => return (FS fin)
34+ Right fin => pure (FS fin)
35
35
36length : Vect n a -> Nat
36length : Vect n a -> Nat
37length {n=n} _ = n
37length {n=n} _ = n
@@ -45,7 +45,7 @@ parseCols {n=S k} row l cs = helper last l
45 let here = (x, row) -- TODO: Determine why naming this makes idris smarter
45 let here = (x, row) -- TODO: Determine why naming this makes idris smarter
46 tok <- parseToken {n=S k} (index x cs)
46 tok <- parseToken {n=S k} (index x cs)
47 case tok of
47 case tok of
48− Nothing => return (_ ** l)
48+ Nothing => pure (_ ** l)
49 Just t =>
49 Just t =>
50 case legalVal b here t of
50 case legalVal b here t of
51 Yes prf => Right (_ ** Step prf l)
51 Yes prf => Right (_ ** Step prf l)
@@ -79,4 +79,4 @@ parse str =
79 let rows = fromList (lines str) in
79 let rows = fromList (lines str) in
80 case parseRows {n=length rows} emptyBoard Base rows of
80 case parseRows {n=length rows} emptyBoard Base rows of
81 Left msg => Left msg
81 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)
184 | Left full = Just (b ** (l, full))
184 | Left full = Just (b ** (l, full))
185 | Right (coords ** p) = recurse last
185 | Right (coords ** p) = recurse last
186 where
186 where
187− %assert_total
188 tryAll : (v : Fin (S n)) -> (Fin (S n), Maybe (b' : Board (S n) ** LegalBoard b'))
187 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))) $
190 case tryValue l coords p v of
189 case tryValue l coords p v of
191 Right success => (v, Just success)
190 Right success => (v, Just success)
192 Left _ => -- TODO: Prove unsolvable
191 Left _ => -- TODO: Prove unsolvable
@@ -194,9 +193,8 @@ fillBoard {n=(S n)} b l with (emptyCell b)
194 FS k => tryAll (weaken k)
193 FS k => tryAll (weaken k)
195 FZ => (v, Nothing)
194 FZ => (v, Nothing)
196
195
197− %assert_total
198 recurse : Fin (S n) -> Maybe (b' : Board (S n) ** CompleteBoard b')
196 recurse : Fin (S n) -> Maybe (b' : Board (S n) ** CompleteBoard b')
199− recurse start =
197+ recurse start = assert_total $
200 case tryAll start of
198 case tryAll start of
201 (_, Nothing) => Nothing
199 (_, Nothing) => Nothing
202 (FZ, Just (b' ** l')) => fillBoard b' l'
200 (FZ, Just (b' ** l')) => fillBoard b' l'
benchmarks/trivial/sortvec.idr+2−2
@@ -15,8 +15,8 @@ vsort [] = []
15vsort (x :: xs) = insert x (vsort xs)
15vsort (x :: xs) = insert x (vsort xs)
16
16
17mkSortVec : (n : Nat) -> Eff (Vect n Int) [RND]
17mkSortVec : (n : Nat) -> Eff (Vect n Int) [RND]
18−mkSortVec Z = return []
18+mkSortVec Z = pure []
19−mkSortVec (S k) = return (fromInteger !(rndInt 0 10000) :: !(mkSortVec k))
19+mkSortVec (S k) = pure (fromInteger !(rndInt 0 10000) :: !(mkSortVec k))
20
20
21main : IO ()
21main : IO ()
22main = do (_ :: arg :: _) <- getArgs
22main = do (_ :: arg :: _) <- getArgs