------------------------------------------------------------------------
-- IO
------------------------------------------------------------------------

{-# 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

------------------------------------------------------------------------
-- The IO monad

-- One cannot write "infinitely large" computations with the
-- postulated IO monad in IO.Primitive without turning off the
-- termination checker (or going via the FFI, or perhaps abusing
-- something else). The following coinductive deep embedding is
-- introduced to avoid this problem. Possible non-termination is
-- isolated to the run function below.

infixl  _>>=_ _>>_

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

-- The use of abstract ensures that the run function will not be
-- unfolded infinitely by the type checker.

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₂)

------------------------------------------------------------------------
-- Utilities

-- Because IO A lives in Set₁ I hesitate to define sequence, which
-- would require defining a Set₁ variant of Colist.

mapM : ∀ {A B} → (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))

-- The reason for not defining mapM′ in terms of mapM is efficiency
-- (the unused results could cause unnecessary memory use).

mapM′ : ∀ {A B} → (A → IO B) → Colist A → IO ⊤
mapM′ f []       = return _
mapM′ f (x ∷ xs) = ♯₁ f x >> ♯₁ mapM′ f (♭ xs)

------------------------------------------------------------------------
-- Simple lazy IO (UTF8-based)

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)

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)