package inferno

  1. Overview
  2. Docs

This unifier operates with the structure specified by the submodule Data.

type variable

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.

type 'a structure = 'a Data.structure

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

type data = variable structure

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.

val get : variable -> data

get v is the structure currently attached with the (equivalence class of the) variable v. The structure that is attached with a class can change when the unifier is invoked.

exception Unify of variable * variable

This exception is raised by unify.

val unify : variable -> variable -> unit

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.


Innovation. Community. Security.