|
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
|
|
|
91 r-node : {value1 : A} → {left right : bt A} → replacedTree key value (node key value left right) (node key value1 left right)
|
|
|
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
|
|
|
100 {-
|
|
|
101 RTtoTI0 : {n : Level} {A : Set n } → (key : ℕ ) → (value : A) → (tree repl : bt A)
|
|
|
102 → treeInvariant tree → replacedTree key value tree repl → treeInvariant repl
|
|
|
103 RTtoTI0 key value leaf (node key value leaf leaf) tr r-leaf = t-single key value
|
|
|
104 RTtoTI0 key value (node key₁ value₁ tree tree₁) (node key₂ value₂ repl repl₁) (t-node x x₁ s s₁) r-node = t-node x x₁ s s₁
|
|
|
105 -}
|
|
|
106 depth-1< : {i j : ℕ} → suc i ≤ suc (i Data.Nat.⊔ j )
|
|
|
107 depth-1< {i} {j} = s≤s (m≤m⊔n _ j)
|
|
|
108 depth-2< : {i j : ℕ} → suc i ≤ suc (j Data.Nat.⊔ i )
|
|
|
109 depth-2< {i} {j} = s≤s (m≤n⊔m j i)
|
|
|
110 depth-3< : {i : ℕ } → suc i ≤ suc (suc i)
|
|
|
111 depth-3< {zero} = s≤s ( z≤n )
|
|
|
112 depth-3< {suc i} = s≤s (depth-3< {i} )
|
|
|
113
|
|
|
114 treeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} → (tleft tright : bt A)
|
|
|
115 → treeInvariant (node key value tleft tright)
|
|
|
116 → treeInvariant tleft
|
|
|
117 treeLeftDown leaf leaf (t-single key value) = t-leaf
|
|
|
118 treeLeftDown leaf (node key value t1 t2) (t-right x ti) = t-leaf
|
|
|
119 treeLeftDown (node key value t t₁) leaf (t-left x ti) = ti
|
|
|
120 treeLeftDown (node key value t t₁) (node key₁ value₁ t1 t2) (t-node x x1 ti ti2 ) = ti
|
|
|
121
|
|
|
122 treeRightDown : {n : Level} {A : Set n} {key : ℕ} {value : A} → (tleft tright : bt A)
|
|
|
123 → treeInvariant (node key value tleft tright)
|
|
|
124 → treeInvariant tright
|
|
|
125 treeRightDown leaf leaf (t-single key value) = t-leaf
|
|
|
126 treeRightDown leaf (node key value t1 t2) (t-right x ti) = ti
|
|
|
127
|
|
|
128 treeRightDown (node key value t t₁) leaf (t-left x ti) = t-leaf
|
|
|
129 treeRightDown (node key value t t₁) (node key₁ value₁ t1 t2) (t-node x x1 ti ti2 ) = ti2
|
|
|
130
|
|
|
131
|
|
|
132 findP : {n m : Level} {A : Set n} {t : Set n} → (tkey : ℕ) → (top orig : bt A) → (st : List (bt A))
|
|
|
133 → (treeInvariant top)
|
|
|
134 → stackInvariant tkey top orig st
|
|
|
135 → (next : (newtop : bt A) → (stack : List (bt A))
|
|
|
136 → (treeInvariant newtop)
|
|
|
137 → (stackInvariant tkey newtop orig stack)
|
|
|
138 → bt-depth newtop < bt-depth top → t)
|
|
|
139 → (exit : (newtop : bt A) → (stack : List (bt A))
|
|
|
140 → (treeInvariant newtop)
|
|
|
141 → (stackInvariant tkey newtop orig stack) --need new stack ?
|
|
|
142 → (newtop ≡ leaf) ∨ (node-key newtop ≡ just tkey) → t)
|
|
|
143 → t
|
|
|
144 findP tkey leaf orig st ti si next exit = exit leaf st ti si (case1 refl)
|
|
|
145 findP tkey (node key value tl tr) orig st ti si next exit with <-cmp tkey key
|
|
|
146 findP tkey top orig st ti si next exit | tri≈ ¬a refl ¬c = exit top st ti si (case2 refl)
|
|
|
147 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)))
|
|
|
148
|
|
|
149 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)))
|
|
|
150
|
|
|
151
|
|
|
152 --RBT
|
|
|
153 data Color : Set where
|
|
|
154 Red : Color
|
|
|
155 Black : Color
|
|
|
156
|
|
|
157 RB→bt : {n : Level} (A : Set n) → (bt (Color ∧ A)) → bt A
|
|
|
158 RB→bt {n} A leaf = leaf
|
|
|
159 RB→bt {n} A (node key ⟪ C , value ⟫ tr t1) = (node key value (RB→bt A tr) (RB→bt A t1))
|
|
|
160
|
|
|
161 color : {n : Level} {A : Set n} → (bt (Color ∧ A)) → Color
|
|
|
162 color leaf = Black
|
|
|
163 color (node key ⟪ C , value ⟫ rb rb₁) = C
|
|
|
164
|
|
|
165 black-depth : {n : Level} {A : Set n} → (tree : bt (Color ∧ A) ) → ℕ
|
|
|
166 black-depth leaf = 0
|
|
|
167 black-depth (node key ⟪ Red , value ⟫ t t₁) = black-depth t ⊔ black-depth t₁
|
|
|
168 black-depth (node key ⟪ Black , value ⟫ t t₁) = suc (black-depth t ⊔ black-depth t₁ )
|
|
|
169
|
|
|
170 data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where
|
|
|
171 rb-leaf : RBtreeInvariant leaf
|
|
|
172 rb-single : (key : ℕ) → (value : A) → RBtreeInvariant (node key ⟪ Black , value ⟫ leaf leaf)
|
|
|
173 rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁
|
|
|
174 → black-depth t ≡ black-depth t₁
|
|
|
175 → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁)
|
|
|
176 → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key₁ ⟪ Black , value₁ ⟫ t t₁))
|
|
|
177 rb-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {c : Color}
|
|
|
178 → black-depth t ≡ black-depth t₁
|
|
|
179 → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁)
|
|
|
180 → RBtreeInvariant (node key ⟪ Black , value ⟫ leaf (node key₁ ⟪ c , value₁ ⟫ t t₁))
|
|
|
181 rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁
|
|
|
182 → black-depth t ≡ black-depth t₁
|
|
|
183 → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁)
|
|
|
184 → RBtreeInvariant (node key ⟪ Red , value ⟫ (node key₁ ⟪ Black , value₁ ⟫ t t₁) leaf )
|
|
|
185 rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {c : Color}
|
|
|
186 → black-depth t ≡ black-depth t₁
|
|
|
187 → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁)
|
|
|
188 → RBtreeInvariant (node key ⟪ Black , value ⟫ (node key₁ ⟪ c , value₁ ⟫ t t₁) leaf)
|
|
|
189 rb-node-red : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂
|
|
|
190 → black-depth t₁ ≡ black-depth t₂
|
|
|
191 → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ t₂)
|
|
|
192 → black-depth t₃ ≡ black-depth t₄
|
|
|
193 → RBtreeInvariant (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)
|
|
|
194 → RBtreeInvariant (node key₁ ⟪ Red , value₁ ⟫ (node key ⟪ Black , value ⟫ t₁ t₂) (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄))
|
|
|
195 rb-node-black : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂
|
|
|
196 → {c c₁ : Color}
|
|
|
197 → black-depth t₁ ≡ black-depth t₂
|
|
|
198 → RBtreeInvariant (node key ⟪ c , value ⟫ t₁ t₂)
|
|
|
199 → black-depth t₃ ≡ black-depth t₄
|
|
|
200 → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)
|
|
|
201 → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄))
|
|
|
202
|
|
|
203
|
|
|
204 data rotatedTree {n : Level} {A : Set n} : (before after : bt A) → Set n where
|
|
|
205 rtt-node : {t : bt A } → rotatedTree t t
|
|
|
206 -- a b
|
|
|
207 -- b c d a
|
|
|
208 -- d e e c
|
|
|
209 --
|
|
|
210 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}
|
|
|
211 --kd < kb < ke < ka< kc
|
|
|
212 → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A}
|
|
|
213 → kd < kb → kb < ke → ke < ka → ka < kc
|
|
|
214 → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1)
|
|
|
215 → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1)
|
|
|
216 → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1)
|
|
|
217 → rotatedTree (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr))
|
|
|
218 (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1)))
|
|
|
219
|
|
|
220 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}
|
|
|
221 --kd < kb < ke < ka< kc
|
|
|
222 → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A} -- after child
|
|
|
223 → kd < kb → kb < ke → ke < ka → ka < kc
|
|
|
224 → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1)
|
|
|
225 → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1)
|
|
|
226 → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1)
|
|
|
227 → rotatedTree (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1)))
|
|
|
228 (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr))
|
|
|
229
|
|
|
230 RBtreeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color}
|
|
|
231 → (tleft tright : bt (Color ∧ A))
|
|
|
232 → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright)
|
|
|
233 → RBtreeInvariant tleft
|
|
|
234 RBtreeLeftDown leaf leaf (rb-single k1 v) = rb-leaf
|
|
|
235 RBtreeLeftDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-red x bde rbti) = rb-leaf
|
|
|
236 RBtreeLeftDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-black x bde rbti) = rb-leaf
|
|
|
237 RBtreeLeftDown leaf (node key ⟪ Red , value ⟫ t1 t2 ) (rb-right-black x bde rbti)= rb-leaf
|
|
|
238 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti
|
|
|
239 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti)= ti
|
|
|
240 RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti
|
|
|
241 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til
|
|
|
242 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til bde2 tir) = til
|
|
|
243 RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til
|
|
|
244 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til
|
|
|
245 RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til
|
|
|
246
|
|
|
247 RBtreeRightDown : {n : Level} {A : Set n} { key : ℕ} {value : A} {c : Color}
|
|
|
248 → (tleft tright : bt (Color ∧ A))
|
|
|
249 → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright)
|
|
|
250 → RBtreeInvariant tright
|
|
|
251 RBtreeRightDown leaf leaf (rb-single k1 v1 ) = rb-leaf
|
|
|
252 RBtreeRightDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-red x bde rbti) = rbti
|
|
|
253 RBtreeRightDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-black x bde rbti) = rbti
|
|
|
254 RBtreeRightDown leaf (node key ⟪ Red , value ⟫ t1 t2 ) (rb-right-black x bde rbti)= rbti
|
|
|
255 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf
|
|
|
256 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti) = rb-leaf
|
|
|
257 RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf
|
|
|
258 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir
|
|
|
259 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til bde2 tir) = tir
|
|
|
260 RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir
|
|
|
261 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir
|
|
|
262 RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir
|
|
|
263
|
|
|
264 findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) )
|
|
|
265 → (stack : List (bt (Color ∧ A)))
|
|
|
266 → treeInvariant tree ∧ stackInvariant key tree tree0 stack
|
|
|
267 → RBtreeInvariant tree
|
|
|
268 → (next : (tree1 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A)))
|
|
|
269 → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
|
|
|
270 → RBtreeInvariant tree1
|
|
|
271 → bt-depth tree1 < bt-depth tree → t )
|
|
|
272 → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A)))
|
|
|
273 → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
|
|
|
274 → RBtreeInvariant tree1
|
|
|
275 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t
|
|
|
276 findRBT key leaf tree0 stack ti rb0 next exit = exit leaf stack ti rb0 (case1 refl)
|
|
|
277 findRBT key n@(node key₁ value left right) tree0 stack ti rb0 next exit with <-cmp key key₁
|
|
|
278 findRBT key (node key₁ value left right) tree0 stack ti rb0 next exit | tri< a ¬b ¬c
|
|
|
279 = next left (left ∷ stack) ⟪ treeLeftDown left right (_∧_.proj1 ti) , s-left a (_∧_.proj2 ti) ⟫ (RBtreeLeftDown left right rb0) depth-1<
|
|
|
280 findRBT key n tree0 stack ti rb0 _ exit | tri≈ ¬a refl ¬c = exit n stack ti rb0 (case2 refl)
|
|
|
281 findRBT key (node key₁ value left right) tree0 stack ti rb0 next exit | tri> ¬a ¬b c
|
|
|
282 = next right (right ∷ stack) ⟪ treeRightDown left right (_∧_.proj1 ti), s-right c (_∧_.proj2 ti) ⟫ (RBtreeRightDown left right rb0) depth-2<
|
|
|
283
|
|
|
284 child-replaced : {n : Level} {A : Set n} (key : ℕ) (tree : bt A) → bt A
|
|
|
285 child-replaced key leaf = leaf
|
|
|
286 child-replaced key (node key₁ value left right) with <-cmp key key₁
|
|
|
287 ... | tri< a ¬b ¬c = left
|
|
|
288 ... | tri≈ ¬a b ¬c = node key₁ value left right
|
|
|
289 ... | tri> ¬a ¬b c = right
|
|
|
290
|
|
|
291
|
|
|
292 data replacedRBTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt (Color ∧ A) ) → Set n where
|
|
|
293 rbr-leaf : {ca cb : Color} → replacedRBTree key value leaf (node key ⟪ cb , value ⟫ leaf leaf)
|
|
|
294 rbr-node : {value₁ : A} → {ca cb : Color } → {t t₁ : bt (Color ∧ A)}
|
|
|
295 → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ cb , value ⟫ t t₁)
|
|
|
296 rbr-right : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
|
|
|
297 → k < key → replacedRBTree key value t2 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t1 t)
|
|
|
298 rbr-left : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
|
|
|
299 → k < key → replacedRBTree key value t1 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t t2)
|
|
|
300
|
|
|
301 data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent uncle grand : bt A) → Set n where
|
|
|
302 s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
303 → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand
|
|
|
304 s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
305 → parent ≡ node kp vp n1 self → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand
|
|
|
306 s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
307 → parent ≡ node kp vp self n1 → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand
|
|
|
308 s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
309 → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand
|
|
|
310
|
|
|
311 record PG {n : Level } (A : Set n) (self : bt A) (stack : List (bt A)) : Set n where
|
|
|
312 field
|
|
|
313 parent grand uncle : bt A
|
|
|
314 pg : ParentGrand self parent uncle grand
|
|
|
315 rest : List (bt A)
|
|
|
316 stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest )
|
|
|
317
|
|
|
318 record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) : Set n where
|
|
|
319 field
|
|
|
320 od d rd : ℕ
|
|
|
321 tree rot : bt (Color ∧ A)
|
|
|
322 origti : treeInvariant orig
|
|
|
323 origrb : RBtreeInvariant orig
|
|
|
324 treerb : RBtreeInvariant tree
|
|
|
325 replrb : RBtreeInvariant repl
|
|
|
326 d=rd : ( d ≡ rd ) ∨ ((suc d ≡ rd ) ∧ (color tree ≡ Red))
|
|
|
327 si : stackInvariant key tree orig stack
|
|
|
328 rotated : rotatedTree tree rot
|
|
|
329 ri : replacedRBTree key value (child-replaced key rot ) repl
|
|
|
330
|
|
|
331
|
|
|
332 {-
|
|
|
333 rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) )
|
|
|
334 → RBtreeInvariant parent
|
|
|
335 → RBtreeInvariant repl
|
|
|
336 → {left right : bt (Color ∧ A)} → parent ≡ node key ⟪ Black , value ⟫ left right
|
|
|
337 → (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl ) )
|
|
|
338 ∧ (color left ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) )
|
|
|
339 rbi-case1 {n} {A} {key} (node key1 ⟪ Black , value1 ⟫ l r) leaf rbip rbir left right x = {!!}
|
|
|
340 rbi-case1 {n} {A} {key} parent (node key₁ value₁ tree1 tree2) rbi rb2 x = {!!}
|
|
|
341
|
|
|
342 -}
|
|
|
343 blackdepth≡ : {n : Level } {A : Set n} → {C : Color} {key : ℕ} {value : A} → (tree1 tree2 : bt (Color ∧ A))
|
|
|
344 → RBtreeInvariant tree1
|
|
|
345 → RBtreeInvariant tree2
|
|
|
346 → RBtreeInvariant (node key ⟪ C , value ⟫ tree1 tree2)
|
|
|
347 → black-depth tree1 ≡ black-depth tree2
|
|
|
348
|
|
|
349 blackdepth≡ leaf leaf ri1 ri2 rip = refl
|
|
|
350 blackdepth≡ leaf (node key value t2 t3) ri1 ri2 rip = {!!} --rip kara mitibiki daseru RBinvariant kara toreruka
|
|
|
351 blackdepth≡ (node key value t1 t3) leaf ri1 ri2 rip = {!!}
|
|
|
352 blackdepth≡ (node key value t1 t3) (node key₁ value₁ t2 t4) ri1 ri2 rip = {!!}
|
|
|
353
|
|
|
354 rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) )
|
|
|
355 → RBtreeInvariant parent
|
|
|
356 → RBtreeInvariant repl
|
|
|
357 → (left right : bt (Color ∧ A)) → parent ≡ node key ⟪ Black , value ⟫ left right
|
|
|
358 → RBtreeInvariant left
|
|
|
359 → RBtreeInvariant right
|
|
|
360 → (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl ) ) ∧ (color left ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) )
|
|
|
361 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
|
|
|
362 = ⟪ {!!} rb-left-black {!!} {!!} li , (λ x → rb-right-black {!!} {!!} ri) ⟫
|
|
|
363
|
|
|
364 --⟪ rb-left-black {!!} {!!} (RBtreeLeftDown left right rbip ) , {!!} ⟫
|
|
|
365 --rbi-case1 {n} {A} {key} parent (node key₁ value₁ tree1 tree2) rbi rb2 x = {!!}
|
