--- a/rbt_delete.agda	Sat Feb 13 07:00:18 2021 +0900
+++ b/rbt_delete.agda	Sat Feb 13 19:50:11 2021 +0900
@@ -61,37 +61,73 @@
 ... | 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
-                              })
+... | bt-node lnode = next record env{vart = bt-node lnode}
 
 {-# 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)
+search-min : Env → Env
+search-min env = search-min-p env (λ env → env)
 
-test-search-min = search-min (rbt_t.Env.vart test'15)
+test-search-min = search-min (record { vart = (rbt_t.Env.vart test'15) ; varn = 1 ; varl = [] })
 
 -- 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
+-- next1 → search-min →  →  delete(min) → 
+-- exit1 bt-delete-1c → merge-tree-c
+-- exit → merge-tree
+bt-delete-c : {le : Level} {t : Set le} → Env → (next : Env → t) → (next-1 : Env → t) → (exit-1 : Env → t) → (exit : Env → t)  → t
+bt-delete-c env next next1 exit1 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 = next record env{vart = tree.rtree node;
+  varl = (bt-node record node{
+    rtree = bt-empty}) ∷ (Env.varl env)} -- listに左右どちらのbalanceなのか保持する。mergeする際にそれを参照する
+... | tri> ¬a ¬b c = next record env{vart = tree.ltree node;
+  varl = (bt-node record node{
+    ltree = 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
+... | record { key = key ; ltree = bt-empty ; rtree = bt-empty } = exit1 env
+... | record { key = key ; ltree = bt-node ltree ; rtree = bt-empty } = exit record env{
+  vart = bt-node record ltree{
+    key = record (tree.key ltree){
+      coler = black}} } -- leftのcolerを黒にしてexit
+... | record { key = key ; ltree = bt-empty ; rtree = bt-node rtree } = next1 record env{
+  vart = tree.rtree node ;
+  varl = (bt-node  node) ∷ (Env.varl env)}  -- なんかやって右balance
+... | record { key = key ; ltree = bt-node ltree ; rtree = bt-node rtree } = next1 record env{
+  vart = tree.rtree node ;
+  varl = (bt-node  node) ∷ (Env.varl env)}  -- なんかやって右balance
+
+-- do rerwite
+-- exit delete
+-- vartのkeyをxtreeに入れてexit
+bt-delete-both-c : {le : Level} {t : Set le} → Env → (exit : Env → t) → t
+bt-delete-both-c env exit with Env.varl env
+... | [] = exit env
+... | bt-empty ∷ varl = exit env
+... | bt-node xtree ∷ varl with Env.vart env
+... | bt-empty = exit env
+... | bt-node node = exit record env{
+  vart = tree.rtree xtree ;
+  varn = node.number (tree.key node) ;
+  varl = bt-node record xtree{key = tree.key node ; rtree = bt-empty } ∷ varl}
+
+
+--- do rewrite
+bt-delete-1c : {le : Level} {t : Set le} → Env → (exit : Env → t) → t
+bt-delete-1c env exit with Env.varl env
+... | [] = exit env
+... | x ∷ s with Env.vart env
+... | bt-empty = exit env
+... | bt-node node with (node.coler (tree.key node))
+... | red = exit record env{varn = 0 ; vart = x ; varl = s}
+... | black = exit record env{varn = 1 ; vart = x ; varl = s}
+
 
 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
@@ -104,8 +140,6 @@
 ... | 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
@@ -274,9 +308,13 @@
 ... | n = n == num
 
 
+
+bt-delete-both-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+bt-delete-both-p env exit = search-min-p env (λ env → bt-delete-both-c env exit)
+
 {-# 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
+bt-delete-p env exit = bt-delete-c env (λ env → bt-delete-p env exit) (λ env → bt-delete-both-p env (λ env → bt-delete-p env exit) ) (λ env → bt-delete-1c 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
@@ -318,9 +356,10 @@
 
 b = find (Env.vart test'15) 123 (λ env → env)
 
-test = bt-delete (Env.vart test'15) 0
+test-delete1 =  bt-delete-p (record { vart = (Env.vart test'7) ; varn = 5 ; varl = [] }) (λ env → env)
+
+test = bt-delete (Env.vart test'7) 1
 
 
 c = check-find (find (Env.vart test'15) 1 (λ env → env) ) 1
 
-

Binary file rbt_delete.agdai has changed