
  0 | module PriorityQueue
  1 | 
  2 | %default total
  3 | 
  4 | public export
  5 | interface PriorityQueue (queue : Type -> Type) where
  6 |   ||| Return an empty queue
  7 |   empty : {auto o : Ord e} -> queue e
  8 |   ||| Create a queue containing only one element
  9 |   singleton : {auto o : Ord e} -> (element : e) -> queue e
 10 |   ||| Return true if the queue is empty
 11 |   isNull : queue e -> Bool
 12 |   ||| Returns the number of elements in the queue
 13 |   length : queue e -> Nat
 14 |   ||| Find the minimum element, if there is one
 15 |   findMin : queue e -> Maybe e
 16 |   ||| Merge two queues
 17 |   meld : (x, y : queue e) -> queue e
 18 |   ||| Insert an element into the queue
 19 |   insert : (element : e) -> queue e -> queue e
 20 |   ||| Removes the minimum element from the queue
 21 |   ||| Does nothing to the empty queue
 22 |   deleteMin : queue e -> queue e
 23 |   ||| Converts an Ord t => Foldable m => m t into a queue of t
 24 |   fromFoldable : Ord e => Foldable m => (xs : m e) -> queue e
 25 |   fromFoldable xs =
 26 |     foldl (flip insert) empty xs
 27 |   ||| Foldl implementation for queues
 28 |   queueFoldl : (f : acc -> e -> acc) -> (init : acc) -> queue e -> acc
 29 |   queueFoldl f acc queue =
 30 |     case findMin queue of
 31 |       Nothing => acc
 32 |       Just val =>
 33 |         queueFoldl f (f acc val) (assert_smaller queue (deleteMin queue))
 34 | 
 35 | export
 36 | {q : _} -> PriorityQueue q => Foldable q where
 37 |   -- This is slow, but there's no other sensible way to do this, only the front
 38 |   -- of the queue is accessible
 39 |   foldr f acc queue = foldr f acc (reverse $ queueFoldl (flip (::)) [] queue)
 40 |   foldl = queueFoldl
 41 |   null = isNull
 42 |   toList queue = reverse $ queueFoldl (flip (::)) [] queue
 43 |