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 Data.List

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


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

SingleLinkedStack = List

emptySingleLinkedStack :  {n : Level } {Data : Set n} -> SingleLinkedStack Data
emptySingleLinkedStack = []

pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
pushSingleLinkedStack stack datum next = next ( datum ∷ stack )

popSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
popSingleLinkedStack [] cs = cs [] nothing
popSingleLinkedStack (data1 ∷ s)  cs = cs s (just data1)

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 : Level } (a : Set n) : Set n where
  field
    root : Maybe (Node a )
    nodeStack : SingleLinkedStack  (Node a )
    -- compare : k → k → Tri A B C
    -- <-cmp 

open RedBlackTree


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

{-# TERMINATING #-}
findNode : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n}  a  → (Node a ) → (RedBlackTree {n}  a → t) → t
findNode {n} {m} {a}  {t} tree n0 next with root tree
findNode {n} {m} {a}  {t} tree n0 next | nothing = next tree
findNode {n} {m} {a}  {t} tree n0 next | just x with <-cmp (key x) (key n0)
findNode {n} {m} {a}  {t} tree n0 next | just x | tri≈ ¬a b ¬c = next tree
findNode {n} {m} {a}  {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}  {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} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → t) → t
findNode1 {n} {m} {a} {t} tree n0 next = findNode2 (root tree) (nodeStack tree)
  module FindNode where
    findNode2 : (Maybe (Node a )) → SingleLinkedStack (Node a ) → t
    findNode2 nothing st = next record { root = nothing ; nodeStack = st }
    findNode2 (just x) st with <-cmp (key n0) (key x)
    ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st })
    ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2 (right x) s1)
    ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2 (left x) s1)

node001 : Node  ℕ 
node001 = record { key = 2 ; value = 3 ; left = nothing ; right = nothing ; color = Black }
node002 : Node  ℕ 
node002 = record { key = 1 ; value = 3 ; left = just node001 ; right = nothing ; color = Black }
node003 : Node  ℕ 
node003 = record { key = 0 ; value = 3 ; left = just node002 ; right = nothing ; color = Black }

test001 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = nothing ; nodeStack = emptySingleLinkedStack } )
   node001 ( λ tree → tree )
test002 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node001 ; nodeStack = emptySingleLinkedStack } )
   node001 ( λ tree → tree )
test003 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } )
   node001 ( λ tree → tree )
test004 = findNode {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } )
   node001 ( λ tree → tree )

replaceNode : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → t) → t
replaceNode {n} {m} {a} {t} tree n0 next = replaceNode2 (nodeStack tree) (λ newNode → next record { root = just newNode ; nodeStack = emptySingleLinkedStack } )
  module FindNodeR where
      replaceNode1 : (Maybe (Node a )) → Node a
      replaceNode1 nothing  = record n0 { left = nothing ; right = nothing  } 
      replaceNode1 (just x)  = record n0 { left = left x ; right = right x } 
      replaceNode2 : SingleLinkedStack (Node a ) → (Node a  → t)  → t
      replaceNode2 [] next = next ( replaceNode1 (root tree) ) 
      replaceNode2 (x ∷ st) next with <-cmp (key x) (key n0)
      replaceNode2 (x ∷ st) next | tri< a ¬b ¬c = replaceNode2 st ( λ new → next ( record x { left = left new } ) )
      replaceNode2 (x ∷ st) next | tri≈ ¬a b ¬c = replaceNode2 st ( λ new → next ( record x { left = left new ; right = right new } ) )
      replaceNode2 (x ∷ st) next | tri> ¬a ¬b c = replaceNode2 st ( λ new → next ( record x { right = right new } ) )

insertNode : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → t) → t
insertNode tree n0 next = findNode1 tree n0 ( λ new → replaceNode tree n0 next )

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

findNodeLeft : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a))  → Set n
findNodeLeft x [] =  (left x ≡ nothing ) ∧ (right x ≡ nothing )
findNodeLeft {n} x (h ∷ t) = Lift n ((key x) < (key h))
findNodeRight : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a))  → Set n
findNodeRight x [] =  (left x ≡ nothing ) ∧ (right x ≡ nothing )
findNodeRight {n} x (h ∷ t) = Lift n ((key x) > (key h))

data FindNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a ) → Set n where
   fni-stackEmpty  : (now :  RedBlackTree {n}  a ) → FindNodeInvariant [] now 
   fni-treeEmpty  : (st : SingleLinkedStack (Node a))  → FindNodeInvariant st record { root = nothing ; nodeStack = st }
   fni-Left  : (x : Node a) (st : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a )
      →  FindNodeInvariant ( x ∷ st ) original → findNodeLeft x st →  FindNodeInvariant st original
   fni-Right  : (x : Node a) (st : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a )
      →  FindNodeInvariant ( x ∷ st ) original → findNodeRight x st →  FindNodeInvariant st original


findNode1h : {n m  : Level } {a : Set n} {t : Set m}  → (tree : RedBlackTree {n} a )  → (Node a )
     → ((new : RedBlackTree {n} a) →  FindNodeInvariant (nodeStack new) tree → t ) 
     → ( FindNodeInvariant (nodeStack tree)  tree) → t
findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) prev
  module FindNodeH where
    findNode2h : (Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → FindNodeInvariant s tree  → t
    findNode2h nothing st prev = next record { root = nothing ; nodeStack = st } {!!}
    findNode2h (just x) st prev with <-cmp (key n0) (key x)
    ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) {!!} -- ( fni-Last ? )
    ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 (fni-Left x s1 tree {!!} {!!}) )
    ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 (fni-Right x s1 tree {!!} {!!}) )


-- replaceNodeH : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → {!!} → t) → {!!} → t
-- replaceNodeH = {!!}