module RedBlackTree where

open import stack
open import Level

record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
  field
    putImpl : treeImpl -> a -> (treeImpl -> t) -> t
    getImpl  : treeImpl -> (treeImpl -> Maybe a -> t) -> t
open TreeMethods

record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
  field
    tree : treeImpl
    treeMethods : TreeMethods {a} {t}
  putTree : a -> (Tree -> t) -> t
  putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} ))
  getTree : (Tree -> Maybe a -> t) -> t
  getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d )

open Tree

data Color : Set where
  Red   : Color
  Black : Color

data CompareResult {n : Level } : Set n where
  LT : CompareResult
  GT : CompareResult
  EQ : CompareResult

record Node (a k : Set) : Set where
  field
    key   : k
    value : a
    right : Maybe (Node a)
    left  : Maybe (Node a)
    color : Color
open Node

record RedBlackTree (a  k si : Set) : Set where
  field
    root : Maybe (Node a k )
    stack : Stack si
    compare : k -> k -> CompareResult

open RedBlackTree

open Stack

insertCase3 : ?
insertCase3 = ? -- tree datum parent grandparent next 

insertCase2 : {n m : Level } {t : Set m } {a : Set n} -> RedBlackTree ? ? -> a (Node a) (Node a) ? -> t
insertCase2 tree datum parent grandparent next with (color parent)
...                                | Red = insertCase3 tree datum parent grandparent next
...                                | Black = next (record { root = ?; stack = createSingleLinkedStack })

insertCase1 : {n m : Level } {t : Set m } {a : Set n} -> RedBlackTree ? ? -> a (Maybe (Node a) ) (Node a) ? -> t
insertCase1 tree datum Nothing grandparent next = next (record { root = ?; stack = createSingleLinkedStack })
insertCase1 tree datum (Just parent) grandparent next = insertCase2 tree datum parent grandparent next

insertNode : ?
insertNode tree datum next = get2Stack (stack tree) (\ s d1 d2 -> insertCase1 ( record { root = root tree; stack = s }) datum d1 d2 next)

findNode1 : {Data t : Set} -> RedBlackTree Data -> Data -> Data -> (Code : RedBlackTree Data (RedBlackTree Data -> t) -> t) -> t
findNode1 tree datum n next with (compare datum n)
...                                | EQ = popStack (tree stack) (\s d -> findNode3 d (record tree { root = just (record n {node = datum}); stack = s }) next)
...                                | GT = findNode2 tree datum (right n) next
...                                | LT = findNode2 tree datum (left n) next
  where
    findNode2 tree datum nothing next = insertNode tree datum next
    findNode2 tree datum (just n) next = findNode (record tree {root = just n}) datum n next
    findNode3 : ?
    findNode3 nothing tree next = next tree
    findNode3 (just n) tree next = 
           popStack (tree stack) (\s d -> findNode3 d (record { root = record n {right = ? } }))

findNode : {Data t : Set} -> RedBlackTree Data -> Data -> Node Data -> (Code : RedBlackTree Data (RedBlackTree Data -> t) -> t) -> t
findNode tree datum n next = pushStack (stack tree) n (\ s -> findNode1 (record tree {stack = s }) datum n next)

putRedBlackTree : {Data t : Set} -> RedBlackTree Data -> Data -> (Code : RedBlackTree Data -> t) -> t
putRedBlackTree tree datum next with (root tree)
...                                | Nothing = insertNode tree datum next
...                                | Just n  = findNode tree datum n (\ tree1 -> insertNode tree1 datum next)

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