Mercurial > hg > Members > Moririn

changeset 777:8e5159a02b76

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, 16 May 2023 17:58:04 +0900
parents 576b35b1d2d7
children 4d71d0894cfa
files hoareBinaryTree1.agda
diffstat 1 files changed, 17 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Fri May 12 13:01:13 2023 +0900
+++ b/hoareBinaryTree1.agda	Tue May 16 17:58:04 2023 +0900
@@ -807,17 +807,17 @@
 
 replaceRBP : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) 
-     → (orig tree : bt (Color ∧ A)) 
+     → (orig repl : bt (Color ∧ A)) 
      → (stack : List (bt (Color ∧ A))) 
-     → (r : RBI key value orig tree stack )
-     → (next : (tree1 : (bt (Color ∧ A))) →  (stack1 : List (bt (Color ∧ A))) 
-        → (r : RBI key value orig tree1 stack1 ) 
+     → (r : RBI key value orig repl stack )
+     → (next : (repl1 : (bt (Color ∧ A))) →  (stack1 : List (bt (Color ∧ A))) 
+        → (r : RBI key value orig repl1 stack1 ) 
         → length stack1 < length stack  → t )
      → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
         →  stack1 ≡ (orig ∷ [])
         →  RBI key value orig repl stack1
         → t ) → t
-replaceRBP {n} {m} {A} {t} key value orig stack r next exit = ? where
+replaceRBP {n} {m} {A} {t} key value orig repl stack r 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
@@ -851,8 +851,18 @@
       -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree
       -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
     insertCase1 : t
-    insertCase1 with stackToPG ? orig ? ?
-    ... | case1 eq = ? -- exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri 
+    insertCase1 with stackToPG (RBI.tree r) orig stack (RBI.si r)
+    ... | case1 eq = exit repl stack eq record {  -- exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri 
+       od = ? ; d = ? ; rd = ?
+       ; tree = RBI.tree r ; rot = ?
+       ; origti = ?
+       ; origrb = ?
+       ; treerb = ?
+       ; replrb = ?
+       ; d=rd = ?
+       ; si = ?
+       ; rotated = ?
+       ; ri = ? }
     ... | case2 (case1 eq ) = ? where
         insertCase12 : (to : bt (Color ∧ A)) → {d : ℕ} → RBtreeInvariant orig d  → to ≡ orig
           → (rr : bt (Color ∧ A)) → {dr : ℕ} → RBtreeInvariant ? dr  → rr ≡ ?