[m-dev.] for review: impure functions

[David Glen JEFFERY]

On 04-Apr-2000, Tyson Dowd <trd at cs.mu.OZ.AU> wrote:
> 
> Add impure functions to Mercury, clean up the purity module somewhat,
> fix some bugs in purity, update and expand the purity documentation, 
> and re-organize the purity checks.

> compiler/notes/authors.html:
> 	Add Peter Schachte to the authors list.

As an aside, there seem to be a few other people missing from the authors list
too...

> doc/reference_manual.texi:
> 	Document impure functions.
> 	Expand more on what impure predicates/functions can do.
> 	Explain the concept of worst purity, and use it to explain the
> 	"inferred purity"/"declared purity" concepts.
> 	Make it more explicit that only impure goals obey
> 	strict-sequential like semantics.
> 
> tests/invalid/type_inf_loop.err_exp2:
> 	Fix this test case to reflect the new error message new that we 
> 	check the purity of this code correctly (or rather, we correctly
> 	fail to be able to purity check this code).
> 
> tests/hard_coded/Mmakefile:
> tests/hard_coded/purity.exp:
> tests/hard_coded/purity.m:
> tests/hard_coded/purity/Mmakefile:
> tests/hard_coded/purity/impure_func_t1.m:
> tests/hard_coded/purity/purity.m:
> tests/hard_coded/purity/runtests:
> 	Remove purity tests from the hard_coded directory, give it a
> 	sub-directory of its own.
> 
> tests/invalid/Mmakefile:
> tests/invalid/purity.err_exp:
> tests/invalid/purity.m:
> tests/invalid/purity_nonsense.err_exp:
> tests/invalid/purity_nonsense.m:
> tests/invalid/purity/Mmakefile:
> tests/invalid/purity/impure_func_t2.err_exp:
> tests/invalid/purity/impure_func_t2.m:
> tests/invalid/purity/impure_func_t3.err_exp:
> tests/invalid/purity/impure_func_t3.m:
> tests/invalid/purity/impure_func_t4.err_exp:
> tests/invalid/purity/impure_func_t4.m:
> tests/invalid/purity/impure_func_t5.err_exp:
> tests/invalid/purity/impure_func_t5.m:
> tests/invalid/purity/impure_pred_t1.err_exp:
> tests/invalid/purity/impure_pred_t1.m:
> tests/invalid/purity/impure_pred_t2.err_exp:
> tests/invalid/purity/impure_pred_t2.m:
> tests/invalid/purity/purity.err_exp:
> tests/invalid/purity/purity.m:
> tests/invalid/purity/purity_nonsense.err_exp:
> tests/invalid/purity/purity_nonsense.m:
> tests/invalid/purity/runtests:
> 	Remove purity tests from the invalid directory, give it a
> 	sub-directory of its own.

> Index: compiler/prog_io_dcg.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/prog_io_dcg.m,v
> retrieving revision 1.14
> diff -u -r1.14 prog_io_dcg.m
> --- compiler/prog_io_dcg.m	2000/01/13 06:16:56	1.14
> +++ compiler/prog_io_dcg.m	2000/03/09 12:26:24

>  parse_dcg_goal_2("=", [A0], Context, VarSet, N, Var, Goal, VarSet, N, Var) :-
>  	term__coerce(A0, A),
> -	Goal = unify(A, term__variable(Var)) - Context.
> +	Goal = unify(A, term__variable(Var), pure) - Context.
>  
>  	% Call to ':='/1 - unify argument with DCG output arg.
>  parse_dcg_goal_2(":=", [A0], Context, VarSet0, N0, _Var0,
>  		Goal, VarSet, N, Var) :-
>  	new_dcg_var(VarSet0, N0, VarSet, N, Var),
>  	term__coerce(A0, A),
> -	Goal = unify(A, term__variable(Var)) - Context.
> +	Goal = unify(A, term__variable(Var), pure) - Context.

It would be nice to eventually be able to have dcg goals of the form
	...
	impure =(an_impure_function(...))
	...
or
	...
	impure :=(an_impure_function(...))
	...

> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/purity.m,v
> retrieving revision 1.23
> diff -u -r1.23 purity.m
> --- compiler/purity.m	2000/03/27 05:07:49	1.23
> +++ compiler/purity.m	2000/04/04 08:19:13

> +	; { PurityCheckResult = no_impure_in_closure },
> +			% We catch this error at the creation of the closure
> +			% It might also make sense to flag missing
> +			% impurity declarations inside closures, but we
> +			% don't do so currently.
> +		{ NumErrors = NumErrors0 }

Do you mean that we don't give an error for a call to an impure pred without
an `impure' annotation inside a closure? If so, you should mark that with
an XXX at least.

> +:- pred check_higher_order_purity(module_info, pred_info,
> +	hlds_goal_info, cons_id, prog_var, list(prog_var),
> +	int, int, purity, io__state, io__state).
> +:- mode check_higher_order_purity(in, in, in, in, in, in, in, out, out, 
> +	di, uo) is det.
> +check_higher_order_purity(ModuleInfo, PredInfo, GoalInfo, ConsId, Var, Args,
> +	NumErrors0, NumErrors, ActualPurity) -->
> +	{ pred_info_clauses_info(PredInfo, ClausesInfo) },
> +	{ clauses_info_vartypes(ClausesInfo, VarTypes) },
> +	{ map__lookup(VarTypes, Var, TypeOfVar) },
> +	( 
> +		{ ConsId = cons(PName, _) },
> +		{ type_is_higher_order(TypeOfVar, PredOrFunc,
> +			_EvalMethod, VarArgTypes) }
> +	->
> +		{ pred_info_typevarset(PredInfo, TVarSet) },
> +		{ map__apply_to_list(Args, VarTypes, ArgTypes0) },
> +		{ list__append(ArgTypes0, VarArgTypes, PredArgTypes) },
> +		( 
> +			{ get_pred_id(PName, PredOrFunc, TVarSet, PredArgTypes,
> +				ModuleInfo, CalleePredId) }
> +		->
> +			{ module_info_pred_info(ModuleInfo,
> +				CalleePredId, CalleePredInfo) },
> +			{ pred_info_get_purity(CalleePredInfo, Purity) },
> +			( { Purity = pure } ->
> +				{ NumErrors = NumErrors0 }
> +			;
> +				{ goal_info_get_context(GoalInfo, CallContext) },
> +				error_missing_body_impurity_decl(ModuleInfo,
> +					CalleePredInfo, CalleePredId,
> +					CallContext, Purity),
> +				{ NumErrors is NumErrors0 + 1 }
> +			)
> +		;
> +			{ goal_info_get_context(GoalInfo, CallContext) },
> +			error_unknown_predicate(CallContext),
> +			{ Purity = pure },
> +			{ NumErrors is NumErrors0 + 1 }

Doesn't this else case correspond to unresolved overloading, and therefore
wouldn't this error be reported elsewhere?

> +:- pred error_unknown_predicate(prog_context, io__state, io__state).
> +:- mode error_unknown_predicate(in, di, uo) is det.
> +
> +error_unknown_predicate(Context) -->
> +	prog_out__write_context(Context),
> +	io__write_string("Unable to purity check this unification.\n"),
> +	prog_out__write_context(Context),
> +	io__write_string("  The purity of the higher order term is unknown.\n"),
> +	prog_out__write_context(Context),
> +	io__write_string("  This can occur if type inference fails.\n"),
> +	prog_out__write_context(Context),
> +	io__write_string("  You should declare the types explicitly.\n").






> @@ -5372,13 +5379,15 @@
>  input/output) without taking an io__state (@pxref{Types}) as input and
>  returning one as output, and do not make any changes to any data
>  structure that will not be undone on backtracking (unless the data
> -structure would be unreachable on backtracking).  The behaviour of other
> -predicates is never affected by the invocation of pure predicates, nor
> -is the behaviour of pure predicates ever affected by the invocation of
> -other predicates.
> +structure would be unreachable on backtracking).  The behaviour of pure
> +predicates is never affected by the invocation of pure predicates.
> +It is possible for the invocation of pure predicate to affect the
> +behaviour of non-pure predicates and vice versa.

The last sentence sounds a little fishy to me. Surely the invocation of
something pure can't affect the behaviour of anything.

There's also a typo: s/of pure predicate/of pure predicates/

> +The compiler should issue a warning if the declared purity of a goal is
> +less pure than its inferred purity.

I'm not sure that the language reference manual should talk about what warnings
the compiler should be expected to produce. (Unless there is a precedent
elsewhere in the manual that I wasn't aware of).

> @@ -5476,11 +5525,23 @@
>  
>  @node Promising purity
>  @section Promising that a predicate is pure
> +
> +Predicates that are implemented in terms of impure or semipure predicates are
> +assumed to have the @emph{worst impurity} 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).

Ditto.

> Index: tests/invalid/purity/impure_pred_t2.m
> ===================================================================
> RCS file: impure_pred_t2.m
> diff -N impure_pred_t2.m
> --- /dev/null	Thu Mar  4 04:20:11 1999
> +++ impure_pred_t2.m	Sun Mar 26 17:55:34 2000
> @@ -0,0 +1,31 @@
> +
> +% Subverting the Mercury purity system.
> +
> +% This should not be possible.
> +
> +:- module impure_pred_t2.
> +
> +:- interface.
> +
> +:- import_module io.
> +
> +:- pred main(state::di, state::uo) is det.
> +
> +:- implementation.
> +:- import_module int, require, list.
> +
> +:- type foo ---> foo(pred(int,int)).

That type decl is unused.

> +
> +main -->
> +	{ Y = get_counter },
> +	{ Y(4, Z) },
> +	print("X = "), 
> +	print(Z), 
> +	nl.
> +
> +:- impure pred get_counter(int::in, int::out) is det.
> +
> +:- pragma c_header_code("extern Integer counter;").
> +:- pragma c_code("Integer counter = 0;").
> +:- pragma c_code(get_counter(Y::in, X::out), will_not_call_mercury, "X = counter + Y;").
> +

> ===================================================================
> RCS file: purity_nonsense.err_exp
> diff -N purity_nonsense.err_exp
> --- /dev/null	Thu Mar  4 04:20:11 1999
> +++ purity_nonsense.err_exp	Wed Nov 10 09:40:13 1999
> @@ -0,0 +1,47 @@

This test case no longer looks right...

> +purity_nonsense.m:003: Error: invalid impurity declaration: func undefined_func = foo.
> +purity_nonsense.m:005: Syntax error at token 'type': unexpected token at start of (sub)term.
> +purity_nonsense.m:006: Syntax error at token 'mode': unexpected token at start of (sub)term.
> +purity_nonsense.m:010: Error: `promise_pure' pragma for purity_nonsense:undefined2/0
> +purity_nonsense.m:010:   without corresponding `pred' or `func' declaration.
> +purity_nonsense.m:012: Error: clause for predicate `purity_nonsense:e12/0'
> +purity_nonsense.m:012:   without preceding `pred' declaration.
> +purity_nonsense.m:013: Error: clause for predicate `purity_nonsense:e13/0'
> +purity_nonsense.m:013:   without preceding `pred' declaration.
> +purity_nonsense.m:018: Warning: unnecessary `impure' marker.
> +purity_nonsense.m:018:   Higher-order goals are always pure.
> +purity_nonsense.m:008: Error: no clauses for predicate `purity_nonsense:undefined/0'.
> +purity_nonsense.m:012: In clause for predicate `purity_nonsense:e12/0':
> +purity_nonsense.m:012:   in argument 1 of call to predicate `impure/1':
> +purity_nonsense.m:012:   error: the language construct \+/1 should be
> +purity_nonsense.m:012:   used as a goal, not as an expression.
> +purity_nonsense.m:012: In clause for predicate `purity_nonsense:e12/0':
> +purity_nonsense.m:012:   in argument 1 of call to predicate `impure/1':
> +purity_nonsense.m:012:   in argument 1 of functor `\+/1':
> +purity_nonsense.m:012:   error: the language construct impure/1 should be
> +purity_nonsense.m:012:   used as a goal, not as an expression.
> +purity_nonsense.m:012: In clause for predicate `purity_nonsense:e12/0':
> +purity_nonsense.m:012:   in argument 1 of call to predicate `impure/1':
> +purity_nonsense.m:012:   in argument 1 of functor `\+/1':
> +purity_nonsense.m:012:   in argument 1 of functor `impure/1':
> +purity_nonsense.m:012:   error: undefined symbol `imp/0'.
> +purity_nonsense.m:012: In clause for predicate `purity_nonsense:e12/0':
> +purity_nonsense.m:012:   error: `impure' marker in an inappropriate place.
> +purity_nonsense.m:013: In clause for predicate `purity_nonsense:e13/0':
> +purity_nonsense.m:013:   in argument 1 of call to predicate `semipure/1':
> +purity_nonsense.m:013:   error: the language construct \+/1 should be
> +purity_nonsense.m:013:   used as a goal, not as an expression.
> +purity_nonsense.m:013: In clause for predicate `purity_nonsense:e13/0':
> +purity_nonsense.m:013:   in argument 1 of call to predicate `semipure/1':
> +purity_nonsense.m:013:   in argument 1 of functor `\+/1':
> +purity_nonsense.m:013:   error: the language construct semipure/1 should be
> +purity_nonsense.m:013:   used as a goal, not as an expression.
> +purity_nonsense.m:013: In clause for predicate `purity_nonsense:e13/0':
> +purity_nonsense.m:013:   in argument 1 of call to predicate `semipure/1':
> +purity_nonsense.m:013:   in argument 1 of functor `\+/1':
> +purity_nonsense.m:013:   in argument 1 of functor `semipure/1':
> +purity_nonsense.m:013:   error: undefined symbol `semi/0'.
> +purity_nonsense.m:013: In clause for predicate `purity_nonsense:e13/0':
> +purity_nonsense.m:013:   error: `semipure' marker in an inappropriate place.
> +purity_nonsense.m:015: In predicate `purity_nonsense:e14/1':
> +purity_nonsense.m:015:   warning: declared `impure' but actually pure.
> +For more information, try recompiling with `-E'.
> Index: tests/invalid/purity/purity_nonsense.m
> ===================================================================
> RCS file: purity_nonsense.m
> diff -N purity_nonsense.m
> --- /dev/null	Thu Mar  4 04:20:11 1999
> +++ purity_nonsense.m	Tue Jan  6 17:31:42 1998
> @@ -0,0 +1,18 @@
> +:- module purity_nonsense.
> +
> +:- impure func undefined_func = foo.		% no impure functions (yet)
> +
> +:- impure type badtype ---> oops.
> +:- impure mode badmode :: free -> free.
> +
> +:- impure pred undefined.
> +:- pragma promise_pure(undefined/0).
> +:- pragma promise_pure(undefined2/0).
> +
> +e12 :- impure (\+ impure imp).
> +e13 :- semipure (\+ semipure semi).
> +
> +:- impure pred e14(pred).
> +:- mode e14(((pred) is semidet)) is semidet.
> +
> +e14(P) :- impure call(P).


dgj
-- 
David Jeffery (dgj at cs.mu.oz.au) | If your thesis is utterly vacuous
PhD student,                    | Use first-order predicate calculus.
Dept. of Comp. Sci. & Soft. Eng.|     With sufficient formality
The University of Melbourne     |     The sheerist banality
Australia                       | Will be hailed by the critics: "Miraculous!"
                                |     -- Anon.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------