module type OrderedContainer =
A (persistent) ordered container, generalising the standard
val of_list :
elt list -> t
Convert a list of elements to a container.
val to_list :
t -> elt list
Convert to a list of unique, sorted elements.
val endomap :
(elt -> elt) -> t -> t
Map a set of elements to another set of elements of the same type.
The size of the set may reduce if there are duplicates produced.
val map_to :
('b -> 'a -> 'a) -> 'a -> (elt -> 'b) -> t -> 'a
map_to add empty f set converts every element of
and then folds over the new collection of elements using as starting
empty and folding operation
val opt_map_to :
('b -> 'a -> 'a) ->
'a -> (elt -> 'b option) -> t -> 'a
opt_map_to add empty f set converts every element of
and then folds over the elements of the new collection which are Some
using as starting value
empty and folding operation
add. That is,
it is equivalent to calling
map_to (Option.dest Fun.id add) empty f set.
val map_to_list :
(elt -> 'a) -> t -> 'a list
map_to_list f set applies
f to every element and constructs a list
of results. The list is ordered just like the container.
val weave :
(elt -> 'a -> 'a list) ->
(elt -> 'a -> 'b) ->
('b list -> 'b) -> t -> 'a -> 'b
Weave combinator - used in the SL Model Checker.
weave split tie join xs acc
is a generalised form of a fold - it takes as arguments three
join), a container
xs to weave (i.e. fold) over,
and an accumulator
acc. Whereas a fold combines the previously accumulated
value with the next value in the set to produce the new accumulated
value, a weave uses its
split argument to combine the next element in
the set with the previously accumulated value to produce a *list* of new
accumulated values - not just a single new value. Each new value in this
list is then used as the accumulator for a distinct recursive call to the
weave function - compared with a single recursive call for a fold. Thus,
at this point, the weave produces a list of final values, which are then
combined using the
join function argument. Furthermore, in constrast to
fold, the weave combinator treats the final element in the list in a
special way, producing only a single value using the
val find :
(elt -> bool) -> t -> elt
find p set returns the first element of
that satisfies the predicate
Not_found if there is no value that satisfies
val find_opt :
(elt -> bool) -> t -> elt option
find_opt pred set returns
Some x for the first
pred x = true, or
val find_map :
(elt -> 'a option) -> t -> 'a option
Optimisation for finding and converting at the same time.
find_map f set
f x for the first
set such that
f x is not
val union_of_list :
t list -> t
Union a list of sets.
val subsets :
t -> t list
Generate all subsets of a set.
val fixpoint :
(t -> t) ->
t -> t
val del_first :
(elt -> bool) -> t -> t
Remove first element satisfying the given predicate.
val disjoint :
t -> t -> bool
Decide if there are no common elements.
val mk_unifier :
('a, 'b, elt) Unification.cps_unifier ->
('a, 'b, t) Unification.cps_unifier
mk_unifier total linear elt_unifier produces a unifier
u for a set of elements
using the unifier
elt_unifier for a single element. If
total is set to true
then the unifier should ensure that if
u succeeds in unifying a set
xs with a
ys then all elements of
ys match with an element of
set to true, then
u must additionally ensure that in calculating a unifying
subsitution no element of
ys is used more than once.