Mercurial > hg > Papers > 2020 > soto-midterm

comparison src/redBlackTreeTest.agda.replaced @ 1:73127e0ab57c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
(none)
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 08 Sep 2020 18:38:08 +0900
parents
children
comparison
equal deleted inserted replaced
0:b919985837a3 1:73127e0ab57c
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 : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t
17 putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree)
18 ... | Nothing = next (record tree {root = Just (leafNode k1 value) })
19 ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s @$\rightarrow$@ findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 @$\rightarrow$@ replaceNode tree1 s n1 next))
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 @$\mathbb{N}$@ @$\mathbb{N}$@)) @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ 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 check2 : {m : Level } (n : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@)) @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Bool {m}
33 check2 Nothing _ = False
34 check2 (Just n) x with compare2 (value n) x
35 ... | EQ = True
36 ... | _ = False
37
38 test1 : putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ {Set Level.zero} ) 1 1 ( \t @$\rightarrow$@ getRedBlackTree t 1 ( \t x @$\rightarrow$@ check2 x 1 @$\equiv$@ True ))
39 test1 = refl
40
41 test2 : putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ {Set Level.zero} ) 1 1 (
42 \t @$\rightarrow$@ putTree1 t 2 2 (
43 \t @$\rightarrow$@ getRedBlackTree t 1 (
44 \t x @$\rightarrow$@ check2 x 1 @$\equiv$@ True )))
45 test2 = refl
46
47 open @$\equiv$@-Reasoning
48 test3 : putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ {Set Level.zero}) 1 1
49 $ \t @$\rightarrow$@ putTree1 t 2 2
50 $ \t @$\rightarrow$@ putTree1 t 3 3
51 $ \t @$\rightarrow$@ putTree1 t 4 4
52 $ \t @$\rightarrow$@ getRedBlackTree t 1
53 $ \t x @$\rightarrow$@ check2 x 1 @$\equiv$@ True
54 test3 = begin
55 check2 (Just (record {key = 1 ; value = 1 ; color = Black ; left = Nothing ; right = Just (leafNode 2 2)})) 1
56 @$\equiv$@@$\langle$@ refl @$\rangle$@
57 True
58 @$\blacksquare$@
59
60 test31 = putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ ) 1 1
61 $ \t @$\rightarrow$@ putTree1 t 2 2
62 $ \t @$\rightarrow$@ putTree1 t 3 3
63 $ \t @$\rightarrow$@ putTree1 t 4 4
64 $ \t @$\rightarrow$@ getRedBlackTree t 4
65 $ \t x @$\rightarrow$@ x
66
67 -- test5 : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@)
68 test5 = putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ ) 4 4
69 $ \t @$\rightarrow$@ putTree1 t 6 6
70 $ \t0 @$\rightarrow$@ clearSingleLinkedStack (nodeStack t0)
71 $ \s @$\rightarrow$@ findNode1 t0 s (leafNode 3 3) ( root t0 )
72 $ \t1 s n1 @$\rightarrow$@ replaceNode t1 s n1
73 $ \t @$\rightarrow$@ getRedBlackTree t 3
74 -- $ \t x @$\rightarrow$@ SingleLinkedStack.top (stack s)
75 -- $ \t x @$\rightarrow$@ n1
76 $ \t x @$\rightarrow$@ root t
77 where
78 findNode1 : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ (Node a k) @$\rightarrow$@ (Maybe (Node a k)) @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Node a k @$\rightarrow$@ t) @$\rightarrow$@ t
79 findNode1 t s n1 Nothing next = next t s n1
80 findNode1 t s n1 ( Just n2 ) next = findNode t s n1 n2 next
81
82 -- test51 : putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {_} {Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@)} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ {Set Level.zero} ) 1 1 $ \t @$\rightarrow$@
83 -- putTree1 t 2 2 $ \t @$\rightarrow$@ putTree1 t 3 3 $ \t @$\rightarrow$@ root t @$\equiv$@ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} )
84 -- test51 = refl
85
86 test6 : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@)
87 test6 = root (createEmptyRedBlackTree@$\mathbb{N}$@ {_} @$\mathbb{N}$@ {Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@)})
88
89
90 test7 : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@)
91 test7 = clearSingleLinkedStack (nodeStack tree2) (\ s @$\rightarrow$@ replaceNode tree2 s n2 (\ t @$\rightarrow$@ root t))
92 where
93 tree2 = createEmptyRedBlackTree@$\mathbb{N}$@ {_} @$\mathbb{N}$@ {Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@)}
94 k1 = 1
95 n2 = leafNode 0 0
96 value1 = 1
97
98 test8 : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@)
99 test8 = putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@) 1 1
100 $ \t @$\rightarrow$@ putTree1 t 2 2 (\ t @$\rightarrow$@ root t)
101
102
103 test9 : putRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ {Set Level.zero} ) 1 1 ( \t @$\rightarrow$@ getRedBlackTree t 1 ( \t x @$\rightarrow$@ check2 x 1 @$\equiv$@ True ))
104 test9 = refl
105
106 test10 : putRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ {Set Level.zero} ) 1 1 (
107 \t @$\rightarrow$@ putRedBlackTree t 2 2 (
108 \t @$\rightarrow$@ getRedBlackTree t 1 (
109 \t x @$\rightarrow$@ check2 x 1 @$\equiv$@ True )))
110 test10 = refl
111
112 test11 = putRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@) 1 1
113 $ \t @$\rightarrow$@ putRedBlackTree t 2 2
114 $ \t @$\rightarrow$@ putRedBlackTree t 3 3
115 $ \t @$\rightarrow$@ getRedBlackTree t 2
116 $ \t x @$\rightarrow$@ root t
117
118
119 redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a @$\mathbb{N}$@)) {t : Set m} @$\rightarrow$@ RedBlackTree {Level.zero} {m} {t} a @$\mathbb{N}$@
120 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }
121
122 -- compare2 : (x y : @$\mathbb{N}$@ ) @$\rightarrow$@ compareresult
123 -- compare2 zero zero = eq
124 -- compare2 (suc _) zero = gt
125 -- compare2 zero (suc _) = lt
126 -- compare2 (suc x) (suc y) = compare2 x y
127
128 putTest1Lemma2 : (k : @$\mathbb{N}$@) @$\rightarrow$@ compare2 k k @$\equiv$@ EQ
129 putTest1Lemma2 zero = refl
130 putTest1Lemma2 (suc k) = putTest1Lemma2 k
131
132 putTest1Lemma1 : (x y : @$\mathbb{N}$@) @$\rightarrow$@ compare@$\mathbb{N}$@ x y @$\equiv$@ compare2 x y
133 putTest1Lemma1 zero zero = refl
134 putTest1Lemma1 (suc m) zero = refl
135 putTest1Lemma1 zero (suc n) = refl
136 putTest1Lemma1 (suc m) (suc n) with Data.Nat.compare m n
137 putTest1Lemma1 (suc .m) (suc .(Data.Nat.suc m + k)) | less m k = lemma1 m
138 where
139 lemma1 : (m : @$\mathbb{N}$@) @$\rightarrow$@ LT @$\equiv$@ compare2 m (@$\mathbb{N}$@.suc (m + k))
140 lemma1 zero = refl
141 lemma1 (suc y) = lemma1 y
142 putTest1Lemma1 (suc .m) (suc .m) | equal m = lemma1 m
143 where
144 lemma1 : (m : @$\mathbb{N}$@) @$\rightarrow$@ EQ @$\equiv$@ compare2 m m
145 lemma1 zero = refl
146 lemma1 (suc y) = lemma1 y
147 putTest1Lemma1 (suc .(Data.Nat.suc m + k)) (suc .m) | greater m k = lemma1 m
148 where
149 lemma1 : (m : @$\mathbb{N}$@) @$\rightarrow$@ GT @$\equiv$@ compare2 (@$\mathbb{N}$@.suc (m + k)) m
150 lemma1 zero = refl
151 lemma1 (suc y) = lemma1 y
152
153 putTest1Lemma3 : (k : @$\mathbb{N}$@) @$\rightarrow$@ compare@$\mathbb{N}$@ k k @$\equiv$@ EQ
154 putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k )
155
156 compareLemma1 : {x y : @$\mathbb{N}$@} @$\rightarrow$@ compare2 x y @$\equiv$@ EQ @$\rightarrow$@ x @$\equiv$@ y
157 compareLemma1 {zero} {zero} refl = refl
158 compareLemma1 {zero} {suc _} ()
159 compareLemma1 {suc _} {zero} ()
160 compareLemma1 {suc x} {suc y} eq = cong ( \z @$\rightarrow$@ @$\mathbb{N}$@.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
161 where
162 lemma2 : compare2 (@$\mathbb{N}$@.suc x) (@$\mathbb{N}$@.suc y) @$\equiv$@ compare2 x y
163 lemma2 = refl
164
165
166 putTest1 :{ m : Level } (n : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@))
167 @$\rightarrow$@ (k : @$\mathbb{N}$@) (x : @$\mathbb{N}$@)
168 @$\rightarrow$@ putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (redBlackInSomeState {_} @$\mathbb{N}$@ n {Set Level.zero}) k x
169 (\ t @$\rightarrow$@ getRedBlackTree t k (\ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True))
170 putTest1 n k x with n
171 ... | Just n1 = lemma2 ( record { top = Nothing } )
172 where
173 lemma2 : (s : SingleLinkedStack (Node @$\mathbb{N}$@ @$\mathbb{N}$@) ) @$\rightarrow$@ putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (@$\lambda$@ t @$\rightarrow$@
174 GetRedBlackTree.checkNode t k (@$\lambda$@ t@$\_{1}$@ x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) (root t))
175 lemma2 s with compare2 k (key n1)
176 ... | EQ = lemma3 {!!}
177 where
178 lemma3 : compare2 k (key n1) @$\equiv$@ EQ @$\rightarrow$@ getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record { root = Just ( record {
179 key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black
180 } ) ; nodeStack = s ; compare = @$\lambda$@ x@$\_{1}$@ y @$\rightarrow$@ compare2 x@$\_{1}$@ y } ) k ( \ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True)
181 lemma3 eq with compare2 x x | putTest1Lemma2 x
182 ... | EQ | refl with compare2 k (key n1) | eq
183 ... | EQ | refl with compare2 x x | putTest1Lemma2 x
184 ... | EQ | refl = refl
185 ... | GT = {!!}
186 ... | LT = {!!}
187
188 ... | Nothing = lemma1
189 where
190 lemma1 : getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record { root = Just ( record {
191 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red
192 } ) ; nodeStack = record { top = Nothing } ; compare = @$\lambda$@ x@$\_{1}$@ y @$\rightarrow$@ compare2 x@$\_{1}$@ y } ) k
193 ( \ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True)
194 lemma1 with compare2 k k | putTest1Lemma2 k
195 ... | EQ | refl with compare2 x x | putTest1Lemma2 x
196 ... | EQ | refl = refl