------------------------------------------------------------------------
-- Breadth-first labelling of trees
------------------------------------------------------------------------

-- This module just defines breadth-first labelling. For a full
-- development including a specification and proof, see BreadthFirst.

module BreadthFirstWithoutProof where

open import Coinduction
open import Data.Product
open import Data.Stream

open import Tree using (Tree; leaf; node)

------------------------------------------------------------------------
-- Universe

data U : Set₁ where
  tree   : (a : U)  U
  stream : (a : U)  U
  _⊗_    : (a b : U)  U
  ⌈_⌉    : (A : Set)  U

El : U  Set
El (tree a)   = Tree (El a)
El (stream a) = Stream (El a)
El (a  b)    = El a × El b
El  A       = A

------------------------------------------------------------------------
-- Programs

infixr 5 _∷_
infixr 4 _,_

mutual

  data ElP : U  Set₁ where
       :  {a} (w : ElW a)  ElP a
    fst :  {a b} (p : ElP (a  b))  ElP a
    snd :  {a b} (p : ElP (a  b))  ElP b
    lab :  {A B} (t : Tree A) (bss : ElP (stream  Stream B )) 
          ElP (tree  B   stream  Stream B )

  -- The term WHNF is a bit of a misnomer here; only recursive
  -- /coinductive/ arguments are suspended (in the form of programs).

  data ElW : U  Set₁ where
    leaf :  {a}  ElW (tree a)
    node :  {a}
           (l :  (ElP (tree a))) (x : ElW a) (r :  (ElP (tree a))) 
           ElW (tree a)
    _∷_  :  {a} (x : ElW a) (xs :  (ElP (stream a)))  ElW (stream a)
    _,_  :  {a b} (x : ElW a) (y : ElW b)  ElW (a  b)
    ⌈_⌉  :  {A} (x : A)  ElW  A 

fstW :  {a b}  ElW (a  b)  ElW a
fstW (x , y) = x

sndW :  {a b}  ElW (a  b)  ElW b
sndW (x , y) = y

-- Uses the n-th stream to label the n-th level in the tree. Returns
-- the remaining stream elements (for every level).

labW :  {A B}  Tree A  ElW (stream  Stream B ) 
       ElW (tree  B   stream  Stream B )
labW leaf         bss                = (leaf , bss)
labW (node l _ r) ( b  bs   bss) =
  (node ( fst x)  b  ( fst y) ,   bs    snd y)
  where
  x = lab ( l) ( bss)
  y = lab ( r) (snd x)

whnf :  {a}  ElP a  ElW a
whnf ( w)       = w
whnf (fst p)     = fstW (whnf p)
whnf (snd p)     = sndW (whnf p)
whnf (lab t bss) = labW t (whnf bss)

mutual

  ⟦_⟧W :  {a}  ElW a  El a
   leaf       ⟧W = leaf
   node l x r ⟧W = node (   l ⟧P)  x ⟧W (   r ⟧P)
   x  xs     ⟧W =  x ⟧W     xs ⟧P
   (x , y)    ⟧W = ( x ⟧W ,  y ⟧W)
    x       ⟧W = x

  ⟦_⟧P :  {a}  ElP a  El a
   p ⟧P =  whnf p ⟧W

------------------------------------------------------------------------
-- Breadth-first labelling

label′ :  {A B}  Tree A  Stream B 
         ElP (tree  B   stream  Stream B )
label′ t bs = lab t ( ( bs    snd (label′ t bs)))

label :  {A B}  Tree A  Stream B  Tree B
label t bs =  fst (label′ t bs) ⟧P