-- 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⇓)