inferno 20220603 · OCaml Package

This functor transforms a type 'a structure, equipped with map, iter and conjunction operations, into the type 'a structure option, equipped with the same operations. The type 'a structure option is typically useful when implementing some form of unification of terms: indeed, the optional structure None indicates the absence of a constraint, while the optional structure Some term indicates the presence of an equality constraint.

Parameters

module S : sig ... end

Signature

type 'a structure = 'a S.structure option

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.

exception InconsistentConjunction

InconsistentConjunction is raised by conjunction.

val conjunction : 
  ('a -> 'a -> unit) ->
  'a structure ->
  'a structure ->
  'a structure

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 map : ('a -> 'b) -> 'a structure -> 'b structure

map applies a transformation to the children of a structure, while preserving the shape of the structure.

val leaf : 'a structure

The constant leaf is a structure that represents the absence of a logical constraint. It is typically used when a variable is created fresh.

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_nonleaf : 'a structure -> 'a S.structure

project_nonleaf (Some s) is s, while project_nonleaf None is undefined. In other words, if os is a non-leaf optional structure, then project_nonleaf os is the underlying structure.

package inferno

Parameters

Signature