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

{-# 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 ℕ ℕ )
        ( s : SingleLinkedStack (Node ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where
  field
    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  → ⊥

open StackTreeInvariant


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