|• The any inst:|
|• Abstract solver type declarations:|
|• Solver type definitions:|
|• Implementing solver types:|
|• Solver types and negated contexts:|
Solver types are an experimental addition to the language supporting the
implementation of constraint solvers.
A program may place constraints on and between variables of a solver type,
limiting the values those variables may take on before they are actually bound.
For example, if
Y are variables belonging to a constrained
integer solver type, we might place constraints upon them such that
X > 3 + Y and
Y =< 7.
A later attempt to unify
10 will fail (it would violate
the second constraint); similarly an attempt to unify
4 would fail (it would violate the first constraint).