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

module Copat_size where

open import Data.Nat hiding(fold)
open import Data.Vec hiding(head;tail;take;zipWith)
open import Coinduction hiding(unfold;fold)
open import Size
open import Data.List hiding(take;zipWith;unfold)

open import Data.Product

record Stream {i : Size} (A : Set) : Set where
  coinductive
  constructor _∷_
  field
    head : A
    tail : ∀{j : Size< i} → Stream {j} A
open Stream

infixr 5 _∷_

zeros : ∀{i} → Stream {i} ℕ
head zeros = 0
tail zeros = zeros

--test₁ = 1 ∷ (2 ∷ (3 ∷ test₁))
test₁ : ∀{i} → Stream {i} ℕ
head test₁               = 1
head (tail test₁)        = 2
head (tail (tail test₁)) = 3
tail (tail (tail test₁)) = test₁

stl : ∀{i A} → Stream {↑ i} A → Stream {i} A
stl {i = i} xs = tail {↑ i} xs

--take : ∀{i} {A : Set} → (n : ℕ) → Stream {i} A → Vec A n
take : ∀{A} → (n : ℕ) → Stream A → Vec A n
take 0 xs = []
take {A} (suc n) xs = head xs ∷ take n (tail xs)

zipWith : ∀ {i A B C} → (A → B → C) → Stream {i} A → Stream {i} B → Stream {i} C
head (zipWith f xs ys) = f (head xs) (head ys)
tail (zipWith f xs ys) = zipWith f (tail xs) (tail ys)

fib : ∀{i} → Stream {i} ℕ
head fib = 0
head (tail fib) = 1
tail (tail fib) = zipWith _+_ fib (tail fib)

-- unfold :: (S -> F S) -> S -> Fix F
-- unfold psi x = fmap (unfold psi) (psi x)
unfold : ∀{i} {A S : Set} → (step : S → A × S) → (s : S) → Stream {i} A 
head (unfold step s) = proj₁ (step s)
tail (unfold step s) = unfold step (proj₂ (step s))

nat : Stream ℕ
nat = unfold (λ x → (x , suc x)) 0

coalg : ∀{A B : Set} → (A → B) → Stream A → B × Stream A
coalg f xs = f (head xs) , tail xs

streammap : ∀{A B : Set} → (A → B) → Stream A → Stream B
streammap f = unfold (coalg f)

smap : ∀{A B : Set} → (A → B) → Stream A → Stream B
head (smap f xs) = f (head xs)
tail (smap f xs) = smap f (tail xs)

open import Data.Sum
open import Data.Unit

-- fold :: (F S -> S) -> Fix F -> S
-- fold phi x = phi (map (fold phi) x)
fold : ∀{A S : Set} → (⊤ ⊎ (A × S) → S) → List A → S
fold f []       = f (inj₁ _)
fold f (x ∷ xs) = f (inj₂ (x , fold f xs))

pairsum : ⊤ ⊎ ℕ × ℕ → ℕ
pairsum (inj₂ (x , y)) = x + y
pairsum (inj₁ _) = 0

listsum : List ℕ → ℕ
listsum = fold pairsum

testlist : List ℕ
testlist = 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []

alg : ∀{A B : Set} → (A → B) → ⊤ ⊎ (A × List B) → List B
alg f (inj₁ _) = []
alg f (inj₂ (a , bs)) = f a ∷ bs

listmap : ∀{A B} → (A → B) → List A → List B
listmap f = fold (alg f)

iterate : ∀{A} → (A → A) → A → Stream A
head (iterate f x) = f x
tail (iterate f x) = iterate f (f x)

teststream : Stream ℕ
teststream = iterate (_+_ 1) 0

_∘_ : ∀{A B C : Set} → (B → C) → (A → B) → (A → C)
f ∘ g = λ x → f (g x)

maptest : Stream ℕ
maptest = smap (_+_ 1) (iterate (_+_ 1) 0)

ittest : Stream ℕ
ittest = iterate (_+_ 1) ((_+_ 1) 0)