module Make:
type
A term denotes a disjoint sum of sets with unification
variables inside.
val variable : Set.t -> term
variable s returns a fresh unification variable whose
denotation cannot intersect s.
val svariable : unit -> term
svariable () is equivalent to variable Set.empty.
val empty : term
empty denotes the constant empty set.
val sum : Set.t -> term -> term
sum s t adds s to the sum denoted by t.
Error is raised if s intersects t.
val unify : term -> term -> unit
unify t t' solves the equality between two disjoint sums
by determining the unification variable if necessary.
If the equality is not satisfiable, Error is raised.
exception Error
Error is raised if the construction of a disjoint sum has
failed.
val print : term -> string
print t returns a string representation of the disjoint
sum t.