
   0 | ||| Map Internals
   1 | module Data.Map.Internal
   2 | 
   3 | import Data.List
   4 | import Data.String
   5 | import Derive.Prelude
   6 | 
   7 | %default total
   8 | %language ElabReflection
   9 | 
  10 | --------------------------------------------------------------------------------
  11 | --          Maps
  12 | --------------------------------------------------------------------------------
  13 | 
  14 | public export
  15 | Size : Type
  16 | Size = Nat
  17 | 
  18 | ||| A finite map from keys k to values v.
  19 | public export
  20 | data Map : (k : Type) -> (v : Type) -> Type where
  21 |   Bin :  Size
  22 |       -> k
  23 |       -> v
  24 |       -> Map k v
  25 |       -> Map k v
  26 |       -> Map k v
  27 |   Tip : Map k v
  28 | 
  29 | %runElab derive "Map" [Eq,Ord,Show]
  30 | 
  31 | public export
  32 | data MinView k a = MinView' k a (Map k a)
  33 | 
  34 | %runElab derive "MinView" [Eq,Ord,Show]
  35 | 
  36 | public export
  37 | data MaxView k a = MaxView' k a (Map k a)
  38 | 
  39 | %runElab derive "MaxView" [Eq,Ord,Show]
  40 | 
  41 | --------------------------------------------------------------------------------
  42 | --          Creating Maps
  43 | --------------------------------------------------------------------------------
  44 | 
  45 | ||| Wrap a single value in a map.
  46 | export
  47 | singleton :  k
  48 |           -> a
  49 |           -> Map k a
  50 | singleton k x =
  51 |   Bin 1 k x Tip Tip
  52 | 
  53 | --------------------------------------------------------------------------------
  54 | --          Query
  55 | --------------------------------------------------------------------------------
  56 | 
  57 | ||| The number of elements in the map. O(1)
  58 | export
  59 | size :  Map k v
  60 |      -> Nat
  61 | size Tip             =
  62 |   0
  63 | size (Bin _ _ _ l r) =
  64 |   1 + size l + size r
  65 | 
  66 | --------------------------------------------------------------------------------
  67 | --          Map Internals
  68 | --------------------------------------------------------------------------------
  69 | 
  70 | {-
  71 |   [balance l x r] balances two trees with value x.
  72 |   The sizes of the trees should balance after decreasing the
  73 |   size of one of them. (a rotation).
  74 | 
  75 |   [delta] is the maximal relative difference between the sizes of
  76 |           two trees, it corresponds with the [w] in Adams' paper.
  77 |   [ratio] is the ratio between an outer and inner sibling of the
  78 |           heavier subtree in an unbalanced setting. It determines
  79 |           whether a double or single rotation should be performed
  80 |           to restore balance. It is corresponds with the inverse
  81 |           of $\alpha$ in Adam's article.
  82 | 
  83 |   Note that according to the Adam's paper:
  84 |   - [delta] should be larger than 4.646 with a [ratio] of 2.
  85 |   - [delta] should be larger than 3.745 with a [ratio] of 1.534.
  86 | 
  87 |   But the Adam's paper is erroneous:
  88 |   - It can be proved that for delta=2 and delta>=5 there does
  89 |     not exist any ratio that would work.
  90 |   - Delta=4.5 and ratio=2 does not work.
  91 | 
  92 |   That leaves two reasonable variants, delta=3 and delta=4,
  93 |   both with ratio=2.
  94 | 
  95 |   - A lower [delta] leads to a more 'perfectly' balanced tree.
  96 |   - A higher [delta] performs less rebalancing.
  97 | 
  98 |   In the benchmarks, delta=3 is faster on insert operations,
  99 |   and delta=4 has slightly better deletes. As the insert speedup
 100 |   is larger, we currently use delta=3.
 101 | -}
 102 | 
 103 | delta : Nat
 104 | delta = 3
 105 | 
 106 | ratio : Nat
 107 | ratio = 2
 108 | 
 109 | ||| The bin constructor maintains the size of the tree.
 110 | bin :  k
 111 |     -> v
 112 |     -> Map k v
 113 |     -> Map k v
 114 |     -> Map k v
 115 | bin k x l r =
 116 |   Bin (size l + size r + 1) k x l r
 117 | 
 118 | ||| Balances a map after the addition, deletion, or updating of a map via a new key and value.
 119 | export
 120 | balance :  k
 121 |         -> v
 122 |         -> Map k v
 123 |         -> Map k v
 124 |         -> Map k v
 125 | balance k x l r =
 126 |   case l of
 127 |     Tip                  =>
 128 |       case r of
 129 |         Tip                                                              =>
 130 |           Bin 1 k x Tip Tip
 131 |         (Bin _  _  _  Tip                          Tip)                  =>
 132 |           Bin 2 k x Tip r
 133 |         (Bin _  rk rx Tip                          rr@(Bin _ _ _ _ _))   =>
 134 |           Bin 3 rk rx (Bin 1 k x Tip Tip) rr
 135 |         (Bin _  rk rx (Bin _ rlk rlx _ _)          Tip)                  =>
 136 |           Bin 3 rlk rlx (Bin 1 k x Tip Tip) (Bin 1 rk rx Tip Tip)
 137 |         (Bin rs rk rx rl@(Bin rls rlk rlx rll rlr) rr@(Bin rrs _ _ _ _)) =>
 138 |           case rls < ratio * rrs of
 139 |             True  =>
 140 |               Bin (1+rs) rk rx (Bin (1+rls) k x Tip rl) rr
 141 |             False =>
 142 |               Bin (1+rs) rlk rlx (Bin (1+size rll) k x Tip rll) (Bin (1+rrs+size rlr) rk rx rlr rr)
 143 |     (Bin ls lk lx ll lr) =>
 144 |       case r of
 145 |         Tip                  =>
 146 |           case (ll,lr) of
 147 |             (Tip,               Tip)                       =>
 148 |               Bin 2 k x l Tip
 149 |             (Tip,               (Bin _ lrk lrx _ _))       =>
 150 |               Bin 3 lrk lrx (Bin 1 lk lx Tip Tip) (Bin 1 k x Tip Tip)
 151 |             ((Bin _ _ _ _ _),   Tip)                       =>
 152 |               Bin 3 lk lx ll (Bin 1 k x Tip Tip)
 153 |             ((Bin lls _ _ _ _), (Bin lrs lrk lrx lrl lrr)) =>
 154 |               case lrs < ratio * lls of
 155 |                 True  =>
 156 |                   Bin (1+ls) lk lx ll (Bin (1+lrs) k x lr Tip)
 157 |                 False =>
 158 |                   Bin (1+ls) lrk lrx (Bin (1+lls+size lrl) lk lx ll lrl) (Bin (1+size lrr) k x lrr Tip)
 159 |         (Bin rs rk rx rl rr) =>
 160 |           case rs > delta * ls of
 161 |             True  =>
 162 |               case (rl,rr) of
 163 |                 (Bin rls rlk rlx rll rlr, Bin rrs _ _ _ _) =>
 164 |                   case rls < ratio * rrs of
 165 |                     True  =>
 166 |                       Bin (1+ls+rs) rk rx (Bin (1+ls+rls) k x l rl) rr
 167 |                     False =>
 168 |                       Bin (1+ls+rs) rlk rlx (Bin (1+ls+size rll) k x l rll) (Bin (1+rrs+size rlr) rk rx rlr rr)
 169 |                 (_,_)                                      =>
 170 |                   assert_total $ idris_crash "Failure in Data.Map.Internal.balance"
 171 |             False =>
 172 |               case ls > delta * rs of
 173 |                 True  =>
 174 |                   case (ll,lr) of
 175 |                     (Bin lls _ _ _ _, Bin lrs lrk lrx lrl lrr) =>
 176 |                       case lrs < ratio * lls of
 177 |                         True  =>
 178 |                           Bin (1+ls+rs) lk lx ll (Bin (1+rs+lrs) k x lr r)
 179 |                         False =>
 180 |                           Bin (1+ls+rs) lrk lrx (Bin (1+lls+size lrl) lk lx ll lrl) (Bin (1+rs+size lrr) k x lrr r)
 181 |                     (_,_)                                      =>
 182 |                       assert_total $ idris_crash "Failure in Data.Map.Internal.balance"
 183 |                 False =>
 184 |                   Bin (1+ls+rs) k x l r
 185 | 
 186 | ||| A specialized version of balance.
 187 | ||| balanceL is called when left subtree might have been inserted to or when
 188 | ||| right subtree might have been deleted from.
 189 | export
 190 | balanceL :  k
 191 |          -> v
 192 |          -> Map k v
 193 |          -> Map k v
 194 |          -> Map k v
 195 | balanceL k x l r =
 196 |   case r of
 197 |     Tip              =>
 198 |       case l of
 199 |         Tip                                                              =>
 200 |           Bin 1 k x Tip Tip
 201 |         (Bin _  _  _  Tip                  Tip)                          =>
 202 |           Bin 2 k x l Tip
 203 |         (Bin _  lk lx Tip                  (Bin _ lrk lrx _ _))          =>
 204 |           Bin 3 lrk lrx (Bin 1 lk lx Tip Tip) (Bin 1 k x Tip Tip)
 205 |         (Bin _  lk lx ll@(Bin _ _ _ _ _)   Tip)                          =>
 206 |           Bin 3 lk lx ll (Bin 1 k x Tip Tip)
 207 |         (Bin ls lk lx ll@(Bin lls _ _ _ _) lr@(Bin lrs lrk lrx lrl lrr)) =>
 208 |           case lrs < ratio * lls of
 209 |             True  =>
 210 |               Bin (1+ls) lk lx ll (Bin (1+lrs) k x lr Tip)
 211 |             False =>
 212 |               Bin (1+ls) lrk lrx (Bin (1+lls+size lrl) lk lx ll lrl) (Bin (1+size lrr) k x lrr Tip)
 213 |     (Bin rs _ _ _ _) =>
 214 |       case l of
 215 |         Tip                  =>
 216 |           Bin (1+rs) k x Tip r
 217 |         (Bin ls lk lx ll lr) =>
 218 |           case ls > delta * rs of
 219 |             True  =>
 220 |               case (ll,lr) of
 221 |                 (Bin lls _ _ _ _, Bin lrs lrk lrx lrl lrr) =>
 222 |                   case lrs < ratio * lls of
 223 |                     True  =>
 224 |                       Bin (1+ls+rs) lk lx ll (Bin (1+rs+lrs) k x lr r)
 225 |                     False =>
 226 |                       Bin (1+ls+rs) lrk lrx (Bin (1+lls+size lrl) lk lx ll lrl) (Bin (1+rs+size lrr) k x lrr r)
 227 |                 (_,_)                                      =>
 228 |                   assert_total $ idris_crash "Failure in Data.Map.Internal.balanceL"
 229 |             False =>
 230 |               Bin (1+ls+rs) k x l r
 231 | 
 232 | ||| A specialized version of balance.
 233 | ||| balanceR is called when right subtree might have been inserted to or when
 234 | ||| left subtree might have been deleted from.
 235 | export
 236 | balanceR :  k
 237 |          -> v
 238 |          -> Map k v
 239 |          -> Map k v
 240 |          -> Map k v
 241 | balanceR k x l r =
 242 |   case l of
 243 |     Tip              =>
 244 |       case r of
 245 |         Tip                                                              =>
 246 |           Bin 1 k x Tip Tip
 247 |         (Bin _  _  _  Tip                          Tip               )   =>
 248 |           Bin 2 k x Tip r
 249 |         (Bin _  rk rx Tip                          rr@(Bin _ _ _ _ _))   =>
 250 |           Bin 3 rk rx (Bin 1 k x Tip Tip) rr
 251 |         (Bin _  rk rx (Bin _ rlk rlx _ _)          Tip)                  =>
 252 |           Bin 3 rlk rlx (Bin 1 k x Tip Tip) (Bin 1 rk rx Tip Tip)
 253 |         (Bin rs rk rx rl@(Bin rls rlk rlx rll rlr) rr@(Bin rrs _ _ _ _)) =>
 254 |           case rls < ratio * rrs of
 255 |             True  =>
 256 |               Bin (1+rs) rk rx (Bin (1+rls) k x Tip rl) rr
 257 |             False =>
 258 |               Bin (1+rs) rlk rlx (Bin (1+size rll) k x Tip rll) (Bin (1+rrs+size rlr) rk rx rlr rr)
 259 |     (Bin ls _ _ _ _) =>
 260 |       case r of
 261 |         Tip                  =>
 262 |           Bin (1+ls) k x l Tip
 263 |         (Bin rs rk rx rl rr) =>
 264 |           case rs > delta * ls of
 265 |             True  =>
 266 |               case (rl,rr) of
 267 |                 (Bin rls rlk rlx rll rlr, Bin rrs _ _ _ _) =>
 268 |                   case rls < ratio * rrs of
 269 |                     True  =>
 270 |                       Bin (1+ls+rs) rk rx (Bin (1+ls+rls) k x l rl) rr
 271 |                     False =>
 272 |                       Bin (1+ls+rs) rlk rlx (Bin (1+ls+size rll) k x l rll) (Bin (1+rrs+size rlr) rk rx rlr rr)
 273 |                 (_,_)                                      =>
 274 |                   assert_total $ idris_crash "Failure in Data.Map.Internal.balanceR"
 275 |             False =>
 276 |               Bin (1+ls+rs) k x l r
 277 | 
 278 | export
 279 | insertMax :  k
 280 |           -> v
 281 |           -> Map k v
 282 |           -> Map k v
 283 | insertMax kx x t =
 284 |   case t of
 285 |     Tip            =>
 286 |       singleton kx x
 287 |     Bin _ ky y l r =>
 288 |       balanceR ky y l (insertMax kx x r)
 289 | 
 290 | export
 291 | insertMin :  k
 292 |           -> v
 293 |           -> Map k v
 294 |           -> Map k v
 295 | insertMin kx x t =
 296 |   case t of
 297 |     Tip            =>
 298 |       singleton kx x
 299 |     Bin _ ky y l r =>
 300 |       balanceL ky y (insertMin kx x l) r
 301 | 
 302 | export
 303 | minViewSure :  k
 304 |             -> v
 305 |             -> Map k v
 306 |             -> Map k v
 307 |             -> MinView k v
 308 | minViewSure k x Tip                 r =
 309 |   MinView' k x r
 310 | minViewSure k x (Bin _ kl xl ll lr) r =
 311 |   case minViewSure kl xl ll lr of
 312 |     MinView' km xm l' => MinView' km xm (balanceR k x l' r)
 313 | 
 314 | export
 315 | maxViewSure :  k
 316 |             -> v
 317 |             -> Map k v
 318 |             -> Map k v
 319 |             -> MaxView k v
 320 | maxViewSure k x l Tip                 =
 321 |   MaxView' k x l
 322 | maxViewSure k x l (Bin _ kr xr rl rr) =
 323 |   case maxViewSure kr xr rl rr of
 324 |     MaxView' km xm r' => MaxView' km xm (balanceL k x l r')
 325 | 
 326 | ||| Glues two maps together (assumes that both maps are already balanced with respect to each other).
 327 | export
 328 | glue :  Map k v
 329 |      -> Map k v
 330 |      -> Map k v
 331 | glue Tip                    r                      =
 332 |   r
 333 | glue l                      Tip                    =
 334 |   l
 335 | glue l@(Bin sl kl xl ll lr) r@(Bin sr kr xr rl rr) =
 336 |   case sl > sr of
 337 |     True  =>
 338 |       let (MaxView' km m l') = maxViewSure kl xl ll lr
 339 |         in balanceR km m l' r
 340 |     False =>
 341 |       let (MinView' km m r') = minViewSure kr xr rl rr
 342 |         in balanceL km m l r'
 343 | 
 344 | ||| Utility function that maintains the balance properties of the tree.
 345 | export
 346 | link2 :  Map k v
 347 |       -> Map k v
 348 |       -> Map k v
 349 | link2 Tip                      r                        =
 350 |   r
 351 | link2 l                        Tip                      =
 352 |   l
 353 | link2 l@(Bin sizeL kx x lx rx) r@(Bin sizeR ky y ly ry) =
 354 |   case delta * sizeL < sizeR of
 355 |     True  =>
 356 |       balanceL ky y (link2 l ly) ry
 357 |     False =>
 358 |       case delta * sizeR < sizeL of
 359 |         True  =>
 360 |           balanceR kx x lx (link2 rx r)
 361 |         False =>
 362 |           glue l r
 363 | 
 364 | ||| Utility function that maintains the balance properties of the tree.
 365 | export
 366 | link :  k
 367 |      -> v
 368 |      -> Map k v
 369 |      -> Map k v
 370 |      -> Map k v
 371 | link kx x Tip                      r                        =
 372 |   insertMin kx x r
 373 | link kx x l                        Tip                      =
 374 |   insertMax kx x l
 375 | link kx x l@(Bin sizeL ky y ly ry) r@(Bin sizeR kz z lz rz) =
 376 |   case delta * sizeL < sizeR of
 377 |     True  =>
 378 |       balanceL kz z (link kx x l lz) rz
 379 |     False =>
 380 |       case delta * sizeR < sizeL of
 381 |         True  =>
 382 |           balanceR ky y ly (link kx x ry r)
 383 |         False =>
 384 |           bin kx x l r
 385 |