Mercurial > hg > Members > Moririn

changeset 727:fd63d70310c3

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 19:12:50 +0900
parents e545646e5f64
children 0786c97b4919
files hoareBinaryTree1.agda
diffstat 1 files changed, 14 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Apr 10 17:57:26 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Apr 10 19:12:50 2023 +0900
@@ -1,6 +1,6 @@
 module hoareBinaryTree1 where
 
-open import Level renaming (zero to Z ; suc to succ)
+open import Level hiding (suc ; zero ; _⊔_ )
 
 open import Data.Nat hiding (compare)
 open import Data.Nat.Properties as NatProp
@@ -37,7 +37,7 @@
 
 bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ
 bt-depth leaf = 0
-bt-depth (node key value t t₁) = suc (Data.Nat._⊔_ (bt-depth t ) (bt-depth t₁ ))
+bt-depth (node key value t t₁) = suc (bt-depth t  ⊔ bt-depth t₁ )
 
 open import Data.Unit hiding ( _≟_ ;  _≤?_ ; _≤_)
 
@@ -528,7 +528,7 @@
 insertTestP1 = insertTreeP leaf 1 1 t-leaf
   $ λ _ x0 P0 → insertTreeP x0 2 1 (proj1 P0) 
   $ λ _ x1 P1 → insertTreeP x1 3 2 (proj1 P1)  
-  $ λ _ x2 P2 → insertTreeP x2 2 2 (proj1 P2) (λ _ x _  → x )
+  $ λ _ x2 P2 → insertTreeP x2 2 2 (proj1 P2) (λ _ x P  → x )
 
 top-value : {n : Level} {A : Set n} → (tree : bt A) →  Maybe A 
 top-value leaf = nothing
@@ -608,10 +608,17 @@
 
 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 key0 → rbt-depth A tree0 < rbt-depth A tree1   → t )
-           → (exit : {key0 d0 : ℕ} {c0 : Color} → (tree0 : RBTree A key0 c0 d0 ) → rbstackInvariant tree key0
-                 → (rbt-depth A tree0 ≡ 0 ) ∨ ( rbt-key A tree0 ≡ just key )  → t ) → t
-findRBP = ?
+           → (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
+                 → (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 = ?
 
 record ReplaceRBT {n : Level} {A : Set n} (key : ℕ) (value : A) {key1 key2 d1 d2 : ℕ} {c1 c2 : Color}
      (tree : RBTree A key1 c1 d1) (repl : RBTree A key2 c2 d2)   : Set n where