Mercurial > hg > Gears > GearsAgda

changeset 794:2a07b50f4bc0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 23 Oct 2023 19:29:43 +0900
parents 08e04ed15468
children e9ba6a5bc64b
files hoareBinaryTree1.agda
diffstat 1 files changed, 20 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sat Oct 21 18:51:25 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Oct 23 19:29:43 2023 +0900
@@ -692,11 +692,13 @@
        tree rot : bt (Color ∧ A)
        origti : treeInvariant orig
        origrb : RBtreeInvariant orig
-       treerb : RBtreeInvariant tree
+       treerb : RBtreeInvariant tree     -- tree node te be replaced
        replrb : RBtreeInvariant repl
        si : stackInvariant key tree orig stack
        rotated : rotatedTree tree rot
        ri : replacedRBTree key value (child-replaced key rot ) repl
+       repl-red : color repl ≡ Red
+       repl-eq : black-depth (child-replaced key rot ) ≡ black-depth repl
 
 --   r (b , b)    inserting a node into black node does not change the black depth, but color may change
 --       → b (b , r ) ∨ b (r , b)
@@ -935,8 +937,9 @@
       -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
     insertCase1 : t
     insertCase1 with stackToPG (RBI.tree r) orig stack (RBI.si r)
-    ... | case1 eq  = exit repl stack eq r
+    ... | case1 eq  = exit repl stack eq r     -- no stack, replace top node
     ... | case2 (case1 eq) = insertCase12 orig refl (RBI.si r)  where
+        -- one level stack, orig is parent of repl
         rb01 : stackInvariant key (RBI.tree r) orig stack
         rb01 = RBI.si r
         insertCase12 :  (tr0 : bt (Color ∧ A)) → tr0 ≡ orig
@@ -947,6 +950,19 @@
         ... | tri< a ¬b ¬c | cr = ?
         ... | tri≈ ¬a b ¬c | cr = ? -- can't happen
         ... | tri> ¬a ¬b c | cr = insertCase13 value₁ refl where
+           --
+           --    orig B
+           --    /  \
+           -- left   tree → rot → repl R
+           --
+           --     B  =>   B             B      =>         B
+           --    / \     / \           / \    rotate L   / \
+           --   L   L1  L   R3        L   R  -- bad     B   B
+           --              / \           / \               / \      1 : child-replace
+           ---            L   L2        L   B             L   L     2:  child-replace ( unbrance )
+           --                              / \                      3:  child-replace ( rotated / balanced )
+           --                             L   L  
+           -- 
            rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → right ≡ RBI.tree r
            rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl = refl
            rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x si) refl refl with si-property1 si
@@ -962,6 +978,8 @@
              ; rotated = subst (λ k → rotatedTree k (node key₁ value₁ left (RBI.rot r))) (
                 trans (cong (λ k → node key₁ value₁ left k) (sym (rb04 si eq refl))) refl) (rtt-node rtt-unit (RBI.rotated r))
              ; ri = proj2 rb05
+             ; repl-red = ?
+             ; repl-eq = ?
              } where
                rb05 : RBtreeInvariant (node key₁ value₁ left repl) ∧  replacedRBTree key value
                     (child-replaced key (node key₁ value₁ left (RBI.rot r))) (node key₁ value₁ left repl)