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

`InconsistentConjunction`

is raised by `conjunction`

.

`conjunction equate s1 s2`

computes the logical conjunction `s`

of the structures `s1`

and `s2`

. If these structures are logically inconsistent with one another (that is, if their conjunction implies a logical contradiction), then the exception `InconsistentConjunction`

is raised.

`conjunction`

invokes `equate`

to emit auxiliary equality constraints that are necessary and sufficient for `s`

to actually represent the conjunction of `s1`

and `s2`

.

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

- the conjunction of
`None`

and`s`

would be`s`

; - the conjunction of
`s`

and`None`

would be`s`

; - the conjunction of
`Some term1`

and`Some term2`

, where the shallow terms`term1`

and`term2`

have the same head constructor, would be`Some term1`

or`Some term2`

(it does not matter which!), and`equate`

would be invoked to equate the leaves of`term1`

and`term2`

; - the conjunction of
`Some term1`

and`Some term2`

, where the shallow terms`term1`

and`term2`

have distinct head constructors, would raise`InconsistentConjunction`

.

`val iter : ( 'a -> unit ) -> 'a structure -> unit`

`iter`

applies an action to every child of a structure.

`val fold : ( 'a -> 'b -> 'b ) -> 'a structure -> 'b -> 'b`

`fold`

applies an action to every child of a structure, and carries an accumulator.

`val pprint : ( 'a -> PPrint.document ) -> 'a structure -> PPrint.document`

`pprint`

is a structure printer, parameterized over a child printer. It is used for debugging purposes only.