[m-dev.] Termination Analysis 2.2

[Fergus Henderson]

Christopher Rodd SPEIRS, you wrote:
> +	% hlds_out__write_pred_id/4 writes out a message such as
> +	% 	predicate `foo:bar/3'
> +	% or	function `foo:myfoo/5'
> +	% unless the predicate name begins with a double underscore "__",
> +	% in which case mercury_output_term is used to print out the
> +	% predicate's (or function's) name. 

Please add "and argument types (since for `__Unify__' predicates,
the module, name and arity are not sufficient to indentify the predicate)".

> +			undefined_pred_or_func_error(SymName, Arity, Context,
> +				":- pragma termination_info declaration"),

Please change that to
				"`:- pragma termination_info' declaration"),

> +			io__write_string("Error: Ambiguous predicate name"),

s/Amb/amb/

> +			io__write_string("  in pragma termination_info\n"),

Please change that to
			io__write_string(
			    "  in `pragma termination_info' declaration.\n"),

> +		    undefined_pred_or_func_error(SymName, Arity, Context,
> +			":- pragma termination_info declaration"),

Please change that to
			"`:- pragma termination_info' declaration"),

> +	io__write_string("\t--termination-norm"),

That should be

	io__write_string("\t--termination-norm {this, that, the_other}"),

where `this', `that', and `the_other' are the possible arguments allowed here.

> +	io__write_string("\t\tSet the norm to be used when doing termination analysis.\n"),

What's a norm?

You need a much better explanation here.

> +	% People never seem to remember what the right operator to use in a
> +	% `:- mode' declaration is, so the syntax is forgiving.  We allow
> +	% `::', the standard one which has the right precedence, but we
> +	% also allow `==' just to be nice.
>  :- pred mode_op(term, term, term).
>  :- mode mode_op(in, out, out) is semidet.
>  mode_op(term__functor(term__atom(Op), [H, B], _), H, B) :-
> -		% People never seem to remember what the right
> -		% operator to use in a `:- mode' declaration is,
> -		% so the syntax is forgiving.
> -		% We allow `::', the standard one which has the right
> -		% precedence, but we also allow `==' just to be nice.
> -	(	Op = "::"
> -	->	true
> -	;	Op = "=="
> +	( Op = "::" ->	
> +		true
> +	;	
> +		Op = "=="
>  	).

Well, if you're going to change that code, best to change it to just

	( Op = "::" ; Op = "==" ).

> +	    parse_qualified_term(ModuleName, PredAndModesTerm,
> +		"pragma termination_info declaration", PredNameResult),

Please change that to

		"`pragma termination_info' declaration", PredNameResult),

> +	    Result0 = error("unexpected variable in pragma termination_info",
> +						ErrorTerm)

Please change that to

	    Result0 = error(
	    "unexpected variable in `pragma termination_info' declaration",
						ErrorTerm)


> +	Result = error("Syntax error in pragma termination_info", ErrorTerm)

Please change that to

	Result = error("syntax error in `pragma termination_info' declaration",
		ErrorTerm)

(note lower-case "s")

> -	Result = error("unexpected variable in pragma(c_code, ...)",
> -						PredAndVarsTerm0)
> +	Result = error("unexpected variable in pragma c_code",
> +		PredAndVarsTerm0)

That's an improvement, but please change it to

	Result = error("unexpected variable in `pragma c_code' declaration",

> +Currently the compiler assumes that all c code terminates for any input.

s/c code/C code/

Or better, rephrase that as

	Currently the compiler assumes that all procedures defined using
	the C interface (@samp{pragma c_code}) terminate for any input.

> + at example
> +:- pragma does_not_terminate(@var{Name}/@var{Arity}).
> + at end example
> +This declaration may be used to inform the compiler that this predicate
> +does not necessarily terminate for any input.  This is useful for c
> +code, which the compiler assumes to terminate by default.

s/c code/procedures defined using the C interface/

> + at c @sp 1
> + at c @item --make-transitive-optimization-interface
> + at c @itemx --make-trans-opt
> + at c Write the @file{@var{module}.trans_opt} file.  This file is used to store
> + at c information used for inter-module optimization. The information is read 
> + at c in when the compiler is invoked with the --transitive-otimization 

	--transitive-otimization

should be

	@samp{--transitive-optimization}
			    ^

> + at c option.  The file is transitive as a @file{@var{module}.trans_opt} file 
> + at c may depend on other @file{@var{module}.trans_opt} files.

s/is transitive as/is called ``transitive'' because/

> + at sp 1
> + at item --check-termination
> + at itemx --check-term
> + at itemx --chk-term
> +Enable termination analysis, and emit warnings for some predicates or
> +functions that cannot be proved to terminate.  In many cases where the
> +compiler is unable to prove termination the problem is either a lack of
> +information about the termination properties of other predicates, or
> +because language constructs (such as higher order calls) were used which
> +could not be analysed. 

Change to

	because the program used language constructs (such as higher
	order calls) which could not be analysed. 

Otherwise that looks fine.

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