Mercurial > hg > Gears > GearsAgda
annotate redBlackTreeTest.agda @ 540:6a4830c5a514
testing
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 11 Jan 2018 11:55:22 +0900 |
| parents | 39d465c20e5a |
| children | 429ece770187 |
| rev | line source |
|---|---|
| 537 | 1 module redBlackTreeTest where |
| 2 | |
| 3 open import RedBlackTree | |
| 4 open import stack | |
| 5 open import Level hiding (zero) | |
| 6 | |
| 7 open import Data.Nat | |
| 8 | |
| 9 open Tree | |
| 10 open Node | |
| 11 open RedBlackTree.RedBlackTree | |
| 12 open Stack | |
| 13 | |
| 14 -- tests | |
| 15 | |
| 16 putTree1 : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> a -> (RedBlackTree {n} {m} {t} a k si -> t) -> t | |
| 17 putTree1 {n} {m} {a} {k} {si} {t} tree k1 value next with (root tree) | |
| 18 ... | Nothing = next (record tree {root = Just (leafNode k1 value) }) | |
|
538
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
19 ... | Just n2 = clearStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> replaceNode tree1 s n1 next)) |
| 537 | 20 |
| 21 open import Relation.Binary.PropositionalEquality | |
| 22 open import Relation.Binary.Core | |
| 23 open import Function | |
| 24 | |
| 25 | |
| 26 check1 : {m : Level } (n : Maybe (Node ℕ ℕ)) -> ℕ -> Bool {m} | |
| 27 check1 Nothing _ = False | |
| 28 check1 (Just n) x with Data.Nat.compare (value n) x | |
| 29 ... | equal _ = True | |
| 30 ... | _ = False | |
| 31 | |
| 32 test1 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( \t -> getRedBlackTree t 1 ( \t x -> check1 x 1 ≡ True )) | |
| 33 test1 = refl | |
| 34 | |
| 35 test2 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( | |
| 36 \t -> putTree1 t 2 2 ( | |
| 37 \t -> getRedBlackTree t 1 ( | |
| 38 \t x -> check1 x 1 ≡ True ))) | |
| 39 test2 = refl | |
| 40 | |
|
538
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
41 test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 |
|
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
42 $ \t -> putTree1 t 2 2 |
|
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
43 $ \t -> getRedBlackTree t 2 |
|
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
44 $ \t x -> check1 x 2 ≡ True |
|
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
45 test3 = refl |
| 537 | 46 |
| 540 | 47 -- test4 : putTree1 {_} {_} {ℕ} {ℕ} ( createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ \t -> putTree1 t 2 2 $ \t -> |
| 48 -- root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} ) | |
| 49 -- test4 = refl | |
|
538
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
50 |
|
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
51 |
| 540 | 52 -- test5 : Maybe (Node ℕ ℕ) |
| 539 | 53 test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 |
| 54 $ \t -> putTree1 t 2 2 | |
| 540 | 55 -- $ \t -> putTree1 t 3 3 |
| 56 $ \t -> clearStack (nodeStack t) | |
| 57 $ \s -> findNode1 t s (leafNode 3 3) ( root t ) | |
| 58 $ \t1 s n1 -> replaceNode t1 s n1 | |
| 539 | 59 $ \t -> getRedBlackTree t 3 |
| 540 | 60 $ \t x -> SingleLinkedStack.top (stack s) |
| 61 -- $ \t x -> n1 | |
| 62 -- $ \t x -> root t1 | |
| 63 where | |
| 64 findNode1 : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> t) -> t | |
| 65 findNode1 t s n1 Nothing next = next t s n1 | |
| 66 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
|
67 |
|
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
68 -- 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
|
69 -- 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
|
70 -- test51 = refl |
| 539 | 71 |
| 72 test6 : Maybe (Node ℕ ℕ) | |
| 73 test6 = root (createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)}) | |
| 74 | |
| 75 | |
| 76 test7 : Maybe (Node ℕ ℕ) | |
| 77 test7 = clearStack (nodeStack tree2) (\ s -> replaceNode tree2 s n2 (\ t -> root t)) | |
| 78 where | |
| 79 tree2 = createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)} | |
| 80 k1 = 1 | |
| 81 n2 = leafNode 0 0 | |
| 82 value1 = 1 | |
| 83 | |
| 84 test8 : Maybe (Node ℕ ℕ) | |
| 85 test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 | |
| 86 $ \t -> putTree1 t 2 2 (\ t -> root t) |