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

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

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 -> check1 x 1 ≡ True  
test3 = begin
    check1 (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 -> check1 x 1 ≡ True   ))
test9 = refl

test10 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
    \t -> putRedBlackTree t 2 2 (
    \t -> getRedBlackTree t 1 (
    \t x -> check1 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 = compareℕ }



putTest1Lemma1 : (k : ℕ) (x : ℕ) -> Data.Nat.compare 1 1 ≡ Data.Nat.equal 1
putTest1Lemma1 k x = refl

-- begin
--     Data.Nat.compare k (key (leafNode k x)) 
--   ≡⟨ {!!} ⟩
--     Data.Nat.equal _
--   ∎


putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
         -> (k : ℕ) (x : ℕ) 
         -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
         (\ t -> getRedBlackTree t k (\ t x1 -> check1 x1 x  ≡ True)) 
putTest1 n k x with n
...  | Just n1 = {!!}
...  | Nothing = {!!}


-- with Data.Nat.compare k (key (leafNode k x))
-- ...            | Data.Nat.equal _ = ?

-- begin
--     ?
--   ≡⟨ ? ⟩
--     True
--   ∎