Mercurial > hg > Members > Moririn

changeset 759:8435718138d1

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, 03 May 2023 16:55:21 +0900
parents 2488a3402c19
children 927c02120a73
files hoareBinaryTree1.agda
diffstat 1 files changed, 13 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Tue May 02 07:42:19 2023 +0900
+++ b/hoareBinaryTree1.agda	Wed May 03 16:55:21 2023 +0900
@@ -738,24 +738,25 @@
 -- if we have replacedNode on RBTree, we have RBtreeInvariant
 
 replaceRBP : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A) → {d0 : ℕ} 
-     → (orig tree 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 ) 
-     → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key tree) repl
-     → (next : {key2 d2 : ℕ} {c2 : Color}   -- rotating case
+     → (key : ℕ) → (value : A) 
+     → (to tr rot rr : bt (Color ∧ A)) 
+     →  {d0 : ℕ} → RBtreeInvariant to d0 
+     →  {d  : ℕ} → RBtreeInvariant tr d →  {dr : ℕ} → RBtreeInvariant rr dr 
+     → (stack : List (bt (Color ∧ A))) → stackInvariant key tr to stack
+     → rotatedTree tr rot
+     → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
+     → (next : {key2 d2 : ℕ} {c2 : Color}   
         → (to tr rot rr : bt (Color ∧ A)) 
-        →  RBtreeInvariant orig d0 
-        →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
+        →  RBtreeInvariant to d0 
+        →  {d : ℕ} → RBtreeInvariant tr 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
-replaceRBP {n} {m} {A} {t} key value orig tree repl rbio rbit rbir stack si ri next exit = insertCase1 where
+        → (ri : rotatedTree to rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
+replaceRBP {n} {m} {A} {t} key value orig tree rot repl rbio rbit rbir stack si roti {c} ri next exit = ? where
     insertCase2 : (tree parent uncle grand : bt (Color ∧ A)) 
       → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
       → (pg : ParentGrand tree parent uncle grand ) → t
@@ -790,7 +791,7 @@
       -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
     insertCase1 : t
     insertCase1 with stackToPG tree orig stack si
-    ... | case1 eq = exit repl repl rbir {!!} (subst₂ (λ j k → replacedTree key ⟪ {!!} , value ⟫ j k ) {!!} {!!} r-node )
+    ... | case1 eq = exit rot repl rbir {!!}  ? -- (subst₂ (λ j k → replacedTree key ⟪ {!!} , value ⟫ j k ) {!!} {!!} r-node )
     ... | case2 (case1 eq ) = {!!}
     ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)