Make.Data
This submodule defines the data attached with a unification variable.
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,
None
, which indicates the absence of a constraint;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.
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.