------------------------------------------------------------------------
-- 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 Data.Product.Base using (_,_)
open import Effect.Monad.Indexed using (RawIMonad)
open import Function.Base using (const; id; _∘_)
open import Level using (Level; _⊔_; suc)
open import Relation.Binary.PropositionalEquality.Core using (refl)
open import Relation.Unary using (_⊆_; _⇒_; _∈_; _∩_; ｛_｝)
open import Relation.Unary.PredicateTransformer using (Pt)

private
  variable
    i ℓ : Level

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

record RawPMonad {I : Set i} (M : Pt I (i ⊔ ℓ)) : Set (suc (i ⊔ ℓ)) 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