module ListSet: Utilsigs.OrderedContainer with type elt = t
A set of term pairs
type
include Utilsigs.BasicType
include Set.S
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 set using f,
and then folds over the new collection of elements using as starting
value empty and folding operation add.
val opt_map_to : ('b -> 'a -> 'a) ->
'a -> (elt -> 'b option) -> t -> 'a
opt_map_to add empty f set converts every element of set using f,
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
operations (split, tie, and 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 tie function.
val find : (elt -> bool) -> t -> elt
find p set returns the first element of set
that satisfies the predicate p.
Raise Not_found if there is no value that satisfies p in set.
val find_opt : (elt -> bool) -> t -> elt option
find_opt pred set returns Some x for the first x in set such
that pred x = true, or None.
val find_map : (elt -> 'a option) -> t -> 'a option
Optimisation for finding and converting at the same time. find_map f set
will return f x for the first x in set such that f x is not None,
or None otherwise.
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 : bool ->
bool ->
('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
set ys then all elements of ys match with an element of xs; if linear is
set to true, then u must additionally ensure that in calculating a unifying
subsitution no element of ys is used more than once.