5
open import Lib.Prelude
7
{-# IMPORT System.Environment #-}
14
putStrLn : String -> IO Unit
15
putStr : String -> IO Unit
16
bindIO : {A B : Set} -> IO A -> (A -> IO B) -> IO B
17
returnIO : {A : Set} -> A -> IO A
18
getArgs : IO (List String)
19
readFile : FilePath -> IO String
20
writeFile : FilePath -> String -> IO Unit
23
{-# COMPILED_TYPE IO IO #-}
25
{-# COMPILED putStr putStr #-}
26
{-# COMPILED putStrLn putStrLn #-}
27
{-# COMPILED bindIO (\_ _ -> (>>=) :: IO a -> (a -> IO b) -> IO b) #-}
28
{-# COMPILED returnIO (\_ -> return :: a -> IO a) #-}
29
-- we need to throw away the type argument to return and bind
30
-- and resolve the overloading explicitly (since Alonzo
31
-- output is sprinkled with unsafeCoerce#).
32
{-# COMPILED getLine getLine #-}
33
{-# COMPILED getArgs System.Environment.getArgs #-}
34
{-# COMPILED readFile readFile #-}
35
{-# COMPILED writeFile writeFile #-}
37
mapM : {A B : Set} -> (A -> IO B) -> List A -> IO (List B)
38
mapM f [] = returnIO []
39
mapM f (x :: xs) = bindIO (f x) \y -> bindIO (mapM f xs) \ys -> returnIO (y :: ys)
41
mapM₋ : {A : Set} -> (A -> IO Unit) -> List A -> IO Unit
42
mapM₋ f xs = bindIO (mapM f xs) \_ -> returnIO unit