------------------------------------------------------------------------
-- The Agda standard library
--
-- Monads on indexed sets (predicates)
------------------------------------------------------------------------

-- Note that currently the monad laws are not included here.

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

module Effect.Monad.Predicate where

open import Effect.Applicative.Indexed
open import Effect.Monad
open import Effect.Monad.Indexed
open import Data.Unit
open import Data.Product
open import Function
open import Level
open import Relation.Binary.PropositionalEquality
open import Relation.Unary
open import Relation.Unary.PredicateTransformer using (Pt)

private
  variable
    i ℓ : Level

------------------------------------------------------------------------

record RawPMonad {I : Set i} (M : Pt I (i ⊔ ℓ)) : Set (suc i ⊔ suc ℓ) where

  infixl  _?>=_ _?>_ _>?>_
  infixr  _=<?_ _<?<_

  -- ``Demonic'' operations (the opponent chooses the state).

  field
    return? : ∀ {P} → P ⊆ M P
    _=<?_   : ∀ {P Q} → P ⊆ M Q → M P ⊆ M Q

  _?>=_ : ∀ {P Q} → M P ⊆ const (P ⊆ M Q) ⇒ M Q
  m ?>= f = f =<? m

  _?>=′_ : ∀ {P Q} → M P ⊆ const (∀ j → {_ : P j} → j ∈ M Q) ⇒ M Q
  m ?>=′ f = m ?>= λ {j} p → f j {p}

  _?>_ : ∀ {P Q} → M P ⊆ const (∀ {j} → j ∈ M Q) ⇒ M Q
  m₁ ?> m₂ = m₁ ?>= λ _ → m₂

  join? : ∀ {P} → M (M P) ⊆ M P
  join? m = m ?>= id

  _>?>_ : {P Q R : _} → P ⊆ M Q → Q ⊆ M R → P ⊆ M R
  f >?> g = _=<?_ g ∘ f

  _<?<_ : ∀ {P Q R} → Q ⊆ M R → P ⊆ M Q → P ⊆ M R
  g <?< f = f >?> g

  -- ``Angelic'' operations (the player knows the state).

  rawIMonad : RawIMonad (λ i j A → i ∈ M (const A ∩ ｛ j ｝))
  rawIMonad = record
    { return = λ x → return? (x , refl)
    ; _>>=_  = λ m k → m ?>= λ { {._} (x , refl) → k x }
    }

  open RawIMonad rawIMonad public