# HG changeset patch
# User soto
# Date 1613167218 -32400
# Node ID 2521da2c3c9a5dae3214b86a3c01baaa55b7b1b3
# Parent  724766af8b1274628462b3dec4f57970812576f3
WIP rbt_delete

diff -r 724766af8b12 -r 2521da2c3c9a rbt_delete.agda
--- a/rbt_delete.agda	Thu Feb 11 19:33:35 2021 +0900
+++ b/rbt_delete.agda	Sat Feb 13 07:00:18 2021 +0900
@@ -14,6 +14,23 @@
 -- これあれか、また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)
@@ -36,8 +53,6 @@
                              ; varl = Env.varl env
                              })
 
-
-
 -- serch min
 -- exit時は終了
 -- next時は自己実行
@@ -52,42 +67,195 @@
                               ; 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 : {le : Level} {t : Set le} → Env → ℕ → (next : Env → t) → (exit : Env → t) → t
-bt-delete env n next exit with Env.vart env
+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 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
+... | 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}
 
 
-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
+-- 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
@@ -97,10 +265,6 @@
 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
@@ -109,10 +273,52 @@
 ... | bt-node node with node.number (tree.key node)
 ... | n = n == num
 
-a = search-min test'15 (λ env → env)
+
+{-# 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
diff -r 724766af8b12 -r 2521da2c3c9a rbt_delete.agdai
Binary file rbt_delete.agdai has changed
diff -r 724766af8b12 -r 2521da2c3c9a rbt_t.agda
--- a/rbt_t.agda	Thu Feb 11 19:33:35 2021 +0900
+++ b/rbt_t.agda	Sat Feb 13 07:00:18 2021 +0900
@@ -262,10 +262,15 @@
 
 
 -- 以下test部分
-test1 = whileTestPCall' bt-empty 0
-test2 = whileTestPCall' (vart test1) 1
-test3 = whileTestPCall' (vart test2) 2
-test4 = whileTestPCall' (vart test3) 3
-test5 = whileTestPCall' (vart test4) 4
-test6 = whileTestPCall' (vart test5) 5
-test7 = whileTestPCall' (vart test6) 6
+test1 = whileTestPCall' bt-empty 8
+test2 = whileTestPCall' (vart test1) 10
+test3 = whileTestPCall' (vart test2) 24
+test4 = whileTestPCall' (vart test3) 31
+test5 = whileTestPCall' (vart test4) 41
+test6 = whileTestPCall' (vart test5) 45
+test7 = whileTestPCall' (vart test6) 50
+test8 = whileTestPCall' (vart test7) 59
+test9 = whileTestPCall' (vart test8) 73
+test10 = whileTestPCall' (vart test9) 74
+test11 = whileTestPCall' (vart test10) 79
+
diff -r 724766af8b12 -r 2521da2c3c9a rbt_t.agdai
Binary file rbt_t.agdai has changed