```{-# OPTIONS --copatterns --sized-types #-}

module Examples where

open import Library
open import SizedInfiniteTypes
open import Terms

-- * Examples
------------------------------------------------------------------------

-- Example: fixed-point combinator

Fix_ : Ty → ∞Ty
force Fix A = ▸̂ Fix A →̂ A

selfApp : ∀{Γ A} → Tm Γ (▸̂ Fix A) → Tm Γ (▸ A)
selfApp x = ▹app (≅delay ≅refl) x (▹ x)

Y : ∀{Γ A} → Tm Γ ((▸ A →̂ A) →̂ A)
Y = abs (app L (▹ L))
where
f = var (suc v₀)
x = var v₀
L = abs (app f (selfApp x))

-- Alternative definition of selfApp

Fix∞_ : ∞Ty → ∞Ty
force Fix∞ A = ▸̂ Fix∞ A →̂ force A

selfApp' : ∀{Γ a∞} → Tm Γ (▸̂ Fix∞ a∞) → Tm Γ (▸̂ a∞)
selfApp' x = ▹app (≅delay ≅refl) x (▹ x)

-- Y' : ∀{Γ}{a∞ : ∞Ty {∞}} → Tm Γ ((▸̂ a∞ →̂ force a∞) →̂ force a∞)
-- Y' = abs {!(app L {!(▹ L)!})!}
--   where L = abs (app (var (suc zero)) (selfApp (var zero)))

-- Example: Streams

mutual
Stream : Ty → Ty
Stream A = A ×̂ ▸̂ Stream∞ A

Stream∞ : Ty → ∞Ty
force (Stream∞ A) = Stream A

-- Stream constructor

cons : ∀{Γ A} → Tm Γ A → Tm Γ (▸ Stream A) → Tm Γ (Stream A)
cons a s = pair a (cast (▸̂ (≅delay ≅refl)) s)

head : ∀{Γ A} → Tm Γ (Stream A) → Tm Γ A

tail : ∀{Γ A} → Tm Γ (Stream A) → Tm Γ (▸ Stream A)
tail s = cast (▸̂ (≅delay ≅refl)) (snd s)

-- repeat a = (a , ▹ repeat a)
-- repeat = λ a → Y λ f → cons a f

repeat : ∀{Γ A} → Tm Γ (A →̂ Stream A)
repeat = abs (app Y (abs (cons (var (suc v₀)) (var v₀))))

-- smap f s = cons (f (head s)) (smap f (tail s))
-- smap = λ f → Y λ map → λ s → (f (head s), map <*> tail s)

smap : ∀{Γ A B} → Tm Γ ((A →̂ B) →̂ (Stream A →̂ Stream B))
smap = abs (app Y (abs (abs
(let f   = var (suc (suc v₀))
map = var (suc v₀)
s   = var v₀
in pair (app f (head s)) (▹app (≅delay ≅refl) map (tail s))))))

-- zipWith f s t = cons (f (head s) (head t)) (zipWith f (tail s) (tail t))
-- zipWith = λ f → Y λ zipWith → λ s t →
--   (f (head s) (head t) , zipWith <*> tail s <*> tail t)

zipWith : ∀{Γ A B C} → Tm Γ ((A →̂ (B →̂ C)) →̂ (Stream A →̂ (Stream B →̂ Stream C)))
zipWith = abs (app Y (abs (abs (abs
(let f   = var (suc (suc (suc v₀)))
zw  = var (suc (suc v₀))
s   = var (suc v₀)
t   = var v₀
(▹app {c∞ = Stream∞ _ ⇒ Stream∞ _} (≅delay ≅refl)
(▹app (≅delay ≅refl) zw (tail s))
(tail t)))))))

-- Fibonacci stream

module Fib (N : Ty) (n0 n1 : ∀{Γ} → Tm Γ N) (plus : ∀{Γ} → Tm Γ (N →̂ (N →̂  N))) where

-- fib = Y λ fib → cons n0 (▹ (cons n1
--   (zipWith plus <\$> fib <*> (tail <\$> fib)))) -- Ill-typed!
--
-- fib = Y λ fib → cons n0 (cons n1 <\$>
--   ((λ s → (zipWith plus <\$> fib) <*> s) <\$> (tail <\$> fib)))

fib : ∀{Γ} → Tm Γ (Stream N)
fib {Γ} = app Y (abs
(let fib  : Tm (_ ∷ Γ) (▸ Stream N)
fib  = var v₀
fib₁  : Tm (_ ∷ _ ∷ Γ) (▸ Stream N)
fib₁  = var (suc v₀)
adds : Tm (_ ∷ _ ∷ Γ) (Stream N →̂ (Stream N →̂ Stream N))