Module type Index.PriorityQueue

module type PriorityQueue = sig .. end

type elt 

Type of elements.

type t 

Type of priority queues of elements.

val create : elt -> t

An empty queue.

val length : t -> int

length q is the number of elements in the queue.

• Ensure length q >= 0

val is_empty : t -> bool

is_empty q is true iff there are no elements enqueued in q.

• Ensure is_empty q = (length q = 0)

val mem : t -> elt -> bool

mem q e is true iff e is enqueued in q.

val head : t -> elt

head q is the highest priority element of q.

• Require not (is_empty q)

val enqueue : t -> elt -> unit

enqueue q e enqueues the element e. The position of e in q is determined by its priority.

Note: The default priority of elements is 0.0.

val dequeue : t -> elt

dequeue q removes the highest priority element from q.
Returns The element removed.

• Require not (is_empty q)

val drop : t -> unit

drop q removes the highest priority element from q.

• Require not (is_empty q)

val priority : t -> elt -> float

The priority of an element.

Note: The default priority of elements is 0.0.

val inc_priority : t -> elt -> float -> unit

inc_priority q e x adds x to the priority of element e. If e is enqueued, it will move up the queue as necessary.

• Require 0.0 < x
• Require priority q e <= max_float -. x

val scale : t -> float -> unit

scale q x multiplies the priority of every element by the constant factor x. The ordering of elements in the queue is unchanged.

• Require x > 0.0.