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