module redBlackTreeTest where

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

open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Core


open Tree
open Node
open RedBlackTree.RedBlackTree
open Stack

-- tests

putTree1 : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> a -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
putTree1 {n} {m} {a} {k} {si} {t} tree k1 value next with (root tree)
...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
...                                | Just n2  = clearStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> replaceNode tree1 s n2 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

test1 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( \t -> getRedBlackTree t 1 ( \t x -> check1 x 1 ≡ True   ))
test1 = refl

test2 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
    \t -> putTree1 t 2 2 (
    \t -> getRedBlackTree t 1 (
    \t x -> check1 x 1 ≡ True   )))
test2 = refl

-- test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 
--     $ \t -> putTree1 t 2 2 
--     $ \t -> getRedBlackTree t 2 
--     $ \t x -> check1 x 2 ≡ True  
-- test3 = {!!}

test4 : putTree1 {_} {_} {ℕ} {ℕ} ( createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $  \t -> putTree1 t 2 2  $ \t ->
  root t ≡ Just (record { key = 1 ; value = 1 ; left = Nothing ; right = Just ( record { key = 2 ; value = 2 } ) } )
test4 = refl