module RedBlackTree where


open import Level hiding (zero)

open import Data.Nat hiding (compare)
open import Data.Nat.Properties as NatProp
open import Data.Maybe
-- open import Data.Bool
open import Data.Empty

open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open import logic

open import stack

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


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

record RedBlackTree {n m : Level } {t : Set m} (a : Set n) : Set (m Level.⊔ n) where
  field
    root : Maybe (Node a )
    nodeStack : SingleLinkedStack  (Node a )

open RedBlackTree

open SingleLinkedStack

compTri : ( x y : ℕ ) ->  Tri ( x < y )  ( x ≡ y )  ( x > y )
compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder <-strictTotalOrder)
  where open import  Relation.Binary

-- put new node at parent node, and rebuild tree to the top
--
{-# TERMINATING #-}   
replaceNode : {n m : Level } {t : Set m } {a : Set n} → RedBlackTree {n} {m} {t} a  → SingleLinkedStack (Node a ) →  Node a → (RedBlackTree {n} {m} {t} a → t) → t
replaceNode {n} {m} {t} {a} tree s n0 next = popSingleLinkedStack s (
      \s parent → replaceNode1 s parent)
       module ReplaceNode where
          replaceNode1 : SingleLinkedStack (Node a) → Maybe ( Node a ) → t
          replaceNode1 s nothing = next ( record tree { root = just (record n0 { color = Black}) } )
          replaceNode1 s (just n1) with compTri  (key n1) (key n0)
          replaceNode1 s (just n1) | tri< lt ¬eq ¬gt = replaceNode {n} {m} {t} {a} tree s ( record n1 { value = value n0 ; left = left n0 ; right = right n0 } ) next
          replaceNode1 s (just n1) | tri≈ ¬lt eq ¬gt = replaceNode {n} {m} {t} {a} tree s ( record n1 { left = just n0 } ) next
          replaceNode1 s (just n1) | tri> ¬lt ¬eq gt = replaceNode {n} {m} {t} {a} tree s ( record n1 { right = just n0 } ) next


rotateRight : {n m : Level } {t : Set m } {a : Set n} → RedBlackTree {n} {m} {t} a → SingleLinkedStack (Node  a) → Maybe (Node a) → Maybe (Node a) →
  (RedBlackTree {n} {m} {t} a → SingleLinkedStack (Node a ) → Maybe (Node a) → Maybe (Node a)  → t) → t
rotateRight {n} {m} {t} {a} tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 → rotateRight1 {n} {m} {t} {a} tree s n0 parent rotateNext)
  where
        rotateRight1 : {n m : Level } {t : Set m } {a : Set n} → RedBlackTree {n} {m} {t} a → SingleLinkedStack (Node  a)  → Maybe (Node a) → Maybe (Node a) →
          (RedBlackTree {n} {m} {t}  a → SingleLinkedStack (Node  a)  → Maybe (Node a) → Maybe (Node a) → t) → t
        rotateRight1 {n} {m} {t} {a} tree s n0 parent rotateNext with n0
        ... | nothing  = rotateNext tree s nothing n0
        ... | just n1 with parent
        ...           | nothing = rotateNext tree s (just n1 ) n0
        ...           | just parent1 with left parent1
        ...                | nothing = rotateNext tree s (just n1) nothing
        ...                | just leftParent with compTri (key n1) (key leftParent)
        rotateRight1 {n} {m} {t} {a} tree s n0 parent rotateNext | just n1 | just parent1 | just leftParent | tri< a₁ ¬b ¬c = rotateNext tree s (just n1) parent
        rotateRight1 {n} {m} {t} {a} tree s n0 parent rotateNext | just n1 | just parent1 | just leftParent | tri≈ ¬a b ¬c = rotateNext tree s (just n1) parent
        rotateRight1 {n} {m} {t} {a} tree s n0 parent rotateNext | just n1 | just parent1 | just leftParent | tri> ¬a ¬b c = rotateNext tree s (just n1) parent


rotateLeft : {n m  : Level } {t : Set m } {a : Set n} → RedBlackTree {n} {m} {t} a → SingleLinkedStack (Node  a) → Maybe (Node a) → Maybe (Node a) →
  (RedBlackTree {n} {m} {t}  a → SingleLinkedStack (Node  a) → Maybe (Node a) → Maybe (Node a) →  t) → t
rotateLeft {n} {m} {t} {a} tree s n0 parent rotateNext = getSingleLinkedStack s (\ s n0 → rotateLeft1 tree s n0 parent rotateNext)
  where
        rotateLeft1 : {n m  : Level } {t : Set m } {a : Set n} → RedBlackTree {n} {m} {t}  a → SingleLinkedStack (Node  a) → Maybe (Node a) → Maybe (Node a) →
          (RedBlackTree {n} {m} {t}  a → SingleLinkedStack (Node  a) → Maybe (Node a) → Maybe (Node a) → t) → t
        rotateLeft1 {n} {m} {t} {a} tree s n0 parent rotateNext with n0
        ... | nothing  = rotateNext tree s nothing n0
        ... | just n1 with parent
        ...           | nothing = rotateNext tree s (just n1) nothing
        ...           | just parent1 with right parent1
        ...                | nothing = rotateNext tree s (just n1) nothing
        ...                | just rightParent with compTri (key n1) (key rightParent)
        rotateLeft1 {n} {m} {t} {a} tree s n0 parent rotateNext | just n1 | just parent1 | just rightParent | tri< a₁ ¬b ¬c = rotateNext tree s (just n1) parent
        rotateLeft1 {n} {m} {t} {a} tree s n0 parent rotateNext | just n1 | just parent1 | just rightParent | tri≈ ¬a b ¬c = rotateNext tree s (just n1) parent
        rotateLeft1 {n} {m} {t} {a} tree s n0 parent rotateNext | just n1 | just parent1 | just rightParent | tri> ¬a ¬b c = rotateNext tree s (just n1) parent

{-# TERMINATING #-}
insertCase5 : {n m  : Level } {t : Set m } {a : Set n} → RedBlackTree {n} {m} {t}  a → SingleLinkedStack (Node a) → Maybe (Node a) → Node a → Node a → (RedBlackTree {n} {m} {t}  a → t) → t
insertCase5 {n} {m} {t} {a} tree s n0 parent grandParent next = pop2SingleLinkedStack s (\ s parent grandParent → insertCase51 tree s n0 parent grandParent next)
  where
    insertCase51 : {n m  : Level } {t : Set m } {a : Set n} → RedBlackTree {n} {m} {t}  a → SingleLinkedStack (Node a) → Maybe (Node a) → Maybe (Node a) → Maybe (Node a) → (RedBlackTree {n} {m} {t}  a → t) → t
    insertCase51 {n} {m} {t} {a} tree s n0 parent grandParent next with n0
    ...     | nothing = next tree
    ...     | just n1  with  parent | grandParent
    ...                 | nothing | _  = next tree
    ...                 | _ | nothing  = next tree
    ...                 | just parent1 | just grandParent1 with left parent1 | left grandParent1
    ...                                                     | nothing | _  = next tree
    ...                                                     | _ | nothing  = next tree
    ...                                                     | just leftParent1 | just leftGrandParent1
      with compTri (key n1) (key leftParent1) | compTri (key leftParent1) (key leftGrandParent1)
    ...    | tri≈ ¬a b ¬c | tri≈ ¬a1 b1 ¬c1  = rotateRight tree s n0 parent (\ tree s n0 parent → insertCase5 tree s n0 parent1 grandParent1 next)
    ...    | _            | _                = rotateLeft tree s n0 parent (\ tree s n0 parent → insertCase5 tree s n0 parent1 grandParent1 next)

insertCase4 : {n m  : Level } {t : Set m } {a : Set n} → RedBlackTree {n} {m} {t}  a → SingleLinkedStack (Node a) → Node a → Node a → Node a → (RedBlackTree {n} {m} {t}  a → t) → t
insertCase4 {n} {m} {t} {a} tree s n0 parent grandParent next
       with  (right parent) | (left grandParent)
...    | nothing | _ = insertCase5 tree s (just n0) parent grandParent next
...    | _ | nothing = insertCase5 tree s (just n0) parent grandParent next
...    | just rightParent | just leftGrandParent with compTri (key n0) (key rightParent) | compTri (key parent) (key leftGrandParent) -- (key n0) (key rightParent) | (key parent) (key leftGrandParent)
...                                                 | tri≈ ¬a b ¬c | tri≈ ¬a1 b1 ¬c1 = popSingleLinkedStack s (\ s n1 → rotateLeft tree s (left n0) (just grandParent) (\ tree s n0 parent → insertCase5 tree s n0 rightParent grandParent next))
... | _            | _               = insertCase41 tree s n0 parent grandParent next
  where
    insertCase41 : {n m  : Level } {t : Set m } {a : Set n} → RedBlackTree {n} {m} {t}  a → SingleLinkedStack (Node a) → Node a → Node a → Node a → (RedBlackTree {n} {m} {t}  a → t) → t
    insertCase41 {n} {m} {t} {a} tree s n0 parent grandParent next
                 with  (left parent) | (right grandParent)
    ...    | nothing | _ = insertCase5 tree s (just n0) parent grandParent next
    ...    | _ | nothing = insertCase5 tree s (just n0) parent grandParent next
    ...    | just leftParent | just rightGrandParent with compTri (key n0) (key leftParent) | compTri (key parent) (key rightGrandParent)
    ... | tri≈ ¬a b ¬c | tri≈ ¬a1 b1 ¬c1 =  popSingleLinkedStack s (\ s n1 → rotateRight tree s (right n0) (just grandParent) (\ tree s n0 parent → insertCase5 tree s n0 leftParent grandParent next))
    ... | _ | _ = insertCase5 tree s (just n0) parent grandParent next

colorNode : {n : Level } {a : Set n} → Node a → Color  → Node a
colorNode old c = record old { color = c }

{-# TERMINATING #-}
insertNode : {n m  : Level } {t : Set m } {a : Set n}  → RedBlackTree {n} {m} {t}  a → SingleLinkedStack (Node a) → Node a → (RedBlackTree {n} {m} {t}  a → t) → t
insertNode {n} {m} {t} {a} tree s n0 next = get2SingleLinkedStack s (insertCase1 n0)
   where
    insertCase1 : Node a → SingleLinkedStack (Node a) → Maybe (Node a) → Maybe (Node a) → t    -- placed here to allow mutual recursion
    insertCase3 : SingleLinkedStack (Node a) → Node a → Node a → Node a → 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 compTri (key uncle ) (key parent )
    insertCase3 s n0 parent grandParent | just uncle | _ | tri≈ ¬a b ¬c = insertCase4 tree s n0 parent grandParent next
    insertCase3 s n0 parent grandParent | just uncle | _ | tri< a ¬b ¬c with color uncle
    insertCase3 s n0 parent grandParent | just uncle | _ | tri< a ¬b ¬c | Red = pop2SingleLinkedStack s ( \s p0 p1 → insertCase1  (
           record grandParent { color = Red ; left = just ( record parent { color = Black } )  ; right = just ( record uncle { color = Black } ) }) s p0 p1 )
    insertCase3 s n0 parent grandParent | just uncle | _ | tri< a ¬b ¬c | Black = insertCase4 tree s n0 parent grandParent next
    insertCase3 s n0 parent grandParent | just uncle | _ | tri> ¬a ¬b c with color uncle
    insertCase3 s n0 parent grandParent | just uncle | _ | tri> ¬a ¬b c | Red = pop2SingleLinkedStack s ( \s p0 p1 → insertCase1  ( record grandParent { color = Red ; left = just ( record parent { color = Black } )  ; right = just ( record uncle { color = Black } ) }) s p0 p1 )
    insertCase3 s n0 parent grandParent | just uncle | _ | tri> ¬a ¬b c | Black = insertCase4 tree s n0 parent grandParent next
    insertCase2 : SingleLinkedStack (Node a) → Node a → Node a → Node a → t
    insertCase2 s n0 parent grandParent with color parent
    ... | Black = replaceNode tree s n0 next
    ... | Red =   insertCase3 s n0 parent grandParent
    insertCase1 n0 s nothing nothing = next tree
    insertCase1 n0 s nothing (just grandParent) = next tree
    insertCase1 n0 s (just parent) nothing = replaceNode tree s (colorNode n0 Black) next
    insertCase1 n0 s (just parent) (just grandParent) = insertCase2 s n0 parent grandParent

----
-- find node potition to insert or to delete, the path will be in the stack
--
findNode : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} {m} {t}   a → SingleLinkedStack (Node a) → (Node a) → (Node a) → (RedBlackTree {n} {m} {t}  a → SingleLinkedStack (Node a) → Node a → t) → t
findNode {n} {m} {a} {t} tree s n0 n1 next = pushSingleLinkedStack s n1 (\ s → findNode1 s n1)
  module FindNode where
    findNode2 : SingleLinkedStack (Node a) → (Maybe (Node a)) → t
    findNode2 s nothing = next tree s n0
    findNode2 s (just n) = findNode tree s n0 n next
    findNode1 : SingleLinkedStack (Node a) → (Node a)  → t
    findNode1 s n1 with (compTri (key n0) (key n1))
    findNode1 s n1 | tri< a ¬b ¬c = popSingleLinkedStack s ( \s _ → next tree s (record n1 {key = key n1 ; value = value n0 } ) )
    findNode1 s n1 | tri≈ ¬a b ¬c = findNode2 s (right n1)
    findNode1 s n1 | tri> ¬a ¬b c = findNode2 s (left n1)
    -- ...                                | EQ = popSingleLinkedStack s ( \s _ → next tree s (record n1 {ey =ey n1 ; value = value n0 } ) )
    -- ...                                | GT = findNode2 s (right n1)
    -- ...                                | LT = findNode2 s (left n1)




leafNode : {n : Level } { a : Set n } → a → ℕ → (Node a)
leafNode v k1 = record {key = k1 ; value = v ; right = nothing ; left = nothing ; color = Red }

putRedBlackTree : {n m : Level} {t : Set m} {a : Set n}  → RedBlackTree {n} {m} {t} a → a → (key1 : ℕ) → (RedBlackTree {n} {m} {t} a → t) → t
putRedBlackTree {n} {m} {t} {a}  tree val1 key1 next with (root tree)
putRedBlackTree {n} {m} {t} {a}  tree val1 key1 next | nothing = next (record tree {root = just (leafNode val1 key1 ) }) 
putRedBlackTree {n} {m} {t} {a}  tree val1 key1 next | just n2 = clearSingleLinkedStack (nodeStack tree) (λ s → findNode tree s (leafNode val1 key1) n2 (λ tree1 s n1 → insertNode tree1 s n1 next)) 


-- getRedBlackTree : {n m  : Level } {t : Set m}  {a : Set n} {k : ℕ} → RedBlackTree {n} {m} {t} {A}  a → → (RedBlackTree {n} {m} {t} {A}  a → (Maybe (Node a)) → t) → t
-- getRedBlackTree {_} {_} {t}  {a} {k} tree1 cs = checkNode (root tree)
--   module GetRedBlackTree where                     -- http://agda.readthedocs.io/en/v2.5.2/language/let-and-where.html
--     search : Node a → t
--     checkNode : Maybe (Node a) → t
--     checkNode nothing = cs tree nothing
--     checkNode (just n) = search n
--     search n with compTri1 (key n)
--     search n | tri< a ¬b ¬c = checkNode (left n)
--     search n | tri≈ ¬a b ¬c = cs tree (just n)
--     search n | tri> ¬a ¬b c = checkNode (right n)



-- putUnblanceTree : {n m : Level } {a : Set n} {k : ℕ} {t : Set m} → RedBlackTree {n} {m} {t} {A}  a → → a → (RedBlackTree {n} {m} {t} {A}  a → t) → t
-- putUnblanceTree {n} {m} {A} {a} {k} {t} tree1 value next with (root tree)
-- ...                                | nothing = next (record tree {root = just (leafNode1 value) })
-- ...                                | just n2  = clearSingleLinkedStack (nodeStack tree) (λ  s → findNode tree s (leafNode1 value) n2 (λ  tree1 s n1 → replaceNode tree1 s n1 next))

createEmptyRedBlackTreeℕ : {n m  : Level} {t : Set m} (a : Set n) 
     → RedBlackTree {n} {m} {t} a 
createEmptyRedBlackTreeℕ a = record {
        root = nothing
     ;  nodeStack = emptySingleLinkedStack
   }


test : {m : Level} (t : Set) → RedBlackTree {Level.zero} {Level.zero}  ℕ
test t = createEmptyRedBlackTreeℕ {Level.zero} {Level.zero} {t} ℕ

-- ts = createEmptyRedBlackTreeℕ {ℕ} {?} {!!} 0

-- tes = putRedBlackTree {_} {_} {_} (createEmptyRedBlackTreeℕ {_} {_} {_} 3 3) 2 2 (λ t → t)