Module Sl_term.Set

module Set: Utilsigs.OrderedContainer  with type elt = t
An ordered set of terms.

type t 
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 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.