[m-rev.] for review: add `any_is_bound' pragma

[Fergus Henderson]

On 24-Jul-2003, David Overton <dmo at cs.mu.OZ.AU> wrote:
> Allow types to be declared as "solver" types using the syntax
> `:- solver type ...'.

extras/trailed_update/var.m and extras/clpr/cfloat.m
should be modified to use the new syntax.

There should be more test cases.  In particular, there should be a
test case to test that `any' matches `bound' for non-solver types.
There should be some tests of whether `any' matches bound for polymorphic
types (it should not) and for tuple types (where it should match unless
one of the tuple elements is a solver type).

> @@ -1070,19 +1082,37 @@
>  :- mode inst_matches_binding_3(in, in, in, in, out) is semidet.
>  
>  % Note that `any' is *not* considered to match `any' unless 
> -% Info ^ any_matches_any = yes.
> +% Info ^ any_matches_any = yes or the type is a solver type.

Shouldn't that be "or the type is not a solver type".

Or, more correctly, "or the type is not a solver type (and does not
contain any solver types)".

> +:- pred maybe_any_to_bound(maybe(type), module_info, uniqueness, inst).
> +:- mode maybe_any_to_bound(in, in, in, out) is semidet.

I suggest adding a comment for this predicate,
e.g. (copied from your log message):

	% For a non-solver type t (i.e. any type declared without using
	% the `solver' keyword), the inst `any' should be considered
	% to be equivalent to a bound inst i where i contains all
	% the functors of the type t and each argument has inst `any'.

> +maybe_any_to_bound(yes(Type), ModuleInfo, Uniq, Inst) :-
> +	\+ type_util__is_solver_type(ModuleInfo, Type),
> +	(
> +		type_constructors(Type, ModuleInfo, Constructors)
> +	->
> +		constructors_to_bound_any_insts(Constructors, Uniq,
> +			ModuleInfo, BoundInsts0),
> +		list__sort_and_remove_dups(BoundInsts0, BoundInsts),
> +		Inst = bound(Uniq, BoundInsts)
> +	;
> +		classify_type(Type, ModuleInfo, user_type)
> +	->
> +		% XXX For a user-defined type for which constructors are not
> +		% available (e.g. an abstract type) we should return `nonvar',
> +		% but we don't have a `nonvar' inst (yet) so we fail, meaning
> +		% that we will use `any' for this type.
> +		fail
> +	;
> +		Inst = ground(Uniq, none)
> +	).

I'm pretty sure it is not safe to use `ground' here in the cases where
classify_type(Type, ModuleInfo, Category) returns Category = tuple_type
or Category = polymorphic_type.

The code should also be written so that it is robust against future
changes to the builtin_type enum that classify_type returns, e.g.
by having this code call a det function that covers all the different
alternatives for builtin_type.

Also, regarding the comment about `nonvar': I'm quite dubious about
adding `nonvar' in the future.  Given that we have no_tag types,
and that the `nonvar' value could just be a no_tag wrapper around a solver
type with inst `any', I don't see how `nonvar' could provide any useful
information.

Otherwise that looks fine.

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