[m-rev.] for review: mode checking changes for HAL

[Fergus Henderson]

On 09-Aug-2002, David Overton <dmo at cs.mu.OZ.AU> wrote:
> 
> Add two new options `--any-matches-ground' and `--ground-matches-bound'
> which, when set, alter mode analysis so that `any' matches `ground' and
> `ground' matches `bound', respectively.  These options are unsafe in
> general, but are required for some Mercury code generated by HAL.  They
> will always be safe to use in such cases since the HAL compiler will
> only produce code where the assumptions are valid.

Hmm.  I'm a bit concerned about option proliferation here.
This change increases the complexity of the user interface,
and also increases the complexity of the Mercury compiler's
mode analysis code.  Are these options really needed? 
Can't we modify the Mercury mode checker so that it accepts the code
output by HAL, or modify the HAL code generator so that it inserts
explicit inst-casts (or whatever) to placate the Mercury mode checker?

Also, this change should include some test cases.

> An example of when this is required is that for certain types, HAL knows
> that `any' is equivalent to `ground', but the Mercury compiler does not
> know this.  If the type is an instance of a type class where the methods
> have arguments requiring inst `any', we would like it to be possible for
> the user to supply an instance where the method argument is required to
> be `ground', if we know that `any' and `ground' are equivalent for this
> type.

How about the following alternative: add a pragma which allows programs
to declare that for a particular type, `any' is equivalent to ground.
Change that mode checker so that it allows `any' to be treated as
equivalent to ground only for those types.

Wouldn't a better solution to this problem?

> The HAL mode checker also carries around more precise type information
> than the Mercury mode checker so sometimes HAL is able to determine that
> `ground' matches a particular `bound' inst for a certain type, but
> Mercury is unable to prove this.

How about the modifying the Mercury mode checker so that it keeps track of
the type information needed in these cases?

> A third case is where an `any' inst appears in a negated context.
> Mercury is unable to prove that the variable with inst `any' is not
> instantiated in the negated context, but HAL can in some cases.

If there are three cases, how come there are only two options?
Wouldn't it make more sense to have a different option
"--any-matches-any" for the last case?

> --- compiler/inst_match.m	20 Mar 2002 12:36:24 -0000	1.50
> +++ compiler/inst_match.m	9 Aug 2002 02:12:28 -0000
> @@ -982,23 +1045,32 @@
>  		inst_match_info).
>  :- mode inst_matches_binding_3(in, in, in, in, out) is semidet.
>  
> -% Note that `any' is *not* considered to match `any'.
> +% Note that `any' is *not* considered to match `any' unless the option
> +% `--any_matches-ground' was given.
> +% WARNING allowing this in negations and the conditions of if-then-elses is
> +% potentially unsound.

s/any_matches/any-matches/

> +++ user_guide.texi	9 Aug 2002 04:05:53 -0000
> @@ -4231,6 +4231,20 @@
>  @cindex Inference of modes
>  @cindex Mode inference
>  Perform at most @var{n} passes of mode inference (default: 30).
> +
> + at sp 1
> + at item --any-matches-ground
> +Assume that @samp{any} matches @samp{ground} when mode checking calls and the
> +ends of procedure bodies.
> +Warning: this option is dangerous if used incorrectly (i.e.@: in situations
> +where the assumption does not hold).
> +
> + at sp 1
> + at item --ground-matches-bound
> +Assume that @samp{ground} matches @samp{bound} when mode checking calls and the
> +ends of procedure bodies.
> +Warning: this option is dangerous if used incorrectly (i.e.@: in situations
> +where the assumption does not hold).
>  @end table

I think these options are too dangerous to use if the Mercury source
code was not automatically generated by some tool which ensures that
the generated code is mode-correct.

In other words, these options are not useful except for HAL and perhaps
other compilers like it that target Mercury.

As a result, I think we should leave them deliberately undocumented
(i.e. the documentation should remain in the source code, but should
be commented out).

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------