Mercurial > hg > Gears > GearsAgda
annotate redBlackTreeTest.agda @ 571:1eccf1f18a59
add more detail
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 27 Apr 2018 19:19:40 +0900 |
| parents | a6aa2ff5fea4 |
| children | eb75d9971451 |
| rev | line source |
|---|---|
| 537 | 1 module redBlackTreeTest where |
| 2 | |
| 3 open import RedBlackTree | |
| 4 open import stack | |
|
554
988c12d7f887
use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
553
diff
changeset
|
5 open import Level hiding (zero) renaming ( suc to succ ) |
| 537 | 6 |
| 553 | 7 open import Data.Empty |
| 8 | |
| 537 | 9 open import Data.Nat |
| 553 | 10 open import Relation.Nullary |
| 537 | 11 |
|
564
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
12 |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
13 open import Algebra |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
14 open import Data.Nat.Properties as NatProp |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
15 |
| 537 | 16 open Tree |
| 17 open Node | |
| 18 open RedBlackTree.RedBlackTree | |
| 19 open Stack | |
| 20 | |
| 21 -- tests | |
| 22 | |
| 562 | 23 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 |
| 543 | 24 putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree) |
| 537 | 25 ... | Nothing = next (record tree {root = Just (leafNode k1 value) }) |
| 562 | 26 ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (λ s → findNode tree s (leafNode k1 value) n2 (λ tree1 s n1 → replaceNode tree1 s n1 next)) |
| 537 | 27 |
| 28 open import Relation.Binary.PropositionalEquality | |
| 29 open import Relation.Binary.Core | |
| 30 open import Function | |
| 31 | |
| 32 | |
| 562 | 33 check1 : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool {m} |
| 537 | 34 check1 Nothing _ = False |
| 35 check1 (Just n) x with Data.Nat.compare (value n) x | |
| 36 ... | equal _ = True | |
| 37 ... | _ = False | |
| 38 | |
| 562 | 39 check2 : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool {m} |
| 549 | 40 check2 Nothing _ = False |
| 41 check2 (Just n) x with compare2 (value n) x | |
| 42 ... | EQ = True | |
| 43 ... | _ = False | |
| 44 | |
| 562 | 45 test1 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 x 1 ≡ True )) |
| 537 | 46 test1 = refl |
| 47 | |
| 48 test2 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( | |
| 562 | 49 λ t → putTree1 t 2 2 ( |
| 50 λ t → getRedBlackTree t 1 ( | |
| 51 λ t x → check2 x 1 ≡ True ))) | |
| 537 | 52 test2 = refl |
| 53 | |
| 545 | 54 open ≡-Reasoning |
| 542 | 55 test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1 |
| 562 | 56 $ λ t → putTree1 t 2 2 |
| 57 $ λ t → putTree1 t 3 3 | |
| 58 $ λ t → putTree1 t 4 4 | |
| 59 $ λ t → getRedBlackTree t 1 | |
| 60 $ λ t x → check2 x 1 ≡ True | |
| 545 | 61 test3 = begin |
| 549 | 62 check2 (Just (record {key = 1 ; value = 1 ; color = Black ; left = Nothing ; right = Just (leafNode 2 2)})) 1 |
| 545 | 63 ≡⟨ refl ⟩ |
| 64 True | |
| 65 ∎ | |
| 542 | 66 |
| 67 test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 | |
| 562 | 68 $ λ t → putTree1 t 2 2 |
| 69 $ λ t → putTree1 t 3 3 | |
| 70 $ λ t → putTree1 t 4 4 | |
| 71 $ λ t → getRedBlackTree t 4 | |
| 72 $ λ t x → x | |
|
538
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
73 |
| 540 | 74 -- test5 : Maybe (Node ℕ ℕ) |
| 541 | 75 test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4 |
| 562 | 76 $ λ t → putTree1 t 6 6 |
| 77 $ λ t0 → clearSingleLinkedStack (nodeStack t0) | |
| 78 $ λ s → findNode1 t0 s (leafNode 3 3) ( root t0 ) | |
| 79 $ λ t1 s n1 → replaceNode t1 s n1 | |
| 80 $ λ t → getRedBlackTree t 3 | |
| 81 -- $ λ t x → SingleLinkedStack.top (stack s) | |
| 82 -- $ λ t x → n1 | |
| 83 $ λ t x → root t | |
| 540 | 84 where |
| 562 | 85 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 | 86 findNode1 t s n1 Nothing next = next t s n1 |
| 87 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
|
88 |
| 562 | 89 -- test51 : putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ λ t → |
| 90 -- 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} ) | |
|
538
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
91 -- test51 = refl |
| 539 | 92 |
| 93 test6 : Maybe (Node ℕ ℕ) | |
| 94 test6 = root (createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)}) | |
| 95 | |
| 96 | |
| 97 test7 : Maybe (Node ℕ ℕ) | |
| 562 | 98 test7 = clearSingleLinkedStack (nodeStack tree2) (λ s → replaceNode tree2 s n2 (λ t → root t)) |
| 539 | 99 where |
| 100 tree2 = createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)} | |
| 101 k1 = 1 | |
| 102 n2 = leafNode 0 0 | |
| 103 value1 = 1 | |
| 104 | |
| 105 test8 : Maybe (Node ℕ ℕ) | |
| 106 test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 | |
| 562 | 107 $ λ t → putTree1 t 2 2 (λ t → root t) |
| 544 | 108 |
| 109 | |
| 562 | 110 test9 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 x 1 ≡ True )) |
| 544 | 111 test9 = refl |
| 112 | |
| 113 test10 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( | |
| 562 | 114 λ t → putRedBlackTree t 2 2 ( |
| 115 λ t → getRedBlackTree t 1 ( | |
| 116 λ t x → check2 x 1 ≡ True ))) | |
| 544 | 117 test10 = refl |
| 118 | |
| 119 test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 | |
| 562 | 120 $ λ t → putRedBlackTree t 2 2 |
| 121 $ λ t → putRedBlackTree t 3 3 | |
| 122 $ λ t → getRedBlackTree t 2 | |
| 123 $ λ t x → root t | |
| 545 | 124 |
| 125 | |
| 562 | 126 redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} → RedBlackTree {Level.zero} {m} {t} a ℕ |
|
564
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
127 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compareT } |
| 545 | 128 |
|
564
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
129 |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
130 compTri : ( x y : ℕ ) -> Tri (x < y) ( x ≡ y ) ( x > y ) |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
131 compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder) |
| 565 | 132 where open import Relation.Binary |
|
564
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
133 |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
134 checkT : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool {m} |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
135 checkT Nothing _ = False |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
136 checkT (Just n) x with compTri (value n) x |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
137 ... | tri≈ _ _ _ = True |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
138 ... | _ = False |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
139 |
| 565 | 140 checkEQ : {m : Level } ( x : ℕ ) -> ( n : Node ℕ ℕ ) -> (value n ) ≡ x -> checkT {m} (Just n) x ≡ True |
| 141 checkEQ x n refl with compTri (value n) x | |
| 566 | 142 ... | tri≈ _ refl _ = refl |
| 143 ... | tri> _ neq gt = ⊥-elim (neq refl) | |
| 144 ... | tri< lt neq _ = ⊥-elim (neq refl) | |
| 565 | 145 |
| 566 | 146 checkEQ' : {m : Level } ( x y : ℕ ) -> ( eq : x ≡ y ) -> ( x ≟ y ) ≡ yes eq |
| 570 | 147 checkEQ' x y refl with x ≟ y |
| 566 | 148 ... | yes refl = refl |
| 149 ... | no neq = ⊥-elim ( neq refl ) | |
| 546 | 150 |
| 571 | 151 --- search -> checkEQ |
| 152 --- findNode -> search | |
| 153 | |
| 545 | 154 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ)) |
| 570 | 155 → (k : ℕ) (x : ℕ) |
| 562 | 156 → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x |
| 570 | 157 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True)) |
| 546 | 158 putTest1 n k x with n |
| 570 | 159 ... | Just n1 = lemma0 |
| 551 | 160 where |
| 570 | 161 tree0 : (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ |
| 162 tree0 s = record { root = Just n1 ; nodeStack = s ; compare = compareT } | |
| 163 lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → findNode (tree0 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1 | |
| 164 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True))) | |
|
564
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
165 lemma2 s with compTri k (key n1) |
| 571 | 166 ... | tri≈ le refl gt = lemma5 s |
| 551 | 167 where |
| 571 | 168 open stack.SingleLinkedStack |
| 169 open stack.Element | |
| 170 lemma6 : (s : SingleLinkedStack (Node ℕ ℕ) ) → (n2 : Element (Node ℕ ℕ) ) | |
| 171 → ReplaceNode.replaceNode1 (tree0 s) s (record n1 { key = k ; value = x } ) (λ t → | |
| 172 GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t)) | |
| 173 (record { top = Element.next n2 }) (Just (Element.datum n2)) | |
| 174 lemma6 s n2 with (top s ) | |
| 175 ... | Just n3 with compTri (key (datum n2)) (key (datum n3)) | |
| 176 ... | tri< _ neq _ = {!!} -- lemma6 ( record {top = next n3} ) {!!} | |
| 177 ... | tri> _ neq _ = {!!} -- lemma6 ( record {top = next n3} ) {!!} | |
| 178 ... | tri≈ _ eq _ = {!!} | |
| 179 lemma6 s n2 | Nothing = {!!} | |
| 180 lemma5 : (s : SingleLinkedStack (Node ℕ ℕ) ) → popSingleLinkedStack ( record { top = Just (cons n1 (SingleLinkedStack.top s)) } ) | |
| 181 ( \ s1 _ -> (replaceNode (tree0 s1) s1 (record n1 { key = k ; value = x } ) (λ t → | |
| 182 GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))) ) | |
| 183 lemma5 s with (top s) | |
| 184 ... | Just n2 with compTri k k | |
| 185 ... | tri< _ neq _ = ⊥-elim (neq refl) | |
| 186 ... | tri> _ neq _ = ⊥-elim (neq refl) | |
| 187 ... | tri≈ _ refl _ = lemma6 s n2 | |
| 188 lemma5 s | Nothing with compTri k k | |
| 189 ... | tri≈ _ refl _ = checkEQ x _ refl | |
| 190 ... | tri< _ neq _ = ⊥-elim (neq refl) | |
| 191 ... | tri> _ neq _ = ⊥-elim (neq refl) | |
|
564
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
192 ... | tri> le eq gt = {!!} |
|
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
193 ... | tri< le eq gt = {!!} |
| 570 | 194 lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1 |
| 195 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True)))) | |
| 196 lemma0 = lemma2 (record {top = Nothing}) | |
| 197 ... | Nothing = lemma1 | |
| 549 | 198 where |
| 199 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { | |
| 571 | 200 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y } ) k |
|
564
40ab3d39e49d
using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
563
diff
changeset
|
201 ( λ t x1 → checkT x1 x ≡ True) |
| 567 | 202 lemma1 with compTri k k |
| 203 ... | tri≈ _ refl _ = checkEQ x _ refl | |
| 204 ... | tri< _ neq _ = ⊥-elim (neq refl) | |
| 205 ... | tri> _ neq _ = ⊥-elim (neq refl) |