------------------------------------------------------------------------
-- The Agda standard library
--
-- The Delay type and some operations
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --sized-types #-}

module Codata.Sized.Delay where

open import Size
open import Codata.Sized.Thunk using (Thunk; force)
open import Codata.Sized.Conat using (Conat; zero; suc; Finite)

open import Data.Empty
open import Relation.Nullary
open import Data.Nat.Base
open import Data.Maybe.Base hiding (map ; fromMaybe ; zipWith ; alignWith ; zip ; align)
open import Data.Product.Base hiding (map ; zip)
open import Data.Sum.Base hiding (map)
open import Data.These.Base using (These; this; that; these)
open import Function.Base using (id)

------------------------------------------------------------------------
-- Definition

data Delay {ℓ} (A : Set ℓ) (i : Size) : Set ℓ where
  now   : A → Delay A i
  later : Thunk (Delay A) i → Delay A i

module _ {ℓ} {A : Set ℓ} where

 length : ∀ {i} → Delay A i → Conat i
 length (now _)   = zero
 length (later d) = suc λ where .force → length (d .force)

 never : ∀ {i} → Delay A i
 never = later λ where .force → never

 fromMaybe : Maybe A → Delay A ∞
 fromMaybe = maybe now never

 runFor : ℕ → Delay A ∞ → Maybe A
 runFor zero    d         = nothing
 runFor (suc n) (now a)   = just a
 runFor (suc n) (later d) = runFor n (d .force)

module _ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} where

 map : (A → B) → ∀ {i} → Delay A i → Delay B i
 map f (now a)   = now (f a)
 map f (later d) = later λ where .force → map f (d .force)

 bind : ∀ {i} → Delay A i → (A → Delay B i) → Delay B i
 bind (now a)   f = f a
 bind (later d) f = later λ where .force → bind (d .force) f

 unfold : (A → A ⊎ B) → A → ∀ {i} → Delay B i
 unfold next seed with next seed
 ... | inj₁ seed′ = later λ where .force → unfold next seed′
 ... | inj₂ b     = now b

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where

 zipWith : (A → B → C) → ∀ {i} → Delay A i → Delay B i → Delay C i
 zipWith f (now a)   d         = map (f a) d
 zipWith f d         (now b)   = map (λ a → f a b) d
 zipWith f (later a) (later b) = later λ where .force → zipWith f (a .force) (b .force)

 alignWith : (These A B → C) → ∀ {i} → Delay A i → Delay B i → Delay C i
 alignWith f (now a)   (now b)   = now (f (these a b))
 alignWith f (now a)   (later _) = now (f (this a))
 alignWith f (later _) (now b)   = now (f (that b))
 alignWith f (later a) (later b) = later λ where
   .force → alignWith f (a .force) (b .force)

module _ {a b} {A : Set a} {B : Set b} where

  zip : ∀ {i} → Delay A i → Delay B i → Delay (A × B) i
  zip   = zipWith _,_

  align : ∀ {i} → Delay A i → Delay B i → Delay (These A B) i
  align = alignWith id

------------------------------------------------------------------------
-- Finite Delays

module _ {ℓ} {A : Set ℓ} where

 infix 3 _⇓
 data _⇓ : Delay A ∞ → Set ℓ where
   now   : ∀ a → now a ⇓
   later : ∀ {d} → d .force ⇓ → later d ⇓

 extract : ∀ {d} → d ⇓ → A
 extract (now a)   = a
 extract (later d) = extract d

 ¬never⇓ : ¬ (never ⇓)
 ¬never⇓ (later p) = ¬never⇓ p

 length-⇓ : ∀ {d} → d ⇓ → Finite (length d)
 length-⇓ (now a)    = zero
 length-⇓ (later d⇓) = suc (length-⇓ d⇓)

module _ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} where

 map-⇓ : ∀ (f : A → B) {d} → d ⇓ → map f d ⇓
 map-⇓ f (now a)   = now (f a)
 map-⇓ f (later d) = later (map-⇓ f d)

 bind-⇓ : ∀ {m} (m⇓ : m ⇓) {f : A → Delay B ∞} → f (extract m⇓) ⇓ → bind m f ⇓
 bind-⇓ (now a)   fa⇓ = fa⇓
 bind-⇓ (later p) fa⇓ = later (bind-⇓ p fa⇓)