module redBlackTreeTest where

open import RedBlackTree
open import stack
open import Level hiding (zero)

open import Data.Empty

open import Data.Nat
open import Relation.Nullary

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 = compare2 }

-- compare2 : (x y : ℕ ) -> CompareResult {Level.zero}
-- compare2 zero zero = EQ
-- compare2 (suc _) zero = GT
-- compare2  zero (suc _) = LT
-- compare2  (suc x) (suc y) = compare2 x y

compareTri1 : (n : ℕ) -> zero < ℕ.suc n 
compareTri1 zero = {!!}
compareTri1 (suc n) = {!!}

compareTri :  Trichotomous  _≡_ _<_
compareTri zero zero = tri≈ (\()) refl (\())
compareTri zero (suc n) = tri< {!!} (\()) (\())
compareTri (suc n) zero = tri> (\()) (\()) {!!}
compareTri (suc n) (suc m) with compareTri n m
... | tri≈ p q r = tri≈ {!!} (cong (\x -> ℕ.suc x) q) {!!}
... | tri< p q r = tri<  {!!} {!!} {!!}
... | tri> p q r = tri> {!!} {!!} {!!}

compareDecTest : (n n1 : Node ℕ ℕ) -> key n ≡ key n1
compareDecTest n n1 with (key n) ≟ (key n1)
...  | yes p = p
...  | no ¬p  = {!!}



putTest1Lemma2 : (k : ℕ)  -> compare2 k k ≡ EQ
putTest1Lemma2 zero = refl
putTest1Lemma2 (suc k) = putTest1Lemma2 k

putTest1Lemma1 : (x y : ℕ)  -> compareℕ x y ≡ compare2 x y
putTest1Lemma1 zero    zero    = refl
putTest1Lemma1 (suc m) zero    = refl
putTest1Lemma1 zero    (suc n) = refl
putTest1Lemma1 (suc m) (suc n) with Data.Nat.compare m n
putTest1Lemma1 (suc .m)           (suc .(Data.Nat.suc m + k)) | less    m k = lemma1  m
 where
    lemma1 : (m :  ℕ) -> LT  ≡ compare2 m (ℕ.suc (m + k)) 
    lemma1  zero = refl
    lemma1  (suc y) = lemma1 y
putTest1Lemma1 (suc .m)           (suc .m)           | equal   m   = lemma1 m
 where
    lemma1 : (m :  ℕ) -> EQ  ≡ compare2 m m
    lemma1  zero = refl
    lemma1  (suc y) = lemma1 y
putTest1Lemma1 (suc .(Data.Nat.suc m + k)) (suc .m)           | greater m k = lemma1 m
 where
    lemma1 : (m :  ℕ) -> GT  ≡ compare2  (ℕ.suc (m + k))  m
    lemma1  zero = refl
    lemma1  (suc y) = lemma1 y

putTest1Lemma3 : (k : ℕ)  -> compareℕ k k ≡ EQ
putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k  ) 

compareLemma1 : {x  y : ℕ}  -> compare2 x y ≡ EQ -> x  ≡ y
compareLemma1 {zero} {zero} refl = refl
compareLemma1 {zero} {suc _} () 
compareLemma1 {suc _} {zero} () 
compareLemma1 {suc x} {suc y} eq = cong ( \z -> ℕ.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
   where
      lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
      lemma2 = refl


putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
         -> (k : ℕ) (x : ℕ) 
         -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
         (\ t -> getRedBlackTree t k (\ t x1 -> check2 x1 x  ≡ True)) 
putTest1 n k x with n
...  | Just n1 = lemma2 ( record { top = Nothing } )
   where
     lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) -> putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t →
         GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t))
     lemma2 s with compare2 k (key n1)
     ... |  EQ = lemma3 {!!}
        where 
           lemma3 : compare2 k (key n1) ≡  EQ -> getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
               key   = key n1 ; value = x ; right = right n1 ; left  = left n1 ; color = Black
               } ) ; nodeStack = s ; compare = λ x₁ y → compare2 x₁ y  } ) k ( \ t x1 -> check2 x1 x  ≡ True)
           lemma3 eq with compare2 x x | putTest1Lemma2 x 
           ... | EQ | refl with compare2 k (key n1)  | eq
           ...              | EQ | refl with compare2 x x | putTest1Lemma2 x
           ...                    | EQ | refl = refl
     ... |  GT = {!!}
     ... |  LT = {!!}
...  | 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 → compare2 x₁ y  } ) k
        ( \ t x1 -> check2 x1 x  ≡ True) 
     lemma1 with compare2 k k | putTest1Lemma2 k
     ... | EQ | refl with compare2 x x | putTest1Lemma2 x
     ...              | EQ | refl = refl