Make.3-O
type 'a structure = 'a S.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,
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 inject : Signatures.id -> tyvar
inject
provides an injection of unique integer identifiers into decoded type variables.
structure s
turns s
, a structure whose children are decoded types, into a decoded type.