#### inferno

Library

Module

Module type

Parameter

Class

Class type

## Parameters

`module S : sig ... end`

## Signature

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

.

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

`is_representative v`

determines whether the variable `v`

is currently the representative element of its equivalence class.