module hoareRedBlackTree 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 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) (k : ℕ) : Set n where
  inductive
  field
    key   : ℕ
    value : a
    right : Maybe (Node a k)
    left  : Maybe (Node a k)
    color : Color {n}
open Node

record RedBlackTree {n m : Level } {t : Set m} (a : Set n) (k : ℕ) : Set (m Level.⊔ n) where
  field
    root : Maybe (Node a k)
    nodeStack : SingleLinkedStack  (Node a k)
    -- compare : k → k → Tri A B C
    -- <-cmp 

open RedBlackTree

open SingleLinkedStack



----
-- find node potition to insert or to delete, the path will be in the stack
--

{-# TERMINATING #-}
findNode : {n m  : Level } {a : Set n} {k : ℕ} {t : Set m}  → RedBlackTree {n} {m} {t}   a k → (Node a k) → (RedBlackTree {n} {m} {t} a k → t) → t
findNode {n} {m} {a} {k} {t} tree n0 next with root tree
findNode {n} {m} {a} {k} {t} tree n0 next | nothing = next tree
findNode {n} {m} {a} {k} {t} tree n0 next | just x with <-cmp (key x) (key n0)
findNode {n} {m} {a} {k} {t} tree n0 next | just x | tri≈ ¬a b ¬c = next tree
findNode {n} {m} {a} {k} {t} tree n0 next | just x | tri< a₁ ¬b ¬c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (left x) ; nodeStack = s}) n0 next)
findNode {n} {m} {a} {k} {t} tree n0 next | just x | tri> ¬a ¬b c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (right x) ; nodeStack = s}) n0 next)


findNode1 : {n m  : Level } {a : Set n} {k : ℕ} {t : Set m}  → RedBlackTree {n} {m} {t}   a k → (Node a k) → (RedBlackTree {n} {m} {t} a k → t) → t
findNode1 {n} {m} {a} {k} {t} tree n0 next = findNode2 (root tree) (nodeStack tree) n0 {!!}
  where
    findNode2 : (Maybe (Node a k)) → SingleLinkedStack (Node a k) → Node a k → (Maybe (Node a k) → SingleLinkedStack (Node a k) → t) → t
    findNode2 nothing st n0 next = next nothing st
    findNode2 (just x) st n0 next with (<-cmp (key n0) (key x))
    findNode2 (just x) st n0 next | tri≈ ¬a b ¬c = {!!}
    findNode2 (just x) st n0 next | tri< a ¬b ¬c = {!!}
    findNode2 (just x) st n0 next | tri> ¬a ¬b c = {!!}

    findNode3 : SingleLinkedStack (Node a k) → Node a k → t
    findNode3 s1 n1 with (<-cmp (key n0) (key n1))
    findNode3 s1 n1 | tri≈ ¬a b ¬c = next (record {root = root tree ; nodeStack = s1})
    findNode3 s1 n1 | tri< a ¬b ¬c = pushSingleLinkedStack (nodeStack tree) n1 (λ s → findNode2 (left n1) s n0 {!!})
    findNode3 s1 n1 | tri> ¬a ¬b c = {!!}

-- pushSingleLinkedStack s n1 (\ s → findNode1 s n1)
  -- module FindNode where
  --   findNode2 : SingleLinkedStack (Node a k) → (Maybe (Node a k)) → t
  --   findNode2 s nothing = next tree
  --   findNode2 s (just n) = findNode tree s n0 n next
  --   findNode1 : SingleLinkedStack (Node a k) → (Node a k)  → t
  --   findNode1 s n1 with (<-cmp (key n0) (key n1))
  --   findNode1 s n1 | tri< a ¬b ¬c = findNode2 s (right 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 (left n1)
    -- ...                                | EQ = popSingleLinkedStack s ( \s _ → next tree s (record n1 { key = key n1 ; value = value n0 } ) )
    -- ...                                | GT = findNode2 s (right n1)
    -- ...                                | LT = findNode2 s (left n1)


createEmptyRedBlackTreeℕ : {n m  : Level} {t : Set m} (a : Set n) (b : ℕ)
     → RedBlackTree {n} {m} {t} a b
createEmptyRedBlackTreeℕ a b = record {
        root = nothing
     ;  nodeStack = emptySingleLinkedStack
     -- ;  nodeComp = λ x x₁ → {!!}
   }


test = findNode (createEmptyRedBlackTreeℕ {!!} 1)