# HG changeset patch
# User ryokka
# Date 1559174043 -32400
# Node ID 7c9b8d601b771991b391ea3a4d1e7adfef71cdca
# Parent  7ed7c121d5b8ca47d93d1d126f1e939bc303c83f
fix deleteMin

diff -r 7ed7c121d5b8 -r 7c9b8d601b77 RBTree.agda
--- a/RBTree.agda	Tue May 14 02:35:21 2019 +0900
+++ b/RBTree.agda	Thu May 30 08:54:03 2019 +0900
@@ -251,12 +251,12 @@
 
   unbalanceL : Color → ℕ → RBTree a → ℕ → RBTree a → (RBTreeBDel a → cg) → cg
   unbalanceL c h l@(node black _ _ _ _) x r cg = turnR l (λ tl → (balanceL black h tl x r (λ t → isColorSame {n} {m} {a} {_} c black (λ issame → cg record {tree = t ; bool = issame}))))
-  unbalanceL Black h l@(node red lh ll lx lr@(node black _ _ _ _)) x r  cg = turnR lr (λ tlr → balanceL black h tlr x r (λ t → cg record { tree = (node black lh ll lx t) ; bool = false}))
+  unbalanceL black h l@(node red lh ll lx lr@(node black _ _ _ _)) x r  cg = turnR lr (λ tlr → balanceL black h tlr x r (λ t → cg record { tree = (node black lh ll lx t) ; bool = false}))
   unbalanceL c h l x r  cg = cg record {tree = leaf ; bool = false}
 
   unbalanceR : Color → ℕ → RBTree a → ℕ → RBTree a → (RBTreeBDel a → cg) → cg
   unbalanceR c h l x r@(node black _ _ _ _) cg = turnR r (λ tr → balanceR black h l x r (λ t → isColorSame {n} {m} {a} {_} c black (λ issame → cg record {tree = t ; bool = issame})))
-  unbalanceR Black h l x (node R rh rl@(node black _ _ _ _) rx rr) cg = turnR rl (λ trl → balanceR black h l x trl (λ t → cg record { tree = (node black rh t rx rr); bool = false}))
+  unbalanceR black h l x (node red rh rl@(node black _ _ _ _) rx rr) cg = turnR rl (λ trl → balanceR black h l x trl (λ t → cg record { tree = (node black rh t rx rr); bool = false}))
   unbalanceR c h l x r cg  = cg record {tree = leaf ; bool = false}
 
 
@@ -381,15 +381,22 @@
 ```
 
 たぶん ((l', d), m) の形になると deleteMin' がしたい
-RBTreeBDel の bool 情報はleaf に着いたかどうかだけ
-ん、node の左に leaf がついてる最小パターン探せばいいのでは？
+~~RBTreeBDel の bool 情報はleaf に着いたかどうかだけ~~ → ではなく unbalance する必要があるのかの確認
+
+ん、じゃあ node の左に leaf がついてる最小パターン探せばいいのでは？
 
+あるパターンは (leaf x leaf), (leaf x r) の2パターンと r が red のケースを含めて 3パターン
+その上のノードからそれを確認すれば良いので
+(node c h (node lc lh leaf lx leaf) x r) と lr が存在するケースを確認すると良い
+終わった tree に対して unbalance するかしないかを確定させたら終わり
 --}
 
+
+
   {-# TERMINATING #-}
   deleteMin' : RBTree ℕ → (RBTreeBDel ℕ → cg) → cg
 
-  deleteMin' leaf cg = cg record {tree = (node black 999 leaf 999 leaf) ; bool = false} -- unreachable case
+  deleteMin' leaf cg = cg record {tree = leaf ; bool = false} -- unreachable case
   deleteMin' (node black _ leaf x leaf) cg = cg record {tree = leaf ; bool = true}
   deleteMin' (node black _ leaf x r@(node red _ _ _ _)) cg = turnB r (λ tr → cg record {tree = tr ; bool = false})
   deleteMin' (node red _ leaf x r) cg = cg record {tree = r ; bool = false}
@@ -398,9 +405,9 @@
       delCheck : { n m : Level} {a : Set n} {cg : Set m} → RBTreeBDel ℕ → (RBTreeBDel ℕ → cg) → cg
       delCheck bt cg with (bool bt)
       delCheck record { tree = leaf ; bool = b } cg | false = cg record {tree = (node red 100 leaf 100 leaf) ; bool = b } -- unreachable case
-      delCheck record { tree = leaf ; bool = b } cg | true = unbalanceR c (h - 1) leaf x r (λ t → cg t)
-      delCheck record { tree = (node x₁ x₂ t₁ x₃ t₂) ; bool = b } cg | false = cg record {tree = (node x₁ x₂ t₁ x₃ t₂) ; bool = false}
-      delCheck record { tree = (node x₁ (x₂) t₁ x₃ t₂) ; bool = b } cg | true = unbalanceR c (h - 1) (node x₁ x₂ t₁ x₃ t₂) x r (λ t → cg t)
+      delCheck record { tree = leaf ; bool = b } cg | true = unbalanceR c (h - 1) leaf x r (λ result → cg result)
+      -- delCheck record { tree = (node x₁ x₂ t₁ x₃ t₂) ; bool = b } cg | false = cg record {tree = (node x₁ x₂ t₁ x₃ t₂) ; bool = false}
+      delCheck record { tree = (node x₁ x₂ t₁ x₃ t₂) ; bool = b } cg | _ = unbalanceR c (h - 1) (node x₁ x₂ t₁ x₃ t₂) x r (λ result → cg result)
 
 {--
 deleteMin では最後に帰ってきたやつを turnB
@@ -409,6 +416,7 @@
 rbtree が tree のとき deleteMin' tree
 ((s, _), _) は RBTreeBDel から RBTree への変換なので outPutTree
 --}
+
   deleteMin : RBTree ℕ → (RBTree ℕ → cg) → cg
   deleteMin leaf cg = cg leaf
   deleteMin tree cg = deleteMin' tree (λ dt → outPutTree {n} {m} {a} dt (λ dct → turnB dct (λ dctb → cg dctb)))
@@ -416,23 +424,12 @@
       outPutTree : { n m : Level} {a : Set n} {cg : Set m} → RBTreeBDel ℕ → (RBTree ℕ → cg) → cg
       outPutTree record { tree = s ; bool = b } cg = cg s
 
--- {--
---  1~7 のとき以降 delcheck の leaf case が出るので多分どこかの red の処理ミスってるっぽい
--- --}
-  cd1 = deleteMin (fromList (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ []))
-  cdd1 = fromList (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ [])
-  cd2 = deleteMin (fromList ( 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ []))
 
--- dd = deleteMin (fromList (1 ∷ 2 ∷ 3 ∷ []))
-
--- {--
---  black 2 ( black 1 leaf 2 leaf) 3 ( red 2 ( black 1 leaf 4 leaf) 5 ( black 1 leaf 6 ( red 1 leaf 7 leaf)))
--- --}
-
---  -- black 3 ( black 2 ( red 999 leaf 999 leaf) 2 ( red 1 leaf 3 leaf)) 4 ( red 2 ( black 1 leaf 5 leaf) 6 ( black 1 leaf 7 leaf))
-
-
--- --  black 2 ( black 1 leaf 2 ( red 1 leaf 3 leaf)) 4 ( red 2 ( black 1 leaf 5 leaf) 6( black 1 leaf 7 leaf))
+  -- > delCheck の node があって false のケースも unbalanceしなきゃいけなかった
+  d1 = deleteMin (fromList (3 ∷ 1 ∷ 2 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ []))
+  l1 = fromList (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ [])
+  l2 = fromList ( 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ [])
+  d2 = deleteMin (fromList ( 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ []))
 
 
 -- delete' : {a : Set} → ℕ → RBTree ℕ → RBTreeBDel ℕ