# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1706347480 -32400
# Node ID ebee6945c697e222ada24ffa4baf26d6d96e4502
# Parent  3f6e13350420f1944ba2cb58f82f1441d79e8156
...

diff -r 3f6e13350420 -r ebee6945c697 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Fri Jan 26 08:54:44 2024 +0900
+++ b/hoareBinaryTree1.agda	Sat Jan 27 18:24:40 2024 +0900
@@ -517,7 +517,7 @@
                (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ record { tree0 = tree ; ti = P0 ; si = proj2 P ; ri = R ; ci = lift tt }
        $  λ p P1 loop → replaceP key value  (proj2 (proj2 p)) (proj1 p) P1
             (λ key value {tree1} repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1  ⟫ ⟫ P2 lt )
-       $ λ tree repl P → {!!} --exit tree repl ⟪ RTtoTI0 _ _ _ _ (proj1 P) (proj2 P) , proj2 P ⟫
+       $ λ tree repl P → exit tree repl {!!} --exit tree repl ⟪ RTtoTI0 _ _ _ _ (proj1 P) (proj2 P) , proj2 P ⟫
 
 insertTestP1 = insertTreeP leaf 1 1 t-leaf
   $ λ _ x0 P0 → insertTreeP x0 2 1 (proj1 P0)
@@ -867,9 +867,11 @@
 ... | tri≈ ¬a b ¬c = rbi
 ... | tri> ¬a ¬b c = RBtreeRightDown _ _ rbi
 
+-- this is too complacted to extend all arguments at once
+-- 
 RBTtoRBI  : {n : Level} {A : Set n}  → (tree repl : bt (Color ∧ A)) → (key : ℕ) → (value : A) → RBtreeInvariant tree
      → replacedRBTree key value tree repl → RBtreeInvariant repl
-RBTtoRBI  = ?
+RBTtoRBI {_} {A} tree repl key value rbi rlt = ?
 --
 -- create RBT invariant after findRBT, continue to replaceRBT
 --
@@ -901,99 +903,40 @@
         → t ) → t
 rebuildRBT = ?
 
-rotateLeft : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A)
-     → (orig tree : bt (Color ∧ A))
-     → (stack : List (bt (Color ∧ A)))
-     → (r : RBI key value orig tree stack )
-     → (pg : PG (Color ∧ A) tree stack)
-     → (next : (current : bt (Color ∧ A)) → (stack1 : List (bt (Color ∧ A)))
-        → (r : RBI key value orig current stack1 )
-        → length stack1 < length stack  → t )
-     → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
-        →  stack1 ≡ (orig ∷ [])
-        →  RBI key value orig repl stack1
-        → t ) → t
-rotateLeft {n} {m} {A} {t} key value = {!!} where
-    rotateLeft1 : t
-    rotateLeft1 with stackToPG {!!} {!!} {!!} {!!}
-    ... | case1 x = {!!} -- {!!} {!!} {!!} {!!} rr
-    ... | case2 (case1 x) = {!!}
-    ... | case2 (case2 pg) = {!!}
-
-rotateRight : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A)
-     → (orig tree : bt (Color ∧ A))
-     → (stack : List (bt (Color ∧ A)))
-     → (r : RBI key value orig tree stack )
-     → (pg : PG (Color ∧ A) tree stack)
-     → (next : (current : bt (Color ∧ A)) → (stack1 : List (bt (Color ∧ A)))
-        → (r : RBI key value orig current stack1 )
-        → length stack1 < length stack  → t )
-     → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
-        →  stack1 ≡ (orig ∷ [])
-        →  RBI key value orig repl stack1
-        → t ) → t
-rotateRight {n} {m} {A} {t} key value = {!!} where
-    rotateRight1 : t
-    rotateRight1 with stackToPG {!!} {!!} {!!} {!!}
-    ... | case1 x = {!!}
-    ... | case2 (case1 x) = {!!}
-    ... | case2 (case2 pg) = {!!}
-
-insertCase6 : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A)
-     → (orig tree : bt (Color ∧ A))
-     → (stack : List (bt (Color ∧ A)))
-     → (r : RBI key value orig tree stack )
-     → (pg : PG (Color ∧ A) tree stack)
-     → (next : (tree1 : (bt (Color ∧ A))) →  (stack1 : List (bt (Color ∧ A)))
-        → (r : RBI key value orig tree1 stack1 )
-        → length stack1 < length stack  → t )
-     → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
-        →  stack1 ≡ (orig ∷ [])
-        →  RBI key value orig repl stack1
-        → t ) → t
-insertCase6 {n} {m} {A} {t} key value = {!!} where
-    -- check inner repl case
-    --     node-key parent < node-key grand  → rotateRight grand 
-    --     node-key grand  < node-key parent → rotateLeft  grand 
-    insertCase61 : t
-    insertCase61 = ?
-
 insertCase5 : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A)
      → (orig tree : bt (Color ∧ A))
      → (stack : List (bt (Color ∧ A)))
      → (r : RBI key value orig tree stack )
      → (pg : PG (Color ∧ A) tree stack)
+     → color (PG.uncle pg) ≡ Black → color (PG.parent pg) ≡ Red
      → (next : (tree1 : (bt (Color ∧ A))) →  (stack1 : List (bt (Color ∧ A)))
         → (r : RBI key value orig tree1 stack1 )
-        → length stack1 < length stack  → t )
-     → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
-        →  stack1 ≡ (orig ∷ [])
-        →  RBI key value orig repl stack1
-        → t ) → t
-insertCase5 {n} {m} {A} {t} key value orig tree stack r pg next exit = {!!} where
+        → length stack1 < length stack  → t ) → t
+insertCase5 {n} {m} {A} {t} key value orig tree stack r pg cu=b cp=r next = {!!} where
     -- check inner repl case
     --     node-key parent < node-key repl < node-key grand  → rotateLeft  parent    then insertCase6
     --     node-key grand  < node-key repl < node-key parent → rotateRight parent    then insertCase6
     --     else insertCase6
     insertCase51 : (tree1 grand : bt (Color ∧ A)) → tree1 ≡ tree → grand ≡ PG.grand pg → t
     insertCase51 leaf grand teq geq = ?    -- can't happen
-    insertCase51 (node key value tree1 tree2) leaf teq geq = ?    -- can't happen
-    insertCase51 (node key value tree1 tree2) (node key₁ value₁ grand grand₁) teq geq with <-cmp key key₁
+    insertCase51 (node kr vr rleft rright) leaf teq geq = ?    -- can't happen
+    insertCase51 (node kr vr rleft rright) (node kg vg grand grand₁) teq geq with <-cmp kr kg
     ... | tri< a ¬b ¬c = ? where
           insertCase511 : (parent : bt (Color ∧ A)) → parent ≡ PG.parent pg → t
           insertCase511 leaf peq = ? -- can't happen
           insertCase511 (node key₂ ⟪ co , value ⟫ n1 n2) peq with <-cmp key key₂
-          ... | tri< a ¬b ¬c = insertCase6 key value orig ? stack ? pg ? ?
+          ... | tri< a ¬b ¬c = next ? ? ? ?
           ... | tri≈ ¬a b ¬c = ? -- can't happen
-          ... | tri> ¬a ¬b c = ? --- rotareRight → insertCase6 key value orig ? stack ? pg next exit
+          ... | tri> ¬a ¬b c = next ? ? ? ? --- rotareRight → insertCase6 key value orig ? stack ? pg next exit
     ... | tri≈ ¬a b ¬c = ? -- can't happen
-    ... | tri> ¬a ¬b c = ?
-
-
+    ... | tri> ¬a ¬b c = ? where
+          insertCase511 : (parent : bt (Color ∧ A)) → parent ≡ PG.parent pg → t
+          insertCase511 leaf peq = ? -- can't happen
+          insertCase511 (node key₂ ⟪ co , value ⟫ n1 n2) peq with <-cmp key key₂
+          ... | tri< a ¬b ¬c = next ? ? ? ? --- rotareLeft → insertCase6 key value orig ? stack ? pg next exit
+          ... | tri≈ ¬a b ¬c = ? -- can't happen
+          ... | tri> ¬a ¬b c = next ? ? ? ?
 
 --
 -- replaced node increase blackdepth, so we need tree rotate