A search queue.

Keys in t.

Priorities in t.

empty is the search queue that contains no bindings.

sg k p is the singleton search queue, containing only the binding k -> p.

t1 ++ t2 contains bindings from t1 and t2. If a key k is bound in both, the result has the binding with lower priority.

Hence,

• t1 ++ t2 = t2 ++ t1
• (t1 ++ t2) ++ t3 = t1 ++ (t2 ++ t3)

is_empty t is true iff t is empty.

size t is the number of distinct bindings in t.

find k t is true iff k is bound in t.

find k t is Some p if t contains the binding k -> p, or None otherwise.

add k p t is t with the binding k -> p.

Note that add does not commute: add k p2 (add k p1 q) <> add k p1 (add k p2 q) when p1 <> p2. Compare push.

push k p t is t with k bound to the lower of p and its previous priority in t, if it exists — when t contains k -> p0, the result contains k -> min p0 p, otherwise it contains k -> p.

Note that push commutes: push k p1 (push k p2 q) = push k p2 (push k p1 q). Compare add.

remove k t is t without any bindings for k.

adjust k f t is t with the binding k -> p replaced by k -> f p. When k is not bound in t, the result is t.

update k f t is t with the binding for k given by f.

When t contains a binding k -> p, the new binding is given by f (Some p); otherwise, by f None.

When the result of applying f is Some p', the binding k -> p' is added to t; otherwise, the binding for k is removed from t.

split_at k t splits t into (t0, t1), such that for all keys k0 in t0, k0 <= k, for all keys k1 in t1, k1 > k, and t = t0 ++ t1.

min t is the binding Some (k, p) where p is minimal in t, or None if t is empty.

When several keys share the minimal priority, min t is the binding with the smallest key.

rest t is t without the binding min t, or None.

pop t is (min t, rest t), or None.

fold_at_most p0 f z q folds f over bindings k -> p where p is not larger than p0, in key-ascending order.

iter_at_most p0 f q applies f to the bindings k -> p where p is not larger than p0, in key-ascending order.

iter_at_most p0 f q is the sequence of bindings k -> p where p not larger than p0, in key-ascending order.

of_list kps is t with bindings kps.

When pks contains multiple priorities for a given k, the lowest one wins.

of_sorted_list kps is t with bindings kps. kps must contain the bindings in key-ascending order without repetitions. When this is not the case, the result is undefined.

Note When applicable, this operation is faster than of_list.

of_seq kps is of_list (List.of_seq kps).

of_seq kps t is t ++ of_seq kps.

to_list t are all the bindings in t in key-ascending order.

to_seq t iterates over bindings in t in key-ascending order.

fold f z t is f k0 p0 (f k1 p1 ... (f kn pn z)), where k0, k1, ..., kn are in ascending order.

iter f t applies f to all bindings in t in key-ascending order.

to_priority_list t are the bindings in t in priority-ascending order.

Note Priority-ordered traversal is slower than key-ordered traversal.

to_priority_seq t is the sequence version of to_priority_list.

Note For traversing the whole t, to_priority_list is more efficient.

filter p t is the search queue with exactly the bindings in t which satisfy the predicate p.

partition p t is (filter p t, filter np t) where np is the negation of p.

pp ?sep pp_kp ppf t pretty-prints t to ppf, using pp_kp to print the bindings and ~sep to separate them.

~sep defaults to Format.print_space.

pp_dump pp_k pp_f ppf t is a handier pretty-printer for development.