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.

These functions are constructed in-line as part of a source-to-source transformation, hence it is an error to define a solver type in the interface section of a module.

If `solver_type` is exported then it is a requirement that
`representation_type`, and, if specified, `equality_pred` and
`comparison_pred` are also exported from the same module.

If `equality_pred` is not specified then the compiler will
generate an equality predicate that throws an exception of type
‘`exception.software_error/0`’ when called.

Likewise, if `comparison_pred` is not 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, []).