Mercurial > hg > Gears > GearsAgda

changeset 916:d3f55f139238

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, 03 Jun 2024 18:06:01 +0900
parents 045c98a3b8d1
children e5502b865a94
files hoareBinaryTree1.agda
diffstat 1 files changed, 22 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Jun 03 16:27:15 2024 +0900
+++ b/hoareBinaryTree1.agda	Mon Jun 03 18:06:01 2024 +0900
@@ -939,6 +939,7 @@
        → (rotated : replacedRBTree key value tree repl)
        → RBI-state key value tree repl stack  -- one stage up
    rotate  : {tree repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → color repl ≡ Red → black-depth repl ≡ black-depth tree
+       → ¬ (tree ≡ leaf) 
        → (rotated : replacedRBTree key value tree repl)
        → RBI-state key value tree repl stack  -- two stages up
    top-black : {tree repl : bt (Color ∧ A) } → {stack : List (bt (Color ∧ A))}  → stack ≡ tree ∷ []
@@ -948,7 +949,6 @@
 record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A)))  : Set n where
    field
        tree repl : bt (Color ∧ A)
-       ¬leaf : ¬ ( tree ≡ leaf )
        origti : treeInvariant orig
        origrb : RBtreeInvariant orig
        treerb : RBtreeInvariant tree     -- tree node te be replaced
@@ -1732,16 +1732,25 @@
  → stackInvariant key tree1 tree0 stack
  → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) 
  → (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 = ?
+replaceRBTNode key value orig rbi ti leaf stack si (case1 refl) exit = exit record {
+     tree = ?
+   ; repl = node key ⟪ Red , value ⟫ leaf leaf
    ; origti = ti
    ; origrb = rbi
    ; treerb = ?
    ; replrb = ?
+   ; si = ?
+   ; state = rotate ? ? ?  ?
+  }
+replaceRBTNode key value orig rbi ti tree@(node key₁ value₁ left right) stack si (case2 P) exit = exit record {
+     tree = tree
+   ; repl = node key₁ ⟪ proj1 value₁ , value ⟫ left right
+   ; origti = ti
+   ; origrb = rbi
+   ; treerb = PGtoRBinvariant1 tree orig rbi stack si
+   ; replrb = ?
    ; si = si
-   ; state = rotate ? ? ?  
+   ; state = rebuild ? ? ?
   }
 
 --
@@ -1801,7 +1810,6 @@
        rb07 (case2 cc ) = exit  (orig ∷ []) refl record {
          tree = orig
          ; repl = node key₁ value₁ repl right
-         ; ¬leaf = λ ()
          ; origti = RBI.origti r
          ; origrb = RBI.origrb r
          ; treerb = RBI.origrb r
@@ -1812,7 +1820,6 @@
        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
          ; treerb = RBI.origrb r
@@ -1852,7 +1859,6 @@
        rb07 (case2 cc ) = exit  (orig ∷ []) refl record {
          tree = orig
          ; repl = node key₁ value₁ left repl 
-         ; ¬leaf = λ ()
          ; origti = RBI.origti r
          ; origrb = RBI.origrb r
          ; treerb = RBI.origrb r
@@ -1863,7 +1869,6 @@
        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
          ; treerb = RBI.origrb r
@@ -1894,7 +1899,6 @@
        ... | 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
           ; treerb = treerb pg
@@ -1913,7 +1917,7 @@
            rb05 : treeInvariant (node kp vp n1 (RBI.tree r))
            rb05 = subst (λ k → treeInvariant k) x (rb08 pg)
            rb04 : kp < key
-           rb04 = si-property-> (RBI.¬leaf r) rb05 (subst (λ k → stackInvariant key (RBI.tree r) orig
+           rb04 = si-property-> ? rb05 (subst (λ k → stackInvariant key (RBI.tree r) orig
               (RBI.tree r ∷ k ∷ PG.grand pg ∷ PG.rest pg)) x (rb00 pg))
            rb06 : black-depth rb01 ≡ black-depth (PG.parent pg)
            rb06 = trans (rb07 vp) ( cong black-depth (sym x) ) where
@@ -1952,7 +1956,6 @@
         ... | 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
             ; treerb = rb02
@@ -1967,7 +1970,7 @@
             rb01 : bt (Color ∧ A)
             rb01 = to-black (node kp vp (node rkey vr rp-left rp-right) (to-red (node kg vg n1 (PG.uncle pg))))
             rb04 : key < kp
-            rb04 = si-property-< (RBI.¬leaf r) (subst (λ k → treeInvariant k) x rb08) (subst (λ k → stackInvariant key (RBI.tree r) orig
+            rb04 = si-property-< ? (subst (λ k → treeInvariant k) x rb08) (subst (λ k → stackInvariant key (RBI.tree r) orig
               (RBI.tree r ∷ k ∷ PG.grand pg ∷ PG.rest pg)) x (rb00))
             rb16 : color n1 ≡ Black
             rb16 = proj2 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) x rb09) (trans (cong color (sym x)) pcolor))
@@ -2027,7 +2030,7 @@
         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)
+    ... | rotate repl-red pdepth-eq ¬leaf rot with stackToPG (RBI.tree r) orig stack (RBI.si r)
     ... | 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
@@ -2044,7 +2047,6 @@
        ... | 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
             ; treerb = treerb pg
@@ -2056,7 +2058,7 @@
             rb01 : bt (Color ∧ A)
             rb01 = node kp vp repl n1
             rb03 : key < kp
-            rb03 = si-property-< (RBI.¬leaf r) (subst (λ k → treeInvariant k) x (rb08 pg)) (subst (λ k → stackInvariant key (RBI.tree r) orig
+            rb03 = si-property-< ¬leaf (subst (λ k → treeInvariant k) x (rb08 pg)) (subst (λ k → stackInvariant key (RBI.tree r) orig
               (RBI.tree r ∷ k ∷ PG.grand pg ∷ PG.rest pg)) x (rb00 pg))
             rb04 :  ⟪ Black , proj2 vp ⟫ ≡ vp
             rb04 with subst (λ k → color k ≡ Black) x pcolor
@@ -2085,18 +2087,17 @@
     ... | Red with PG.uncle pg in uneq
     ... | 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
+    ... | node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ with PG.pg pg   -- insertCase2 : uncle and parent are Red, flip color and go up by two level
     ... | 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
              ; treerb = rb01
              ; replrb = rb-red _ _ refl (RBtreeToBlackColor _ rb02) rb12 (rb-black _ _ rb13 (RBI.replrb r) rb04) (RBtreeToBlack _ rb02)
              ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
-             ; state = rotate refl rb17 (subst₂ (λ j k → replacedRBTree key value j k ) (sym rb09) refl  (rbr-flip-ll repl-red (rb05 refl uneq) rb06 rot))
+             ; state = rotate refl rb17 ? (subst₂ (λ j k → replacedRBTree key value j k ) (sym rb09) refl  (rbr-flip-ll repl-red (rb05 refl uneq) rb06 rot))
          }  rb15 where
            rb00 : stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
            rb00 = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r)
@@ -2115,7 +2116,7 @@
            rb07 : treeInvariant (node kp vp (RBI.tree r) n1)
            rb07 = subst (λ k → treeInvariant k) x (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00))
            rb06 : key < kp
-           rb06 = si-property-< (RBI.¬leaf r) rb07 (subst (λ k → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ k ∷ PG.grand pg ∷ PG.rest pg)) x rb00)
+           rb06 = si-property-< ¬leaf rb07 (subst (λ k → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ k ∷ PG.grand pg ∷ PG.rest pg)) x rb00)
            rb10 : vg ≡ ⟪ Black , proj2 vg ⟫
            rb10 with RBtreeParentColorBlack _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) (case1 pcolor)
            ... | refl = refl