--- a/RBTree.agda	Mon May 13 19:54:15 2019 +0900
+++ b/RBTree.agda	Tue May 14 02:35:21 2019 +0900
@@ -139,7 +139,6 @@
 
 
 module _ { n m : Level} {a : Set n} {cg : Set m} where
-
   -- _,_ : (tree : RBTree a) → (b : Bool) → Set
   -- leaf , false = (leaf , false)
   -- leaf , true = {!!}
@@ -202,16 +201,16 @@
   isRed (node red x₁ t x₂ t₁) = true
   isRed _ = false
 
-  isColorSame : Color → Color → Bool
-  isColorSame red red = true
-  isColorSame red black = false
-  isColorSame black red = false
-  isColorSame black black = true
+  isColorSame : Color → Color → (Bool → cg) → cg
+  isColorSame red red cg = cg true
+  isColorSame red black cg = cg false
+  isColorSame black red cg = cg false
+  isColorSame black black cg = cg true
 
-  root→ℕ : Maybe (RBTree a) → Maybe ℕ
-  root→ℕ (just leaf) = nothing
-  root→ℕ (just (node x x₁ x₂ x₃ x₄)) = just x₃
-  root→ℕ nothing = nothing
+  node→ℕ : Maybe (RBTree a) → Maybe ℕ
+  node→ℕ (just leaf) = nothing
+  node→ℕ (just (node x x₁ x₂ x₃ x₄)) = just x₃
+  node→ℕ nothing = nothing
 
 
 -- basic operations
@@ -220,6 +219,8 @@
 -- balance
 
 
+
+
 module _ { n m : Level} {a : Set n} {cg : Set m}  where
 
   balanceL' :  ℕ → RBTree a → ℕ → RBTree a → (RBTree a → cg) → cg
@@ -245,18 +246,18 @@
 -- unbalance
 
   -- unbalanceL' : Color → ℕ -> RBTree a -> a -> RBTree a -> (RBTreeBDel a → cg) → cg
-  -- unbalanceL' c h l@(node black _ _ _ _) x r cg = cg record { tree = ? ; bool = (isColorSame c black) }
+  -- unbalanceL' c h l@(node black _ _ _ _) x r cg = isColorSame c black ( λ issame → cg record { tree = {!!} ; bool = issame })
   -- unbalanceL' c h l x r cg = {!!}
 
-  -- unbalanceL : Color → ℕ → RBTree a → a → RBTree a → (RBTree a → cg) → cg
-  -- unbalanceL c h l@(node black _ _ _ _) x r  cg = cg (balanceL black h (turnR l) x r cg)
-  -- unbalanceL Black h l@(node red lh ll lx lr@(node black _ _ _ _)) x r  cg = cg (node black lh ll lx (balanceL black h (turnR lr) x r))
-  -- unbalanceL c h l x r  cg = cg leaf
+  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 c h l x r  cg = cg record {tree = leaf ; bool = false}
 
-  -- unbalanceR : Color → ℕ → RBTree ℕ → ℕ → RBTree ℕ → RBTreeBDel ℕ
-  -- unbalanceR c h l x r@(node black _ _ _ _)  = record {t = (balanceR black h l x (turnR r)) ; b = (checkColor c black)}
-  -- unbalanceR Black h l x (node R rh rl@(node black _ _ _ _) rx rr) = record { t = (node black rh (balanceR black h l x (turnR rl)) rx rr); b = false}
-  -- unbalanceR c h l x r  = record {t = leaf ; b = 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 c h l x r cg  = cg record {tree = leaf ; bool = false}
 
 
 
@@ -326,11 +327,8 @@
 
 cget = get 6 c1 (λ a → a)
 
-hoge = rootChildFix (node black 3 (node black 2 (node black 1 leaf 1 leaf) 2 (node black 1 (node red 1 leaf 3 leaf) 4 leaf)) 5 (node black 2 (node black 1 leaf 6 leaf) 7 (node black 1 leaf 8 leaf))) (λ t → t)
 
-fuga = rootChildFix c3
-
-proof-leaf : {l : Level} {D : Set l} (n : ℕ) → insert {_} {_} {ℕ} {Set} n leaf (λ t1 → get n t1 (λ n1 → (just n ≡ (root→ℕ {_} {_} {ℕ} {ℕ} n1))))
+proof-leaf : {l : Level} {D : Set l} (n : ℕ) → insert {_} {_} {ℕ} {Set} n leaf (λ t1 → get n t1 (λ n1 → (just n ≡ (node→ℕ {_} {_} {ℕ} {ℕ} n1))))
 proof-leaf n with n Data.Nat.≟ n | compareTri n n
 proof-leaf n | yes p | tri< a ¬b ¬c = ⊥-elim (¬b p)
 proof-leaf n | yes p | tri≈ ¬a b ¬c = refl
@@ -368,36 +366,62 @@
 rb 含めると、色関係、枝の長さ、になりそう?
 --}
 
+module _ { n m : Level} {a : Set n} {cg : Set m}  where
 
--- {-# TERMINATING #-}
--- deleteMin' : RBTree ℕ → RBTreeBDel ℕ
--- deleteMin' leaf  = record {t = (node black 999 leaf 999 leaf) ; b = false} -- unreachable case
--- deleteMin' (node black _ leaf x leaf) = record {t = leaf ; b = true}
--- deleteMin' (node black _ leaf x r@(node red _ _ _ _))  = record {t = (turnB {ℕ} r) ; b = false}
--- deleteMin' (node red _ leaf x r)  = record {t = r ; b = false}
--- deleteMin' (node c h l x r) = (delCheck (deleteMin' l))
---   where
---     delCheck : RBTreeBDel ℕ → RBTreeBDel ℕ
---     delCheck bt with (b bt)
---     delCheck record { t = leaf ; b = b } | false = record {t = (node red 100 leaf 100 leaf) ; b = b } -- unreachable case
---     delCheck record { t = leaf ; b = b } | true = unbalanceR {ℕ} c (h - 1) leaf x r
---     delCheck record { t = (node x₁ x₂ t₁ x₃ t₂) ; b = b } | false = deleteMin' (node x₁ x₂ t₁ x₃ t₂)
---     delCheck record { t = (node x₁ (x₂) t₁ x₃ t₂) ; b = b } | true = unbalanceR {ℕ} c (h - 1) (node x₁ x₂ t₁ x₃ t₂) x r
+{--
+deleteMin' は後ろに bool(Color の変更情報?)を持ちながら再帰する
+再帰に一つ関数が挟まってるけど互いに呼んでるからどう書くべきかわからん
+
+```Haskell Source
+deleteMin' (Node c h l x r)               = if d then (tD, m) else (tD', m)
+
+((l', d), m) = deleteMin' l
+tD  = unbalancedR c (h-1) l' x r
+tD' = (Node c h l' x r, False)
+```
+
+たぶん ((l', d), m) の形になると deleteMin' がしたい
+RBTreeBDel の bool 情報はleaf に着いたかどうかだけ
+ん、node の左に leaf がついてる最小パターン探せばいいのでは？
+
+--}
+
+  {-# TERMINATING #-}
+  deleteMin' : RBTree ℕ → (RBTreeBDel ℕ → cg) → cg
 
--- deleteMin : RBTree ℕ → RBTree ℕ
--- deleteMin leaf = empty
--- deleteMin t = turnB {ℕ} (outPutTree (deleteMin' t))
---   where
---     outPutTree : RBTreeBDel ℕ → RBTree ℕ
---     outPutTree record { t = s ; b = b } = s
+  deleteMin' leaf cg = cg record {tree = (node black 999 leaf 999 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}
+  deleteMin' (node c h l x r) cg = deleteMin' l (λ dt → delCheck {n} {m} {a} dt (λ dct → cg dct))
+    where
+      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)
 
+{--
+deleteMin では最後に帰ってきたやつを turnB
+型は rbtree → (rbtree → cg) → cg
+
+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)))
+    where
+      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 の処理ミスってるっぽい
 -- --}
--- cd = deleteMin (fromList ( 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ []))
-
--- cdc = fromList ( 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ [])
+  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 ∷ []))