[m-dev.] for review: constrain interface assertions to using interface symbols

[Peter Ross]

On 11-Nov-1999, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> On 11-Nov-1999, Peter Ross <petdr at cs.mu.OZ.AU> wrote:
> > Assertion declarations in the interface must not contain any symbols from
> > modules imported only in the implementation.  This constraint requires
> > that each imported symbol be annotated with whether it is imported from
> > the interface or implementation.
> >
> > compiler/prog_data.m:
> >     Update the pseudo declaration `:- imported' to include which section
> >     (either implementation or interface) the items following it where
> >     imported from.
> 
> s/where/were/
> 
Done.

> > compiler/module_qual.m:
> >     Any unqualified symbol in an assertion might come from *any*
> >     of the imported modules, so turn off the warning about modules which
> >     are imported in the interface but not used,
> 
> I suggest you make it clear in the log message exactly when
> you are disabling the warning:
> 	- if an unqualified symbol appears in an assertion?
> 	- if the interface contains an assertion?
> 	- all the time?

How about

compiler/module_qual.m:
    Any unqualified symbol in an assertion might come from *any*
    of the imported modules, so turn off the warning about modules which
    are imported in the interface but not used, if an unqualified symbol
    appears in the assertion.

> > compiler/accumulator.m:
> >     Use where a symbol is imported from when deciding whether an
> >     assertion in the interface is valid.
> 
> Did you mean `assertion.m' rather than `accumulator.m' here?
> I don't see why accumulator.m should have to change as a result
> of this change.
> 
Woops, yes.

> > Index: hlds_pred.m
> > ===================================================================
> > RCS file: /home/staff/zs/imp/mercury/compiler/hlds_pred.m,v
> > retrieving revision 1.66
> > diff -u -r1.66 hlds_pred.m
> > --- hlds_pred.m	1999/10/15 03:44:49	1.66
> > +++ hlds_pred.m	1999/10/27 04:48:20
> > @@ -974,8 +975,8 @@
> >  pred_info_mark_as_external(PredInfo0, PredInfo) :-
> >  	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, _, K, L, M, N, O, P,
> >  		Q, R, S, T, U, V),
> > -	PredInfo  = predicate(A, B, C, D, E, F, G, H, I, imported, K, L, M, 
> > -		N, O, P, Q, R, S, T, U, V).
> > +	PredInfo  = predicate(A, B, C, D, E, F, G, H, I, imported(interface),
> > +		K, L, M, N, O, P, Q, R, S, T, U, V).
> 
> Hmm, is that correct?
No.

> Shouldn't you check whether the old status was
> `local' or `exported'?  If it was `local', then
> the new status should be `imported(implementation)',
> not `imported(interface)'.
> 
How about

Index: hlds_pred.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/hlds_pred.m,v
retrieving revision 1.66
diff -u -r1.66 hlds_pred.m
--- hlds_pred.m	1999/10/15 03:44:49	1.66
+++ hlds_pred.m	1999/11/11 04:21:43
@@ -972,10 +973,20 @@
 	).
 
 pred_info_mark_as_external(PredInfo0, PredInfo) :-
-	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, _, K, L, M, N, O, P,
-		Q, R, S, T, U, V),
-	PredInfo  = predicate(A, B, C, D, E, F, G, H, I, imported, K, L, M, 
-		N, O, P, Q, R, S, T, U, V).
+	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, ImportStatus,
+		K, L, M, N, O, P, Q, R, S, T, U, V),
+	status_is_exported(ImportStatus, Exported),
+	(
+		Exported = yes,
+		PredInfo  = predicate(A, B, C, D, E, F, G, H, I,
+				imported(interface), K, L, M, N, O,
+				P, Q, R, S, T, U, V)
+	;
+		Exported = no,
+		PredInfo  = predicate(A, B, C, D, E, F, G, H, I,
+				imported(implementation), K, L, M, N, O,
+				P, Q, R, S, T, U, V)
+	).
 
 pred_info_set_import_status(PredInfo0, Status, PredInfo) :-
 	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, _, K, L, M, N, O, P,


> I suggest you add the following test case to tests/invalid
> 
Please see my other message for my additions to the test directory.

> > +collect_mq_info_2(assertion(_, _), Info0, Info) :-
> > +	% Any unqualified symbol in the assertion might come from *any*
> > +	% of the imported modules.
> > +	% There's no way for us to tell which ones.
> > +	% So we conservatively assume that it uses all of them.
> > +	% XXX a better solution would be to only make this assumption if
> > +	% the assertion contains an unqualified symbol, however since
> > +	% the structure isn't in superhomogenous form yet processing the
> > +	% goal is complicated.
> > +	set__init(UnusedInterfaceModules),
> > +	mq_info_set_unused_interface_modules(Info0, UnusedInterfaceModules,
> > +		Info).
> 
> Well, not _that_ complicated; you do have to traverse the `goal' type
> (requiring one ~30-line predicate), but once you get to a `call'
> or `unify', it's fairly easy: 
> 
> 
> Go on, it should only take you another 5-15 minutes to finish that off ;-)
> 
I can't believe I succumbed to peer group pressure :)

Index: module_qual.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/module_qual.m,v
retrieving revision 1.51
diff -u -r1.51 module_qual.m
--- module_qual.m	1999/10/04 04:04:43	1.51
+++ module_qual.m	1999/11/11 07:10:48
@@ -198,7 +198,32 @@
 collect_mq_info_2(pred_mode(_,_,_,_,_), Info, Info).
 collect_mq_info_2(func_mode(_,_,_,_,_,_), Info, Info).
 collect_mq_info_2(pragma(_), Info, Info).
-collect_mq_info_2(assertion(_, _), Info, Info).
+collect_mq_info_2(assertion(Goal, _ProgVarSet), Info0, Info) :-
+	process_assert(Goal, SymNames, Success),
+	(
+		Success = yes,
+		list__foldl((pred(SymName::in, I0::in, I::out) is det :- 
+				(
+					SymName = qualified(ModuleName, _)
+				->
+					mq_info_set_module_used(I0,
+							ModuleName, I)
+				;
+					error("collect_mq_info_2: SymName not qualified.")
+				)
+			), 
+			SymNames, Info0, Info)
+	;
+			% Any unqualified symbol in the assertion might
+			% come from *any* of the imported modules.
+			% There's no way for us to tell which ones.  So
+			% we conservatively assume that it uses all of
+			% them. 
+		Success = no,
+		set__init(UnusedInterfaceModules),
+		mq_info_set_unused_interface_modules(Info0,
+				UnusedInterfaceModules, Info)
+	).
 collect_mq_info_2(nothing, Info, Info).
 collect_mq_info_2(typeclass(_, Name, Vars, _, _), Info0, Info) :-
 	add_typeclass_defn(Name, Vars, Info0, Info).
@@ -321,6 +346,125 @@
 
 %------------------------------------------------------------------------------
 
+	% process_assert(G, SNs, B)
+	%
+	% Scan the goal, G, building the list of qualified symbols, SNs.
+	% If there exists a single unqualifed symbol in G, the bool, B,
+	% will be set to no.
+:- pred process_assert(goal::in, list(sym_name)::out, bool::out) is det.
+
+	% AAA Some more stuff to do accumulator introduction on, it
+	% would be better to rewrite using maybes and then to declare
+	% the maybe_and predicate to be associative.
+	% NB. accumulator introduction doesn't work on this case yet.
+process_assert((GA , GB) - _, Symbols, Success) :-
+	process_assert(GA, SymbolsA, SuccessA),
+	process_assert(GB, SymbolsB, SuccessB),
+	list__append(SymbolsA, SymbolsB, Symbols),
+	bool__and(SuccessA, SuccessB, Success).
+process_assert(true - _, [], yes).
+process_assert((GA & GB) - _, Symbols, Success) :-
+	process_assert(GA, SymbolsA, SuccessA),
+	process_assert(GB, SymbolsB, SuccessB),
+	list__append(SymbolsA, SymbolsB, Symbols),
+	bool__and(SuccessA, SuccessB, Success).
+process_assert((GA ; GB) - _, Symbols, Success) :-
+	process_assert(GA, SymbolsA, SuccessA),
+	process_assert(GB, SymbolsB, SuccessB),
+	list__append(SymbolsA, SymbolsB, Symbols),
+	bool__and(SuccessA, SuccessB, Success).
+process_assert(fail - _, [], yes).
+process_assert(some(_, G) - _, Symbols, Success) :-
+	process_assert(G, Symbols, Success).
+process_assert(all(_, G) - _, Symbols, Success) :-
+	process_assert(G, Symbols, Success).
+process_assert(implies(GA, GB) - _, Symbols, Success) :-
+	process_assert(GA, SymbolsA, SuccessA),
+	process_assert(GB, SymbolsB, SuccessB),
+	list__append(SymbolsA, SymbolsB, Symbols),
+	bool__and(SuccessA, SuccessB, Success).
+process_assert(equivalent(GA, GB) - _, Symbols, Success) :-
+	process_assert(GA, SymbolsA, SuccessA),
+	process_assert(GB, SymbolsB, SuccessB),
+	list__append(SymbolsA, SymbolsB, Symbols),
+	bool__and(SuccessA, SuccessB, Success).
+process_assert(not(G) - _, Symbols, Success) :-
+	process_assert(G, Symbols, Success).
+process_assert(if_then(_, GA, GB) - _, Symbols, Success) :-
+	process_assert(GA, SymbolsA, SuccessA),
+	process_assert(GB, SymbolsB, SuccessB),
+	list__append(SymbolsA, SymbolsB, Symbols),
+	bool__and(SuccessA, SuccessB, Success).
+process_assert(if_then_else(_, GA, GB, GC) - _, Symbols, Success) :-
+	process_assert(GA, SymbolsA, SuccessA),
+	process_assert(GB, SymbolsB, SuccessB),
+	process_assert(GC, SymbolsC, SuccessC),
+	list__append(SymbolsA, SymbolsB, Symbols0),
+	list__append(Symbols0, SymbolsC, Symbols),
+	bool__and(SuccessA, SuccessB, Success0),
+	bool__and(Success0, SuccessC, Success).
+process_assert(call(SymName, Args0, _) - _, Symbols, Success) :-
+	(
+		SymName = qualified(_, _)
+	->
+		list__map(term__coerce, Args0, Args),
+		(
+			term_qualified_symbols_list(Args, Symbols0)
+		->
+			Symbols = [SymName | Symbols0],
+			Success = yes
+		;
+			Symbols = [],
+			Success = no
+		)
+	;
+		Symbols = [],
+		Success = no
+	).
+process_assert(unify(LHS0, RHS0) - _, Symbols, Success) :-
+	term__coerce(LHS0, LHS),
+	term__coerce(RHS0, RHS),
+	(
+		term_qualified_symbols(LHS, SymbolsL),
+		term_qualified_symbols(RHS, SymbolsR)
+	->
+		list__append(SymbolsL, SymbolsR, Symbols),
+		Success = yes
+	;
+		Symbols = [],
+		Success = no
+	).
+
+	% term_qualified_symbols(T, S)
+	%
+	% Given a term, T, return the list of all the sym_names, S, in
+	% the term.  The predicate fails if any sub-term of T is
+	% unqualified.
+:- pred term_qualified_symbols(term::in, list(sym_name)::out) is semidet.
+
+term_qualified_symbols(Term, Symbols) :-
+	(
+		sym_name_and_args(Term, SymName, Args)
+	->
+		SymName = qualified(_, _),
+		term_qualified_symbols_list(Args, Symbols0),
+		Symbols = [SymName | Symbols0]
+	;
+		Symbols = []
+	).
+
+:- pred term_qualified_symbols_list(list(term)::in,
+		list(sym_name)::out) is semidet.
+
+	% Yeah one more place where accumulators will be introduced!
+term_qualified_symbols_list([], []).
+term_qualified_symbols_list([Term | Terms], Symbols) :-
+	term_qualified_symbols(Term, TermSymbols),
+	term_qualified_symbols_list(Terms, Symbols0),
+	list__append(Symbols0, TermSymbols, Symbols).
+
+%------------------------------------------------------------------------------
+
 	% Iterate over the item list module qualifying all declarations.
 	% Stop when the :- imported or :- opt_imported pseudo-declaration
 	% is reached, since imported declarations should already be


> >  :- pred warn_if_duplicate_use_import_decls(module_name, list(module_name),
> >  		list(module_name), list(module_name), list(module_name), 
> > +		list(module_name), list(module_name), list(module_name), 
> > +		list(module_name), io__state, io__state).
> > +:- mode warn_if_duplicate_use_import_decls(in, in, out, in, out, in, out,
> > +		in, out, di, uo) is det.
> > +
> > +% This predicate ensures that all every import_module declaration is
> > +% checked against every use_module declaration.
> > +% warn_if_duplicate_use_import_decls/7 is called to generate the actual
> > +% warnings.
> > +
> > +warn_if_duplicate_use_import_decls(ModuleName,
> > +		IntImportedModules0, IntImportedModules, 
> > +		IntUsedModules0, IntUsedModules, 
> > +		ImpImportedModules0, ImpImportedModules, 
> > +		ImpUsedModules0, ImpUsedModules) -->
> > +
> > +	warn_if_duplicate_use_import_decls(ModuleName,
> > +		IntImportedModules0, IntImportedModules1,
> > +		IntUsedModules0, IntUsedModules1),
> > +	warn_if_duplicate_use_import_decls(ModuleName,
> > +		IntImportedModules1, IntImportedModules,
> > +		ImpUsedModules0, ImpUsedModules1),
> > +
> > +	warn_if_duplicate_use_import_decls(ModuleName,
> > +		ImpImportedModules0, ImpImportedModules1,
> > +		IntUsedModules1, IntUsedModules),
> > +	warn_if_duplicate_use_import_decls(ModuleName,
> > +		ImpImportedModules1, ImpImportedModules,
> > +		ImpUsedModules1, ImpUsedModules).
> > +
> 
> Actually I think it makes perfect sense to have `:- use_module foo'.
> in the interface and `:- import_module foo.' in the implementation.
> The other three cases don't make sense, but that one does.
> The compiler should not warn about it.
> So I think you should delete that third call to
> `warn_if_duplicate_use_import_decls',
> and modify the documentation for this pred accordingly.
> 
Index: modules.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/modules.m,v
retrieving revision 1.110
diff -u -r1.110 modules.m
--- modules.m	1999/10/21 14:36:31	1.110
+++ modules.m	1999/11/11 05:20:44
@@ -1311,6 +1350,37 @@
 
 :- pred warn_if_duplicate_use_import_decls(module_name, list(module_name),
 		list(module_name), list(module_name), list(module_name), 
+		list(module_name), list(module_name), list(module_name), 
+		list(module_name), io__state, io__state).
+:- mode warn_if_duplicate_use_import_decls(in, in, out, in, out, in, out,
+		in, out, di, uo) is det.
+
+% This predicate ensures that all every import_module declaration is
+% checked against every use_module declaration, except for the case
+% where the interface has `:- use_module foo.' and the implementation
+% `:- import_module foo.'.
+% warn_if_duplicate_use_import_decls/7 is called to generate the actual
+% warnings.
+
+warn_if_duplicate_use_import_decls(ModuleName,
+		IntImportedModules0, IntImportedModules, 
+		IntUsedModules0, IntUsedModules, 
+		ImpImportedModules0, ImpImportedModules, 
+		ImpUsedModules0, ImpUsedModules) -->
+
+	warn_if_duplicate_use_import_decls(ModuleName,
+		IntImportedModules0, IntImportedModules1,
+		IntUsedModules0, IntUsedModules),
+	warn_if_duplicate_use_import_decls(ModuleName,
+		IntImportedModules1, IntImportedModules,
+		ImpUsedModules0, ImpUsedModules1),
+
+	warn_if_duplicate_use_import_decls(ModuleName,
+		ImpImportedModules0, ImpImportedModules,
+		ImpUsedModules1, ImpUsedModules).
+
+:- pred warn_if_duplicate_use_import_decls(module_name, list(module_name),
+		list(module_name), list(module_name), list(module_name), 
 		io__state, io__state).
 :- mode warn_if_duplicate_use_import_decls(in, in, out, in, out, di, uo) is det.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------