{-# OPTIONS --copatterns #-}

module Copat where

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

record Stream {α} (A : Set α) : Set α where
  coinductive
  constructor _∷_
  field
    head : A
    tail : Stream A
open Stream

infixr 5 _∷_

zeros : Stream ℕ
head zeros = 0
tail zeros = zeros

--test₁ = 1 ∷ 2 ∷ 3 ∷ test₁
test₁ : Stream ℕ
head test₁               = 1
head (tail test₁)        = 2
head (tail (tail test₁)) = 3
tail (tail (tail test₁)) = test₁

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

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

{-# NON_TERMINATING #-}
fib : Stream ℕ
head fib = 0
head (tail fib) = 1
tail (tail fib) = zipWith _+_ fib (tail fib)