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 m : Level } (a : Set n) : Set (m Level.⊔ 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} {m}  a  → (Node a ) → (RedBlackTree {n} {m}  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} {m}  a  → (Node a ) → (RedBlackTree {n} {m}  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 )

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

popAllNode1 : {n : Level } {a : Set n} → SingleLinkedStack (Node a ) → Node a →  Maybe (Node a)
popAllNode1 [] r = nothing
popAllNode1 (x ∷ t) r with popAllNode1 t r
... | ttt = {!!}

popAllnode : {n m  : Level } {a : Set n} → RedBlackTree {n} {m}  a  → RedBlackTree {n} {m}  a → Set
popAllnode {n} {m} {a} now original = {!!}

record findNodeInvariant {n m  : Level } {a : Set n} {t : Set m} (now original :  RedBlackTree {n} {m}  a ) : Set (m Level.⊔ n) where
   field
     tree+stack : popAllnode now original