diff: bug fix for quantification problem

[Fergus Henderson]

On 21-Jan-1998, Andrew Bromage <bromage at cs.mu.OZ.AU> wrote:
> only_space_chars(Cs) :-
> 	all [C] list__member(C, Cs) => C = ' '.
> 
> produces the following error:
> 
> <<
> x.m:006: In predicate `x:only_space_chars/1':
> x.m:006:   warning: unresolved polymorphism.
> x.m:006:   The variable with an unbound type was:
> x.m:006:       C :: V_1
> x.m:006:   The unbound type variable(s) will be implicitly
> x.m:006:   bound to the builtin type `void'.
> >>
> 
> The problem is that the variable which is quantified (`C') is renamed
> apart from the occurrences of `C' in the body of the quantifier, so
> after quantification and simplification, it looks like this:
> 
> <<
> only_space_chars(Cs) :-
> 	\+ (
> 		some [C_3] (
> 			list__member(C_4, Cs),
> 			\+ (
> 				C_4 = ' '
> 			)
> 		)
> 	).
> >>
> 
> This is IMO counter-intuitive.

Estimated hours taken: 1

compiler/quantification.m:
	Fix a problem where the use of explicit quantifiers lead to
	spurious warnings about unbound type variables, by deleting
	explicit quantifiers during quantification (once the
	variables have been renamed apart, the explicit quantifiers
	are no longer needed).

tests/valid/Mmakefile:
tests/valid/explicit_quant.m:
	Regression test.

cvs diff  compiler/quantification.m tests/valid/Mmakefile tests/valid/explicit_quant.m
Index: compiler/quantification.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/quantification.m,v
retrieving revision 1.57
diff -u -r1.57 quantification.m
--- quantification.m	1998/01/13 10:13:31	1.57
+++ quantification.m	1998/01/21 05:55:30
@@ -171,12 +171,17 @@
 				hlds_goal_expr, quant_info, quant_info).
 :- mode implicitly_quantify_goal_2(in, in, out, in, out) is det.
 
-	% we retain explicit existential quantifiers in the source code,
-	% even though they are redundant with the goal_info non_locals,
-	% so that we can easily recalculate the goal_info non_locals
-	% if necessary after program transformation.
+	% After this pass, explicit quantifiers are redundant,
+	% since all variables which were explicitly quantified
+	% have been renamed apart.  So we don't keep them.
+	% We need to keep the structure, though, so that mode
+	% analysis doesn't try to reorder through quantifiers.
+	% (Actually it would make sense to allow mode analysis
+	% to do that, but there reference manual says it doesn't,
+	% so we don't.)  Thus we replace `some(Vars, Goal0)' with
+	% an empty quantifier `some([], Goal)'.
 
-implicitly_quantify_goal_2(some(Vars0, Goal0), Context, some(Vars, Goal)) -->
+implicitly_quantify_goal_2(some(Vars0, Goal0), Context, some([], Goal)) -->
 	quantification__get_outside(OutsideVars),
 	quantification__get_lambda_outside(LambdaOutsideVars),
 	quantification__get_quant_vars(QuantVars),
Index: tests/valid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/valid/Mmakefile,v
retrieving revision 1.8
diff -u -r1.8 Mmakefile
--- Mmakefile	1998/01/09 12:35:14	1.8
+++ Mmakefile	1998/01/21 06:00:07
@@ -29,6 +29,7 @@
 	empty_bound_inst_list.m \
 	empty_switch.m \
 	error.m \
+	explicit_quant.m \
 	fail_ite.m \
 	followcode_det_problem.m \
 	func_int_bug_main.m \
@@ -124,6 +125,7 @@
 GRADEFLAGS-agc_unused_in	= --gc accurate
 MCFLAGS-compl_unify_bug		= -O3
 MCFLAGS-double_vn		= -O4
+MCFLAGS-explicit_quant		= --halt-at-warn
 MCFLAGS-higher_order_implied_mode = -O-1
 MCFLAGS-inhibit_warn_test       = --inhibit-warnings --halt-at-warn
 MCFLAGS-livevals_seq		= -O5 --opt-space
Index: tests/valid/explicit_quant.m
===================================================================
RCS file: explicit_quant.m
diff -N explicit_quant.m
--- /dev/null	Thu Jan 22 18:12:30 1998
+++ explicit_quant.m	Wed Jan 21 16:59:38 1998
@@ -0,0 +1,11 @@
+:- module explict_quant.
+
+:- interface.
+:- import_module list, char.
+
+:- pred only_space_chars(list(char) :: in) is semidet.
+
+:- implementation.
+
+only_space_chars(Cs) :-
+	all [C] list__member(C, Cs) => C = ' '.

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