Next: Implementing solver types, Previous: Abstract solver type declarations, Up: Solver types [Contents]

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, []).