Previous  Up  Next

Module Unifier (.ml)

module Unifier: sig .. end
This module implements unification of (ranked) multi-equations over a row algebra, that is, an algebra obtained by extending a free algebra A with rows (see module CoreAlgebra).

For the purposes of this module, a rank is an element of an arbitrary total order. A rank is associated with every multi-equation. When two multi-equations are merged, the smaller rank is kept.

It is understood that finite and infinite terms are legal -- no occur check is performed here.

exception CannotUnify of Positions.position * MultiEquation.crterm * MultiEquation.crterm
val unify : ?tracer:(MultiEquation.variable -> MultiEquation.variable -> unit) ->
       Positions.position ->
       (MultiEquation.variable -> unit) ->
       MultiEquation.variable -> MultiEquation.variable -> unit
unify pos register v1 v2 equates the variables v1 and v2. That is, it adds the equation v1 = v2 to the system of equations which v1 and v2 are already implicitly part of. Then, it rewrites the system of equations in a number of ways until an inconsistency is found or a standard (satisfiable) form is reached. In the former case, the exception Inconsistency is raised. In the latter case, the function returns normally, without returning a result.

Every variable that is newly allocated during the process is passed to register, so as to make the unifier's client aware of its existence. The variable's rank is already properly initialized when register is called.