Mercurial > hg > Members > Moririn

changeset 725:9e29894ae866

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, 10 Apr 2023 16:08:38 +0900
parents 35891ec243a0
children e545646e5f64
files hoareBinaryTree1.agda
diffstat 1 files changed, 40 insertions(+), 27 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Apr 10 15:06:29 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Apr 10 16:08:38 2023 +0900
@@ -547,18 +547,18 @@
 data RBTree {n : Level} (A : Set n) : (key : ℕ) → Color → (b-depth : ℕ) → Set n where
     rb-leaf     : (key : ℕ) → RBTree A key Black 0
     rb-single   : (key : ℕ) → (value : A) → (c : Color) →  RBTree A key c 1
-    t-right-red : {key key₁ : ℕ} → (value : A) → key < key₁ → {d : ℕ } → RBTree A key₁ Black d → RBTree A key Red d
-    t-right-black : {key key₁ : ℕ} → (value : A) → key < key₁ → {c : Color} → {d : ℕ }→ RBTree A key₁ c d
+    t-right-red : (key : ℕ) {key₁ : ℕ} → (value : A) → key < key₁ → {d : ℕ } → RBTree A key₁ Black d → RBTree A key Red d
+    t-right-black : (key : ℕ) {key₁ : ℕ} → (value : A) → key < key₁ → {c : Color} → {d : ℕ }→ RBTree A key₁ c d
        → RBTree A key Black (suc d)
-    t-left-red  : {key key₁ : ℕ} → (value : A) → key < key₁ → {d : ℕ} → RBTree A key Black d
+    t-left-red  : (key₁ : ℕ) { key : ℕ} → (value : A) → key < key₁ → {d : ℕ} → RBTree A key Black d
        → RBTree A key₁ Red d
-    t-left-black  : {key key₁ : ℕ} → (value : A) → key < key₁  → {c : Color} → {d : ℕ}  → RBTree A key  c d
+    t-left-black  : (key₁ : ℕ) {key : ℕ} → (value : A) → key < key₁  → {c : Color} → {d : ℕ}  → RBTree A key  c d
        → RBTree A key₁ Black (suc d)
-    t-node-red  : {key key₁ key₂ : ℕ} → (value : A) → key < key₁ → key₁ < key₂   →  {d : ℕ}
+    t-node-red  : (key₁ : ℕ) { key key₂ : ℕ} → (value : A) → key < key₁ → key₁ < key₂   →  {d : ℕ}
        → RBTree A key Black d
        → RBTree A key₂ Black d
        → RBTree A key₁ Red d
-    t-node-black  : {key key₁ key₂ : ℕ} → (value : A) → key < key₁ → key₁ < key₂  →  {c c1 : Color} {d : ℕ}
+    t-node-black  : (key₁ : ℕ) {key key₂ : ℕ} → (value : A) → key < key₁ → key₁ < key₂  →  {c c1 : Color} {d : ℕ}
        → RBTree A key c d
        → RBTree A key₂ c1 d
        → RBTree A key₁ Black (suc d)
@@ -573,39 +573,52 @@
 RB→bt : {n : Level} (A : Set n) {key d : ℕ} {c : Color } → (rb : RBTree A key c d ) → bt A
 RB→bt {n} A (rb-leaf _) = leaf
 RB→bt {n} A (rb-single key value _) = node key value leaf leaf
-RB→bt {n} A (t-right-red {key} value x rb) = node key value leaf (RB→bt A rb)
-RB→bt {n} A (t-right-black {key} value x rb) = node key value leaf (RB→bt A rb)
-RB→bt {n} A (t-left-red {_} {key} value x rb) = node key value (RB→bt A rb) leaf
-RB→bt {n} A (t-left-black {_} {key} value x rb) = node key value (RB→bt A rb) leaf
-RB→bt {n} A (t-node-red {_} {key} value x x₁ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁) 
-RB→bt {n} A (t-node-black {_} {key} value x x₁ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁) 
+RB→bt {n} A (t-right-red key value x rb) = node key value leaf (RB→bt A rb)
+RB→bt {n} A (t-right-black key value x rb) = node key value leaf (RB→bt A rb)
+RB→bt {n} A (t-left-red key value x rb) = node key value (RB→bt A rb) leaf
+RB→bt {n} A (t-left-black key value x rb) = node key value (RB→bt A rb) leaf
+RB→bt {n} A (t-node-red key value x x₁ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁) 
+RB→bt {n} A (t-node-black key value x x₁ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁) 
 
 rbt-depth : {n : Level} (A : Set n) {key : ℕ} {c : Color} {d : ℕ} → RBTree A key c d → ℕ
 rbt-depth A (rb-leaf _) = zero
 rbt-depth A (rb-single _ value _) = 1
-rbt-depth A (t-right-red value x ab) = suc ( rbt-depth A ab)
-rbt-depth A (t-right-black value x ab) = suc ( rbt-depth A ab)
-rbt-depth A (t-left-red value x ab) = suc ( rbt-depth A ab)
-rbt-depth A (t-left-black value x ab) = suc ( rbt-depth A ab)
-rbt-depth A (t-node-red value x x₁ ab ab₁) = suc (Data.Nat._⊔_ (rbt-depth A ab ) (rbt-depth A ab₁ )) 
-rbt-depth A (t-node-black value x x₁ ab ab₁) = suc (Data.Nat._⊔_ (rbt-depth A ab ) (rbt-depth A ab₁ )) 
+rbt-depth A (t-right-red _ value x ab) = suc ( rbt-depth A ab)
+rbt-depth A (t-right-black _ value x ab) = suc ( rbt-depth A ab)
+rbt-depth A (t-left-red _ value x ab) = suc ( rbt-depth A ab)
+rbt-depth A (t-left-black _ value x ab) = suc ( rbt-depth A ab)
+rbt-depth A (t-node-red _ value x x₁ ab ab₁) = suc (Data.Nat._⊔_ (rbt-depth A ab ) (rbt-depth A ab₁ )) 
+rbt-depth A (t-node-black _ value x x₁ ab ab₁) = suc (Data.Nat._⊔_ (rbt-depth A ab ) (rbt-depth A ab₁ )) 
 
-rbt-key : ?
-rbt-key = ?
-
+rbt-key : {n : Level} (A : Set n) {key : ℕ} {c : Color} {d : ℕ} → RBTree A key c d → Maybe ℕ
+rbt-key {n} A (rb-leaf _) = nothing
+rbt-key {n} A (rb-single key value _) = just key
+rbt-key {n} A (t-right-red key value x rb) = just key
+rbt-key {n} A (t-right-black key value x rb) = just key
+rbt-key {n} A (t-left-red key value x rb) = just key
+rbt-key {n} A (t-left-black key value x rb) = just key
+rbt-key {n} A (t-node-red key value x x₁ rb rb₁) = just key
+rbt-key {n} A (t-node-black key value x x₁ rb rb₁) = just key
 
-findRBP : {n m : Level} {A : Set n} {t : Set m} → (key key1 d d1 : ℕ) → (c : Color) → (tree : RBTree A key c d ) (tree1 : RBTree A key1 ? d1 ) 
+findRBP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) {key1 d d1 : ℕ} → {c c1 : Color} → (tree : RBTree A key c d ) (tree1 : RBTree A key1 c1 d1 ) 
            →  rbstackInvariant tree key1
-           → (next : (key0 d0 : ℕ) (tree1 : RBTree A key0 ? d0 ) → rbstackInvariant tree1 key0 → rbt-depth A tree1 < rbt-depth A tree   → t )
-           → (exit : (key0 d0 : ℕ) (tree0 : RBTree A key0 ? d0 ) → rbstackInvariant tree1 key0
-                 → (tree1 ≡ ? ) ∨ ( rbt-key tree1 ≡ just key )  → t ) → t
+           → (next : {key0 d0 : ℕ} {c0 : Color} → (tree0 : RBTree A key0 c0 d0 ) → rbstackInvariant tree key0 → rbt-depth A tree0 < rbt-depth A tree1   → t )
+           → (exit : {key0 d0 : ℕ} {c0 : Color} → (tree0 : RBTree A key0 c0 d0 ) → rbstackInvariant tree key0
+                 → (rbt-depth A tree0 ≡ 0 ) ∨ ( rbt-key A tree0 ≡ just key )  → t ) → t
 findRBP = ?
 
-
+record ReplaceRBT {n : Level} {A : Set n} (key : ℕ) (value : A) {key0 key1 d0 d1 : ℕ} {c0 c1 : Color}
+     (orig : RBTree A ? ? ? ) 
+     (tree : RBTree A key0 c0 d0) (repl : RBTree A key1 c1 d1)  (si : rbstackInvariant orig key0) : Set n where
+   field
+     keyr dr : ℕ
+     cr : Color
+     treer : RBTree A keyr cr dr
+     ri : replacedTree key value ? ?
 
 replaceRBP : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) → {key1 key2 d1 d2 : ℕ} {c1 c2 : Color}  → (tree : RBTree A key1 c1 d1 ) ( repl : RBTree A key2 c2 d2 )
-     → ?
+     → (RR : ReplaceRBT A ? ? ? ? ? )
      → (next : ℕ → A → {tree1 : RBTree A ? ? ? } (repl : RBTree A ? ? ? ) → (stack1 : rbstackInvariant tree1 key1 ) → ? → t )
      → (exit : (tree1 : RBTree A ? ? ? ) → (repl : RBTree A ? ? ? ) → t ) → t
 replaceRBP = ?