Mercurial > hg > Gears > GearsAgda

changeset 915:045c98a3b8d1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
repl in RBI field
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 03 Jun 2024 16:27:15 +0900
parents e87dca1b4c21
children d3f55f139238
files hoareBinaryTree1.agda
diffstat 1 files changed, 31 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Jun 03 15:42:43 2024 +0900
+++ b/hoareBinaryTree1.agda	Mon Jun 03 16:27:15 2024 +0900
@@ -945,9 +945,9 @@
        → (rotated : replacedRBTree key value tree repl ∨ replacedRBTree key value (to-black tree) repl)
        → RBI-state key value tree repl stack
 
-record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A)))  : Set n where
+record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A)))  : Set n where
    field
-       tree : bt (Color ∧ A)
+       tree repl : bt (Color ∧ A)
        ¬leaf : ¬ ( tree ≡ leaf )
        origti : treeInvariant orig
        origrb : RBtreeInvariant orig
@@ -1731,9 +1731,10 @@
  → (stack : List (bt (Color ∧ A)))
  → stackInvariant key tree1 tree0 stack
  → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) 
- → (exit : (r : RBI key value tree0 tree1 stack ) → t ) → t
+ → (exit : (r : RBI key value tree0 stack ) → t ) → t
 replaceRBTNode key value orig rbi ti tree stack si P exit = exit record {
      tree = tree
+   ; repl = ?
    ; ¬leaf = ?
    ; origti = ti
    ; origrb = rbi
@@ -1748,21 +1749,22 @@
 --
 replaceRBP : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A)
-     → (orig repl : bt (Color ∧ A))
+     → (orig : bt (Color ∧ A))
      → (stack : List (bt (Color ∧ A)))
-     → (r : RBI key value orig repl stack )
-     → (next : (repl1 : (bt (Color ∧ A))) →  (stack1 : List (bt (Color ∧ A)))
-        → (r : RBI key value orig repl1 stack1 )
+     → (r : RBI key value orig stack )
+     → (next :  (stack1 : List (bt (Color ∧ A)))
+        → (r : RBI key value orig stack1 )
         → length stack1 < length stack  → t )
-     → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
+     → (exit : (stack1 : List (bt (Color ∧ A)))
         →  stack1 ≡ (orig ∷ [])
-        →  RBI key value orig repl stack1
+        →  RBI key value orig stack1
         → t ) → t
-replaceRBP {n} {m} {A} {t} key value orig repl stack r next exit = replaceRBP1 where
+replaceRBP {n} {m} {A} {t} key value orig stack r next exit = replaceRBP1 where
     -- we have no grand parent
     -- eq : stack₁ ≡ RBI.tree r ∷ orig ∷ []
     -- change parent color ≡ Black and exit
     -- one level stack, orig is parent of repl
+    repl = RBI.repl r
     insertCase4 :  (tr0 : bt (Color ∧ A)) → tr0 ≡ orig
        → (eq : stack ≡ RBI.tree r ∷ orig ∷ [])
        → (rot : replacedRBTree key value (RBI.tree r) repl)
@@ -1796,8 +1798,9 @@
        ... | Black = subst (λ k → RBtreeInvariant (node key₁ k repl right)) (cong (λ k → ⟪ k , _ ⟫) (sym coeq) )
            (rb-black _ (proj2 value₁) rb06 (RBI.replrb r) (RBtreeRightDown _ _ (RBI.origrb r)))
        rb07 : ( color repl ≡ Red ) ∨ (color (RBI.tree r) ≡ color repl) → t
-       rb07 (case2 cc ) = exit (node key₁ value₁ repl right) (orig ∷ []) refl record {
+       rb07 (case2 cc ) = exit  (orig ∷ []) refl record {
          tree = orig
+         ; repl = node key₁ value₁ repl right
          ; ¬leaf = λ ()
          ; origti = RBI.origti r
          ; origrb = RBI.origrb r
@@ -1806,8 +1809,9 @@
          ; si = s-nil
          ; state = top-black  refl (case1 (rbr-left (trans (cong color (rb04 si eq refl)) cc) a (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot)))
          }
-       rb07 (case1 repl-red) = exit (to-black (node key₁ value₁ repl right)) (orig ∷ []) refl record {
+       rb07 (case1 repl-red) = exit  (orig ∷ []) refl record {
          tree = orig
+         ; repl = to-black (node key₁ value₁ repl right)
          ; ¬leaf = λ ()
          ; origti = RBI.origti r
          ; origrb = RBI.origrb r
@@ -1845,8 +1849,9 @@
        ... | Black = subst (λ k → RBtreeInvariant (node key₁ k left repl )) (cong (λ k → ⟪ k , _ ⟫) (sym coeq) )
            (rb-black _ (proj2 value₁) (sym rb06)  (RBtreeLeftDown _ _ (RBI.origrb r)) (RBI.replrb r))
        rb07 : ( color repl ≡ Red ) ∨ (color (RBI.tree r) ≡ color repl) → t
-       rb07 (case2 cc ) = exit (node key₁ value₁ left repl ) (orig ∷ []) refl record {
+       rb07 (case2 cc ) = exit  (orig ∷ []) refl record {
          tree = orig
+         ; repl = node key₁ value₁ left repl 
          ; ¬leaf = λ ()
          ; origti = RBI.origti r
          ; origrb = RBI.origrb r
@@ -1855,8 +1860,9 @@
          ; si = s-nil
          ; state = top-black  refl (case1 (rbr-right (trans (cong color (rb04 si eq refl)) cc) c (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot)))
          }
-       rb07 (case1 repl-red ) = exit (to-black (node key₁ value₁ left repl)) (orig ∷ [])  refl record {
+       rb07 (case1 repl-red ) = exit  (orig ∷ [])  refl record {
          tree = orig
+         ; repl = to-black (node key₁ value₁ left repl)
          ; ¬leaf = λ ()
          ; origti = RBI.origti r
          ; origrb = RBI.origrb r
@@ -1869,7 +1875,7 @@
        → (bdepth-eq : black-depth repl ≡ black-depth (RBI.tree r))
        → (rot       : replacedRBTree key value (RBI.tree r) repl ) → t
     rebuildCase ceq bdepth-eq rot with stackToPG (RBI.tree r) orig stack (RBI.si r)
-    ... | case1 x = exit repl stack x r  where  -- single node case
+    ... | case1 x = exit stack x r  where  -- single node case
         rb00 : stack ≡ orig ∷ [] → orig ≡ RBI.tree r
         rb00 refl = si-property1 (RBI.si r)
     ... | case2 (case1 x) = insertCase4 orig refl x rot (case2 ceq) (RBI.si r)   -- one level stack, orig is parent of repl
@@ -1885,8 +1891,9 @@
        ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ?
        ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ?
        ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ?
-       ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = next rb01 (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
+       ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
           tree = PG.parent pg
+          ; repl = rb01
           ; ¬leaf = subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())
           ; origti = RBI.origti r
           ; origrb = RBI.origrb r
@@ -1942,8 +1949,9 @@
 
         insertCase51 : t
         insertCase51 with PG.pg pg
-        ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = next rb01 (PG.grand pg ∷ PG.rest pg) record {
+        ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = next (PG.grand pg ∷ PG.rest pg) record {
             tree = PG.grand pg
+            ; repl = rb01
             ; ¬leaf = subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())
             ; origti = RBI.origti r
             ; origrb = RBI.origrb r
@@ -2015,12 +2023,12 @@
     replaceRBP1 : t
     replaceRBP1 with RBI.state r
     ... | rebuild ceq bdepth-eq rot = rebuildCase ceq bdepth-eq rot
-    ... | top-black eq rot = exit repl stack (trans eq (cong (λ k → k ∷ []) rb00)) r where
+    ... | top-black eq rot = exit stack (trans eq (cong (λ k → k ∷ []) rb00)) r where
         rb00 : RBI.tree r ≡ orig
         rb00 with si-property-last _ _ _ _ (subst (λ k → stackInvariant key (RBI.tree r) orig k) (eq) (RBI.si r))
         ... | refl = refl
     ... | rotate repl-red pdepth-eq rot with stackToPG (RBI.tree r) orig stack (RBI.si r)
-    ... | case1 eq  = exit repl stack eq r     -- no stack, replace top node
+    ... | case1 eq  = exit stack eq r     -- no stack, replace top node
     ... | case2 (case1 eq) = insertCase4 orig refl eq rot (case1 repl-red) (RBI.si r)     -- one level stack, orig is parent of repl
     ... | case2 (case2 pg) with color (PG.parent pg) in pcolor
     ... | Black = insertCase1 where
@@ -2033,8 +2041,9 @@
        rb08 pg = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (rb00 pg))
        insertCase1 : t
        insertCase1 with PG.pg pg
-       ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = next rb01 (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
+       ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
             tree = PG.parent pg
+            ; repl = rb01
             ; ¬leaf = subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())
             ; origti = RBI.origti r
             ; origrb = RBI.origrb r
@@ -2077,9 +2086,10 @@
     ... | leaf = insertCase5 repl refl pg rot repl-red (cong color uneq) pcolor
     ... | node key₁ ⟪ Black , value₁ ⟫ t₁ t₂ = insertCase5 repl refl pg rot repl-red (cong color uneq) pcolor
     ... | node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ with PG.pg pg   -- inswertCse2 : uncle and parent are Red, flip color and go up by two level
-    ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = next (to-red (node kg vg (to-black (node kp vp repl n1)) (to-black (PG.uncle pg)))) (PG.grand pg ∷ (PG.rest pg))
+    ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = next  (PG.grand pg ∷ (PG.rest pg))
         record {
              tree = PG.grand pg
+             ; repl = to-red (node kg vg (to-black (node kp vp repl n1)) (to-black (PG.uncle pg)))
              ; ¬leaf = subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())
              ; origti = RBI.origti r
              ; origrb = RBI.origrb r