Mercurial > hg > Members > Moririn

changeset 738:da56e6fb7667

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 Sat, 22 Apr 2023 14:54:28 +0900
parents 7ae2dea2546b
children 3443703a68cc
files hoareBinaryTree1.agda
diffstat 1 files changed, 27 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sat Apr 22 10:26:00 2023 +0900
+++ b/hoareBinaryTree1.agda	Sat Apr 22 14:54:28 2023 +0900
@@ -563,6 +563,9 @@
        → RBTree A key₂ c1 d
        → RBTree A key₁ Black (suc d)
 
+color : {n : Level} (A : Set n) {key d : ℕ} {c : Color } → (rb : RBTree A key c d ) → Color
+color {n} A {k} {d} {c} rb = c
+
 RB→bt : {n : Level} (A : Set n) {key d : ℕ} {c : Color } → (rb : RBTree A key c d ) → bt A
 RB→bt {n} A (rb-leaf _) = leaf
 RB→bt {n} A (rb-single key value _) = node key value leaf leaf
@@ -647,20 +650,31 @@
      → (key : ℕ) → (value : A) → {key0 key1 d0 d1 : ℕ} {c0 c1 : Color}  
      → (orig : RBTree A key0 c0 d0 ) → (tree : RBTree A key1 c1 d1 ) 
      → (stack : List (bt A)) → (si : stackInvariant key (RB→bt A tree) (RB→bt A orig) stack ) 
-     → (next : {key2 d2 : ℕ} {c2 : Color} → (tree2 : RBTree A key2 c2 d2 ) → (stack1 : List (bt A)) → stackInvariant key (RB→bt A tree2)  (RB→bt A orig) stack1 
+     → (next : {key2 d2 : ℕ} {c2 : Color} → (tree2 : RBTree A key2 c2 d2 ) 
+        → {tr to : bt A} → RB→bt A tree2 ≡ tr → RB→bt A orig ≡ to
+        → (stack1 : List (bt A)) → stackInvariant key tr to stack1 
         → length stack1 < length stack  → t )
      → (exit : {k1 d1 : ℕ} {c1 : Color} → (repl1 : RBTree A k1 c1 d1 ) → (rot : bt A )
-         → (ri : rotatedTree (RB→bt A orig) rot ) → replacedTree key value rot (RB→bt A repl1)
-         → t ) → t
-replaceRBP {n} {m} {A} {t} key value {_} {key1} orig tree stack si next exit = insertCase1 ? ? where
-    insertCase4 : (key1 : ℕ) → (si : ParentGrand ? ? ? ) →  {k1 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) → t
-    insertCase4 = ?
-    insertCase3 : (key1 : ℕ) → (si : ParentGrand ? ? ? ) →  {k1 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) → t
-    insertCase3 key1 si parent grandparent = ?
-    insertCase2 : (key1 : ℕ) → (si : ParentGrand ? ? ? ) →  {k1 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) → t
-    insertCase2 key1 si {_} {_} {_} {_} {Red} parent grand = insertCase3 key1 si parent grand
-    insertCase2 key1 si {_} {_} {_} {_} {Black} parent grand = next ? ? ? ?
-    insertCase1 : (key1 : ℕ)  (si : ParentGrand ? ? ? )  → t
-    insertCase1 key1 = ?
+         → (ri : rotatedTree (RB→bt A orig) rot ) → replacedTree key value rot (RB→bt A repl1) → t ) → t
+replaceRBP {n} {m} {A} {t} key value {_} {key1} orig tree stack si next exit = insertCase1 stack _ _ refl refl si where
+    insertCase2 : {k0 k1 d0 d1 d2 : ℕ} {c0 c1 c2 : Color} → (tree : RBTree A k0 c0 d0) 
+      → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) 
+      → (stack : List (bt A)) → (tr to : bt A) → RB→bt A grand ≡ tr →  RB→bt A orig ≡ to → (si : stackInvariant key tr to stack ) 
+      → (pg : ParentGrand (RB→bt A tree) (RB→bt A parent) tr ) → t
+    insertCase2 tree parent grand stack tr to treq toeq si pg with color A parent
+    ... | Black = next grand ? ? stack si ?
+    ... | Red = ? where
+        insertCase4 : (key1 : ℕ) → (si : ParentGrand ? ? ? ) →  {k1 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) → t
+        insertCase4 = ?
+        insertCase3 : (key1 : ℕ) → (si : ParentGrand ? ? ? ) →  {k1 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) → t
+        insertCase3 key1 si parent grandparent = ?
+    insertCase1 : (stack : List (bt A)) → (tr to : bt A) → RB→bt A tree ≡ tr →  RB→bt A orig ≡ to → (si : stackInvariant key tr to stack ) → t
+    insertCase1 .(tr ∷ []) tr .tr req oeq s-nil = ?
+    insertCase1 .(tr ∷ node _ _ _ tr ∷ []) tr .(node _ _ _ tr) req oeq (s-right x s-nil) = ?
+    insertCase1 .(tr ∷ node _ _ _ tr ∷ _) tr to req oeq (s-right x (s-right x₁ si)) = ?
+    insertCase1 .(tr ∷ node _ _ _ tr ∷ _) tr to req oeq (s-right x (s-left x₁ si)) = ?
+    insertCase1 .(tr ∷ node _ _ tr _ ∷ []) tr .(node _ _ tr _) req oeq (s-left x s-nil) = ?
+    insertCase1 .(tr ∷ node _ _ tr _ ∷ _) tr to req oeq (s-left x (s-right x₁ si)) = ?
+    insertCase1 .(tr ∷ node _ _ tr _ ∷ _) tr to req oeq (s-left x (s-left x₁ si)) = ?