[m-dev.] For review: documentation for solver types

[Ralph Becket]

Estimated hours taken: 4
Branches: main

doc/reference_manual.texi:
	Document the interface to the new solver types.

Index: reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.295
diff -u -r1.295 reference_manual.texi
--- reference_manual.texi	28 Jun 2004 04:49:53 -0000	1.295
+++ reference_manual.texi	22 Jul 2004 07:09:46 -0000
@@ -1549,6 +1549,7 @@
 * User-defined types::
 * Predicate and function type declarations::
 * Field access functions::
+* Solver types::
 @end menu
 
 @node Builtin types
@@ -2088,6 +2089,212 @@
                 Map ^ elem(Index) ^ field2 := Value.
 @end example
 
+ at node Solver types
+ at section Solver types
+
+ at menu
+* The any inst::
+* Abstract solver type declarations::
+* Solver type definitions::
+* Implementing solver types::
+* Solver type constraints and negated contexts::
+* Polymorphic solver types::
+ 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 samp{X} and @samp{Y} are variables belonging to a constrained integer
+solver type, we might place constraints upon them such that @samp{X > 3
++ Y} and @samp{Y =< 7}.  A later attempt to unify @samp{Y} with
+ at samp{10} will fail (it would violate the second constraint); similarly
+an attempt to unify @samp{X} with @samp{5} and @samp{Y} with @samp{4}
+would fail (it would violate the first constraint).
+
+ at node The any inst
+ at subsection The any inst
+
+A special inst, @samp{any}, is associated with solver types.  A variable
+of a solver type with inst @samp{any} means that that variable 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, @samp{X} is ground if for any values @samp{Y} and
+ at samp{Z} that unify with @samp{X}, it is the case that @samp{Y} and
+ at samp{Z} also unify with each other.  @samp{X} is non-ground if there
+are values @samp{Y} and @samp{Z} that unify with @samp{X}, but which do
+not unify with each other.
+
+For non-solver types, @samp{any} is equivalent to @samp{ground}.
+
+ at node Abstract solver type declarations
+ at subsection Abstract solver type declarations
+
+The type declarations
+
+ at example
+:- solver type t1.
+:- solver type t2(T1, T2).
+ at end example
+
+declare types @samp{t1/0} and @samp{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 subsection Solver type definitions
+
+A solver type definition takes the following form:
+
+ at example
+:- solver type solver_type
+        where   representation is representation_type,
+                initialisation is initialisation_pred,
+                ground         is ground_inst,
+                any            is any_inst,
+                equality       is equality_pred,
+                comparison     is comparison_pred.
+ at end example
+
+The first four attributes after the @samp{where} are mandatory, 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 @samp{representation_type} is the type used to implement the
+ at samp{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 samp{solver_type} values may be represented by
+ground at samp{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 @samp{solver_type}.
+ at end itemize
+
+The @samp{initialisation_pred} is the name of a predicate defined in the same
+module as the solver type, with the following signature:
+
+ at example
+:- pred initialisation_pred(solver_type::out(any)) is det.
+ at end example
+
+Calls to this predicate are inserted automatically by the compiler when
+a @samp{free} @samp{solver_type} variable has to be converted to @samp{any}
+(the initialisation predicate is responsible for registering the new,
+unbound variable with the corresponding constraint solver state).
+
+The @samp{ground_inst} is the inst associated with
+ at samp{representation_type} values denoting @samp{ground}
+ at samp{solver_type} values.
+
+The @samp{any_inst} is the inst associated with
+ at samp{representation_type} values denoting @samp{any} @samp{solver_type}
+values.
+
+The compiler constructs three impure functions for converting between
+ at samp{solver_type} values and @samp{representation_type} values
+(@samp{name} is the function symbol used to name @samp{solver_type} and
+ at samp{arity} is the number of type parameters it takes):
+
+ at example
+:- impure func 'representation of name/arity'(solver_type) =
+                        representation_type.
+:-        mode 'representation of name/arity'(in) =
+                        out(ground_inst) is det.
+:-        mode 'representation of 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.
+
+Two @samp{representation_type}-to- at samp{solver_type} functions are
+needed to avoid mode ambiguity in the case where @samp{any_inst} and
+ at samp{ground_inst} are equivalent.
+
+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 @samp{solver_type} is exported then it is a requirement that
+ at samp{representation_type}, @samp{initialisation_pred}, and, if
+specified, @samp{equality_pred} and @samp{comparison_pred} are also
+exported from the same module.
+
+ 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 @samp{any} solver type variables to @samp{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 type constraints and negated contexts
+ at subsection Solver type constraints and negated contexts
+
+It is (a currently unchecked) error to place a constraint on a solver
+type variable in a negated context.  The reason for this is that the
+compiler does not understand what constraints mean and therefore it
+cannot enforce their negation outside a negated context.
+
+For this reason, soundness of a program is not guaranteed if constraints
+are placed on solver type variables inside negations or the conditions of
+if-then-else goals.  Particular care is needed since unification is a primary
+form of constraint.
+
+ at node Polymorphic solver types
+ at subsection Polymorphic solver types
+
+Under the current design the compiler does not have enough information
+to initialise variables belonging to polymorphic parameters that are
+themselves expected to be solver types.  We intend to lift this
+restriction with an extension to the current design in the future.
+
 @node Modes
 @chapter Modes
 
@@ -2160,10 +2367,12 @@
 or the term @code{[A,A]} (the elements are not distinct variables).
 
 As a shorthand, the mode system provides @samp{free} and @samp{ground}
-as names for instantiatedness trees
-all of whose nodes are free and bound respectively.
-The shape of these trees is determined by
-the type of the variable to which they apply.
+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 @samp{bound} instantiatedness
 trees:
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------