------------------------------------------------------------------------
-- Andreas Abel and Brigitte Pientka,
-- Wellfounded Recursion with Copatterns and Sized Types.
--
-- Journal of Functional Programming, volume 26, 2016
--
-- Agda code for examples
------------------------------------------------------------------------

{-# OPTIONS --postfix-projections #-}

module Fibonacci where

open import Prelude

------------------------------------------------------------------------
-- Section 2.1 Example: Fibonacci
------------------------------------------------------------------------

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

zipWith : ∀{i A B C} → (A → B → C) → Stream i A → Stream i B → Stream i C
zipWith f s t .head = f (s .head) (t .head)
zipWith f s t .tail = zipWith f (s .tail) (t .tail)

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