#### inferno

Library

Module

Module type

Parameter

Class

Class type

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.

`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.