module ListSet:`Utilsigs.OrderedContainer`

`with type elt = t`

A set of term pairs

`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 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.