module redBlackTreeTest where

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

open import Data.Nat

open Tree
open Node
open RedBlackTree.RedBlackTree
open Stack

-- tests

putTree1 : {n m : Level } {a k : Set n} {t : Set m} !$\rightarrow$! RedBlackTree {n} {m} {t} a k !$\rightarrow$! k !$\rightarrow$! a !$\rightarrow$! (RedBlackTree {n} {m} {t} a k !$\rightarrow$! t) !$\rightarrow$! 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 !$\rightarrow$! findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 !$\rightarrow$! replaceNode tree1 s n1 next))

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


check1 : {m : Level } (n : Maybe (Node  !$\mathbb{N}$! !$\mathbb{N}$!)) !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! 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  !$\mathbb{N}$! !$\mathbb{N}$!)) !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! Bool {m}
check2 Nothing _ = False
check2 (Just n)  x with compare2 (value n)  x
...  | EQ = True
...  | _ = False

test1 : putTree1 {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$! {Set Level.zero} ) 1 1 ( \t !$\rightarrow$! getRedBlackTree t 1 ( \t x !$\rightarrow$! check2 x 1 !$\equiv$! True   ))
test1 = refl

test2 : putTree1 {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$! {Set Level.zero} ) 1 1 (
    \t !$\rightarrow$! putTree1 t 2 2 (
    \t !$\rightarrow$! getRedBlackTree t 1 (
    \t x !$\rightarrow$! check2 x 1 !$\equiv$! True   )))
test2 = refl

open !$\equiv$!-Reasoning
test3 : putTree1 {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$! {Set Level.zero}) 1 1
    $ \t !$\rightarrow$! putTree1 t 2 2
    $ \t !$\rightarrow$! putTree1 t 3 3
    $ \t !$\rightarrow$! putTree1 t 4 4
    $ \t !$\rightarrow$! getRedBlackTree t 1
    $ \t x !$\rightarrow$! check2 x 1 !$\equiv$! True
test3 = begin
    check2 (Just (record {key = 1 ; value = 1 ; color = Black ; left = Nothing ; right = Just (leafNode 2 2)})) 1
  !$\equiv$!!$\langle$! refl !$\rangle$!
    True
  !$\blacksquare$!

test31 = putTree1 {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$! ) 1 1
    $ \t !$\rightarrow$! putTree1 t 2 2
    $ \t !$\rightarrow$! putTree1 t 3 3
    $ \t !$\rightarrow$! putTree1 t 4 4
    $ \t !$\rightarrow$! getRedBlackTree t 4
    $ \t x !$\rightarrow$! x

-- test5 : Maybe (Node !$\mathbb{N}$! !$\mathbb{N}$!)
test5 = putTree1 {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$! ) 4 4
    $ \t !$\rightarrow$! putTree1 t 6 6
    $ \t0 !$\rightarrow$!  clearSingleLinkedStack (nodeStack t0)
    $ \s !$\rightarrow$! findNode1 t0 s (leafNode 3 3) ( root t0 )
    $ \t1 s n1 !$\rightarrow$! replaceNode t1 s n1
    $ \t !$\rightarrow$! getRedBlackTree t 3
    -- $ \t x !$\rightarrow$! SingleLinkedStack.top (stack s)
    -- $ \t x !$\rightarrow$! n1
    $ \t x !$\rightarrow$! root t
  where
     findNode1 : {n m : Level } {a k : Set n} {t : Set m} !$\rightarrow$! RedBlackTree {n} {m} {t} a k !$\rightarrow$! SingleLinkedStack (Node a k) !$\rightarrow$! (Node a k) !$\rightarrow$! (Maybe (Node a k)) !$\rightarrow$! (RedBlackTree {n} {m} {t} a k !$\rightarrow$! SingleLinkedStack (Node a k) !$\rightarrow$! Node a k !$\rightarrow$! t) !$\rightarrow$! 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 {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} {_} {Maybe (Node !$\mathbb{N}$! !$\mathbb{N}$!)} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$! {Set Level.zero} ) 1 1 $ \t !$\rightarrow$!
--   putTree1 t 2 2 $ \t !$\rightarrow$! putTree1 t 3 3 $ \t !$\rightarrow$! root t !$\equiv$! Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} )
-- test51 = refl

test6 : Maybe (Node !$\mathbb{N}$! !$\mathbb{N}$!)
test6 = root (createEmptyRedBlackTree!$\mathbb{N}$! {_} !$\mathbb{N}$! {Maybe (Node !$\mathbb{N}$! !$\mathbb{N}$!)})


test7 : Maybe (Node !$\mathbb{N}$! !$\mathbb{N}$!)
test7 = clearSingleLinkedStack (nodeStack tree2) (\ s !$\rightarrow$! replaceNode tree2 s n2 (\ t !$\rightarrow$! root t))
  where
    tree2 = createEmptyRedBlackTree!$\mathbb{N}$! {_} !$\mathbb{N}$! {Maybe (Node !$\mathbb{N}$! !$\mathbb{N}$!)}
    k1 = 1
    n2 = leafNode 0 0
    value1 = 1

test8 : Maybe (Node !$\mathbb{N}$! !$\mathbb{N}$!)
test8 = putTree1 {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$!) 1 1
    $ \t !$\rightarrow$! putTree1 t 2 2 (\ t !$\rightarrow$! root t)


test9 : putRedBlackTree {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$! {Set Level.zero} ) 1 1 ( \t !$\rightarrow$! getRedBlackTree t 1 ( \t x !$\rightarrow$! check2 x 1 !$\equiv$! True   ))
test9 = refl

test10 : putRedBlackTree {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$! {Set Level.zero} ) 1 1 (
    \t !$\rightarrow$! putRedBlackTree t 2 2 (
    \t !$\rightarrow$! getRedBlackTree t 1 (
    \t x !$\rightarrow$! check2 x 1 !$\equiv$! True   )))
test10 = refl

test11 = putRedBlackTree {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$!) 1 1
    $ \t !$\rightarrow$! putRedBlackTree t 2 2
    $ \t !$\rightarrow$! putRedBlackTree t 3 3
    $ \t !$\rightarrow$! getRedBlackTree t 2
    $ \t x !$\rightarrow$! root t


redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a !$\mathbb{N}$!)) {t : Set m} !$\rightarrow$! RedBlackTree {Level.zero} {m} {t} a !$\mathbb{N}$!
redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }

-- compare2 : (x y : !$\mathbb{N}$! ) !$\rightarrow$! compareresult
-- compare2 zero zero = eq
-- compare2 (suc _) zero = gt
-- compare2  zero (suc _) = lt
-- compare2  (suc x) (suc y) = compare2 x y

putTest1Lemma2 : (k : !$\mathbb{N}$!)  !$\rightarrow$! compare2 k k !$\equiv$! EQ
putTest1Lemma2 zero = refl
putTest1Lemma2 (suc k) = putTest1Lemma2 k

putTest1Lemma1 : (x y : !$\mathbb{N}$!)  !$\rightarrow$! compare!$\mathbb{N}$! x y !$\equiv$! 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 :  !$\mathbb{N}$!) !$\rightarrow$! LT  !$\equiv$! compare2 m (!$\mathbb{N}$!.suc (m + k))
    lemma1  zero = refl
    lemma1  (suc y) = lemma1 y
putTest1Lemma1 (suc .m)           (suc .m)           | equal   m   = lemma1 m
 where
    lemma1 : (m :  !$\mathbb{N}$!) !$\rightarrow$! EQ  !$\equiv$! 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 :  !$\mathbb{N}$!) !$\rightarrow$! GT  !$\equiv$! compare2  (!$\mathbb{N}$!.suc (m + k))  m
    lemma1  zero = refl
    lemma1  (suc y) = lemma1 y

putTest1Lemma3 : (k : !$\mathbb{N}$!)  !$\rightarrow$! compare!$\mathbb{N}$! k k !$\equiv$! EQ
putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k  )

compareLemma1 : {x  y : !$\mathbb{N}$!}  !$\rightarrow$! compare2 x y !$\equiv$! EQ !$\rightarrow$! x  !$\equiv$! y
compareLemma1 {zero} {zero} refl = refl
compareLemma1 {zero} {suc _} ()
compareLemma1 {suc _} {zero} ()
compareLemma1 {suc x} {suc y} eq = cong ( \z !$\rightarrow$! !$\mathbb{N}$!.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
   where
      lemma2 : compare2 (!$\mathbb{N}$!.suc x) (!$\mathbb{N}$!.suc y) !$\equiv$! compare2 x y
      lemma2 = refl


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