Mercurial > hg > Members > Moririn

changeset 730:dbef4bd0f69b

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 Tue, 11 Apr 2023 19:42:06 +0900
parents 5599bd559f3e
children 5b2985ecfcf7
files hoareBinaryTree1.agda
diffstat 1 files changed, 18 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Tue Apr 11 19:08:39 2023 +0900
+++ b/hoareBinaryTree1.agda	Tue Apr 11 19:42:06 2023 +0900
@@ -645,23 +645,28 @@
      → (orig : RBTree A key1 c1 d1 ) → (tree : RBTree A key1 c1 d1 ) ( repl : RBTree A key2 c2 d2 )
      → (si : rbstackInvariant orig key1)
      → (ri : replacedTree key value (RB→bt A tree) (RB→bt A repl))
-     → (next : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 : RBTree A k1 c1 d1 ) → (repl1 : RBTree A k2 c2 d2 ) 
+     → (next : ℕ → A → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (tree1 : RBTree A k1 c1 d1 ) (repl1 : RBTree A k2 c2 d2 ) 
+         → (si1 : rbstackInvariant orig k1)
+         → (ri : replacedTree key value (RB→bt A tree1) (RB→bt A repl1))
+         → rbsi-len orig si1 < rbsi-len orig si → t )
+     → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 : RBTree A k1 c1 d1 ) → (repl1 : RBTree A k2 c2 d2 ) 
          → (ri : replacedTree key value (RB→bt A orig) (RB→bt A repl1))
          → t ) → t
-replaceRBP {n} {m} {A} {t} key value orig tree repl si ri next = ? where
-    insertCase4 : (key1 : ℕ) → (si : rbstackInvariant orig key1) → (parent : RBTree A ? ? ?) → (grand : RBTree A ? ? ?) → t
+replaceRBP {n} {m} {A} {t} key value {_} {key2} orig tree repl si ri next exit = replaceRBP1 key2 si where
+    insertCase4 : (key1 : ℕ) → (si : rbstackInvariant orig key1) →  {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A k2 c2 d2) → t
     insertCase4 = ?
-    insertCase3 : (key1 : ℕ) → (si : rbstackInvariant orig key1) → (parent : RBTree A ? ? ?) → (grand : RBTree A ? ? ?) → t
+    insertCase3 : (key1 : ℕ) → (si : rbstackInvariant orig key1) →  {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A k2 c2 d2) → t
     insertCase3 = ?
-    insertCase2 : (key1 : ℕ) → (si : rbstackInvariant orig key1) → (parent : RBTree A ? ? ?) → (grand : RBTree A ? ? ?) → t
-    insertCase2 key1 si parent grand = ?
+    insertCase2 : (key1 : ℕ) → (si : rbstackInvariant orig key1) →  {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A k2 c2 d2) → t
+    insertCase2 key1 si {_} {_} {_} {_} {Red} parent grand = insertCase3 key1 si parent grand
+    insertCase2 key1 si {_} {_} {_} {_} {Black} parent grand = next ? ? ? ? ? ? ?
     replaceRBP1 : (key1 : ℕ)  (si : rbstackInvariant orig key1)  → t
-    replaceRBP1 key1 s-nil = ?
-    replaceRBP1 key1 (s-right {key₁} {key₂} x top s-nil) = ?
-    replaceRBP1 key1 (s-right {key₁} {key₂} x top (s-right {key₃} {key₄} x₁ top₁ si)) = insertCase2 key₃ si ? ?
-    replaceRBP1 key1 (s-right {key₁} {key₂} x top (s-left {key₃} {key₄} x₁ top₁ si)) = ?
-    replaceRBP1 key1 (s-left {key₁} {key₂} x top s-nil) = ?
-    replaceRBP1 key1 (s-left {key₁} {key₂} x top (s-right {key₃} {key₄} x₁ top₁ si)) = ?
-    replaceRBP1 key1 (s-left {key₁} {key₂} x top (s-left {key₃} {key₄} x₁ top₁ si)) = ?
+    replaceRBP1 key1 s-nil = exit ? ? ?
+    replaceRBP1 key1 (s-right {key₁} {key₂} x top s-nil) = exit ? ? ?
+    replaceRBP1 key1 (s-right {key₁} {key₂} x top (s-right {key₃} {key₄} x₁ top₁ si)) = insertCase2 key₃ si top top₁ 
+    replaceRBP1 key1 (s-right {key₁} {key₂} x top (s-left {key₃} {key₄} x₁ top₁ si)) = insertCase2 key₃ si top top₁ 
+    replaceRBP1 key1 (s-left {key₁} {key₂} x top s-nil) = exit ? ? ?
+    replaceRBP1 key1 (s-left {key₁} {key₂} x top (s-right {key₃} {key₄} x₁ top₁ si)) = insertCase2 key₃ si top top₁ 
+    replaceRBP1 key1 (s-left {key₁} {key₂} x top (s-left {key₃} {key₄} x₁ top₁ si)) = insertCase2 key₃ si top top₁