[m-dev.] for review: more assertion integration

[Fergus Henderson]

Hi Pete,

Thanks for your work on adding support for assertions.
Here's some review comments.

On 30-Aug-1999, Peter Ross <petdr at cs.mu.OZ.AU> wrote:
> More integration of assertions with the compiler.
> 
> compiler/accumulator.m:
>     Use the new assertion__is_commutative predicate.

There were other changes to that file not mentioned in the log message.

Also, I find log messages more readable if the changes are listed
in a semantically meaningful ordering (e.g. grouping related changes
and making sure that log messages which introduces some new thing
occurs before the log messages which mention the use of that new thing)
rather than alphabetical ordering.

> compiler/assertion.m:
>     Add assertion__is_commutative, which given an assertion_id returns
>     whether or not the assertion is commutative.

What does it mean for an assertion to be commutative?
The standard mathematical definition of "commutative" only makes sense
for binary functions or binary predicates.

Perhaps you meant that the assertion was stating the commutitivity of
a procedure?  If so, the name `assertion__is_commutative' is misleading,
and so I suggest you use something else, e.g. perhaps
`assertion__is_comutativity_assertion'.

>     Add assertion__check_exported, which ensures that an assertion which
>     is defined in the interface only refers to constructors, functions
>     and predicates defined in that interface.

I thought we agreed that we'd allow assertions in the interface to refer
to anything that is imported into the interface, not only just stuff
that is defined in that interface?

> compiler/dead_proc_elim.m:
>     Don't eliminate the clauses for assertions.

Why not?  The log message should state the rationale.

> compiler/goal_util.m:
>     Add the mode (in, out) to goal_calls_pred_id.

Why?  The log message should state the rationale.

Also I suggest s/(in, out)/`(in, out) is nondet'/

> compiler/hlds_data.m:
>     Add assertion_table_pred_ids, which returns all the predids of every
>     assertion.
> 
> compiler/hlds_out.m:
>     Add hlds_out__write_assertion, which will write an assertion.

Again, the log message should state the rationale for both of these.
It could be as simple as "for use by such-and-such".

It would be a good idea to add code to hlds_out.m so that it dumps
out the assertion table.

> compiler/intermod.m:
>     Ensure that assertions defined in the interface, get written out to
>     the .opt file.

s/,//

> compiler/make_hlds.m:
>     When adding an assertion add an implicit pred declaration.

Why?

> compiler/modules.m:
>     Discard assertions so that they are not written out in interface files.

You should be more specific about where/when assertions are discarded.

> compiler/polymorphism.m:
>     Remove assertions from futher processing after the polymorphism
>     pass.
>
> compiler/post_typecheck.m:
> compiler/purity.m:
>     Don't remove assertions after typechecking as polymorphism needs to
>     be run to allow the difference between functions and data
>     constructors to be resolved.

It would probably be better to change those three modules so that
function overloading was resolved by post_typecheck.m rather than
by polymorphism.m.

Also s/futher/further/

> compiler/notes/compiler_design.html:
>     Move the documentation on assertions to after the documentation on
>     polymorphism.

Why?  Please state the rationale.

> Index: accumulator.m
...
>  	%
> +	% commutative_assertion
> +	%
> +	% Does there exist one (and only one) commutative assertion for the 
> +	% current predicate.
> +	% The and only one condition is required because we currently
> +	% don't handle the case of predicates which have individual
> +	% parts which are commutative, because then we don't know which
> +	% variable is descended from which.
> +	%
> +:- pred commutative_assertion(list(assert_id)::in, module_info::in,
> +		prog_vars::in, set(prog_var)::out) is semidet.
> +
> +commutative_assertion([AssertId | AssertIds], ModuleInfo, Args0,
> +		PossibleStaticVars) :-
> +	(
> +		assertion__is_commutative(AssertId, ModuleInfo, Args0,
> +				PossibleStaticVars0)
> +	->
> +		\+ commutative_assertion(AssertIds, ModuleInfo, Args0, _),
> +		PossibleStaticVars = set__list_to_set(PossibleStaticVars0)
> +	;
> +		commutative_assertion(AssertIds, ModuleInfo, Args0,
> +				PossibleStaticVars)
> +	).

I think s/commutative/commutativity/g here would make more sense.

> +
> +	%
> +	% check_modes(Vs, CVs, Ms, MI)
> +	%
> +	% Given a list of variables, Vs, and associated modes, Ms, make
> +	% sure that each variable that is commutative (member of CVs)
> +	% has a mode where the instantiatedness of the the variable
> +	% doesn't change (ie an in mode).

I don't think it makes sense to talk about a "commutative variable".

>  :- pred assoc_fact(module_name::in, string::in, arity::in,
>  		list(mode)::in, module_info::in, prog_vars::in,
> -		prog_vars::out, set(prog_var)::out, bool::out) is semidet.
> -
> -assoc_fact(unqualified("int"), "+", 3, [In, In, Out], ModuleInfo, 
> -		[A, B, C], [A, B, C], PossibleStaticVars, no) :-
> -	set__list_to_set([A, B], PossibleStaticVars),
> -	mode_is_input(ModuleInfo, In),
> -	mode_is_output(ModuleInfo, Out).
> -
> -assoc_fact(unqualified("int"), "*", 3, [In, In, Out], ModuleInfo, 
> -		[A, B, C], [A, B, C], PossibleStaticVars, no) :-
> -	set__list_to_set([A, B], PossibleStaticVars),
> -	mode_is_input(ModuleInfo, In),
> -	mode_is_output(ModuleInfo, Out).

That change was not mentioned in the log message.

> +++ assertion.m	1999/07/30 07:27:43
...
> @@ -36,15 +37,91 @@
>  :- pred assertion__record_preds_used_in(hlds_goal::in, assert_id::in,
>  		module_info::in, module_info::out) is det.
>  
> +	% 
> +	% assertion__is_commutative(Id, MI, Vs, CVs)
> +	%
> +	% Does the assertion represented by the assertion id, Id,
> +	% represent a commutative pred/func?

s/represent a commutative/state the commutativity of a/

Also, I suggest you add something along the lines of "We extend the usual
definition of commutativity to apply to predicates or functions with more
than two arguments as follows: [... give definition here ...]".

> +	% If so, CVs, returns the two variables which can be swapped in
> +	% order if it was a call to Vs.

s/CVs, returns/returns (in CVs)/

If CVs is always of length exactly two, then its type should be
`pair(prog_var)' rather than `list(prog_var)'.

> +:- pred implies(hlds_goal::in, hlds_goal::out, hlds_goal::out) is semidet.
>  
> +implies(Goal, P, Q) :-
> +		% Goal = P => Q

s/P => Q/(P => Q)/

> +:- pred equal_unification(unify_rhs::in, unify_rhs::in, subst::in,
> +		subst::out) is semidet.
>  
> +equal_unification(var(A), var(B), Subst0, Subst) :-
> +	equal_vars([A], [B], Subst0, Subst).
> +equal_unification(functor(ConsId, VarsA), functor(ConsId, VarsB),
> +		Subst0, Subst) :-
> +	equal_vars(VarsA, VarsB, Subst0, Subst).

You should handle the `lambda_goal' case here.

> +:- pred write_error_message(prog_context::in,
> +		pred_or_func::in, sym_name::in, arity::in,
> +		module_specifier::in, io__state::di, io__state::uo) is det.
> +
> +write_error_message(Context, PredOrFunc, SymName, Arity, ModSpec) -->
> +	prog_out__write_context(Context),
> +	io__write_string("Error: "),
> +	hlds_out__write_simple_call_id(PredOrFunc, SymName, Arity),
> +	io__write_string(" in an assertion which is in an interface\n"),
> +	prog_out__write_context(Context),
> +	io__write_string("  and not an exported "),
> +	hlds_out__write_pred_or_func(PredOrFunc),
> +	io__write_string(" of the module `"),
> +	prog_out__write_sym_name(ModSpec),
> +	io__write_string("'\n").

The name `write_error_message' is very generic.  I think you should name
this predicate something which indicates what kind of error it is reporting.

I think the error message

	Error: function `foo' in an assertion which is in an interface
	  and not an exported function of the module `bar'

is not very clear at all.  Perhaps you mean `is not' rather than `and not'?
Also, the error message should end in a full stop.
And I suggest using "the interface" rather than "an interface".

Even with these changes, I think the message

	Error: function `foo' in an assertion which is in the interface
	  and not an exported function of the module `bar'

is still not very clear.

I think

	In interface for module `bar':
	  error: exported assertion refers to function `foo'
	  which is not defined in the interface of module `bar'.

would be a bit clearer.

Also you should give a more detailed explanation if `--verbose-errors'
is specified.


> +:- pred write_error_message(prog_context::in, cons_id::in,
> +		module_specifier::in, io__state::di, io__state::uo) is det.
>
> +write_error_message(Context, ConsId, ModSpec) -->
> +	prog_out__write_context(Context),
> +	io__write_string("Error: Constructor `"),
> +	hlds_out__write_cons_id(ConsId),
> +	io__write_string("' in an assertion in the interface section\n"),
> +	prog_out__write_context(Context),
> +	io__write_string("  which is not module qualified with `"),
> +	prog_out__write_sym_name(ModSpec),
> +	io__write_string("'\n").

The same comments apply here.

s/Constructor/constructor/

The error message here should be the same as the one for functions or
predicates -- the only difference is that it should use `constructor'
rather than `function' or `predicate'.

> Index: hlds_out.m
> @@ -846,6 +871,7 @@
>  	},
>  	globals__io_lookup_string_option(dump_hlds_options, Verbose),
>  	( { string__contains_char(Verbose, 'm') } ->
> +		hlds_out__write_indent(Indent),
>  		hlds_out__write_indent(Indent),
>  		io__write_string("% Modes for which this clause applies: "),
>  		{ list__map(lambda([Mode :: in, ModeInt :: out] is det,

That change looks like a bug.

> Index: intermod.m
> ===================================================================
> RCS file: /home/staff/zs/imp/mercury/compiler/intermod.m,v
> retrieving revision 1.68
> diff -u -r1.68 intermod.m
> --- intermod.m	1999/08/26 03:11:49	1.68
> +++ intermod.m	1999/08/27 05:51:27
> @@ -91,7 +91,11 @@
>  		{ ModuleInfo = ModuleInfo0 }
>  	;
>  		{ Result2 = ok },
> -		{ module_info_predids(ModuleInfo0, PredIds) },
> +		{ module_info_predids(ModuleInfo0, RealPredIds) },
> +		{ module_info_assertion_table(ModuleInfo0, AssertionTable) },
> +		{ assertion_table_pred_ids(AssertionTable, AssertPredIds) },
> +		{ list__append(AssertPredIds, RealPredIds, PredIds0) },
> +		{ list__reverse(PredIds0, PredIds) },

You should explain the call to list__reverse here.

> +:- pred intermod__should_be_processed(pred_id::in, pred_info::in,
> +		set(pred_id)::in, int::in, bool::in,
> +		module_info::in) is semidet.
> +
> +intermod__should_be_processed(PredId, PredInfo, TypeSpecForcePreds,
> +		InlineThreshold, Deforestation, ModuleInfo) :-
> +	%
> +	% note: we can't include exported_to_submodules predicates in
> +	% the `.opt' file, for reasons explained in the comments for
> +	% intermod_info_add_proc
> +	%
> +	pred_info_is_exported(PredInfo),
> +	(
...
> +	;
> +		pred_info_get_goal_type(PredInfo, assertion)
> +
> +	).

The blank line here is unnecessary.
Also I think it would be a good idea to add a comment
"% assertions should always get included in the `.opt' file."
or something like that before the call to
`pred_info_get_goal_type(PredInfo, assertion)' here.

> +++ make_hlds.m	1999/08/27 07:39:38
> @@ -695,9 +695,22 @@
>  		{ Info = Info0 }	
>  	).
>  add_item_clause(assertion(Goal0, VarSet),
> -		Status, Status, Context, Module0, Module, Info0, Info) -->
> +		Status0, Status, Context, Module0, Module, Info0, Info) -->
>  
>  		%
> +		% If the assertion is imported, we need to change it to
> +		% opt_imported so that type and purity checking, and
> +		% polymorphism get run on it.
> +		%
> +	(
> +		{ Status0 = imported }
> +	->
> +		{ Status = opt_imported }
> +	;
> +		{ Status = Status0 }
> +	),
> +
> +		%

That change was not mentioned in the log message.

...
> @@ -4388,8 +4447,6 @@
>  		Goal, VarSet, Warnings, Module0, Module, Info0, Info) -->
>  	transform_goal(Body, VarSet0, Subst, Goal1, VarSet1, Info0, Info1),
>  	{ term__apply_substitution_to_list(Args0, Subst, Args) },
> -	insert_arg_unifications(HeadVars, Args, Context, head, no,
> -		Goal1, VarSet1, Goal2, VarSet2, Info1, Info),
>  	{ map__init(Empty) },
>  		
>  		%
> @@ -4401,11 +4458,15 @@
>  	(
>  		{ IsAssertion = yes }
>  	->
> -			% Use Goal1, since HeadVar__* not yet introduced.
> -		report_implicit_quant_errs(Goal1, Args, VarSet0,
> -				Context, Module0, Module)
> +		report_implicit_quant_errs(Goal1, Args, VarSet1,
> +				Context, Module0, Module),
> +		{ VarSet2 = VarSet1 },
> +		{ Goal2 = Goal1 },
> +		{ Info = Info0 }
>  	;
> -		{ Module = Module0 }
> +		{ Module = Module0 },
> +		insert_arg_unifications(HeadVars, Args, Context, head, no,
> +			Goal1, VarSet1, Goal2, VarSet2, Info1, Info)
>  	),
>  	{ implicitly_quantify_clause_body(HeadVars, Goal2, VarSet2, Empty,
>  				Goal, VarSet, _, Warnings) }.

That change was not mentioned in the log message.
And at first glance, I don't understand it.
Why did you delete the comment "% Use Goal1, since HeadVar__* not
yet introduced."?

> Index: modules.m
> ===================================================================
> RCS file: /home/staff/zs/imp/mercury/compiler/modules.m,v
> retrieving revision 1.107
> diff -u -r1.107 modules.m
> --- modules.m	1999/08/18 06:26:04	1.107
> +++ modules.m	1999/08/25 07:27:57
> @@ -807,6 +807,10 @@
>  		report_warning("Warning: pragma in module interface.\n"),
>  		check_for_clauses_in_interface(Items0, Items)
>  	;
> +		{ Item0 = assertion(_, _) }
> +	->
> +		check_for_clauses_in_interface(Items0, Items)
> +	;
>  		{ Items = [ItemAndContext0 | Items1] },
>  		check_for_clauses_in_interface(Items0, Items1)
>  	).

If you want to change check_for_clauses_in_interface to also
delete assertions, then you should carefully document that,
both here where they are being removed, and also in documentation
at the top of the predicate which describes what it does.

But it might be a better idea to handle deletion of assertions
in a different predicate rather than by changing the semantics
of one of the existing predicates.

> @@ -844,6 +848,11 @@
>  		; Item0 = pragma(Pragma),
>  		  pragma_allowed_in_interface(Pragma, no)
>  		)
> +	->
> +		split_clauses_and_decls(Items0, ClauseItems1, InterfaceItems),
> +		ClauseItems = [ItemAndContext0 | ClauseItems1]
> +	;
> +		Item0 = assertion(_, _)
>  	->
>  		split_clauses_and_decls(Items0, ClauseItems1, InterfaceItems),
>  		ClauseItems = [ItemAndContext0 | ClauseItems1]

The same comment applies here, only stronger, because I think some of
the callers of split_clauses_and_decls would be broken if you made
this change.

> +	%
> +	% Now that the assertion has finished being typechecked,
> +	% and has had all of its pred_ids identified,
> +	% remove the assertion from the list of pred ids to be processed
> +	% in the future and place the pred_info associated with the
> +	% assertion into the assertion table.
> +	% Also record for each predicate that is used in an assertion
> +	% which assertion it is used in.
> +	% 
> +:- pred polymorphism__finish_assertion(module_info, pred_id,
> +		module_info, io__state, io__state).
> +:- mode polymorphism__finish_assertion(in, in, out, di, uo) is det.
> +
> +polymorphism__finish_assertion(Module0, PredId, Module) -->
> +		% store into assertion table.
> +	{ module_info_assertion_table(Module0, AssertTable0) },
> +	{ assertion_table_add_assertion(PredId,
> +			AssertTable0, Id, AssertTable) },
> +	{ module_info_set_assertion_table(Module0, AssertTable, Module1) },
> +		
> +		% Remove from further processing.
> +	{ module_info_remove_predid(Module1, PredId, Module2) },
> +
> +	{ module_info_pred_info(Module2, PredId, PredInfo) },
> +	{ assertion__goal(Id, Module2, Goal) },
> +	(
> +		{ pred_info_is_exported(PredInfo) }
> +	->
> +		{ module_info_name(Module2, ModSpec) },
> +		assertion__check_exported(Goal, Module2, ModSpec)
> +	;
> +		[]
> +	),
> +
> +		% record which predicates are used in assertions
> +	{ assertion__record_preds_used_in(Goal, Id, Module2, Module) }.

You should document the group of 10 lines of code that calls
assertion__check_exported, both with a comment immediately preceding it,
and also with a comment in the documentation at the top of the predicate.

Also I suggest s/Id/AssertionId/g.

> Index: notes/compiler_design.html
> ===================================================================
> RCS file: /home/staff/zs/imp/mercury/compiler/notes/compiler_design.html,v
> retrieving revision 1.35
> diff -u -r1.35 compiler_design.html
> --- compiler_design.html	1999/08/05 11:57:42	1.35
> +++ compiler_design.html	1999/08/17 06:01:18
...
> @@ -307,15 +305,6 @@
>  	  It also removes assertions from further processing.
>  	</ul>

That comment above, relating to post_typecheck.m, is no longer true
after your change; it should be moved.

----------

This will need another round of reviewing, IMHO.

Cheers,
	Fergus.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------