Fix a spurious warning bug reported by Mark Brown.

Estimated hours taken: 1.5

Fix a spurious warning bug reported by Mark Brown.

compiler/quantification.m:
	Change quantification.m so that for quantified variables from
	quantifiers in if-then-elses, after it has renamed apart all
	their occurrences, it eliminates the variables from the quantifier.
	This change matches what we currently do for the quantified
	variables in ordinary existentially quantication goals,
	and is needed to avoid spurious warnings about those
	variables having unbound types (their type remains unbound
	because after all occurrences have been renamed apart they don't
	actually occur anywhere in the goal anymore other than in the
	quantifier).

tests/valid/Mmakefile:
tests/valid/quantifier_warning.m:
	Add a regression test for the above bug-fix.
This commit is contained in:
Fergus Henderson
2000-02-18 07:44:59 +00:00
parent 4aee4cd2fb
commit 830e21e4a1
3 changed files with 44 additions and 1 deletions

View File

@@ -368,8 +368,13 @@ implicitly_quantify_goal_2(not(Goal0), _, not(Goal)) -->
quantification__set_outside(OutsideVars),
quantification__set_quant_vars(QuantVars).
% After this pass, explicit quantifiers are redundant,
% since all variables which were explicitly quantified
% have been renamed apart. So we don't keep them.
% Thus we replace `if_then_else(Vars, ....)' with
% `if_then_else([], ...)'.
implicitly_quantify_goal_2(if_then_else(Vars0, Cond0, Then0, Else0, SM),
Context, if_then_else(Vars, Cond, Then, Else, SM)) -->
Context, if_then_else([], Cond, Then, Else, SM)) -->
quantification__get_quant_vars(QuantVars),
quantification__get_outside(OutsideVars),
quantification__get_lambda_outside(LambdaOutsideVars),

View File

@@ -102,6 +102,7 @@ OTHER_SOURCES= \
parsing_bug_main.m \
pred_with_no_modes.m \
qualified_cons_id.m \
quantifier_warning.m \
same_length_2.m \
semidet_disj.m \
shape_type.m \
@@ -209,6 +210,7 @@ MCFLAGS-livevals_seq = -O5 --opt-space
MCFLAGS-middle_rec_labels = --middle-rec --no-follow-vars
MCFLAGS-mostly_uniq_mode_inf = --infer-all
MCFLAGS-pred_with_no_modes = --infer-all
MCFLAGS-quantifier_warning = --halt-at-warn
MCFLAGS-simplify_bug = -O-1
MCFLAGS-two_way_unif = -O-1
MCFLAGS-type_inf_ambig_test = --infer-all

View File

@@ -0,0 +1,36 @@
% The compiler used to issue a spurious warning
% about `M' having an unbound type.
:- module quantifier_warning.
:- interface.
:- import_module io.
:- pred main(io__state::di, io__state::uo) is det.
:- implementation.
:- import_module std_util, int, bool.
main -->
{ p(1, R) },
io__write(R),
io__nl.
:- pred p(int::in, bool::out) is det.
p(N, R) :-
(
some [M] (
M > 5,
q(N, M)
)
->
R = yes
;
R = no
).
:- pred q(int::in, int::out) is nondet.
q(0, 0).
q(1, 1).
q(1, 2).
q(1, 3).
q(2, 2).
q(2, 4).