Unifier.MakeThis module implements a unification algorithm for first-order terms whose structure is specified by the parameter S. In particular, the operation S.conjunction specifies how two structural constraints bearing on a variable are combined.
module S : sig ... endA unifier maintains a graph whose vertices are equivalence classes of variables. With each equivalence class, a piece of information of type data is attached.
type 'a structure = 'a S.structureThe type '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 data, 'a is instantiated with variable.
By definition, 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 v1 and v2. These variables become part of the same equivalence class. The structures carried by v1 and v2 are combined by invoking the conjunction function supplied by the user as an argument to Unifier.Make. 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 v1 and v2 carried by the exception Unify can participate in cycles. When reporting a unification error, a cyclic decoder should be used: see Decoder.Make.
val is_representative : variable -> boolis_representative v determines whether the variable v is currently the representative element of its equivalence class.