[m-dev.] for review: assertions in the interface

[Fergus Henderson]

On 02-Sep-1999, Peter Ross <petdr at cs.mu.OZ.AU> wrote:
> Extend the assertion system by
>     * handling assertions in the interface of a module differently to
>       those in the implementation.
>     * testing an assertion for the commutivity property.
...
> +assertion__in_interface_check(call(PredId,_,_,_,_,SymName) - GoalInfo,
> +		ModuleInfo) -->
> +	{ module_info_pred_info(ModuleInfo, PredId, PredInfo)  },
> +	(
> +		{ pred_info_import_status(PredInfo, ImportStatus) },
> +		{ \+ is_defined_in_implementation_section(ImportStatus) }
> +	->
> +		[]
> +	;
> +		{ goal_info_get_context(GoalInfo, Context) },
> +		{ pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
> +		{ pred_info_arity(PredInfo, Arity) },
> +		write_assertion_interface_error(Context,
> +				call(PredOrFunc, SymName, Arity), ModuleInfo)
> +	).

I think it would be clearer to move the call to pred_info_import_status
out of the if-then-else.  It would also be clearer, I think, to replace

	( { \+ <Cond> } -> [] ; <Error> )

with
	( { <Cond> } -> <Error> ; [] )

> +assertion__in_interface_check(pragma_c_code(_,PredId,_,_,_,_,_) - GoalInfo,
> +		ModuleInfo) -->
> +	{ module_info_pred_info(ModuleInfo, PredId, PredInfo) },
> +	(
> +		{ pred_info_import_status(PredInfo, ImportStatus) },
> +		{ \+ is_defined_in_implementation_section(ImportStatus) }
> +	->
> +		[]
> +	;
> +		{ goal_info_get_context(GoalInfo, Context) },
> +		{ pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
> +		{ pred_info_name(PredInfo, Name) },
> +		{ SymName = unqualified(Name) },
> +		{ pred_info_arity(PredInfo, Arity) },
> +		write_assertion_interface_error(Context,
> +				call(PredOrFunc, SymName, Arity), ModuleInfo)
> +	).

Likewise.

> +:- pred assertion__in_interface_check_unify_rhs(unify_rhs::in, prog_context::in,
> +		module_info::in, io__state::di, io__state::uo) is det.
> +
> +assertion__in_interface_check_unify_rhs(var(_), _, _) --> [].
> +assertion__in_interface_check_unify_rhs(functor(ConsId, _), Context,
> +		ModuleInfo) -->
> +	{ module_info_ctors(ModuleInfo, ConsTable) },
> +	{ map__lookup(ConsTable, ConsId, Defns) },
> +	(
> +		{ Defns = [hlds_cons_defn(_, _, _, TypeId, _)] }
> +	->
> +
> +		(
> +			{ module_info_types(ModuleInfo, Types) },
> +			{ map__lookup(Types, TypeId, TypeDefn) },
> +			{ hlds_data__get_type_defn_status(TypeDefn,
> +					TypeStatus) },
> +			{ \+ is_defined_in_implementation_section(TypeStatus) }
> +		->
> +			[]
> +		;
> +			write_assertion_interface_error(Context,
> +					cons(ConsId), ModuleInfo)
> +		)

Likewise.

> +	;
> +		prog_out__write_context(Context),
> +		io__write_string("In assertion:\n"),
> +
> +		prog_out__write_context(Context),
> +		io__write_string("  ambiguity error: constructor `"),
> +		hlds_out__write_cons_id(ConsId),
> +		io__write_string("' appears in multiple types.\n"),

Hmm... won't type checking already resolve this ambiguity,
or report an error if it is unresolvable?

That is, rather than looking up the cons_id in the ConsTable, and using that
to figure out the TypeId, I think you should obtain the TypeId by looking
at the type of the variable on the unification's LHS, as inferred by
typecheck.m and post_typecheck.m.

> +:- pred is_defined_in_implementation_section(import_status::in) is semidet.
> +
> +is_defined_in_implementation_section(abstract_exported).
> +is_defined_in_implementation_section(exported_to_submodules).
> +is_defined_in_implementation_section(local).

It might be better to make that a det function returning bool rather than
a predicate, to ensure that you cover all cases.  Otherwise this might
break when someone adds a new import_status...

> +	globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
> +	(
> +		{ VerboseErrors = yes }
> +	->
> +		prog_out__write_context(Context),
> +		io__write_string("  Either move the assertion into the "),
> +		io__write_string("implementation\n"),

I suggest adding " section" after "implementation".

> +		prog_out__write_context(Context),
> +		io__write_string("  or the definition into the interface.\n")

I suggest adding "move" before "the definition".

> --- hlds_out.m	1999/08/13 01:43:00	1.224
> +++ hlds_out.m	1999/09/01 06:08:47
> -	hlds_out__write_sym_name_and_args(PredName,
> -		ArgVars, VarSet, AppendVarnums),
> +	(
> +		{ PredOrFunc = predicate },
> +		{ NewArgVars = ArgVars }
> +	;
> +		{ PredOrFunc = function },
> +		(
> +			{ MaybeUnifyContext = yes(UnifyContext) },
> +			{ UnifyContext = call_unify_context(A, UnifyRHS, _) },
> +			{ UnifyRHS = functor(_ConsId, NewArgVars0) }
> +		->
> +			{ NewArgVars = NewArgVars0 },
> +			mercury_output_var(A, VarSet, AppendVarnums),
> +			io__write_string(" = ")
> +		;
> +			{ error("hlds_out: function without unify context") }
> +		)
> +	),
> +	hlds_out__write_sym_name_and_args(PredName, NewArgVars, VarSet,
> +			AppendVarnums),

You shouldn't output the variables from the unify_context,
because they might not be the same as the variables in the call.
E.g. after polymorphism has been run, the variables in the call
will include type_infos but the unify_context will remain unchanged.

Instead, you should use pred_args_to_func_args/3 defined in hlds_pred.m.

> +++ modules.m	1999/08/31 08:58:21
> @@ -738,13 +738,16 @@
>  		;
>  			%
>  			% Strip out the imported interfaces,
> +			% assertions are also striped since they should
> +			% only be written to .opt files,

s/striped/stripped/

>  make_short_interface(ModuleName, Items0) -->
>  	{ get_interface(Items0, no, InterfaceItems0) },
> -	check_for_clauses_in_interface(InterfaceItems0, InterfaceItems),
> +		% assertions are also striped since they should
> +		% only be written to .opt files,
> +	{ strip_assertions(InterfaceItems0, InterfaceItems1) },
> +	check_for_clauses_in_interface(InterfaceItems1, InterfaceItems),

Likewise.

> cvs [diff aborted]: there is no version here; do 'cvs checkout' first

Hmm, perhaps the diff that you posted was incomplete.

You should modify the notes/compiler_design.html file to
reflect your change to when function overloading is resolved.

----------

OK, those are minor points, and most of them should be easily resolved.
There are also a few more significant issues.

The most significant issue is that your diff does not properly check
for assertions in the interface depending on things in the implementation.

Here's what I proposed earlier:
| After type-checking the module, the implementation should check that any 
| assertion declarations in the interface do not contain any symbols from  
| modules imported only in the implementation.

But your change does not do this, it only checks that assertion declarations
in the interface do not contain any symbols from the implementation.
In particular, it won't catch the error in the following code:

	% foo.m
	:- module foo.
	:- interface.
	:- assertion all [X] bar__p(X).		% refers to `bar', which has
						% not been imported in the
						% interface section.
	:- implementation.
	:- use_module bar.
	:- end_module foo.

	% bar.m
	:- module bar.
	:- interface.
	:- pred p(int::in) is det.
	:- implementation.
	p(_).
	:- end_module bar.


Another issue is that ":- assertion" should be ":- promise".
That change can be committed separately, though, if you prefer.


The other important issue is that the proposed documentation is not adequate,
IMHO.  I agree with Lee's earlier comments on it.

For the moment, I suggest you keep the documentation of assertions commented
out (using `@c' in the TexInfo source).

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