------------------------------------------------------------------------
-- The Agda standard library
--
-- The reader monad transformer
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}


module Effect.Monad.Reader.Transformer where

open import Algebra using (RawMonoid)
open import Effect.Choice using (RawChoice)
open import Effect.Empty using (RawEmpty)
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative using (RawApplicative; RawApplicativeZero; RawAlternative)
open import Effect.Monad using (RawMonad; RawMonadZero; RawMonadPlus; RawMonadT)
open import Function.Base using (_∘′_; const; _$_)
open import Level using (Level; _⊔_)

private
  variable
    r g g₁ g₂ : Level
    R R₁ R₂ : Set r
    A B : Set r
    M : Set r → Set g

------------------------------------------------------------------------
-- Re-export the basic type definitions

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

------------------------------------------------------------------------
-- Structure

functor : RawFunctor M → RawFunctor (ReaderT R M)
functor M = record
  { _<$>_ = λ f ma → mkReaderT (λ r → f <$> ReaderT.runReaderT ma r)
  } where open RawFunctor M

applicative : RawApplicative M → RawApplicative (ReaderT R M)
applicative M = record
  { rawFunctor = functor rawFunctor
  ; pure = mkReaderT ∘′ const ∘′ pure
  ; _<*>_ = λ mf mx → mkReaderT (λ r → ReaderT.runReaderT mf r <*> ReaderT.runReaderT mx r)
  } where open RawApplicative M

empty : RawEmpty M → RawEmpty (ReaderT R M)
empty M = record
  { empty = mkReaderT (const (RawEmpty.empty M))
  }

choice : RawChoice M → RawChoice (ReaderT R M)
choice M = record
  { _<|>_ = λ ma₁ ma₂ → mkReaderT $ λ r →
            ReaderT.runReaderT ma₁ r
            <|> ReaderT.runReaderT ma₂ r
  } where open RawChoice M

applicativeZero : RawApplicativeZero M → RawApplicativeZero (ReaderT R M)
applicativeZero M = record
  { rawApplicative = applicative rawApplicative
  ; rawEmpty = empty rawEmpty
  } where open RawApplicativeZero M using (rawApplicative; rawEmpty)

alternative : RawAlternative M → RawAlternative (ReaderT R M)
alternative M = record
  { rawApplicativeZero = applicativeZero rawApplicativeZero
  ; rawChoice = choice rawChoice
  } where open RawAlternative M

monad : RawMonad M → RawMonad (ReaderT R M)
monad M = record
  { rawApplicative = applicative rawApplicative
  ; _>>=_ = λ ma f → mkReaderT $ λ r →
              do a ← ReaderT.runReaderT ma r
                 ReaderT.runReaderT (f a) r
  } where open RawMonad M

monadZero : RawMonadZero M → RawMonadZero (ReaderT R M)
monadZero M = record
  { rawMonad = monad (RawMonadZero.rawMonad M)
  ; rawEmpty = empty (RawMonadZero.rawEmpty M)
  }

monadPlus : RawMonadPlus M → RawMonadPlus (ReaderT R M)
monadPlus M = record
  { rawMonadZero = monadZero rawMonadZero
  ; rawChoice = choice rawChoice
  } where open RawMonadPlus M

------------------------------------------------------------------------
-- Monad reader transformer specifics

monadT : RawMonadT {g₁ = g₁} {g₂ = r ⊔ g₁} (ReaderT {r} R)
monadT M = record
  { lift = mkReaderT ∘′ const
  ; rawMonad = monad M
  }

monadReader : RawMonad M → RawMonadReader R (ReaderT R M)
monadReader M = record
  { reader = λ f → mkReaderT (pure ∘′ f)
  ; local = λ f ma → mkReaderT (ReaderT.runReaderT ma ∘′ f)
  } where open RawMonad M

liftReaderT : RawMonadReader R₁ M →
              RawMonadReader R₁ (ReaderT R₂ M)
liftReaderT MRead = record
  { reader = λ k → mkReaderT (const (reader k))
  ; local = λ f mx → mkReaderT (λ r₂ → local f (runReaderT mx r₂))
  } where open RawMonadReader MRead

open import Data.Product.Base using (_×_; _,_)
open import Effect.Monad.Writer.Transformer.Base

liftWriterT : (MR : RawMonoid r g) →
              RawFunctor M →
              RawMonadReader R M →
              RawMonadReader R (WriterT MR M)
liftWriterT MR M MRead = record
  { reader = λ k → mkWriterT λ w → ((w ,_) <$> reader k)
  ; local = λ f mx → mkWriterT λ w → (local f (runWriterT mx w))
  } where open RawMonadReader MRead
          open RawFunctor M

open import Effect.Monad.State.Transformer.Base

liftStateT : RawFunctor M →
             RawMonadReader R₁ M →
             RawMonadReader R₁ (StateT R₂ M)
liftStateT M MRead = record
  { reader = λ k → mkStateT (λ s → (s ,_) <$> reader k)
  ; local = λ f mx → mkStateT (λ s → local f (runStateT mx s))
  } where open RawMonadReader MRead
          open RawFunctor M