Mercurial > hg > Members > Moririn

changeset 724:35891ec243a0

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 15:06:29 +0900
parents 43180a01bfbe
children 9e29894ae866
files hoareBinaryTree1.agda
diffstat 1 files changed, 18 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Apr 10 10:43:00 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Apr 10 15:06:29 2023 +0900
@@ -18,12 +18,6 @@
 open import logic
 
 
-_iso_ : {n : Level} {a : Set n} → ℕ → ℕ → Set
-d iso d' = (¬ (suc d ≤ d')) ∧ (¬ (suc d' ≤ d))
-
-iso-intro : {n : Level} {a : Set n} {x y : ℕ} → ¬ (suc x ≤ y) → ¬ (suc y ≤ x) → _iso_ {n} {a} x y
-iso-intro = λ z z₁ → record { proj1 = z ; proj2 = z₁ }
-
 --
 --
 --  no children , having left node , having right node , having both
@@ -586,8 +580,15 @@
 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 : ?
-rbt-depth = ?
+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-key : ?
 rbt-key = ?
@@ -595,10 +596,18 @@
 
 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 ) 
            →  rbstackInvariant tree key1
-           → (next : (key0 d0 : ℕ ) (tree1 : RBTree A key0 ? d0 ) → rbstackInvariant tree1 key0 → rbt-depth tree1 < rbt-depth tree   → t )
+           → (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
 findRBP = ?
 
 
 
+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 )
+     → ?
+     → (next : ℕ → A → {tree1 : RBTree A ? ? ? } (repl : RBTree A ? ? ? ) → (stack1 : rbstackInvariant tree1 key1 ) → ? → t )
+     → (exit : (tree1 : RBTree A ? ? ? ) → (repl : RBTree A ? ? ? ) → t ) → t
+replaceRBP = ?
+
+