Data.Heap.Mutable.ModelC

This module provides a variant of a mutable binary min heap that is used elsewhere to implement Dijkstra's algorithm. It is unlikely that there are other uses for this specific implementation. The binary heap in this module uses the standard array-as-binary-heap approach where the 0-index item in the array is unused, the 1-index item is the root, and the n element has its left child at 2n and its right child at 2n + 1. The following additions (which are uncommon) have been made:

• This heap only supports Int elements but is polymorphic in the priority data type.
• When the heap is initialized, it is given an Int. This represents and exclusive upper bound on the allowed elements. For example, if you pass 40, then you can only push 0 through 39 as elements.
• Most of the functions in this module take an extra Int (right after the RawHeap argument). This Int tells us the number of items currently in the heap. In some cases, this argument is not even used, but it is present so that LiquidHaskell can provide extra bound-checking assurances. For example, if we initialize the heap with new 90, and then push three elements, we do not want to be able to read the 83rd element in the rawHeapPriorities and rawHeapElements arrays. Even though the this index is technically in bounds, the element stored there is not actually in the heap. Many places where this bounding number is passed around to a function should be eliminated by the inliner and do not affect runtime performance. The ModelD module provides a much more usable heap implementation where the currenty heap size is stored in a MutVar. It is not implemented as a MutVar in here because LiquidHaskell cannot (to my knowledge) use mutable values for meaningful proofs.
• This heap implements decrease-key as a part of push. If you push an already existing element onto the heap, the priority of the existing one and the priority of the one you are attempting to push will be combined with the Monoid instance. (Note: this could definitely be weakened to Semigroup). At the moment, only bubble up is attempted after this operation, so if this causes the priority to increase, the heap becomes invalid (but not in a way that causes segfaults).

As a result of the last constraint, the Monoid instance and Ord instance of the priority type must obey these additional laws:

mappend a b ≤ a
mappend a b ≤ b
mempty ≥ c

In more colloquial terms, the monoidal append of two priorities must be less than or equal to the smaller of the two. Additionally, mempty must be the largest priority.

Documentation

data RawHeap s p

Constructors

RawHeap

Fields

• rawHeapBound :: !Int

  This bound is exclusive

• rawHeapPriorities :: !(MutableArray s p)

  Binary tree of priorities

• rawHeapElements :: !(MutableByteArray s)

  Binary tree of elements

• rawHeapInvertedIndex :: !(MutableByteArray s)

  Lookup binary tree index by element, used for increase and decrease priority

readHeapPriority :: PrimMonad m => RawHeap (PrimState m) p -> Int -> Int -> m p

readHeapElement :: PrimMonad m => RawHeap (PrimState m) p -> Int -> Int -> m Int

writeHeapPriority :: PrimMonad m => RawHeap (PrimState m) p -> Int -> Int -> p -> m ()

writeHeapElement :: PrimMonad m => RawHeap (PrimState m) p -> Int -> Int -> Int -> m ()

readHeapInvertedIndex :: PrimMonad m => RawHeap (PrimState m) p -> Int -> Int -> m Int

writeHeapInvertedIndex :: PrimMonad m => RawHeap (PrimState m) p -> Int -> Int -> Int -> m ()

swapHeap :: PrimMonad m => RawHeap (PrimState m) p -> Int -> Int -> Int -> m ()

pop :: (PrimMonad m, Ord p) => RawHeap (PrimState m) p -> Int -> m (Int, Maybe (p, Int))

bubbleDown :: forall p m. (Ord p, PrimMonad m) => RawHeap (PrimState m) p -> Int -> m ()

unsafePush :: forall m p k. (Ord p, Monoid p, PrimMonad m) => p -> Int -> Int -> RawHeap (PrimState m) p -> m Int

appendElem :: (Ord p, PrimMonad m) => p -> Int -> Int -> RawHeap (PrimState m) p -> m ()

combineElem :: (Monoid p, Ord p, PrimMonad m) => p -> Int -> Int -> Int -> RawHeap (PrimState m) p -> m ()

bubbleUp :: (Ord p, PrimMonad m) => Int -> Int -> RawHeap (PrimState m) p -> m ()

new :: (PrimMonad m, Monoid p) => Int -> m (Int, RawHeap (PrimState m) p)