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

[David Overton]

On Thu, Jul 24, 2003 at 03:46:24PM +1000, Fergus Henderson wrote:
> 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.

Done.

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

Done.

> 
> > @@ -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)".

Yes, I've changed the comment.

> 
> > +:- 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'.

Done.

> 
> > +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 is correct (although not as robust as it could be).  For
polymorphic_type, the call to type_util__is_solver_type will succeed so
maybe_any_to_bound will fail.  For tuple types, the call to
type_constructors will succeed so we return the appropriate bound inst.

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

Done.

> 
> Otherwise that looks fine.

Okay.  I'll commit this now.  Relative diff below.

--- CVSLOG.1	Fri Jul 25 12:15:36 2003
+++ CVSLOG	Fri Jul 25 12:18:37 2003
@@ -81,4 +81,16 @@
 
 tests/invalid/any_mode.m:
 tests/invalid/any_mode.err_exp:
-	Modify this test case to use a "solver" type instead of `int'.
+tests/hard_coded/any_free_unify.m:
+	Modify these test cases to use a "solver" type instead of `int'.
+
+tests/valid/any_matches_bound.m:
+tests/valid/Mmakefile:
+tests/invalid/Mmakefile:
+tests/invalid/any_should_not_match_bound.m:
+tests/invalid/any_should_not_match_bound.err_exp:
+	Add new test cases.
+
+extras/trailed_update/var.m:
+clpr/cfloat.m:
+	Modify to use the new `:- solver type' syntax.

diff -u compiler/inst_match.m compiler/inst_match.m
--- compiler/inst_match.m	22 Jul 2003 07:05:54 -0000
+++ compiler/inst_match.m	25 Jul 2003 01:41:04 -0000
@@ -1082,7 +1082,8 @@
 :- 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 or the type is a solver type.
+% Info ^ any_matches_any = yes or the type is not a solver type (and does not
+% contain any solver types).
 inst_matches_binding_3(free, free, _, I, I).
 inst_matches_binding_3(any(UniqA), any(UniqB), Type, Info0, Info) :-
 	( Info0 ^ any_matches_any = yes ->
@@ -1944,6 +1945,10 @@
 
 %-----------------------------------------------------------------------------%
 
+	% 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'.
 :- pred maybe_any_to_bound(maybe(type), module_info, uniqueness, inst).
 :- mode maybe_any_to_bound(in, in, in, out) is semidet.
 
@@ -1957,16 +1962,34 @@
 		list__sort_and_remove_dups(BoundInsts0, BoundInsts),
 		Inst = bound(Uniq, BoundInsts)
 	;
-		classify_type(Type, ModuleInfo, user_type)
+		type_may_contain_solver_type(Type, ModuleInfo)
 	->
-		% 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.
+		% For a type for which constructors are not available (e.g. an
+		% abstract type) and which may contain solver types, we fail,
+		% meaning that we will use `any' for this type.
 		fail
 	;
 		Inst = ground(Uniq, none)
 	).
+
+:- pred type_may_contain_solver_type((type), module_info).
+:- mode type_may_contain_solver_type(in, in) is semidet.
+
+type_may_contain_solver_type(Type, ModuleInfo) :-
+	classify_type(Type, ModuleInfo, Category),
+	type_may_contain_solver_type_2(Category) = yes.
+
+:- func type_may_contain_solver_type_2(builtin_type) = bool.
+
+type_may_contain_solver_type_2(int_type) = no.
+type_may_contain_solver_type_2(char_type) = no.
+type_may_contain_solver_type_2(str_type) = no.
+type_may_contain_solver_type_2(float_type) = no.
+type_may_contain_solver_type_2(pred_type) = no.
+type_may_contain_solver_type_2(tuple_type) = yes.
+type_may_contain_solver_type_2(enum_type) = no.
+type_may_contain_solver_type_2(polymorphic_type) = yes.
+type_may_contain_solver_type_2(user_type) = yes.
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
only in patch2:
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/valid/any_matches_bound.m	25 Jul 2003 01:42:48 -0000
@@ -0,0 +1,42 @@
+:- module any_matches_bound.
+
+:- interface.
+
+:- pred p(T::in, T::out(any)) is det.
+
+:- pred test_any_string(string::in(any), string::out) is det.
+:- pred test_any_int(int::in(any), int::out) is det.
+:- pred test_any_float(float::in(any), float::out) is det.
+:- pred test_any_char(character::in(any), character::out) is det.
+:- pred test_any_enum(enum::in(any), enum::out) is det.
+:- pred test_any_tuple({enum, int}::in(any), {enum, int}::out) is det.
+:- pred test_any_du(du(enum)::in(any), du(enum)::out) is det.
+
+:- type enum ---> foo ; bar ; baz.
+
+:- type du(T) ---> nil ; cons(T, du(T)).
+
+:- implementation.
+
+p(X, X).
+
+test_any_string(X, Y) :-
+	p(X, Y).
+
+test_any_int(X, Y) :-
+	p(X, Y).
+
+test_any_float(X, Y) :-
+	p(X, Y).
+
+test_any_char(X, Y) :-
+	p(X, Y).
+
+test_any_enum(X, Y) :-
+	p(X, Y).
+
+test_any_tuple(X, Y) :-
+	p(X, Y).
+
+test_any_du(X, Y) :-
+	p(X, Y).
only in patch2:
--- tests/valid/Mmakefile	17 May 2003 04:31:53 -0000	1.129
+++ tests/valid/Mmakefile	25 Jul 2003 01:44:09 -0000
@@ -52,6 +52,7 @@
 
 OTHER_PROGS= \
 	any_inst_merge \
+	any_matches_bound \
 	common_struct_bug \
 	compl_unify_bug \
 	complicated_unify \
only in patch2:
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/any_should_not_match_bound.m	25 Jul 2003 02:02:48 -0000
@@ -0,0 +1,30 @@
+:- module any_should_not_match_bound.
+
+:- interface.
+
+:- pred p(T::in, T::out(any)) is det.
+
+:- pred test_any_poly(T::in(any), T::out) is det.
+:- pred test_any_tuple({int, foo}::in(any), {int, foo}::out) is det.
+:- pred test_any_du(du(T)::in(any), du(T)::out) is det.
+:- pred test_any_solver(foo::in(any), foo::out) is det.
+
+:- solver type foo ---> bar ; baz.
+
+:- type du(T) ---> nil ; cons(T, du(T)).
+
+:- implementation.
+
+p(X, X).
+
+test_any_poly(X, Y) :-
+	p(X, Y).
+
+test_any_tuple(X, Y) :-
+	p(X, Y).
+
+test_any_du(X, Y) :-
+	p(X, Y).
+
+test_any_solver(X, Y) :-
+	p(X, Y).
only in patch2:
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/any_should_not_match_bound.err_exp	25 Jul 2003 02:03:46 -0000
@@ -0,0 +1,17 @@
+any_should_not_match_bound.m:021: In clause for `test_any_poly(in(any), out)':
+any_should_not_match_bound.m:021:   in argument 1 of call to predicate `any_should_not_match_bound.p/2':
+any_should_not_match_bound.m:021:   mode error: variable `X' has instantiatedness `any',
+any_should_not_match_bound.m:021:   expected instantiatedness was `ground'.
+any_should_not_match_bound.m:024: In clause for `test_any_tuple(in(any), out)':
+any_should_not_match_bound.m:024:   in argument 1 of call to predicate `any_should_not_match_bound.p/2':
+any_should_not_match_bound.m:024:   mode error: variable `X' has instantiatedness `any',
+any_should_not_match_bound.m:024:   expected instantiatedness was `ground'.
+any_should_not_match_bound.m:027: In clause for `test_any_du(in(any), out)':
+any_should_not_match_bound.m:027:   in argument 1 of call to predicate `any_should_not_match_bound.p/2':
+any_should_not_match_bound.m:027:   mode error: variable `X' has instantiatedness `any',
+any_should_not_match_bound.m:027:   expected instantiatedness was `ground'.
+any_should_not_match_bound.m:030: In clause for `test_any_solver(in(any), out)':
+any_should_not_match_bound.m:030:   in argument 1 of call to predicate `any_should_not_match_bound.p/2':
+any_should_not_match_bound.m:030:   mode error: variable `X' has instantiatedness `any',
+any_should_not_match_bound.m:030:   expected instantiatedness was `ground'.
+For more information, try recompiling with `-E'.
only in patch2:
--- tests/invalid/Mmakefile	2 Jun 2003 04:56:30 -0000	1.137
+++ tests/invalid/Mmakefile	25 Jul 2003 02:04:51 -0000
@@ -31,6 +31,7 @@
 
 SINGLEMODULE_PROGS= \
 	any_mode \
+	any_should_not_match_bound \
 	assert_in_interface \
 	bigtest \
 	bind_in_negated \
only in patch2:
--- tests/hard_coded/any_free_unify.m	2 Jun 2003 04:56:30 -0000	1.1
+++ tests/hard_coded/any_free_unify.m	25 Jul 2003 01:11:04 -0000
@@ -14,7 +14,9 @@
 	{ test_any_free_unify([], Result1) },
 	io__print(Result1), io__nl.
 
-:- pred test_any_free_unify(list(int), bool).
+:- solver type foo ---> bar ; baz.
+
+:- pred test_any_free_unify(list(foo), bool).
 :- mode test_any_free_unify(in(list_skel(any)), out) is det.
 
 % In the unification in the condition of the if-then-else, the variable
only in patch2:
--- extras/trailed_update/var.m	7 Nov 2002 06:19:09 -0000	1.21
+++ extras/trailed_update/var.m	25 Jul 2003 00:02:15 -0000
@@ -1,5 +1,5 @@
 %-----------------------------------------------------------------------------%
-% Copyright (C) 1998-2000, 2002 The University of Melbourne.
+% Copyright (C) 1998-2000, 2002-2003 The University of Melbourne.
 % This file may only be copied under the terms of the GNU Library General
 % Public License - see the file COPYING.LIB in the Mercury distribution.
 %-----------------------------------------------------------------------------%
@@ -34,7 +34,7 @@
 :- import_module io, std_util.
 
 	% A `var(T)' is a Prolog-style variable that holds a value of type T.
-:- type var(T).
+:- solver type var(T).
 
 	% `init(Var)' can be used to initialize
 	% the inst of a variable to `any'.
@@ -166,7 +166,7 @@
 	% representations simply because that name is "traditional".
 	% (Note that the representation can be printed out, if you call
 	% io__write(Var), so this is not entirely hidden from the user.)
-:- type var(T) ---> '$VAR'(var_rep(T))
+:- solver type var(T) ---> '$VAR'(var_rep(T))
 	where equality is (==).
 
 :- type var_rep(T)
only in patch2:
--- extras/clpr/cfloat.m	7 Nov 2002 05:38:38 -0000	1.35
+++ extras/clpr/cfloat.m	25 Jul 2003 00:01:48 -0000
@@ -1,5 +1,5 @@
 %-----------------------------------------------------------------------------%
-% Copyright (C) 1996-1997, 1999-2000 The University of Melbourne.
+% Copyright (C) 1996-1997, 1999-2000, 2003 The University of Melbourne.
 % This file may only be copied under the terms of the GNU Library General
 % Public License - see the file COPYING.LIB in the Mercury distribution.
 %-----------------------------------------------------------------------------%
@@ -44,7 +44,7 @@
 
 %-----------------------------------------------------------------------------%
 
-:- type cfloat.
+:- solver type cfloat.
 
 
 % NOTE:
@@ -349,7 +349,7 @@
 
 %----------------------------------------------------------------------------%
 
-:- type cfloat ---> cfloat(int)
+:- solver type cfloat ---> cfloat(int)
 	where equality is cfloat__eq.
 	% The cfloat is stored as an int (the CLP(R) solver_id for it).
 

-- 
David Overton                  Uni of Melbourne     +61 3 8344 1354
dmo at cs.mu.oz.au                Monash Uni (Clayton) +61 3 9905 5779
http://www.cs.mu.oz.au/~dmo    Mobile Phone         +61 4 0337 4393
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------