module rbt_delete where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat hiding (compare)

open import Data.List
open import Data.Bool

open import Data.Nat.Properties as NatProp -- <-cmp
open import Relation.Binary -- need <-cmp relation

open import rbt_t

-- これあれか、またmergeする時にListにして今回はさらにbaranceも保持しないといけないのか
-- 再起処理側はmerge側に

rbt-find : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
rbt-find env next exit with (Env.varn env)
... | n with (Env.vart env)
... | bt-empty = exit (record
                              { vart = bt-empty
                              ; varn = Env.varn env
                              ; varl = Env.varl env
                              })
... | bt-node node with node.number (tree.key node)
... | x with <-cmp n x
... | tri≈ ¬a b ¬c = exit env
... | tri< a ¬b ¬c = next (record
                             { vart = tree.ltree node
                             ; varn = Env.varn env
                             ; varl = Env.varl env
                             })
... | tri> ¬a ¬b c = next (record
                             { vart = tree.rtree node
                             ; varn = Env.varn env
                             ; varl = Env.varl env
                             })



-- serch min
-- exit時は終了
-- next時は自己実行
rbt-search-min : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
rbt-search-min env next exit with Env.vart env
... | bt-empty = exit env
... | bt-node node with tree.ltree node
... | bt-empty = exit env
... | bt-node lnode = next (record
                              { vart = bt-node lnode
                              ; varn = Env.varn env
                              ; varl = Env.varl env
                              })

-- find(分岐から)　分岐後、delete → balance → 終了

-- 右も左もenptyならreturn node をexit
-- numberが一致しているなら, next(自己実行)へ
bt-delete : {le : Level} {t : Set le} → Env → ℕ → (next : Env → t) → (exit : Env → t) → t
bt-delete env n next exit with Env.vart env
... | bt-empty = exit env
... | bt-node node with (node.number (tree.key node))
... | num with <-cmp num n
... | tri< a ¬b ¬c = next {!!} -- listに左右どちらのbalanceなのか保持する。mergeする際にそれを参照する
... | tri> ¬a ¬b c = next {!!} -- 同上
... | tri≈ ¬a b ¬c with  node
... | record { key = key ; ltree = bt-empty ; rtree = bt-empty } = exit {!!} -- colerを赤にしてexit
... | record { key = key ; ltree = bt-node node₁ ; rtree = bt-empty } = {!!} -- leftのcolerを黒にしてexit
... | record { key = key ; ltree = ltree ; rtree = bt-node node₁ } = {!!} -- なんかやって右balance

-- bt-delete record { vart = bt-empty ; varn = varn ; varl = varl } selfdo next exit = {!!}
-- bt-delete record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } selfdo next exit = {!!}



test'1 = whileTestPCall' bt-empty 0
test'2 = whileTestPCall' (rbt_t.Env.vart test'1) 1
test'3 = whileTestPCall' (rbt_t.Env.vart test'2) 2
test'4 = whileTestPCall' (rbt_t.Env.vart test'3) 3
test'5 = whileTestPCall' (rbt_t.Env.vart test'4) 4
test'6 = whileTestPCall' (rbt_t.Env.vart test'5) 5
test'7 = whileTestPCall' (rbt_t.Env.vart test'6) 6
test'8 = whileTestPCall' (rbt_t.Env.vart test'7) 7
test'9 = whileTestPCall' (rbt_t.Env.vart test'8) 8
test'10 = whileTestPCall' (rbt_t.Env.vart test'9) 9
test'11 = whileTestPCall' (rbt_t.Env.vart test'10) 10
test'12 = whileTestPCall' (rbt_t.Env.vart test'11) 11
test'13 = whileTestPCall' (rbt_t.Env.vart test'12) 12
test'14 = whileTestPCall' (rbt_t.Env.vart test'13) 13
test'15 = whileTestPCall' (rbt_t.Env.vart test'14) 14

{-# TERMINATING #-}
find-com : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
find-com env exit = rbt-find env (λ env → find-com env exit ) exit

--init
find : {l : Level} {t : Set l} → rbt → ℕ → (exit : Env → t) → t
find tree num exit = find-com (record{ vart = tree ; varn = num; varl = [] }) exit

{-# TERMINATING #-}
search-min : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
search-min env exit = rbt-search-min env (λ env → search-min env exit ) exit

open import Agda.Builtin.Nat

check-find : Env → ℕ → Bool
check-find tree num with Env.vart tree
... | bt-empty = false
... | bt-node node with node.number (tree.key node)
... | n = n == num

a = search-min test'15 (λ env → env)

b = find (Env.vart test'15) 123 (λ env → env)



c = check-find (find (Env.vart test'15) 1 (λ env → env) ) 1