|
0
|
1 open import Level renaming (suc to succ ; zero to Zero )
|
|
|
2 module RBTree where
|
|
|
3
|
|
|
4 -- {
|
|
|
5 -- RBTree,
|
|
|
6 -- Node,
|
|
|
7 -- Color,
|
|
|
8 -- hight,
|
|
|
9 -- nulln,
|
|
|
10 -- empty,
|
|
|
11 -- singleton
|
|
|
12 -- }
|
|
|
13
|
|
|
14 open import Data.List
|
|
|
15 open import Data.Maybe
|
|
|
16 open import Data.Nat
|
|
|
17 open import Data.Bool
|
|
|
18 open import Data.Empty
|
|
|
19 open import Relation.Binary.PropositionalEquality
|
|
|
20 open import Relation.Binary
|
|
|
21 open import Relation.Binary.Core
|
|
|
22 open import Relation.Nullary
|
|
|
23 -- open import Level
|
|
|
24
|
|
|
25 -- Builtin Function
|
|
|
26
|
|
|
27 _==_ : ℕ → ℕ → Bool
|
|
|
28 _==_ x y with compare x y
|
|
|
29 (x == .(ℕ.suc (x + k))) | less .x k = false
|
|
|
30 (x == .x) | equal .x = true
|
|
|
31 (.(ℕ.suc (y + k)) == y) | greater .y k = false
|
|
|
32
|
|
|
33 _-_ : ℕ → ℕ → ℕ
|
|
|
34 ℕ.zero - ℕ.zero = ℕ.zero
|
|
|
35 ℕ.zero - ℕ.suc y = ℕ.zero
|
|
|
36 ℕ.suc x - ℕ.zero = ℕ.suc x
|
|
|
37 ℕ.suc x - ℕ.suc y = x - y
|
|
|
38
|
|
|
39 contraposition : {m : Level } {A B : Set m} → (B → A) → (¬ A → ¬ B)
|
|
|
40 contraposition f = λ x y → x (f y)
|
|
|
41
|
|
|
42
|
|
|
43 compareTri1 : (n : ℕ) → zero <′ suc n
|
|
|
44 compareTri1 zero = ≤′-refl
|
|
|
45 compareTri1 (suc n) = ≤′-step ( compareTri1 n )
|
|
|
46
|
|
|
47 compareTri2 : (n m : ℕ) → n ≤′ m → suc n ≤′ suc m
|
|
|
48 compareTri2 _ _ ≤′-refl = ≤′-refl
|
|
|
49 compareTri2 n (suc m) ( ≤′-step p ) = ≤′-step { suc n } ( compareTri2 n m p )
|
|
|
50
|
|
|
51 <′dec : Set
|
|
|
52 <′dec = ∀ m n → Dec ( m ≤′ n )
|
|
|
53
|
|
|
54 compareTri6 : ∀ m {n} → ¬ m ≤′ n → ¬ suc m ≤′ suc n
|
|
|
55
|
|
|
56 is≤′ : <′dec
|
|
|
57 is≤′ zero zero = yes ≤′-refl
|
|
|
58 is≤′ zero (suc n) = yes (lemma n)
|
|
|
59 where
|
|
|
60 lemma : (n : ℕ) → zero ≤′ suc n
|
|
|
61 lemma zero = ≤′-step ≤′-refl
|
|
|
62 lemma (suc n) = ≤′-step (lemma n)
|
|
|
63 is≤′ (suc m) (zero) = no ( λ () )
|
|
|
64 is≤′ (suc m) (suc n) with is≤′ m n
|
|
|
65 ... | yes p = yes ( compareTri2 _ _ p )
|
|
|
66 ... | no p = no ( compareTri6 _ p )
|
|
|
67
|
|
|
68 compareTri20 : {n : ℕ} → ¬ suc n ≤′ zero
|
|
|
69 compareTri20 ()
|
|
|
70
|
|
|
71
|
|
|
72 compareTri21 : (n m : ℕ) → suc n ≤′ suc m → n ≤′ m
|
|
|
73 compareTri21 _ _ ≤′-refl = ≤′-refl
|
|
|
74 compareTri21 (suc n) zero ( ≤′-step p ) = compareTri23 (suc n) ( ≤′-step p ) p
|
|
|
75 where
|
|
|
76 compareTri23 : (n : ℕ) → suc n ≤′ suc zero → suc n ≤′ zero → n ≤′ zero
|
|
|
77 compareTri23 zero ( ≤′-step p ) _ = ≤′-refl
|
|
|
78 compareTri23 zero ≤′-refl _ = ≤′-refl
|
|
|
79 compareTri23 (suc n1) ( ≤′-step p ) ()
|
|
|
80 compareTri21 n (suc m) ( ≤′-step p ) = ≤′-step (compareTri21 _ _ p)
|
|
|
81 compareTri21 zero zero ( ≤′-step p ) = ≤′-refl
|
|
|
82
|
|
|
83
|
|
|
84 compareTri3 : ∀ m {n} → ¬ m ≡ suc (m + n)
|
|
|
85 compareTri3 zero ()
|
|
|
86 compareTri3 (suc m) eq = compareTri3 m (cong pred eq)
|
|
|
87
|
|
|
88 compareTri4' : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
|
|
|
89 compareTri4' m {n} with n Data.Nat.≟ m
|
|
|
90 ... | yes refl = λ x y → x refl
|
|
|
91 ... | no p = λ x y → p ( cong pred y )
|
|
|
92
|
|
|
93 compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
|
|
|
94 compareTri4 m = contraposition ( λ x → cong pred x )
|
|
|
95
|
|
|
96 -- compareTri6 : ∀ m {n} → ¬ m ≤′ n → ¬ suc m ≤′ suc n
|
|
|
97 compareTri6 m {n} = λ x y → x (compareTri21 _ _ y)
|
|
|
98
|
|
|
99 compareTri5 : ∀ m {n} → ¬ m <′ n → ¬ suc m <′ suc n
|
|
|
100 compareTri5 m {n} = compareTri6 (suc m)
|
|
|
101
|
|
|
102
|
|
|
103 compareTri : Trichotomous _≡_ _<′_
|
|
|
104 compareTri zero zero = tri≈ ( λ ()) refl ( λ ())
|
|
|
105 compareTri zero (suc n) = tri< ( compareTri1 n ) ( λ ()) ( λ ())
|
|
|
106 compareTri (suc n) zero = tri> ( λ ()) ( λ ()) ( compareTri1 n )
|
|
|
107 compareTri (suc n) (suc m) with compareTri n m
|
|
|
108 ... | tri< p q r = tri< (compareTri2 (suc n) m p ) (compareTri4 _ q) ( compareTri5 _ r )
|
|
|
109 ... | tri≈ p refl r = tri≈ (compareTri5 _ p) refl ( compareTri5 _ r )
|
|
|
110 ... | tri> p q r = tri> ( compareTri5 _ p ) (compareTri4 _ q) (compareTri2 (suc m) n r )
|
|
|
111
|
|
|
112
|
|
|
113 data Color : Set where
|
|
|
114 red : Color
|
|
|
115 black : Color
|
|
|
116
|
|
|
117 record Node {a : Set} : Set where
|
|
|
118 inductive
|
|
|
119 field
|
|
|
120 color : Color
|
|
|
121 blackHeight : ℕ
|
|
|
122 right : Node {a}
|
|
|
123 datum : ℕ
|
|
|
124 left : Node {a}
|
|
|
125 open Node
|
|
|
126
|
|
|
127 -- node は node であり 部分的に分けられた redblacktree そのもの
|
|
|
128
|
|
|
129 data RBTree {n : Level} (a : Set n) : Set n where
|
|
|
130 leaf : RBTree a
|
|
|
131 node : Color → ℕ → RBTree a → ℕ → RBTree a → RBTree a
|
|
|
132
|
|
|
133
|
|
|
134 record RBTreeBDel {n : Level} (a : Set n) : Set n where
|
|
|
135 field
|
|
|
136 tree : RBTree a
|
|
|
137 bool : Bool
|
|
|
138 open RBTreeBDel
|
|
|
139
|
|
|
140
|
|
|
141 module _ { n m : Level} {a : Set n} {cg : Set m} where
|
|
|
142 -- _,_ : (tree : RBTree a) → (b : Bool) → Set
|
|
|
143 -- leaf , false = (leaf , false)
|
|
|
144 -- leaf , true = {!!}
|
|
|
145 -- (node x x₁ t x₂ t₁) , bb = {!!}
|
|
|
146
|
|
|
147
|
|
|
148 hight? : RBTree a → ℕ
|
|
|
149 hight? leaf = 0
|
|
|
150 hight? (node c h l x r) = h
|
|
|
151
|
|
|
152 isLeaf : RBTree a → Bool
|
|
|
153 isLeaf leaf = true
|
|
|
154 isLeaf (node x x₁ t x₂ t₁) = false
|
|
|
155
|
|
|
156 empty : RBTree a
|
|
|
157 empty = leaf
|
|
|
158
|
|
|
159 singleton : ℕ → RBTree a
|
|
|
160 singleton x = (node black 1 leaf x leaf)
|
|
|
161
|
|
|
162 isMember : ℕ → RBTree ℕ → Bool
|
|
|
163 isMember _ leaf = false
|
|
|
164 isMember x (node _ _ l y r) with compare x y
|
|
|
165 isMember x (node _ _ l y r) | less x k = isMember x l
|
|
|
166 isMember x (node _ _ l x r) | equal x = true
|
|
|
167 isMember x (node _ _ l y r) | greater y k = isMember x r
|
|
|
168
|
|
|
169 blacks? : RBTree a → ℕ
|
|
|
170 blacks? = blacks' 0
|
|
|
171 where
|
|
|
172 blacks' : ℕ → RBTree a → ℕ
|
|
|
173 blacks' n leaf = (n + 1)
|
|
|
174 blacks' n (node red _ l _ r) = (blacks' n l) + (blacks' n r)
|
|
|
175 blacks' n (node black _ l _ r) = (blacks' (n + 1) l) + (blacks' (n + 1) r)
|
|
|
176
|
|
|
177 reds : Color → RBTree a → Bool
|
|
|
178 reds _ leaf = true
|
|
|
179 reds red (node x x₁ t x₂ t₁) = false
|
|
|
180 reds black (node c x₁ l x₂ r) = reds c l ∧ reds c r
|
|
|
181
|
|
|
182 turnR : RBTree a → (RBTree a → cg) → cg
|
|
|
183 turnR leaf cg = cg leaf
|
|
|
184 turnR (node _ h l x r) cg = cg (node red h l x r)
|
|
|
185
|
|
|
186 turnB : RBTree a → (RBTree a → cg) → cg
|
|
|
187 turnB leaf cg = cg leaf
|
|
|
188 turnB (node _ h l x r) cg = cg (node black h l x r)
|
|
|
189
|
|
|
190 minimum : RBTree ℕ → ℕ
|
|
|
191 minimum (node c h leaf x r) = x
|
|
|
192 minimum (node c h l x r) = minimum l
|
|
|
193 minimum leaf = 774
|
|
|
194
|
|
|
195 maximum : RBTree ℕ → ℕ
|
|
|
196 maximum (node c x₁ t x leaf) = x
|
|
|
197 maximum (node x x₁ t x₂ r) = maximum r
|
|
|
198 maximum leaf = 0
|
|
|
199
|
|
|
200 isRed : RBTree a → Bool
|
|
|
201 isRed (node red x₁ t x₂ t₁) = true
|
|
|
202 isRed _ = false
|
|
|
203
|
|
1
|
204 isColorSame : Color → Color → (Bool → cg) → cg
|
|
|
205 isColorSame red red cg = cg true
|
|
|
206 isColorSame red black cg = cg false
|
|
|
207 isColorSame black red cg = cg false
|
|
|
208 isColorSame black black cg = cg true
|
|
0
|
209
|
|
1
|
210 node→ℕ : Maybe (RBTree a) → Maybe ℕ
|
|
|
211 node→ℕ (just leaf) = nothing
|
|
|
212 node→ℕ (just (node x x₁ x₂ x₃ x₄)) = just x₃
|
|
|
213 node→ℕ nothing = nothing
|
|
0
|
214
|
|
|
215
|
|
|
216 -- basic operations
|
|
|
217 -- Code Gear Style (CPS : Contination Passing Style)
|
|
|
218
|
|
|
219 -- balance
|
|
|
220
|
|
|
221
|
|
1
|
222
|
|
|
223
|
|
0
|
224 module _ { n m : Level} {a : Set n} {cg : Set m} where
|
|
|
225
|
|
|
226 balanceL' : ℕ → RBTree a → ℕ → RBTree a → (RBTree a → cg) → cg
|
|
|
227 balanceL' h (node red h1 (node red hl a x b) y c) z d cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
|
|
|
228 balanceL' h (node red _ a x (node red _ b y c)) z d cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
|
|
|
229 balanceL' h l x r cg = cg (node black h l x r)
|
|
|
230
|
|
|
231 balanceR' : ℕ -> RBTree a -> ℕ -> RBTree a -> (RBTree a → cg) → cg
|
|
|
232 balanceR' h a x (node red _ b y (node red _ c z d)) cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
|
|
|
233 balanceR' h a x (node red _ (node red _ b y c) z d) cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
|
|
|
234 balanceR' h l x r cg = cg (node black h l x r)
|
|
|
235
|
|
|
236 balanceL : Color → ℕ → RBTree a → ℕ → RBTree a → (RBTree a → cg) → cg
|
|
|
237 balanceL black h (node red h1 (node red hl a x b) y c) z d cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
|
|
|
238 balanceL black h (node red _ a x (node red _ b y c)) z d cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
|
|
|
239 balanceL k h l x r cg = cg (node k h l x r)
|
|
|
240
|
|
|
241 balanceR : Color → ℕ -> RBTree a -> ℕ -> RBTree a -> (RBTree a → cg) → cg
|
|
|
242 balanceR black h a x (node red _ b y (node red _ c z d)) cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
|
|
|
243 balanceR black h a x (node red _ (node red _ b y c) z d) cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
|
|
|
244 balanceR k h l x r cg = cg (node k h l x r)
|
|
|
245
|
|
|
246 -- unbalance
|
|
|
247
|
|
|
248 -- unbalanceL' : Color → ℕ -> RBTree a -> a -> RBTree a -> (RBTreeBDel a → cg) → cg
|
|
1
|
249 -- unbalanceL' c h l@(node black _ _ _ _) x r cg = isColorSame c black ( λ issame → cg record { tree = {!!} ; bool = issame })
|
|
0
|
250 -- unbalanceL' c h l x r cg = {!!}
|
|
|
251
|
|
1
|
252 unbalanceL : Color → ℕ → RBTree a → ℕ → RBTree a → (RBTreeBDel a → cg) → cg
|
|
|
253 unbalanceL c h l@(node black _ _ _ _) x r cg = turnR l (λ tl → (balanceL black h tl x r (λ t → isColorSame {n} {m} {a} {_} c black (λ issame → cg record {tree = t ; bool = issame}))))
|
|
2
|
254 unbalanceL black h l@(node red lh ll lx lr@(node black _ _ _ _)) x r cg = turnR lr (λ tlr → balanceL black h tlr x r (λ t → cg record { tree = (node black lh ll lx t) ; bool = false}))
|
|
1
|
255 unbalanceL c h l x r cg = cg record {tree = leaf ; bool = false}
|
|
0
|
256
|
|
1
|
257 unbalanceR : Color → ℕ → RBTree a → ℕ → RBTree a → (RBTreeBDel a → cg) → cg
|
|
|
258 unbalanceR c h l x r@(node black _ _ _ _) cg = turnR r (λ tr → balanceR black h l x r (λ t → isColorSame {n} {m} {a} {_} c black (λ issame → cg record {tree = t ; bool = issame})))
|
|
2
|
259 unbalanceR black h l x (node red rh rl@(node black _ _ _ _) rx rr) cg = turnR rl (λ trl → balanceR black h l x trl (λ t → cg record { tree = (node black rh t rx rr); bool = false}))
|
|
1
|
260 unbalanceR c h l x r cg = cg record {tree = leaf ; bool = false}
|
|
0
|
261
|
|
|
262
|
|
|
263
|
|
|
264 {--
|
|
|
265 Insert Function
|
|
|
266
|
|
|
267 All Nodes → ℕ
|
|
|
268 search Insert Location → O(log ℕ)
|
|
|
269 fix Tree (balanceR,L) → O(log ℕ)
|
|
|
270 Root Child Color Fix → O(1)
|
|
|
271 Total → O(2 log ℕ + 1)
|
|
|
272 --}
|
|
|
273
|
|
|
274 -- turnRtree : RBTree a → (RBTree a → cg) → cg
|
|
|
275 -- turnRtree leaf cg = cg leaf
|
|
|
276 -- -- turnRtree (node black h l@(node black _ _ _ _) x r@(node black _ _ _ _)) cg = turnRtree (node red h l x r) cg
|
|
|
277 -- turnRtree (node c h l x r) cg = turnRtree r cg
|
|
|
278
|
|
|
279 rootChildFix : RBTree a → (RBTree a → cg) → cg
|
|
|
280 rootChildFix (node black h (node black lh ll@(node black llh lll llx llr) lx lr@(node black lrh lrl lrx lrr)) x (node black rh rl@(node black rlh rll rlx rlr) rx rr@(node black rrh rrl rrx rrr))) cg = cg (node black (h - 1) (node red (lh - 1) ll lx lr) x (node red (rh - 1) rl rx rr))
|
|
|
281 rootChildFix n cg = cg n
|
|
|
282
|
|
|
283 insert' : ℕ → RBTree a → (RBTree a → cg) → cg
|
|
|
284 insert' kx leaf cg = cg (node red 1 leaf kx leaf)
|
|
|
285
|
|
|
286 insert' kx (node black h l x r) cg with compare kx x
|
|
|
287 insert' kx (node black h l x r) cg | less kx k = insert' kx l (λ t → balanceL' h t x r (λ tt → cg tt))
|
|
|
288 insert' kx s@(node black h l x r) cg | equal kx = cg s
|
|
|
289 insert' kx (node black h l x r) cg | greater x k = insert' kx r (λ t → balanceR' h l x t (λ tt → cg tt))
|
|
|
290
|
|
|
291 insert' kx (node red h l x r) cg with compare kx x
|
|
|
292 insert' kx (node red h l x r) cg | less kx k = insert' kx l (λ t → cg (node red h t x r))
|
|
|
293 insert' kx s@(node red h l x r) cg | equal kx = cg s
|
|
|
294 insert' kx (node red h l x r) cg | greater x k = insert' kx r (λ t → cg (node red h l x t))
|
|
|
295
|
|
|
296 insert : ℕ → RBTree a → (RBTree a → cg) → cg
|
|
|
297 insert kx t cg = insert' kx t (λ t1 → turnB t1 (λ t2 → rootChildFix t2 cg))
|
|
|
298
|
|
|
299
|
|
|
300 get : ℕ → RBTree a → (Maybe (RBTree a) → cg) → cg
|
|
|
301 get x leaf cg = cg nothing
|
|
|
302 get x (node c h l x1 r) cg with compareTri x x1
|
|
|
303 get x (node c h l x1 r) cg | tri< a ¬b ¬c = get x l cg
|
|
|
304 get x t@(node c h l x1 r) cg | tri≈ ¬a b ¬c = cg (just t)
|
|
|
305 get x (node c h l x1 r) cg | tri> ¬a ¬b c₁ = get x r cg
|
|
|
306
|
|
|
307
|
|
|
308
|
|
|
309 {- Check Balance, Color rule and hight calc -}
|
|
|
310
|
|
|
311 -- create RBTree from Nat List
|
|
|
312 fromList : List ℕ → RBTree ℕ
|
|
|
313 fromList [] = empty {_} {_} {ℕ} {Set}
|
|
|
314 fromList (x ∷ l) = (maketree x (empty {_} {_} {ℕ} {Set}) (λ t → fromList' l t (λ tt → tt)))
|
|
|
315 where
|
|
|
316 module _ {l : Level} {cg1 : Set l} {a : Set} where
|
|
|
317 maketree : ℕ → RBTree a → (RBTree a → cg1) → cg1
|
|
|
318 maketree x t1 cg = insert x t1 cg
|
|
|
319 fromList' : List ℕ → RBTree a → (RBTree a → cg1) → cg1
|
|
|
320 fromList' [] t cg = cg t
|
|
|
321 fromList' (x1 ∷ nl) t cg = maketree x1 t (λ tt → fromList' nl tt (λ ttt → cg ttt))
|
|
|
322
|
|
|
323
|
|
|
324 c1 = fromList (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ 8 ∷ 9 ∷ [])
|
|
|
325 c2 = fromList (5 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 6 ∷ 7 ∷ 8 ∷ 9 ∷ [])
|
|
|
326 c3 = fromList (8 ∷ 7 ∷ 6 ∷ 1 ∷ 2 ∷ 5 ∷ 4 ∷ 3 ∷ 9 ∷ [])
|
|
|
327
|
|
|
328 cget = get 6 c1 (λ a → a)
|
|
|
329
|
|
|
330
|
|
1
|
331 proof-leaf : {l : Level} {D : Set l} (n : ℕ) → insert {_} {_} {ℕ} {Set} n leaf (λ t1 → get n t1 (λ n1 → (just n ≡ (node→ℕ {_} {_} {ℕ} {ℕ} n1))))
|
|
0
|
332 proof-leaf n with n Data.Nat.≟ n | compareTri n n
|
|
|
333 proof-leaf n | yes p | tri< a ¬b ¬c = ⊥-elim (¬b p)
|
|
|
334 proof-leaf n | yes p | tri≈ ¬a b ¬c = refl
|
|
|
335 proof-leaf n | yes p | tri> ¬a ¬b c = ⊥-elim (¬b p)
|
|
|
336 proof-leaf n | no ¬p | tri< a ¬b ¬c = ⊥-elim (¬c a)
|
|
|
337 proof-leaf n | no ¬p | tri≈ ¬a b ¬c = refl
|
|
|
338 proof-leaf n | no ¬p | tri> ¬a ¬b c = ⊥-elim (¬a c)
|
|
|
339
|
|
|
340
|
|
|
341
|
|
|
342
|
|
|
343 -- 任意の木だと insert でノードをどこに入れるか決められず計算が進まない
|
|
|
344 -- 任意の木の root が Nothing のケースはもちろんできる
|
|
|
345 -- proof1 : {l : Level} {D : Set l} (n : ℕ) → (t : RBTree D) → insert n t (λ t1 → get n t1 (λ n1 → (just n ≡ (root→ℕ n1))))
|
|
|
346 -- proof1 n t with n Data.Nat.≟ n | compareTri n n
|
|
|
347 -- proof1 n t | yes p | tri< a ¬b ¬c = ⊥-elim (¬b p)
|
|
|
348 -- proof1 n t | yes p | tri> ¬a ¬b c = ⊥-elim (¬b p)
|
|
|
349 -- proof1 n t | no ¬p | tri< a ¬b ¬c = ⊥-elim (¬c a)
|
|
|
350 -- proof1 n t | no ¬p | tri> ¬a ¬b c = ⊥-elim (¬a c)
|
|
|
351 -- proof1 n leaf | yes p | tri≈ ¬a b ¬c with compareTri n n
|
|
|
352 -- proof1 n leaf | yes p | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b p)
|
|
|
353 -- proof1 n leaf | yes p | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl
|
|
|
354 -- proof1 n leaf | yes p | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b p)
|
|
|
355 -- proof1 n (node x x₁ t x₂ t₁) | yes p | tri≈ ¬a b ¬c = {!!}
|
|
|
356 -- proof1 n t | no ¬p | tri≈ ¬a b ¬c = {!!}
|
|
|
357
|
|
|
358
|
|
|
359 {--
|
|
|
360 書くなら全ての探索が木の高さ分で終わることを証明しとく必要がありそう
|
|
|
361 あと探索で木の高さが消化されていくことも示す
|
|
|
362 stack の push は存在してるデータ構造に関係なく上に乗るから任意のstack で証明できる
|
|
|
363 Tree でデータの保存を確かめるには…？
|
|
|
364
|
|
|
365 tree で証明するくらいだったら、親子関係、
|
|
|
366 rb 含めると、色関係、枝の長さ、になりそう?
|
|
|
367 --}
|
|
|
368
|
|
1
|
369 module _ { n m : Level} {a : Set n} {cg : Set m} where
|
|
0
|
370
|
|
1
|
371 {--
|
|
|
372 deleteMin' は後ろに bool(Color の変更情報?)を持ちながら再帰する
|
|
|
373 再帰に一つ関数が挟まってるけど互いに呼んでるからどう書くべきかわからん
|
|
|
374
|
|
|
375 ```Haskell Source
|
|
|
376 deleteMin' (Node c h l x r) = if d then (tD, m) else (tD', m)
|
|
|
377
|
|
|
378 ((l', d), m) = deleteMin' l
|
|
|
379 tD = unbalancedR c (h-1) l' x r
|
|
|
380 tD' = (Node c h l' x r, False)
|
|
|
381 ```
|
|
|
382
|
|
|
383 たぶん ((l', d), m) の形になると deleteMin' がしたい
|
|
2
|
384 ~~RBTreeBDel の bool 情報はleaf に着いたかどうかだけ~~ → ではなく unbalance する必要があるのかの確認
|
|
|
385
|
|
|
386 ん、じゃあ node の左に leaf がついてる最小パターン探せばいいのでは？
|
|
1
|
387
|
|
2
|
388 あるパターンは (leaf x leaf), (leaf x r) の2パターンと r が red のケースを含めて 3パターン
|
|
|
389 その上のノードからそれを確認すれば良いので
|
|
|
390 (node c h (node lc lh leaf lx leaf) x r) と lr が存在するケースを確認すると良い
|
|
|
391 終わった tree に対して unbalance するかしないかを確定させたら終わり
|
|
1
|
392 --}
|
|
|
393
|
|
2
|
394
|
|
|
395
|
|
1
|
396 {-# TERMINATING #-}
|
|
|
397 deleteMin' : RBTree ℕ → (RBTreeBDel ℕ → cg) → cg
|
|
0
|
398
|
|
2
|
399 deleteMin' leaf cg = cg record {tree = leaf ; bool = false} -- unreachable case
|
|
1
|
400 deleteMin' (node black _ leaf x leaf) cg = cg record {tree = leaf ; bool = true}
|
|
|
401 deleteMin' (node black _ leaf x r@(node red _ _ _ _)) cg = turnB r (λ tr → cg record {tree = tr ; bool = false})
|
|
|
402 deleteMin' (node red _ leaf x r) cg = cg record {tree = r ; bool = false}
|
|
|
403 deleteMin' (node c h l x r) cg = deleteMin' l (λ dt → delCheck {n} {m} {a} dt (λ dct → cg dct))
|
|
|
404 where
|
|
|
405 delCheck : { n m : Level} {a : Set n} {cg : Set m} → RBTreeBDel ℕ → (RBTreeBDel ℕ → cg) → cg
|
|
|
406 delCheck bt cg with (bool bt)
|
|
|
407 delCheck record { tree = leaf ; bool = b } cg | false = cg record {tree = (node red 100 leaf 100 leaf) ; bool = b } -- unreachable case
|
|
2
|
408 delCheck record { tree = leaf ; bool = b } cg | true = unbalanceR c (h - 1) leaf x r (λ result → cg result)
|
|
|
409 -- delCheck record { tree = (node x₁ x₂ t₁ x₃ t₂) ; bool = b } cg | false = cg record {tree = (node x₁ x₂ t₁ x₃ t₂) ; bool = false}
|
|
|
410 delCheck record { tree = (node x₁ x₂ t₁ x₃ t₂) ; bool = b } cg | _ = unbalanceR c (h - 1) (node x₁ x₂ t₁ x₃ t₂) x r (λ result → cg result)
|
|
0
|
411
|
|
1
|
412 {--
|
|
|
413 deleteMin では最後に帰ってきたやつを turnB
|
|
|
414 型は rbtree → (rbtree → cg) → cg
|
|
|
415
|
|
|
416 rbtree が tree のとき deleteMin' tree
|
|
|
417 ((s, _), _) は RBTreeBDel から RBTree への変換なので outPutTree
|
|
|
418 --}
|
|
2
|
419
|
|
1
|
420 deleteMin : RBTree ℕ → (RBTree ℕ → cg) → cg
|
|
|
421 deleteMin leaf cg = cg leaf
|
|
|
422 deleteMin tree cg = deleteMin' tree (λ dt → outPutTree {n} {m} {a} dt (λ dct → turnB dct (λ dctb → cg dctb)))
|
|
|
423 where
|
|
|
424 outPutTree : { n m : Level} {a : Set n} {cg : Set m} → RBTreeBDel ℕ → (RBTree ℕ → cg) → cg
|
|
|
425 outPutTree record { tree = s ; bool = b } cg = cg s
|
|
0
|
426
|
|
|
427
|
|
2
|
428 -- > delCheck の node があって false のケースも unbalanceしなきゃいけなかった
|
|
|
429 d1 = deleteMin (fromList (3 ∷ 1 ∷ 2 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ []))
|
|
|
430 l1 = fromList (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ [])
|
|
|
431 l2 = fromList ( 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ [])
|
|
|
432 d2 = deleteMin (fromList ( 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ []))
|
|
0
|
433
|
|
|
434
|
|
|
435 -- delete' : {a : Set} → ℕ → RBTree ℕ → RBTreeBDel ℕ
|
|
|
436 -- delete' _ leaf = record { t = leaf ; b = false}
|
|
|
437 -- delete' x (node c h l y r) with compare x y
|
|
|
438 -- delete' x (node c h l y r) | less .x k = delCheck (delete' {ℕ} x l)
|
|
|
439 -- where
|
|
|
440 -- delCheck : RBTreeBDel ℕ → RBTreeBDel ℕ
|
|
|
441 -- delCheck bt with (b bt)
|
|
|
442 -- delCheck record { t = leaf ; b = b } | false = record {t = (node red 100 leaf 100 leaf) ; b = b } -- unreachable case
|
|
|
443 -- delCheck record { t = leaf ; b = b } | true = unbalanceR {ℕ} c (h - 1) leaf x r
|
|
|
444 -- delCheck record { t = (node x₁ x₂ t₁ x₃ t₂) ; b = b } | false = deleteMin' (node x₁ x₂ t₁ x₃ t₂)
|
|
|
445 -- delCheck record { t = (node x₁ (x₂) t₁ x₃ t₂) ; b = b } | true = unbalanceR {ℕ} c (h - 1) (node x₁ x₂ t₁ x₃ t₂) x r
|
|
|
446 -- delete' x (node c h l y r) | greater .y k = delCheck (delete' {ℕ} x r)
|
|
|
447 -- where
|
|
|
448 -- delCheck : RBTreeBDel ℕ → RBTreeBDel ℕ
|
|
|
449 -- delCheck bt with (b bt)
|
|
|
450 -- delCheck record { t = leaf ; b = b } | false = record {t = (node red 100 leaf 100 leaf) ; b = b } -- unreachable case
|
|
|
451 -- delCheck record { t = leaf ; b = b } | true = unbalanceR {ℕ} c (h - 1) leaf x r
|
|
|
452 -- delCheck record { t = (node x₁ x₂ t₁ x₃ t₂) ; b = b } | false = deleteMin' (node x₁ x₂ t₁ x₃ t₂)
|
|
|
453 -- delCheck record { t = (node x₁ (x₂) t₁ x₃ t₂) ; b = b } | true = unbalanceR {ℕ} c (h - 1) (node x₁ x₂ t₁ x₃ t₂) x r
|
|
|
454 -- delete' x (node c h l .x leaf) | equal .x with checkColor {ℕ} c black
|
|
|
455 -- delete' x (node c h l .x leaf) | equal .x | false = record {t = l ; b = false}
|
|
|
456 -- delete' x (node c h l .x leaf) | equal .x | true = blackify l
|
|
|
457 -- where
|
|
|
458 -- blackify : RBTree ℕ → RBTreeBDel ℕ
|
|
|
459 -- blackify (node red x₂ a x₃ a₁) = record {t = turnB {ℕ} (node red x₂ a x₃ a₁) ; b = false}
|
|
|
460 -- blackify s = record {t = s; b = true}
|
|
|
461 -- delete' x (node c h l .x (node x₁ x₂ r x₃ r₁)) | equal .x with r
|
|
|
462 -- delete' x (node c h l .x (node x₁ x₂ r x₃ r₁)) | equal .x | leaf with checkColor {ℕ} c black
|
|
|
463 -- delete' x (node c h l .x (node x₁ x₂ r x₃ r₁)) | equal .x | leaf | false = blackify l
|
|
|
464 -- where
|
|
|
465 -- blackify : RBTree ℕ → RBTreeBDel ℕ
|
|
|
466 -- blackify (node red x₂ a x₃ a₁) = record {t = turnB {ℕ} (node red x₂ a x₃ a₁) ; b = false}
|
|
|
467 -- blackify s = record {t = s; b = true}
|
|
|
468 -- delete' x (node c h l .x (node x₁ x₂ r x₃ r₁)) | equal .x | leaf | true = record {t = l ; b = false}
|
|
|
469 -- delete' x (node c h l .x (node x₁ x₂ r x₃ r₁)) | equal .x | node x₄ x₅ rnod x₆ rnod₁ = {!!}
|
|
|
470
|
|
|
471 -- -- where
|
|
|
472 -- -- delCheck : RBTreeBDel ℕ → RBTreeBDel ℕ
|
|
|
473 -- -- delCheck bt with (b bt)
|
|
|
474 -- -- delCheck record { t = leaf ; b = b } | false = record {t = (node red 100 leaf 100 leaf) ; b = b } -- unreachable case
|
|
|
475 -- -- delCheck record { t = leaf ; b = b } | true = unbalanceR {ℕ} c (h - 1) leaf x r
|
|
|
476 -- -- delCheck record { t = (node x₁ x₂ t₁ x₃ t₂) ; b = b } | false = deleteMin' (node x₁ x₂ t₁ x₃ t₂)
|
|
|
477 -- -- delCheck record { t = (node x₁ (x₂) t₁ x₃ t₂) ; b = b } | true = unbalanceR {ℕ} c (h - 1) (node x₁ x₂ t₁ x₃ t₂) x r
|
|
|
478 -- -- 謎フラグがtrue なら バランスしろとのお達しなのでどっかで持ちましょうはい。
|
|
|
479 -- -- 多分 record で適当に持つのがよいっぽい
|
|
|
480
|
|
|
481 -- delete : {a : Set} → ℕ → RBTree ℕ → RBTree ℕ
|
|
|
482 -- delete kx t = turnB {ℕ} (outPutTree (delete' {ℕ} kx t))
|
|
|
483 -- where
|
|
|
484 -- outPutTree : RBTreeBDel ℕ → RBTree ℕ
|
|
|
485 -- outPutTree record { t = s ; b = b } = s
|
|
|
486
|
|
|
487 -- proofs
|
|
|
488 -- isOrdered : RBTree a → Bool
|
|
|
489 -- isOrdered t = {!!}
|
|
|
490
|
|
|
491 -- isBlackSame : RBTree a → Bool
|
|
|
492 -- isBlackSame t = {!!}
|
|
|
493
|
|
|
494 -- isBalanced : RBTree a → Bool
|
|
|
495 -- isBalanced t = {!!}
|
