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 Relation.Binary
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 }

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

contraposition : {m : Level } {A B : Set m} → (B → A) → (¬ A → ¬ B)
contraposition f = λ x y → x (f y)
 
compareTri1 : (n : ℕ) → zero <′ suc n 
compareTri1 zero =   ≤′-refl 
compareTri1 (suc n) =  ≤′-step ( compareTri1 n )

compareTri2 : (n m : ℕ) → n ≤′ m → suc n ≤′ suc m
compareTri2 _ _  ≤′-refl = ≤′-refl 
compareTri2 n (suc m) ( ≤′-step p ) =  ≤′-step { suc n }  ( compareTri2 n m p )

<′dec : Set
<′dec = ∀ m n → Dec ( m ≤′ n )

compareTri6 : ∀ m {n} → ¬ m ≤′ n →  ¬ suc m ≤′ suc n

is≤′ :  <′dec
is≤′  zero zero = yes ≤′-refl
is≤′  zero (suc n) = yes (lemma n)
  where
     lemma :  (n : ℕ) → zero ≤′ suc n
     lemma zero =   ≤′-step  ≤′-refl
     lemma (suc n) =  ≤′-step (lemma n)
is≤′  (suc m) (zero) = no ( λ () )
is≤′  (suc m) (suc n) with is≤′ m n
... | yes p = yes ( compareTri2 _ _ p )
... | no p = no ( compareTri6 _ p )

compareTri20 : {n : ℕ} → ¬ suc n ≤′ zero
compareTri20 () 


compareTri21 : (n m : ℕ) → suc n ≤′ suc m →  n ≤′ m
compareTri21 _ _  ≤′-refl = ≤′-refl
compareTri21 (suc n) zero ( ≤′-step p ) = compareTri23 (suc n) ( ≤′-step p ) p
  where
        compareTri23 : (n : ℕ) → suc n ≤′ suc zero → suc n ≤′ zero →  n ≤′ zero
        compareTri23 zero ( ≤′-step p ) _ =   ≤′-refl
        compareTri23 zero ≤′-refl _ =   ≤′-refl
        compareTri23 (suc n1) ( ≤′-step p ) ()
compareTri21 n (suc m) ( ≤′-step p ) = ≤′-step (compareTri21 _ _ p)
compareTri21 zero zero ( ≤′-step p ) = ≤′-refl
   

compareTri3 : ∀ m {n} → ¬ m ≡ suc (m + n)
compareTri3 zero    ()
compareTri3 (suc m) eq = compareTri3 m (cong pred eq)

compareTri4' : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
compareTri4' m {n} with n ≟ m
... | yes refl  = λ x y → x refl
... | no  p  = λ x y → p ( cong pred y )

compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
compareTri4 m = contraposition ( λ x → cong pred x )

-- compareTri6 : ∀ m {n} → ¬ m ≤′ n →  ¬ suc m ≤′ suc n
compareTri6  m {n} = λ x y → x (compareTri21 _ _ y)

compareTri5 : ∀ m {n} → ¬ m <′ n →  ¬ suc m <′ suc n
compareTri5  m {n}  = compareTri6 (suc m)

compareTri :  Trichotomous  _≡_ _<′_
compareTri zero zero = tri≈ ( λ ()) refl ( λ ())
compareTri zero (suc n) = tri< ( compareTri1 n )  ( λ ()) ( λ ())
compareTri (suc n) zero = tri> ( λ ()) ( λ ()) ( compareTri1 n )
compareTri (suc n) (suc m) with compareTri n m
... | tri< p q r = tri<  (compareTri2 (suc n) m p ) (compareTri4 _ q) ( compareTri5 _ r )
... | tri≈ p refl r = tri≈ (compareTri5 _ p) refl ( compareTri5 _ r )
... | tri> p q r = tri> ( compareTri5 _ p ) (compareTri4 _ q) (compareTri2 (suc m) n r )

compareDecTest : (n n1 : Node ℕ ℕ) → ( key n ≡ key n1 ) ∨ ( ¬  key n ≡ key n1 )
compareDecTest n n1 with (key n) ≟ (key n1)
...  | yes p  = pi1  p
...  | no ¬p  = pi2 ¬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

open IsStrictTotalOrder

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

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


putTest1 :{ m : Level } (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 = lemma2 ( record { top = Nothing } )
   where
     lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) →
       putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compareT }) k x (λ t →
       GetRedBlackTree.checkNode t k (λ t₁ x1 → checkT x1 x ≡ True) (root t))
     lemma2 s with compTri k (key n1)
     ... |  tri≈ le eq gt = lemma3
        where 
           lemma3 : 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 → compareT x₁ y  } ) k ( λ  t x1 → checkT x1 x  ≡ True)
           lemma3 = {!!}
     ... |  tri> le eq gt = {!!}
     ... |  tri< le eq gt = {!!}
...  | 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 = {!!}