------------------------------------------------------------------------
-- The Agda standard library
--
-- The IO monad
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --guardedness #-}

module Effect.Monad.IO where

open import Data.Product.Base using (_,_)
open import Effect.Functor using (RawFunctor)
open import Function.Base using (id)
open import IO.Base using (IO)
open import Level using (Level; suc)

private
  variable
    f g : Level
    A : Set f
    M : Set f → Set g

------------------------------------------------------------------------
-- IO monad operations

record RawMonadIO
       (M : Set f → Set (suc f))
       : Set (suc f) where
  field
    liftIO : IO A → M A

------------------------------------------------------------------------
-- IO monad specifics

monadIO : RawMonadIO {f} IO
monadIO = record { liftIO = id }

open import Effect.Monad.State.Transformer.Base using (StateT; mkStateT)

liftStateT : ∀ {S} → RawFunctor M → RawMonadIO M → RawMonadIO (StateT S M)
liftStateT M MIO = record
  { liftIO = λ io → mkStateT (λ s → (s ,_) <$> liftIO io)
  } where open RawFunctor M; open RawMonadIO MIO

open import Effect.Monad.Reader.Transformer.Base using (ReaderT; mkReaderT)

liftReaderT : ∀ {R} → RawMonadIO M → RawMonadIO (ReaderT R M)
liftReaderT MIO = record
  { liftIO = λ io → mkReaderT (λ r → liftIO io)
  } where open RawMonadIO MIO

open import Effect.Monad.Writer.Transformer.Base using (WriterT; mkWriterT)

liftWriterT : ∀ {f 𝕎} → RawFunctor M → RawMonadIO M → RawMonadIO (WriterT {f = f} 𝕎 M)
liftWriterT M MIO = record
  { liftIO = λ io → mkWriterT (λ w → (w ,_) <$> liftIO io)
  } where open RawFunctor M; open RawMonadIO MIO