Mercurial > hg > Members > Moririn

changeset 751:4ecad6cfef4b

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 Wed, 26 Apr 2023 09:20:38 +0900
parents 61e16b7489b8
children 44837beece64
files hoareBinaryTree1.agda
diffstat 1 files changed, 25 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Wed Apr 26 09:10:12 2023 +0900
+++ b/hoareBinaryTree1.agda	Wed Apr 26 09:20:38 2023 +0900
@@ -641,27 +641,33 @@
                  → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
 findRBT = ?
 
-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 tree repl : bt (Color ∧ A)  )
-     → (si : ParentGrand ? ? ?)
-     → (ri : rotatedTree (RB→bt A tree) (RB→bt A repl))
-     → (next : ℕ → A → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (tree1 repl1 : bt (Color ∧ A))
-         → (si1 : ParentGrand ? ? ?)
-         → (ri : rotatedTree (RB→bt A tree1) (RB→bt A repl1))
-         → length ? < length ? → t )
-     → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 repl1 : bt (Color ∧ A)) 
-         → (ri : rotatedTree (RB→bt A orig) (RB→bt A repl1))
-         → t ) → t
+     → (key : ℕ) → (value : A) → {d0 : ℕ} 
+     → (orig tree rot repl : bt (Color ∧ A)) {d0 : ℕ}
+     →  RBtreeInvariant orig d0 
+     →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant repl dr 
+     → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
+     → rotatedTree tree rot
+     → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl
+     → (next : {key2 d2 : ℕ} {c2 : Color}   -- rotating case
+        → (to tr rot rr : bt (Color ∧ A)) 
+        →  RBtreeInvariant orig d0 
+        →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
+        → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 
+        → rotatedTree tr rot
+        → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
+        → length stack1 < length stack  → t )
+     → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
+        →  {d : ℕ} → RBtreeInvariant repl d 
+        → (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
 insertCase5 {n} {m} {A} {t} key value orig tree repl si ri next exit = ? where
     insertCase51 : (key1 : ℕ)  (si : ParentGrand ? ? ? )  → t
     insertCase51 = ?
+    rotateRight : ?
+    rotateRight = ?
+    rotateLeft : ?
+    rotateLeft = ?
+
 
 -- if we have replacedNode on RBTree, we have RBtreeInvariant
 
@@ -672,7 +678,7 @@
      →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant repl dr 
      → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
      → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key tree) repl
-     → (next : {key2 d2 : ℕ} {c2 : Color}  
+     → (next : {key2 d2 : ℕ} {c2 : Color}   -- no rotating case
         → (to tr rr : bt (Color ∧ A)) 
         →  RBtreeInvariant orig d0 
         →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
@@ -688,7 +694,7 @@
       → (pg : ParentGrand tree parent grand ) → t
     insertCase2 tree parent grand stack si pg with color A parent
     ... | Black = ?   -- tree stuctre is preserved
-    ... | Red = insertCase3 grand refl where
+    ... | Red = ? where  -- insertCase3 grand refl where
         --
         --  in some case, stack is poped and loop to replaceRBP
         --     it means, we have to create replacedTree