Mercurial > hg > Gears > GearsAgda

changeset 821:aeb14a056896

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 Fri, 26 Jan 2024 04:55:57 +0900
parents 317539bdba03
children 3f6e13350420
files hoareBinaryTree1.agda
diffstat 1 files changed, 52 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Thu Jan 25 20:37:25 2024 +0900
+++ b/hoareBinaryTree1.agda	Fri Jan 26 04:55:57 2024 +0900
@@ -727,12 +727,54 @@
 -- create replaceRBTree with rotate
 
 data replacedRBTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt (Color ∧ A) ) → Set n where
-    rbr-leaf : {ca cb : Color} → replacedRBTree key value leaf (node key ⟪ cb , value ⟫ leaf leaf)
-    rbr-node : {value₁ : A} → {ca cb : Color } → {t t₁ : bt (Color ∧ A)} → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ cb , value ⟫ t t₁)
-    rbr-right : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
-          → k < key →  replacedRBTree key value t2 t →  replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t1 t)
-    rbr-left : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
-          → key < k →  replacedRBTree key value t1 t →  replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t t2) -- k < key → key < k 
+    rbr-leaf : replacedRBTree key value leaf (node key ⟪ Red , value ⟫ leaf leaf)
+    rbr-node : {value₁ : A} → {ca : Color } → {t t₁ : bt (Color ∧ A)} → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ ca , value ⟫ t t₁)
+    rbr-right : {k : ℕ } {v1 : A} → {ca : Color} → {t t1 t2 : bt (Color ∧ A)}
+          → k < key →  replacedRBTree key value t2 t →  replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ ca , v1 ⟫ t1 t)
+    rbr-left  : {k : ℕ } {v1 : A} → {ca : Color} → {t t1 t2 : bt (Color ∧ A)}
+          → key < k →  replacedRBTree key value t1 t →  replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ ca , v1 ⟫ t t2) -- k < key → key < k 
+
+    rbr-black-right : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ}
+         → color t₂ ≡ Red → replacedRBTree key value t₁ t₂
+         → replacedRBTree key value (node key₁ ⟪ Black , value₁ ⟫ t t₁) (node key₁ ⟪ Black , value₁ ⟫ t t₂)
+    rbr-black-left : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ}
+         → color t₂ ≡ Red → replacedRBTree key value t₁ t₂
+         → replacedRBTree key value (node key₁ ⟪ Black , value₁ ⟫ t₁ t) (node key₁ ⟪ Black , value₁ ⟫ t₂ t)
+
+    rbr-flip-ll : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
+         → color t₂ ≡ Red → replacedRBTree key value t₁ t₂
+         → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red   , vp ⟫ t₁ t)           uncle) 
+                                    (node kg ⟪ Red ,   vg ⟫ (node kp ⟪ Black , vp ⟫ t₂ t) (to-black uncle))
+    rbr-flip-lr : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
+         → color t₂ ≡ Red → replacedRBTree key value t₁ t₂
+         → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red   , vp ⟫ t t₁)           uncle) 
+                                    (node kg ⟪ Red ,   vg ⟫ (node kp ⟪ Black , vp ⟫ t t₂) (to-black uncle))
+    rbr-flip-rl : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
+         → color t₂ ≡ Red → replacedRBTree key value t₁ t₂
+         → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle            (node kp ⟪ Red   , vp ⟫ t₁ t))  
+                                    (node kg ⟪ Red ,   vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t₂ t))
+    rbr-flip-rr : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
+         → color t₂ ≡ Red → replacedRBTree key value t₁ t₂
+         → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle            (node kp ⟪ Red   , vp ⟫ t t₁))  
+                                    (node kg ⟪ Red ,   vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t t₂))
+
+    rbr-rotate-ll : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}   - case6
+         → color t₂ ≡ Red → replacedRBTree key value t₁ t₂
+         → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t)    uncle) 
+                                    (node kp ⟪ Black , vp ⟫ t₂                            (node kg ⟪ Red , vg ⟫ t uncle))
+    rbr-rotate-rr : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}   - case6
+         → color t₂ ≡ Red → replacedRBTree key value t₁ t₂
+         → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle                          (node kp ⟪ Red   , vp ⟫ t t₁)) 
+                                    (node kp ⟪ Black , vp ⟫ (node kg ⟪ Red , vg ⟫ uncle t) t₂ )
+    rbr-rotate-lr : {t t₁ t₂ t₃ uncle : bt (Color ∧ A)} {kg kp kn : ℕ} {vg vp vn : A}   - case56
+         → replacedRBTree key value t (node kn ⟪ Red , vn ⟫ t₁ t₂)
+         → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₃ t)  uncle) 
+                                    (node kn ⟪ Black , vn ⟫ (node kp ⟪ Red , vp ⟫ t₃ t₁) (node kg ⟪ Red , vg ⟫ t₂ uncle))
+    rbr-rotate-rl : {t t₁ t₂ t₃ uncle : bt (Color ∧ A)} {kg kp kn : ℕ} {vg vp vn : A    - case56
+         → replacedRBTree key value t (node kn ⟪ Red , vn ⟫ t₁ t₂)
+         → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle                           (node kp ⟪ Red , vp ⟫ t  t₃)) 
+                                    (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , vg ⟫ t₁ uncle) (node kp ⟪ Red , vp ⟫ t₂ t₃)) 
+
 
 data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent uncle grand : bt A) → Set n where
     s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
@@ -757,8 +799,10 @@
 --
 
 data RBI-state  {n : Level} {A : Set n} (key : ℕ) : (tree repl : bt (Color ∧ A) ) → Set n where
-   rebuild : {tree repl : bt (Color ∧ A) } → black-depth repl ≡ black-depth (child-replaced key tree) → RBI-state key tree repl
-   rotate  : {tree repl : bt (Color ∧ A) } → color repl ≡ Red → black-depth repl ≡ black-depth (child-replaced key tree) → RBI-state key tree repl
+   rebuild : {tree repl : bt (Color ∧ A) } → black-depth repl ≡ black-depth (child-replaced key tree) 
+       → RBI-state key tree repl   -- one stage up
+   rotate  : {tree repl : bt (Color ∧ A) } → color repl ≡ Red → black-depth repl ≡ black-depth (child-replaced key tree) 
+       → RBI-state key tree repl   -- two stages up
 
 record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A)))  : Set n where
    field