module RedBlackTree where

open import stack

record Tree {a t : Set} (treeImpl : Set) : Set  where
  field
    tree : treeImpl
    put : treeImpl -> a -> (treeImpl -> t) -> t
    get  : treeImpl -> (treeImpl -> Maybe a -> t) -> t

record RedBlackTree (a : Set) : Set where
  field
    top : Maybe (Element a)
    stack : Stack
open RedBlackTree

putRedBlackTree : {Data t : Set} -> RedBlackTree Data -> Data -> (Code : RedBlackTree Data -> t) -> t
putRedBlackTree stack datum next = next newtree
  where
    element = cons datum (top stack)
    newtree  = record {top = Just element}

getRedBlackTree : {a t : Set} -> RedBlackTree a -> (Code : RedBlackTree a -> (Maybe a) -> t) -> t
getRedBlackTree tree cs with (top tree)
...                                | Nothing = cs tree  Nothing
...                                | Just d  = cs stack1 (Just data1)
  where
    data1  = datum d
    stack1 = record { top = (next d) }