Library
Module
Module type
Parameter
Class
Class type
Signature of priority search queues.
Keys in t
.
Priorities in t
.
val empty : t
empty
is the search queue that contains no bindings.
val size : t -> int
size t
is the number of distinct bindings in t
.
k
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
. If k
is already bound in t
, that binding is replaced.
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
.
p
min t
is the binding Some (k, p)
where p
is minimal in t
, or None
if t
is empty
.
Note that min t
is actually the smallest (p, k)
in t
— when multiple bindings share p
, min t
is the one with the smallest k
.
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 there are multiple bindings for a given k
, the rightmost binding is chosen.
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 This operation is faster than of_list
.
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
.