Module MultiEquation (.ml)

module MultiEquation: sig .. end

type variable = descriptor UnionFind.point 

The structure of the terms manipulated by a unifier is fixed and made visible to the outside, because it must be accessible to the constraint solver, which is built on top of a unifier.

The unifier relies on a union/find algorithm. A variable is represented as a point of the union/find algorithm. An equivalence class of points corresponds, roughly speaking, to what is called a ``standard multi-equation'' in the book. Every multi-equation carries a descriptor.

type descriptor = {

A descriptor contains several pieces of information, the most important of which is the structure of the multi-equation, or, in other words, its unique non-variable member, if there is one.

If the structure field is None, then the multi-equation only has variable members. If it is Some t, then the multi-equation contains a non-variable member, namely the term t. Note that t is a term whose head symbol belongs to the algebra and whose parameters are again variables. Thus, the unifier works with so-called ``small terms'' only.

The rank field contains the rank currently attached to the multi-equation. As far as the unifier is concerned, ranks have no meaning. The unifier only knows that ranks are totally ordered. When two multi-equations are fused, the smaller rank is kept.

The mark field is transient, and may be used by the unifier's client for any purpose.

type structure = variable CoreAlgebra.term 

A multi-equation can be related to a term. In that case, it is structured.

type variable_kind = 

There are two kinds of variable. A Flexible variable can be unified with other variables or terms. A Rigid variable cannot.

type tname = 

tname is the type of type identifiers.

type crterm = variable CoreAlgebra.arterm 

The type of term of arbitrary depth.

val is_structured : variable -> bool

is_structured v tests if v is related to a term.

val are_equivalent : variable -> variable -> bool

are_equivalent v1 v2 tests if v1 and v2 are in the same multi-equation.

val variable_name : variable -> tname option

variable_name v returns the name of v if it exists.

val variable_structure : variable -> structure option

variable_structure v returns the structure of v if it exists.

val explode : crterm -> variable CoreAlgebra.term

explode t converts an arbitrary depth tree into a 1-depth one using variables.

val variable : variable_kind ->
       ?name:tname ->
       ?structure:crterm ->
       ?pos:Positions.position -> unit -> variable

variable() returns a new variable.

val variable_list : variable_kind ->
       'a list -> variable list * ('a * crterm) list

variable_list xs allocates a fresh variable for every element in the list xs, and returns both a list of these variables and an association list that maps elements to variables, viewed as types.

val variable_list_from_names : (tname ->
        variable_kind * tname option) ->
       tname list ->
       variable list *
       (tname * crterm) list

variable_list_from_strings f xs allocates a fresh variable for every string in the list xs, and returns both a list of these variables and an association list that maps elements to variables, viewed as types. The kind is determined using the provided function f.

val variable_set : (tname ->
        variable_kind * tname option) ->
       Misc.StringSet.t ->
       variable list *
       (crterm * Positions.position) Misc.StringMap.t

variable_set xs allocates a fresh variable for every element in the set xs, and returns both a list of these variables and a map of elements to variables.

val is_rigid : variable -> bool

is_rigid v returns true if v is a constant or rigid variable.

val is_flexible : variable -> bool

is_flexible v returns true if v is a flexible variable.

type pool 

pool is an abstract type denoting a set of type variables related to a variable binding location.

val inhabitants : pool -> variable list

inhabitants p returns the type variables of a pool.

val number : pool -> int

number p returns the rank of a p.

val new_pool : pool -> pool

new_pool p introduces a new pool with a rank equals to the one of p + 1.

val init : unit -> pool

init () returns a fresh pool.

val register : pool -> variable -> unit

register p v adds v into the pool p without modifying the rank of v.

val introduce : pool -> variable -> unit

introduce p v registers v into p and updates its rank accordingly.

val instance : pool -> variable -> variable

instance p v returns a valid instance of v.

val chop : pool -> crterm -> variable

chop p t introduces t into p by registering a variable into p for each node of its tree maintaining its structure using links between these variables.

val chopi : IntRank.t -> crterm -> variable

chopi rank term chops a term. Any freshly created variables receive rank rank, but are not added to any pool.