[m-rev.] For review: change the way we handle inst any non-locals in negated contexts (again)

[Mark Brown]

On 14-Dec-2005, Mark Brown <mark at cs.mu.OZ.AU> wrote:
> After an extended discussion in the office, our plan is for Ralph to commit
> his change after addressing Julien's comments, then I will start work on
> overhauling the purity system.  Changes to the reference manual will be
> posted for review first, so discussion of the new purity system will continue
> then.

Here they are.

The reference manual is meant to be self-explanatory so I will omit
any preliminary remarks at this stage, except to note that one section
(marked with an XXX) is not complete, and that some of the cross-referencing
is not ideal and will be improved later.

Enjoy!

Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.342
diff -u -r1.342 reference_manual.texi
--- doc/reference_manual.texi	14 Dec 2005 05:14:15 -0000	1.342
+++ doc/reference_manual.texi	15 Dec 2005 05:01:53 -0000
@@ -484,12 +484,9 @@
 promise_exclusive               fy                950
 promise_exclusive_exhaustive    fy                950
 promise_exhaustive              fy                950
-promise_impure                  fx                950
-promise_impure_implicit         fx                950
 promise_pure                    fx                950
-promise_pure_implicit           fx                950
 promise_semipure                fx                950
-promise_semipure_implicit       fx                950
+infer_purity                    fx                950
 some                            fxy               950
 ,                               xfy               1000
 &                               xfy               1025
@@ -647,35 +644,17 @@
 @var{Goal} must be a valid goal.
 This is an abbreviation for @samp{not (some @var{Vars} not @var{Goal})}.
 
- at item @code{promise_pure @var{Goal}}
-A purity cast.
+ at item @code{@var{Purity} @var{Goal}}
+A purity-annotated goal.
+ at var{Purity} must be a valid purity annotation.
 @var{Goal} must be a valid goal.
-This goal promises that @var{Goal} implements a pure interface,
-even though it may include impure and semipure components.
+See @ref{Impurity} for the possible purity annotations and their meanings.
 
- at item @code{promise_semipure @var{Goal}}
-A purity cast.
- at var{Goal} must be a valid goal.
-This goal promises that @var{Goal} implements a semipure interface,
-even though it may include impure components.
-
- at item @code{promise_impure @var{Goal}}
-A purity cast.
- at var{Goal} must be a valid goal.
-This goal instructs the compiler to treat @var{Goal} as though it were impure,
-regardless of its actual purity.
-
- at item @code{promise_pure_implicit @var{Goal}}
-Equivalent to @code{promise_pure @var{Goal}}, except that purity annotations on
-semipure and impure subgoals in @var{Goal} are optional.
-
- at item @code{promise_semipure_implicit @var{Goal}}
-Equivalent to @code{promise_semipure @var{Goal}}, except that purity
-annotations on semipure and impure subgoals in @var{Goal} are optional.
-
- at item @code{promise_impure_implicit @var{Goal}}
-Equivalent to @code{promise_impure @var{Goal}}, except that purity annotations
-on semipure and impure subgoals in @var{Goal} are optional.
+ at item @code{infer_purity @var{Goal}}
+Introduces a scope within which the purity of all goals is inferred
+by the compiler.  @var{Goal} must be a valid goal,
+with the exception that all purity annotations (@pxref{Impurity})
+that would otherwise be required on subgoals are optional.
 
 @item @code{promise_equivalent_solutions @var{Vars} @var{Goal}}
 A determinism cast.
@@ -1426,6 +1405,9 @@
 whose value is the predicate or function of the specified arguments
 determined by the specified goal.  @xref{Higher-order}.
 
+Lambda expressions may also contain purity annotations.
+ at xref{Purity annotations on lambda expressions}.
+
 A lambda expression introduces a new scope: any variables occurring in
 the arguments Arg1, Arg2, @dots{} are locally quantified, i.e.@: 
 any occurrences of variables with that name in the lambda
@@ -1476,6 +1458,10 @@
 It denotes the result of applying the specified function to the
 specified arguments.  @xref{Higher-order}.
 
+If the higher-order function is impure then the application takes a
+slightly different form.
+ at xref{Purity annotations on higher-order calls}.
+
 @node Explicit type qualification
 @subsection Explicit type qualification
 
@@ -1636,6 +1622,9 @@
 @itemx @code{func(T1, T2) = T}, @dots{}
 These higher-order function and predicate types are used to pass procedure
 addresses and closures to other predicates.  @xref{Higher-order}.
+The purity of a higher-order value is considered part of the type,
+so higher-order function and predicate types may require a purity annotation.
+ at xref{Impurity}.
 
 @item Tuple types: @code{@{@}}, @code{@{T@}}, @code{@{T1, T2@}}, @dots{}. 
 A tuple type is equivalent to a discriminated union type
@@ -1876,6 +1865,12 @@
 :- pred f(int, T, U) = U.
 @end example
 
+Predicate and function declarations may also include a purity annotation.
+If @code{`with_type`} is used then the actual purity is determined by the
+annotation on the declaration, however this annotation must be consistent
+with that of the given higher-order type.
+ at xref{Impurity}.
+
 Type variables in predicate and function declarations
 are implicitly universally quantified by default;
 that is, the predicate or function may be called with arguments
@@ -2378,13 +2373,20 @@
 @node Solver types and negated contexts
 @subsection Solver types and negated contexts
 
-Referential transparency can be violated if a non-local solver type variable
-with inst @code{any} is used in a negated context (i.e., the body of a negated
-goal or the condition of an if-then-else) or in a lambda expression.  Programs
-are therefore required to place such goals inside a @code{promise_pure},
- at code{promise_semipure}, or @code{promise_impure} scope, and to declare such
-lambda expressions to be @code{impure}, even if they would normally be
-considered pure.
+Negation is implemented using ``negation-as-failure'', which is unsound
+if non-local variables can become bound inside a negation.
+It is not generally possible to determine whether a non-local variable
+with inst @code{any} will become bound at a point where it is used,
+which means that a negation containing such a variable,
+or an if-then-else whose condition contains such a variable,
+cannot be proven to be safe.
+Such goals are therefore inferred to be impure.
+
+Similarly, referential transparency can be violated if a non-local variable
+with inst @code{any} is used in a lambda expression.  Programs are therefore
+required to declare such lambda expressions to be @code{impure}.
+
+ at xref{Impurity}.
 
 @node Polymorphic solver types
 @subsection Polymorphic solver types
@@ -2910,18 +2912,16 @@
 
 Because of this possibility, predicates or functions which are defined
 using different code for different modes are by default assumed to be
-impure; the programmer must either (1) carefully ensure that the
-logical meaning of the clauses is the same for all modes,
-in which case a @samp{pragma promise_pure} declaration can be used
-or (2) declare the predicate or function as impure.
+impure; the programmer must therefore place a purity annotation on the
+declaration.
 @xref{Impurity}.
 
 In the example with @samp{append} above, the two ways of implementing
-append do have the same declarative semantics, so we can safely use
-the first approach:
+append do have the same declarative semantics, so we can safely promise
+it to be pure:
 
 @example
-	:- pragma promise_pure(append/3).
+	:- promise_pure pred append(list(T), list(T), list(T)).
 @end example
 
 In the example with @samp{var/1} above, the two clauses have different
@@ -3520,10 +3520,12 @@
 
 If you just want to see if a nondeterministic goal is satisfiable or not,
 without needing to know what variable bindings it produces,
-then there is no problem -
+then there is no problem ---
 determinism analysis considers @code{nondet} and @code{multi} goals
 with no non-local output variables to be
 @code{semidet} and @code{det} respectively.
+(There is an exception to this rule if the code is not pure.
+ at xref{Impurity}.)
 
 If you want to use the values of output variables,
 then you need to ask yourself
@@ -6056,8 +6058,8 @@
 All @samp{foreign_proc} implementations are assumed to be impure.
 If they are actually pure or semipure, they must be explicitly
 promised as such by the user (either by using foreign language
-attributes specified below, or a promise_pure or promise_semipure pragma
-as specified in @ref{Impurity}.
+attributes specified below, or a promise_pure or promise_semipure annotation
+as specified in @ref{Impurity}).
 
 Additional restrictions on the foreign language interface code
 depend on the foreign language and compilation options.
@@ -6079,7 +6081,7 @@
 @example
 :- func sin(float) = float.
 :- pragma foreign_proc("C", sin(X::in) = (Sin::out),
-        [may_call_mercury],
+        [may_call_mercury, promise_pure],
         "Sin = sin(X);").
 @end example
 
@@ -6128,8 +6130,8 @@
 @item @samp{promise_pure}/@samp{promise_semipure}
 This attribute promises that the purity of the given predicate or
 function definition is pure or semipure.
-It is equivalent to a corresponding @samp{pragma promise_pure}
-or @samp{pragma promise_semipure} declaration (@pxref{Impurity}).
+It is equivalent to a corresponding @samp{promise_pure}
+or @samp{promise_semipure} annotation on the declaration (@pxref{Impurity}).
 If omitted, the clause specified by the @samp{foreign_proc} is
 assumed to be impure.
 
@@ -8429,7 +8431,7 @@
 @c such as implementing your own exception handling.
 
 @node Impurity
- at chapter Impurity declarations
+ at chapter Impurity
 
 In order to efficiently implement certain predicates, it is occasionally
 necessary to venture outside pure logic programming.  Other predicates
@@ -8443,33 +8445,43 @@
 predicates written in Mercury significantly more efficient than similar
 C code.
 
+For this reason, Mercury allows predicates, functions and goals to be
+annotated with a purity level.
+The effect of these annotations is to give the programmer more control
+over the operational semantics of their program,
+and thereby make it possible to safely implement non-pure code
+using a variety of techniques.
+The cost of using these annotations is that the programmer must
+assume some additional responsibility to ensure that the code is safe.
+
 One important aim of Mercury's impurity system is to make the
 distinction between the pure and impure code very clear.  This is done
 by requiring every impure predicate or function to be so declared, and
-by requiring every call to an impure predicate or function to be flagged as
-such.
-Predicates or functions that are implemented in terms of impure predicates
-or functions are assumed to be impure themselves unless they are
-explicitly promised to be pure.
+by requiring every goal that introduces non-pure code to have a purity
+annotation.
+Additionally, the interfaces between pure and non-pure code must be
+explicitly marked with a ``promise'' which clearly delineates regions
+where it is the compiler's responsibility to ensure the code is safe
+from regions where this responsibility is the programmer's.
 
 Please note that the facilities described here are needed only very
 rarely.  The main intent is for implementing language primitives such as
-the all solutions predicates, or for implementing interfaces to foreign
-language libraries using the foreign language interface.  Any other use of
- at samp{impure} or @samp{semipure} probably indicates either a weakness in
-the Mercury standard library, or the programmer's lack of familiarity
-with the standard library.  Newcomers to Mercury are hence encouraged to
- at strong{skip this section}.
+the all solutions predicates, for implementing interfaces to foreign
+language libraries using the foreign language interface, or for implementing
+code that needs tighter control over the operational semantics, such
+as constraint solver implementations.  Any other use of purity annotations
+probably indicates either a weakness in the Mercury standard library,
+or the programmer's lack of familiarity with the standard library.
+Newcomers to Mercury are hence encouraged to @strong{skip this section}.
 
 @menu
 * Purity levels::       	Choosing the right level of purity.
-* Purity ordering::     	How purity levels are ordered 
+* Purity annotations::		Marking the purity level of code.
+* Purity inference::		How the purity of code is determined.
 * Impurity semantics::  	What impure code means.
-* Declaring impurity::  	Declaring predicates impure.
-* Impure goals::        	Marking a goal as impure.
-* Promising purity::    	Promising that a predicate is pure.
 * Impurity Example::    	A simple example using impurity.
 * Higher-order impurity::    	Using impurity with higher-order code.
+* Purity and type qualifiers::	Extra rules for declarations.
 @end menu
 
 
@@ -8480,14 +8492,21 @@
 
 @table @dfn
 @item pure
-For pure procedures, the set of solutions depends only on the
-values of the input arguments.
-They do not interact with the ``real'' world (i.e., do any
-input/output) without taking an io.state (@pxref{Types}) as input and
-returning one as output, and do not change the value of any data
-structure that will not be undone on backtracking (unless the data
-structure would be unreachable on backtracking).  Note that equality
-axioms are important when considering the value of data structures.
+For pure predicates and functions, there must exist a declarative semantics
+(that is, a set of ground solutions) which, given the bindings of
+arguments when called, fully determines all possible bindings at exit.
+All pure functions must be referentially transparent in the sense that
+any two expressions which are syntactically equal must be semantically
+equal.
+
+Pure predicates and functions do not interact with the ``real'' world
+(i.e., do any input/output) without taking an @code{io.state} (@pxref{Types})
+as input and returning one as output,
+and do not change the value of any data structure that will not be undone
+on backtracking (unless the data structure would be unreachable on
+backtracking).  Note that equality axioms are important when considering
+the value of data structures.
+
 The declarative semantics of pure predicates is never affected by the
 invocation of other predicates.
 It is possible for the invocation of pure predicates to affect the
@@ -8495,8 +8514,9 @@
 
 By default, Mercury predicates and functions are pure.
 Without using the foreign language interface, writing mode-specific
-clauses or calling other impure predicates and functions it is
-impossible to write impure code in Mercury.
+clauses, using a variable with inst `any' in a negated context, or calling
+other impure predicates and functions it is impossible to write impure code
+in Mercury.
 
 @item semipure
 Semipure predicates are just like pure predicates, except that their
@@ -8514,179 +8534,276 @@
 
 @end table
 
- at node Purity ordering 
- at section Purity ordering
-
 The three levels of purity have a total ordering defined upon them
 (which we will simply call the purity), where @code{pure > semipure > impure}.
 
- at node Impurity semantics
- at section Semantics
+ at node Purity annotations
+ at section Purity annotations
 
-It is important to the proper operation of impure and semipure code, to
-the flexibility of the compiler to optimize pure code, and to the
-semantics of the Mercury language, that a clear distinction be drawn
-between ordinary Mercury code and imperative code written with Mercury
-syntax.  How this distinction is drawn will be explained below; the
-purpose of this section is to explain the semantics of programs with
-impure predicates.
+There are four purity annotations that can be used to assert purity
+levels in code.
+The first two of these, @samp{impure} and @samp{semipure},
+are used to declare that a predicate, function or goal has a certain purity.
+These two annotations are checked by the compiler
+according to the rules in @ref{Purity inference},
+and it is an error if they do not match the purity level it infers.
+The remaining two, @samp{promise_pure} and @samp{promise_semipure},
+are used to assert that a predicate, function or goal is known to have
+a certain purity even though it can't be inferred.
+The compiler does not insist that these annotations match the inferred purity;
+it instead checks that the promised purity exceeds the inferred purity ---
+these annotations indicate points in the program where the programmer
+assumes responsibility for the safety of the code.
+(As with all such promises, you should use these with the utmost caution:
+if you lie to the compiler it will have its revenge!)
+
+Note that since Mercury code is pure by default,
+there is no need for a @samp{pure} annotation.
+Likewise, since asserting that code is impure imposes no burden of proof
+on the programmer, there is no need for a @samp{promise_impure} annotation.
 
-A @emph{declarative} semantics of impure Mercury code would be largely
-useless, because the declarative semantics cannot capture the intent of
-the programmer.  Impure predicates are executed for their side-effects,
-which by definition are not part of their declarative semantics.  Thus
-it is the @emph{operational} semantics of impure predicates that Mercury
-must specify, and Mercury compilers must respect.
+Purity annotations can be used in a number of places:
+ at itemize @bullet
+ at item
+In @samp{:- pred} and @samp{:- func} declarations,
+immediately after the @samp{:-}.
+ at item
+Immediately preceding a goal.
+ at item
+In the head of a lambda expression,
+immediately preceding the @samp{pred} or @samp{func}.
+ at item
+In the attributes of a @code{foreign_proc} declaration
+(@pxref{Foreign code attributes}).
+Only @code{promise_pure} and @code{promise_semipure} may be used here.
+ at item
+Immediately preceding a method in a typeclass declaration.
+Only @code{impure} and @code{semipure} may be used here.
+An instance of the type class must provide method implementations that are
+at least as pure as the method declaration. 
+ at item
+In a higher-order type expression,
+immediately preceding the @samp{pred} or @samp{func}.
+Only @code{impure} and @code{semipure} may be used here.
+ at end itemize
 
-The operational semantics of a Mercury predicate which invokes
- at emph{impure} code is a modified form of the @emph{strict sequential}
-semantics (@pxref{Semantics}).  @emph{Impure} goals may not be reordered
-relative to any other goals; not even ``minimal'' reordering as implied
-by the modes is permitted.  If any such reordering is needed, this is a
-mode error.  However, @emph{pure} and @emph{semipure} goals may be
-reordered as the compiler desires (within the bounds of the semantics
-the user has specified for the program) as long as they are not moved
-across an impure goal.  Execution of impure goals is strict: they must
-be executed if they are reached, even if it can be determined that the
-computation cannot lead to successful termination.
+Purity annotations are compulsory in some, but not all, places.
+The compiler will report an error if any purity annotation
+is not consistent with the inferred purity level,
+or if a purity annotation is not present where one is required.
+The places where a purity annotation is required are as follows:
+ at itemize @bullet
+ at item
+In @samp{pred} and @samp{func} declarations for which the definition
+is inferred to be something other than pure.
+ at item
+In front of a goal which introduces impurity or semipurity.
+ at item
+In the head of a lambda expression for which the body is inferred
+to be something other than pure,
+or which uses non-local variables with inst @samp{any}.
+ at end itemize
 
-Semipure goals can be given a ``contextual'' declarative semantics.
-They cannot have any side-effects, so it is expected that, given the
-context in which they are called (relative to any impure goals in the
-program), their declarative semantics fully captures the intent of the
-programmer.  Thus a semipure goal has a perfectly consistent declarative
-semantics, until an impure goal is reached.  After that, it has another
-(possibly different) declarative semantics, until the next impure goal
-is executed, and so on.  Mercury compilers must respect this contextual
-nature of the semantics of semipure goals; within a single context, a
-compiler may treat a semipure goal as if it were pure.
-
-
- at node Declaring impurity
- at section Declaring impure functions and predicates
-
-Every Mercury predicate or function has exactly two purity values
-associated with it.
-One is the @emph{declared} purity of the predicate or function, which is
-given by the programmer.
-The other value is the @emph{inferred} purity,
-which is calculated from the purity of goals in the body of the
-predicate or function.
-
-A predicate is declared to be impure or semipure by preceding the word
- at code{pred} in its @code{pred} declaration with @code{impure}
-or @code{semipure}, respectively.  
-Similarly, a function is declared impure or semipure by preceding the
-word @code{func} in its @code{func} declaration with @code{impure} or
- at code{semipure}.
-That is, a declaration of the form:
+ at noindent
+The only exception to this is that purity annotations are not compulsory
+on goals that are within an @code{infer_purity} scope (@pxref{Goals}).
+Inside such a scope, unannotated goals which introduce impurity (semipurity)
+are treated as if they had an @code{impure} (@code{semipure}) annotation,
+and all other goals are left unchanged.
+(Note, however, that there is a current limitation that the purity level
+of higher-order calls cannot be inferred,
+so omitting the annotation from a higher-order call is likely to lead
+to a type error.
+XXX there may also be a similar limitation whereby argument unifications
+are not handled properly without an explicit annotation.)
+
+The requirement that goals which introduce impurity (semipurity)
+be marked with @code{impure} (@code{semipure}) allows someone 
+reading the code to tell which goals are not pure and why,
+making code which relies on side effects somewhat less mysterious.
+Furthermore, it means that if a call is @emph{not} preceded by
+ at code{impure} or @code{semipure}, then the reader can rely on the call
+having a proper declarative semantics, without hidden side-effects,
+can rely on negations being implemented soundly,
+and can rely on expressions being referentially transparent.
+
+ at node Purity inference
+ at section Purity inference
+
+Purity inference for goals is a fairly straightforward bottom-up analysis.
+Some goals, listed below, introduce impurity, and this impurity propagates
+upwards until a ``promise'' removes it, or until it is encapsulated in a
+lambda expression.
 
- at example
-:- impure pred @var{Pred}(@var{Arguments}@dots{}).
-:- semimpure pred @var{Pred}(@var{Arguments}@dots{}).
- at end example
+Impurity and semipurity are introduced by the following goals:
 
- at noindent
-or
+ at itemize @bullet
+ at item
+Calls to impure (semipure) predicates or functions are impure (semipure).
+Note that calls to impure or semipure functions can only occur if the
+function call is at the top level
+(i.e., immediately adjacent to the @samp{=/2} predicate).
+ at item
+Calls to higher-order values which have an impure (semipure) type
+are impure (semipure).
+ at item
+Negations which use non-local variables with inst @samp{any} are impure.
+ at item
+If-then-elses which use non-local variables with inst @samp{any}
+in the condition are impure.
+ at end itemize
 
- at example
-:- impure func @var{Func}(@var{Arguments}@dots{}) = Result.
-:- semipure func @var{Func}(@var{Arguments}@dots{}) = Result.
- at end example
+For other goals, the purity level is determined as follows:
 
- at noindent
-declares the predicate @var{Pred} to be impure and the function
- at var{Func} to be semipure, respectively.
+ at table @asis
+ at item @code{some @var{Vars} @var{Goal}}
+ at itemx @code{all @var{Vars} @var{Goal}}
+ at itemx @code{infer_purity @var{Goal}}
+ at itemx @code{promise_equivalent_solutions @var{Vars} @var{Goal}}
+ at itemx @code{not @var{Goal}}
+ at itemx @code{\+ @var{Goal}}
+The purity level is the same as that of @var{Goal}.
 
-Type class methods may also be declared as @code{impure} or
- at code{semipure} by preceeding the word @code{pred} or @code{func} with the
-appropriate purity level.  An instance of the type class must provide
-method implementations that are at least as pure as the method
-declaration. 
+ at item @code{@var{Purity} @var{Goal}}
+If @var{Purity} is @code{promise_pure} (@code{promise_semipure}) then
+the purity level is @code{pure} (@code{semipure}).
+If @var{Purity} is @code{impure} (@code{semipure}) then
+the purity level is @code{impure} (@code{semipure}),
+and must be the same as the purity level of @var{Goal}.
 
- at node Impure goals
- at section Marking a goal as impure
+ at item @code{@var{Goal1}, @var{Goal2}}
+ at itemx @code{@var{Goal1} ; @var{Goal2}}
+ at itemx @code{@var{Goal1} => @var{Goal2}}
+ at itemx @code{@var{Goal1} <= @var{Goal2}}
+ at itemx @code{@var{Goal1} <=> @var{Goal2}}
+The purity level is the same as that of @var{Goal1} or @var{Goal2},
+whichever is lower in the purity ordering.
 
-If predicate @code{p/N} is declared to be @code{impure} (@code{semipure})
-then all calls to @code{p/N} must be annotated with @code{impure}
-(@code{semipure}):
+ at item @code{if @var{CondGoal} then @var{ThenGoal} else @var{ElseGoal}}
+ at itemx @code{@var{CondGoal} -> @var{ThenGoal} ; @var{ElseGoal}}
+The purity level is the same as that of @var{CondGoal}, @var{ThenGoal}
+or @var{ElseGoal},
+whichever is lower in the purity ordering.
 
- at example
-	impure p(X1, X2, ..., XN)
- at end example
+ at item @code{true}
+ at itemx @code{fail}
+The purity level is @code{pure}.
 
-If function @code{f/N} is declared to be @code{impure} (@code{semipure})
-then all applications of @code{f/N} must be obtained by unification with a
-variable and the unification goal as a whole be annotated with @code{impure}
+ at item @code{@var{Term1} = @var{Term2}}
+Unifications that do not involve calls to impure or semipure functions
+are @code{pure}.
 
- at example
-	impure X = f(X1, X2, ..., XN)
- at end example
+ at item @code{@var{Term1} \= @var{Term2}}
+Inequalities that do not involve calls to impure or semipure functions
+are @code{pure}.
 
-Any call or unification goal containing a non-local variable with inst any that
-appears in a negated context (i.e., in a negation or the condition of an
-if-then-else goal) must be given an @code{impure} annotation because it may
-violate referential transparency.
+ at item @code{call(Closure)}
+ at itemx @code{call(Closure1, Arg1)}
+ at itemx @code{call(Closure2, Arg1, Arg2)}
+ at itemx @code{call(Closure3, Arg1, Arg2, Arg3)}
+ at itemx @dots{}
+ at itemx @code{Var}
+ at itemx @code{Var(Arg1)}
+ at itemx @code{Var(Arg2)}
+ at itemx @code{Var(Arg2, Arg3)}
+ at itemx @dots{}
+Calls to higher-order values with pure types are @code{pure}.
+
+ at ifset aditi
+
+ at item @code{aditi_bulk_delete(@dots{})}
+ at itemx @code{aditi_bulk_insert(@dots{})}
+ at itemx @code{aditi_bulk_modify(@dots{})}
+ at itemx @code{aditi_delete(@dots{})}
+ at itemx @code{aditi_insert(@dots{})}
+The Aditi database interface is pure.
+(XXX ?)
+
+ at end ifset
+ at c aditi
+
+ at item @code{@var{Call}}
+Calls to pure predicates are @code{pure}.
 
-Compound goals should not have purity annotations.
+ at end table
 
-The compiler will report an error if a required purity annotation is 
-omitted from a call or unification goal or if a @code{semipure} annotation
-is used where an @code{impure} annotation is required.  The compiler will
-report a warning if a semipure goal is annotated with @code{impure} or a
-pure goal is annotated with @code{semipure}
+The purity of a lambda expression is @code{impure} if the
+lambda expression uses any non-local variables with inst @samp{any}.
+Otherwise the purity is the same as that of the body of the expression.
+Note that the assignment of a higher-order value to a variable is pure,
+even of the value has a type which is not.
 
-The requirement that impure or semipure calls be marked with
- at code{impure} or @code{semipure} allows someone 
-reading the code to tell which goals are not pure, making code which
-relies on side effects somewhat less mysterious.  Furthermore, it means
-that if a call is @emph{not} preceded by @code{impure} or
- at code{semipure}, then the reader can rely on the call having a proper
-declarative semantics, without hidden side-effects.  
+The purity of a predicate or function definition is inferred as follows:
 
+ at itemize @bullet
+ at item
+If it is defined using @code{foreign_proc} then its purity is
+determined by the attributes on the foreign code.
+By default it will be inferred impure.
+ at item
+If it is defined using different code for different modes then
+it is inferred impure.
+ at item
+Otherwise, its purity level will be inferred to be the same as
+the purity level of the body of the definition.
+ at end itemize
 
- at node Promising purity
- at section Promising that a predicate is pure
+ at noindent
+If more than one of these rules applies
+then the inferred purity level is the minimum of the applicable levels,
+according to the purity ordering.
+
+Note that the @emph{actual} purity of a predicate or function will
+differ from the inferred purity if the declaration has a @code{promise_pure}
+or @code{promise_semipure} annotation.
 
-Predicates that are implemented in terms of impure or semipure predicates are
-assumed to have the least of the purity of the goals in their body.
-The declared purity of a predicate must not be more pure
-than the inferred purity; if it is, the compiler must generate an error.
-If the declared purity is less pure than the inferred purity, the
-compiler should issue a warning (this is similar to the above case for
-goals).
-Because the inferred purity of the predicate is calculated from the
-declared purity of the calls it executes,  the lowest purity bound is
-propagated up from callee to caller through the program.
+ at node Impurity semantics
+ at section Semantics
 
-In some cases the impurity of a predicate's body is an implementation
-detail which should not be exposed to callers. These predicates are
-pure or semipure even though they call impure or semipure predicates.
-The only way for the programmer to stop the propagation of impurity is to
-explicitly promise that the predicate or function is pure or semipure.
+It is important to the proper operation of impure and semipure code, to
+the flexibility of the compiler to optimize pure code, and to the
+semantics of the Mercury language, that a clear distinction be drawn
+between ordinary Mercury code and imperative code written with Mercury
+syntax.  How this distinction is drawn is explained above; the
+purpose of this section is to explain the semantics of programs with
+impure predicates.
 
-Of course, the Mercury compiler cannot verify that the predicate's
-purity matches the promise, so it is the programmer's responsibility
-to ensure this.  If a predicate is promised pure or semipure and is not,
-the behaviour of the program is undefined.
+A @emph{declarative} semantics of impure Mercury code would be largely
+useless, because the declarative semantics cannot capture the intent of
+the programmer.  Impure predicates are executed for their side-effects,
+which by definition are not part of their declarative semantics.  Thus
+it is the @emph{operational} semantics of impure predicates that Mercury
+must specify, and Mercury compilers must respect.
 
-The programmer may promise that a predicate or function is pure or semipure
-using the @code{promise_pure} and @code{promise_semipure} pragmas:
+The operational semantics of a Mercury predicate which contains
+ at emph{impure} goals is a modified form of the @emph{strict sequential}
+semantics (@pxref{Semantics}).  Goals which have an @code{impure} annotation
+may not be reordered relative to any other goals;
+not even ``minimal'' reordering as implied by the modes is permitted.
+If any such reordering is needed, this is a mode error.
+However, goals with a @code{semipure} annotation and goals with no annotation
+may be reordered as the compiler desires (within the bounds of the semantics
+the user has specified for the program) as long as they are not moved
+across an goal which is annotated @code{impure}.
 
- at example
-:- pragma promise_pure(@var{Name}/@var{Arity}).
-:- pragma promise_semipure(@var{Name}/@var{Arity}).
- at end example
+Execution of impure goals is strict: they must
+be executed if they are reached, even if it can be determined that the
+computation cannot lead to successful termination.
+Impure disjuncts cannot be pruned away even if the disjunction has
+already succeeded and there are no output variables.
 
-Programmers should be very careful about mixing code that is promised
-pure with impure predicates or functions that may manipulate the
-same hidden state (for example, the impure predicates used to implement 
-a predicate that is promised pure); the @samp{promise pure} declaration
-is supposed to promise that impure code cannot change the declarative
-semantics of pure code.  The module system can be used to minimize the
-possibility of making errors with such code, by keeping impure
-predicates or functions behind the interface where code is promised
-pure.
+Goals which are annotated @code{semipure} can be given a ``contextual''
+declarative semantics.  They cannot have any side-effects,
+so it is expected that, given the context in which they are called
+(relative to any @code{impure} annotations in the program),
+their declarative semantics fully captures the intent of the
+programmer.  Thus a semipure goal has a perfectly consistent declarative
+semantics, until a goal with an @code{impure} annotation is reached.
+After that, it has another (possibly different) declarative semantics,
+until the next goal with @code{impure} annotation is executed, and so on.
+Mercury compilers must respect this contextual nature of the semantics of
+semipure goals; within a single context, a compiler may treat a semipure
+goal as if it were pure.
 
 @node Impurity Example
 @section An example using impurity
@@ -8714,8 +8831,7 @@
         [will_not_call_mercury],
         "X = max;").
 
-:- pragma promise_pure(max_solution/2).
-:- pred max_solution(pred(int), int).
+:- promise_pure pred max_solution(pred(int), int).
 :- mode max_solution(pred(out) is multi, out) is det.
 
 max_solution(Generator, Max) :-
@@ -8823,6 +8939,18 @@
 		impure Ys = map(ImpureFunc, Ys).
 @end example
 
+ at node Purity and type qualifiers
+ at section Purity and type qualifiers
+
+Predicate and function declarations that make use of @code{`with_type`}
+can contain purity annotations in more than one location.
+These must be consistent, but they need not match exactly.
+The rules for which combinations are legal,
+and determining the purity level that results,
+are as follows:
+
+XXX
+
 @node Pragmas
 @chapter Pragmas
 
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------