Mercurial > hg > Gears > GearsAgda
changeset 815:e22ebb0f00a3
add replaceRBTNode
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 24 Jan 2024 10:36:44 +0900 |
| parents | 82029d2a8970 |
| children | a16f0b2ce509 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 101 insertions(+), 71 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Tue Jan 23 15:33:18 2024 +0900 +++ b/hoareBinaryTree1.agda Wed Jan 24 10:36:44 2024 +0900 @@ -805,6 +805,36 @@ ... | tri≈ ¬a b ¬c = rbi ... | tri> ¬a ¬b c = RBtreeRightDown _ _ rbi +-- +-- create RBT invariant after findRBT, continue to replaceRBT +-- +replaceRBTNode : {n m : Level} {A : Set n } {t : Set m } + → (key : ℕ) (value : A) + → (tree0 : bt (Color ∧ A)) + → RBtreeInvariant tree0 + → (tree1 : bt (Color ∧ A)) + → (stack : List (bt (Color ∧ A))) + → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack + → (exit : (r : RBI key value tree0 tree1 stack ) → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )) → t +replaceRBTNode = ? + +-- +-- RBT is blanced with the stack, simply rebuild tree without totation +-- +rebuildRBT : {n m : Level} {A : Set n} {t : Set m} + → (key : ℕ) → (value : A) + → (orig repl : bt (Color ∧ A)) + → (stack : List (bt (Color ∧ A))) + → (r : RBI key value orig repl stack ) + → black-depth repl ≡ black-depth (child-replaced key (RBI.tree r)) + → (next : (repl1 : (bt (Color ∧ A))) → (stack1 : List (bt (Color ∧ A))) + → (r : RBI key value orig repl1 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 +rebuildRBT = ? rotateLeft : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) @@ -903,7 +933,11 @@ → stack1 ≡ (orig ∷ []) → RBI key value orig repl stack1 → t ) → t -replaceRBP {n} {m} {A} {t} key value orig repl stack r next exit = insertCase1 where +replaceRBP {n} {m} {A} {t} key value orig repl stack r next exit with RBI.state r +... | rebuild bdepth-eq = rebuildRBT key value orig repl stack r bdepth-eq next exit +... | rotate repl-red pbdeth< with stackToPG (RBI.tree r) orig stack (RBI.si r) +... | case1 eq = exit repl stack eq r -- no stack, replace top node +... | case2 (case1 eq) = insertCase12 orig refl (RBI.si r) where insertCase2 : (tree parent uncle grand : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) → (pg : ParentGrand tree parent uncle grand ) → t @@ -936,76 +970,72 @@ -- tree is right of parent, parent is right of grand -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree -- 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 -- 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 - → stackInvariant key (RBI.tree r) orig stack - → t - insertCase12 leaf eq1 si = {!!} -- can't happen - insertCase12 tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁ - ... | tri< a ¬b ¬c = {!!} where - rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → left ≡ RBI.tree r - rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x s-nil) refl refl = refl - rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl with si-property1 si - ... | refl = ⊥-elim ( nat-<> x a ) - ... | tri≈ ¬a b ¬c = {!!} -- can't happen - ... | tri> ¬a ¬b c = 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 ( unbalanced ) - -- / \ 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 - ... | refl = ⊥-elim ( nat-<> x c ) - -- - -- RBI key value (node key₁ ⟪ Black , value₄ ⟫ left right) repl stack - -- - insertCase13 : (v : Color ∧ A ) → v ≡ value₁ → t - insertCase13 ⟪ Black , value₄ ⟫ refl = exit (node key₁ ⟪ Black , value₄ ⟫ left repl) (orig ∷ []) refl record { - tree = orig - ; origti = RBI.origti r - ; origrb = RBI.origrb r - ; treerb = RBI.origrb r - ; replrb = ? - ; si = s-nil - ; rotated = ? - ; ri = ? - ; state = ? - } where - rb09 : {n : Level} {A : Set n} → {key key1 key2 : ℕ} {value value1 : A} {t1 t2 : bt (Color ∧ A)} - → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key1 ⟪ Black , value1 ⟫ t1 t2)) - → key < key1 - rb09 (rb-right-red x x0 x2) = x - -- rb05 should more general - tkey : {n : Level} {A : Set n } → (rbt : bt (Color ∧ A)) → ℕ - tkey (node key value t t2) = key - tkey leaf = {!!} -- key is none - rb051 : {n : Level} {A : Set n} {key key1 : ℕ } {value : A} {t t1 t2 : bt (Color ∧ A)} {c : Color} → replacedTree key ⟪ ? , value ⟫ (node key1 ⟪ c , value ⟫ t1 t2) (node key1 ⟪ c , value ⟫ t1 t) → key1 < key - rb051 = {!!} - rb052 : {key key₁ : ℕ} → stackInvariant key (RBI.tree r) orig stack → key < key₁ - rb052 = {!!} - insertCase13 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r) - ... | Black = exit {!!} {!!} {!!} {!!} - ... | Red = exit {!!} {!!} {!!} {!!} - -- r = orig RBI.tree b - -- / \ => / \ - -- b b → r RBI.tree r r = orig o (r/b) - ... | case2 (case2 pg) = {!!} -- insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) + -- 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 + → stackInvariant key (RBI.tree r) orig stack + → t + insertCase12 leaf eq1 si = {!!} -- can't happen + insertCase12 tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁ + ... | tri< a ¬b ¬c = {!!} where + rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → left ≡ RBI.tree r + rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x s-nil) refl refl = refl + rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl with si-property1 si + ... | refl = ⊥-elim ( nat-<> x a ) + ... | tri≈ ¬a b ¬c = {!!} -- can't happen + ... | tri> ¬a ¬b c = 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 ( unbalanced ) + -- / \ 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 + ... | refl = ⊥-elim ( nat-<> x c ) + -- + -- RBI key value (node key₁ ⟪ Black , value₄ ⟫ left right) repl stack + -- + insertCase13 : (v : Color ∧ A ) → v ≡ value₁ → t + insertCase13 ⟪ Black , value₄ ⟫ refl = exit (node key₁ ⟪ Black , value₄ ⟫ left repl) (orig ∷ []) refl record { + tree = orig + ; origti = RBI.origti r + ; origrb = RBI.origrb r + ; treerb = RBI.origrb r + ; replrb = ? + ; si = s-nil + ; rotated = ? + ; ri = ? + ; state = ? + } where + rb09 : {n : Level} {A : Set n} → {key key1 key2 : ℕ} {value value1 : A} {t1 t2 : bt (Color ∧ A)} + → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key1 ⟪ Black , value1 ⟫ t1 t2)) + → key < key1 + rb09 (rb-right-red x x0 x2) = x + -- rb05 should more general + tkey : {n : Level} {A : Set n } → (rbt : bt (Color ∧ A)) → ℕ + tkey (node key value t t2) = key + tkey leaf = {!!} -- key is none + rb051 : {n : Level} {A : Set n} {key key1 : ℕ } {value : A} {t t1 t2 : bt (Color ∧ A)} {c : Color} → replacedTree key ⟪ ? , value ⟫ (node key1 ⟪ c , value ⟫ t1 t2) (node key1 ⟪ c , value ⟫ t1 t) → key1 < key + rb051 = {!!} + rb052 : {key key₁ : ℕ} → stackInvariant key (RBI.tree r) orig stack → key < key₁ + rb052 = {!!} + insertCase13 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r) + ... | Black = exit {!!} {!!} {!!} {!!} + ... | Red = exit {!!} {!!} {!!} {!!} + -- r = orig RBI.tree b + -- / \ => / \ + -- b b → r RBI.tree r r = orig o (r/b) +... | case2 (case2 pg) = {!!} -- insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)