0 | ||| Set Internals
  1 | module Data.Set.Internal
  2 |
  3 | import Data.List
  4 | import Data.String
  5 | import Derive.Prelude
  6 |
  7 | %default total
  8 | %language ElabReflection
  9 |
 10 | --------------------------------------------------------------------------------
 11 | --          Sets
 12 | --------------------------------------------------------------------------------
 13 |
 14 | public export
 15 | Size : Type
 16 | Size = Nat
 17 |
 18 | ||| A finite set of values.
 19 | public export
 20 | data Set : (a : Type) -> Type where
 21 |   Bin :  Size
 22 |       -> a
 23 |       -> Set a
 24 |       -> Set a
 25 |       -> Set a
 26 |   Tip : Set a
 27 |
 28 | %runElab derive "Set" [Eq,Ord,Show]
 29 |
 30 | --------------------------------------------------------------------------------
 31 | --          Creating Sets
 32 | --------------------------------------------------------------------------------
 33 |
 34 | ||| Wrap a single value in a set.
 35 | export
 36 | singleton :  a
 37 |           -> Set a
 38 | singleton x =
 39 |   Bin 1 x Tip Tip
 40 |
 41 | --------------------------------------------------------------------------------
 42 | --          Query
 43 | --------------------------------------------------------------------------------
 44 |
 45 | ||| The number of elements in the set. O(1)
 46 | export
 47 | size :  Set a
 48 |      -> Nat
 49 | size Tip           =
 50 |   0
 51 | size (Bin _ _ l r) =
 52 |   1 + size l + size r
 53 |
 54 | --------------------------------------------------------------------------------
 55 | --          Set Internals
 56 | --------------------------------------------------------------------------------
 57 |
 58 | {-
 59 |   [balance l x r] balances two trees with value x.
 60 |   The sizes of the trees should balance after decreasing the
 61 |   size of one of them. (a rotation).
 62 |
 63 |   [delta] is the maximal relative difference between the sizes of
 64 |           two trees, it corresponds with the [w] in Adams' paper.
 65 |   [ratio] is the ratio between an outer and inner sibling of the
 66 |           heavier subtree in an unbalanced setting. It determines
 67 |           whether a double or single rotation should be performed
 68 |           to restore balance. It is corresponds with the inverse
 69 |           of $\alpha$ in Adam's article.
 70 |
 71 |   Note that according to the Adam's paper:
 72 |   - [delta] should be larger than 4.646 with a [ratio] of 2.
 73 |   - [delta] should be larger than 3.745 with a [ratio] of 1.534.
 74 |
 75 |   But the Adam's paper is erroneous:
 76 |   - It can be proved that for delta=2 and delta>=5 there does
 77 |     not exist any ratio that would work.
 78 |   - Delta=4.5 and ratio=2 does not work.
 79 |
 80 |   That leaves two reasonable variants, delta=3 and delta=4,
 81 |   both with ratio=2.
 82 |
 83 |   - A lower [delta] leads to a more 'perfectly' balanced tree.
 84 |   - A higher [delta] performs less rebalancing.
 85 |
 86 |   In the benchmarks, delta=3 is faster on insert operations,
 87 |   and delta=4 has slightly better deletes. As the insert speedup
 88 |   is larger, we currently use delta=3.
 89 | -}
 90 |
 91 | export
 92 | delta : Nat
 93 | delta = 3
 94 |
 95 | ratio : Nat
 96 | ratio = 2
 97 |
 98 | ||| The bin constructor maintains the size of the tree.
 99 | bin :  a
100 |     -> Set a
101 |     -> Set a
102 |     -> Set a
103 | bin x l r =
104 |   Bin (size l + size r + 1) x l r
105 |
106 | ||| A specialized version of balance.
107 | ||| balanceL is called when left subtree might have been inserted to or when
108 | ||| right subtree might have been deleted from.
109 | export
110 | balanceL :  a
111 |          -> Set a
112 |          -> Set a
113 |          -> Set a
114 | balanceL x l r =
115 |   case r of
116 |     Tip              =>
117 |       case l of
118 |         Tip                                                     =>
119 |           Bin 1 x Tip Tip
120 |         (Bin _  _  Tip                Tip)                      =>
121 |           Bin 2 x l Tip
122 |         (Bin _  lx Tip                (Bin _ lrx _ _))          =>
123 |           Bin 3 lrx (Bin 1 lx Tip Tip) (Bin 1 x Tip Tip)
124 |         (Bin _  lx ll@(Bin _ _ _ _)   Tip)                      =>
125 |           Bin 3 lx ll (Bin 1 x Tip Tip)
126 |         (Bin ls lx ll@(Bin lls _ _ _) lr@(Bin lrs lrx lrl lrr)) =>
127 |           case lrs < ratio * lls of
128 |             True  =>
129 |               Bin (1+ls) lx ll (Bin (1+lrs) x lr Tip)
130 |             False =>
131 |               Bin (1+ls) lrx (Bin (1+lls+size lrl) lx ll lrl) (Bin (1+size lrr) x lrr Tip)
132 |     (Bin rs _ _ _) =>
133 |       case l of
134 |         Tip               =>
135 |           Bin (1+rs) x Tip r
136 |         (Bin ls lx ll lr) =>
137 |           case ls > delta * rs of
138 |             True  =>
139 |               case (ll,lr) of
140 |                 (Bin lls _ _ _, Bin lrs lrx lrl lrr) =>
141 |                   case lrs < ratio * lls of
142 |                     True  =>
143 |                       Bin (1+ls+rs) lx ll (Bin (1+rs+lrs) x lr r)
144 |                     False =>
145 |                       Bin (1+ls+rs) lrx (Bin (1+lls+size lrl) lx ll lrl) (Bin (1+rs+size lrr) x lrr r)
146 |                 (_,_)                                      =>
147 |                   assert_total $ idris_crash "Failure in Data.Set.Internal.balanceL"
148 |             False =>
149 |               Bin (1+ls+rs) x l r
150 |
151 | ||| A specialized version of balance.
152 | ||| balanceR is called when right subtree might have been inserted to or when
153 | ||| left subtree might have been deleted from.
154 | export
155 | balanceR :  a
156 |          -> Set a
157 |          -> Set a
158 |          -> Set a
159 | balanceR x l r =
160 |   case l of
161 |     Tip            =>
162 |       case r of
163 |         Tip                                                     =>
164 |           Bin 1 x Tip Tip
165 |         (Bin _  _  Tip                      Tip)                =>
166 |           Bin 2 x Tip r
167 |         (Bin _  rx Tip                      rr@(Bin _ _ _ _))   =>
168 |           Bin 3 rx (Bin 1 x Tip Tip) rr
169 |         (Bin _  rx (Bin _ rlx _ _)          Tip)                =>
170 |           Bin 3 rlx (Bin 1 x Tip Tip) (Bin 1 rx Tip Tip)
171 |         (Bin rs rx rl@(Bin rls rlx rll rlr) rr@(Bin rrs _ _ _)) =>
172 |           case rls < ratio * rrs of
173 |             True  =>
174 |               Bin (1+rs) rx (Bin (1+rls) x Tip rl) rr
175 |             False =>
176 |               Bin (1+rs) rlx (Bin (1+size rll) x Tip rll) (Bin (1+rrs+size rlr) rx rlr rr)
177 |     (Bin ls _ _ _) =>
178 |       case r of
179 |         Tip                  =>
180 |           Bin (1+ls) x l Tip
181 |         (Bin rs rx rl rr) =>
182 |           case rs > delta * ls of
183 |             True  =>
184 |               case (rl,rr) of
185 |                 (Bin rls rlx rll rlr, Bin rrs _ _ _) =>
186 |                   case rls < ratio * rrs of
187 |                     True  =>
188 |                       Bin (1+ls+rs) rx (Bin (1+ls+rls) x l rl) rr
189 |                     False =>
190 |                       Bin (1+ls+rs) rlx (Bin (1+ls+size rll) x l rll) (Bin (1+rrs+size rlr) rx rlr rr)
191 |                 (_,_)                                      =>
192 |                   assert_total $ idris_crash "Failure in Data.Set.Internal.balanceR"
193 |             False =>
194 |               Bin (1+ls+rs) x l r
195 |
196 | export
197 | insertMax :  a
198 |           -> Set a
199 |           -> Set a
200 | insertMax x t =
201 |   case t of
202 |     Tip            =>
203 |       singleton x
204 |     Bin _ y l r =>
205 |       balanceR y l (insertMax x r)
206 |
207 | export
208 | insertMin :  a
209 |           -> Set a
210 |           -> Set a
211 | insertMin x t =
212 |   case t of
213 |     Tip            =>
214 |       singleton x
215 |     Bin _ y l r =>
216 |       balanceL y (insertMin x l) r
217 |
218 | export
219 | minViewSure :  a
220 |             -> Set a
221 |             -> Set a
222 |             -> (a, Set a)
223 | minViewSure x Tip              r =
224 |   (x, r)
225 | minViewSure x (Bin _ xl ll lr) r =
226 |   case minViewSure xl ll lr of
227 |     (xm, l') =>
228 |       (xm, balanceR x l' r)
229 |
230 | export
231 | maxViewSure :  a
232 |             -> Set a
233 |             -> Set a
234 |             -> (a, Set a)
235 | maxViewSure x l Tip              =
236 |   (x, l)
237 | maxViewSure x l (Bin _ xr rl rr) =
238 |   case maxViewSure xr rl rr of
239 |     (xm, r') =>
240 |       (xm, balanceL x l r')
241 |
242 | ||| Glues two sets together (assumes that both sets are already balanced with respect to each other).
243 | export
244 | glue :  Set a
245 |      -> Set a
246 |      -> Set a
247 | glue Tip                    r                =
248 |   r
249 | glue l                      Tip              =
250 |   l
251 | glue l@(Bin sl xl ll lr) r@(Bin sr xr rl rr) =
252 |   case sl > sr of
253 |     True  =>
254 |       let (m, l') = maxViewSure xl ll lr
255 |         in balanceR m l' r
256 |     False =>
257 |       let (m, r') = minViewSure xr rl rr
258 |         in balanceL m l r'
259 |
260 | ||| Utility function that maintains the balance properties of the tree.
261 | export
262 | link :  a
263 |      -> Set a
264 |      -> Set a
265 |      -> Set a
266 | link x Tip                      r                  =
267 |   insertMin x r
268 | link x l                        Tip                =
269 |   insertMax x l
270 | link x l@(Bin sizeL y ly ry) r@(Bin sizeR z lz rz) =
271 |   case delta * sizeL < sizeR of
272 |     True  =>
273 |       balanceL z (link x l lz) rz
274 |     False =>
275 |       case delta * sizeR < sizeL of
276 |         True  =>
277 |           balanceR y ly (link x ry r)
278 |         False =>
279 |           bin x l r
280 |