Next: , Previous: , Up: Solver types   [Contents]


16.3 Solver type definitions

A solver type definition takes the following form:

:- solver type solver_type
        where   representation   is representation_type,
                ground           is ground_inst,
                any              is any_inst,
                constraint_store is mutable_decls,
                equality         is equality_pred,
                comparison       is comparison_pred.

The ‘representation’ attribute is mandatory ‘ground_inst’ and ‘any_inst’ default to ‘ground’, ‘mutable_decls’ is 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), and attributes must appear in the order shown.

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

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 ground name/arity'(solver_type) =
                        representation_type.
:-        mode 'representation of ground name/arity'(in) =
                        out(ground_inst) is det.

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

:- impure func 'representation to ground name/arity'(representation_type) =
                        solver_type.
:-        mode 'representation to ground name/arity'(in(ground_inst)) =
                        out is det.

:- impure func 'representation to any name/arity'(representation_type) =
                        solver_type.
:-        mode 'representation to any name/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, initialisation_pred, 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, []).

Next: , Previous: , Up: Solver types   [Contents]