[m-dev.] Diff: Make Mercury cope with impure code (part 2/2)

[Fergus Henderson]

Peter Schachte wrote:

reference_manual.texi:
>  There is another operational semantics of Mercury programs called
>  the @dfn{strict commutative} operational semantics.  This semantics
> -is equivalent to the strict sequential operation semantics except
> +is equivalent to the strict sequential operational semantics except
>  that there is no requirement that function calls, conjunctions and disjunctions 
>  be executed left-to-right; they may be executed in any order.
> + at c XXX May they be interleaved?
>  (The order may even be different each time a particular goal
>  is entered.)

Yes, they can be interleaved.
Please add that.

> + at node Impurity
> + at section Impurity declarations
> +
> +In order to efficiently implement certain predicates, it is sometimes
> +necessary to venture outside pure logic programming.

I suggest s/sometimes/occaisionally/

> +Other predicates
> +cannot be implemented at all within the paradigm of logic programming,
> +for example, all solutions predicates.  Such predicates are often
> +written using the C interface.  Sometimes, however, it would be more
> +convenient, or more efficient, to write such predicates using the
> +facilities of Mercury.  For example, it is much more convenient to
> +access arguments of compound Mercury terms in Mercury than in C, and the
> +ability of the Mercury compiler to specialize code can make higher-order
> +predicates written in Mercury significantly more efficient than similar
> +C code.
> +
> +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 to be so declared, and by requiring
> +every call to an impure predicate to be flagged as such.  Predicates
> +that are implemented in terms of impure predictes are assumed to be
> +impure themselves unless they are explicitly promised to be pure.

I suggest you add the following paragraph here:

	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.  Any use of `impure' or `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
	@strong{skip this section}.

> +Most Mercury predicates are pure.  

I suggest s/Most/The vast majority of/

> +The operational semantics of a Mercury predicate which invokes impure
> +code is a modified form of the @emph{strict sequential} semantics
> +(@pxref{Semantics}).  Firstly, only impure goals may not be reordered
> +relative to other goals, pure and semipure goals may be reordered as
> +long as they are not moved across an impure goal.

I think it would be clearer if you delete the word "only", and
change the last comma to a semi-colon.

> Secondly, not even
> +``minimal'' reordering of impure goals is permitted; if such reordering
> +is needed, this is an error.

I would change that to

	Secondly, for impure goals not even ``minimal'' reordering
	as implied by the modes is permitted; if any such reordering
        is needed, this is a mode error.

And maybe delete the "Firstly, " and "Secondly, ".

> +A predicate is declared to be impure (semipure) by preceding the word
> + at code{predicate} in its @code{pred} declaration with @code{impure}
> +(@code{semipure}).  That is, a declaration of the form:

I think you should make the following changes:

	s/impure (semipure)/impure or semipure/
	s/@code{impure} (@code{semipure})/impure or semipure respectively/

and ditto elsewhere.

> + at node Impure calls
> + at subsection Marking a call as impure
> +
> +If a predicate is impure (semipure), all calls to it must be preceded
> +with the word @code{impure} (@code{semipure}).  This allows someone
> +reading the code to tell which goals are not pure, making code which
> +relies on side effects somewhat less mysterious.

and (more importantly) ensuring that if a call is @emph{not} preceded by
@code{impure} or @code{semipure}, then the reader can rely on
the call having a proper declarative semantics, without hidden
side-effects.


>See @ref{Impurity
> +Example} for an example of this.

Put this before the previous sentence, otherwise the referent of
"this" gets lost with the text I've added.

> Note that only predicate calls need to
> +be prefixed with @code{impure} or @code{semipure}, compound goals never
> +need this.
> +
> +
> + at node Promising purity
> + at subsection Promising a predicate is pure
> +
> +Some predicates which call impure or semipure predicates are themselves
> +pure.  In fact, the main purpose of the Mercury impurity system is to
> +allow users to write pure predicates using impure ones, while protecting
> +the procedural implementation from aggressive compiler optimizations.
> +Of course, the Mercury compiler cannot verify that a predicate is pure,
> +so this is the user's responsibility.
> +
> +The user may promise that a predicate is pure using the
> + at code{promise_pure} pragma:

s/user/programmer/g

This is typically supposed to be used only by _implementors_, not users.

> + at node Impurity Example
> + at subsection An example using impurity
[...]
> + at example
> +:- pragma c_header_code("int max;").

s/int/Integer/

> +:- impure pred init_max is det.
> +:- pragma c_code(init_max,
> +        will_not_call_mercury,
> +        "max = (int)(~(((unsigned)(~0))>>1));").

As I said last time: why not "max = INT_MIN" instead?
(You'd also need `:- pragma c_header_code("#include <limits.h>")'.)

> +++ transition_guide.texi	1997/10/01 00:53:09
> @@ -154,6 +154,7 @@
>  end_module      fx              1199
>  if              fx              1160
>  import_module   fx              1199
> +impure          fy              1199
>  inst            fx              1199
>  is              xfx             700
>  mod             xfx             300
> @@ -163,6 +164,7 @@
>  or              xfy             740
>  pred            fx              1180
>  rule            fx              1199
> +semipure        fy              1199
>  some            fxy             950
>  then            xfx             1150
>  type            fx              1180

You should also change the precedence of `pred' and `func'.

> %  XXX The current implementation doesn't handle impure functions.  The main
> %      reason is that handling of nested functions is likely to get pretty 
> %      confusing.  Because impure functions can't be reordered, the execution
> %      order would have to be strictly innermost-first, left-to-right, and 
> %      predicate arguments would always have to be evaluated before the
> %      predicate call.  Implied modes are right out.  All in all, they just
> %      won't be as natural as one might think at first.

True, but semipure functions might be quite desirable...

How much extra work would it be to implement impure/semipure functions?

purity.m:
> :- implementation.
> 
> :- import_module make_hlds, hlds_data, hlds_pred, hlds_goal, prog_io_util.
> :- import_module type_util, mode_util, code_util, prog_data, unify_proc.
> :- import_module globals, options, mercury_to_mercury, hlds_out, int, set.
> :- import_module passes_aux, typecheck, module_qual, clause_to_proc.
> :- import_module modecheck_unify, modecheck_call, inst_util.
> :- import_module list, map, varset, term, prog_out, string, require, std_util.
> :- import_module assoc_list, bool.

Please keep the library modules and compiler modules in separate lists.
`prog_out', `int', and `set' are in the wrong list.

> %			Check purity of a single predicate
> %
> %  Purity checking is quite simple.  Since impurity /must/ be declared, we can
> %  perform a single pass checking that the actual purity of each predicate
> %  matches the declared (or implied) purity.  A predicate is just as pure as
> %  its least pure goal.  While we're doing this, we attach a `feature' to each
> %  goal that is not pure, including non-atomic goals, indicating its purity.
> %  This information must be maintained by later compilation passes, at least
> %  until after the last pass that may perform transformations that would not
> %  be correct for impure code.

I suspect that you have just introduced a significant number of bugs :-(

Any ideas on how we can verify that the existing compiler passes
preserve the purity feature in goal_infos?

> As we check purity and attach impurity
> %  features, we also check that impure (semipure) atomic goals were marked in
> %  the source code as impure (semipure).  At this stage in the computation,
> %  this is indicated by already having the appropriate goal feature.  (During
> %  the translation from term to goal, calls have their purity attached to
> %  them, and in the translation from goal to hlds_goal, the attached purity is
> %  turned into the appropriate feature in the hlds_goal_info.

You're missing a ')'.

> compute_expr_purity(Unif0, Unif, GoalInfo, PredInfo, ModuleInfo, InClosure,
> 		pure, NumErrors0, NumErrors) -->
> 	{ Unif0 = unify(A,RHS0,C,D,E) },
> 	{ Unif  = unify(A,RHS,C,D,E) },
> 	error_if_body_purity_indicated(GoalInfo, NumErrors0, NumErrors1,
> 				       InClosure, "unification"),
> 	(   { RHS0 = lambda_goal(F, G, H, I, Goal0-Info0) } ->
> 		{ RHS = lambda_goal(F, G, H, I, Goal-Info0) },

Please s/-/ - /g

> compute_expr_purity(Ccode, Ccode, _, _, _, _, pure, NumErrors, NumErrors) -->
> 	{ Ccode = pragma_c_code(_,_,_,_,_,_,_,_) }.

Hmm, what if the pragma_c_code is for an impure pred?
That won't happen currently, because we don't inline pragma_c_codes until
_after_ purity checking, but I think it might be more robust to check it.
You just need to look up the pred_info for the pred (the pred_id is
one of the fields of `pragma_c_code(...)' HLDS goals).

> :- pred error_inconsistent_promise(module_info, pred_info, pred_id, purity,
> 				  io__state, io__state).
> :- mode error_inconsistent_promise(in, in, in, in, di, uo) is det.
> 
> error_inconsistent_promise(ModuleInfo, PredInfo, PredId, Purity) -->
> 	{ pred_info_context(PredInfo, Context) },
> 	write_context_and_pred_id(ModuleInfo, PredInfo, PredId),
> 	prog_out__write_context(Context),
> 	report_warning("  warning: declared "),
> 	write_purity(Purity),
> 	io__write_string(" but promised pure.\n"),

The message will probably be clearer if you insert some quotes:

 	report_warning("  warning: declared `"),
 	write_purity(Purity),
 	io__write_string("' but promised `pure'.\n"),

> warn_exaggerated_impurity_decl(ModuleInfo, PredInfo, PredId,
> 		DeclPurity, AcutalPurity) -->
> 	{ pred_info_context(PredInfo, Context) },
> 	write_context_and_pred_id(ModuleInfo, PredInfo, PredId),
> 	prog_out__write_context(Context),
> 	report_warning("  warning: declared "),
> 	write_purity(DeclPurity),
> 	io__write_string(" but actually "),
> 	write_purity(AcutalPurity),
> 	io__write_string(".\n").

Ditto.

> :- pred warn_unnecessary_promise_pure(module_info, pred_info, pred_id,
> 				  io__state, io__state).
> :- mode warn_unnecessary_promise_pure(in, in, in, di, uo) is det.
> 
> warn_unnecessary_promise_pure(ModuleInfo, PredInfo, PredId) -->
> 	{ pred_info_context(PredInfo, Context) },
> 	write_context_and_pred_id(ModuleInfo, PredInfo, PredId),
> 	prog_out__write_context(Context),
> 	report_warning("  warning: unnecessary `promise_pure' pragma.\n"),
> 	globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
> 	( { VerboseErrors = yes } ->
> 		prog_out__write_context(Context),
> 		{ pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
> 		io__write_string("  This "),
> 		hlds_out__write_pred_or_func(PredOrFunc),
> 		io__write_string(
> 		    " does not invoke any non-pure code,\n"
> 		),

"non-pure" is not very nice English, IMHO.
I suggest "impure or semipure" instead.

(Ditto in a couple of other places.  Do a grep for "non-pure".)

> New File: tests/hard_coded/purity.m
> ===================================================================
> % Various checks that impurity declarations are treated properly.
> 
> :- module purity.
> :- interface.
> :- import_module io.
> :- impure pred main(io__state::di, io__state::uo) is det.

I'm still not sure whether we should not allow main/2 to be impure.
One argument against allowing main/2 to be impure is that it would
make it a little bit harder for an implementation to use a different
calling convention for impure goals.

Oh, and one more thing -- can you add a test case for inlining of impure goals?

-- 
Fergus Henderson <fjh at cs.mu.oz.au>   WWW: <http://www.cs.mu.oz.au/~fjh>  
Note: due to some buggy software and a (probably accidental)
denial-of-service attack, any mail sent to me between
	Tue Nov 25 20:00:00 UTC (6am Wed, local time)
and	Wed Nov 26 06:00:00 UTC (4pm, local time)
may have gone into the bit-bucket.  Please re-send it.