module IO.Primitive where
open import Data.String hiding (Costring)
open import Data.Char
open import Foreign.Haskell
postulate
IO : Set → Set
{-# COMPILED_TYPE IO IO #-}
infixl 1 _>>=_
postulate
return : ∀ {A} → A → IO A
_>>=_ : ∀ {A B} → IO A → (A → IO B) → IO B
{-# COMPILED return (\_ -> return :: a -> IO a) #-}
{-# COMPILED _>>=_ (\_ _ -> (>>=) :: IO a -> (a -> IO b) -> IO b) #-}
private
Costring = Colist Char
postulate
getContents : IO Costring
readFile : String → IO Costring
writeFile : String → Costring → IO Unit
appendFile : String → Costring → IO Unit
putStr : Costring → IO Unit
putStrLn : Costring → IO Unit
{-# COMPILED getContents getContents #-}
{-# COMPILED readFile readFile #-}
{-# COMPILED writeFile writeFile #-}
{-# COMPILED appendFile appendFile #-}
{-# COMPILED putStr putStr #-}
{-# COMPILED putStrLn putStrLn #-}