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


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

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

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

search-min : rbt → ℕ
search-min tree = search-min-p (record { vart = tree ; varn = zero ; varl = [] }) (λ env → Env.varn env)

test-search-min = search-min (rbt_t.Env.vart test'15)

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

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

merge-tree-c : {le : Level} {t : Set le} → Env → (next-bl : Env → t) →  (next-br : Env → t) → (exit : Env → t) → t
merge-tree-c env next-bl next-br exit with Env.vart env
... | bt-empty = exit env
... | bt-node node with Env.varl env
... | [] = exit env
... | bt-empty ∷ varl = exit env
... | bt-node xtree ∷ varl with <-cmp (node.number (tree.key node)) (node.number (tree.key xtree))
... | tri≈ ¬a b ¬c = exit env
... | tri< a ¬b ¬c = next-bl record env{vart = bt-node record xtree{ltree = Env.vart env} ; varl = varl}
... | tri> ¬a ¬b c = next-br record env{vart = bt-node record xtree{rtree = Env.vart env} ; varl = varl}

-- 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 = {!!}

-- do branch
-- next12 rotate_left → barance-12-c
-- next47 part-tree → rotate_right → barance-47-bc → rotate_left → barance-47-fc
-- exit merge_tree
balance_left-c : {le : Level} {t : Set le} → Env → (next12 : Env → t) → (next47 : Env → t) → (exit : Env → t) → t
balance_left-c env next12 next47 exit with (Env.varn env) -- flag
... | suc d = exit env -- flug true
... | zero with (Env.vart env)
... | bt-empty = exit env
... | bt-node node with (tree.rtree node)
... | bt-empty = exit env
... | bt-node rtree with (tree.ltree rtree)
... | bt-empty = exit env
... | bt-node rltree with (node.coler (tree.key rltree))
... | black = next12 env
... | red = next47 record env{vart = tree.rtree node; varl = (bt-node record node{rtree = bt-empty}) ∷ (Env.varl env)}  -- part-treeする

-- next merge-tree
barance-12-c : {le : Level} {t : Set le} → Env → (next : Env → t) → t
barance-12-c env next with (Env.vart env)
... | bt-empty = next env
... | bt-node node with (node.coler (tree.key node))
... | red = next record env{vart = bt-node record node{key = record (tree.key node){coler = black} } }
... | black = next record env{varn = 0}


-- do merge-tree rtree
-- post rotate-left → barance-47-fc
barance-47-bc : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
barance-47-bc env next exit with (Env.varl env)
... | [] = next env
... | bt-empty ∷ s = next env
... | bt-node node ∷ s = next record env{vart = bt-node record node{rtree = Env.vart env} ; varl = s}

-- do rewrite
-- post merge-tree
barance-47-fc : {le : Level} {t : Set le} → Env → (next : Env → t) → t
barance-47-fc env next with (Env.vart env)
... | bt-empty = next env
... | bt-node node with tree.ltree node
... | bt-empty = next env
... | bt-node ltree  with tree.rtree node
... | bt-empty = next env
... | bt-node rtree = next record env{vart = bt-node record node{
  rtree = bt-node record rtree{
    key = record (tree.key rtree){
      coler = black} } ;
  ltree = bt-node record ltree{
    key = record (tree.key ltree){
      coler = black} } } }

-- do branch
-- next12 rewrite → barance-12-c
-- next3 barance-3c
-- next58 rotate_right → barance-58-c
-- exit merge_tree
balance_right-c : {le : Level} {t : Set le} → Env → (next12 : Env → t) → (next3 : Env → t) → (next58 : Env → t) → (exit : Env → t) → t
balance_right-c env next12 next3 next58 exit with (Env.varn env) -- flag
... | suc d = exit env -- flug true
... | zero with (Env.vart env)
... | bt-empty = exit env
... | bt-node node with (tree.ltree node)
... | bt-empty = exit env
... | bt-node ltree with (tree.ltree ltree)
... | bt-empty = exit env
... | bt-node lltree with (node.coler (tree.key lltree))
... | red = next58 env
... | black with (node.coler (tree.key ltree))
... | black = next12 record env{vart = bt-node record node{
  ltree = bt-node record ltree{
    key = record(tree.key ltree){
      coler = red} }}}
... | red = next3 env

-- do rewrite
-- post merge-tree
balance-58-c : {le : Level} {t : Set le} → Env → (next : Env → t) → t -- 47-bcと一緒
balance-58-c env next with (Env.vart env)
... | bt-empty = next env
... | bt-node node with tree.ltree node
... | bt-empty = next env
... | bt-node ltree  with tree.rtree node
... | bt-empty = next env
... | bt-node rtree = next record env{vart = bt-node record node{
  rtree = bt-node record rtree{
    key = record (tree.key rtree){
      coler = black} } ;
  ltree = bt-node record ltree{
    key = record (tree.key ltree){
      coler = black} } } }

-- do branch
-- next-r rotate-right → barance-3-rc
-- next-l part-tree left → rotate-left → barance-3-lbc(marge-tree left) → rotate-right → barance-3-lfc
-- exit merge-tree
balance-3-c : {le : Level} {t : Set le} → Env → (next-r : Env → t) → (next-l : Env → t) → (exit : Env → t) → t
balance-3-c env next-r next-l exit with (Env.vart env)
... | bt-empty = exit env
... | bt-node node with tree.ltree node
... | bt-empty = exit env
... | bt-node ltree  with tree.rtree ltree
... | bt-empty = exit env
... | bt-node lrtree  with tree.ltree lrtree
... | bt-empty = exit env
... | bt-node lrltree with (node.coler (tree.key lrltree))
... | black = next-r env
... | red =  next-l record env{vart = tree.ltree node; varl = (bt-node record node{ltree = bt-empty}) ∷ (Env.varl env)} -- part-tree left

-- do rewrite
-- next marge-tree
barance-3-rc : {le : Level} {t : Set le} → Env → (next : Env → t) → t
barance-3-rc env next with (Env.vart env)
... | bt-empty = next env
... | bt-node node with tree.rtree node
... | bt-empty = next env
... | bt-node rtree  with tree.ltree rtree
... | bt-empty = next env
... | bt-node rltree = next record env{vart = bt-node record node{
  rtree = bt-node record rtree{
    key = record (tree.key rtree){
      coler = black};
    ltree =  bt-node record rltree{
      key = record (tree.key rltree){coler = red}} } } }

-- do marge-tree left
-- next rotate-right → barance-3-lfc
barance-3-lbc : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
barance-3-lbc env next exit with (Env.varl env)
... | [] = exit env
... | bt-empty ∷ s = exit env
... | bt-node node ∷ s = next record env{vart = bt-node record node{ltree = Env.vart env} ; varl = s}

-- do rewrite
-- next marge-tree
barance-3-lfc : {le : Level} {t : Set le} → Env → (next : Env → t) → t
barance-3-lfc env next with (Env.vart env)
... | bt-empty = next env
... | bt-node node with tree.rtree node
... | bt-empty = next env
... | bt-node rtree with tree.ltree node
... | bt-empty = next env
... | bt-node ltree  with tree.rtree ltree
... | bt-empty = next env
... | bt-node lrtree = next record env{vart = bt-node record node{
  rtree = bt-node record rtree{
    key = record (tree.key rtree){
      coler = black};
    ltree =  bt-node record lrtree{
      key = record (tree.key lrtree){coler = red}} } } }

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

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


{-# TERMINATING #-}
bt-delete-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
bt-delete-p env exit = bt-delete-c env (λ env → bt-delete-p env exit) exit

balance-12-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
balance-12-p env exit = merge-rotate-left env (λ env → barance-12-c env exit) exit

balance-47-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
balance-47-p env exit = merge-rotate-right env (λ env → barance-47-bc env (λ env → merge-rotate-left env (λ env → barance-47-fc env exit) exit) exit) exit

-- exit merge-tree
balance_left-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
balance_left-p env exit = balance_left-c env (λ env → balance-12-p env exit) (λ env → balance-47-p env exit) exit

balance-3-r-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
balance-3-r-p env exit = merge-rotate-right env (λ env → barance-3-rc env exit) exit


balance-3-l-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
balance-3-l-p env exit = merge-rotate-left env (λ env → barance-3-lbc env (λ env → merge-rotate-right env (λ env → barance-3-lfc env exit) exit) exit) exit


balance-3-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
balance-3-p env exit = balance-3-c env  (λ env → balance-3-r-p env exit)  (λ env → balance-3-l-p env exit) exit

balance-58-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
balance-58-p env exit = merge-rotate-right env  (λ env → balance-58-c env exit) exit

-- exit merge-tree
balance_right-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
balance_right-p env exit = balance_right-c env (λ env → barance-12-c env exit) (λ env → balance-3-p env exit) (λ env → balance-58-p env exit) exit

{-# TERMINATING #-}
delete-merge-tree-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
delete-merge-tree-p env exit = merge-tree-c env (λ env → balance_left-p env  (λ env → delete-merge-tree-p env exit)) (λ env → balance_right-p env  (λ env → delete-merge-tree-p env exit)) exit

bt-delete-init :  Env → rbt
bt-delete-init env = bt-delete-p env (λ env → delete-merge-tree-p env (λ env → Env.vart env))

bt-delete : rbt → ℕ → rbt
bt-delete rbt n = bt-delete-init (record { vart = rbt ; varn = n ; varl = [] })

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

test = bt-delete (Env.vart test'15) 0


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