Module Make.Data

This submodule defines the data attached with a unification variable.

type 'a structure

A structure is a piece of information that the unifier attaches to a variable (or, more accurately, to an equivalence class of variables).

In some contexts, a structure represents a logical constraint that bears on a variable. A structure of type 'a structure may itself contain variables, which are represented as values of type 'a. We refer to these values as the children of this structure.

In some contexts, a structure may record not only a logical constraint, but also other kinds of meta-information, such as the unique identifier of this equivalence class, where and how it is bound (its rank; whether it is rigid or flexible; etc.).

For example, in the case of first-order unification, a structure might be an optional shallow term: that is,

  • either None, which indicates the absence of a constraint;
  • or Some term, where term is a shallow term (a term of depth 1 whose leaves are variables of type 'a), which indicates the presence of an equality constraint.
val iter : ( 'a -> unit ) -> 'a structure -> unit

iter applies an action to every child of a structure.

val id : 'a structure -> Signatures.id

id extracts the unique identifier of a structure.

val map : ( 'a -> 'b ) -> 'a structure -> 'b structure

map applies a transformation to the children of a structure, while preserving the shape of the structure.

val is_leaf : 'a structure -> bool

is_leaf s determines whether the structure s is a leaf, that is, whether it represents the absence of a logical constraint. This function is typically used by a decoder to determine which equivalence classes should be translated to "type variables" in a decoded type.

val project : 'a structure -> 'a S.structure

The type 'a structure is richer (carries more information) than the type 'a S.structure. The function project witnesses this fact. It drops the extra information and extracts the underlying user-defined structure.