Mercurial > hg > Gears > GearsAgda

changeset 923:62393055b0dd

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, 07 Jun 2024 17:18:41 +0900
parents 5fb90d662aa4
children 69aab3105ac4
files hoareBinaryTree1.agda
diffstat 1 files changed, 85 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Thu Jun 06 17:53:41 2024 +0900
+++ b/hoareBinaryTree1.agda	Fri Jun 07 17:18:41 2024 +0900
@@ -39,6 +39,9 @@
 bt-depth leaf = 0
 bt-depth (node key value t t₁) = suc (bt-depth t  ⊔ bt-depth t₁ )
 
+bt-ne : {n : Level} {A : Set n} {key : ℕ} {value : A} {t t₁ : bt A} → ¬ ( leaf ≡ node key value t t₁ )
+bt-ne {n} {A} {key} {value} {t} {t₁} () 
+
 open import Data.Unit hiding ( _≟_ ) -- ;  _≤?_ ; _≤_)
 
 tr< : {n : Level} {A : Set n} → (key : ℕ) → bt A → Set
@@ -183,8 +186,8 @@
 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-pne :  {n : Level} {A : Set n}  {key key₁ : ℕ} {value₁ : A} (tree orig : bt A) → {left right : bt A} → (stack  : List (bt A)) {rest : List (bt A)}
-    → stack ≡ tree ∷ node key₁ value₁ left right ∷ rest
+si-property-pne :  {n : Level} {A : Set n}  {key key₁ : ℕ} {value₁ : A} (tree orig : bt A) → {left right x : bt A} → (stack  : List (bt A)) {rest : List (bt A)}
+    → stack ≡ x ∷ node key₁ value₁ left right ∷ rest
     → stackInvariant key tree orig stack
     → ¬ ( key ≡ key₁ )
 si-property-pne tree orig .(tree ∷ node _ _ _ _ ∷ _) refl (s-right .tree .orig tree₁ x si) eq with si-property1 si
@@ -192,6 +195,15 @@
 si-property-pne tree orig .(tree ∷ node _ _ _ _ ∷ _) refl (s-left .tree .orig tree₁ x si) eq with si-property1 si
 ... | refl = ⊥-elim ( nat-≡< eq x)
 
+si-property-parent-node :  {n : Level} {A : Set n}  {key : ℕ}  (tree orig : bt A) {x : bt A}
+    → (stack  : List (bt A)) {rest : List (bt A)}
+    → stackInvariant key tree orig stack
+    → ¬ ( stack ≡ x ∷ leaf ∷ rest )
+si-property-parent-node {n} {A} tree orig .(tree ∷ leaf ∷ _) (s-right .tree .orig tree₁ x si) refl with si-property1 si
+... | ()
+si-property-parent-node {n} {A} tree orig .(tree ∷ leaf ∷ _) (s-left .tree .orig tree₁ x si) refl with si-property1 si
+... | ()
+
 
 rt-property1 :  {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf )
 rt-property1 {n} {A} key value .leaf .(node key value leaf leaf) r-leaf ()
@@ -1720,7 +1732,7 @@
 --
 -- create RBT invariant after findRBT, continue to replaceRBT
 --
-replaceRBTNode : {n m : Level} {A : Set n } {t : Set m }
+createRBT : {n m : Level} {A : Set n } {t : Set m }
  → (key : ℕ) (value : A)
  → (tree0 : bt (Color ∧ A))
  → RBtreeInvariant tree0
@@ -1730,26 +1742,80 @@
  → stackInvariant key tree1 tree0 stack
  → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) 
  → (exit : (stack : List ( bt (Color ∧ A))) (r : RBI key value tree0 stack ) → t ) → t
-replaceRBTNode {n} {m} {A} {t} key value orig rbi ti leaf stack si (case1 refl) exit = exit ? record {
-         tree = ?
-         ; repl = ?
+createRBT {n} {m} {A} {t} key value orig rbi ti tree (x ∷ []) si P exit = crbt00 orig P refl where
+     crbt00 : (tree1 : bt (Color ∧ A)) → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) → tree1 ≡ orig → t
+     crbt00 leaf P refl = exit (x ∷ []) record {  
+         tree = leaf
+         ; repl = node key ⟪ Red , value ⟫ leaf leaf
+         ; origti = ti
+         ; origrb = rbi
+         ; treerb = rb-leaf 
+         ; replrb = rb-red key value refl refl refl rb-leaf rb-leaf
+         ; si = subst (λ k → stackInvariant key k leaf _ ) crbt01 si
+         ; state = rotate refl refl rbr-leaf
+         } where
+             crbt01 : tree ≡ leaf
+             crbt01 with si-property-last _ _ _ _ si | si-property1 si
+             ... | refl | refl = refl
+     crbt00 (node key₁ value₁ left right ) (case1 eq) refl with si-property-last _ _ _ _ si | si-property1 si
+     ... | refl | refl = ⊥-elim (bt-ne (sym eq))
+     crbt00 (node key₁ value₁ left right ) (case2 eq) refl with si-property-last _ _ _ _ si | si-property1 si
+     ... | refl | refl = exit (x ∷ []) record {  
+         tree = node key₁ value₁ left right
+         ; repl = node key₁ ⟪ proj1 value₁ , value ⟫ left right 
+         ; origti = ti
+         ; origrb = rbi
+         ; treerb = rbi
+         ; replrb = crbt03 value₁ rbi
+         ; si = si
+         ; state = rebuild refl (crbt01 value₁ ) crbt04
+         }  where 
+             crbt01 : (value₁ : Color ∧ A) → black-depth (node key₁ ⟪ proj1 value₁ , value ⟫ left right) ≡ black-depth (node key₁ value₁ left right)
+             crbt01 ⟪ Red , proj4 ⟫ = refl
+             crbt01 ⟪ Black , proj4 ⟫ = refl
+             crbt03 : (value₁ : Color ∧ A) → RBtreeInvariant (node key₁ value₁ left right) → RBtreeInvariant (node key₁ ⟪ proj1 value₁ , value ⟫ left right)
+             crbt03 ⟪ Red , proj4 ⟫ (rb-red .key₁ .proj4 x x₁ x₂ rbi rbi₁) = rb-red key₁ _ x x₁ x₂ rbi rbi₁
+             crbt03 ⟪ Black , proj4 ⟫ (rb-black .key₁ .proj4 x rbi rbi₁) = rb-black key₁ _ x rbi rbi₁
+             keq : ( just key₁ ≡ just key ) → key₁ ≡ key
+             keq refl = refl
+             crbt04 : replacedRBTree key value (node key₁ value₁ left right) (node key₁ ⟪ proj1 value₁ , value ⟫ left right)
+             crbt04 = subst (λ k → replacedRBTree k value (node key₁ value₁ left right) (node key₁ ⟪ proj1 value₁ , value ⟫ left right)) (keq eq) rbr-node
+createRBT {n} {m} {A} {t} key value orig rbi ti tree (x ∷ leaf ∷ stack) si P exit = ⊥-elim (si-property-parent-node _ _ _ si refl)
+createRBT {n} {m} {A} {t} key value orig rbi ti tree sp@(x ∷ node kp vp pleft pright ∷ stack) si P exit with <-cmp key kp
+... | tri< a ¬b ¬c = crbt00 tree P refl where
+     crbt00 : (tree1 : bt (Color ∧ A)) → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) → tree1 ≡ tree → t
+     crbt00 leaf P refl = exit sp record {  
+         tree = leaf
+         ; repl = node key ⟪ Red , value ⟫ leaf leaf
+         ; origti = ti
+         ; origrb = rbi
+         ; treerb = rb-leaf
+         ; replrb = rb-red key value refl refl refl rb-leaf rb-leaf
+         ; si = si
+         ; state = rotate refl refl rbr-leaf
+         } 
+     crbt00 (node key₁ value₁ left right ) (case1 eq) refl = ⊥-elim (bt-ne (sym eq))
+     crbt00 (node key₁ value₁ left right ) (case2 eq) refl with si-property-last _ _ _ _ si | si-property1 si
+     ... | eq1 | eq2 = exit sp record {  
+         tree = node key₁ value₁ left right
+         ; repl = node key₁ ⟪ proj1 value₁ , value ⟫ left right 
          ; origti = ti
          ; origrb = rbi
          ; treerb = ?
          ; replrb = ?
-         ; si = ?
-         ; state = rotate ? ? ? 
-         }
-replaceRBTNode {n} {m} {A} {t} key value orig rbi ti (node key₁ value₁ left right) stack si (case2 x) exit = exit ? record { 
-         tree = ?
-         ; repl = ?
-         ; origti = ti
-         ; origrb = rbi
-         ; treerb = ?
-         ; replrb = ?
-         ; si = ?
-         ; state = rebuild ? ? ? 
-         }
+         ; si = si
+         ; state = rebuild refl (crbt01 value₁ ) crbt04
+         }  where 
+             crbt01 : (value₁ : Color ∧ A) → black-depth (node key₁ ⟪ proj1 value₁ , value ⟫ left right) ≡ black-depth (node key₁ value₁ left right)
+             crbt01 ⟪ Red , proj4 ⟫ = refl
+             crbt01 ⟪ Black , proj4 ⟫ = refl
+             crbt03 : (value₁ : Color ∧ A) → RBtreeInvariant (node key₁ value₁ left right) → RBtreeInvariant (node key₁ ⟪ proj1 value₁ , value ⟫ left right)
+             crbt03 ⟪ Red , proj4 ⟫ (rb-red .key₁ .proj4 x x₁ x₂ rbi rbi₁) = rb-red key₁ _ x x₁ x₂ rbi rbi₁
+             crbt03 ⟪ Black , proj4 ⟫ (rb-black .key₁ .proj4 x rbi rbi₁) = rb-black key₁ _ x rbi rbi₁
+             crbt04 : replacedRBTree key value (node key₁ value₁ left right) (node key₁ ⟪ proj1 value₁ , value ⟫ left right)
+             crbt04 = subst (λ k → replacedRBTree k value (node key₁ value₁ left right) (node key₁ ⟪ proj1 value₁ , value ⟫ left right)) ? rbr-node
+... | tri≈ ¬a b ¬c = ⊥-elim (si-property-pne _ _ _ refl si b)
+... | tri> ¬a ¬b c = ?
 
 --
 --   rotate and rebuild replaceTree and rb-invariant