
   0 | ||| Ordered Priority Search Queue Internals
   1 | module Data.OrdPSQ.Internal
   2 | 
   3 | import Data.List
   4 | import Data.String
   5 | import Derive.Prelude
   6 | 
   7 | %default total
   8 | %language ElabReflection
   9 | 
  10 | --------------------------------------------------------------------------------
  11 | --          Elem
  12 | --------------------------------------------------------------------------------
  13 | 
  14 | public export
  15 | Size : Type
  16 | Size = Nat
  17 | 
  18 | ||| Elem k p v binds the key k to the value v with priority p.
  19 | public export
  20 | data Elem : (k : Type) -> (p : Type) -> (v : Type) -> Type where
  21 |   MkElem :  k
  22 |          -> p
  23 |          -> v
  24 |          -> Elem k p v
  25 | 
  26 | %runElab derive "Elem" [Eq,Ord,Show]
  27 | 
  28 | namespace Elem
  29 |   export
  30 |   foldr :  (a -> b -> b)
  31 |         -> b
  32 |         -> Elem k p a
  33 |         -> b
  34 |   foldr f z (MkElem _ _ v) =
  35 |     f v z
  36 | 
  37 |   export
  38 |   foldl :  (b -> a -> b)
  39 |         -> b
  40 |         -> Elem k p a
  41 |         -> b
  42 |   foldl f z (MkElem _ _ v) =
  43 |     f z v
  44 | 
  45 |   export
  46 |   map :  (a -> b)
  47 |       -> Elem k p a
  48 |       -> Elem k p b
  49 |   map f (MkElem k p v) =
  50 |     MkElem k p (f v)
  51 | 
  52 | export
  53 | Functor (Elem k p) where
  54 |   map f v = map f v
  55 | 
  56 | export
  57 | Foldable (Elem k p) where
  58 |   foldr f z = Data.OrdPSQ.Internal.Elem.foldr f z
  59 |   foldl f z = Data.OrdPSQ.Internal.Elem.foldl f z
  60 | 
  61 | --------------------------------------------------------------------------------
  62 | --          LTree
  63 | --------------------------------------------------------------------------------
  64 | 
  65 | public export
  66 | data LTree : (k : Type) -> (p : Type) -> (v : Type) -> Type where
  67 |   Start  :  LTree k p v
  68 |   LLoser :  Size
  69 |          -> Elem k p v
  70 |          -> LTree k p v
  71 |          -> k            -- split key
  72 |          -> LTree k p v
  73 |          -> LTree k p v
  74 |   RLoser :  Size
  75 |          -> Elem k p v
  76 |          -> LTree k p v
  77 |          -> k            -- split key
  78 |          -> LTree k p v
  79 |          -> LTree k p v
  80 | 
  81 | %runElab derive "LTree" [Eq,Ord,Show]
  82 | 
  83 | namespace LTree
  84 |   export
  85 |   foldr :  (a -> b -> b)
  86 |         -> b
  87 |         -> LTree k p a
  88 |         -> b
  89 |   foldr f z Start              =
  90 |     z
  91 |   foldr f z (LLoser _ e l _ r) =
  92 |     foldr f (Prelude.foldr f (foldr f z r) e) l
  93 |   foldr f z (RLoser _ e l _ r) =
  94 |     foldr f (Prelude.foldr f (foldr f z r) e) l
  95 | 
  96 |   export
  97 |   foldl :  (b -> a -> b)
  98 |         -> b
  99 |         -> LTree k p a
 100 |         -> b
 101 |   foldl f z Start              =
 102 |     z
 103 |   foldl f z (LLoser _ e l _ r) =
 104 |     foldl f (Prelude.foldl f (foldl f z l) e) r
 105 |   foldl f z (RLoser _ e l _ r) =
 106 |     foldl f (Prelude.foldl f (foldl f z l) e) r
 107 | 
 108 |   export
 109 |   map :  (a -> b)
 110 |       -> LTree k p a
 111 |       -> LTree k p b
 112 |   map _ Start              =
 113 |     Start
 114 |   map f (LLoser s e l k r) =
 115 |     LLoser s (map f e) (map f l) k (map f r)
 116 |   map f (RLoser s e l k r) =
 117 |     RLoser s (map f e) (map f l) k (map f r)
 118 | 
 119 | export
 120 | Functor (LTree k p) where
 121 |   map f v = map f v
 122 | 
 123 | export
 124 | Foldable (LTree k p) where
 125 |   foldr f z = Data.OrdPSQ.Internal.LTree.foldr f z
 126 |   foldl f z = Data.OrdPSQ.Internal.LTree.foldl f z
 127 | 
 128 | --------------------------------------------------------------------------------
 129 | --          OrdPSQ
 130 | --------------------------------------------------------------------------------
 131 | 
 132 | ||| An OrdPSQ uses the Ord instance of the key type to build a priority search queue.
 133 | ||| It is a mapping from keys k to priorities p and values v.
 134 | public export
 135 | data OrdPSQ : (k : Type) -> (p : Type) -> (v : Type) -> Type where
 136 |   Void   :  OrdPSQ k p v
 137 |   Winner :  Elem k p v
 138 |          -> LTree k p v
 139 |          -> k
 140 |          -> OrdPSQ k p v
 141 | 
 142 | %runElab derive "OrdPSQ" [Eq,Ord,Show]
 143 | 
 144 | --------------------------------------------------------------------------------
 145 | --          Balancing Internals
 146 | --------------------------------------------------------------------------------
 147 | 
 148 | ||| Balance factor
 149 | ||| Has to be greater than 3.75 (see Hinze's paper).
 150 | private
 151 | omega : Nat
 152 | omega = 4
 153 | 
 154 | ||| When priorities are equal, the tree with the lowest key wins. This is
 155 | ||| important to have a deterministic `==`, which requires on `minView` pulling
 156 | ||| out the elements in the right order.
 157 | private
 158 | beats :  Ord k
 159 |       => Ord p
 160 |       => (p, k)
 161 |       -> (p, k)
 162 |       -> Bool
 163 | beats (p, k) (p', k') =
 164 |   p < p' || (p == p' && k < k')
 165 | 
 166 | export
 167 | size' :  LTree p k v
 168 |       -> Size
 169 | size' Start              =
 170 |   0
 171 | size' (LLoser s _ _ _ _) =
 172 |   s
 173 | size' (RLoser s _ _ _ _) =
 174 |   s
 175 | 
 176 | private
 177 | left :  LTree k p v
 178 |      -> LTree k p v
 179 | left Start               =
 180 |   assert_total $ idris_crash "Data.OrdPSQ.Internal.left: empty loser tree"
 181 | left (LLoser _ _ tl _ _) =
 182 |   tl
 183 | left (RLoser _ _ tl _ _) =
 184 |   tl
 185 | 
 186 | private
 187 | right :  LTree k p v
 188 |       -> LTree k p v
 189 | right Start               =
 190 |   assert_total $ idris_crash "Data.OrdPSQ.Internal.right: empty loser tree"
 191 | right (LLoser _ _ _ _ tr) =
 192 |   tr
 193 | right (RLoser _ _ _ _ tr) =
 194 |   tr
 195 | 
 196 | export
 197 | maxKey :  OrdPSQ k p v
 198 |        -> k
 199 | maxKey Void           =
 200 |   assert_total $ idris_crash "Data.OrdPSQ.Internal.maxKey: empty queue"
 201 | maxKey (Winner _ _ m) =
 202 |   m
 203 | 
 204 | private
 205 | lLoser :  k
 206 |        -> p
 207 |        -> v
 208 |        -> LTree k p v
 209 |        -> k
 210 |        -> LTree k p v
 211 |        -> LTree k p v
 212 | lLoser k p v tl m tr =
 213 |   LLoser (1 + size' tl + size' tr) (MkElem k p v) tl m tr
 214 | 
 215 | private
 216 | rLoser :  k
 217 |        -> p
 218 |        -> v
 219 |        -> LTree k p v
 220 |        -> k
 221 |        -> LTree k p v
 222 |        -> LTree k p v
 223 | rLoser k p v tl m tr =
 224 |   RLoser (1 + size' tl + size' tr) (MkElem k p v) tl m tr
 225 | 
 226 | private
 227 | lSingleLeft :  Ord k
 228 |             => Ord p
 229 |             => k
 230 |             -> p
 231 |             -> v
 232 |             -> LTree k p v
 233 |             -> k
 234 |             -> LTree k p v
 235 |             -> LTree k p v
 236 | lSingleLeft k1 p1 v1 t1 m1 (LLoser _ (MkElem k2 p2 v2) t2 m2 t3) =
 237 |   case (p1, k1) `beats` (p2, k2) of
 238 |     True  =>
 239 |       lLoser k1 p1 v1 (rLoser k2 p2 v2 t1 m1 t2) m2 t3
 240 |     False =>
 241 |       lLoser k2 p2 v2 (lLoser k1 p1 v1 t1 m1 t2) m2 t3
 242 | lSingleLeft k1 p1 v1 t1 m1 (RLoser _ (MkElem k2 p2 v2) t2 m2 t3) =
 243 |   rLoser k2 p2 v2 (lLoser k1 p1 v1 t1 m1 t2) m2 t3
 244 | lSingleLeft _  _  _  _  _  _                                     =
 245 |   assert_total $ idris_crash "Data.OrdPSQ.Internal.lSingleLeft: malformed tree"
 246 | 
 247 | private
 248 | rSingleLeft :  k
 249 |             -> p
 250 |             -> v
 251 |             -> LTree k p v
 252 |             -> k
 253 |             -> LTree k p v
 254 |             -> LTree k p v
 255 | rSingleLeft k1 p1 v1 t1 m1 (LLoser _ (MkElem k2 p2 v2) t2 m2 t3) =
 256 |     rLoser k1 p1 v1 (rLoser k2 p2 v2 t1 m1 t2) m2 t3
 257 | rSingleLeft k1 p1 v1 t1 m1 (RLoser _ (MkElem k2 p2 v2) t2 m2 t3) =
 258 |     rLoser k2 p2 v2 (rLoser k1 p1 v1 t1 m1 t2) m2 t3
 259 | rSingleLeft _  _  _  _  _  _                                     =
 260 |   assert_total $ idris_crash "Data.OrdPSQ.Internal.rSingleLeft: malformed tree"
 261 | 
 262 | private
 263 | lSingleRight :  k
 264 |              -> p
 265 |              -> v
 266 |              -> LTree k p v
 267 |              -> k
 268 |              -> LTree k p v
 269 |              -> LTree k p v
 270 | lSingleRight k1 p1 v1 (LLoser _ (MkElem k2 p2 v2) t1 m1 t2) m2 t3 =
 271 |     lLoser k2 p2 v2 t1 m1 (lLoser k1 p1 v1 t2 m2 t3)
 272 | lSingleRight k1 p1 v1 (RLoser _ (MkElem k2 p2 v2) t1 m1 t2) m2 t3 =
 273 |     lLoser k1 p1 v1 t1 m1 (lLoser k2 p2 v2 t2 m2 t3)
 274 | lSingleRight _  _  _  _                                     _  _  =
 275 |   assert_total $ idris_crash "Data.OrdPSQ.Internal.lSingleRight: malformed tree"
 276 | 
 277 | private
 278 | rSingleRight :  Ord k
 279 |              => Ord p
 280 |              => k
 281 |              -> p
 282 |              -> v
 283 |              -> LTree k p v
 284 |              -> k
 285 |              -> LTree k p v
 286 |              -> LTree k p v
 287 | rSingleRight k1 p1 v1 (LLoser _ (MkElem k2 p2 v2) t1 m1 t2) m2 t3 =
 288 |     lLoser k2 p2 v2 t1 m1 (rLoser k1 p1 v1 t2 m2 t3)
 289 | rSingleRight k1 p1 v1 (RLoser _ (MkElem k2 p2 v2) t1 m1 t2) m2 t3 =
 290 |   case (p1, k1) `beats` (p2, k2) of
 291 |     True  =>
 292 |       rLoser k1 p1 v1 t1 m1 (lLoser k2 p2 v2 t2 m2 t3)
 293 |     False =>
 294 |       rLoser k2 p2 v2 t1 m1 (rLoser k1 p1 v1 t2 m2 t3)
 295 | rSingleRight _  _  _  _                                     _  _  =
 296 |   assert_total $ idris_crash "Data.OrdPSQ.Internal.rSingleRight: malformed tree"
 297 | 
 298 | private
 299 | lDoubleLeft :  Ord k
 300 |             => Ord p
 301 |             => k
 302 |             -> p
 303 |             -> v
 304 |             -> LTree k p v
 305 |             -> k
 306 |             -> LTree k p v
 307 |             -> LTree k p v
 308 | lDoubleLeft k1 p1 v1 t1 m1 (LLoser _ (MkElem k2 p2 v2) t2 m2 t3) =
 309 |   lSingleLeft k1 p1 v1 t1 m1 (lSingleRight k2 p2 v2 t2 m2 t3)
 310 | lDoubleLeft k1 p1 v1 t1 m1 (RLoser _ (MkElem k2 p2 v2) t2 m2 t3) =
 311 |   lSingleLeft k1 p1 v1 t1 m1 (rSingleRight k2 p2 v2 t2 m2 t3)
 312 | lDoubleLeft _  _  _  _  _  _                                     =
 313 |   assert_total $ idris_crash "Data.OrdPSQ.Internal.lDoubleLeft: malformed tree"
 314 | 
 315 | private
 316 | lDoubleRight :  Ord k
 317 |              => Ord p
 318 |              => k
 319 |              -> p
 320 |              -> v
 321 |              -> LTree k p v
 322 |              -> k
 323 |              -> LTree k p v
 324 |              -> LTree k p v
 325 | lDoubleRight k1 p1 v1 (LLoser _ (MkElem k2 p2 v2) t1 m1 t2) m2 t3 =
 326 |   lSingleRight k1 p1 v1 (lSingleLeft k2 p2 v2 t1 m1 t2) m2 t3
 327 | lDoubleRight k1 p1 v1 (RLoser _ (MkElem k2 p2 v2) t1 m1 t2) m2 t3 =
 328 |   lSingleRight k1 p1 v1 (rSingleLeft k2 p2 v2 t1 m1 t2) m2 t3
 329 | lDoubleRight _  _  _  _                                     _  _  =
 330 |   assert_total $ idris_crash "Data.OrdPSQ.Internal.lDoubleRight: malformed tree"
 331 | 
 332 | private
 333 | rDoubleLeft :  Ord k
 334 |             => Ord p
 335 |             => k
 336 |             -> p
 337 |             -> v
 338 |             -> LTree k p v
 339 |             -> k
 340 |             -> LTree k p v
 341 |             -> LTree k p v
 342 | rDoubleLeft k1 p1 v1 t1 m1 (LLoser _ (MkElem k2 p2 v2) t2 m2 t3) =
 343 |   rSingleLeft k1 p1 v1 t1 m1 (lSingleRight k2 p2 v2 t2 m2 t3)
 344 | rDoubleLeft k1 p1 v1 t1 m1 (RLoser _ (MkElem k2 p2 v2) t2 m2 t3) =
 345 |   rSingleLeft k1 p1 v1 t1 m1 (rSingleRight k2 p2 v2 t2 m2 t3)
 346 | rDoubleLeft _  _  _  _  _  _                                     =
 347 |   assert_total $ idris_crash "Data.OrdPSQ.Internal.rDoubleLeft: malformed tree"
 348 | 
 349 | private
 350 | rDoubleRight :  Ord k
 351 |              => Ord p
 352 |              => k
 353 |              -> p
 354 |              -> v
 355 |              -> LTree k p v
 356 |              -> k
 357 |              -> LTree k p v
 358 |              -> LTree k p v
 359 | rDoubleRight k1 p1 v1 (LLoser _ (MkElem k2 p2 v2) t1 m1 t2) m2 t3 =
 360 |   rSingleRight k1 p1 v1 (lSingleLeft k2 p2 v2 t1 m1 t2) m2 t3
 361 | rDoubleRight k1 p1 v1 (RLoser _ (MkElem k2 p2 v2) t1 m1 t2) m2 t3 =
 362 |   rSingleRight k1 p1 v1 (rSingleLeft k2 p2 v2 t1 m1 t2) m2 t3
 363 | rDoubleRight _  _  _  _                                     _  _  =
 364 |   assert_total $ idris_crash "Data.OrdPSQ.Internal.rDoubleRight: malformed tree"
 365 | 
 366 | private
 367 | lBalanceLeft :  Ord k
 368 |              => Ord p
 369 |              => k
 370 |              -> p
 371 |              -> v
 372 |              -> LTree k p v
 373 |              -> k
 374 |              -> LTree k p v
 375 |              -> LTree k p v
 376 | lBalanceLeft  k p v l m r =
 377 |   case size' (left r) < size' (right r) of
 378 |     True  =>
 379 |       lSingleLeft k p v l m r
 380 |     False =>
 381 |       lDoubleLeft k p v l m r
 382 | 
 383 | private
 384 | lBalanceRight :  Ord k
 385 |               => Ord p
 386 |               => k
 387 |               -> p
 388 |               -> v
 389 |               -> LTree k p v
 390 |               -> k
 391 |               -> LTree k p v
 392 |               -> LTree k p v
 393 | lBalanceRight k p v l m r =
 394 |   case size' (left l) > size' (right l) of
 395 |     True  =>
 396 |       lSingleRight k p v l m r
 397 |     False =>
 398 |       lDoubleRight k p v l m r
 399 | 
 400 | private
 401 | rBalanceLeft :  Ord k
 402 |              => Ord p
 403 |              => k
 404 |              -> p
 405 |              -> v
 406 |              -> LTree k p v
 407 |              -> k
 408 |              -> LTree k p v
 409 |              -> LTree k p v
 410 | rBalanceLeft  k p v l m r =
 411 |   case size' (left r) < size' (right r) of
 412 |     True  =>
 413 |       rSingleLeft k p v l m r
 414 |     False =>
 415 |       rDoubleLeft k p v l m r
 416 | 
 417 | private
 418 | rBalanceRight :  Ord k
 419 |               => Ord p
 420 |               => k
 421 |               -> p
 422 |               -> v
 423 |               -> LTree k p v
 424 |               -> k
 425 |               -> LTree k p v
 426 |               -> LTree k p v
 427 | rBalanceRight k p v l m r =
 428 |   case size' (left l) > size' (right l) of
 429 |     True  =>
 430 |       rSingleRight k p v l m r
 431 |     False =>
 432 |       rDoubleRight k p v l m r
 433 | 
 434 | private
 435 | lBalance :  Ord k
 436 |          => Ord p
 437 |          => k
 438 |          -> p
 439 |          -> v
 440 |          -> LTree k p v
 441 |          -> k
 442 |          -> LTree k p v
 443 |          -> LTree k p v
 444 | lBalance k p v Start m r     =
 445 |   lLoser k p v Start m r
 446 | lBalance k p v l     m Start =
 447 |   lLoser k p v l m Start
 448 | lBalance k p v l     m r     =
 449 |   case size' r > omega * size' l of
 450 |     True  =>
 451 |       lBalanceLeft k p v l m r
 452 |     False =>
 453 |       case size' l > omega * size' r of
 454 |         True  =>
 455 |           lBalanceRight k p v l m r
 456 |         False =>
 457 |           lLoser k p v l m r
 458 | 
 459 | private
 460 | rBalance :  Ord k
 461 |          => Ord p
 462 |          => k
 463 |          -> p
 464 |          -> v
 465 |          -> LTree k p v
 466 |          -> k
 467 |          -> LTree k p v
 468 |          -> LTree k p v
 469 | rBalance k p v Start m r     =
 470 |   rLoser k p v Start m r
 471 | rBalance k p v l     m Start =
 472 |   rLoser k p v l m Start
 473 | rBalance k p v l     m r     =
 474 |   case size' r > omega * size' l of
 475 |     True  =>
 476 |       rBalanceLeft k p v l m r
 477 |     False =>
 478 |       case size' l > omega * size' r of
 479 |         True  =>
 480 |           rBalanceRight k p v l m r
 481 |         False =>
 482 |           rLoser k p v l m r
 483 | 
 484 | --------------------------------------------------------------------------------
 485 | --          Tournament View
 486 | --------------------------------------------------------------------------------
 487 | 
 488 | public export
 489 | data TourView : (k : Type) -> (p : Type) -> (v : Type) -> Type where
 490 |   Null   :  TourView k p v
 491 |   Single :  Elem k p v
 492 |          -> TourView k p v
 493 |   Play   :  OrdPSQ k p v
 494 |          -> OrdPSQ k p v
 495 |          -> TourView k p v
 496 | 
 497 | %runElab derive "TourView" [Eq,Ord,Show]
 498 | 
 499 | export
 500 | tourView :  OrdPSQ k p v
 501 |          -> TourView k p v
 502 | tourView Void                                =
 503 |   Null
 504 | tourView (Winner e Start _)                  =
 505 |   Single e
 506 | tourView (Winner e (RLoser _ e' tl m tr) m') =
 507 |   Winner e tl m `Play` Winner e' tr m'
 508 | tourView (Winner e (LLoser _ e' tl m tr) m') =
 509 |   Winner e' tl m `Play` Winner e tr m'
 510 | 
 511 | ||| Take two pennants and returns a new pennant that is the union of
 512 | ||| the two with the precondition that the keys in the first tree are
 513 | ||| strictly smaller than the keys in the second tree.
 514 | export
 515 | play :  Ord k
 516 |      => Ord p
 517 |      => OrdPSQ k p v
 518 |      -> OrdPSQ k p v
 519 |      -> OrdPSQ k p v
 520 | Void                          `play` t'                                  =
 521 |   t'
 522 | t                             `play` Void                                =
 523 |   t
 524 | (Winner e@(MkElem k p v) t m) `play` (Winner e'@(MkElem k' p' v') t' m') =
 525 |   case (p, k) `beats` (p', k') of
 526 |     True  =>
 527 |       Winner e (rBalance k' p' v' t m t') m'
 528 |     False =>
 529 |       Winner e' (lBalance k p v t m t') m'
 530 |