Data.NatPSQ.Internal

Ordered Nat Priority Search Queue Internals

Definitions

Size : Type

  Size is a natural machine word
  (Bits32/Bits64 or the size of an unsigned Int on the host system).

Totality: total
Visibility: public export

Key : Type

  The Nat type are keys for the queue (Ordered Nat Priority Search Queue).

Totality: total
Visibility: public export

Mask : Type

  We store Masks as the index of the bit that determines the branching.

Totality: total
Visibility: public export

zero : Key -> Mask -> Bool

Totality: total
Visibility: export

noMatch : Key -> Key -> Mask -> Bool

Totality: total
Visibility: export

branchMask : Key -> Key -> Mask

Totality: total
Visibility: export

data NatPSQ : Type -> Type -> Type

  A priority search queue with Nat keys
  and priorities of type p and values of type v.
  Many operations have a worst-case complexity of O(min(n,W)).
  This means that the operation can become linear in the number of elements with a maximum of W
  (the number of bits in an Int (32 or 64)).
  It is generally much faster than an OrdPSQ.

Totality: total
Visibility: public export
Constructors:

Bin : Key -> p -> v -> Mask -> NatPSQ p v -> NatPSQ p v -> NatPSQ p v

Tip : Key -> p -> v -> NatPSQ p v

Nil : NatPSQ p v

Hints:

Eq p => Eq v => Eq (NatPSQ p v)

Foldable (NatPSQ p)

Functor (NatPSQ p)

Ord p => Ord v => Ord (NatPSQ p v)

Show p => Show v => Show (NatPSQ p v)