------------------------------------------------------------------------
-- 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 BreadthFirst where

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 .label = ss .head .head
bfs ss .tree .left  = bfs (ss .tail) .tree
bfs ss .tree .right = bfs (bfs (ss .tail) .rest) .tree
bfs ss .rest .head  = ss .head. tail
bfs ss .rest .tail  = bfs (bfs (ss .tail) .rest) .rest

-- "Tying the knot"

bfp : ∀{i A} → Stream ∞ A → Result i A
bfp vs = fixR λ r → bfs (cons vs (r .rest))

-- Breadth-first labelling

bf : ∀{i A} → Stream ∞ A → Tree i A
bf vs = bfp vs .tree