------------------------------------------------------------------------
-- The "always true" predicate, □
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

module Delay-monad.Sized.Always where

open import Prelude

open import Delay-monad.Sized
open import Delay-monad.Sized.Monad

-- The "always true" predicate, □.

mutual

  data  {a p} {A : Size  Set a} (i : Size) (P : A   Set p) :
         Delay A   Set (a  p) where
    □-now   :  {x}  P x   i P (now x)
    □-later :  {x}  ∞□ i P (force x)   i P (later x)

  record ∞□ {a p} {A : Size  Set a} (i : Size) (P : A   Set p)
            (x : Delay A ) : Set (a  p) where
    coinductive
    field
      force : {j : Size< i}   j P x

open ∞□ public

mutual

  -- □ is closed, in a certain sense, under bind.

  □->>= :
     {i a b p q}
      {A : Size  Set a} {B : Size  Set b}
      {P : A   Set p} {Q : B   Set q}
      {x : Delay A } {f :  {i}  A i  Delay B i} 
     i P x  (∀ {x}  P x   i Q (f x))   i Q (x >>= f)
  □->>= (□-now P-x)   □-f = □-f P-x
  □->>= (□-later □-x) □-f = □-later (∞□->>= □-x □-f)

  ∞□->>= :
     {i a b p q}
      {A : Size  Set a} {B : Size  Set b}
      {P : A   Set p} {Q : B   Set q}
      {x : Delay A } {f :  {i}  A i  Delay B i} 
    ∞□ i P x  (∀ {x}  P x   i Q (f x))  ∞□ i Q (x >>= f)
  force (∞□->>= □-x □-f) = □->>= (force □-x) □-f