Next: Trace goals, Previous: Impurity, Up: Top [Contents]

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

and `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 `Y`

with `10`

will fail
(it would violate the second constraint);
similarly an attempt to unify `X`

with `5`

and `Y`

with `4`

would fail (it would violate the first constraint).

Variables with solver types can have one of three possible insts:
`free`

, `ground`

or `any`

.
A variable with a solver type with inst `any`

may not (yet) be semantically ground, in the following sense:
if a variable is semantically ground,
then the set of values it unifies with form an equivalence class;
if a variable is non-ground,
then the set of values it unifies with do not form an equivalence class.

More formally, `X`

is ground
if for values `Y`

and `Z`

that unify with `X`

,
it is the case that `Y`

and `Z`

also unify with each other.
`X`

is non-ground
if there are values `Y`

and `Z`

that unify with `X`

,
but which do not unify with each other.

A non-solver type value will have inst `any`

if it is constructed using one or more inst `any`

values.

The builtin modes `ia`

and `oa`

are equivalent to `in(any)`

and `out(any)`

respectively.

The type declarations

:- solver type t1. :- solver type t2(T1, T2).

declare types `t1/0`

and `t2/2`

to be abstract solver types.
Abstract solver type declarations are
identical to ordinary abstract type declarations
except for the `solver`

keyword.

A solver type definition takes the following form:

:- solver typesolver_typewhere representation isrepresentation_type, ground isground_inst, any isany_inst, constraint_store ismutable_decls, equality isequality_pred, comparison iscomparison_pred.

The `representation`

attribute is mandatory.
The `ground_inst` and `any_inst` attributes are optional
and default to `ground`

.
The `constraint_store`

attribute is mandatory:
`mutable_decls` must be either a single mutable declaration
(see Module-local mutable variables),
or a comma separated list of mutable declarations in brackets.
The `equality`

and `comparison`

attributes are optional,
although a solver type without equality would not be very useful.
The attributes that are not omitted must appear in the order shown above.

The `representation_type`
is the type used to implement the `solver_type`.
A two-tier scheme of this kind is necessary for a number of reasons,
including

- a semantic gap is necessary to accommodate the fact that
non-ground
`solver_type`values may be represented by ground`representation_type`values (in the context of the corresponding constraint solver state); - this approach greatly simplifies
the definition of equality and comparison predicates for the
`solver_type`.

The `ground_inst` is the inst associated with
`representation_type` values denoting `ground`

`solver_type` values.

The `any_inst` is the inst associated with `representation_type` values
denoting `any`

`solver_type`

values.

The compiler constructs four impure functions
for converting between `solver_type` values
and `representation_type` values
(`name` is the function symbol used to name `solver_type`
and `arity` is the number of type parameters it takes):

:- impure func 'representation of groundname/arity'(solver_type) =representation_type. :- mode 'representation of groundname/arity'(in) = out(ground_inst) is det. :- impure func 'representation of anyname/arity'(solver_type) =representation_type. :- mode 'representation of anyname/arity'(in(any)) = out(any_inst) is det. :- impure func 'representation to groundname/arity'(representation_type) =solver_type. :- mode 'representation to groundname/arity'(in(ground_inst)) = out is det. :- impure func 'representation to anyname/arity'(representation_type) =solver_type. :- mode 'representation to anyname/arity'(in(any_inst)) = out(any) is det.

These functions are impure because of the semantic gap issue mentioned above.

Solver types may be exported from their defining module, but only in an abstract form. This requires the full definition to appear in the implementation section of the module, and an abstract declaration like the following in its interface:

:- solver typesolver_type.

If a solver type is exported, then its representation type, and, if specified, its equality and/or comparison predicates must also exported from the same module.

If a solver type has no equality predicate specified,
then the compiler will generate an equality predicate
that throws an exception of type ‘`exception.software_error/0`’ when called.

Likewise, if a solver type has no equality comparison specified,
then the compiler will generate a comparison predicate
that throws an exception of type ‘`exception.software_error/0`’ when called.

If provided,
any mutable declarations given for the `constraint_store`

attribute
are equivalent to separate mutable declarations;
their association with the solver type is for the purposes of documentation.
That is,

:- solver type t where …, constraint_store is [ mutable(a, int, 42, ground, []), mutable(b, string, "Hi", ground, []) ], …

is equivalent to

:- solver type t where … :- mutable(a, int, 42, ground, []). :- mutable(b, string, "Hi", ground, []).

A solver type is an abstraction, implemented using a combination of a private representation type and a constraint store.

The constraint store is an (impure) piece of state used to keep track of the extant constraints on variables of the solver type. This will typically be implemented using foreign code.

It is important that changes to the constraint store are properly trailed (see Trailing) so that changes can be undone on backtracking.

The solver type implementation should provide functions and predicates

- to construct and deconstruct solver type values,
- to place constraints on solver type variables,
- to convert
`any`

solver type variables to`ground`

if possible (this is obviously an impure operation — see Impurity), - to convert solver type values to non-solver type values (again, this is impure and requires the argument solver type values be sufficiently ground),
- to ask questions about the extant constraints on solver type variables without constraining them further (this too is impure because the set of constraints on a variable may change during execution of the program).

Mercury’s negation and if-then-else goals
(and hence also inequalities and universal quantifications)
are implemented using *negation as failure*,
meaning that the failure to find a proof of one statement
is regarded as a proof of its negation.
Negation as failure is sound
provided that no non-local variable becomes further bound
during the execution of a goal which may be negated.
This includes negated goals themselves,
as well as the conditions of if-then-elses,
which are negated iff they fail without producing any solution,
and the bodies of pred or func expressions,
which may be called or applied in one of the other contexts,
or indeed in another pred or func expression.

Mercury checks that any solver variables that are used in the above contexts
are used in such a way that negation as failure remains sound.
In the case of negation and if-then-else goals,
if any non-local solver type variable or higher-order variable
with inst `any`

is used in a negated context,
the goal must be placed inside
a `promise_pure`

, `promise_semipure`

, or `promise_impure`

scope.
The first two promises assert that (among other things)
no solver variable becomes further bound in the negated context.
The third promise makes the weaker assertion that the goal satisfies
the requirements of all impure goals
(namely, that it does not interfere with the semantics of other pure goals).

In the case of pred and func expressions, Mercury allows three possibilities.
The higher-order value may be considered `ground`

,
which means that all non-local variables used in the body of the expression
(including those with other higher-order values) must themselves be ground.
Higher-order values that are ground
can be safely called or applied in any context, including negated contexts,
since none of their (ground) non-local variables
can become further bound by doing so.
Alternatively, the higher-order value
may be considered to have inst `any`

,
which allows non-local variables used in the body of the expression
to have inst `any`

.
Calling or applying these values
*may* further bind non-local variables,
so if this occurs in a negated context
then, as in the case of solver variables,
a promise will be required around the negation or if-then-else.

Pred and func expressions with inst `any`

are written using `any_pred`

and `any_func`

in place of `pred`

and `func`

, respectively.

The third possibility is that the higher-order value can be given an impure type (see Higher-order impurity).

Previous: Implementing solver types, Up: Solver types [Contents]