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

[Mark Brown]

On 16-Dec-2005, Julien Fischer <juliensf at cs.mu.OZ.AU> wrote:
> 
> On Thu, 15 Dec 2005, Mark Brown wrote:
> > +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}.
> > +
> 
> Could we avoid referring to `with_type` since `:` is also acceptable?
> How about:
> 
> 	If an explicit type qualification is used then the ...

okay.  Note that "with_type" is still used in lots of places in the
reference manual.

> > +A @emph{declarative} semantics of impure Mercury code would be largely
> > +useless, because the declarative semantics cannot capture the intent of
> 
> Is there any point in quantifying the degree of uselessness?

:-)

No, it is fairly pointless.

> 
> > +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.
> >
> 
> Elsewhere in the reference manual we use the terminology "Mercury
> implementations" rather than "Mercury compilers".

Fixed.  But there are also a few existing places that refer to the
compiler rather than the implementation.

> > -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;
> 
> s/cannot/may not/

Changed to "will not", as per our in-person discussion.

Thanks for the comments.  I think I've addressed all the points that have
come up so far -- relative diff follows.

Cheers,
Mark.

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	16 Dec 2005 06:16:36 -0000
@@ -484,12 +484,11 @@
 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
+implicitly_pure                 fx                950
+implicitly_semipure             fx                950
+implicitly_impure               fx                950
 some                            fxy               950
 ,                               xfy               1000
 &                               xfy               1025
@@ -647,35 +646,25 @@
 @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{implicitly_pure @var{PureGoal}}
+ at itemx @code{implicitly_semipure @var{SemipureGoal}}
+ at itemx @code{implicitly_impure @var{ImpureGoal}}
+Introduces a scope within which purity annotations (@pxref{Impurity}) are
+optional, and all purity levels are inferred.
+ at var{PureGoal} must be a valid goal which is inferred pure.
+ at var{SemipureGoal} must be a valid goal which is inferred semipure.
+ at var{ImpureGoal} must be a valid goal which is inferred impure.
+(Note, however, that there is a current limitation that the purity level of
+higher-order predicate calls and function applications cannot be inferred,
+so omitting the annotations on these is likely to lead to a type error.
+There is also a similar limitation whereby argument unifications are not
+handled properly without a purity annotation.)
 
 @item @code{promise_equivalent_solutions @var{Vars} @var{Goal}}
 A determinism cast.
@@ -1426,6 +1415,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 +1468,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 +1632,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 +1875,12 @@
 :- pred f(int, T, U) = U.
 @end example
 
+Predicate and function declarations may also include a purity annotation.
+If an explicit type qualification 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{Purity and explicit type qualification}.
+
 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 +2383,19 @@
 @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 inferred to be impure.
+
+Similarly, referential transparency may 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 +2921,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 +3529,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 +6067,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 +6090,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 +6139,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 +8440,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 +8454,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 explicit type qualification::	Extra rules for declarations.
 @end menu
 
 
@@ -8480,14 +8501,22 @@
 
 @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, the set of solutions depends only on
+the initial bindings of the arguments (including the return value in the
+case of functions).  That is, there must exist a declarative semantics
+(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 function
+applications 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 +8524,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 +8544,292 @@
 
 @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 ``purity cast'' in the downwards direction can be effected by the
+use of one of the builtin predicates @samp{impure_true}, @samp{impure_false},
+ at samp{semipure_true} or @samp{semipure_false}.
+These are declaratively equivalent to @samp{true} or @samp{false},
+as appropriate, but are defined to be less pure.
 
-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 the following 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.  It is 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
+(@pxref{Purity inference}).
+ 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{implicitly_pure}, @code{implicitly_semipure},
+or @code{implicitly_impure} 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 predicate calls and function applications cannot be inferred,
+so omitting the annotations on these is likely to lead to a type error.
+There is also a similar limitation whereby argument unifications are not
+handled properly without a purity annotation.)
+
+The requirement for goals which introduce impurity (semipurity)
+to 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 bottom-up process.
+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{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{implicitly_pure @var{Goal}}
+The purity level is @code{pure}.
 
- at node Impure goals
- at section Marking a goal as impure
+ at item @code{implicitly_semipure @var{Goal}}
+The purity level is @code{semipure}.
 
-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{implicitly_impure @var{Goal}}
+The purity level is @code{impure}.
+
+ 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 example
-	impure p(X1, X2, ..., XN)
- at end example
+ 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 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{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 X = f(X1, X2, ..., XN)
- at end example
+ at item @code{true}
+ at itemx @code{fail}
+The purity level is @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{@var{Term1} = @var{Term2}}
+Unifications that do not involve calls to impure or semipure functions
+are @code{pure}.
 
-Compound goals should not have purity annotations.
+ at item @code{@var{Term1} \= @var{Term2}}
+Inequalities that do not involve calls to impure or semipure functions
+are @code{pure}.
 
-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}
+ 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}.
 
-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.  
+ 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 node Promising purity
- at section Promising that a predicate is pure
+ at end ifset
+ at c aditi
 
-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 item @code{@var{Call}}
+Calls to pure predicates are @code{pure}.
 
-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.
+ at end table
 
-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.
+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 programmer may promise that a predicate or function is pure or semipure
-using the @code{promise_pure} and @code{promise_semipure} pragmas:
+The purity of a predicate or function definition is inferred as follows:
 
- at example
-:- pragma promise_pure(@var{Name}/@var{Arity}).
-:- pragma promise_semipure(@var{Name}/@var{Arity}).
- at end example
+ 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 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.
+
+ at node Impurity semantics
+ at section Semantics
+
+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 code.
+
+For the purposes of this section, ``impure goals'' refers to goals that
+have an explicit @code{impure} annotation or goals that introduce impurity.
+The latter may not have an explicit annotation if they are within a
+scope which makes these optional, but the semantics is not affected by that.
+Similarly, ``semipure goals'' refers to goals that have an explicit
+ at code{semipure} annotation or goals that introduce impurity.
+
+A @emph{declarative} semantics of impure Mercury code would be useless,
+because the declarative semantics cannot capture the intent of
+the programmer.  Impure goals 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 goals that Mercury
+must specify, and Mercury implementations must respect.
+
+The operational semantics of a Mercury predicate that contains impure
+goals is a modified form of the @emph{strict sequential} semantics
+(@pxref{Semantics}).  Impure goals will not be reordered relative to any
+other goals; not even ``minimal'' reordering as implied by the modes is
+permitted.  It is a mode error if any such reordering is required.
+All other goals (including 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.
+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.
+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),
+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 reached,
+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 +8857,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 +8965,18 @@
 		impure Ys = map(ImpureFunc, Ys).
 @end example
 
+ at node Purity and explicit type qualification
+ at section Purity and explicit type qualification
+
+Predicate and function declarations that make use of explicit type
+qualification may 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
--------------------------------------------------------------------------