Mercurial > hg > Members > Moririn
annotate redBlackTreeTest.agda @ 553:7d9af1d4b5af
add compareTri
| author | ryokka |
|---|---|
| date | Mon, 26 Mar 2018 17:50:04 +0900 |
| parents | 5f4c5a663219 |
| children | 988c12d7f887 |
| rev | line source |
|---|---|
| 537 | 1 module redBlackTreeTest where |
| 2 | |
| 3 open import RedBlackTree | |
| 4 open import stack | |
| 5 open import Level hiding (zero) | |
| 6 | |
| 553 | 7 open import Data.Empty |
| 8 | |
| 537 | 9 open import Data.Nat |
| 553 | 10 open import Relation.Nullary |
| 537 | 11 |
| 12 open Tree | |
| 13 open Node | |
| 14 open RedBlackTree.RedBlackTree | |
| 15 open Stack | |
| 16 | |
| 17 -- tests | |
| 18 | |
| 543 | 19 putTree1 : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t |
| 20 putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree) | |
| 537 | 21 ... | Nothing = next (record tree {root = Just (leafNode k1 value) }) |
| 543 | 22 ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> replaceNode tree1 s n1 next)) |
| 537 | 23 |
| 24 open import Relation.Binary.PropositionalEquality | |
| 25 open import Relation.Binary.Core | |
| 26 open import Function | |
| 27 | |
| 28 | |
| 29 check1 : {m : Level } (n : Maybe (Node ℕ ℕ)) -> ℕ -> Bool {m} | |
| 30 check1 Nothing _ = False | |
| 31 check1 (Just n) x with Data.Nat.compare (value n) x | |
| 32 ... | equal _ = True | |
| 33 ... | _ = False | |
| 34 | |
| 549 | 35 check2 : {m : Level } (n : Maybe (Node ℕ ℕ)) -> ℕ -> Bool {m} |
| 36 check2 Nothing _ = False | |
| 37 check2 (Just n) x with compare2 (value n) x | |
| 38 ... | EQ = True | |
| 39 ... | _ = False | |
| 40 | |
| 41 test1 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( \t -> getRedBlackTree t 1 ( \t x -> check2 x 1 ≡ True )) | |
| 537 | 42 test1 = refl |
| 43 | |
| 44 test2 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( | |
| 45 \t -> putTree1 t 2 2 ( | |
| 46 \t -> getRedBlackTree t 1 ( | |
| 549 | 47 \t x -> check2 x 1 ≡ True ))) |
| 537 | 48 test2 = refl |
| 49 | |
| 545 | 50 open ≡-Reasoning |
| 542 | 51 test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1 |
| 52 $ \t -> putTree1 t 2 2 | |
| 53 $ \t -> putTree1 t 3 3 | |
| 544 | 54 $ \t -> putTree1 t 4 4 |
| 545 | 55 $ \t -> getRedBlackTree t 1 |
| 549 | 56 $ \t x -> check2 x 1 ≡ True |
| 545 | 57 test3 = begin |
| 549 | 58 check2 (Just (record {key = 1 ; value = 1 ; color = Black ; left = Nothing ; right = Just (leafNode 2 2)})) 1 |
| 545 | 59 ≡⟨ refl ⟩ |
| 60 True | |
| 61 ∎ | |
| 542 | 62 |
| 63 test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 | |
| 64 $ \t -> putTree1 t 2 2 | |
| 65 $ \t -> putTree1 t 3 3 | |
| 66 $ \t -> putTree1 t 4 4 | |
| 544 | 67 $ \t -> getRedBlackTree t 4 |
| 68 $ \t x -> x | |
|
538
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
69 |
| 540 | 70 -- test5 : Maybe (Node ℕ ℕ) |
| 541 | 71 test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4 |
| 72 $ \t -> putTree1 t 6 6 | |
| 543 | 73 $ \t0 -> clearSingleLinkedStack (nodeStack t0) |
| 541 | 74 $ \s -> findNode1 t0 s (leafNode 3 3) ( root t0 ) |
| 540 | 75 $ \t1 s n1 -> replaceNode t1 s n1 |
| 539 | 76 $ \t -> getRedBlackTree t 3 |
| 541 | 77 -- $ \t x -> SingleLinkedStack.top (stack s) |
| 540 | 78 -- $ \t x -> n1 |
| 541 | 79 $ \t x -> root t |
| 540 | 80 where |
| 543 | 81 findNode1 : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> t) -> t |
| 540 | 82 findNode1 t s n1 Nothing next = next t s n1 |
| 83 findNode1 t s n1 ( Just n2 ) next = findNode t s n1 n2 next | |
|
538
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
84 |
|
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
85 -- test51 : putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ \t -> |
|
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
86 -- putTree1 t 2 2 $ \t -> putTree1 t 3 3 $ \t -> root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} ) |
|
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
87 -- test51 = refl |
| 539 | 88 |
| 89 test6 : Maybe (Node ℕ ℕ) | |
| 90 test6 = root (createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)}) | |
| 91 | |
| 92 | |
| 93 test7 : Maybe (Node ℕ ℕ) | |
| 543 | 94 test7 = clearSingleLinkedStack (nodeStack tree2) (\ s -> replaceNode tree2 s n2 (\ t -> root t)) |
| 539 | 95 where |
| 96 tree2 = createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)} | |
| 97 k1 = 1 | |
| 98 n2 = leafNode 0 0 | |
| 99 value1 = 1 | |
| 100 | |
| 101 test8 : Maybe (Node ℕ ℕ) | |
| 102 test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 | |
| 103 $ \t -> putTree1 t 2 2 (\ t -> root t) | |
| 544 | 104 |
| 105 | |
| 549 | 106 test9 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( \t -> getRedBlackTree t 1 ( \t x -> check2 x 1 ≡ True )) |
| 544 | 107 test9 = refl |
| 108 | |
| 109 test10 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( | |
| 110 \t -> putRedBlackTree t 2 2 ( | |
| 111 \t -> getRedBlackTree t 1 ( | |
| 549 | 112 \t x -> check2 x 1 ≡ True ))) |
| 544 | 113 test10 = refl |
| 114 | |
| 115 test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 | |
| 116 $ \t -> putRedBlackTree t 2 2 | |
| 117 $ \t -> putRedBlackTree t 3 3 | |
| 118 $ \t -> getRedBlackTree t 2 | |
| 119 $ \t x -> root t | |
| 545 | 120 |
| 121 | |
| 122 redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ | |
| 549 | 123 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 } |
| 545 | 124 |
| 549 | 125 -- compare2 : (x y : ℕ ) -> CompareResult {Level.zero} |
| 126 -- compare2 zero zero = EQ | |
| 127 -- compare2 (suc _) zero = GT | |
| 128 -- compare2 zero (suc _) = LT | |
| 129 -- compare2 (suc x) (suc y) = compare2 x y | |
| 546 | 130 |
| 553 | 131 compareTri1 : (n : ℕ) -> zero < ℕ.suc n |
| 132 compareTri1 zero = {!!} | |
| 133 compareTri1 (suc n) = {!!} | |
| 134 | |
| 135 compareTri : Trichotomous _≡_ _<_ | |
| 136 compareTri zero zero = tri≈ (\()) refl (\()) | |
| 137 compareTri zero (suc n) = tri< {!!} (\()) (\()) | |
| 138 compareTri (suc n) zero = tri> (\()) (\()) {!!} | |
| 139 compareTri (suc n) (suc m) with compareTri n m | |
| 140 ... | tri≈ p q r = tri≈ {!!} (cong (\x -> ℕ.suc x) q) {!!} | |
| 141 ... | tri< p q r = tri< {!!} {!!} {!!} | |
| 142 ... | tri> p q r = tri> {!!} {!!} {!!} | |
| 143 | |
| 144 compareDecTest : (n n1 : Node ℕ ℕ) -> key n ≡ key n1 | |
| 145 compareDecTest n n1 with (key n) ≟ (key n1) | |
| 146 ... | yes p = p | |
| 147 ... | no ¬p = {!!} | |
| 148 | |
| 149 | |
| 150 | |
| 548 | 151 putTest1Lemma2 : (k : ℕ) -> compare2 k k ≡ EQ |
| 152 putTest1Lemma2 zero = refl | |
| 153 putTest1Lemma2 (suc k) = putTest1Lemma2 k | |
| 546 | 154 |
| 548 | 155 putTest1Lemma1 : (x y : ℕ) -> compareℕ x y ≡ compare2 x y |
| 156 putTest1Lemma1 zero zero = refl | |
| 157 putTest1Lemma1 (suc m) zero = refl | |
| 158 putTest1Lemma1 zero (suc n) = refl | |
| 159 putTest1Lemma1 (suc m) (suc n) with Data.Nat.compare m n | |
| 160 putTest1Lemma1 (suc .m) (suc .(Data.Nat.suc m + k)) | less m k = lemma1 m | |
| 161 where | |
| 162 lemma1 : (m : ℕ) -> LT ≡ compare2 m (ℕ.suc (m + k)) | |
| 163 lemma1 zero = refl | |
| 164 lemma1 (suc y) = lemma1 y | |
| 165 putTest1Lemma1 (suc .m) (suc .m) | equal m = lemma1 m | |
| 166 where | |
| 167 lemma1 : (m : ℕ) -> EQ ≡ compare2 m m | |
| 168 lemma1 zero = refl | |
| 169 lemma1 (suc y) = lemma1 y | |
| 170 putTest1Lemma1 (suc .(Data.Nat.suc m + k)) (suc .m) | greater m k = lemma1 m | |
| 171 where | |
| 172 lemma1 : (m : ℕ) -> GT ≡ compare2 (ℕ.suc (m + k)) m | |
| 173 lemma1 zero = refl | |
| 174 lemma1 (suc y) = lemma1 y | |
| 175 | |
| 176 putTest1Lemma3 : (k : ℕ) -> compareℕ k k ≡ EQ | |
| 177 putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k ) | |
| 546 | 178 |
| 551 | 179 compareLemma1 : {x y : ℕ} -> compare2 x y ≡ EQ -> x ≡ y |
| 180 compareLemma1 {zero} {zero} refl = refl | |
| 181 compareLemma1 {zero} {suc _} () | |
| 182 compareLemma1 {suc _} {zero} () | |
| 183 compareLemma1 {suc x} {suc y} eq = cong ( \z -> ℕ.suc z ) ( compareLemma1 ( trans lemma2 eq ) ) | |
|
550
2476f7123dc3
root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
549
diff
changeset
|
184 where |
|
2476f7123dc3
root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
549
diff
changeset
|
185 lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y |
|
2476f7123dc3
root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
549
diff
changeset
|
186 lemma2 = refl |
| 549 | 187 |
| 546 | 188 |
| 545 | 189 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ)) |
| 190 -> (k : ℕ) (x : ℕ) | |
| 191 -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x | |
| 549 | 192 (\ t -> getRedBlackTree t k (\ t x1 -> check2 x1 x ≡ True)) |
| 546 | 193 putTest1 n k x with n |
| 552 | 194 ... | Just n1 = lemma2 ( record { top = Nothing } ) |
| 551 | 195 where |
| 552 | 196 lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) -> putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t → |
| 551 | 197 GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t)) |
| 552 | 198 lemma2 s with compare2 k (key n1) |
| 553 | 199 ... | EQ = lemma3 {!!} |
| 551 | 200 where |
| 552 | 201 lemma3 : compare2 k (key n1) ≡ EQ -> getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { |
| 551 | 202 key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black |
| 552 | 203 } ) ; nodeStack = s ; compare = λ x₁ y → compare2 x₁ y } ) k ( \ t x1 -> check2 x1 x ≡ True) |
| 204 lemma3 eq with compare2 x x | putTest1Lemma2 x | |
| 205 ... | EQ | refl with compare2 k (key n1) | eq | |
| 206 ... | EQ | refl with compare2 x x | putTest1Lemma2 x | |
| 207 ... | EQ | refl = refl | |
| 551 | 208 ... | GT = {!!} |
| 209 ... | LT = {!!} | |
| 549 | 210 ... | Nothing = lemma1 |
| 211 where | |
| 212 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { | |
| 213 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red | |
| 214 } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y } ) k | |
| 215 ( \ t x1 -> check2 x1 x ≡ True) | |
|
550
2476f7123dc3
root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
549
diff
changeset
|
216 lemma1 with compare2 k k | putTest1Lemma2 k |
|
2476f7123dc3
root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
549
diff
changeset
|
217 ... | EQ | refl with compare2 x x | putTest1Lemma2 x |
|
2476f7123dc3
root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
549
diff
changeset
|
218 ... | EQ | refl = refl |