[m-rev.] for review: make solver types a separate chapter in reference manual
Julien Fischer
juliensf at csse.unimelb.edu.au
Wed Nov 3 23:32:14 AEDT 2010
Shift the description of solver types out of the reference manual chapter
``Types'' and into a separate ``Solver types'' chapter which occurs much
later in the manual.
This avoids cluttering up the ``Types'' chapter with details of what is
quite an advanced language feature and one that moreover also involves
aspects of the mode system.
There are no changes to any of the content.
doc/reference_manual.texi:
As above.
Julien.
Index: reference_manual.texi
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.450
diff -u -r1.450 reference_manual.texi
--- reference_manual.texi 14 Oct 2010 05:29:32 -0000 1.450
+++ reference_manual.texi 3 Nov 2010 12:18:46 -0000
@@ -104,6 +104,7 @@
* Foreign language interface:: Calling code written in other programming
languages from Mercury code
* Impurity:: Users can write impure Mercury code.
+* Solver types:: Support for constraint logic programming
* Trace goals:: Trace goals allow programmers to add debugging and
logging code to their programs.
* Pragmas:: Various compiler directives, used for example to
@@ -1769,7 +1770,6 @@
* User-defined types::
* Predicate and function type declarations::
* Field access functions::
-* Solver types::
@end menu
@node Builtin types
@@ -2309,433 +2309,156 @@
Map ^ elem(Index) ^ field2 := Value.
@end example
- at node Solver types
- at section Solver types
+ at node Modes
+ at chapter Modes
@menu
-* The any inst::
-* Abstract solver type declarations::
-* Solver type definitions::
-* Implementing solver types::
-* Solver types and negated contexts::
+* Insts modes and mode definitions::
+* Predicate and function mode declarations::
+* Constrained polymorphic modes::
+* Different clauses for different modes::
@end menu
-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
- at code{X} and @code{Y} are variables belonging to a constrained integer
-solver type, we might place constraints upon them such that @code{X > 3
-+ Y} and @code{Y =< 7}. A later attempt to unify @code{Y} with
- at code{10} will fail (it would violate the second constraint); similarly
-an attempt to unify @code{X} with @code{5} and @code{Y} with @code{4}
-would fail (it would violate the first constraint).
+ at node Insts modes and mode definitions
+ at section Insts, modes, and mode definitions
- at node The any inst
- at subsection The @samp{any} inst
+The @dfn{mode} of a predicate, or function, is a mapping
+from the initial state of instantiation of the arguments of the predicate,
+or the arguments and result of a function,
+to their final state of instantiation.
+To describe states of instantiation,
+we use information provided by the type system.
+Types can be viewed as regular trees with two kinds of nodes:
+or-nodes representing types
+and and-nodes representing constructors.
+The children of an or-node are the constructors
+that can be used to construct terms of that type;
+the children of an and-node are the types
+of the arguments of the constructors.
+We attach mode information to the or-nodes of type trees.
-Variables with solver types can have one of three possible insts: @code{free},
- at code{ground} or @code{any}.
-A variable with a solver type with inst @code{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.
+An @dfn{instantiatedness tree} is an assignment
+of an @dfn{instantiatedness} --- either @dfn{free} or @dfn{bound} ---
+to each or-node of a type tree,
+with the constraint that all descendants of a free node must be free.
-More formally, @code{X} is ground if for values @code{Y} and
- at code{Z} that unify with @code{X}, it is the case that @code{Y} and
- at code{Z} also unify with each other. @code{X} is non-ground if there
-are values @code{Y} and @code{Z} that unify with @code{X}, but which do
-not unify with each other.
+A term is @dfn{approximated by} an instantiatedness tree
+if for every node in the instantiatedness tree,
-A non-solver type value will have inst @code{any} if it is constructed using
-one or more inst @code{any} values.
+ at itemize @bullet
+ at item
+if the node is ``free'',
+then the corresponding node in the term (if any)
+is a free variable that does not share with any other variable
+(we call such variables @dfn{distinct});
-The built-in modes @code{ia} and @code{oa} are equivalent to @code{in(any)}
-and @code{out(any)} respectively.
+ at item
+if the node is ``bound'',
+then the corresponding node in the term (if any)
+is a function symbol.
- at node Abstract solver type declarations
- at subsection Abstract solver type declarations
+ at end itemize
-The type declarations
+When an instantiatedness tree tells us that a variable is bound,
+there may be several alternative function symbols to which it could be bound.
+The instantiatedness tree does not tell us which of these it is bound to;
+instead for each possible function symbol it tells us exactly
+which arguments of the function symbol will be free and which will be bound.
+The same principle applies recursively to these bound arguments.
+
+Mercury's mode system allows users
+to declare names for instantiatedness trees using declarations such as
@example
-:- solver type t1.
-:- solver type t2(T1, T2).
+:- inst listskel == bound( [] ; [free | listskel] ).
@end example
- at noindent
-declare types @code{t1/0} and @code{t2/2} to be abstract solver types.
-Abstract solver type declarations are identical to ordinary abstract
-type declarations except for the solver keyword.
+This instantiatedness tree describes lists
+whose skeleton is known but whose elements are distinct variables.
+As such, it approximates the term @code{[A,B]}
+but not the term @code{[H|T]} (only part of the skeleton is known),
+the term @code{[A,2]} (not all elements are variables),
+or the term @code{[A,A]} (the elements are not distinct variables).
- at node Solver type definitions
- at subsection Solver type definitions
+As a shorthand, the mode system provides @code{free} and @code{ground}
+as names for instantiatedness trees all of whose nodes are free and
+bound respectively (with the exception of solver type values which may
+be semantically ground, but be defined in terms of non-ground solver
+type values; see @ref{Solver types} for more detail). The shape of
+these trees is determined by the type of the variable to which they
+apply.
-A solver type definition takes the following form:
+A more concise, alternative syntax exists for @code{bound} instantiatedness
+trees:
@example
-:- 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.
+:- inst maybeskel ---> no ; yes(ground).
@end example
-The @samp{representation} attribute is mandatory
- at samp{ground_inst} and @samp{any_inst} default to @samp{ground},
- at samp{mutable_decls} is either a single mutable declaration
-(@pxref{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 @code{representation_type} is the type used to implement the
- at code{solver_type}. A two-tier scheme of this kind is necessary for a
-number of reasons, including
- at itemize @bullet
- at item
-a semantic gap is necessary to accommodate the fact that non-ground
- at code{solver_type} values may be represented by ground
- at code{representation_type} values (in the context of the corresponding
-constraint solver state);
- at item
-this approach greatly simplifies the definition of equality and
-comparison predicates for the @code{solver_type}.
- at end itemize
-
- at c XXX The following paragraph describes the old support for automatic
- at c initialisation of solver types. We no longer officially support
- at c automatic initialisation as part of the language but the compiler
- at c still contains the code necessary to implement it.
- at c
- at c The @code{initialisation_pred} is the name of a predicate defined in the
- at c same module as the solver type, with the following signature:
- at c
- at c @example
- at c :- pred initialisation_pred(solver_type::out(any)) is det.
- at c @end example
- at c
- at c Calls to this predicate are inserted automatically by the compiler when a
- at c @code{free} @code{solver_type} variable has to be given inst @code{any}.
- at c (The initialisation predicate is responsible for registering the new,
- at c unbound variable with the corresponding constraint solver state.)
-
-The @code{ground_inst} is the inst associated with
- at code{representation_type} values denoting @code{ground}
- at code{solver_type} values.
+ at noindent
+which is equivalent to writing
-The @code{any_inst} is the inst associated with
- at code{representation_type} values denoting @code{any} @code{solver_type}
-values.
+ at example
+:- inst maybeskel == bound(no ; yes(ground)).
+ at end example
-The compiler constructs four impure functions for converting between
- at code{solver_type} values and @code{representation_type} values
-(@samp{name} is the function symbol used to name @code{solver_type} and
- at samp{arity} is the number of type parameters it takes):
+As execution proceeds, variables may become more instantiated.
+A @dfn{mode mapping} is a mapping
+from an initial instantiatedness tree to a final instantiatedness tree,
+with the constraint that no node of the type tree
+is transformed from bound to free.
+Mercury allows the user to specify mode mappings directly
+by expressions such as @code{inst1 >> inst2},
+or to give them a name using declarations such as
@example
-:- 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.
+:- mode m == inst1 >> inst2.
+ at end example
-:- impure func 'representation to ground name/arity'(representation_type) =
- solver_type.
-:- mode 'representation to ground name/arity'(in(ground_inst)) =
- out is det.
+Two standard shorthand modes are provided,
+corresponding to the standard notions of inputs and outputs:
-:- impure func 'representation to any name/arity'(representation_type) =
- solver_type.
-:- mode 'representation to any name/arity'(in(any_inst)) =
- out(any) is det.
+ at example
+:- mode in == ground >> ground.
+:- mode out == free >> ground.
@end example
-These functions are impure because of the semantic gap issue mentioned
-above.
+Prolog fans who want to use the symbols @samp{+} and @samp{-}
+can do so by simply defining them using a mode declaration:
-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.
+ at example
+:- mode (+) == in.
+:- mode (-) == out.
+ at end example
-If @code{solver_type} is exported then it is a requirement that
- at code{representation_type}, @code{initialisation_pred}, and, if
-specified, @code{equality_pred} and @code{comparison_pred} are also
-exported from the same module.
+These two modes are enough for most functions and predicates.
+Nevertheless, Mercury's mode system is sufficiently
+expressive to handle more complex data-flow patterns,
+including those involving partially instantiated data structures.
+(The current implementation does not handle
+partially instantiated data structures yet.)
-If @code{equality_pred} is not specified then the compiler will
-generate an equality predicate that throws an exception of type
- at samp{exception.software_error/0} when called.
+For example, consider an
+interface to a database that associates data with keys, and provides
+read and write access to the items it stores. To represent accesses to
+the database over a network, you would need declarations such as
-Likewise, if @code{comparison_pred} is not specified then the compiler
-will generate a comparison predicate that throws an exception of
-type @samp{exception.software_error/0} when called.
+ at example
+:- type operation
+ ---> lookup(key, data)
+ ; set(key, data).
+:- inst request
+ ---> lookup(ground, free)
+ ; set(ground, ground).
+:- mode create_request == free >> request.
+:- mode satisfy_request == request >> ground.
+ at end example
-If provided, any mutable declarations given for the @code{constraint_store}
-attribute are equivalent to separate mutable declarations; their association
-with the solver type is for the purposes of documentation. That is,
+ at samp{inst} and @samp{mode} declarations can be parametric.
+For example, the following declaration
@example
-:- solver type t
- where ... constraint_store is [ mutable(a, int, 42, ground, []),
- mutable(b, string, "Hi", ground, [])
- ],
- ...
- at end example
-
- at noindent
-is equivalent to
-
- at example
-:- solver type t
- where ...
-:- mutable(a, int, 42, ground, []).
-:- mutable(b, string, "Hi", ground, []).
- at end example
-
- at node Implementing solver types
- at subsection Implementing solver types
-
-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 @ref{Trailing}) so that changes can be undone on
-backtracking.
-
-The solver type implementation should provide functions and predicates
-to
- at itemize @bullet
- at item
-construct and deconstruct solver type values,
- at item
-to place constraints on solver type variables,
- at item
-to convert @code{any} solver type variables to @code{ground} if possible
-(this is obviously an impure operation --- see @ref{Impurity}),
- at item
-to convert solver type values to non-solver type values (again, this is
-impure and requires the argument solver type values be
-sufficiently ground),
- at item
-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).
- at end itemize
-
- at node Solver types and negated contexts
- at subsection Solver types and negated contexts
-
-Mercury's negation and if-then-else goals
-(and hence also inequalities and universal quantifications)
-are implemented using @emph{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 @code{any} is used in a negated context,
-the goal must be placed inside a @code{promise_pure}, @code{promise_semipure},
-or @code{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 doesn't 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 @code{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
- at code{any}, which allows non-local variables used in the body of the
-expression to have inst @code{any}.
-Calling or applying these values @emph{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 @code{any} are written using
- at code{any_pred} and @code{any_func} in place of @code{pred} and @code{func},
-respectively.
-
-The third possibility is that the higher order value can be given an
-impure type (@pxref{Higher-order impurity}).
-
- at node Modes
- at chapter Modes
-
- at menu
-* Insts modes and mode definitions::
-* Predicate and function mode declarations::
-* Constrained polymorphic modes::
-* Different clauses for different modes::
- at end menu
-
- at node Insts modes and mode definitions
- at section Insts, modes, and mode definitions
-
-The @dfn{mode} of a predicate, or function, is a mapping
-from the initial state of instantiation of the arguments of the predicate,
-or the arguments and result of a function,
-to their final state of instantiation.
-To describe states of instantiation,
-we use information provided by the type system.
-Types can be viewed as regular trees with two kinds of nodes:
-or-nodes representing types
-and and-nodes representing constructors.
-The children of an or-node are the constructors
-that can be used to construct terms of that type;
-the children of an and-node are the types
-of the arguments of the constructors.
-We attach mode information to the or-nodes of type trees.
-
-An @dfn{instantiatedness tree} is an assignment
-of an @dfn{instantiatedness} --- either @dfn{free} or @dfn{bound} ---
-to each or-node of a type tree,
-with the constraint that all descendants of a free node must be free.
-
-A term is @dfn{approximated by} an instantiatedness tree
-if for every node in the instantiatedness tree,
-
- at itemize @bullet
- at item
-if the node is ``free'',
-then the corresponding node in the term (if any)
-is a free variable that does not share with any other variable
-(we call such variables @dfn{distinct});
-
- at item
-if the node is ``bound'',
-then the corresponding node in the term (if any)
-is a function symbol.
-
- at end itemize
-
-When an instantiatedness tree tells us that a variable is bound,
-there may be several alternative function symbols to which it could be bound.
-The instantiatedness tree does not tell us which of these it is bound to;
-instead for each possible function symbol it tells us exactly
-which arguments of the function symbol will be free and which will be bound.
-The same principle applies recursively to these bound arguments.
-
-Mercury's mode system allows users
-to declare names for instantiatedness trees using declarations such as
-
- at example
-:- inst listskel == bound( [] ; [free | listskel] ).
- at end example
-
-This instantiatedness tree describes lists
-whose skeleton is known but whose elements are distinct variables.
-As such, it approximates the term @code{[A,B]}
-but not the term @code{[H|T]} (only part of the skeleton is known),
-the term @code{[A,2]} (not all elements are variables),
-or the term @code{[A,A]} (the elements are not distinct variables).
-
-As a shorthand, the mode system provides @code{free} and @code{ground}
-as names for instantiatedness trees all of whose nodes are free and
-bound respectively (with the exception of solver type values which may
-be semantically ground, but be defined in terms of non-ground solver
-type values; see @ref{Solver types} for more detail). The shape of
-these trees is determined by the type of the variable to which they
-apply.
-
-A more concise, alternative syntax exists for @code{bound} instantiatedness
-trees:
-
- at example
-:- inst maybeskel ---> no ; yes(ground).
- at end example
-
- at noindent
-which is equivalent to writing
-
- at example
-:- inst maybeskel == bound(no ; yes(ground)).
- at end example
-
-As execution proceeds, variables may become more instantiated.
-A @dfn{mode mapping} is a mapping
-from an initial instantiatedness tree to a final instantiatedness tree,
-with the constraint that no node of the type tree
-is transformed from bound to free.
-Mercury allows the user to specify mode mappings directly
-by expressions such as @code{inst1 >> inst2},
-or to give them a name using declarations such as
-
- at example
-:- mode m == inst1 >> inst2.
- at end example
-
-Two standard shorthand modes are provided,
-corresponding to the standard notions of inputs and outputs:
-
- at example
-:- mode in == ground >> ground.
-:- mode out == free >> ground.
- at end example
-
-Prolog fans who want to use the symbols @samp{+} and @samp{-}
-can do so by simply defining them using a mode declaration:
-
- at example
-:- mode (+) == in.
-:- mode (-) == out.
- at end example
-
-These two modes are enough for most functions and predicates.
-Nevertheless, Mercury's mode system is sufficiently
-expressive to handle more complex data-flow patterns,
-including those involving partially instantiated data structures.
-(The current implementation does not handle
-partially instantiated data structures yet.)
-
-For example, consider an
-interface to a database that associates data with keys, and provides
-read and write access to the items it stores. To represent accesses to
-the database over a network, you would need declarations such as
-
- at example
-:- type operation
- ---> lookup(key, data)
- ; set(key, data).
-:- inst request
- ---> lookup(ground, free)
- ; set(ground, ground).
-:- mode create_request == free >> request.
-:- mode satisfy_request == request >> ground.
- at end example
-
- at samp{inst} and @samp{mode} declarations can be parametric.
-For example, the following declaration
-
- at example
-:- inst maybeskel(Inst) ---> no ; yes(Inst).
+:- inst maybeskel(Inst) ---> no ; yes(Inst).
@end example
@noindent
@@ -9212,6 +8935,284 @@
impure Ys = map(ImpureFunc, Ys).
@end example
+ at node Solver types
+ at chapter Solver types
+
+ at menu
+* The any inst::
+* Abstract solver type declarations::
+* Solver type definitions::
+* Implementing solver types::
+* Solver types and negated contexts::
+ at end menu
+
+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
+ at code{X} and @code{Y} are variables belonging to a constrained integer
+solver type, we might place constraints upon them such that @code{X > 3
++ Y} and @code{Y =< 7}. A later attempt to unify @code{Y} with
+ at code{10} will fail (it would violate the second constraint); similarly
+an attempt to unify @code{X} with @code{5} and @code{Y} with @code{4}
+would fail (it would violate the first constraint).
+
+ at node The any inst
+ at section The @samp{any} inst
+
+Variables with solver types can have one of three possible insts: @code{free},
+ at code{ground} or @code{any}.
+A variable with a solver type with inst @code{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, @code{X} is ground if for values @code{Y} and
+ at code{Z} that unify with @code{X}, it is the case that @code{Y} and
+ at code{Z} also unify with each other. @code{X} is non-ground if there
+are values @code{Y} and @code{Z} that unify with @code{X}, but which do
+not unify with each other.
+
+A non-solver type value will have inst @code{any} if it is constructed using
+one or more inst @code{any} values.
+
+The built-in modes @code{ia} and @code{oa} are equivalent to @code{in(any)}
+and @code{out(any)} respectively.
+
+ at node Abstract solver type declarations
+ at section Abstract solver type declarations
+
+The type declarations
+
+ at example
+:- solver type t1.
+:- solver type t2(T1, T2).
+ at end example
+
+ at noindent
+declare types @code{t1/0} and @code{t2/2} to be abstract solver types.
+Abstract solver type declarations are identical to ordinary abstract
+type declarations except for the solver keyword.
+
+ at node Solver type definitions
+ at section Solver type definitions
+
+A solver type definition takes the following form:
+
+ at example
+:- 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.
+ at end example
+
+The @samp{representation} attribute is mandatory
+ at samp{ground_inst} and @samp{any_inst} default to @samp{ground},
+ at samp{mutable_decls} is either a single mutable declaration
+(@pxref{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 @code{representation_type} is the type used to implement the
+ at code{solver_type}. A two-tier scheme of this kind is necessary for a
+number of reasons, including
+ at itemize @bullet
+ at item
+a semantic gap is necessary to accommodate the fact that non-ground
+ at code{solver_type} values may be represented by ground
+ at code{representation_type} values (in the context of the corresponding
+constraint solver state);
+ at item
+this approach greatly simplifies the definition of equality and
+comparison predicates for the @code{solver_type}.
+ at end itemize
+
+ at c XXX The following paragraph describes the old support for automatic
+ at c initialisation of solver types. We no longer officially support
+ at c automatic initialisation as part of the language but the compiler
+ at c still contains the code necessary to implement it.
+ at c
+ at c The @code{initialisation_pred} is the name of a predicate defined in the
+ at c same module as the solver type, with the following signature:
+ at c
+ at c @example
+ at c :- pred initialisation_pred(solver_type::out(any)) is det.
+ at c @end example
+ at c
+ at c Calls to this predicate are inserted automatically by the compiler when a
+ at c @code{free} @code{solver_type} variable has to be given inst @code{any}.
+ at c (The initialisation predicate is responsible for registering the new,
+ at c unbound variable with the corresponding constraint solver state.)
+
+The @code{ground_inst} is the inst associated with
+ at code{representation_type} values denoting @code{ground}
+ at code{solver_type} values.
+
+The @code{any_inst} is the inst associated with
+ at code{representation_type} values denoting @code{any} @code{solver_type}
+values.
+
+The compiler constructs four impure functions for converting between
+ at code{solver_type} values and @code{representation_type} values
+(@samp{name} is the function symbol used to name @code{solver_type} and
+ at samp{arity} is the number of type parameters it takes):
+
+ at example
+:- 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.
+ at end example
+
+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 @code{solver_type} is exported then it is a requirement that
+ at code{representation_type}, @code{initialisation_pred}, and, if
+specified, @code{equality_pred} and @code{comparison_pred} are also
+exported from the same module.
+
+If @code{equality_pred} is not specified then the compiler will
+generate an equality predicate that throws an exception of type
+ at samp{exception.software_error/0} when called.
+
+Likewise, if @code{comparison_pred} is not specified then the compiler
+will generate a comparison predicate that throws an exception of
+type @samp{exception.software_error/0} when called.
+
+If provided, any mutable declarations given for the @code{constraint_store}
+attribute are equivalent to separate mutable declarations; their association
+with the solver type is for the purposes of documentation. That is,
+
+ at example
+:- solver type t
+ where ... constraint_store is [ mutable(a, int, 42, ground, []),
+ mutable(b, string, "Hi", ground, [])
+ ],
+ ...
+ at end example
+
+ at noindent
+is equivalent to
+
+ at example
+:- solver type t
+ where ...
+:- mutable(a, int, 42, ground, []).
+:- mutable(b, string, "Hi", ground, []).
+ at end example
+
+ at node Implementing solver types
+ at section Implementing solver types
+
+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 @ref{Trailing}) so that changes can be undone on
+backtracking.
+
+The solver type implementation should provide functions and predicates
+to
+ at itemize @bullet
+ at item
+construct and deconstruct solver type values,
+ at item
+to place constraints on solver type variables,
+ at item
+to convert @code{any} solver type variables to @code{ground} if possible
+(this is obviously an impure operation --- see @ref{Impurity}),
+ at item
+to convert solver type values to non-solver type values (again, this is
+impure and requires the argument solver type values be
+sufficiently ground),
+ at item
+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).
+ at end itemize
+
+ at node Solver types and negated contexts
+ at section Solver types and negated contexts
+
+Mercury's negation and if-then-else goals
+(and hence also inequalities and universal quantifications)
+are implemented using @emph{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 @code{any} is used in a negated context,
+the goal must be placed inside a @code{promise_pure}, @code{promise_semipure},
+or @code{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 doesn't 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 @code{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
+ at code{any}, which allows non-local variables used in the body of the
+expression to have inst @code{any}.
+Calling or applying these values @emph{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 @code{any} are written using
+ at code{any_pred} and @code{any_func} in place of @code{pred} and @code{func},
+respectively.
+
+The third possibility is that the higher order value can be given an
+impure type (@pxref{Higher-order impurity}).
+
+
@node Trace goals
@chapter Trace goals
--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to: mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions: mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------
More information about the reviews
mailing list