[m-dev.] Tdiff: termination analysis (BIG!)

[Fergus Henderson]

Christopher Rodd SPEIRS, you wrote:

> Index: make_hlds.m
> ===================================================================
> RCS file: /home/staff/zs/imp/mercury/compiler/make_hlds.m,v
> retrieving revision 1.226
> diff -u -r1.226 make_hlds.m
> +		undefined_pred_or_func_error(Name, Arity, Context,
> +			"Predicate not declared"),
> +		{ module_info_incr_errors(Module0, Module) },
> +		{ Markers = [] }
> +	).

The string passed to `undefined_pred_or_func_error' should
indicate the context, e.g. "pragma terminates" or "pragma check_termination".

> +:- pred terminates_and_check_termination_warning(sym_name, int, term__context
> +	, io__state, io__state).
> +:- mode terminates_and_check_termination_warning(in, in, in, di, uo) is det.
> +terminates_and_check_termination_warning(Name, Arity, Context) -->
> +	prog_out__write_context(Context),
> +	report_warning("Warning: 'pragma terminates("),
> +	hlds_out__write_pred_call_id(Name / Arity),
> +	io__write_string(")' and\n"),
> +	prog_out__write_context(Context),
> +	io__write_string("  'pragma check_termination("),
> +	hlds_out__write_pred_call_id(Name / Arity),
> +	io__write_string(")' defined on the one predicate\n").

The opening single quotes should be back-quote (`) not forward-quote (').
Please insert "both" after "Warning: ".
s/one/same/
Instead of hard-coding "predicate", it should print either "predicate"
or "function" as appropriate.

> +++ mercury_compile.m	1997/04/08 15:09:18
>  		mercury_compile__middle_pass(ModuleName, HLDS25, HLDS50),
> +		( { MakeTransOptInt = yes } ->
> +			trans_opt__write_optfile(HLDS50)
> +		;
> +			[]
> +		),

Shouldn't the `--make-trans-opt' option be mutually exclusive with
the `--compile-to-C' option?  The code you have there will make the
.trans_opt file and then will continue on and compile the main source
file.  Is that deliberate?  If so, why?

> +	% termination analysis requires polymorphism to be run,
> +	% as termination analysis cannot handle complex unification

Why not?
You can safely assume that complex unification will terminate if the
inputs are finite, can't you?

> +qualify_pragma(opt_terminates(A, B, C, D, E), opt_terminates(A, B, C, D, E),
> +				Info, Info) --> [].
> +qualify_pragma(terminates(A, B), terminates(A, B), Info, Info) --> [].
> +qualify_pragma(check_termination(A, B), check_termination(A, B), Info
> +		, Info) --> [].

That looks buggy to me.  Don't you need to module-qualify the pred names in
`pragma terminates' and `pragma check_termination' declarations?
(You might possibly need to module-qualify something in `opt_terminates'
declarations too.)

> Index: modules.m
> -		% `pragma obsolete' declarations are supposed to go
> +		% `pragma (obsolete, terminates, check_termination)' 
> +		% declarations are supposed to go

Please either change that to

	pragma `obsolete', `terminates', and `check_termination'
	declarations are supposed to go ...

or spell it out as

	`pragma obsolete', `pragma terminates', and `pragma check_termination'
	declarations are supposed to go ...

Should `pragma check_termination' really go in the interface??
I think only `pragma terminates' should go in the interface.

options.m:
> -	warn_simple_code	-	bool(yes),
> +	warn_simple_code	-	bool(no),

Uh, please explain?
I think that change would be a bad idea.

> +	io__write_string("\t--make-transitive-optimization-interface\n"),
> +	io__write_string("\t--make-trans-opt\n"),
> +	io__write_string("\t\tOutput transient optimization information\n"),
> +	io__write_string("\t\tinto the <module>.trans_opt file.\n").

s/transient/transitive/ ?

> +	io__write_string("\t--transient-intermodule-optimization\n"),
> +	io__write_string("\t--trans-intermod-opt\n"),
> +	io__write_string("\t\tImport data the transient intermodule optimization data..\n"),

Please rephrase that.  Fix the double-`.' problem.

> +	io__write_string("\t\tThis data is stored in the <module>.trans_opt file\n"),

Shouldn't that be plural rather than singular?

> +	io__write_string("\t--check-termination"),
> +	io__write_string("\t--check-term"),
> +	io__write_string("\t--term"),
> +	io__write_string("\t\tAnalyse each predicate to discover if it terminates.\n"),

Does this really analyze each and every predicate, or just the
ones for which there are `pragma check_termination' declarations?

> +	;	unused_args(pred_or_func, sym_name, int,
> +			proc_id, list(int))
> +			% PredName, Arity, Mode, Optimized pred name,
> +			% 	Removed arguments.
> +			% Used for inter-module unused argument
> +			% removal, should only appear in .opt files.
> +
> +	;	fact_table(sym_name, arity, string)
> +			% Predname, Arity, Fact file name.
> +	;	opt_terminates(pred_or_func, sym_name, int, proc_id,
> +			termination)
> +			% PredName, Arity, Mode, Termination
> +			% Used for inter-module termination analysis
> +			% should only appear in .opt files.
> +	;	terminates(sym_name, int)
> +			% Predname, Arity
> +	;	check_termination(sym_name, int).
> +			% Predname, Arity

Can you please insert some blank lines?
Also, can you please use `arity' rather than `int'?
(`arity' is defined somewhere as a typedef for `int'.)

> +++ prog_io_pragma.m	1997/04/09 12:27:15
> +parse_pragma_type(ModuleName, "assert_terminates", PragmaTerms,
> +				ErrorTerm, _VarSet, Result) :-
> +	parse_simple_pragma(ModuleName, "terminates",
> +		lambda([Name::in, Arity::in, Pragma::out] is det,
> +			Pragma = terminates(Name, Arity)),
> +		PragmaTerms, ErrorTerm, Result).

Hmm... how come it is "assert_terminates" in one spot and "terminates"
in the other?

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