Mercurial > hg > Gears > GearsAgda

changeset 734:9d5e749531b1

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 Fri, 21 Apr 2023 10:36:49 +0900
parents 737c5f95e5b3
children 7901892bb1d8
files hoareBinaryTree1.agda
diffstat 1 files changed, 36 insertions(+), 43 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Thu Apr 13 16:13:42 2023 +0900
+++ b/hoareBinaryTree1.agda	Fri Apr 21 10:36:49 2023 +0900
@@ -563,24 +563,6 @@
        → RBTree A key₂ c1 d
        → RBTree A key₁ Black (suc d)
 
-data rbstackInvariant {n : Level} {A : Set n}  {key : ℕ} {c : Color} {d : ℕ} (orig : RBTree A key c d ) : (key₁ : ℕ ) → Set n where
-    s-nil :  rbstackInvariant orig key
-    s-right :  {key₁ key₂ : ℕ} → {c1 : Color} {d1 : ℕ} → key₁ < key₂  →  (top : RBTree A key₁ c1 d1) 
-        → rbstackInvariant orig key₁ → rbstackInvariant orig key
-    s-left :   {key₁ key₂ : ℕ} → {c1 : Color} {d1 : ℕ} → key₂ < key₁  →  (top : RBTree A key₁ c1 d1) 
-        → rbstackInvariant orig key₁ → rbstackInvariant orig key
-
-data rbstackInvariant2 {n : Level} {A : Set n}  {key : ℕ} {c : Color} {d : ℕ} (orig : RBTree A key c d ) : 
-        {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (parent : RBTree A k1 c1 d1) (grand : RBTree A k2 c2 d2) Set n where
-    s-head :  rbstackInvariant2 orig ? orig
-    s-right : rbstackInvariant2 orig ? ? → rbstackInvariant2 orig ? ?
-
-rbsi-len :  {n : Level} {A : Set n}  {key : ℕ} {c : Color} {d : ℕ} (orig : RBTree A key c d ) {key₁ : ℕ } 
-     → rbstackInvariant orig key₁ → ℕ
-rbsi-len orig s-nil = 0
-rbsi-len orig (s-right x top ri) = suc (rbsi-len orig ri)
-rbsi-len orig (s-left x top ri)  = suc (rbsi-len orig ri)
-
 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
@@ -611,10 +593,27 @@
 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}  {key : ℕ} {c : Color} {d : ℕ} (orig : RBTree A key c d ) : 
+        {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (parent : RBTree A k1 c1 d1) (grand : RBTree A k2 c2 d2) → Set n where
+    s-head :  rbstackInvariant2 orig ? orig
+    s-right : rbstackInvariant2 orig ? ? → rbstackInvariant2 orig ? ?
+
+data replacedTreeRotate  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt A ) → Set n where
+    r-leaf : replacedTreeRotate key value leaf (node key value leaf leaf)
+    r-node : {value₁ : A} → {t t₁ : bt A} → replacedTreeRotate key value (node key value₁ t t₁) (node key value t t₁) 
+    r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
+          → k < key →  replacedTreeRotate key value t2 t →  replacedTreeRotate key value (node k v1 t1 t2) (node k v1 t1 t) 
+    r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
+          → key < k →  replacedTreeRotate key value t1 t →  replacedTreeRotate key value (node k v1 t1 t2) (node k v1 t t2) 
+
+rbsi-len :  {n : Level} {A : Set n}  {key : ℕ} {c : Color} {d : ℕ} (orig : RBTree A key c d ) {key₁ : ℕ } 
+     → rbstackInvariant2 ? ? ? → ℕ
+rbsi-len orig = ?
+
 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 ) 
-           →  rbstackInvariant tree key1
-           → (next : {key0 d0 : ℕ} {c0 : Color} → (tree0 : RBTree A key0 c0 d0 ) → rbstackInvariant tree key1 → rbt-depth A tree0 < rbt-depth A tree1   → t )
-           → (exit : {key0 d0 : ℕ} {c0 : Color} → (tree0 : RBTree A key0 c0 d0 ) → rbstackInvariant tree key1
+           →  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 = ?
@@ -634,46 +633,40 @@
 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 : rbstackInvariant orig key1)
-     → (ri : replacedTree key value (RB→bt A tree) (RB→bt A repl))
+     → (si : rbstackInvariant2 ? ? ?)
+     → (ri : replacedTreeRotate key value (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 : rbstackInvariant orig k1)
-         → (ri : replacedTree key value (RB→bt A tree1) (RB→bt A repl1))
+         → (si1 : rbstackInvariant2 ? ? ?)
+         → (ri : replacedTreeRotate key value (RB→bt A tree1) (RB→bt A repl1))
          → rbsi-len orig si1 < rbsi-len orig si → t )
      → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 : RBTree A k1 c1 d1 ) → (repl1 : RBTree A k2 c2 d2 ) 
-         → (ri : replacedTree key value (RB→bt A orig) (RB→bt A repl1))
+         → (ri : replacedTreeRotate key value (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 : rbstackInvariant orig key1)  → t
+    insertCase51 : (key1 : ℕ)  (si : rbstackInvariant2 ? ? ? )  → 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 : rbstackInvariant orig key1)
-     → (ri : replacedTree key value (RB→bt A tree) (RB→bt A repl))
+     → (si : rbstackInvariant2 ? ? ? )
+     → (ri : replacedTreeRotate key value (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 : rbstackInvariant orig k1)
-         → (ri : replacedTree key value (RB→bt A tree1) (RB→bt A repl1))
+         → (si1 : rbstackInvariant2 ? ? ? )
+         → (ri : replacedTreeRotate key value (RB→bt A tree1) (RB→bt A repl1))
          → rbsi-len orig si1 < rbsi-len orig si → t )
      → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 : RBTree A k1 c1 d1 ) → (repl1 : RBTree A k2 c2 d2 ) 
-         → (ri : replacedTree key value (RB→bt A orig) (RB→bt A repl1))
+         → (ri : replacedTreeRotate key value (RB→bt A orig) (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 : rbstackInvariant orig key1) →  {k1 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) → t
+    insertCase4 : (key1 : ℕ) → (si : rbstackInvariant2 ? ? ? ) →  {k1 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) → t
     insertCase4 = ?
-    insertCase3 : (key1 : ℕ) → (si : rbstackInvariant orig key1) →  {k1 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) → t
+    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 parent grandparent = ?
-    insertCase2 : (key1 : ℕ) → (si : rbstackInvariant orig key1) →  {k1 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) → t
+    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 {_} {_} {_} {_} {Red} parent grand = insertCase3 key1 si parent grand
     insertCase2 key1 si {_} {_} {_} {_} {Black} parent grand = next ? ? ? ? ? ? ?
-    insertCase1 : (key1 : ℕ)  (si : rbstackInvariant orig key1)  → t
-    insertCase1 key1 s-nil = exit ? ? ?
-    insertCase1 key1 (s-right {key₁} {key₂} x top s-nil) = exit ? ? ?
-    insertCase1 key1 (s-right {key₁} {key₂} x top (s-right {key₃} {key₄} x₁ top₁ si)) = insertCase2 key₃ si ? top₁ 
-    insertCase1 key1 (s-right {key₁} {key₂} x top (s-left {key₃} {key₄} x₁ top₁ si)) = insertCase2 key₃ si top top₁ 
-    insertCase1 key1 (s-left {key₁} {key₂} x top s-nil) = exit ? ? ?
-    insertCase1 key1 (s-left {key₁} {key₂} x top (s-right {key₃} {key₄} x₁ top₁ si)) = insertCase2 key₃ si top top₁ 
-    insertCase1 key1 (s-left {key₁} {key₂} x top (s-left {key₃} {key₄} x₁ top₁ si)) = insertCase2 key₃ si top top₁ 
+    insertCase1 : (key1 : ℕ)  (si : rbstackInvariant2 ? ? ? )  → t
+    insertCase1 key1 = ?