Mercurial > hg > Gears > GearsAgda

changeset 808:5d15ec862bcb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add findRBTreeTest
author Moririn
date Sat, 20 Jan 2024 20:14:15 +0900
parents 858655384dea
children 243faca58e90
files hoareBinaryTree1.agda
diffstat 1 files changed, 48 insertions(+), 27 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sat Jan 20 20:01:01 2024 +0900
+++ b/hoareBinaryTree1.agda	Sat Jan 20 20:14:15 2024 +0900
@@ -668,23 +668,20 @@
 
 findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) )
            → (stack : List (bt (Color ∧ A)))
-           → treeInvariant tree ∧  stackInvariant key tree tree0 stack
-           → RBtreeInvariant tree
+           → RBtreeInvariant tree ∧  stackInvariant key tree tree0 stack
            → (next : (tree1 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A)))
-                   → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
-                   → RBtreeInvariant tree1
+                   → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
                    → bt-depth tree1 < bt-depth tree → t )
            → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A)))
-                 → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
-                 → RBtreeInvariant tree1
+                 → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
                  → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
-findRBT key leaf tree0 stack ti rb0 next exit = exit leaf stack ti rb0 (case1 refl)
-findRBT key n@(node key₁ value left right) tree0 stack ti  rb0 next exit with <-cmp key key₁
-findRBT key (node key₁ value left right) tree0 stack ti rb0 next exit | tri< a ¬b ¬c
- = next left (left ∷ stack) ⟪ treeLeftDown left right (_∧_.proj1 ti) , s-left _ _ _ a (_∧_.proj2 ti) ⟫ (RBtreeLeftDown left right rb0) depth-1<
-findRBT key n tree0 stack ti rb0 _ exit | tri≈ ¬a refl ¬c = exit n stack ti rb0 (case2 refl)
-findRBT key (node key₁ value left right) tree0 stack ti rb0 next exit | tri> ¬a ¬b c
- = next right (right ∷ stack) ⟪ treeRightDown left right (_∧_.proj1 ti), s-right _ _ _ c (_∧_.proj2 ti) ⟫ (RBtreeRightDown left right rb0) depth-2<
+findRBT key leaf tree0 stack rb0 next exit = exit leaf stack rb0 (case1 refl)
+findRBT key (node key₁ value left right) tree0 stack rb0 next exit with <-cmp key key₁
+findRBT key (node key₁ value left right) tree0 stack  rb0 next exit | tri< a ¬b ¬c
+ = next left (left ∷ stack) ⟪ RBtreeLeftDown left right (_∧_.proj1 rb0) , s-left _ _ _ a (_∧_.proj2 rb0) ⟫  depth-1<
+findRBT key n tree0 stack  rb0 _ exit | tri≈ ¬a refl ¬c = exit n stack rb0 (case2 refl)
+findRBT key (node key₁ value left right) tree0 stack  rb0 next exit | tri> ¬a ¬b c
+ = next right (right ∷ stack) ⟪ RBtreeRightDown left right (_∧_.proj1 rb0), s-right _ _ _ c (_∧_.proj2 rb0) ⟫ depth-2<
 
 
 blackdepth≡ : {n : Level } {A : Set n} → {C : Color} {key key1 : ℕ} {value value1 : A} → (tree1 tree2 : bt (Color ∧ A))
@@ -700,6 +697,42 @@
 blackdepth≡ (node key .(⟪ Black , _ ⟫) t1 t3) (node key₁ .(⟪ Black , _ ⟫) t2 t4) ri1 ri2 (rb-node-red x x₁ x₂ rip rip₁) = DepthCal (black-depth  (node key ⟪ Black , _ ⟫ t1 t3)) (black-depth (node key₁ ⟪ Black , _ ⟫ t2 t4)) 0
 blackdepth≡ (node key .(⟪ _ , _ ⟫) t1 t3) (node key₁ .(⟪ _ , _ ⟫) t2 t4) ri1 ri2 (rb-node-black x x₁ x₂ rip rip₁) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) ( black-depth (node key₁ ⟪ _ , _ ⟫ t2 t4))  (black-depth (node key₁ (⟪ _ , _ ⟫) t2 t4))
 
+
+findTest : {n m : Level} {A : Set n } {t : Set m }
+ → (key : ℕ)
+ → (tree0 : bt (Color ∧ A))
+ → RBtreeInvariant tree0
+ → (exit : (tree1 : bt (Color ∧ A))
+   → (stack : List (bt (Color ∧ A)))
+   → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
+   → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
+findTest {n} {m} {A} {t} k tr0 rb0 exit = TerminatingLoopS (bt (Color ∧ A) ∧ List (bt (Color ∧ A)))
+ {λ p → RBtreeInvariant (proj1 p) ∧ stackInvariant k (proj1 p) tr0 (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tr0 , tr0 ∷ [] ⟫ ⟪ rb0 , s-nil ⟫
+       $ λ p RBP loop → findRBT k (proj1 p) tr0 (proj2 p) RBP  (λ t1 s1 P2 lt1 → loop ⟪ t1 ,  s1  ⟫ P2 lt1 )
+       $ λ tr1 st P2 O → exit tr1 st P2 O
+
+
+testRBTree0 :  bt (Color ∧ ℕ)
+testRBTree0 = node 8 ⟪ Black , 800 ⟫ (node 5 ⟪ Red , 500 ⟫ (node 2 ⟪ Black , 200 ⟫ leaf leaf) (node 6 ⟪ Black , 600 ⟫ leaf leaf)) (node 10 ⟪ Red , 1000 ⟫ (leaf) (node 15 ⟪ Black , 1500 ⟫ (node 14 ⟪ Red , 1400 ⟫ leaf leaf) leaf))
+
+record result {n : Level} {A : Set n} {key : ℕ} {tree0 : bt (Color ∧ A)} : Set n where
+   field
+     tree : bt (Color ∧ A)
+     stack : List (bt (Color ∧ A))
+     ti : RBtreeInvariant tree
+     si : stackInvariant key tree tree0 stack
+
+testRBI0 : RBtreeInvariant testRBTree0
+testRBI0 = rb-node-black (add< 2) (add< 1) refl (rb-node-red (add< 2) (add< 0) refl (rb-single 2 200) (rb-single 6 600)) (rb-right-red (add< 4) refl (rb-left-black (add< 0) refl (rb-single 14 1400) ))
+
+findRBTreeTest : result
+findRBTreeTest = findTest 14 testRBTree0 testRBI0
+       $ λ tr s P O → (record {tree = tr ; stack = s ; ti = (proj1 P) ; si = (proj2 P)})
+
+
+
+
+
 data replacedRBTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt (Color ∧ A) ) → Set n where
     rbr-leaf : {ca cb : Color} → replacedRBTree key value leaf (node key ⟪ cb , value ⟫ leaf leaf)
     rbr-node : {value₁ : A} → {ca cb : Color } → {t t₁ : bt (Color ∧ A)} → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ cb , value ⟫ t t₁)
@@ -718,7 +751,7 @@
     s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
         → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand
 
-
+{-
 record PG {n : Level } (A : Set n) (self : bt A) (stack : List (bt A)) : Set n where
     field
        parent grand uncle : bt A
@@ -788,18 +821,6 @@
 ... | tri≈ ¬a b ¬c = rbi
 ... | tri> ¬a ¬b c = RBtreeRightDown _ _ rbi
 
--- findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) )
---           → (stack : List (bt (Color ∧ A)))           → treeInvariant tree0 ∧  stackInvariant key tree tree0 stack
---           → {d : ℕ} →  RBtreeInvariant tree0
---           → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A)))
---                 → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
---                 → {d1 : ℕ} → RBtreeInvariant tree1
---                 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
---findRBT {_} {_} {A} {t} key tree0 leaf stack ti {d} rb0 exit = {!!}
---findRBT {_} {_} {A} {t} key tree0 (node key₁ value left right) stack ti {d} rb0 exit with <-cmp key key₁
---... | tri< a ¬b ¬c = {!!}
---... | tri≈ ¬a b ¬c = {!!}
---... | tri> ¬a ¬b c = {!!}
 
 rotateLeft : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A)
@@ -1006,6 +1027,6 @@
            --     b   b → r RBI.tree r             r = orig   o (r/b)
     ... | case2 (case2 pg) = {!!} -- insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)
 
+-}
 
 
-