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. 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

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, 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]