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.
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)
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
.
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
.
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
.
p
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.
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
.
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
.