|
3
|
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
|
