[m-dev.] for review: add parsing/storing of assertions

[Fergus Henderson]

On 08-Jul-1999, Peter Ross <petdr at cs.mu.OZ.AU> wrote:
> This is for DJ to review.

Hope you don't mind if I take a shot at it first...

> Add the infrastructure for assertions into the compiler.
> 
> compiler/check_assertion.m:
>     Module that ensures that the form of an assertion is syntactically valid.

You should document this module in compiler/notes/compiler_design.html.

...
> compiler/make_hlds.m:
>     Transform the assertion to a HLDS data structure that can be
>     typechecked.

Does make_hlds.m invoke the check_assertion module?
If so, it would be helpful if the log message, the comments
at the top of check_assertion, and the documentation that you
will add to compiler/notes/compiler_design.html all made this clear.
Also, it would be helpful to document which data structure
check_assertion acts on (i.e. is it the parse tree, or the HLDS?)

> compiler/post_typecheck.m:
>     Add to comments about what happens when typechecking assertions.

s/Add to comments/Add comments/ ?

> compiler/prog_data.m:
>     Add assertion to the type goal_expr.

Didn't you add it to the type `item', not the type `goal_expr'?

> compiler/accumulator.m:
>     A minor code reordering.

That change looks unrelated; I suggest you commit it separately.

check_assertion.m:
> +:- pred check_assertion(goal::in, prog_varset::in, goal::out,
> +		list(prog_term)::out, module_info::in, module_info::out,
> +		io__state::di, io__state::uo) is det.

You should document the meaning of this predicate's arguments.

> +	%
> +	% check_assertion
> +	%
> +	% An assertion is valid, iff the assertion begins with the
> +	% universally quantified variables and each variable is
> +	% explicitly quantified before its use.  At a later date these
> +	% restrictions should be relaxed, once we work out how to
> +	% correctly implicitly quantify the assertions.
> +	%
> +check_assertion(Goal, VarSet, NewGoal, HeadVars, Module0, Module) -->
> +	(
> +		{ Goal = all(Vars, AllGoal) - _Context }
> +	->
> +		{ term__var_list_to_term_list(Vars, HeadVars) },
> +		{ NewGoal = AllGoal },
> +		{ set__list_to_set(Vars, InitialVarSet) },
> +		check_assertion_quantification(AllGoal, InitialVarSet, VarSet,
> +				Module0, Module)
> +	;
> +		{ HeadVars = [] },
> +		{ NewGoal = true - Context },
> +		{ Goal = _ - Context },
> +		prog_out__write_context(Context),
> +		io__write_string("Error: assertion doesn't begin with a universal quantifier\n"),
> +		{ module_info_incr_errors(Module0, Module) },
> +		globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
> +		( { VerboseErrors = yes } ->
> +			prog_out__write_context(Context),
> +			io__write_string("Maybe you want all []\n")
> +		;
> +			[]
> +		)
> +	).

s/want all []/want `all []'./
                   ^      ^^

I don't completely understand the rationale for requiring all assertions
to begin with a universal quantifier.  If the assertion contains
no variables (e.g. `:- assertion (pi > 3.0, pi < 4.0).'), then
I don't see what benefit there is in requiring the user to insert
a meaningless `all []' quantifier.  If the assertion does contain
variables, then check_assertion_quantification will check that they
are all explicitly quantified, so I don't see the need for this
additional check here.

> +	% Make sure that each variable is explicitly quantified.
> +:- pred check_assertion_quantification(goal::in, set(prog_var)::in,
> +		prog_varset::in, module_info::in, module_info::out,
> +		io__state::di, io__state::uo) is det.
> +
> +check_assertion_quantification(true - _, _, _, Module, Module) --> [].
> +check_assertion_quantification(fail - _, _, _, Module, Module) --> [].
> +check_assertion_quantification(unify(LHS, RHS) - Context, Quantified, VarSet,
> +		Module0, Module) -->
> +	{ term__vars_list([LHS, RHS], Vars) },
> +	check_assertion__atomic(Vars, Context, VarSet, Quantified,
> +			Module0, Module).
...

It would be much simpler to check the quantification if you did this
check on the HLDS rather than on the parse tree; then you could just
use quantification__goal_vars/2 to find all the unquantified variables.
Is there any particular reason why the check needs to be done on the
parse tree rather than the HLDS?

(If so, it would be helpful to explain that in the documentation
for this module.)

> +++ hlds_data.m	1999/07/07 06:52:08
...
> +	%
> +	% A table that records all the assertions in the system.
> +	% 
> +:- type assert_id.
> +:- type assertion_table.

It would be helpful here to include a pointer to some documentation
which explains what "assertions" are.  Note that assertions in
Mercury are very different to assert in Prolog!  Some readers
might find this confusing.  In fact, it would also be helpful
to add an entry for "assertion" in compiler/notes/glossary.html.

> +	%
> +	% After typechecking is finished the pred_info describing the
> +	% assertion should be removed from further processing and the
> +	% pred_id which describes the assertion stored in the
> +	% assertion_table.
> +	%
> +:- pred remove_assertion_from_further_processing(pred_id::in,
> +		module_info::in, module_info::out) is det.

I think it might make more sense to put that in hlds_module.m
rather than hlds_data.m.  What do you think?

> +assertion_table_add_assertion(Assertion, AssertionTable0, AssertionTable) :-
> +	AssertionTable0 = assertion_table(Id, AssertionMap0),
> +	map__det_insert(AssertionMap0, Id, Assertion, AssertionMap),
> +	AssertionTable = assertion_table(Id+1, AssertionMap).

s/Id+1/Id + 1/

> Index: hlds_out.m
> ===================================================================
> RCS file: /home/staff/zs/imp/mercury/compiler/hlds_out.m,v
> retrieving revision 1.221
> diff -u -r1.221 hlds_out.m
> --- hlds_out.m	1999/06/30 17:12:24	1.221
> +++ hlds_out.m	1999/07/07 07:59:25
> @@ -299,6 +299,10 @@
>  	->
>  		io__write_string("type class method implementation")
>  	;
> +		{ pred_info_get_goal_type(PredInfo, assertion) }
> +	->
> +		io__write_string("the assertion")
> +	;

As the documentation for that predicate says:

        % The code of this predicate duplicates the functionality of
        % term_errors__describe_one_pred_name. Changes here should be made
        % there as well.

Also, I think you should probably just write "assertion" rather than
"the assertion".

> +++ hlds_pred.m	1999/07/07 15:37:21
> @@ -179,6 +179,7 @@
>  
>  :- type goal_type 	--->	pragmas		% pragma c_code(...)
>  			;	clauses		
> +			;	{ assertion }
>  			;	none.

I presume the reason that "assertion" is in braces here is because it
is an operator?  If so, I suggest you use "(assertion)" rather than
"{ assertion }", just for consistency with how this issue is dealt with
elsewhere.

> Index: make_hlds.m
...
> +add_item_clause(assertion(Goal0, VarSet),
> +		Status, Status, Context, Module0, Module, Info0, Info) -->
> +	check_assertion(Goal0, VarSet, Goal, HeadVars, Module0, Module1),
> +
> +	{ term__context_line(Context, Line) },
> +	{ term__context_file(Context, File) },
> +	{ string__format("assertion__%d__%s", [i(Line), s(File)], Name) },
> +
> +	module_add_pred_clause(Module1, VarSet, unqualified(Name),
> +			HeadVars, Goal, Status, Context, yes, Module,
> +			Info0, Info).
> +

A comment here would be helpful.

Also it would be clearer if you wrote

	IsAssertion = yes,
	module_add_pred_clause(Module1, VarSet, unqualified(Name),
			HeadVars, Goal, Status, Context, IsAssertion, Module,
			Info0, Info).

>  module_add_pred_clause(ModuleInfo0, ClauseVarSet, PredName, Args, Body,
> -			Status, Context, ModuleInfo, Info0, Info) -->
> +			Status, Context, Assertion, ModuleInfo, Info0, Info) -->

I think that "IsAssertion" would be a clearer variable name than
"Assertion" here.  It makes it more immediately obvious that this
field is a boolean rather than some representation of the assertion itself.

(The same comment applies to a number of places within this module.)

> @@ -2810,7 +2852,7 @@
>  		module_info_set_predicate_table(ModuleInfo0, PredicateTable,
>  			ModuleInfo)
>  		},
> -		( { Status \= opt_imported } ->
> +		( { Status \= opt_imported, Assertion = no } ->
>  			% warn about singleton variables 
>  			maybe_warn_singletons(VarSet,
>  				PredOrFunc - PredName/Arity, ModuleInfo, Goal),

Why don't you want to warn about singleton variables in assertions?

> @@ -5355,7 +5397,7 @@
>  
>  % This is not considered an unconditional error anymore:
>  % if there is no :- pred declaration, we just infer one,
> -% unless the `--no-infer-types' option was specified.
> +% unless the `--no-infer-types' option was specified

I preferred it the previous way ;-)

> +++ mercury_to_mercury.m	1999/07/08 00:46:16
> @@ -422,6 +422,14 @@
>  			"check_termination")
>  	).
>  
> +mercury_output_item(assertion(Goal, VarSet), _) -->
> +	io__write_string(":- assertion "),
> +	{ Indent = 1 },
> +	mercury_output_newline(Indent),
> +	mercury_output_goal(Goal, VarSet, Indent, yes),
> +	io__write_string("."),
> +	io__nl.

Might as well just do `io__write_string(".\n").', IMHO.

> -:- pred mercury_output_goal(goal, prog_varset, int, io__state, io__state).
> -:- mode mercury_output_goal(in, in, in, di, uo) is det.
> +:- pred mercury_output_goal(goal, prog_varset, int, bool, io__state, io__state).
> +:- mode mercury_output_goal(in, in, in, in, di, uo) is det.
...
>  	% Implication and equivalence should have been transformed out
> -	% by now
> -mercury_output_goal_2(implies(_G1,_G2), _VarSet, _Indent) -->
> +	% by now, unless they are in an assertion.
> +mercury_output_goal_2(implies(_G1,_G2), _VarSet, _Indent, no) -->
>  	{ error("mercury_to_mercury: implies/2 in mercury_output_goal")}.
> +mercury_output_goal_2(implies(G1,G2), VarSet, Indent, yes) -->
> +	{ Indent1 is Indent + 1 },
> +	io__write_string("("),
> +	mercury_output_newline(Indent1),
> +	mercury_output_goal(G1, VarSet, Indent1, yes),
> +	mercury_output_newline(Indent),
> +	io__write_string("=>"),
> +	mercury_output_newline(Indent1),
> +	mercury_output_goal(G2, VarSet, Indent1, yes),
> +	mercury_output_newline(Indent),
> +	io__write_string(")").

I don't think it is worthwhile adding the boolean `InAssertion' argument
to mercury_output_goal, if the only reason to add it is to allow you to
call error/1 -- the call to error/1 there wasn't put there for the
purposes of internal consistency checking, it was just put in there
to minimize the amount of stuff that we needed to implement. 
In other words, the condition which the call to error/1 is checking is
an incidental condition that happened to be true and which we therefore
took advantage of, not an important consistency requirement that we
need to check.

mercury_to_mercury.m:
>  mercury_unary_prefix_op("?-").
>  mercury_unary_prefix_op("\\").
>  mercury_unary_prefix_op("\\+").
> +mercury_unary_prefix_op("assertion").
>  mercury_unary_prefix_op("delete").
>  mercury_unary_prefix_op("dynamic").
>  mercury_unary_prefix_op("end_module").

You also need to add the operator to library/ops.m and to
doc/transition_guide.texi.

> Index: prog_io_assertion.m
> ===================================================================
> RCS file: prog_io_assertion.m
> diff -N prog_io_assertion.m
> --- /dev/null	Thu Jul  8 11:01:06 1999
> +++ prog_io_assertion.m	Wed Jun 30 17:19:33 1999
> @@ -0,0 +1,31 @@
> +%-----------------------------------------------------------------------------%
> +% Copyright (C) 1996-1999 The University of Melbourne.
> +% This file may only be copied under the terms of the GNU General
> +% Public License - see the file COPYING in the Mercury distribution.
> +%-----------------------------------------------------------------------------%
> +%
> +% File: prog_io_assertion.m.
> +% Main authors: petdr
> +%
> +% This module handles the parsing of assertion directives.
> +
> +:- module prog_io_assertion.
> +
> +:- interface.
> +
> +:- import_module prog_data, prog_io_util.
> +:- import_module list, varset, term.
> +
> +	% parse the assertion declaration. 
> +:- pred parse_assertion(module_name, varset, list(term), maybe1(item)).
> +:- mode parse_assertion(in, in, in, out) is semidet.
> +
> +:- implementation.
> +
> +:- import_module prog_io, prog_io_goal.
> +:- import_module term_util, term_errors.
> +
> +parse_assertion(_ModuleName, VarSet, [AssertionTerm], Result) :-
> +	varset__coerce(VarSet, ProgVarSet),
> +	parse_goal(AssertionTerm, ProgVarSet, AssertGoal, AssertVarSet),
> +	Result = ok(assertion(AssertGoal, AssertVarSet)).

I don't think it is worth adding a new module for one 4-line predicate.
I suggest you just define this predicate in prog_io.m rather than
adding a new module.

> compiler/purity.m:
>     After finished typechecking assertions, remove the assertions from
>     further processing.

> Index: purity.m
> ===================================================================
> RCS file: /home/staff/zs/imp/mercury/compiler/purity.m,v
> retrieving revision 1.14
> diff -u -r1.14 purity.m
> --- purity.m	1999/06/30 17:12:38	1.14
> +++ purity.m	1999/07/06 06:38:03
> @@ -290,7 +290,15 @@
>  	{ predicate_table_set_preds(PredTable0, Preds, PredTable) },
>  	{ module_info_set_predicate_table(ModuleInfo0, PredTable,
>  					  ModuleInfo1) },
> -	check_preds_purity_2(PredIds, FoundTypeError, ModuleInfo1, ModuleInfo,
> +
> +	(
> +		{ pred_info_get_goal_type(PredInfo0, assertion) }
> +	->
> +		{ module_info_remove_predid(ModuleInfo1, PredId, ModuleInfo2) }
> +	;
> +		{ ModuleInfo2 = ModuleInfo1 }
> +	),
> +	check_preds_purity_2(PredIds, FoundTypeError, ModuleInfo2, ModuleInfo,
>  				  NumErrors1, NumErrors).

Shouldn't you call `remove_assertion_from_further_processing'
rather than `module_info_remove_predid' here?

BTW, perhaps `remove_assertion_from_further_processing' would be
better named `move_assertion_to_assertion_table', since it doesn't
just call module_info_remove_predid, it also adds the pred to the
assertion table.

It's kind of a pity that this code has to go in purity.m rather than
post_typecheck.m.  Even though this code fragment is small, it might
be worth making it into a separate procedure in post_typecheck.m
and then calling it from purity.m.  This would keeps the conceptual
separation between post_typecheck.m and purity.m clearer, and make
it clearer that this code fragment is part of the post_typecheck phase
rather than being something related to purity analysis.

Apart from that, this change looks fine.  It would be good to see both
a relative diff and a complete diff when you've addressed those issues.

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