0 | module Structures.PriorityQueue.Bootstrap
  1 |
  2 | import Structures.PriorityQueue
  3 |
  4 | ||| Datastructurally bootstrapped priority queue per Optimal purely functional
  5 | ||| priority queues (Brodal, G. S., & Okasaki, C. (1996).)
  6 | |||
  7 | ||| Reduces the time of every operation except `deleteMin` to O(1), with
  8 | ||| `deleteMin` remaining O(log n)
  9 | |||
 10 | ||| This internally uses overridden Ord and Eq implementations, the Ord
 11 | ||| implementation should always be correct for the application, but the Eq
 12 | ||| implementation only compares on the minimum value of a queue, and may break
 13 | ||| queue implementations that rely on proper equality for some operations,
 14 | ||| which does not include any of the implementations in this package.
 15 | export
 16 | data Bootstrap : (inner : Type -> Type) -> (e : Type) -> Type where
 17 |   Empty : {auto o : Ord e} -> {auto o' : Ord (Bootstrap inner e)}
 18 |     -> Bootstrap inner e
 19 |   Single : {auto o : Ord e} -> {auto o' : Ord (Bootstrap inner e)}
 20 |     -> (element : e) -> Bootstrap inner e
 21 |   Root : {auto o : Ord e} -> {auto o' : Ord (Bootstrap inner e)}
 22 |     -> (element : e) -> (queue : inner (Bootstrap inner e)) -> Bootstrap inner e
 23 | %name Bootstrap btq, ctq, dtq
 24 |
 25 | ||| Eq implementation that compares on the minimum value of each queue, this
 26 | ||| should be, but could potentialy break a queue implementation that relies on
 27 | ||| the equality of its elements
 28 | Eq e => Eq (Bootstrap inner e) where
 29 |   (==) Empty Empty = True
 30 |   (==) Empty _ = False
 31 |   (==) (Single element) Empty = False
 32 |   (==) (Single element) (Single x) = element == x
 33 |   (==) (Single element) (Root x _) = element == x
 34 |   (==) (Root element _) Empty = False
 35 |   (==) (Root element _) (Single x) = element == x
 36 |   (==) (Root element _) (Root x _) = element == x
 37 |
 38 | ||| Ord implementation that compares on the minimum value of each queue. This
 39 | ||| _should_ always be correct for this application.
 40 | {inner : _} -> PriorityQueue inner => Ord e => Ord (Bootstrap inner e) where
 41 |   compare Empty Empty = EQ
 42 |   compare Empty _ = LT
 43 |   compare (Single element) Empty = GT
 44 |   compare (Single {o} x) (Single y) =
 45 |     compare @{o} x y
 46 |   compare (Single {o} x) (Root y _) =
 47 |     compare @{o} x y
 48 |   compare (Root x _) Empty = GT
 49 |   compare (Root {o} x _) (Single y) =
 50 |     compare @{o} x y
 51 |   compare (Root {o} x _) (Root y _) =
 52 |     compare @{o} x y
 53 |
 54 | export
 55 | {inner : _} -> PriorityQueue inner => PriorityQueue (Bootstrap inner) where
 56 |   empty = Empty
 57 |
 58 |   singleton element = singleton element
 59 |
 60 |   isNull Empty = True
 61 |   isNull _ = False
 62 |
 63 |   findMin Empty = Nothing
 64 |   findMin (Single element) = Just element
 65 |   findMin (Root element queue) = Just element
 66 |
 67 |   length xs = length' xs 0 []
 68 |     where
 69 |     length' : (xs : Bootstrap inner e) -> (acc : Nat) ->
 70 |       (stack : List (Bootstrap inner e)) -> Nat
 71 |     length' Empty acc [] = acc
 72 |     length' Empty acc (y :: ys) =
 73 |       length' y acc ys
 74 |     length' (Single element) acc [] =
 75 |       1 + acc
 76 |     length' (Single element) acc (y :: ys) =
 77 |       length' y (1 + acc) ys
 78 |     length' (Root element queue) acc ys =
 79 |       case findMin queue of
 80 |         Nothing =>
 81 |           length' Empty (1 + acc) ys
 82 |         Just y =>
 83 |           length' (Root element (deleteMin queue)) acc (y :: ys)
 84 |
 85 |   meld Empty y = y
 86 |   meld (Single {o} {o'} element) Empty = Single {o} {o'} element
 87 |   meld (Single {o} {o'} x) (Single y) =
 88 |     if (<) @{o} x y
 89 |       then Root {o} {o'} x (singleton {o = o'} (Single {o} {o'} y))
 90 |       else Root {o} {o'} y (singleton {o = o'} (Single {o} {o'} x))
 91 |   meld (Single {o} {o'} x) (Root y queue) =
 92 |     if (<) @{o} x y
 93 |       then Root {o} {o'} x (insert (Single {o} {o'} y) queue)
 94 |       else Root {o} {o'} y (insert (Single {o} {o'} x) queue)
 95 |   meld (Root {o} {o'} element queue) Empty = Root {o} {o'} element queue
 96 |   meld (Root {o} {o'} x queue) (Single y) =
 97 |     if (<) @{o} x y
 98 |       then Root {o} {o'} x (insert (Single {o} {o'} y) queue)
 99 |       else Root {o} {o'} y (insert (Single {o} {o'} x) queue)
100 |   meld (Root {o} {o'} x queue) (Root y queue') =
101 |     if (<) @{o} x y
102 |       then Root {o} {o'} x (insert (Single {o} {o'} y) (meld queue queue'))
103 |       else Root {o} {o'} y (insert (Single {o} {o'} x) (meld queue queue'))
104 |
105 |   insert element Empty = Single element
106 |   insert element (Single x) =
107 |     if element < x
108 |       then Root element (singleton (Single x))
109 |       else Root x (singleton (Single element))
110 |   insert element (Root x queue) =
111 |     if element < x
112 |       then Root element (insert (Single x) queue)
113 |       else Root x (insert (Single element) queue)
114 |
115 |   deleteMin Empty = Empty
116 |   deleteMin (Single element) = Empty
117 |   deleteMin (Root {o} {o'} element queue) =
118 |     case findMin queue of
119 |       Nothing => Empty
120 |       Just next =>
121 |         let rest = deleteMin queue
122 |         in case next of
123 |           Empty => Empty {o} {o'}
124 |           (Single x) => Root {o} {o'} x rest
125 |           (Root e q) => Root {o} {o'} e (meld q rest)
126 |