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

[Peter Ross]

Just to address some of your comments directly.

On 08-Jul-1999, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> On 08-Jul-1999, Peter Ross <petdr at cs.mu.OZ.AU> wrote:
> > +	% 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?
> 

It is now done on the HLDS, I didn't realise that the predicate existed.

> > +	%
> > +	% 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?
> 
Even better, put it in post_typecheck


> > 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.
> 
Who reads the documentation! ;)

> > @@ -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?
> 
To get rid of a bogus error message, however I can't seem to regenerate
that message, so maybe it was all just a figment of my imagination.

> > @@ -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 ;-)
> 
So did I that is why I almost deleted all my additions and the full stop
for full measure.

> > 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.
> 
I call post_typecheck__finish_assertion, which has the body
from remove_assertion_from_further_processing.

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