module redBlackTreeTest where

open import RedBlackTree
open import stack
open import Level hiding (zero) renaming ( suc to succ )

open import Data.Empty

open import Data.Nat
open import Relation.Nullary


open import Algebra
open import Data.Nat.Properties   as NatProp

open Tree
open Node
open RedBlackTree.RedBlackTree
open Stack

-- tests

putTree1 : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → k → a → (RedBlackTree {n} {m} {t} a k → t) → t
putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree)
...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (λ  s → findNode tree s (leafNode k1 value) n2 (λ  tree1 s n1 → replaceNode tree1 s n1 next))

open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Core
open import Function


check1 : {m : Level } (n : Maybe (Node  ℕ ℕ)) → ℕ → Bool {m}
check1 Nothing _ = False
check1 (Just n)  x with Data.Nat.compare (value n)  x
...  | equal _ = True
...  | _ = False

check2 : {m : Level } (n : Maybe (Node  ℕ ℕ)) → ℕ → Bool {m}
check2 Nothing _ = False
check2 (Just n)  x with compare2 (value n)  x
...  | EQ = True
...  | _ = False

test1 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 x 1 ≡ True   ))
test1 = refl

test2 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
    λ t → putTree1 t 2 2 (
    λ t → getRedBlackTree t 1 (
    λ t x → check2 x 1 ≡ True   )))
test2 = refl

open ≡-Reasoning
test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1
    $ λ t → putTree1 t 2 2
    $ λ t → putTree1 t 3 3
    $ λ t → putTree1 t 4 4
    $ λ t → getRedBlackTree t 1
    $ λ t x → check2 x 1 ≡ True
test3 = begin
    check2 (Just (record {key = 1 ; value = 1 ; color = Black ; left = Nothing ; right = Just (leafNode 2 2)})) 1
  ≡⟨ refl ⟩
    True
  ∎

test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1
    $ λ t → putTree1 t 2 2
    $ λ t → putTree1 t 3 3
    $ λ t → putTree1 t 4 4
    $ λ t → getRedBlackTree t 4
    $ λ t x → x

-- test5 : Maybe (Node ℕ ℕ)
test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4
    $ λ t → putTree1 t 6 6
    $ λ t0 →  clearSingleLinkedStack (nodeStack t0)
    $ λ s → findNode1 t0 s (leafNode 3 3) ( root t0 )
    $ λ t1 s n1 → replaceNode t1 s n1
    $ λ t → getRedBlackTree t 3
    -- $ λ t x → SingleLinkedStack.top (stack s)
    -- $ λ t x → n1
    $ λ t x → root t
  where
     findNode1 : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → (Node a k) → (Maybe (Node a k)) → (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → t) → t
     findNode1 t s n1 Nothing next = next t s n1
     findNode1 t s n1 ( Just n2 ) next = findNode t s n1 n2 next

-- test51 : putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ λ t →
--   putTree1 t 2 2 $ λ t → putTree1 t 3 3 $ λ t → root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} )
-- test51 = refl

test6 : Maybe (Node ℕ ℕ)
test6 = root (createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)})


test7 : Maybe (Node ℕ ℕ)
test7 = clearSingleLinkedStack (nodeStack tree2) (λ  s → replaceNode tree2 s n2 (λ  t → root t))
  where
    tree2 = createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)}
    k1 = 1
    n2 = leafNode 0 0
    value1 = 1

test8 : Maybe (Node ℕ ℕ)
test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1
    $ λ t → putTree1 t 2 2 (λ  t → root t)


test9 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 x 1 ≡ True   ))
test9 = refl

test10 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
    λ t → putRedBlackTree t 2 2 (
    λ t → getRedBlackTree t 1 (
    λ t x → check2 x 1 ≡ True   )))
test10 = refl

test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1
    $ λ t → putRedBlackTree t 2 2
    $ λ t → putRedBlackTree t 3 3
    $ λ t → getRedBlackTree t 2
    $ λ t x → root t


redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} → RedBlackTree {Level.zero} {m} {t} a ℕ
redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compareT }


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

checkT : {m : Level } (n : Maybe (Node  ℕ ℕ)) → ℕ → Bool {m}
checkT Nothing _ = False
checkT (Just n) x with compTri (value n)  x
...  | tri≈ _ _ _ = True
...  | _ = False

checkEQ :  {m : Level }  ( x :  ℕ ) -> ( n : Node  ℕ ℕ ) -> (value n )  ≡ x  -> checkT {m} (Just n) x ≡ True
checkEQ x n refl with compTri (value n)  x
... |  tri≈ _ refl _ = refl
... |  tri> _ neq gt =  ⊥-elim (neq refl)
... |  tri< lt neq _ =  ⊥-elim (neq refl)

checkEQ' :  {m : Level }  ( x y :  ℕ ) -> ( eq : x  ≡ y  ) -> ( x  ≟ y ) ≡ yes eq
checkEQ' x y refl with  x ≟ y
... | yes refl = refl
... | no neq = ⊥-elim ( neq refl )

---  search -> checkEQ
---  findNode -> search

open stack.SingleLinkedStack
open stack.Element

{-# TERMINATING #-}
inStack : {l : Level} (n : Node ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → Bool {l}
inStack  n s with ( top s )
... | Nothing = True
... | Just n1 with  compTri (key n) (key (datum n1))
...            | tri> _ neq _ =  inStack  n ( record { top = next n1 } )
...            | tri< _ neq _ =  inStack  n ( record { top = next n1 } )
...            | tri≈  _ refl _  = False

record StackTreeInvariant  ( n : Node ℕ ℕ )
        ( s : SingleLinkedStack (Node  ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where
  field
    sti : replaceNode t s n $ λ  t1 → getRedBlackTree t1 (key n) (λ  t2 x1 → checkT x1 (value n)  ≡ True)
    notInStack : inStack n s ≡ True  → ⊥

open StackTreeInvariant

putTest1 : (n : Maybe (Node ℕ ℕ))
         → (k : ℕ) (x : ℕ)
         → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
           (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True))
putTest1 n k x with n
...  | Just n1 = lemma0
   where
     upelem : (eleN : Element (Node ℕ ℕ)) -> (Node ℕ ℕ)
     upelem eleN = n1
     tree0 : (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ
     tree0 s = record { root = Just n1 ; nodeStack = s ; compare = compareT }
     lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → StackTreeInvariant (leafNode k x) s (tree0 s)
         → findNode (tree0 s) s (leafNode k x) n1 (λ  tree1 s n1 → replaceNode tree1 s n1
              (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True)))
     lemma2 s STI with compTri k (key n1)
     ... |  tri≈ le refl gt = lemma5 s ( tree0 s ) n1
        where
           lemma5 :  (s : SingleLinkedStack (Node ℕ ℕ) )  → ( t :  RedBlackTree  ℕ ℕ  ) → ( n :  Node ℕ ℕ  ) → popSingleLinkedStack ( record { top = Just (cons n (SingleLinkedStack.top s)) }  )
                   ( \ s1  _ -> (replaceNode (tree0 s1) s1 (record n1 { key = k ; value = x } ) (λ t →
                      GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))) )
           lemma5 s t n with (top s)
           ...          | Just n2  with compTri k k
           ...            | tri< _ neq _ =  ⊥-elim (neq refl)
           ...            | tri> _ neq _ =  ⊥-elim (neq refl)
           ...            | tri≈  _ refl _  =  ⊥-elim (notInStack STI ({!!}))
           lemma5 s t n | Nothing with compTri k k
           ...            | tri≈  _ refl _  = checkEQ x _ refl
           ...            | tri< _ neq _ =  ⊥-elim (neq refl)
           ...            | tri> _ neq _ =  ⊥-elim (neq refl)
     ... |  tri> le eq gt = sti ( record { sti = {!!} ; notInStack = {!!}  } )
     ... |  tri< le eq gt = {!!}
     lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 s) s (leafNode k x) n1 (λ  tree1 s n1 → replaceNode tree1 s n1
              (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True))))
     lemma0 = lemma2 (record {top = Nothing}) ( record { sti = {!!}  ; notInStack = {!!} } )
...  | Nothing = lemma1
   where
     lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
               key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y  } ) k
        ( λ  t x1 → checkT x1 x  ≡ True)
     lemma1 with compTri k k
     ... | tri≈  _ refl _ = checkEQ x _ refl
     ... | tri< _ neq _ =  ⊥-elim (neq refl)
     ... | tri> _ neq _ =  ⊥-elim (neq refl)