------------------------------------------------------------------------
-- The Agda standard library
--
-- The indexed reader monad
------------------------------------------------------------------------

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

open import Level using (Level; _⊔_; suc; Lift; lift)

module Effect.Monad.Reader.Indexed {r} (R : Set r) (a : Level) where

open import Function.Base using (const; flip; _∘_)
open import Function.Identity.Effectful as Id using (Identity)
open import Effect.Applicative.Indexed
  using (IFun; RawIApplicative; RawIApplicativeZero; RawIAlternative)
open import Effect.Monad.Indexed using (RawIMonad; RawIMonadZero;
  RawIMonadPlus)

private
  variable
     : Level
    A B I : Set 

------------------------------------------------------------------------
-- Indexed reader

IReaderT : IFun I (r  a)  IFun I (r  a)
IReaderT M i j A = R  M i j A

module _ {M : IFun I (r  a)} where

  ----------------------------------------------------------------------
  -- Indexed reader applicative

  ReaderTIApplicative : RawIApplicative M  RawIApplicative (IReaderT M)
  ReaderTIApplicative App = record
    { pure = λ x r  pure x
    ; _⊛_ = λ m n r  m r  n r
    } where open RawIApplicative App

  ReaderTIApplicativeZero : RawIApplicativeZero M 
                            RawIApplicativeZero (IReaderT M)
  ReaderTIApplicativeZero App = record
    { applicative = ReaderTIApplicative applicative
    ;  = const 
    } where open RawIApplicativeZero App

  ReaderTIAlternative : RawIAlternative M  RawIAlternative (IReaderT M)
  ReaderTIAlternative Alt = record
    { applicativeZero = ReaderTIApplicativeZero applicativeZero
    ; _∣_ = λ m n r  m r  n r
    } where open RawIAlternative Alt

  ----------------------------------------------------------------------
  -- Indexed reader monad

  ReaderTIMonad : RawIMonad M  RawIMonad (IReaderT M)
  ReaderTIMonad Mon = record
    { return = λ x r  return x
    ; _>>=_ = λ m f r  m r >>= flip f r
    } where open RawIMonad Mon

  ReaderTIMonadZero : RawIMonadZero M  RawIMonadZero (IReaderT M)
  ReaderTIMonadZero Mon = record
    { monad = ReaderTIMonad monad
    ; applicativeZero = ReaderTIApplicativeZero applicativeZero
    } where open RawIMonadZero Mon

  ReaderTIMonadPlus : RawIMonadPlus M  RawIMonadPlus (IReaderT M)
  ReaderTIMonadPlus Mon = record
    { monad = ReaderTIMonad monad
    ; alternative = ReaderTIAlternative alternative
    } where open RawIMonadPlus Mon

------------------------------------------------------------------------
-- Reader monad operations

record RawIMonadReader {I : Set } (M : IFun I (r  a))
                       : Set (  suc (r  a)) where
  field
    monad  : RawIMonad M
    reader :  {i}  (R  A)  M i i A
    local  :  {i j}  (R  R)  M i j A  M i j A

  open RawIMonad monad public

  ask :  {i}  M i i (Lift (r  a) R)
  ask = reader lift

  asks :  {i}  (R  A)  M i i A
  asks = reader

ReaderTIMonadReader : {I : Set } {M : IFun I (r  a)} 
                      RawIMonad M  RawIMonadReader (IReaderT M)
ReaderTIMonadReader Mon = record
  { monad = ReaderTIMonad Mon
  ; reader = λ f r  return (f r)
  ; local = λ f m  m  f
  } where open RawIMonad Mon