{-# 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)