[m-rev.] For review: more fixes to impurity

[Ralph Becket]

Julien Fischer, Friday, 18 November 2005:
> On Fri, 18 Nov 2005, Ralph Becket wrote:
> 
> > Estimated hours taken: 2
> > Branches: main
> >
> > Remove now incorrect errors of the form "unification with expression was
> > declared impure, but expression was not a function call."
> >
> > compiler/purity.m:
> > 	Prevent purity.m from reporting unifications marked with
> > 	impure as errors: unifications *can* be impure if they
> > 	unify two inst any variables in a negated context.  Purity
> > 	error reporting for unifications is now handled in modecheck_unify.m.
> >
> The fact that unifications can now have purity annotations attached to
> them should be mentioned in the purity section of the reference manual.
> >
> You will probably also need to have a look at
> tests/warnings/purity_warnings as well.

How about this:

unchanged:
--- doc/reference_manual.texi	16 Nov 2005 07:02:00 -0000	1.337
+++ doc/reference_manual.texi	18 Nov 2005 05:53:23 -0000
@@ -8439,7 +8439,7 @@
 * Purity ordering::     	How purity levels are ordered 
 * Impurity semantics::  	What impure code means.
 * Declaring impurity::  	Declaring predicates impure.
-* Impure calls::        	Marking a call as 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.
@@ -8577,32 +8577,37 @@
 method implementations that are at least as pure as the method
 declaration. 
 
- at node Impure calls
- at section Marking a call as impure
+ at node Impure goals
+ at section Marking a goal as impure
 
-Every call to a Mercury predicate or function also has exactly two
-purity values associated with it.
-One is the declared purity of the call, which is
-given by the programmer as an annotation of the call.
-The other value is the inferred purity,
-which is the purity of the predicate or function.
-
-It is an error for the declared purity of a goal to be more pure than
-the inferred purity; the compiler should flag this as an error.
-The compiler should issue a warning if the declared purity of a goal is
-less pure than its inferred purity.
-
-If a predicate is impure or semipure, all calls to it must be preceded
-with the word @code{impure} or @code{semipure}, respectively. 
-
-If a function is impure or semipure, it must be called as part of a
-simple unification with a variable, and this unification must be
-prefixed by the word @code{impure} or @code{semipure}, respectively.
-
-Note that only predicate calls and unifications of variables with 
-functions need to (and are permitted to) be prefixed
-with @code{impure} or @code{semipure}.  Compound goals never need this.
-See @ref{Impurity Example} for an example of this syntax.
+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 start example
+	impure p(X1, X2, ..., XN)
+ at end example
+
+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 start example
+	impure X = f(X1, X2, ..., XN)
+ at end example
+
+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.
+
+Compound goals should not have impurity annotations.
+
+The compiler will report an error if a required impurity 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 @{impure} or a pure goal
+is annotated with @code{semipure}
 
 The requirement that impure or semipure calls be marked with
 @code{impure} or @code{semipure} allows someone 
only in patch2:
unchanged:
--- tests/warnings/purity_warnings.exp	17 Jan 2005 05:01:48 -0000	1.2
+++ tests/warnings/purity_warnings.exp	18 Nov 2005 04:47:21 -0000
@@ -11,11 +11,15 @@
 purity_warnings.m:036: In call to predicate `io.write_string/3':
 purity_warnings.m:036:   warning: unnecessary `semipure' indicator.
 purity_warnings.m:036:   No purity indicator is necessary.
-purity_warnings.m:034: In predicate `purity_warnings.semipure_pred/2':
-purity_warnings.m:034:   warning: declared semipure but actually pure.
 purity_warnings.m:065: In call to predicate `io.print/3':
 purity_warnings.m:065:   warning: unnecessary `impure' indicator.
 purity_warnings.m:065:   No purity indicator is necessary.
+purity_warnings.m:060: In predicate `purity_warnings.impure_method1a_impl/2':
+purity_warnings.m:060:   purity error: predicate is impure.
+purity_warnings.m:060:   It must be declared `impure' or promised pure.
 purity_warnings.m:071: In call to predicate `io.print/3':
 purity_warnings.m:071:   warning: unnecessary `semipure' indicator.
 purity_warnings.m:071:   No purity indicator is necessary.
+purity_warnings.m:062: In predicate `purity_warnings.semipure_method_a_impl/2':
+purity_warnings.m:062:   purity error: predicate is semipure.
+purity_warnings.m:062:   It must be declared `semipure' or promised pure.
only in patch2:
unchanged:
--- tests/warnings/purity_warnings.m	20 Feb 2004 04:18:16 -0000	1.2
+++ tests/warnings/purity_warnings.m	18 Nov 2005 04:46:57 -0000
@@ -31,7 +31,7 @@
 	{ semipure get_x(X) },
 	print("X = "), print(X), nl.
 
-:- semipure pred semipure_pred(io__state::di, io__state::uo) is det. % warn
+:- semipure pred semipure_pred(io__state::di, io__state::uo) is det.
 semipure_pred -->
 	semipure io__write_string("semipure_pred1\n").		% warn
 
@@ -57,9 +57,9 @@
 		semipure print("semipure_method_b\n"))	% XXX should warn
 ].
 
-:- pred impure_method1a_impl(io::di, io::uo) is det.
+:- pred impure_method1a_impl(io::di, io::uo) is det.	% warn
 :- semipure pred impure_method2a_impl(io::di, io::uo) is det.
-:- pred semipure_method_a_impl(io::di, io::uo) is det.
+:- pred semipure_method_a_impl(io::di, io::uo) is det.	% warn
 
 impure_method1a_impl -->
 	impure print("impure_method1a_impl\n").		% warn


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