|
10
|
1 module rbt_delete where
|
|
|
2
|
|
|
3 open import Level renaming ( suc to succ ; zero to Zero )
|
|
|
4 open import Data.Nat hiding (compare)
|
|
|
5
|
|
|
6 open import Data.List
|
|
|
7 open import Data.Bool
|
|
|
8
|
|
|
9 open import Data.Nat.Properties as NatProp -- <-cmp
|
|
|
10 open import Relation.Binary -- need <-cmp relation
|
|
|
11
|
|
|
12 open import rbt_t
|
|
|
13
|
|
|
14 -- これあれか、またmergeする時にListにして今回はさらにbaranceも保持しないといけないのか
|
|
|
15 -- 再起処理側はmerge側に
|
|
|
16
|
|
14
|
17
|
|
|
18 test'1 = whileTestPCall' bt-empty 0
|
|
|
19 test'2 = whileTestPCall' (rbt_t.Env.vart test'1) 1
|
|
|
20 test'3 = whileTestPCall' (rbt_t.Env.vart test'2) 2
|
|
|
21 test'4 = whileTestPCall' (rbt_t.Env.vart test'3) 3
|
|
|
22 test'5 = whileTestPCall' (rbt_t.Env.vart test'4) 4
|
|
|
23 test'6 = whileTestPCall' (rbt_t.Env.vart test'5) 5
|
|
|
24 test'7 = whileTestPCall' (rbt_t.Env.vart test'6) 6
|
|
|
25 test'8 = whileTestPCall' (rbt_t.Env.vart test'7) 7
|
|
|
26 test'9 = whileTestPCall' (rbt_t.Env.vart test'8) 8
|
|
|
27 test'10 = whileTestPCall' (rbt_t.Env.vart test'9) 9
|
|
|
28 test'11 = whileTestPCall' (rbt_t.Env.vart test'10) 10
|
|
|
29 test'12 = whileTestPCall' (rbt_t.Env.vart test'11) 11
|
|
|
30 test'13 = whileTestPCall' (rbt_t.Env.vart test'12) 12
|
|
|
31 test'14 = whileTestPCall' (rbt_t.Env.vart test'13) 13
|
|
|
32 test'15 = whileTestPCall' (rbt_t.Env.vart test'14) 14
|
|
|
33
|
|
10
|
34 rbt-find : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
|
|
|
35 rbt-find env next exit with (Env.varn env)
|
|
|
36 ... | n with (Env.vart env)
|
|
|
37 ... | bt-empty = exit (record
|
|
|
38 { vart = bt-empty
|
|
|
39 ; varn = Env.varn env
|
|
|
40 ; varl = Env.varl env
|
|
|
41 })
|
|
|
42 ... | bt-node node with node.number (tree.key node)
|
|
|
43 ... | x with <-cmp n x
|
|
|
44 ... | tri≈ ¬a b ¬c = exit env
|
|
|
45 ... | tri< a ¬b ¬c = next (record
|
|
|
46 { vart = tree.ltree node
|
|
|
47 ; varn = Env.varn env
|
|
|
48 ; varl = Env.varl env
|
|
|
49 })
|
|
|
50 ... | tri> ¬a ¬b c = next (record
|
|
|
51 { vart = tree.rtree node
|
|
|
52 ; varn = Env.varn env
|
|
|
53 ; varl = Env.varl env
|
|
|
54 })
|
|
|
55
|
|
|
56 -- serch min
|
|
|
57 -- exit時は終了
|
|
|
58 -- next時は自己実行
|
|
|
59 rbt-search-min : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
|
|
|
60 rbt-search-min env next exit with Env.vart env
|
|
|
61 ... | bt-empty = exit env
|
|
|
62 ... | bt-node node with tree.ltree node
|
|
|
63 ... | bt-empty = exit env
|
|
|
64 ... | bt-node lnode = next (record
|
|
|
65 { vart = bt-node lnode
|
|
|
66 ; varn = Env.varn env
|
|
|
67 ; varl = Env.varl env
|
|
|
68 })
|
|
|
69
|
|
14
|
70 {-# TERMINATING #-}
|
|
|
71 search-min-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
|
72 search-min-p env exit = rbt-search-min env (λ env → search-min-p env exit ) exit
|
|
|
73
|
|
|
74 search-min : rbt → ℕ
|
|
|
75 search-min tree = search-min-p (record { vart = tree ; varn = zero ; varl = [] }) (λ env → Env.varn env)
|
|
|
76
|
|
|
77 test-search-min = search-min (rbt_t.Env.vart test'15)
|
|
|
78
|
|
10
|
79 -- find(分岐から) 分岐後、delete → balance → 終了
|
|
|
80
|
|
|
81 -- 右も左もenptyならreturn node をexit
|
|
|
82 -- numberが一致しているなら, next(自己実行)へ
|
|
14
|
83 bt-delete-c : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
|
|
|
84 bt-delete-c env next exit with Env.vart env
|
|
10
|
85 ... | bt-empty = exit env
|
|
|
86 ... | bt-node node with (node.number (tree.key node))
|
|
14
|
87 ... | num with <-cmp num (Env.varn env)
|
|
|
88 ... | tri< a ¬b ¬c = next record env{vart = tree.ltree node; varl = (bt-node record node{ltree = bt-empty}) ∷ (Env.varl env)} -- listに左右どちらのbalanceなのか保持する。mergeする際にそれを参照する
|
|
|
89 ... | tri> ¬a ¬b c = next record env{vart = tree.rtree node; varl = (bt-node record node{rtree = bt-empty}) ∷ (Env.varl env)} -- 同上
|
|
|
90 ... | tri≈ ¬a b ¬c with node
|
|
|
91 ... | record { key = key ; ltree = bt-empty ; rtree = bt-empty } = exit record env{vart = bt-node record node {key = record key{coler = red} } } -- colerを赤にしてexit
|
|
|
92 ... | record { key = key ; ltree = bt-node ltree ; rtree = bt-empty } = exit record env{vart = bt-node record ltree{key = record key{coler = black}} } -- leftのcolerを黒にしてexit
|
|
|
93 ... | record { key = key ; ltree = bt-empty ; rtree = bt-node rtree } = next env -- なんかやって右balance
|
|
|
94 ... | record { key = key ; ltree = bt-node ltree ; rtree = bt-node rtree } = next env -- なんかやって右balance
|
|
|
95
|
|
|
96 merge-tree-c : {le : Level} {t : Set le} → Env → (next-bl : Env → t) → (next-br : Env → t) → (exit : Env → t) → t
|
|
|
97 merge-tree-c env next-bl next-br exit with Env.vart env
|
|
|
98 ... | bt-empty = exit env
|
|
|
99 ... | bt-node node with Env.varl env
|
|
|
100 ... | [] = exit env
|
|
|
101 ... | bt-empty ∷ varl = exit env
|
|
|
102 ... | bt-node xtree ∷ varl with <-cmp (node.number (tree.key node)) (node.number (tree.key xtree))
|
|
|
103 ... | tri≈ ¬a b ¬c = exit env
|
|
|
104 ... | tri< a ¬b ¬c = next-bl record env{vart = bt-node record xtree{ltree = Env.vart env} ; varl = varl}
|
|
|
105 ... | tri> ¬a ¬b c = next-br record env{vart = bt-node record xtree{rtree = Env.vart env} ; varl = varl}
|
|
10
|
106
|
|
|
107 -- bt-delete record { vart = bt-empty ; varn = varn ; varl = varl } selfdo next exit = {!!}
|
|
|
108 -- bt-delete record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } selfdo next exit = {!!}
|
|
|
109
|
|
14
|
110 -- do branch
|
|
|
111 -- next12 rotate_left → barance-12-c
|
|
|
112 -- next47 part-tree → rotate_right → barance-47-bc → rotate_left → barance-47-fc
|
|
|
113 -- exit merge_tree
|
|
|
114 balance_left-c : {le : Level} {t : Set le} → Env → (next12 : Env → t) → (next47 : Env → t) → (exit : Env → t) → t
|
|
|
115 balance_left-c env next12 next47 exit with (Env.varn env) -- flag
|
|
|
116 ... | suc d = exit env -- flug true
|
|
|
117 ... | zero with (Env.vart env)
|
|
|
118 ... | bt-empty = exit env
|
|
|
119 ... | bt-node node with (tree.rtree node)
|
|
|
120 ... | bt-empty = exit env
|
|
|
121 ... | bt-node rtree with (tree.ltree rtree)
|
|
|
122 ... | bt-empty = exit env
|
|
|
123 ... | bt-node rltree with (node.coler (tree.key rltree))
|
|
|
124 ... | black = next12 env
|
|
|
125 ... | red = next47 record env{vart = tree.rtree node; varl = (bt-node record node{rtree = bt-empty}) ∷ (Env.varl env)} -- part-treeする
|
|
|
126
|
|
|
127 -- next merge-tree
|
|
|
128 barance-12-c : {le : Level} {t : Set le} → Env → (next : Env → t) → t
|
|
|
129 barance-12-c env next with (Env.vart env)
|
|
|
130 ... | bt-empty = next env
|
|
|
131 ... | bt-node node with (node.coler (tree.key node))
|
|
|
132 ... | red = next record env{vart = bt-node record node{key = record (tree.key node){coler = black} } }
|
|
|
133 ... | black = next record env{varn = 0}
|
|
10
|
134
|
|
|
135
|
|
14
|
136 -- do merge-tree rtree
|
|
|
137 -- post rotate-left → barance-47-fc
|
|
|
138 barance-47-bc : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
|
|
|
139 barance-47-bc env next exit with (Env.varl env)
|
|
|
140 ... | [] = next env
|
|
|
141 ... | bt-empty ∷ s = next env
|
|
|
142 ... | bt-node node ∷ s = next record env{vart = bt-node record node{rtree = Env.vart env} ; varl = s}
|
|
|
143
|
|
|
144 -- do rewrite
|
|
|
145 -- post merge-tree
|
|
|
146 barance-47-fc : {le : Level} {t : Set le} → Env → (next : Env → t) → t
|
|
|
147 barance-47-fc env next with (Env.vart env)
|
|
|
148 ... | bt-empty = next env
|
|
|
149 ... | bt-node node with tree.ltree node
|
|
|
150 ... | bt-empty = next env
|
|
|
151 ... | bt-node ltree with tree.rtree node
|
|
|
152 ... | bt-empty = next env
|
|
|
153 ... | bt-node rtree = next record env{vart = bt-node record node{
|
|
|
154 rtree = bt-node record rtree{
|
|
|
155 key = record (tree.key rtree){
|
|
|
156 coler = black} } ;
|
|
|
157 ltree = bt-node record ltree{
|
|
|
158 key = record (tree.key ltree){
|
|
|
159 coler = black} } } }
|
|
|
160
|
|
|
161 -- do branch
|
|
|
162 -- next12 rewrite → barance-12-c
|
|
|
163 -- next3 barance-3c
|
|
|
164 -- next58 rotate_right → barance-58-c
|
|
|
165 -- exit merge_tree
|
|
|
166 balance_right-c : {le : Level} {t : Set le} → Env → (next12 : Env → t) → (next3 : Env → t) → (next58 : Env → t) → (exit : Env → t) → t
|
|
|
167 balance_right-c env next12 next3 next58 exit with (Env.varn env) -- flag
|
|
|
168 ... | suc d = exit env -- flug true
|
|
|
169 ... | zero with (Env.vart env)
|
|
|
170 ... | bt-empty = exit env
|
|
|
171 ... | bt-node node with (tree.ltree node)
|
|
|
172 ... | bt-empty = exit env
|
|
|
173 ... | bt-node ltree with (tree.ltree ltree)
|
|
|
174 ... | bt-empty = exit env
|
|
|
175 ... | bt-node lltree with (node.coler (tree.key lltree))
|
|
|
176 ... | red = next58 env
|
|
|
177 ... | black with (node.coler (tree.key ltree))
|
|
|
178 ... | black = next12 record env{vart = bt-node record node{
|
|
|
179 ltree = bt-node record ltree{
|
|
|
180 key = record(tree.key ltree){
|
|
|
181 coler = red} }}}
|
|
|
182 ... | red = next3 env
|
|
|
183
|
|
|
184 -- do rewrite
|
|
|
185 -- post merge-tree
|
|
|
186 balance-58-c : {le : Level} {t : Set le} → Env → (next : Env → t) → t -- 47-bcと一緒
|
|
|
187 balance-58-c env next with (Env.vart env)
|
|
|
188 ... | bt-empty = next env
|
|
|
189 ... | bt-node node with tree.ltree node
|
|
|
190 ... | bt-empty = next env
|
|
|
191 ... | bt-node ltree with tree.rtree node
|
|
|
192 ... | bt-empty = next env
|
|
|
193 ... | bt-node rtree = next record env{vart = bt-node record node{
|
|
|
194 rtree = bt-node record rtree{
|
|
|
195 key = record (tree.key rtree){
|
|
|
196 coler = black} } ;
|
|
|
197 ltree = bt-node record ltree{
|
|
|
198 key = record (tree.key ltree){
|
|
|
199 coler = black} } } }
|
|
|
200
|
|
|
201 -- do branch
|
|
|
202 -- next-r rotate-right → barance-3-rc
|
|
|
203 -- next-l part-tree left → rotate-left → barance-3-lbc(marge-tree left) → rotate-right → barance-3-lfc
|
|
|
204 -- exit merge-tree
|
|
|
205 balance-3-c : {le : Level} {t : Set le} → Env → (next-r : Env → t) → (next-l : Env → t) → (exit : Env → t) → t
|
|
|
206 balance-3-c env next-r next-l exit with (Env.vart env)
|
|
|
207 ... | bt-empty = exit env
|
|
|
208 ... | bt-node node with tree.ltree node
|
|
|
209 ... | bt-empty = exit env
|
|
|
210 ... | bt-node ltree with tree.rtree ltree
|
|
|
211 ... | bt-empty = exit env
|
|
|
212 ... | bt-node lrtree with tree.ltree lrtree
|
|
|
213 ... | bt-empty = exit env
|
|
|
214 ... | bt-node lrltree with (node.coler (tree.key lrltree))
|
|
|
215 ... | black = next-r env
|
|
|
216 ... | red = next-l record env{vart = tree.ltree node; varl = (bt-node record node{ltree = bt-empty}) ∷ (Env.varl env)} -- part-tree left
|
|
|
217
|
|
|
218 -- do rewrite
|
|
|
219 -- next marge-tree
|
|
|
220 barance-3-rc : {le : Level} {t : Set le} → Env → (next : Env → t) → t
|
|
|
221 barance-3-rc env next with (Env.vart env)
|
|
|
222 ... | bt-empty = next env
|
|
|
223 ... | bt-node node with tree.rtree node
|
|
|
224 ... | bt-empty = next env
|
|
|
225 ... | bt-node rtree with tree.ltree rtree
|
|
|
226 ... | bt-empty = next env
|
|
|
227 ... | bt-node rltree = next record env{vart = bt-node record node{
|
|
|
228 rtree = bt-node record rtree{
|
|
|
229 key = record (tree.key rtree){
|
|
|
230 coler = black};
|
|
|
231 ltree = bt-node record rltree{
|
|
|
232 key = record (tree.key rltree){coler = red}} } } }
|
|
|
233
|
|
|
234 -- do marge-tree left
|
|
|
235 -- next rotate-right → barance-3-lfc
|
|
|
236 barance-3-lbc : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
|
|
|
237 barance-3-lbc env next exit with (Env.varl env)
|
|
|
238 ... | [] = exit env
|
|
|
239 ... | bt-empty ∷ s = exit env
|
|
|
240 ... | bt-node node ∷ s = next record env{vart = bt-node record node{ltree = Env.vart env} ; varl = s}
|
|
|
241
|
|
|
242 -- do rewrite
|
|
|
243 -- next marge-tree
|
|
|
244 barance-3-lfc : {le : Level} {t : Set le} → Env → (next : Env → t) → t
|
|
|
245 barance-3-lfc env next with (Env.vart env)
|
|
|
246 ... | bt-empty = next env
|
|
|
247 ... | bt-node node with tree.rtree node
|
|
|
248 ... | bt-empty = next env
|
|
|
249 ... | bt-node rtree with tree.ltree node
|
|
|
250 ... | bt-empty = next env
|
|
|
251 ... | bt-node ltree with tree.rtree ltree
|
|
|
252 ... | bt-empty = next env
|
|
|
253 ... | bt-node lrtree = next record env{vart = bt-node record node{
|
|
|
254 rtree = bt-node record rtree{
|
|
|
255 key = record (tree.key rtree){
|
|
|
256 coler = black};
|
|
|
257 ltree = bt-node record lrtree{
|
|
|
258 key = record (tree.key lrtree){coler = red}} } } }
|
|
10
|
259
|
|
|
260 {-# TERMINATING #-}
|
|
|
261 find-com : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
|
262 find-com env exit = rbt-find env (λ env → find-com env exit ) exit
|
|
|
263
|
|
|
264 --init
|
|
|
265 find : {l : Level} {t : Set l} → rbt → ℕ → (exit : Env → t) → t
|
|
|
266 find tree num exit = find-com (record{ vart = tree ; varn = num; varl = [] }) exit
|
|
|
267
|
|
|
268 open import Agda.Builtin.Nat
|
|
|
269
|
|
|
270 check-find : Env → ℕ → Bool
|
|
|
271 check-find tree num with Env.vart tree
|
|
|
272 ... | bt-empty = false
|
|
|
273 ... | bt-node node with node.number (tree.key node)
|
|
|
274 ... | n = n == num
|
|
|
275
|
|
14
|
276
|
|
|
277 {-# TERMINATING #-}
|
|
|
278 bt-delete-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
|
279 bt-delete-p env exit = bt-delete-c env (λ env → bt-delete-p env exit) exit
|
|
|
280
|
|
|
281 balance-12-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
|
282 balance-12-p env exit = merge-rotate-left env (λ env → barance-12-c env exit) exit
|
|
|
283
|
|
|
284 balance-47-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
|
285 balance-47-p env exit = merge-rotate-right env (λ env → barance-47-bc env (λ env → merge-rotate-left env (λ env → barance-47-fc env exit) exit) exit) exit
|
|
|
286
|
|
|
287 -- exit merge-tree
|
|
|
288 balance_left-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
|
289 balance_left-p env exit = balance_left-c env (λ env → balance-12-p env exit) (λ env → balance-47-p env exit) exit
|
|
|
290
|
|
|
291 balance-3-r-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
|
292 balance-3-r-p env exit = merge-rotate-right env (λ env → barance-3-rc env exit) exit
|
|
|
293
|
|
|
294
|
|
|
295 balance-3-l-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
|
296 balance-3-l-p env exit = merge-rotate-left env (λ env → barance-3-lbc env (λ env → merge-rotate-right env (λ env → barance-3-lfc env exit) exit) exit) exit
|
|
|
297
|
|
|
298
|
|
|
299 balance-3-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
|
300 balance-3-p env exit = balance-3-c env (λ env → balance-3-r-p env exit) (λ env → balance-3-l-p env exit) exit
|
|
|
301
|
|
|
302 balance-58-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
|
303 balance-58-p env exit = merge-rotate-right env (λ env → balance-58-c env exit) exit
|
|
|
304
|
|
|
305 -- exit merge-tree
|
|
|
306 balance_right-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
|
307 balance_right-p env exit = balance_right-c env (λ env → barance-12-c env exit) (λ env → balance-3-p env exit) (λ env → balance-58-p env exit) exit
|
|
|
308
|
|
|
309 {-# TERMINATING #-}
|
|
|
310 delete-merge-tree-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
|
311 delete-merge-tree-p env exit = merge-tree-c env (λ env → balance_left-p env (λ env → delete-merge-tree-p env exit)) (λ env → balance_right-p env (λ env → delete-merge-tree-p env exit)) exit
|
|
|
312
|
|
|
313 bt-delete-init : Env → rbt
|
|
|
314 bt-delete-init env = bt-delete-p env (λ env → delete-merge-tree-p env (λ env → Env.vart env))
|
|
|
315
|
|
|
316 bt-delete : rbt → ℕ → rbt
|
|
|
317 bt-delete rbt n = bt-delete-init (record { vart = rbt ; varn = n ; varl = [] })
|
|
10
|
318
|
|
|
319 b = find (Env.vart test'15) 123 (λ env → env)
|
|
|
320
|
|
14
|
321 test = bt-delete (Env.vart test'15) 0
|
|
10
|
322
|
|
|
323
|
|
|
324 c = check-find (find (Env.vart test'15) 1 (λ env → env) ) 1
|
|
|
325
|
|
|
326
|
