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 {n} {m} {a} {t} treeImpl
  putTree : a -> (Tree treeImpl -> t) -> t
  putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} ))
  getTree : (Tree treeImpl -> Maybe a -> t) -> t
  getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d )

open Tree

data Color {n : Level } : Set n where
  Red   : Color
  Black : Color

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

record Node {n : Level } (a k : Set n) : Set n where
  inductive
  field
    key   : k
    value : a
    right : Maybe (Node a k)
    left  : Maybe (Node a k)
    color : Color {n}
open Node

Stak : {n m : Level }  (a k : Set n) (t : Set m ) -> Set (m ⊔ n)
Stak {n} {m} a k t = Stack {n} {m} (Node a k) {t} (SingleLinkedStack (Node a k))
open Stack

record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.⊔ n) where
  field
    root : Maybe (Node a k)
    nodeStack :  Stak a k t 
    compare : k -> k -> CompareResult {n}

open RedBlackTree



--
-- put new node at parent node, and rebuild tree to the top
--
{-# TERMINATING #-}   -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html
replaceNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k  -> Stak a k t -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k  -> t) -> t
replaceNode {n} {m} {t} {a} {k} tree s parent n0 next = popStack s (
      \s grandParent -> replaceNode1 s grandParent ( compare tree (key parent) (key n0) ) )
  where
        replaceNode1 : Stak a k t -> Maybe ( Node a k ) -> CompareResult -> t
        replaceNode1 s Nothing LT = next ( record tree { root = Just ( record parent { left = Just n0 ; color = Black } ) } )   
        replaceNode1 s Nothing GT = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } )   
        replaceNode1 s Nothing EQ = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } )   
        replaceNode1 s (Just grandParent) result with result
        ... | LT =  replaceNode tree s grandParent ( record parent { left = Just n0 } ) next
        ... | GT =  replaceNode tree s grandParent ( record parent { right = Just n0 } ) next
        ... | EQ =  next tree 

rotateRight : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
rotateRight {n} {m} {t} {a} {k}  tree s n0 parent grandParent next = {!!}

rotateLeft : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
rotateLeft {n} {m} {t} {a} {k}  tree s n0 parent grandParent next = {!!}

insertCase5 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
insertCase5 {n} {m} {t} {a} {k}  tree s n0 parent grandParent next = {!!}

insertCase4 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
insertCase4 {n} {m} {t} {a} {k}  tree s n0 parent grandParent next = {!!}

{-# TERMINATING #-}
insertNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> (RedBlackTree {n} {m} {t} a k -> t) -> t
insertNode {n} {m} {t} {a} {k}  tree s n0 next = get2Stack s (\ s d1 d2 -> insertCase1 s n0 d1 d2 )
   where
    insertCase1 : Stack (Node a k) (SingleLinkedStack (Node a k)) -> Node a k -> Maybe (Node a k) -> Maybe (Node a k) -> t    -- placed here to allow mutual recursion
          -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html
    insertCase3 : Stak a k t -> Node a k -> Node a k -> Node a k -> t
    insertCase3 s n0 parent grandParent with left grandParent | right grandParent
    ... | Nothing | Nothing = insertCase4 tree s n0 parent grandParent next
    ... | Nothing | Just uncle  = insertCase4 tree s n0 parent grandParent next
    ... | Just uncle | _  with compare tree ( key uncle ) ( key parent )
    ...                   | EQ =  insertCase4 tree s n0 parent grandParent next
    ...                   | _ with color uncle
    ...                           | Red = pop2Stack s ( \s p0 p1 -> insertCase1 s ( 
           record grandParent { color = Red ; left = Just ( record parent { color = Black ; left = Just n0 } )  ; right = Just ( record uncle { color = Black } ) }) p0 p1 )
    ...                           | Black = insertCase4 tree s n0 parent grandParent next
    insertCase2 : Stak a k t -> Node a k -> Node a k -> Node a k -> t
    insertCase2 s n0 parent grandParent with color parent
    ... | Black = replaceNode tree s grandParent n0 next
    ... | Red = insertCase3 s n0 parent grandParent
    insertCase1 s n0 Nothing Nothing = next tree
    insertCase1 s n0 Nothing (Just grandParent) = replaceNode tree s grandParent n0 next
    insertCase1 s n0 (Just grandParent) Nothing = replaceNode tree s grandParent n0 next
    insertCase1 s n0 (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent
      where

findNode : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> Stak a k t -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k -> Stak a k t -> Node a k -> t) -> t
findNode {n} {m} {a} {k}  {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1)
  where
    findNode2 : Stak a k t -> (Maybe (Node a k)) -> t
    findNode2 s Nothing = next tree s n0
    findNode2 s (Just n) = findNode tree s n0 n next
    findNode1 : Stak a k t -> (Node a k)  -> t
    findNode1 s n1 with (compare tree (key n0) (key n1))
    ...                                | EQ = next tree s n0 
    ...                                | GT = findNode2 s (right n1)
    ...                                | LT = findNode2 s (left n1)


leafNode : {n : Level } {a k : Set n}  -> k -> a -> Node a k
leafNode k1 value = record {
    key   = k1 ;
    value = value ;
    right = Nothing ;
    left  = Nothing ;
    color = Black 
  }

putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree a k  -> k -> a -> (RedBlackTree a k  -> t) -> t
putRedBlackTree {n} {m} {a} {k}  {t} tree k1 value next with (root tree)
...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
...                                | Just n2  = findNode tree (nodeStack tree) (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)

getRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k  -> k -> (RedBlackTree a k  -> (Maybe (Node a k)) -> t) -> t
getRedBlackTree {_} {_} {a} {k} {t} tree k1 cs = checkNode (root tree)
  where
    checkNode : Maybe (Node a k) -> t
    checkNode Nothing = cs tree Nothing
    checkNode (Just n) = search n
      where
        search : Node a k -> t
        search n with compare tree k1 (key n)
        search n | LT = checkNode (left n)
        search n | GT = checkNode (right n)
        search n | EQ = cs tree (Just n)