module redBlackTreeTest where

open import Level hiding (zero) renaming ( suc to succ )

open import Data.Empty
open import Data.List
open import Data.Maybe
open import Data.Bool
open import Data.Nat
open import Data.Nat.Properties  as NatProp

open import Relation.Nullary
open import Relation.Binary

open import Algebra

open import RedBlackTree
open import stack

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
-- check1 nothing _ = false
-- check1 (just n)  x with Data.Nat.compare (value n)  x
-- ...  | equal _ = true
-- ...  | _ = false

check2 : {m : Level } (n : Maybe (Node  ℕ ℕ)) → ℕ → Bool
check2 nothing _ = false
check2 (just n)  x with compare2 (value n)  x
...  | EQ = true
...  | _ = false

test1 : {m : Level} {A B C : Set} → putTree1 {Level.zero} {succ Level.zero} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ {!!} {!!} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 {m} x 1 ≡ true ))
test1 = {!!}

-- test2 : {m : Level} → putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
--     λ t → putTree1 t 2 2 (
--     λ t → getRedBlackTree t 1 (
--     λ t x → check2 {m} x 1 ≡ true   )))
-- test2 = refl

-- open ≡-Reasoning
-- test3 : {m : Level} → 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 {m} x 1 ≡ true
-- test3 {m} = begin
--     check2 {m} (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 : {m : Level} → putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 {m} x 1 ≡ true   ))
-- test9 = refl

-- test10 : {m : Level} → putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
--     λ t → putRedBlackTree t 2 2 (
--     λ t → getRedBlackTree t 1 (
--     λ t x → check2 {m} 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


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

checkT : {m : Level } (n : Maybe (Node  ℕ ℕ)) → ℕ → Bool
checkT nothing _ = false
checkT (just n) x with compTri (value n)  x
...  | tri≈ _ _ _ = true
...  | _ = false

checkEQ :  {m : Level }  ( x :  ℕ ) -> ( n : Node  ℕ ℕ ) -> (value n )  ≡ x  -> checkT {m} (just n) x ≡ true
checkEQ x n refl with compTri (value n)  x
... |  tri≈ _ refl _ = refl
... |  tri> _ neq gt =  ⊥-elim (neq refl)
... |  tri< lt neq _ =  ⊥-elim (neq refl)

-- checkEQ' :  {m : Level }  ( x y :  ℕ ) -> ( eq : x ≡ y  ) -> ( x ≟ y ) ≡ yes eq
-- checkEQ' x y refl with  x ≟ y
-- ... | yes refl = refl
-- ... | no neq = ⊥-elim ( neq refl )

---  search -> checkEQ
---  findNode -> search

redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} {A B C : Set Level.zero } → RedBlackTree {Level.zero} {m} {t} {A} {B} {C} a ℕ
redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; nodeComp = λ x x₁ → {!!} } -- record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compTri }


open stack.SingleLinkedStack
open stack.Element


insertP :  { a : Set } { t : Set } {P : Set }   → ( f : ( a  → t )  → t )  ( g : a  → t ) ( g' :  P  → a  → t )
   → ( p : P )
   → ( g ≡ g' p )
   →  f ( λ x → g' p x ) ≡ f ( λ x → g x )  
insertP f g g' p refl = refl


{-# TERMINATING #-}
inStack : {l : Level} (n : Node ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → Bool
inStack {l} n s with ( top s )
... | nothing = true
... | just n1 with  compTri (key n) (key (datum n1))
...            | tri> _ neq _ =  inStack {l} n ( record { top = next n1 } )
...            | tri< _ neq _ =  inStack {l} n ( record { top = next n1 } )
...            | tri≈  _ refl _  = false

record StackTreeInvariant  ( n : Node ℕ ℕ )
<<<<<<< working copy
        ( s : SingleLinkedStack (Node  ℕ ℕ) )  : Set where
||||||| base
        ( s : SingleLinkedStack (Node  ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where
=======
        ( s : SingleLinkedStack (Node ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where
>>>>>>> destination
  field
<<<<<<< working copy
    -- sti : replaceNode t s n $ λ  t1 → getRedBlackTree t1 (key n) (λ  t2 x1 → checkT x1 (value n)  ≡ True)
    notInStack : inStack n s ≡ True  → ⊥
||||||| base
    sti : replaceNode t s n $ λ  t1 → getRedBlackTree t1 (key n) (λ  t2 x1 → checkT x1 (value n)  ≡ True)
    notInStack : inStack n s ≡ True  → ⊥
=======
    sti : {m : Level} → replaceNode t s n $ λ  t1 → getRedBlackTree t1 (key n) (λ  t2 x1 → checkT {m} x1 (value n)  ≡ true)
    notInStack : {m : Level} → inStack {m} n s ≡ true  → ⊥
>>>>>>> destination

open StackTreeInvariant

<<<<<<< working copy
putTest1 : (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 = lemma0
   where
     tree0 : (n1 : Node  ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ
     tree0 n1 s = record { root = Just n1 ; nodeStack = s ; compare = compareT }
     lemma2 : (n1 : Node  ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → StackTreeInvariant (leafNode k x) s 
         → findNode (tree0 n1 s) s (leafNode k x) n1 (λ  tree1 s n1 → replaceNode tree1 s n1
              (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True)))
     lemma2 n1 s STI with compTri k (key n1)
     ... |  tri> le eq gt with (right n1) 
     ...                  | Just rightNode = {!!} -- ( lemma2 rightNode  ( record { top = Just ( cons n1 (top s)  ) }   )  (record {notInStack = {!!}  } ) )
     ...                  | Nothing with compTri k k
     ...                           | tri≈  _ refl _ = {!!}
     ...                           | tri< _ neq _ =  ⊥-elim (neq refl)
     ...                           | tri> _ neq _ =  ⊥-elim (neq refl)
     lemma2 n1 s STI |  tri< le eq gt = {!!}
     lemma2 n1 s STI |  tri≈ le refl gt = lemma5 s ( tree0 n1 s ) n1
        where 
           lemma5 :  (s : SingleLinkedStack (Node ℕ ℕ) )  → ( t :  RedBlackTree  ℕ ℕ  ) → ( n :  Node ℕ ℕ  ) → popSingleLinkedStack ( record { top = Just (cons n (SingleLinkedStack.top s)) }  )
                   ( \ s1  _ -> (replaceNode (tree0 n1 s1) s1 (record n1 { key = k ; value = x } ) (λ t → 
                      GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))) )
           lemma5 s t n with (top s)
           ...          | Just n2  with compTri k k
           ...            | tri< _ neq _ =  ⊥-elim (neq refl)
           ...            | tri> _ neq _ =  ⊥-elim (neq refl)
           ...            | tri≈  _ refl _  =  ⊥-elim ( (notInStack STI)  {!!} )
           lemma5 s t n | Nothing with compTri k k
           ...            | tri≈  _ refl _  = checkEQ x _ refl
           ...            | tri< _ neq _ =  ⊥-elim (neq refl)
           ...            | tri> _ neq _ =  ⊥-elim (neq refl)
     lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 n1 s) s (leafNode k x) n1 (λ  tree1 s n1 → replaceNode tree1 s n1
              (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True))))
     lemma0 = lemma2 n1 (record {top = Nothing}) ( record { notInStack = {!!} } )
...  | 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 with compTri k k 
     ... | tri≈  _ refl _ = checkEQ x _ refl
     ... | tri< _ neq _ =  ⊥-elim (neq refl)
     ... | tri> _ neq _ =  ⊥-elim (neq refl)
||||||| base
putTest1 : (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 = lemma0
   where
     tree0 : (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ
     tree0 s = record { root = Just n1 ; nodeStack = s ; compare = compareT }
     lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → StackTreeInvariant (leafNode k x) s (tree0 s)
         → findNode (tree0 s) s (leafNode k x) n1 (λ  tree1 s n1 → replaceNode tree1 s n1
              (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True)))
     lemma2 s STI with compTri k (key n1)
     ... |  tri≈ le refl gt = lemma5 s ( tree0 s ) n1
        where 
           lemma5 :  (s : SingleLinkedStack (Node ℕ ℕ) )  → ( t :  RedBlackTree  ℕ ℕ  ) → ( n :  Node ℕ ℕ  ) → popSingleLinkedStack ( record { top = Just (cons n (SingleLinkedStack.top s)) }  )
                   ( \ s1  _ -> (replaceNode (tree0 s1) s1 (record n1 { key = k ; value = x } ) (λ t → 
                      GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))) )
           lemma5 s t n with (top s)
           ...          | Just n2  with compTri k k
           ...            | tri< _ neq _ =  ⊥-elim (neq refl)
           ...            | tri> _ neq _ =  ⊥-elim (neq refl)
           ...            | tri≈  _ refl _  =  ⊥-elim ( (notInStack STI)  {!!} )
           lemma5 s t n | Nothing with compTri k k
           ...            | tri≈  _ refl _  = checkEQ x _ refl
           ...            | tri< _ neq _ =  ⊥-elim (neq refl)
           ...            | tri> _ neq _ =  ⊥-elim (neq refl)
     ... |  tri> le eq gt = sti ( record { sti = {!!} ; notInStack = {!!}  } )
     ... |  tri< le eq gt = {!!}
     lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 s) s (leafNode k x) n1 (λ  tree1 s n1 → replaceNode tree1 s n1
              (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True))))
     lemma0 = lemma2 (record {top = Nothing}) ( record { sti = {!!}  ; notInStack = {!!} } )
...  | 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 with compTri k k 
     ... | tri≈  _ refl _ = checkEQ x _ refl
     ... | tri< _ neq _ =  ⊥-elim (neq refl)
     ... | tri> _ neq _ =  ⊥-elim (neq refl)
=======

-- testn :  {!!}
-- testn  =  putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 2 2
--   $ λ t → putTree1 t 1 1
--   $ λ t → putTree1 t 3 3 (λ ta → record {root = root ta ; nodeStack = nodeStack ta })


-- List と Node で書こうとしたがなんだかんだListに直したほうが楽そうだった

nullNode = (record {key = 0 ; value = 0 ; right = nothing ; left = nothing ; color = Red})

-- treeTotal : { m : Level } {t : Set m} → ( s : List ℕ ) → ( tr : (Node ℕ ℕ) ) → (List ℕ → t) → t
-- treeTotal {m} {t} s tr next with (left tr) | (right tr)
-- treeTotal {m} {t} s tr next | nothing | nothing = next ((key tr) ∷ [])
-- treeTotal {m} {t} s tr next | nothing | just x = treeTotal {m} {t} s x (λ li → next ((key tr) ∷ li))
-- treeTotal {m} {t} s tr next | just x | nothing = treeTotal {m} {t} s x (λ li → next ((key tr) ∷ li))
-- treeTotal {m} {t} s tr next | just x | just x₁ = treeTotal {m} {t} s x (λ li1 → treeTotal {m} {t} s x₁ (λ li2 → next (s ++ li1 ++ li2)))
treeTotal : { n m : Level } {a : Set n} {t : Set m} → ( s : List a ) → ( tr : (Node a a) ) → List a
treeTotal {n} {m} {a} {t} s tr with (left tr) | (right tr)
treeTotal {n} {m} {a} {t} s tr | nothing | nothing = (key tr) ∷ []
treeTotal {n} {m} {a} {t} s tr | nothing | just x = (key tr) ∷ (treeTotal {n} {m} {a} {t} s x)
treeTotal {n} {m} {a} {t} s tr | just x | nothing = (key tr) ∷ (treeTotal {n} {m} {a} {t} s x)
treeTotal {n} {m} {a} {t} s tr | just x | just x₁ = s ++ ((key tr) ∷ (treeTotal {n} {m} {a} {t} s x) ++ (treeTotal {n} {m} {a} {t} s x₁))


-- treeTotalA : { m : Level } {t : Set m} → ( s : List ℕ ) → ( tr : (Node ℕ ℕ) ) → List ℕ

-- (treeTotal {_} {ℕ} ([]) (Data.Maybe.fromMaybe nullNode (root (putTree1 {_} {_} {ℕ} {ℕ} testn 5 5 {!!}))))

-- exput : (treeTotal {_} {ℕ} (5 ∷ []) (Data.Maybe.fromMaybe nullNode (root (createEmptyRedBlackTreeℕ ℕ))) (λ total → {!!})) ≡ {!!}
-- exput = {!!}


-- aaa = (treeTotal {_} {_} {ℕ} {_} (5 ∷ []) ((record { key = 4 ; value = 4 ; right = just (leafNode 6 6) ; left = just (leafNode 3 3) ; color = Black })))


-- fuga = putTree1 {_} {_} {ℕ} {ℕ} (record {root = just (record { key = 4 ; value = 4 ; right = just (leafNode 6 6) ; left = just (leafNode 3 3) ; color = Black }) ; nodeStack = ( record {top = nothing}) ; compare = (λ x x₁ → EQ) }) 5 5 (λ aaa → aaa )

-- nontree ++ 2 :: []

-- piyo =  putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 2 2 ( λ t1 → findNode t1 (record {top = nothing}) (leafNode 2 2) (Data.Maybe.fromMaybe nullNode (root t1)) (λ tree stack node → {!!}))


-- exn2l : {!!} ≡ (treeTotal {_} {ℕ} ([]) (putTree1 {_} {_} {ℕ} {ℕ} {!!} 5 5 (λ t → {!!}))) -- (treeTotal {_} {ℕ} (5 ∷ []) (Data.Maybe.fromMaybe nullNode (root testn)))
-- exn2l = refl





-- record FS {n m : Level } {a : Set n} {t : Set m} (oldTotal : List a) ( s : List a ) ( tr : (Node a a) ) : Set where
--   field
--     total : treeTotal {n} {m} {a} {t} s tr ≡ oldTotal
-- -- usage = FS.total -- relation

-- data P { n m : Level } { t : Set m } : Set where
--   P₀ : (old : List ℕ) ( s : List ℕ ) → (tr : (Node ℕ ℕ) ) → FS {m} {t} old s tr → P



-- ttt = putTree1 {_} {_} {ℕ} {ℕ}

-- record TreeInterface {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set n where
--   field
--     tree : treeImpl
--     list : List ℕ
--     node : Node ℕ ℕ
--     putTreeHoare : (FS {_} {ℕ} list list node) → putTree1 {!!} {!!} {!!} {!!}

stack2list : {n m : Level} {t : Set m} {a : Set n} → (s : SingleLinkedStack a) → List a
stack2list stack with top stack
stack2list stack | just x = (datum x) ∷ (elm2list {_} {_} {ℕ} x)
  where
    elm2list : {n m : Level} {t : Set m} {a : Set n} → (elm : (Element a)) → List a
    elm2list el with next el
    elm2list el | just x = (datum el) ∷ (elm2list {_} {_} {ℕ} x)
    elm2list el | nothing = (datum el) ∷ []
stack2list stack | nothing = []


-- list2element : {n m : Level} {t : Set m} {a : Set n} → (l : List a) → Maybe (Element a)
-- list2element [] = nothing
-- list2element (x ∷ l) = just (cons x (list2element {_} {_} {ℕ} l))

-- ltest = list2element (1 ∷ 2 ∷ 3 ∷ [])

list2stack : {n m : Level} {t : Set m} {a : Set n} {st : SingleLinkedStack a} → (l : List a)  → SingleLinkedStack a
list2stack {n} {m} {t} {a} {s} (x ∷ l)  = pushSingleLinkedStack s x (λ s1 → list2stack {n} {m} {t} {a} {s1} l )
list2stack {n} {m} {t} {a} {s} [] = s



-- stest = list2stack (1 ∷ 2 ∷ 3 ∷ [])

open Node

exfind : { m : Level } { t : Set m} → (dt : ℕ) → (node : (Node ℕ ℕ))  → (st : List ℕ) →  findNode {_} {_} {ℕ} {ℕ} (redBlackInSomeState ℕ (just node)) (emptySingleLinkedStack) (leafNode dt dt) (node) (λ t1 st1 n1 → (( treeTotal {_} {m} {ℕ} {t} (dt ∷ st) (node) ) ≡ ( treeTotal {_} {m} {ℕ} {t} (dt ∷ st) (node) ) ))
exfind dt node st with left node | right node
exfind dt node st | just x | just x₁ = {!!}
exfind dt node st | just x | nothing = {!!}
exfind dt node st | nothing | just x = {!!}
exfind dt node st | nothing | nothing with (compTri dt (key node))
exfind dt node st | nothing | nothing | tri< a ¬b ¬c = {!!}
exfind dt node st | nothing | nothing | tri≈ ¬a b ¬c = {!!}
exfind dt node st | nothing | nothing | tri> ¬a ¬b c = {!!}

-- exput : (ni : ℕ) → (tn : Node ℕ ℕ) → (ts : List ℕ) → (treeTotal {_} {ℕ} (ni ∷ ts) tn)
--                  ≡ (treeTotal {_} {ℕ} (ts) (Data.Maybe.fromMaybe nullNode (root (putTree1 {_} {_} {ℕ} {ℕ} (record { root = just tn } ) ni ni (λ tt → tt)))))
-- exput datum node [] with (right node) | (left node)
-- exput datum node [] | nothing | nothing = {!!}
-- exput datum node [] | just x | just x₁ = {!!}
-- exput datum node [] | just x | nothing = {!!}
-- exput datum node [] | nothing | just x = {!!}
-- exput datum node (x ∷ stack₁) = {!!}


-- proofTree : {n m : Level} {t : Set m} {a : Set n} (old stackl : List ℕ) → (node : Node ℕ ℕ) → (FS {_} {ℕ} old stackl node) → (tree : RedBlackTree ℕ ℕ) → (key : ℕ) → findNode  {{!!}} {{!!}} {{!!}} {{!!}} tree (list2stack {!!} (record {top = nothing})) (leafNode key key) node (λ tree1 stack1 datum → {!!})
-- -- -- -- putTree1 tree key key (λ t → (FS {_} {ℕ} old stackl (Data.Maybe.fromMaybe nullNode (root tree))) )
-- proofTree old stack node fs t k = {!!}

-- FS は 証明そのものになると思ってたけど実は違いそう
-- oldTotal と 現在の node, stack の組み合わせを比較する
-- oldTotal はどうやって作る? ><
-- treeTotal は list と node を受け取って それの total を出すのでそれで作る(list に put するデータなどを入れることで適当に作れる)

-- p : {n m : Level} {t : Set m} {a : Set n} → ( s : SingleLinkedStack ℕ )  ( tr : (Node ℕ ℕ) ) ( tree : RedBlackTree ℕ ℕ ) (k : ℕ) →  (FS (treeTotal (k ∷ (stack2list s)) tr) (stack2list s) tr) → putTree1 tree k k (λ atree  → FS (treeTotal (stack2list s) (Data.Maybe.fromMaybe (tr) (root atree))) {!!} {!!})
-- p stack node tree key = {!!}

-- tt = (FS {_} {ℕ} [] [] (Data.Maybe.fromMaybe nullNode (root (createEmptyRedBlackTreeℕ {_} ℕ {ℕ}))))

-- ttt : (a : P) → P
-- ttt a = P₀ {!!} {!!} (record { key = {!!} ; value = {!!} ; right = {!!} ; left = {!!} ; color = {!!} }) (record { total = {!!} })


-- FS では stack tree をあわせた整合性を示したい
-- そのためには...?
-- stack は前の node (というか一段上)が入ってる
-- tree は現在の node がある


 --   tr(Node ℕ ℕ)      s (List (Node))
 --     3                  []
 --    / \
 --   2   5
 --  /   / \
 -- 1   4   6

 --   search 6 (6 > 3)
 --   tr(Node ℕ ℕ)      s (List (Node))
 --     5                 just (node (1 2 nothing) 3 (4 5 6)
 --    / \                 []
 --   4   6

--   search 6 (6 > 5)
--   tr(Node ℕ ℕ)      s (List (Node))
--       6              just (node (4 5 6))
--                      just (node (1 2 nothing) 3 (4 5 6)
--                       []

-- just 6 → true みたいな感じ

-- stack に node ごと入れるのは間違い…？
-- 一応非破壊な感じがする(新しく作り直してる)
-- どう釣り合いをとるか

-- stack+tree : {n m : Level} {t : Set m} → List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → (Maybe (Node ℕ ℕ) → t) → t
-- stack+tree {n} stack mid org = st stack mid org where
-- st : List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → Maybe (Node ℕ ℕ)
-- st [] _ _ = nothing
-- st (x ∷ []) n n1 with Data.Nat.compare (key x) (key org) | Data.Nat.compare (value x) (value org)
-- st (x ∷ []) n n1 | equal .(key x) | equal .(value x) = just org
-- st (x ∷ []) n n1 | _ | _ = nothing
-- st (x ∷ a)  n n1 with st a n n1
-- st (x ∷ a) n n1 | just x₁ = {!!}
-- st (x ∷ a) n n1 | nothing = nothing


-- stack+tree : {n m : Level} {t : Set m} → List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → (Maybe (Node ℕ ℕ) → t) → t
-- stack+tree {n} stack mid org cg = st stack mid org
--   where
--            st : List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → Maybe (Node ℕ ℕ)
--            st [] _ _ = nothing
--            st (x ∷ []) n n1 with Data.Nat.compare (key x) (key org) | Data.Nat.compare (value x) (value org)
--            st (x ∷ []) n n1 | equal .(key x) | equal .(value x) = just org
--            st (x ∷ []) n n1 | _ | _ = nothing
--            st (x ∷ a)  n n1 with st a n n1
--            st (x ∷ a) n n1 | just x₁ = {!!}
--            st (x ∷ a) n n1 | nothing = nothing

-- findNodePush : {n : Level}  → (stack : List (Node ℕ ℕ)) → (mid : Node ℕ ℕ) → (org : Node ℕ ℕ) → stack+tree stack mid org ≡ just ?
--                → ? {return (? ∷ stack),mid'} → stack+tree (? ∷ stack) (mid') org ≡ just ?
-- findNodePush 

-- stack+tree が just だって言えたらよい
-- {}2 は orig の どっちかのNode

>>>>>>> destination