Mercurial > hg > Gears > GearsAgda

changeset 906:a1b7703f8551

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, 31 May 2024 17:23:46 +0900
parents acee838690c9
children fb6644858d1a 15a47dd48d8e
files hoareBinaryTree1.agda
diffstat 1 files changed, 15 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Fri May 31 14:41:59 2024 +0900
+++ b/hoareBinaryTree1.agda	Fri May 31 17:23:46 2024 +0900
@@ -183,6 +183,13 @@
 si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ _ _ _ si ) with  si-property1  si
 ... | refl = si-property-last key x t0 (x ∷ st)   si
 
+si-property-not-orig-leaf : {n : Level} {A : Set} {stack : List ( bt A)} {tree orig : bt A} {key : ℕ} → stackInvariant key tree orig stack → ¬ ( orig ≡ leaf )
+si-property-not-orig-leaf {n} {A} {stack} {tree} {orig} {key} (s-nil ) = ?
+si-property-not-orig-leaf {n} {A} {stack} {tree} {orig} {key} (s-right _ _ _ _ si) = ?
+si-property-not-orig-leaf {n} {A} {stack} {tree} {orig} {key} (s-left _ _ _ _ si) = ?
+
+--       rb04  refl refl (s-right tree leaf tree₁ x si) = si-property2 _ (s-right tree leaf tree₁ x si) refl
+--       rb04  refl refl (s-left tree₁ leaf tree x si) = si-property2 _  (s-left tree₁ leaf tree x si) refl
 
 -- Diffkey : {n : Level} (A : Set n) (tree0 : bt A) → (key : ℕ) →  (tree : bt A) → (stack  : List (bt A)) → (si : stackInvariant key tree tree0 stack) → Set
 -- Diffkey A leaf key .leaf .(leaf ∷ []) s-nil = ?
@@ -930,7 +937,7 @@
 --
 
 data RBI-state  {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree repl : bt (Color ∧ A) ) → (stak : List (bt (Color ∧ A))) → Set n where
-   rebuild : {tree repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → black-depth repl ≡ black-depth (child-replaced key tree)
+   rebuild : {tree repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → black-depth repl ≡ black-depth tree
        → (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
@@ -1732,24 +1739,6 @@
  → (exit : (r : RBI key value tree0 tree1 stack ) → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )) → t
 replaceRBTNode key value tree0 rbi tree1 stack rbi-stack exit = {!!}
 
---
--- RBT is blanced with the stack, simply rebuild tree without rototation
---
-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 key value orig repl stack r bdepth-eq next exit = {!!}
-
 insertCase5 : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A)
      → (orig tree : bt (Color ∧ A))
@@ -1818,7 +1807,9 @@
         →  RBI key value orig repl stack1
         → t ) → t
 replaceRBP {n} {m} {A} {t} key value orig repl stack r next exit with RBI.state r
-... | rebuild bdepth-eq rot = rebuildRBT key value orig repl stack r bdepth-eq next exit
+... | rebuild bdepth-eq rot = ? where   --  rebuildRBT key value orig repl stack r bdepth-eq next exit
+    rebuildCase : (tr0 : bt (Color ∧ A)) → tr0 ≡ orig → stackInvariant key (RBI.tree r) orig stack → t
+    rebuildCase tr0 eq1 si = ?
 ... | top-black eq rot = {!!}
 ... | rotate repl-red pdepth< rot with stackToPG (RBI.tree r) orig stack (RBI.si r)
 ... | case1 eq  = exit repl stack eq r     -- no stack, replace top node
@@ -1841,7 +1832,7 @@
     insertCase12  tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁ | child-replaced key (node key₁ value₁ left right) in creq
     ... | tri< a ¬b ¬c | cr = exit (to-black (node key₁ value₁ repl right)) (orig ∷ []) refl record {
          tree = orig
-         ; ¬leaf = ?
+         ; ¬leaf = λ ()
          ; origti = RBI.origti r
          ; origrb = RBI.origrb r
          ; treerb = RBI.origrb r
@@ -1874,7 +1865,7 @@
        rb06 (.left ∷ node key₁ value₁ left right ∷ []) refl (s-left .left .(node key₁ value₁ left right) .right x s-nil) eq = ⊥-elim ( nat-≡< eq x)
     ... | tri> ¬a ¬b c | cr = exit (to-black (node key₁ value₁ left repl)) (orig ∷ [])  refl record {
          tree = orig
-         ; ¬leaf = ?
+         ; ¬leaf = λ ()
          ; origti = RBI.origti r
          ; origrb = RBI.origrb r
          ; treerb = RBI.origrb r
@@ -1899,11 +1890,11 @@
          black-depth left ∎
             where open ≡-Reasoning  
 ... | case2 (case2 pg) with color (PG.parent pg) in pcolor
-... | Black = ?  -- insertCase1 -- parent is Black 
+... | Black = ? -- rebuildRBT key value orig ? ? ? ? next exit where   -- insertCase1 -- parent is Black 
 ... | Red with PG.uncle pg in uneq
 ... | leaf = {!!} -- insertCase5
 ... | node key₁ ⟪ Black , value₁ ⟫ t₁ t₂ = {!!} -- insertCase5
-... | node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ with PG.pg pg
+... | node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ with PG.pg pg   -- 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))
     record {
          tree = PG.grand pg