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.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:
None
and s
would be s
;s
and None
would be s
;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
;Some term1
and Some term2
, where the shallow terms term1
and term2
have distinct head constructors, would raise InconsistentConjunction
.