A unifier maintains a graph whose vertices are equivalence classes of variables. With each equivalence class, a piece of information of type
data is attached.
'a structure describes the information that is attached with each class. It is parameterized over a type
'a of children. In the definition of the type
'a is instantiated with
data is a synonym for
variable structure. So, the data attached with an equivalence class of variables is a structure whose children are variables.
unify v1 v2 equates the two variables
v2. These variables become part of the same equivalence class. The structures carried by
v2 are combined by invoking the
conjunction function supplied by the user as an argument to
conjunction itself is given access to an
equate function which submits an equality constraint to the unifier.
If a logical inconsistency is detected,
Unify (v1, v2) is raised, and the state of the unifier is unaffected. (The unifier undoes any updates that it may have performed.) For this undo machinery to work correctly, the
conjunction function provided by the user must not perform any side effect.
Unification can create cycles in the graph maintained by the unifier. By default, the unifier tolerates these cycles. An occurs check, which detects these cycles, is provided separately: see
OccursCheck.Make. Because cycles are permitted, the variables
v2 carried by the exception
Unify can participate in cycles. When reporting a unification error, a cyclic decoder should be used: see
val is_representative : variable -> bool
is_representative v determines whether the variable
v is currently the representative element of its equivalence class.