|
781
|
1 module work where
|
|
|
2 open import Level hiding (suc ; zero ; _⊔_ )
|
|
|
3
|
|
|
4 open import Data.Nat hiding (compare)
|
|
|
5 open import Data.Nat.Properties as NatProp
|
|
|
6 open import Data.Maybe
|
|
|
7 -- open import Data.Maybe.Properties
|
|
|
8 open import Data.Empty
|
|
|
9 open import Data.List
|
|
|
10 open import Data.Product
|
|
|
11
|
|
|
12 open import Function as F hiding (const)
|
|
|
13
|
|
|
14 open import Relation.Binary
|
|
|
15 open import Relation.Binary.PropositionalEquality
|
|
|
16 open import Relation.Nullary
|
|
|
17 open import logic
|
|
|
18
|
|
|
19 data bt {n : Level} (A : Set n) : Set n where
|
|
|
20 leaf : bt A
|
|
|
21 node : (key : ℕ) → (value : A) → (left : bt A) → (right : bt A) → bt A
|
|
|
22
|
|
|
23 node-key : {n : Level}{A : Set n} → bt A → Maybe ℕ
|
|
|
24 node-key leaf = nothing
|
|
|
25 node-key (node key value tree tree₁) = just key
|
|
|
26
|
|
|
27 node-value : {n : Level} {A : Set n} → bt A → Maybe A
|
|
|
28 node-value leaf = nothing
|
|
|
29 node-value (node key value tree tree₁) = just value
|
|
|
30
|
|
|
31 bt-depth : {n : Level} {A : Set n} → (tree : bt A) → ℕ
|
|
|
32 bt-depth leaf = 0
|
|
|
33 bt-depth (node key value tree tree₁) = suc (bt-depth tree ⊔ bt-depth tree₁)
|
|
|
34 --一番下のleaf =0から戻るたびにsucをしていく
|
|
|
35 treeTest1 : bt ℕ
|
|
|
36 treeTest1 = node 0 0 leaf (node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf))
|
|
|
37
|
|
|
38 -- 0 0
|
|
|
39 -- / \
|
|
|
40 -- leaf 3 1
|
|
|
41 -- / \
|
|
|
42 -- 2 5 2
|
|
|
43 -- / \
|
|
|
44 -- 1 leaf 3
|
|
|
45 -- / \
|
|
|
46 -- leaf leaf 4
|
|
|
47
|
|
|
48 treeTest2 : bt ℕ
|
|
|
49 treeTest2 = node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf)
|
|
|
50
|
|
|
51 testdb : ℕ
|
|
|
52 testdb = bt-depth treeTest1 -- 4
|
|
|
53
|
|
|
54 import Data.Unit hiding ( _≟_ ; _≤?_ ; _≤_)
|
|
|
55
|
|
|
56 data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
|
|
|
57 t-leaf : treeInvariant leaf
|
|
|
58
|
|
|
59 t-single : (key : ℕ) → (value : A) → treeInvariant (node key value leaf leaf)
|
|
|
60
|
|
|
61 t-left : {key key1 : ℕ} → {value value1 : A} → {t1 t2 : bt A} → key < key1
|
|
|
62 → treeInvariant (node key value t1 t2)
|
|
|
63 → treeInvariant (node key1 value1 (node key value t1 t2) leaf)
|
|
|
64
|
|
|
65 t-right : {key key1 : ℕ} → {value value1 : A} → {t1 t2 : bt A} → key < key1
|
|
|
66 → treeInvariant (node key1 value1 t1 t2)
|
|
|
67 → treeInvariant (node key value leaf (node key1 value1 t1 t2))
|
|
|
68
|
|
|
69 t-node : {key key1 key2 : ℕ}→ {value value1 value2 : A} → {t1 t2 t3 t4 : bt A} → key1 < key → key < key2
|
|
|
70 → treeInvariant (node key1 value1 t1 t2)
|
|
|
71 → treeInvariant (node key2 value2 t3 t4)
|
|
|
72 → treeInvariant (node key value (node key1 value1 t1 t2) (node key2 value2 t3 t4))
|
|
|
73
|
|
|
74 data stackInvariant {n : Level} {A : Set n} (key : ℕ ) : (top orig : bt A)
|
|
|
75 → (stack : List (bt A)) → Set n where
|
|
|
76 s-nil : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [] )
|
|
|
77
|
|
|
78 s-right : {key1 : ℕ } → {value : A } → {tree0 t1 t2 : bt A } → {st : List (bt A)}
|
|
|
79 → key1 < key
|
|
|
80 → stackInvariant key (node key1 value t1 t2) tree0 st
|
|
|
81 → stackInvariant key t2 tree0 (t2 ∷ st)
|
|
|
82
|
|
|
83 s-left : {key1 : ℕ } → {value : A } → {tree0 t1 t2 : bt A } → {st : List (bt A)}
|
|
|
84 → key < key1
|
|
|
85 → stackInvariant key (node key1 value t1 t2) tree0 st
|
|
|
86 → stackInvariant key t1 tree0 (t1 ∷ st)
|
|
|
87
|
|
|
88 data replacedTree {n : Level } {A : Set n} (key : ℕ) (value : A) : (before after : bt A) → Set n where
|
|
|
89 r-leaf : replacedTree key value leaf (node key value leaf leaf)
|
|
|
90
|
|
783
|
91 r-node : {value₁ : A} → {left right : bt A} → replacedTree key value (node key value₁ left right) (node key value left right)
|
|
781
|
92
|
|
|
93 -- key is the repl's key , so need comp key and key1
|
|
|
94 r-left : {key1 : ℕ} {value1 : A }→ {left right repl : bt A} → key < key1
|
|
|
95 → replacedTree key value left repl → replacedTree key value (node key1 value1 left right) (node key1 value1 repl right)
|
|
|
96
|
|
|
97 r-right : {key1 : ℕ } {value1 : A} → {left right repl : bt A} → key1 < key
|
|
|
98 → replacedTree key value right repl → replacedTree key value (node key1 value1 left right) (node key1 value1 left repl)
|
|
|
99
|
|
783
|
100
|
|
781
|
101 depth-1< : {i j : ℕ} → suc i ≤ suc (i Data.Nat.⊔ j )
|
|
|
102 depth-1< {i} {j} = s≤s (m≤m⊔n _ j)
|
|
|
103 depth-2< : {i j : ℕ} → suc i ≤ suc (j Data.Nat.⊔ i )
|
|
|
104 depth-2< {i} {j} = s≤s (m≤n⊔m j i)
|
|
|
105 depth-3< : {i : ℕ } → suc i ≤ suc (suc i)
|
|
|
106 depth-3< {zero} = s≤s ( z≤n )
|
|
|
107 depth-3< {suc i} = s≤s (depth-3< {i} )
|
|
|
108
|
|
|
109 treeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} → (tleft tright : bt A)
|
|
|
110 → treeInvariant (node key value tleft tright)
|
|
|
111 → treeInvariant tleft
|
|
|
112 treeLeftDown leaf leaf (t-single key value) = t-leaf
|
|
|
113 treeLeftDown leaf (node key value t1 t2) (t-right x ti) = t-leaf
|
|
|
114 treeLeftDown (node key value t t₁) leaf (t-left x ti) = ti
|
|
|
115 treeLeftDown (node key value t t₁) (node key₁ value₁ t1 t2) (t-node x x1 ti ti2 ) = ti
|
|
|
116
|
|
|
117 treeRightDown : {n : Level} {A : Set n} {key : ℕ} {value : A} → (tleft tright : bt A)
|
|
|
118 → treeInvariant (node key value tleft tright)
|
|
|
119 → treeInvariant tright
|
|
|
120 treeRightDown leaf leaf (t-single key value) = t-leaf
|
|
|
121 treeRightDown leaf (node key value t1 t2) (t-right x ti) = ti
|
|
|
122
|
|
|
123 treeRightDown (node key value t t₁) leaf (t-left x ti) = t-leaf
|
|
|
124 treeRightDown (node key value t t₁) (node key₁ value₁ t1 t2) (t-node x x1 ti ti2 ) = ti2
|
|
|
125
|
|
|
126
|
|
|
127 findP : {n m : Level} {A : Set n} {t : Set n} → (tkey : ℕ) → (top orig : bt A) → (st : List (bt A))
|
|
|
128 → (treeInvariant top)
|
|
|
129 → stackInvariant tkey top orig st
|
|
|
130 → (next : (newtop : bt A) → (stack : List (bt A))
|
|
|
131 → (treeInvariant newtop)
|
|
|
132 → (stackInvariant tkey newtop orig stack)
|
|
|
133 → bt-depth newtop < bt-depth top → t)
|
|
|
134 → (exit : (newtop : bt A) → (stack : List (bt A))
|
|
|
135 → (treeInvariant newtop)
|
|
|
136 → (stackInvariant tkey newtop orig stack) --need new stack ?
|
|
|
137 → (newtop ≡ leaf) ∨ (node-key newtop ≡ just tkey) → t)
|
|
|
138 → t
|
|
|
139 findP tkey leaf orig st ti si next exit = exit leaf st ti si (case1 refl)
|
|
|
140 findP tkey (node key value tl tr) orig st ti si next exit with <-cmp tkey key
|
|
|
141 findP tkey top orig st ti si next exit | tri≈ ¬a refl ¬c = exit top st ti si (case2 refl)
|
|
|
142 findP tkey (node key value tl tr) orig st ti si next exit | tri< a ¬b ¬c = next tl (tl ∷ st) (treeLeftDown tl tr ti) (s-left a si) (s≤s (m≤m⊔n (bt-depth tl) (bt-depth tr)))
|
|
|
143
|
|
|
144 findP tkey (node key value tl tr) orig st ti si next exit | tri> ¬a ¬b c = next tr (tr ∷ st) (treeRightDown tl tr ti) (s-right c si) (s≤s (m≤n⊔m (bt-depth tl) (bt-depth tr)))
|
|
|
145
|
|
|
146
|
|
|
147 --RBT
|
|
|
148 data Color : Set where
|
|
|
149 Red : Color
|
|
|
150 Black : Color
|
|
|
151
|
|
|
152 RB→bt : {n : Level} (A : Set n) → (bt (Color ∧ A)) → bt A
|
|
|
153 RB→bt {n} A leaf = leaf
|
|
|
154 RB→bt {n} A (node key ⟪ C , value ⟫ tr t1) = (node key value (RB→bt A tr) (RB→bt A t1))
|
|
|
155
|
|
|
156 color : {n : Level} {A : Set n} → (bt (Color ∧ A)) → Color
|
|
|
157 color leaf = Black
|
|
|
158 color (node key ⟪ C , value ⟫ rb rb₁) = C
|
|
|
159
|
|
|
160 black-depth : {n : Level} {A : Set n} → (tree : bt (Color ∧ A) ) → ℕ
|
|
|
161 black-depth leaf = 0
|
|
|
162 black-depth (node key ⟪ Red , value ⟫ t t₁) = black-depth t ⊔ black-depth t₁
|
|
|
163 black-depth (node key ⟪ Black , value ⟫ t t₁) = suc (black-depth t ⊔ black-depth t₁ )
|
|
|
164
|
|
|
165 data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where
|
|
|
166 rb-leaf : RBtreeInvariant leaf
|
|
|
167 rb-single : (key : ℕ) → (value : A) → RBtreeInvariant (node key ⟪ Black , value ⟫ leaf leaf)
|
|
|
168 rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁
|
|
|
169 → black-depth t ≡ black-depth t₁
|
|
|
170 → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁)
|
|
|
171 → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key₁ ⟪ Black , value₁ ⟫ t t₁))
|
|
|
172 rb-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {c : Color}
|
|
|
173 → black-depth t ≡ black-depth t₁
|
|
|
174 → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁)
|
|
|
175 → RBtreeInvariant (node key ⟪ Black , value ⟫ leaf (node key₁ ⟪ c , value₁ ⟫ t t₁))
|
|
|
176 rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁
|
|
|
177 → black-depth t ≡ black-depth t₁
|
|
|
178 → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁)
|
|
|
179 → RBtreeInvariant (node key ⟪ Red , value ⟫ (node key₁ ⟪ Black , value₁ ⟫ t t₁) leaf )
|
|
|
180 rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {c : Color}
|
|
|
181 → black-depth t ≡ black-depth t₁
|
|
|
182 → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁)
|
|
|
183 → RBtreeInvariant (node key ⟪ Black , value ⟫ (node key₁ ⟪ c , value₁ ⟫ t t₁) leaf)
|
|
|
184 rb-node-red : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂
|
|
|
185 → black-depth t₁ ≡ black-depth t₂
|
|
|
186 → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ t₂)
|
|
|
187 → black-depth t₃ ≡ black-depth t₄
|
|
|
188 → RBtreeInvariant (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)
|
|
|
189 → RBtreeInvariant (node key₁ ⟪ Red , value₁ ⟫ (node key ⟪ Black , value ⟫ t₁ t₂) (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄))
|
|
|
190 rb-node-black : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂
|
|
|
191 → {c c₁ : Color}
|
|
|
192 → black-depth t₁ ≡ black-depth t₂
|
|
|
193 → RBtreeInvariant (node key ⟪ c , value ⟫ t₁ t₂)
|
|
|
194 → black-depth t₃ ≡ black-depth t₄
|
|
|
195 → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)
|
|
|
196 → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄))
|
|
|
197
|
|
|
198
|
|
|
199 data rotatedTree {n : Level} {A : Set n} : (before after : bt A) → Set n where
|
|
|
200 rtt-node : {t : bt A } → rotatedTree t t
|
|
|
201 -- a b
|
|
|
202 -- b c d a
|
|
|
203 -- d e e c
|
|
|
204 --
|
|
|
205 rtt-right : {ka kb kc kd ke : ℕ} {va vb vc vd ve : A} → {c d e c1 d1 e1 : bt A} → {ctl ctr dtl dtr etl etr : bt A}
|
|
|
206 --kd < kb < ke < ka< kc
|
|
|
207 → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A}
|
|
|
208 → kd < kb → kb < ke → ke < ka → ka < kc
|
|
|
209 → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1)
|
|
|
210 → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1)
|
|
|
211 → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1)
|
|
|
212 → rotatedTree (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr))
|
|
|
213 (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1)))
|
|
|
214
|
|
|
215 rtt-left : {ka kb kc kd ke : ℕ} {va vb vc vd ve : A} → {c d e c1 d1 e1 : bt A} → {ctl ctr dtl dtr etl etr : bt A}
|
|
|
216 --kd < kb < ke < ka< kc
|
|
|
217 → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A} -- after child
|
|
|
218 → kd < kb → kb < ke → ke < ka → ka < kc
|
|
|
219 → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1)
|
|
|
220 → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1)
|
|
|
221 → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1)
|
|
|
222 → rotatedTree (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1)))
|
|
|
223 (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr))
|
|
|
224
|
|
|
225 RBtreeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color}
|
|
|
226 → (tleft tright : bt (Color ∧ A))
|
|
|
227 → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright)
|
|
|
228 → RBtreeInvariant tleft
|
|
|
229 RBtreeLeftDown leaf leaf (rb-single k1 v) = rb-leaf
|
|
|
230 RBtreeLeftDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-red x bde rbti) = rb-leaf
|
|
|
231 RBtreeLeftDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-black x bde rbti) = rb-leaf
|
|
|
232 RBtreeLeftDown leaf (node key ⟪ Red , value ⟫ t1 t2 ) (rb-right-black x bde rbti)= rb-leaf
|
|
|
233 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti
|
|
|
234 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti)= ti
|
|
|
235 RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti
|
|
|
236 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til
|
|
|
237 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til bde2 tir) = til
|
|
|
238 RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til
|
|
|
239 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til
|
|
|
240 RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til
|
|
|
241
|
|
|
242 RBtreeRightDown : {n : Level} {A : Set n} { key : ℕ} {value : A} {c : Color}
|
|
|
243 → (tleft tright : bt (Color ∧ A))
|
|
|
244 → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright)
|
|
|
245 → RBtreeInvariant tright
|
|
|
246 RBtreeRightDown leaf leaf (rb-single k1 v1 ) = rb-leaf
|
|
|
247 RBtreeRightDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-red x bde rbti) = rbti
|
|
|
248 RBtreeRightDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-black x bde rbti) = rbti
|
|
|
249 RBtreeRightDown leaf (node key ⟪ Red , value ⟫ t1 t2 ) (rb-right-black x bde rbti)= rbti
|
|
|
250 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf
|
|
|
251 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti) = rb-leaf
|
|
|
252 RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf
|
|
|
253 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir
|
|
|
254 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til bde2 tir) = tir
|
|
|
255 RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir
|
|
|
256 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir
|
|
|
257 RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir
|
|
|
258
|
|
|
259 findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) )
|
|
|
260 → (stack : List (bt (Color ∧ A)))
|
|
|
261 → treeInvariant tree ∧ stackInvariant key tree tree0 stack
|
|
|
262 → RBtreeInvariant tree
|
|
|
263 → (next : (tree1 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A)))
|
|
|
264 → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
|
|
|
265 → RBtreeInvariant tree1
|
|
|
266 → bt-depth tree1 < bt-depth tree → t )
|
|
|
267 → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A)))
|
|
|
268 → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
|
|
|
269 → RBtreeInvariant tree1
|
|
|
270 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t
|
|
|
271 findRBT key leaf tree0 stack ti rb0 next exit = exit leaf stack ti rb0 (case1 refl)
|
|
|
272 findRBT key n@(node key₁ value left right) tree0 stack ti rb0 next exit with <-cmp key key₁
|
|
|
273 findRBT key (node key₁ value left right) tree0 stack ti rb0 next exit | tri< a ¬b ¬c
|
|
|
274 = next left (left ∷ stack) ⟪ treeLeftDown left right (_∧_.proj1 ti) , s-left a (_∧_.proj2 ti) ⟫ (RBtreeLeftDown left right rb0) depth-1<
|
|
|
275 findRBT key n tree0 stack ti rb0 _ exit | tri≈ ¬a refl ¬c = exit n stack ti rb0 (case2 refl)
|
|
|
276 findRBT key (node key₁ value left right) tree0 stack ti rb0 next exit | tri> ¬a ¬b c
|
|
|
277 = next right (right ∷ stack) ⟪ treeRightDown left right (_∧_.proj1 ti), s-right c (_∧_.proj2 ti) ⟫ (RBtreeRightDown left right rb0) depth-2<
|
|
|
278
|
|
|
279 child-replaced : {n : Level} {A : Set n} (key : ℕ) (tree : bt A) → bt A
|
|
|
280 child-replaced key leaf = leaf
|
|
|
281 child-replaced key (node key₁ value left right) with <-cmp key key₁
|
|
|
282 ... | tri< a ¬b ¬c = left
|
|
|
283 ... | tri≈ ¬a b ¬c = node key₁ value left right
|
|
|
284 ... | tri> ¬a ¬b c = right
|
|
|
285
|
|
|
286
|
|
|
287 data replacedRBTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt (Color ∧ A) ) → Set n where
|
|
|
288 rbr-leaf : {ca cb : Color} → replacedRBTree key value leaf (node key ⟪ cb , value ⟫ leaf leaf)
|
|
|
289 rbr-node : {value₁ : A} → {ca cb : Color } → {t t₁ : bt (Color ∧ A)}
|
|
|
290 → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ cb , value ⟫ t t₁)
|
|
|
291 rbr-right : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
|
|
|
292 → k < key → replacedRBTree key value t2 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t1 t)
|
|
|
293 rbr-left : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
|
|
|
294 → k < key → replacedRBTree key value t1 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t t2)
|
|
|
295
|
|
|
296 data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent uncle grand : bt A) → Set n where
|
|
|
297 s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
298 → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand
|
|
|
299 s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
300 → parent ≡ node kp vp n1 self → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand
|
|
|
301 s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
302 → parent ≡ node kp vp self n1 → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand
|
|
|
303 s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
304 → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand
|
|
|
305
|
|
|
306 record PG {n : Level } (A : Set n) (self : bt A) (stack : List (bt A)) : Set n where
|
|
|
307 field
|
|
|
308 parent grand uncle : bt A
|
|
|
309 pg : ParentGrand self parent uncle grand
|
|
|
310 rest : List (bt A)
|
|
|
311 stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest )
|
|
|
312
|
|
|
313 record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) : Set n where
|
|
|
314 field
|
|
|
315 od d rd : ℕ
|
|
|
316 tree rot : bt (Color ∧ A)
|
|
|
317 origti : treeInvariant orig
|
|
|
318 origrb : RBtreeInvariant orig
|
|
|
319 treerb : RBtreeInvariant tree
|
|
|
320 replrb : RBtreeInvariant repl
|
|
|
321 d=rd : ( d ≡ rd ) ∨ ((suc d ≡ rd ) ∧ (color tree ≡ Red))
|
|
|
322 si : stackInvariant key tree orig stack
|
|
|
323 rotated : rotatedTree tree rot
|
|
|
324 ri : replacedRBTree key value (child-replaced key rot ) repl
|
|
|
325
|
|
|
326
|
|
|
327 rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) )
|
|
|
328 → RBtreeInvariant parent
|
|
|
329 → RBtreeInvariant repl
|
|
|
330 → {left right : bt (Color ∧ A)} → parent ≡ node key ⟪ Black , value ⟫ left right
|
|
|
331 → (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl ) )
|
|
|
332 ∧ (color left ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) )
|
|
783
|
333 rbi-case1 {n} {A} {key} parent repl rbtip rbtir x = ⟪ {!!} , {!!} ⟫
|
|
781
|
334
|
|
|
335 blackdepth≡ : {n : Level } {A : Set n} → {C : Color} {key : ℕ} {value : A} → (tree1 tree2 : bt (Color ∧ A))
|
|
|
336 → RBtreeInvariant tree1
|
|
|
337 → RBtreeInvariant tree2
|
|
|
338 → RBtreeInvariant (node key ⟪ C , value ⟫ tree1 tree2)
|
|
|
339 → black-depth tree1 ≡ black-depth tree2
|
|
|
340
|
|
|
341 blackdepth≡ leaf leaf ri1 ri2 rip = refl
|
|
|
342 blackdepth≡ leaf (node key value t2 t3) ri1 ri2 rip = {!!} --rip kara mitibiki daseru RBinvariant kara toreruka
|
|
|
343 blackdepth≡ (node key value t1 t3) leaf ri1 ri2 rip = {!!}
|
|
|
344 blackdepth≡ (node key value t1 t3) (node key₁ value₁ t2 t4) ri1 ri2 rip = {!!}
|
|
|
345
|
|
783
|
346
|
|
|
347 {-
|
|
|
348 rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) )
|
|
|
349 → RBtreeInvariant parent
|
|
|
350 → RBtreeInvariant repl → (left right : bt (Color ∧ A)) → parent ≡ node key ⟪ Black , value ⟫ left right
|
|
781
|
351 → RBtreeInvariant left
|
|
|
352 → RBtreeInvariant right
|
|
783
|
353 → (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl ) ) ∧ (color left ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) )
|
|
|
354
|
|
|
355 rbi-case1 {n} {A} {key} (node key1 ⟪ Black , value1 ⟫ l r) leaf rbip rbir (node key3 ⟪ Red , val3 ⟫ la ra) (node key4-- ⟪ Red , val4 ⟫ lb rb) pa li ri = {!!}
|
|
|
356 -}
|
