Mercurial > hg > Gears > GearsAgda

changeset 723:43180a01bfbe

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 Mon, 10 Apr 2023 10:43:00 +0900
parents b088fa199d3d
children 35891ec243a0
files hoareBinaryTree1.agda
diffstat 1 files changed, 51 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sun Apr 09 17:15:42 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Apr 10 10:43:00 2023 +0900
@@ -550,23 +550,55 @@
     Red : Color
     Black : Color
 
-data rbInvariant {n : Level} {A : Set n} : bt A → Color → ℕ → Set n where
-    rb-leaf     : rbInvariant leaf Black 0
-    rb-single   : (key : ℕ) → (value : A) → (c : Color) →  rbInvariant (node key value leaf leaf) c 1
-    t-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → {d : ℕ } → rbInvariant (node key₁ value₁ t₁ t₂) Black d
-       → rbInvariant (node key value leaf (node key₁ value₁ t₁ t₂)) Red d
-    t-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → {c : Color} → {d : ℕ }→ rbInvariant (node key₁ value₁ t₁ t₂) c d
-       → rbInvariant (node key value leaf (node key₁ value₁ t₁ t₂)) Black (suc d)
-    t-left-red  : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → {d : ℕ} → rbInvariant (node key value t₁ t₂) Black d
-       → rbInvariant (node key₁ value₁ (node key value t₁ t₂) leaf ) Red d
-    t-left-black  : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → {c : Color} → {d : ℕ}  → rbInvariant (node key value t₁ t₂) c d
-       → rbInvariant (node key₁ value₁ (node key value t₁ t₂) leaf ) Black (suc d)
-    t-node-red  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} {d : ℕ}
-       → rbInvariant (node key value t₁ t₂) Black d
-       → rbInvariant (node key₂ value₂ t₃ t₄) Black d
-       → rbInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) Red d
-    t-node-black  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} {c c1 : Color} {d : ℕ}
-       → rbInvariant (node key value t₁ t₂) c d
-       → rbInvariant (node key₂ value₂ t₃ t₄) c1 d
-       → rbInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) Black (suc d)
+data RBTree {n : Level} (A : Set n) : (key : ℕ) → Color → (b-depth : ℕ) → Set n where
+    rb-leaf     : (key : ℕ) → RBTree A key Black 0
+    rb-single   : (key : ℕ) → (value : A) → (c : Color) →  RBTree A key c 1
+    t-right-red : {key key₁ : ℕ} → (value : A) → key < key₁ → {d : ℕ } → RBTree A key₁ Black d → RBTree A key Red d
+    t-right-black : {key key₁ : ℕ} → (value : A) → key < key₁ → {c : Color} → {d : ℕ }→ RBTree A key₁ c d
+       → RBTree A key Black (suc d)
+    t-left-red  : {key key₁ : ℕ} → (value : A) → key < key₁ → {d : ℕ} → RBTree A key Black d
+       → RBTree A key₁ Red d
+    t-left-black  : {key key₁ : ℕ} → (value : A) → key < key₁  → {c : Color} → {d : ℕ}  → RBTree A key  c d
+       → RBTree A key₁ Black (suc d)
+    t-node-red  : {key key₁ key₂ : ℕ} → (value : A) → key < key₁ → key₁ < key₂   →  {d : ℕ}
+       → RBTree A key Black d
+       → RBTree A key₂ Black d
+       → RBTree A key₁ Red d
+    t-node-black  : {key key₁ key₂ : ℕ} → (value : A) → key < key₁ → key₁ < key₂  →  {c c1 : Color} {d : ℕ}
+       → RBTree A key c d
+       → 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-single :  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
 
+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
+RB→bt {n} A (t-right-red {key} value x rb) = node key value leaf (RB→bt A rb)
+RB→bt {n} A (t-right-black {key} value x rb) = node key value leaf (RB→bt A rb)
+RB→bt {n} A (t-left-red {_} {key} value x rb) = node key value (RB→bt A rb) leaf
+RB→bt {n} A (t-left-black {_} {key} value x rb) = node key value (RB→bt A rb) leaf
+RB→bt {n} A (t-node-red {_} {key} value x x₁ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁) 
+RB→bt {n} A (t-node-black {_} {key} value x x₁ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁) 
+
+rbt-depth : ?
+rbt-depth = ?
+
+rbt-key : ?
+rbt-key = ?
+
+
+findRBP : {n m : Level} {A : Set n} {t : Set m} → (key key1 d d1 : ℕ) → (c : Color) → (tree : RBTree A key c d ) (tree1 : RBTree A key1 ? d1 ) 
+           →  rbstackInvariant tree key1
+           → (next : (key0 d0 : ℕ ) (tree1 : RBTree A key0 ? d0 ) → rbstackInvariant tree1 key0 → rbt-depth tree1 < rbt-depth tree   → t )
+           → (exit : (key0 d0 : ℕ) (tree0 : RBTree A key0 ? d0 ) → rbstackInvariant tree1 key0
+                 → (tree1 ≡ ? ) ∨ ( rbt-key tree1 ≡ just key )  → t ) → t
+findRBP = ?
+
+
+