7
|
1 module rbt_t where
|
|
2
|
|
3 open import Data.Nat hiding (compare)
|
|
4 open import Data.Nat.Properties as NatProp -- <-cmp
|
|
5 open import Relation.Binary
|
|
6 open import Data.List
|
|
7
|
|
8 -- → t を適用するために必要だった
|
|
9 open import Level renaming ( suc to succ ; zero to Zero )
|
|
10 open import Level
|
|
11
|
|
12
|
|
13 data col : Set where
|
|
14 black : col
|
|
15 red : col
|
|
16
|
|
17 record node (A B : Set) : Set where
|
|
18 field
|
|
19 coler : A
|
|
20 number : B
|
9
|
21 open node
|
7
|
22
|
|
23 record tree (A B C : Set) : Set where
|
|
24 field
|
|
25 key : A
|
|
26 ltree : B
|
|
27 rtree : C
|
9
|
28 open tree
|
7
|
29
|
|
30 data rbt : Set where
|
|
31 bt-empty : rbt
|
|
32 bt-node : (node : tree (node col ℕ) rbt rbt ) → rbt
|
|
33
|
|
34 record Env : Set (succ Zero) where
|
|
35 field
|
|
36 vart : rbt
|
|
37 varn : ℕ
|
|
38 varl : List rbt
|
|
39 open Env
|
|
40
|
8
|
41 whileTest-next : {l : Level} {t : Set l} → (c10 : rbt) → (n : ℕ) → (list : List rbt) → (next : Env → t) → (exit : Env → t) → t
|
|
42 whileTest-next c10 n list next exit = next (record {vart = c10 ; varn = n ; varl = list} )
|
7
|
43
|
|
44 merge-tree : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
|
|
45
|
|
46 -- 全てmerge-treeへ
|
|
47 split : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
|
|
48 split node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
|
|
49 split node@record { vart = (bt-node record { key = key ; ltree = bt-empty ; rtree = rtree }) ; varn = varn ; varl = varl } next exit = exit node
|
|
50 split node@record { vart = (bt-node record { key = key ; ltree = (bt-node node₁) ; rtree = bt-empty }) ; varn = varn ; varl = varl } next exit = exit node
|
|
51 split record { vart = (bt-node record { key = record { coler = coler₁ ; number = number₁ }
|
|
52 ; ltree = (bt-node record { key = record { coler = ly ; number = ln } ; ltree = ll ; rtree = lr })
|
|
53 ; rtree = (bt-node record { key = record { coler = ry ; number = rn } ; ltree = rl ; rtree = rr }) })
|
|
54 ; varn = varn ; varl = varl } next exit
|
|
55 = next record { vart = (bt-node record { key = record { coler = red ; number = number₁ }
|
|
56 ; ltree = (bt-node record { key = record { coler = black ; number = ln } ; ltree = ll ; rtree = lr })
|
|
57 ; rtree = (bt-node record { key = record { coler = black ; number = rn } ; ltree = rl ; rtree = rr }) })
|
|
58 ; varn = varn ; varl = varl }
|
|
59
|
|
60
|
|
61 -- 右回転
|
|
62 -- 実行時splitへ、それ以外はmerge-treeへ
|
8
|
63 merge-rotate-right : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
|
|
64 merge-rotate-right node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
|
|
65 merge-rotate-right node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = bt-empty ; rtree = r } ; varn = varn ; varl = varl } next exit = exit node
|
|
66 merge-rotate-right record { vart = bt-node record { key = record { coler = y ; number = x }
|
7
|
67 ; ltree = (bt-node record { key = record { coler = ly ; number = lx } ; ltree = ll ; rtree = lr })
|
|
68 ; rtree = r }
|
|
69 ; varn = varn ; varl = varl } next exit
|
|
70 = next record { vart = bt-node record { key = record { coler = y ; number = lx }
|
|
71 ; ltree = ll
|
|
72 ; rtree = (bt-node record { key = record { coler = red ; number = x } ; ltree = lr; rtree = r }) }
|
|
73 ; varn = varn ; varl = varl }
|
|
74
|
|
75
|
|
76 -- split
|
8
|
77 split-branch : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
|
|
78 split-branch node@record{ vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
|
|
79 split-branch node@record{ vart = bt-node record { key = key ; ltree = bt-empty ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
|
|
80 split-branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = lc ; number = number } ; ltree = bt-empty ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
|
|
81 split-branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = black ; number = number } ; ltree = (bt-node node₁) ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
|
|
82 split-branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = red ; number = number₁ } ; ltree = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree₁ }) ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
|
|
83 split-branch node@record{ vart = bt-node record { key = key₁
|
7
|
84 ; ltree = (bt-node record { key = record { coler = red ; number = number₁ }
|
|
85 ; ltree = (bt-node record { key = record { coler = red ; number = number } ; ltree = ltree ; rtree = rtree₁ })
|
|
86 ; rtree = lr })
|
|
87 ; rtree = rtree }
|
|
88 ; varn = varn ; varl = varl } next exit
|
|
89 = next node
|
|
90
|
|
91
|
|
92 -- 左回転、exitはsplit_branchへ nextもsplit_branchへ
|
8
|
93 merge-rotate-left : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
|
|
94 merge-rotate-left node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
|
|
95 merge-rotate-left node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = bt-empty } ; varn = varn ; varl = varl } next exit = exit node
|
|
96 merge-rotate-left record { vart = bt-node record { key = record { coler = y ; number = x } ; ltree = l ; rtree = (bt-node record { key = record { coler = ry ; number = rx } ; ltree = rl ; rtree = rr }) } ; varn = varn ; varl = varl } next exit
|
7
|
97 = next record { vart = bt-node record { key = record { coler = y ; number = rx }
|
|
98 ; ltree = (bt-node record { key = record { coler = red ; number = x } ; ltree = l ; rtree = rl })
|
|
99 ; rtree = rr}
|
|
100 ; varn = varn ; varl = varl }
|
|
101
|
|
102
|
|
103 -- skew exitがsplitへ nextが左回転
|
|
104 skew-bt : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
|
|
105 skew-bt node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
|
|
106 skew-bt node@record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) ; varn = varn ; varl = varl } next exit = exit node
|
|
107 skew-bt node@record { vart = (bt-node record { key = key₁
|
|
108 ; ltree = ltree₁
|
|
109 ; rtree = (bt-node record { key = record { coler = black ; number = number }
|
|
110 ; ltree = ltree ; rtree = rtree }) }) ; varn = varn ; varl = varl } next exit
|
|
111 = exit node
|
|
112 skew-bt node@record { vart = (bt-node record { key = key₁
|
|
113 ; ltree = ltree₁
|
|
114 ; rtree = (bt-node record { key = record { coler = red ; number = number } ; ltree = ltree ; rtree = rtree }) })
|
|
115 ; varn = varn ; varl = varl } next exit
|
|
116 = next node
|
|
117
|
|
118
|
8
|
119 set-node-coler : Env → Env
|
|
120 set-node-coler node@record { vart = bt-empty ; varn = varn ; varl = varl } = node
|
|
121 set-node-coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
|
7
|
122 = record { vart = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
|
|
123
|
8
|
124 init-node-coler : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
|
|
125 init-node-coler node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
|
|
126 init-node-coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit
|
|
127 = exit record { vart = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
|
7
|
128
|
9
|
129 --修正前
|
8
|
130 merge-tree node@record { vart = vart ; varn = varn ; varl = [] } next exit = exit node
|
7
|
131 merge-tree node@record { vart = vart ; varn = varn ; varl = (bt-empty ∷ varl₁) } next exit = exit node
|
9
|
132
|
7
|
133 merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit with <-cmp varn number
|
9
|
134
|
7
|
135 merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri≈ ¬a b ¬c
|
|
136 = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = number ; varl = varl₁ }
|
|
137
|
|
138 merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri> ¬a ¬b c
|
|
139 = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = vart }) ; varn = number ; varl = varl₁ }
|
|
140
|
|
141 merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri< a ¬b ¬c
|
|
142 = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = vart ; rtree = rtree }) ; varn = number ; varl = varl₁ }
|
|
143
|
9
|
144 --修正後
|
|
145 merge-tree1 : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
|
|
146 merge-tree1 env next exit with varl env
|
|
147 ... | [] = exit env
|
|
148 ... | bt-empty ∷ nl = exit env
|
|
149 ... | bt-node node₁ ∷ nl with <-cmp (varn env) (number ( key node₁ ))
|
|
150 ... | tri≈ ¬a b ¬c = next (record env { varn = number (key node₁) ; varl = nl })
|
|
151 -- next (record{ vart = vart env ; varn = number (key node₁) ; varl = nl })
|
|
152 ... | tri> ¬a ¬b c = next (record env { vart = (bt-node record { key = key node₁ ; ltree = ltree node₁ ; rtree = vart env }) ; varn = number (key node₁) ; varl = nl })
|
|
153 -- next (record{ vart = (bt-node record { key = key node₁ ; ltree = ltree node₁ ; rtree = vart env }) ; varn = number (key node₁) ; varl = nl })
|
|
154 ... | tri< a ¬b ¬c = next (record{ vart = (bt-node record { key = key node₁ ; ltree = vart env ; rtree = rtree node₁ }) ; varn = number (key node₁) ; varl = nl })
|
7
|
155
|
|
156 -- insert
|
|
157 bt-insert : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
|
|
158 -- mergeへ遷移する
|
|
159 bt-insert (record { vart = bt-empty ; varn = varn ; varl = varl }) next exit
|
|
160 = exit (record { vart = (bt-node (record { key = record { coler = red ; number = varn }; ltree = bt-empty; rtree = bt-empty })) ; varn = varn ; varl = varl })
|
|
161
|
|
162 -- 場合分けを行う
|
|
163 bt-insert record {vart = (bt-node record { key = record { coler = y; number = x } ; ltree = ltree ; rtree = rtree }) ; varn = n ; varl = varl } next exit with <-cmp x n
|
|
164 bt-insert node@(record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } ) next exit | tri≈ ¬a b ¬c
|
|
165 = exit node
|
|
166
|
|
167 bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri> ¬a ¬b c
|
|
168 = next (record {vart = ltree ; varn = varn ; varl = (bt-node record { key = key ; ltree = bt-empty ; rtree = rtree }) ∷ varl })
|
|
169
|
|
170 bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri< a ¬b ¬c
|
|
171 = next (record {vart = rtree ; varn = varn ; varl = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) ∷ varl })
|
|
172
|
9
|
173
|
|
174
|
7
|
175 -- normal loop without termination
|
|
176 {-# TERMINATING #-}
|
|
177 insert : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
178 insert env exit = bt-insert env (λ env → insert env exit ) exit
|
|
179
|
8
|
180
|
|
181
|
|
182 init-col : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
183 init-col env exit = init-node-coler env exit exit
|
|
184
|
|
185 {-
|
7
|
186 {-# TERMINATING #-}
|
|
187 merge : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
188
|
|
189 {-# TERMINATING #-}
|
|
190 split-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
191 split-p env exit = split env (λ env → merge env (λ env → merge env exit ) ) exit
|
|
192
|
|
193 {-# TERMINATING #-}
|
|
194 rotate_right : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
8
|
195 rotate_right env exit = merge-rotate-right env (λ env → split-p env (λ env → merge env exit ) ) exit
|
7
|
196
|
|
197 {-# TERMINATING #-}
|
|
198 split-b : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
8
|
199 split-b env exit = split-branch env (λ env → rotate_right env exit ) λ env → merge env exit
|
7
|
200
|
|
201 {-# TERMINATING #-}
|
|
202 rotate_left : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
8
|
203 rotate_left env exit = merge-rotate-left env (λ env → split-b env exit ) exit
|
7
|
204
|
|
205 {-# TERMINATING #-}
|
|
206 skew : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
207 skew env exit = skew-bt env (λ env → rotate_left env (λ env → split-b env exit ) ) exit
|
|
208
|
|
209 merge env exit = merge-tree env (λ env → skew env exit ) exit
|
8
|
210 -}
|
|
211 -- skewはnextがrotate-right。exitはsplitとなる
|
|
212 -- skewの中にrotate-rightが内包され、実行後は必ずsplitに遷移する
|
|
213 -- それはskewのexitと等しいので同時に記述してやる。
|
|
214 skew' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
215 skew' env exit = skew-bt env (λ env → merge-rotate-left env exit exit ) exit
|
|
216
|
|
217 split' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
218 split' env exit = split-branch env (λ env → merge-rotate-right env (λ env → split env exit exit ) (λ env → split env exit exit ) ) exit
|
7
|
219
|
|
220
|
8
|
221 {-
|
|
222 merge' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
223 merge' node@record { vart = vart ; varn = varn ; varl = [] } exit = exit node
|
|
224 merge' node@record { vart = vart ; varn = varn ; varl = (x ∷ varl₁) } exit = merge' (merge-tree node (λ env → skew' env (λ env → split' env (λ env → env) ) ) (λ env → env) ) exit
|
|
225 -}
|
7
|
226
|
|
227 whileTestP : {l : Level} {t : Set l} → (tree : rbt) → (n : ℕ) → (Code : Env → t) → t
|
|
228 whileTestP tree n next = next (record {vart = tree ; varn = n ; varl = [] } )
|
|
229
|
8
|
230
|
7
|
231
|
8
|
232 {-# TERMINATING #-}
|
|
233 mergeP : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
234 mergeP env exit = merge-tree env (λ env → skew' env (λ env → split' env (λ env → mergeP env exit)) ) exit
|
7
|
235
|
|
236 {-
|
9
|
237 mergeP1 : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
238 mergeP1 record { vart = vart ; varn = varn ; varl = [] } exit = {!!}
|
|
239 mergeP1 record { vart = vart ; varn = varn ; varl = (x ∷ varl₁) } exit = {!!}
|
|
240 -}
|
|
241
|
|
242 {-
|
8
|
243 merge-tree env
|
|
244 (λ env → skew-bt env
|
|
245 (λ env → merge-rotate-left env
|
|
246 (λ env → split-branch env
|
|
247 (λ env → merge-rotate-right env
|
|
248 (λ env → split env (λ env → mergeP env exit ) (λ env → mergeP env exit ) ) exit)
|
|
249 (λ env → mergeP env exit ) )
|
|
250 exit )
|
|
251 exit ) exit
|
7
|
252 -}
|
|
253
|
8
|
254 --whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (c11 : ℕ) → (Code : Envc → t) → t
|
|
255 --whileTestP c10 n next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )
|
7
|
256
|
8
|
257 --whileTestPCall : (tree : rbt) → (n : ℕ) → Env
|
|
258 --whileTestPCall tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → merge env (λ env → init-col env (λ env → env ) ) ) )
|
|
259
|
|
260 whileTestPCall' : (tree : rbt) → (n : ℕ) → Env
|
|
261 whileTestPCall' tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → mergeP env (λ env → init-col env (λ env → env ) ) ) )
|
7
|
262
|
|
263
|
8
|
264 -- 以下test部分
|
|
265 test1 = whileTestPCall' bt-empty 0
|
|
266 test2 = whileTestPCall' (vart test1) 1
|
|
267 test3 = whileTestPCall' (vart test2) 2
|
|
268 test4 = whileTestPCall' (vart test3) 3
|
|
269 test5 = whileTestPCall' (vart test4) 4
|
|
270 test6 = whileTestPCall' (vart test5) 5
|
|
271 test7 = whileTestPCall' (vart test6) 6
|