[m-dev.] Termination Analysis part 1.1

[Fergus Henderson]

Christopher Rodd SPEIRS, you wrote:
> 
> Before I add the files, there is a decision that needs to be made about
> the options which control the termination analysis.  Currently there are
> two options to control termination analysis:
> 
> --enable-termination 
>  	This option enables the analyser.  This means that the compiler
> 	will emit warnings for any predicate which cannot be proved to
> 	terminate and has a check_termination pragma defined on it.
> 
> --check-termination
>  	This option implies the --enable-termination option.  When this
> 	option is enabled, warnings are emitted for every predicate
> 	which the compiler could not prove to terminate, unless the
> 	proof failed because the analysis is not powerful enough.  For
> 	example, warnings are not emitted if termination could not be
> 	proved just because a higher order call was made.
> 
> 	If verbose errors are enabled (-E), then warnings are emitted
> 	for every predicate which could not be proved to terminate.
> 	Unfortunatly, this is often a huge list of errors which are not
> 	very useful, but sometimes it is required.  
> 
> Now, the questions - Firstly, should we add a
> --verbose-termination-errors option?  If we do, then should this option
> imply the --check-termination option?  Also, do we want a shorter form of 
> --verbose-termination-errors?  If so, what?  We do currently have short 
> forms of --check-termination (--chk-term) and --enable-termination 
> (--enable-term).

I think it would be better to add a --verbose-termination-errors option
or something like that; the intent of `-E' is just that you get more
verbose explanations, so compiling with `-E' should not produce errors 
if compiling without `-E' didn't.

I don't mind what the options name are or whether --verbose-termination-errors
implies --check-termination.  A short version of all options with really
long names is a good idea.  For --verbose-termination-errors, I'd suggest
`--verb-term-errs'.

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