Mercurial > hg > Members > Moririn

changeset 726:e545646e5f64

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 17:57:26 +0900
parents 9e29894ae866
children fd63d70310c3
files hoareBinaryTree1.agda
diffstat 1 files changed, 19 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Apr 10 16:08:38 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Apr 10 17:57:26 2023 +0900
@@ -570,6 +570,12 @@
     s-left :   {key₁ key₂ : ℕ} → {c1 : Color} {d1 : ℕ} → key₂ < key₁  →  (top : RBTree A key₁ c1 d1) 
         → rbstackInvariant orig key₁ → rbstackInvariant orig key
 
+rbsi-len :  {n : Level} {A : Set n}  {key : ℕ} {c : Color} {d : ℕ} (orig : RBTree A key c d ) {key₁ : ℕ } 
+     → rbstackInvariant orig key₁ → ℕ
+rbsi-len orig s-single = 0
+rbsi-len orig (s-right x top ri) = suc (rbsi-len orig ri)
+rbsi-len orig (s-left x top ri)  = suc (rbsi-len orig ri)
+
 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
@@ -607,20 +613,23 @@
                  → (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
+record ReplaceRBT {n : Level} {A : Set n} (key : ℕ) (value : A) {key1 key2 d1 d2 : ℕ} {c1 c2 : Color}
+     (tree : RBTree A key1 c1 d1) (repl : RBTree A key2 c2 d2)   : Set n where
    field
-     keyr dr : ℕ
-     cr : Color
-     treer : RBTree A keyr cr dr
-     ri : replacedTree key value ? ?
+     key0 d0 : ℕ
+     c0 : Color
+     orig : RBTree A key0 c0 d0
+     si : rbstackInvariant orig key0
+     ri : replacedTree key value (RB→bt A tree) (RB→bt A repl)
+   si-len : ℕ
+   si-len = rbsi-len orig si
 
 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
+     → (RR : ReplaceRBT key value tree repl  )
+     → (next : ℕ → A → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (tree1 : RBTree A k1 c1 d1 ) (repl : RBTree A k2 c2 d2 ) → (RR1 : ReplaceRBT key value tree1 repl ) 
+         → ReplaceRBT.si-len RR1 < ReplaceRBT.si-len RR    → t )
+     → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 : RBTree A k1 c1 d1 ) → (repl : RBTree A k2 c2 d2 ) → t ) → t
 replaceRBP = ?