Data.HashPSQ.Internal

Hash Priority Search Queue Internals

Definitions

data Bucket : Type -> Type -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

MkBucket : k -> v -> OrdPSQ k p v -> Bucket k p v

Hints:

Eq k => Eq v => Eq p => Eq (Bucket k p v)

Ord k => Ord v => Ord p => Ord (Bucket k p v)

Show k => Show v => Show p => Show (Bucket k p v)

toBucket : Ord k => Ord p => OrdPSQ k p v -> Maybe (p, Bucket k p v)

Totality: total
Visibility: export

mkBucket : Ord k => Ord p => k -> p -> v -> OrdPSQ k p v -> (p, Bucket k p v)

  Smart constructor which takes care of placing the minimum element directly
  in the Bucket.

Totality: total
Visibility: export

data HashPSQ : Type -> Type -> Type -> Type

  A priority search queue with keys of type k and priorities of type p
  and values of type v.
  A HashPSQ offers very similar performance to NatPSQ.
  In case of collisions, it uses an OrdPSQ locally to solve those.
  This means worst case complexity is usually given by O(min(n,W), log n), where W is the number of bits in an Int.
  This simplifies to O(min(n, W)) since log n is always smaller than W on current machines.

Totality: total
Visibility: public export
Constructor: 

MkHashPSQ : NatPSQ p (Bucket k p v) -> HashPSQ k p v

Hints:

Eq p => Eq k => Eq v => Eq (HashPSQ k p v)

Functor (HashPSQ k p)

Ord p => Ord k => Ord v => Ord (HashPSQ k p v)

Show p => Show k => Show v => Show (HashPSQ k p v)