```------------------------------------------------------------------------
-- 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 #-}

open import Prelude

------------------------------------------------------------------------
-- Section 2.6 Example: breadth-first labelled infinite trees
------------------------------------------------------------------------

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

-- Infinite node-labelled binary trees

record Tree (i : Size) (A : Set) : Set where
coinductive
field label : ∀{j : Size< i} → A
left  : ∀{j : Size< i} → Tree j A
right : ∀{j : Size< i} → Tree j A
open Tree

-- Stream of streams of labels

SS : (i : Size) (A : Set) → Set
SS i A = Stream i (Stream ∞ A)

-- A particular pair type, just nice names for
-- Tree i A × SS i A

record Result (i : Size) (A : Set) : Set where
field tree : Tree i A
rest : SS i A
open Result

-- A fixed-point combinator for Result
--
-- Here, Agda needs a hint (size for recursive call).

fixR : ∀{i A} → (∀{j} → Result j A → Result (↑ j) A) → Result i A
fixR f .tree .label {j} = f (fixR {j} f) .tree .label
fixR f .tree .left  {j} = f (fixR {j} f) .tree .left
fixR f .tree .right {j} = f (fixR {j} f) .tree .right
fixR f .rest .head  {j} = f (fixR {j} f) .rest .head
fixR f .rest .tail  {j} = f (fixR {j} f) .rest .tail

-- Breadth-first labelling with a stream of streams (nested corecursion)

bfs : ∀{i A} → SS i A → Result i A
bfs ss .tree .left  = bfs (ss .tail) .tree
bfs ss .tree .right = bfs (bfs (ss .tail) .rest) .tree