Mercurial > hg > Members > Moririn

changeset 760:927c02120a73

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 Thu, 04 May 2023 18:40:10 +0900
parents 8435718138d1
children 6ae130db4c5b 56de8e7dca7a
files hoareBinaryTree1.agda
diffstat 1 files changed, 17 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Wed May 03 16:55:21 2023 +0900
+++ b/hoareBinaryTree1.agda	Thu May 04 18:40:10 2023 +0900
@@ -634,6 +634,16 @@
 stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left {_} {_} {t1} {k1} {v1} x (s-left x₁ (s-left x₂ si))) = case2 (case2
     record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
 
+stackCase1 : {n : Level} {A : Set n} → {key : ℕ } → {tree orig : bt A }
+           →  {stack : List (bt A)} → stackInvariant key tree orig stack
+           →  stack ≡ orig ∷ [] → tree ≡ orig
+stackCase1 s-nil refl = refl
+
+stackCase2 : {n : Level} {A : Set n} → {key : ℕ } → {tree orig : bt A }
+           →  {stack : List (bt A)} → stackInvariant key tree orig stack
+           → stack ≡ tree ∷ orig ∷ [] → {k1 : ℕ} {v1 : A} →  (orig ≡  node k1 v1 tree leaf) ∨ (orig ≡  node k1 v1 leaf tree )
+stackCase2 (s-right x s-nil) refl = case2 ?
+stackCase2 (s-left x si) refl = ?
 
 PGtoRBinvariant : {n : Level} {A : Set n} → {key d0 ds dp dg : ℕ } → (tree orig : bt (Color ∧ A) )
            →  RBtreeInvariant orig d0 
@@ -753,9 +763,9 @@
         → 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) )
+     → (exit : (rot repl : bt (Color ∧ A) )
         →  {d : ℕ} → RBtreeInvariant repl d 
-        → (ri : rotatedTree to rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
+        → (ri : rotatedTree to rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key 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 ) 
@@ -791,8 +801,11 @@
       -- 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 rot repl rbir {!!}  ? -- (subst₂ (λ j k → replacedTree key ⟪ {!!} , value ⟫ j k ) {!!} {!!} r-node )
-    ... | case2 (case1 eq ) = {!!}
+    ... | case1 eq = exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri 
+    ... | case2 (case1 eq ) = ? where
+        insertCase12 : t
+        insertCase12 = ?
+    -- exit rot repl rbir ? ? 
     ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)