Mercurial > hg > Gears > GearsAgda

changeset 731:5b2985ecfcf7

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 20:06:26 +0900
parents dbef4bd0f69b
children 18cd778f4bad
files hoareBinaryTree1.agda
diffstat 1 files changed, 14 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Tue Apr 11 19:42:06 2023 +0900
+++ b/hoareBinaryTree1.agda	Tue Apr 11 20:06:26 2023 +0900
@@ -620,6 +620,11 @@
 findRBP {n} {m} {A} {t} key tree (t-node-red _ value x x₁ tree1 tree2) si next exit = ?
 findRBP {n} {m} {A} {t} key tree (t-node-black _ value x x₁ tree1 tree2) si next exit = ?
 
+rotateRight : ?
+rotateRight = ?
+rotateLeft : ?
+rotateLeft = ?
+
 insertCase5 : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) → {key0 key1 key2 d0 d1 d2 : ℕ} {c0 c1 c2 : Color}  
      → (orig : RBTree A key1 c1 d1 ) → (tree : RBTree A key1 c1 d1 ) ( repl : RBTree A key2 c2 d2 )
@@ -633,10 +638,6 @@
          → (ri : replacedTree key value (RB→bt A orig) (RB→bt A repl1))
          → t ) → t
 insertCase5 {n} {m} {A} {t} key value orig tree repl si ri next exit = ? where
-    rotateRight : ?
-    rotateRight = ?
-    rotateLeft : ?
-    rotateLeft = ?
     insertCase51 : (key1 : ℕ)  (si : rbstackInvariant orig key1)  → t
     insertCase51 = ?
 
@@ -652,7 +653,7 @@
      → (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 {_} {key2} orig tree repl si ri next exit = replaceRBP1 key2 si where
+replaceRBP {n} {m} {A} {t} key value {_} {key2} orig tree repl si ri next exit = insertCase1 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) →  {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A k2 c2 d2) → t
@@ -660,13 +661,13 @@
     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 = 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₁ 
+    insertCase1 : (key1 : ℕ)  (si : rbstackInvariant orig key1)  → t
+    insertCase1 key1 s-nil = exit ? ? ?
+    insertCase1 key1 (s-right {key₁} {key₂} x top s-nil) = exit ? ? ?
+    insertCase1 key1 (s-right {key₁} {key₂} x top (s-right {key₃} {key₄} x₁ top₁ si)) = insertCase2 key₃ si top top₁ 
+    insertCase1 key1 (s-right {key₁} {key₂} x top (s-left {key₃} {key₄} x₁ top₁ si)) = insertCase2 key₃ si top top₁ 
+    insertCase1 key1 (s-left {key₁} {key₂} x top s-nil) = exit ? ? ?
+    insertCase1 key1 (s-left {key₁} {key₂} x top (s-right {key₃} {key₄} x₁ top₁ si)) = insertCase2 key₃ si top top₁ 
+    insertCase1 key1 (s-left {key₁} {key₂} x top (s-left {key₃} {key₄} x₁ top₁ si)) = insertCase2 key₃ si top top₁