Mercurial > hg > Members > Moririn

changeset 737:7ae2dea2546b

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 10:26:00 +0900
parents 744ead2536a4
children da56e6fb7667
files hoareBinaryTree1.agda
diffstat 1 files changed, 28 insertions(+), 39 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Fri Apr 21 14:44:52 2023 +0900
+++ b/hoareBinaryTree1.agda	Sat Apr 22 10:26:00 2023 +0900
@@ -593,14 +593,13 @@
 rbt-key {n} A (t-node-red key value x x₁ rb rb₁) = just key
 rbt-key {n} A (t-node-black key value x x₁ rb rb₁) = just key
 
-data rbstackInvariant2 {n : Level} {A : Set n} (self : bt A) : (parent grand : bt A) → Set n where
-    s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent : bt A } → parent ≡ node kp vp self n1 → rbstackInvariant2 self parent (node kg vg parent n2) 
-    s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent : bt A } → parent ≡ node kp vp n1 self → rbstackInvariant2 self parent (node kg vg parent n2) 
-    s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent : bt A } → parent ≡ node kp vp self n1 → rbstackInvariant2 self parent (node kg vg n2 parent) 
-    s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent : bt A } → parent ≡ node kp vp n1 self → rbstackInvariant2 self parent (node kg vg n2 parent) 
+data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent grand : bt A) → Set n where
+    s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent : bt A } → parent ≡ node kp vp self n1 → ParentGrand self parent (node kg vg parent n2) 
+    s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent : bt A } → parent ≡ node kp vp n1 self → ParentGrand self parent (node kg vg parent n2) 
+    s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent : bt A } → parent ≡ node kp vp self n1 → ParentGrand self parent (node kg vg n2 parent) 
+    s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent : bt A } → parent ≡ node kp vp n1 self → ParentGrand self parent (node kg vg n2 parent) 
 
 data rotatedTree  {n : Level} {A : Set n}  : (before after : bt A ) → Set n where
-    rr-leaf : rotatedTree leaf leaf
     rr-node : {t : bt A} → rotatedTree t t
     rr-right : {ka kb : ℕ } {va vb : A} → {ta tb tc ta1 tb1 tc1 : bt A}
           → ka < kb
@@ -612,22 +611,15 @@
           → rotatedTree (node kb vb ta (node ka va tb tc) ) (node ka va (node kb vb ta1 tb1)  tc1) 
 
 rbsi-len :  {n : Level} {A : Set n} {orig parent grand : bt A}
-     → rbstackInvariant2 orig parent grand → ℕ
+     → ParentGrand orig parent grand → ℕ
 rbsi-len {n} {A} {s} {p} {g} st = ?
 
-findRBP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) {key1 d d1 : ℕ} → {c c1 : Color} → (tree : RBTree A key c d ) (tree1 : RBTree A key1 c1 d1 ) 
-           →  rbstackInvariant2 ? ? ?
-           → (next : {key0 d0 : ℕ} {c0 : Color} → (tree0 : RBTree A key0 c0 d0 ) → rbstackInvariant2 ? ? ? → rbt-depth A tree0 < rbt-depth A tree1   → t )
-           → (exit : {key0 d0 : ℕ} {c0 : Color} → (tree0 : RBTree A key0 c0 d0 ) → rbstackInvariant2 ? ? ?
-                 → (rbt-depth A tree ≡ 0 ) ∨ ( rbt-key A tree ≡ just key )  → t ) → t
-findRBP {n} {m} {A} {t} key {key1} tree (rb-leaf _) si next exit = exit tree si ?
-findRBP {n} {m} {A} {t} key tree (rb-single _ value _) si next exit = ?
-findRBP {n} {m} {A} {t} key tree (t-right-red _ value x tree1) si next exit = ?
-findRBP {n} {m} {A} {t} key tree (t-right-black _ value x tree1) si next exit = ?
-findRBP {n} {m} {A} {t} key tree (t-left-red _ value x tree1) si next exit = ?
-findRBP {n} {m} {A} {t} key tree (t-left-black _ value x tree1) si next exit = ?
-findRBP {n} {m} {A} {t} key tree (t-node-red _ value x x₁ tree1 tree2) si next exit = ?
-findRBP {n} {m} {A} {t} key tree (t-node-black _ value x x₁ tree1 tree2) si next exit = ?
+findRBP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) {key1 d d1 : ℕ} → {c c1 : Color} → (tree : RBTree A key c d ) (orig : RBTree A key1 c1 d1 ) 
+           →  (stack : List (bt A)) → stackInvariant key (RB→bt A tree) (RB→bt A orig) stack
+           → (next : {key0 d0 : ℕ} {c0 : Color} → (tree1 : RBTree A key0 c0 d0 ) → (stack : List (bt A)) → stackInvariant key (RB→bt A tree1) (RB→bt A orig) stack  → rbt-depth A tree1 < rbt-depth A tree   → t )
+           → (exit : {key0 d0 : ℕ} {c0 : Color} → (tree1 : RBTree A key0 c0 d0 ) → (stack : List (bt A)) → stackInvariant key (RB→bt A tree1) (RB→bt A orig) stack 
+                 → (rbt-depth A tree1 ≡ 0 ) ∨ ( rbt-key A tree1 ≡ just key )  → t ) → t
+findRBP {n} {m} {A} {t} key {key1} tree orig st si next exit = ?
 
 rotateRight : ?
 rotateRight = ?
@@ -638,40 +630,37 @@
 insertCase5 : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) → {key0 key1 key2 d0 d1 d2 : ℕ} {c0 c1 c2 : Color}  
      → (orig : RBTree A key1 c1 d1 ) → (tree : RBTree A key1 c1 d1 ) ( repl : RBTree A key2 c2 d2 )
-     → (si : rbstackInvariant2 ? ? ?)
+     → (si : ParentGrand ? ? ?)
      → (ri : rotatedTree (RB→bt A tree) (RB→bt A repl))
      → (next : ℕ → A → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (tree1 : RBTree A k1 c1 d1 ) (repl1 : RBTree A k2 c2 d2 ) 
-         → (si1 : rbstackInvariant2 ? ? ?)
+         → (si1 : ParentGrand ? ? ?)
          → (ri : rotatedTree (RB→bt A tree1) (RB→bt A repl1))
          → rbsi-len si1 < rbsi-len si → t )
      → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 : RBTree A k1 c1 d1 ) → (repl1 : RBTree A k2 c2 d2 ) 
          → (ri : rotatedTree (RB→bt A orig) (RB→bt A repl1))
          → t ) → t
 insertCase5 {n} {m} {A} {t} key value orig tree repl si ri next exit = ? where
-    insertCase51 : (key1 : ℕ)  (si : rbstackInvariant2 ? ? ? )  → t
+    insertCase51 : (key1 : ℕ)  (si : ParentGrand ? ? ? )  → t
     insertCase51 = ?
 
 replaceRBP : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A) → {key0 key1 key2 d0 d1 d2 : ℕ} {c0 c1 c2 : Color}  
-     → (orig : RBTree A key1 c1 d1 ) → (tree : RBTree A key1 c1 d1 ) ( repl : RBTree A key2 c2 d2 )
-     → (si : rbstackInvariant2 ? ? ? )
-     → (ri : rotatedTree (RB→bt A tree) (RB→bt A repl))
-     → (next : ℕ → A → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (tree1 : RBTree A k1 c1 d1 ) (repl1 : RBTree A k2 c2 d2 ) 
-         → (si1 : rbstackInvariant2 ? ? ? )
-         → (ri : rotatedTree (RB→bt A tree1) (RB→bt A repl1))
-         → rbsi-len si1 < rbsi-len si → t )
-     → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 : RBTree A k1 c1 d1 ) → (repl1 : RBTree A k2 c2 d2 ) 
-         → (ri : rotatedTree (RB→bt A orig) (RB→bt A repl1))
+     → (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 
+        → 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 {_} {key2} orig tree repl si ri next exit = insertCase1 key2 si where
-    insertCase4 : (key1 : ℕ) → (si : rbstackInvariant2 ? ? ? ) →  {k1 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) → 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 : rbstackInvariant2 ? ? ? ) →  {k1 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) → t
+    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 : rbstackInvariant2 ? ? ? ) →  {k1 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) → t
+    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 : rbstackInvariant2 ? ? ? )  → t
+    insertCase2 key1 si {_} {_} {_} {_} {Black} parent grand = next ? ? ? ?
+    insertCase1 : (key1 : ℕ)  (si : ParentGrand ? ? ? )  → t
     insertCase1 key1 = ?