Make.1-S
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.