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

[Fergus Henderson]

I'm going to do this reviewing in dribs and drabs.
Here's the first file.

> doc/user_guide.texi:
> 	Added documentation about new options added to control termination 
> 	analysis and transient optimization files.

> +++ user_guide.texi	1997/04/09 12:20:17
> + at sp 1
> + at itemx --make-transient-optimization-interface
> + at itemx --make-trans-opt
> +Write the @file{@var{module}.trans_opt} file.  This file is used to store
> +information about the module that can be used for optimization. The 
> +file is transient as a @file{@var{module}.trans_opt} file may depend on other
> + at file{@var{module}.trans_opt} files.

TexInfo formatting error: the first `@itemx' should be `@item'.

The documentation for `--make-trans-opt' is in the wrong section.
It should be in the "output options" section, just after the
documentation for `--make-optimization-interface'.

s/transient/transitive/g and rephrase accordingly.

You should state when the trans_opt files are used
("... that can be used for optimization" is not sufficient).

You need to document the `.trans_opt' file extension in the
chapter on file naming conventions.

You also need to document the use of the `--make-trans-opt' option
in the sections on "using mc" and "using mmake". 

In particular, you need to clearly document the requirement to rerun
`mmake depend' when adding/removing `--make-trans-opt' from the
MCFLAGS.

> + at sp 1
> + at item --transient-intermodule-optimization
> + at item --trans-intermod-opt
> +Use the information stored in the @file{@var{module}.trans_opt} file
> +to make intermodule optimizations. 

That's wrong, isn't it?  Shouldn't it use the information stored
in the trans_opt files for all the imported modules, rather than
in that for the file being compiled?

> + at sp 1
> + at item --check-termination
> + at item --check-term
> + at item --term
> +Enable termination analysis.  Termination analysis analyses each mode of each
> +predicate to see whether it terminates.  @samp{pragma assert_terminates} and
> + at samp{pragma check_termination} pragmas have no effect unless termination
> +analysis is enabled.  When using termination,
> + at samp{--transient-intermodule-optimization} should be enabled, as it greatly
> +improves the accuracy of the analysis.

After giving it a bit more thought, I think it would be best
for the alternative spellings of this option to be the following two:

	--check-termination
	--chk-term

Also, on seeing it, I don't like `pragma assert_terminates(foo/1)'.
I think I prefer `pragma terminates(foo/1)'.
Or possibly `pragma assert(terminates(foo/1))' -- but that would
probably be too confusing given Prolog's use of `assert'.
So could you please s/assert_terminates/terminates/g.

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