{-# OPTIONS --no-termination-check #-}
module IO where
open import Coinduction
open import Data.Unit
open import Data.String
open import Data.Colist
import Foreign.Haskell as Haskell
import IO.Primitive as Prim
infixl 1 _>>=_ _>>_
data IO : Set → Set₁ where
lift : ∀ {A} (m : Prim.IO A) → IO A
return : ∀ {A} (x : A) → IO A
_>>=_ : ∀ {A B} (m : ∞ (IO A)) (f : (x : A) → ∞ (IO B)) → IO B
_>>_ : ∀ {A B} (m₁ : ∞ (IO A)) (m₂ : ∞ (IO B)) → IO B
abstract
run : ∀ {A} → IO A → Prim.IO A
run (lift m) = m
run (return x) = Prim.return x
run (m >>= f) = Prim._>>=_ (run (♭ m )) λ x → run (♭ (f x))
run (m₁ >> m₂) = Prim._>>=_ (run (♭ m₁)) λ _ → run (♭ m₂)
mapM : {A B : Set} → (A → IO B) → Colist A → IO (Colist B)
mapM f [] = return []
mapM f (x ∷ xs) = ♯ f x >>= λ y →
♯ (♯ mapM f (♭ xs) >>= λ ys →
♯ return (y ∷ ♯ ys))
mapM′ : {A B : Set} → (A → IO B) → Colist A → IO ⊤
mapM′ f [] = return _
mapM′ f (x ∷ xs) = ♯ f x >> ♯ mapM′ f (♭ xs)
getContents : IO Costring
getContents =
♯ lift Prim.getContents >>= λ s →
♯ return (Haskell.toColist s)
readFile : String → IO Costring
readFile f =
♯ lift (Prim.readFile f) >>= λ s →
♯ return (Haskell.toColist s)
writeFile∞ : String → Costring → IO ⊤
writeFile∞ f s =
♯ lift (Prim.writeFile f (Haskell.fromColist s)) >>
♯ return _
writeFile : String → String → IO ⊤
writeFile f s = writeFile∞ f (toCostring s)
appendFile∞ : String → Costring → IO ⊤
appendFile∞ f s =
♯ lift (Prim.appendFile f (Haskell.fromColist s)) >>
♯ return _
appendFile : String → String → IO ⊤
appendFile f s = appendFile∞ f (toCostring s)
putStr∞ : Costring → IO ⊤
putStr∞ s =
♯ lift (Prim.putStr (Haskell.fromColist s)) >>
♯ return _
putStr : String → IO ⊤
putStr s = putStr∞ (toCostring s)
putStrLn∞ : Costring → IO ⊤
putStrLn∞ s =
♯ lift (Prim.putStrLn (Haskell.fromColist s)) >>
♯ return _
putStrLn : String → IO ⊤
putStrLn s = putStrLn∞ (toCostring s)