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