diff: Fix problem with quantifiers and double negation

[Fergus Henderson]

doc/reference_manual.texi:
compiler/make_hlds.m:
	Fix a problem reported by Dante Baldan <dba at info.fundp.ac.be>,
	where the use of `all [X] p(X) <=> q(X)' lead to spurious mode
	errors, due to failure to eliminate certain kinds of double
	negations: in particular, the compiler should convert
	negated conjunctions of negations into disjunctions.

tests/hard_coded/Mmakefile:
tests/hard_coded/quantifier.m:
tests/hard_coded/quantifier.exp:
	Add a regression test for the above change.

cvs diff -N compiler/make_hlds.m doc/reference_manual.texi tests/hard_coded/Mmakefile tests/hard_coded/quantifier.exp tests/hard_coded/quantifier.m
Index: compiler/make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.266
diff -u -r1.266 make_hlds.m
--- make_hlds.m	1998/06/09 02:13:32	1.266
+++ make_hlds.m	1998/06/11 00:33:34
@@ -3543,10 +3543,21 @@
 
 transform_goal_2(not(A0), _, VarSet0, Subst, Goal, VarSet, Info0, Info) -->
 	transform_goal(A0, VarSet0, Subst, A, VarSet, Info0, Info),
-	% eliminate double negations
-	{ A = not(Goal1) - _ ->
+	{
+		% eliminate double negations
+		A = not(Goal1) - _
+	->
 		Goal = Goal1
 	;
+		% convert negated conjunctions of negations
+		% into disjunctions
+		A = conj(NegatedGoals) - _,
+		all_negated(NegatedGoals, UnnegatedGoals)
+	->
+		goal_info_init(GoalInfo),
+		map__init(StoreMap),
+		Goal = disj(UnnegatedGoals, StoreMap) - GoalInfo
+	;
 		goal_info_init(GoalInfo),
 		Goal = not(A) - GoalInfo
 	}.
@@ -3653,6 +3664,13 @@
 	{ term__apply_substitution(B0, Subst, B) },
 	unravel_unification(A, B, Context, explicit, [],
 			VarSet0, Goal, VarSet, Info0, Info).
+
+:- pred all_negated(list(hlds_goal), list(hlds_goal)).
+:- mode all_negated(in, out) is semidet.
+
+all_negated([], []).
+all_negated([not(Goal) - _ | NegatedGoals], [Goal | Goals]) :-
+	all_negated(NegatedGoals, Goals).
 
 %-----------------------------------------------------------------------------
 
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.96
diff -u -r1.96 reference_manual.texi
--- reference_manual.texi	1998/05/30 19:32:08	1.96
+++ reference_manual.texi	1998/06/10 23:33:31
@@ -781,8 +781,14 @@
 can cause the introduction of double negations
 which could make otherwise well-formed code mode-incorrect.
 To avoid this problem, the language specifies that
-double negations are removed after syntax analysis,
-before mode analysis is performed.
+after syntax analysis, and before mode analysis is performed,
+the implementation must delete any double negations
+and must replace any negations of conjunctions of negations
+with disjunctions.  (Both of these transformations
+preserve the logical meaning and type-correctness of the code,
+and they preserve or improve mode-correctness:
+they never transform code fragments that would be
+well-moded into ones that would be ill-moded.)
 
 @node Types
 @chapter Types
Index: tests/hard_coded/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/hard_coded/Mmakefile,v
retrieving revision 1.32
diff -u -r1.32 Mmakefile
--- Mmakefile	1998/06/03 00:43:53	1.32
+++ Mmakefile	1998/06/12 07:01:26
@@ -61,6 +61,7 @@
 	qual_adv_test \
 	qual_basic_test \
 	qual_is_test \
+	quantifier \
 	quoting_bug_test \
 	rational_test \
 	relation_test \
Index: tests/hard_coded/quantifier.exp
===================================================================
RCS file: quantifier.exp
diff -N quantifier.exp
--- /dev/null	Fri Jun 12 17:01:25 1998
+++ quantifier.exp	Fri Jun 12 16:29:06 1998
@@ -0,0 +1 @@
+equivalent
Index: tests/hard_coded/quantifier.m
===================================================================
RCS file: quantifier.m
diff -N quantifier.m
--- /dev/null	Fri Jun 12 17:01:25 1998
+++ quantifier.m	Fri Jun 12 16:01:36 1998
@@ -0,0 +1,35 @@
+:- module quantifier.
+
+:- interface.
+
+:- import_module io.
+
+:- pred main(io__state::di,io__state::uo) is det.
+
+:- implementation.
+
+:- import_module list, int.
+
+:- pred sum(list(int),int).
+:- mode sum(in,out) is det.
+
+sum([],0).
+sum([X|L],X + N1) :- sum(L,N1). 
+
+
+:- pred foo(pred(int)).
+:- mode foo(free->pred(out) is det) is det.
+
+foo(sum([1,2,3])).
+
+
+main -->
+	( {P = lambda([X :: out] is det, X = 6),
+		foo(Q), 
+		all [X] (call(P,X) <=> call(Q,X))}
+	->
+		print("equivalent")
+	;
+		print("not equivalent")
+	), nl.
+

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