[m-dev.] for review: fix quantification of "<=>" [1/2]

[Fergus Henderson]

Estimated hours taken: 10

Handle quantification analysis of bi-implication (`<=>') goals correctly.
Previously we used to expand bi-implications before doing quantification
analysis, which stuffed up the results of quantification analysis for
those goals.  We need to do quantification analysis first, and only
then can we expand bi-implications.  In addition, elimination of double
negation needs to come after expansion of bi-implication, so I moved
that from make_hlds.m to purity.m.

compiler/hlds_goal.m:
	Add a new alternative to the HLDS goal type for bi-implications.
	Also add a new predicate negate_goal, for use by purity.m.

compiler/make_hlds.m:
	Don't expand bi-implication here, instead just use the new
	bi_implication/2 HLDS goal type.
	Don't eliminated double negation here.
	
compiler/quantification.m:
	Handle quantification for bi-implications.
	Expand bi-implications.

compiler/purity.m:
	Eliminate double negation.

compiler/hlds_out.m:
	Add code to print out bi-implication goals.

compiler/*.m:
	Trivial changes to handle the new bi_implication/2
	alternative in the HLDS goal type.

compiler/notes/compiler_design.html:
	Document the above changes.

tests/hard_coded/Mmakefile:
tests/hard_coded/quantifier2.m:
tests/hard_coded/quantifier2.exp:
	A regression test for the above change.

Workspace: /d-drive/home/hg/fjh/mercury
Index: compiler/assertion.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/assertion.m,v
retrieving revision 1.2
diff -u -d -r1.2 assertion.m
--- compiler/assertion.m	1999/09/12 04:26:37	1.2
+++ compiler/assertion.m	1999/10/21 13:48:32
@@ -211,6 +211,10 @@
 	equal_vars(VarsA, VarsB, Subst0, Subst).
 equal_goals(par_conj(GoalAs, _) - _, par_conj(GoalBs, _) - _, Subst0, Subst) :-
 	equal_goals_list(GoalAs, GoalBs, Subst0, Subst).
+equal_goals(bi_implication(LeftGoalA, RightGoalA) - _,
+	    bi_implication(LeftGoalB, RightGoalB) - _, Subst0, Subst) :-
+	equal_goals(LeftGoalA, LeftGoalB, Subst0, Subst1),
+	equal_goals(RightGoalA, RightGoalB, Subst1, Subst).
 
 :- pred equal_vars(prog_vars::in, prog_vars::in, subst::in,
 		subst::out) is semidet.
@@ -324,6 +328,10 @@
 	assertion__normalise_goal(Else0, Else).
 assertion__normalise_goal(par_conj(Goal0s,B) - GI, par_conj(Goals,B) - GI) :-
 	assertion__normalise_goals(Goal0s, Goals).
+assertion__normalise_goal(bi_implication(LHS0, RHS0) - GI,
+		bi_implication(LHS, RHS) - GI) :-
+	assertion__normalise_goal(LHS0, LHS),
+	assertion__normalise_goal(RHS0, RHS).
 
 %-----------------------------------------------------------------------------%
 
@@ -409,6 +417,10 @@
 	assertion__in_interface_check(Else, PredInfo, ModuleInfo).
 assertion__in_interface_check(par_conj(Goals,_) - _, PredInfo, ModuleInfo) -->
 	assertion__in_interface_check_list(Goals, PredInfo, ModuleInfo).
+assertion__in_interface_check(bi_implication(LHS, RHS) - _, PredInfo,
+		ModuleInfo) -->
+	assertion__in_interface_check(LHS, PredInfo, ModuleInfo),
+	assertion__in_interface_check(RHS, PredInfo, ModuleInfo).
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/dependency_graph.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/dependency_graph.m,v
retrieving revision 1.43
diff -u -d -r1.43 dependency_graph.m
--- compiler/dependency_graph.m	1999/07/13 08:52:47	1.43
+++ compiler/dependency_graph.m	1999/10/21 11:08:20
@@ -275,6 +275,11 @@
 dependency_graph__add_arcs_in_goal_2(pragma_c_code(_, _, _, _, _, _, _), _,
 	DepGraph, DepGraph).
 
+dependency_graph__add_arcs_in_goal_2(bi_implication(LHS, RHS), Caller, 
+		DepGraph0, DepGraph) :-
+	dependency_graph__add_arcs_in_list([LHS, RHS], Caller,
+			DepGraph0, DepGraph).
+
 %-----------------------------------------------------------------------------%
 
 :- pred dependency_graph__add_arcs_in_list(list(hlds_goal), relation_key,
@@ -688,6 +693,9 @@
 		Map, Map) --> [].
 process_aditi_goal(_IsNeg, pragma_c_code(_, _, _, _, _, _, _) - _,
 		Map, Map) --> [].
+process_aditi_goal(_, bi_implication(_, _) - _, _, _) -->
+	% these should have been expanded out by now
+	{ error("process_aditi_goal: unexpected bi_implication") }.
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/dnf.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/dnf.m,v
retrieving revision 1.37
diff -u -d -r1.37 dnf.m
--- compiler/dnf.m	1999/07/13 08:52:50	1.37
+++ compiler/dnf.m	1999/10/21 16:33:06
@@ -240,6 +240,10 @@
 		ModuleInfo = ModuleInfo0,
 		NewPredIds = NewPredIds0,
 		Goal = Goal0
+	;
+		GoalExpr0 = bi_implication(_, _),
+		% these should have been expanded out by now
+		error("dnf__transform_goal: unexpected bi_implication")
 	).
 
 %-----------------------------------------------------------------------------%
@@ -468,6 +472,7 @@
 	).
 dnf__is_atomic_expr(_, _, _, if_then_else(_, _, _, _, _), no).
 dnf__is_atomic_expr(_, _, _, pragma_c_code(_, _, _, _, _, _, _), yes).
+dnf__is_atomic_expr(_, _, _, bi_implication(_, _), no).
 
 :- pred dnf__free_of_nonatomic(hlds_goal::in,
 	set(pred_proc_id)::in) is semidet.
Index: compiler/goal_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/goal_util.m,v
retrieving revision 1.58
diff -u -d -r1.58 goal_util.m
--- compiler/goal_util.m	1999/10/15 03:44:44	1.58
+++ compiler/goal_util.m	1999/10/21 14:53:56
@@ -368,6 +368,11 @@
 		pragma_c_code(A,B,C,Vars,E,F,G)) :-
 	goal_util__rename_var_list(Vars0, Must, Subn, Vars).
 
+goal_util__name_apart_2(bi_implication(LHS0, RHS0), Must, Subn,
+		bi_implication(LHS, RHS)) :-
+	goal_util__rename_vars_in_goal(LHS0, Must, Subn, LHS),
+	goal_util__rename_vars_in_goal(RHS0, Must, Subn, RHS).
+
 %-----------------------------------------------------------------------------%
 
 :- pred goal_util__name_apart_list(list(hlds_goal), bool,
@@ -591,6 +596,10 @@
 		Set0, Set) :-
 	set__insert_list(Set0, ArgVars, Set).
 
+goal_util__goal_vars_2(bi_implication(LHS - _, RHS - _), Set0, Set) :-
+	goal_util__goal_vars_2(LHS, Set0, Set1),
+	goal_util__goal_vars_2(RHS, Set1, Set).
+
 goal_util__goals_goal_vars([], Set, Set).
 goal_util__goals_goal_vars([Goal - _ | Goals], Set0, Set) :-
 	goal_util__goal_vars_2(Goal, Set0, Set1),
@@ -728,6 +737,10 @@
 goal_expr_size(generic_call(_, _, _, _), 1).
 goal_expr_size(unify(_, _, _, _, _), 1).
 goal_expr_size(pragma_c_code(_, _, _, _, _, _, _), 1).
+goal_expr_size(bi_implication(LHS, RHS), Size) :-
+	goal_size(LHS, Size1),
+	goal_size(RHS, Size2),
+	Size is Size1 + Size2 + 1.
 
 %-----------------------------------------------------------------------------%
 %
Index: compiler/hlds_goal.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_goal.m,v
retrieving revision 1.63
diff -u -d -r1.63 hlds_goal.m
--- compiler/hlds_goal.m	1999/09/12 04:26:41	1.63
+++ compiler/hlds_goal.m	1999/10/21 14:55:52
@@ -29,7 +29,7 @@
 	--->	conj(hlds_goals)
 
 		% A predicate call.
-		% Initially only the sym_name and arguments
+		% Initially only the sym_name, arguments, and context
 		% are filled in. Type analysis fills in the
 		% pred_id. Mode analysis fills in the
 		% proc_id and the builtin_state field.
@@ -179,12 +179,28 @@
 					% pragma_c_codes; none for others.
 		)
 
+		% parallel conjunction
 	;	par_conj(hlds_goals, store_map)
-					% parallel conjunction
 					% The store_map specifies the locations
 					% in which live variables should be
 					% stored at the start of the parallel
 					% conjunction.
+
+		% bi-implication (A <=> B)
+		%
+		% These get eliminated by quantification.m,
+		% so most passes of the compiler will just call error/1
+		% if they occur.
+		%
+		% Note that ordinary implications (A => B)
+		% and reverse implications (A <= B) are expanded
+		% out before we construct the HLDS.  But we can't
+		% do that for bi-implications, because if expansion
+		% of bi-implications is done before implicit quantification,
+		% then the quantification would be wrong.
+
+	;	bi_implication(hlds_goal, hlds_goal)
+
 	.
 
 :- type generic_call
@@ -880,6 +896,11 @@
 :- pred conjoin_goals(hlds_goal, hlds_goal, hlds_goal).
 :- mode conjoin_goals(in, in, out) is det.
 
+	% Negate a goal, eliminating double negations as we go.
+	%
+:- pred negate_goal(hlds_goal, hlds_goal_info, hlds_goal).
+:- mode negate_goal(in, in, out) is det.
+
 	% A goal is atomic iff it doesn't contain any sub-goals
 	% (except possibly goals inside lambda expressions --
 	% but lambda expressions will get transformed into separate
@@ -1242,6 +1263,37 @@
 	),
 	conjoin_goal_and_goal_list(Goal1, GoalList, Goal).
 	
+	% Negate a goal, eliminating double negations as we go.
+
+negate_goal(Goal, GoalInfo, NegatedGoal) :-
+	(
+		% eliminate double negations
+		Goal = not(Goal1) - _
+	->
+		NegatedGoal = Goal1
+	;
+		% convert negated conjunctions of negations
+		% into disjunctions
+		Goal = conj(NegatedGoals) - _,
+		all_negated(NegatedGoals, UnnegatedGoals)
+	->
+		map__init(StoreMap),
+		NegatedGoal = disj(UnnegatedGoals, StoreMap) - GoalInfo
+	;
+		NegatedGoal = not(Goal) - GoalInfo
+	).
+
+:- 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).
+all_negated([conj(NegatedConj) - _GoalInfo | NegatedGoals], Goals) :-
+	all_negated(NegatedConj, Goals1),
+	all_negated(NegatedGoals, Goals2),
+	list__append(Goals1, Goals2, Goals).
+
 %-----------------------------------------------------------------------------%
 
 goal_is_atomic(conj([])).
@@ -1345,6 +1397,10 @@
 	Goal = unify(_, _, _, _, _).
 set_goal_contexts_2(_, Goal, Goal) :-
 	Goal = pragma_c_code(_, _, _, _, _, _, _).
+set_goal_contexts_2(Context, bi_implication(LHS0, RHS0),
+		bi_implication(LHS, RHS)) :-
+	set_goal_contexts(Context, LHS0, LHS),
+	set_goal_contexts(Context, RHS0, RHS).
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/hlds_out.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_out.m,v
retrieving revision 1.227
diff -u -d -r1.227 hlds_out.m
--- compiler/hlds_out.m	1999/10/15 03:44:46	1.227
+++ compiler/hlds_out.m	1999/10/21 11:25:52
@@ -1539,6 +1539,21 @@
 	io__write_string(")"),
 	io__write_string(Follow).
 
+hlds_out__write_goal_2(bi_implication(LHS, RHS), ModuleInfo, VarSet,
+		AppendVarnums, Indent, Follow, TypeQual) -->
+	hlds_out__write_indent(Indent),
+	io__write_string("( % bi-implication\n"),
+	{ Indent1 is Indent + 1 },
+	hlds_out__write_goal_a(LHS, ModuleInfo, VarSet, AppendVarnums,
+		Indent1, "\n", TypeQual),
+	hlds_out__write_indent(Indent),
+	io__write_string("<=>\n"),
+	hlds_out__write_goal_a(RHS, ModuleInfo, VarSet, AppendVarnums,
+		Indent1, "\n", TypeQual),
+	hlds_out__write_indent(Indent),
+	io__write_string(")"),
+	io__write_string(Follow).
+
 :- pred hlds_out__write_varnum_list(list(prog_var), io__state, io__state).
 :- mode hlds_out__write_varnum_list(in, di, uo) is det.
 
Index: compiler/make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.310
diff -u -d -r1.310 make_hlds.m
--- compiler/make_hlds.m	1999/10/14 04:27:52	1.310
+++ compiler/make_hlds.m	1999/10/21 16:47:36
@@ -4014,6 +4014,12 @@
 	warn_singletons_in_pragma_c_code(PragmaImpl, ArgInfo, Context, 
 		PredCallId, MI).
 
+warn_singletons_in_goal_2(bi_implication(LHS, RHS), _GoalInfo, QuantVars,
+		VarSet, PredCallId, MI) -->
+	warn_singletons_in_goal_list([LHS, RHS], QuantVars, VarSet,
+		PredCallId, MI).
+
+
 :- pred warn_singletons_in_goal_list(list(hlds_goal), set(prog_var),
 		prog_varset, simple_call_id, module_info,
 		io__state, io__state).
@@ -4661,24 +4667,8 @@
 
 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) - _
-	->
-		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
-	}.
+	{ goal_info_init(GoalInfo) },
+	{ Goal = not(A) - GoalInfo }.
 
 transform_goal_2((A0,B0), _, VarSet0, Subst, Goal, VarSet, Info0, Info) -->
 	get_conj(B0, Subst, [], VarSet0, L0, VarSet1, Info0, Info1),
@@ -4705,13 +4695,19 @@
 	transform_goal_2(TransformedGoal, Context, VarSet0, Subst,
 		Goal, VarSet, Info0, Info).
 
-transform_goal_2(equivalent(P, Q), Context, VarSet0, Subst, Goal, VarSet,
+transform_goal_2(equivalent(P0, Q0), _Context, VarSet0, Subst, Goal, VarSet,
 		Info0, Info) -->
-		% `P <=> Q' is defined as `(P => Q), (Q => P)'
-	{ TransformedGoal = (implies(P, Q) - Context,
-				implies(Q, P) - Context) },
-	transform_goal_2(TransformedGoal, Context, VarSet0, Subst,
-		Goal, VarSet, Info0, Info).
+	%
+	% `P <=> Q' is defined as `(P => Q), (Q => P)',
+	% but that transformation must not be done until
+	% after quantification analysis, lest the duplication of
+	% the goals concerned affect the implicit quantification
+	% of the variables inside them.
+	%
+	{ goal_info_init(GoalInfo) },
+	transform_goal(P0, VarSet0, Subst, P, VarSet1, Info0, Info1),
+	transform_goal(Q0, VarSet1, Subst, Q, VarSet, Info1, Info),
+	{ Goal = bi_implication(P, Q) - GoalInfo }.
 
 transform_goal_2(call(Name, Args0, Purity), Context, VarSet0, Subst, Goal,
 		VarSet, Info0, Info) -->
@@ -4801,18 +4797,6 @@
 	{ 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).
-% nested conjunctions shouldn't occur here anyway, but just in case...
-all_negated([conj(NegatedConj) - _GoalInfo | NegatedGoals], Goals) :-
-	all_negated(NegatedConj, Goals1),
-	all_negated(NegatedGoals, Goals2),
-	list__append(Goals1, Goals2, Goals).
 
 :- inst aditi_update_str =
 	bound(	"aditi_insert"
Index: compiler/purity.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/purity.m,v
retrieving revision 1.19
diff -u -d -r1.19 purity.m
--- compiler/purity.m	1999/09/12 04:26:51	1.19
+++ compiler/purity.m	1999/10/21 17:12:08
@@ -25,7 +25,11 @@
 %  so they need to be a separate "post-typecheck pass"; they are done
 %  here in combination with the purity-analysis pass for efficiency reasons.
 %
+%  We also do elimination of double-negation in this pass.
+%  It needs to be done somewhere after quantification analysis and
+%  before mode analysis, and this is convenient place to do it.
 %
+%
 %  The aim of Mercury's purity system is to allow one to declare certain parts
 %  of one's program to be impure, thereby forbidding the compiler from making
 %  certain optimizations to that part of the code.  Since one can often
@@ -508,10 +512,21 @@
 		ModuleInfo, InClosure, Purity, NumErrors0, NumErrors) -->
 	compute_goals_purity(Goals0, Goals, PredInfo, ModuleInfo,
 			     InClosure, pure, Purity, NumErrors0, NumErrors).
-compute_expr_purity(not(Goal0), not(Goal), _, PredInfo, ModuleInfo,
+compute_expr_purity(not(Goal0), NotGoal, GoalInfo0, PredInfo, ModuleInfo,
 		InClosure, Purity, NumErrors0, NumErrors) -->
-	compute_goal_purity(Goal0, Goal, PredInfo, ModuleInfo, 
-			    InClosure, Purity, NumErrors0, NumErrors).
+	%
+	% eliminate double negation
+	%
+	{ negate_goal(Goal0, GoalInfo0, NotGoal0) },
+	( { NotGoal0 = not(Goal1) - _GoalInfo1 } ->
+		compute_goal_purity(Goal1, Goal, PredInfo, ModuleInfo, 
+				    InClosure, Purity, NumErrors0, NumErrors),
+		{ NotGoal = not(Goal) }
+	;
+		compute_goal_purity(NotGoal0, NotGoal1, PredInfo, ModuleInfo, 
+				    InClosure, Purity, NumErrors0, NumErrors),
+		{ NotGoal1 = NotGoal - _ }
+	).
 compute_expr_purity(some(Vars, CanRemove, Goal0), some(Vars, CanRemove, Goal),
 		_, PredInfo, ModuleInfo, InClosure, Purity,
 		NumErrors0, NumErrors) -->
@@ -534,6 +549,9 @@
 	{ module_info_preds(ModuleInfo, Preds) },
 	{ map__lookup(Preds, PredId, PredInfo) },
 	{ pred_info_get_purity(PredInfo, Purity) }.
+compute_expr_purity(bi_implication(_, _), _, _, _, _, _, _, _, _) -->
+	% these should have been expanded out by now
+	{ error("compute_expr_purity: unexpected bi_implication") }.
 
 :- pred compute_goal_purity(hlds_goal, hlds_goal, pred_info,
 	module_info, bool, purity, int, int, io__state, io__state).
Index: compiler/quantification.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/quantification.m,v
retrieving revision 1.68
diff -u -d -r1.68 quantification.m
--- compiler/quantification.m	1999/07/13 08:53:26	1.68
+++ compiler/quantification.m	1999/10/24 15:32:11
@@ -12,6 +12,10 @@
 	% For the rules on implicit quantification, see the
 	% Mercury language reference manual.
 	%
+	% This pass also expands out bi-implications (that has to be
+	% done after quantification, and preferably as soon as possible,
+	% so we do it here).
+	%
 	% Rather than making implicit quantification explicit by
 	% inserting additional existential quantifiers in the form of
 	% `some/2' goals, we instead record existential quantification
@@ -353,6 +357,82 @@
 		pragma_c_code(A,B,C,Vars,E,F,G)) --> 
 	implicitly_quantify_atomic_goal(Vars).
 
+implicitly_quantify_goal_2(bi_implication(LHS0, RHS0), Context, Goal) -->
+		% get the initial values of various settings
+	quantification__get_quant_vars(QuantVars0),
+	quantification__get_outside(OutsideVars0),
+	quantification__get_lambda_outside(LambdaOutsideVars0),
+
+		% quantified variables cannot be pushed inside a negation,
+		% so we insert the quantified vars into the outside vars set,
+		% and initialize the new quantified vars set to be empty
+		% (the lambda outside vars remain unchanged)
+	{ set__union(OutsideVars0, QuantVars0, OutsideVars1) },
+	{ set__init(QuantVars1) },
+	{ LambdaOutsideVars1 = LambdaOutsideVars0 },
+	quantification__set_quant_vars(QuantVars1),
+
+		% prepare for quantifying the LHS:
+		% add variables from the RHS to the outside vars
+		% and the outside lambda vars sets.
+	{ quantification__goal_vars(RHS0, RHS_Vars, RHS_LambdaVars) },
+	{ set__union(OutsideVars1, RHS_Vars, LHS_OutsideVars) },
+	{ set__union(LambdaOutsideVars1, RHS_LambdaVars,
+			LHS_LambdaOutsideVars) },
+
+		% quantify the LHS
+	quantification__set_outside(LHS_OutsideVars),
+	quantification__set_lambda_outside(LHS_LambdaOutsideVars),
+	implicitly_quantify_goal(LHS0, LHS),
+	quantification__get_nonlocals(LHS_NonLocalVars),
+
+		% prepare for quantifying the RHS:
+		% add nonlocals from the LHS to the outside vars.
+		% (We use the nonlocals rather than the more symmetric
+		% approach of calling quantification__goal_vars on the
+		% LHS goal because it is more efficient.)
+	{ set__union(OutsideVars1, LHS_NonLocalVars, RHS_OutsideVars) },
+	{ RHS_LambdaOutsideVars = LambdaOutsideVars1 },
+
+		% quantify the RHS
+	quantification__set_outside(RHS_OutsideVars),
+	quantification__set_lambda_outside(RHS_LambdaOutsideVars),
+	implicitly_quantify_goal(RHS0, RHS),
+	quantification__get_nonlocals(RHS_NonLocalVars),
+
+		% compute the nonlocals for this goal
+	{ set__union(LHS_NonLocalVars, RHS_NonLocalVars, AllNonLocalVars) },
+	{ set__intersect(AllNonLocalVars, OutsideVars0, NonLocalVarsO) },
+	{ set__intersect(AllNonLocalVars, LambdaOutsideVars0, NonLocalVarsL) },
+	{ set__union(NonLocalVarsO, NonLocalVarsL, NonLocalVars) },
+	quantification__set_nonlocals(NonLocalVars),
+
+		% restore the original values of various settings
+	quantification__set_outside(OutsideVars0),
+	quantification__set_lambda_outside(LambdaOutsideVars0),
+	quantification__set_quant_vars(QuantVars0),
+
+		%
+		% We've figured out the quantification.
+		% Now expand the bi-implication according to the usual
+		% rules:
+		%	LHS <=> RHS
+		% ===>
+		%	(LHS => RHS), (RHS => LHS)
+		% ===>
+		%	(not (LHS, not RHS)), (not (RHS, not LHS))
+		%
+	{ goal_info_init(GoalInfo0) },
+	{ goal_info_set_context(GoalInfo0, Context, GoalInfo1) },
+	{ goal_info_set_nonlocals(GoalInfo1, LHS_NonLocalVars, LHS_GI) },
+	{ goal_info_set_nonlocals(GoalInfo1, RHS_NonLocalVars, RHS_GI) },
+	{ goal_info_set_nonlocals(GoalInfo1, NonLocalVars, GI) },
+	{ NotLHS = not(LHS) - LHS_GI },
+	{ NotRHS = not(RHS) - RHS_GI },
+	{ ForwardsImplication = not(conj([LHS, NotRHS]) - GI) - GI },
+	{ ReverseImplication = not(conj([RHS, NotLHS]) - GI) - GI },
+	{ Goal = conj([ForwardsImplication, ReverseImplication]) }.
+
 :- pred implicitly_quantify_atomic_goal(list(prog_var), quant_info, quant_info).
 :- mode implicitly_quantify_atomic_goal(in, in, out) is det.
 
@@ -715,6 +795,10 @@
 quantification__goal_vars_2(pragma_c_code(_, _, _, ArgVars, _, _, _),
 		Set0, LambdaSet, Set, LambdaSet) :-
 	set__insert_list(Set0, ArgVars, Set).
+
+quantification__goal_vars_2(bi_implication(LHS, RHS), Set0, LambdaSet0, Set,
+		LambdaSet) :-
+	goal_list_vars_2([LHS, RHS], Set0, LambdaSet0, Set, LambdaSet).
 
 :- pred quantification__unify_rhs_vars(unify_rhs, set(prog_var), set(prog_var),
 					set(prog_var), set(prog_var)).
Index: compiler/typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
retrieving revision 1.265
diff -u -d -r1.265 typecheck.m
--- compiler/typecheck.m	1999/07/22 17:14:39	1.265
+++ compiler/typecheck.m	1999/10/21 16:22:40
@@ -978,6 +978,10 @@
 		OrigTypeAssignSet) },
 	typecheck_call_pred_id(PredId, Args),
 	perform_context_reduction(OrigTypeAssignSet).
+typecheck_goal_2(bi_implication(LHS0, RHS0), bi_implication(LHS, RHS)) -->
+	checkpoint("<=>"),
+	typecheck_goal(LHS0, LHS),
+	typecheck_goal(RHS0, RHS).
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/notes/compiler_design.html
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/notes/compiler_design.html,v
retrieving revision 1.39
diff -u -d -r1.39 compiler_design.html
--- compiler/notes/compiler_design.html	1999/10/14 05:27:35	1.39
+++ compiler/notes/compiler_design.html	1999/10/21 16:01:22
@@ -206,6 +206,9 @@
 
 	make_hlds.m transforms the code into superhomogeneous form,
 	and at the same time converts the parse tree into the HLDS.
+	It expands away universal quantification
+	(using `all [Vs] G' ===> `not (some [Vs] (not G))')
+	and implication (using `A => B' ===> `not(A, not B)').
 	It converts `pragma import', `pragma c_code' and `pragma fact_table'
 	declarations into clauses with HLDS `pragma_c_code'
 	instructions for bodies.
@@ -258,7 +261,10 @@
 	<dd>
 	quantification.m handles implicit quantification and computes
 	the set of non-local variables for each sub-goal.
-    This is done in transform in make_hlds.m
+	It also expands away bi-implication (unlike the expansion
+	of implication and universal quantification, this expansion
+	cannot be done until after quantification).
+	This pass is called from the `transform' predicate in make_hlds.m.
 
 <dt> checking typeclass instances (check_typeclass.m)
 	<dd>
@@ -324,6 +330,8 @@
 	complete the handling of predicate
 	overloading for cases which typecheck.m is unable to handle,
 	and to check for unbound type variables.
+	Elimination of double negation is also done here; that needs to
+	be done after quantification analysis and before mode analysis.
 
 <dt> polymorphism transformation
 
Index: tests/hard_coded/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/hard_coded/Mmakefile,v
retrieving revision 1.67
diff -u -d -r1.67 Mmakefile
--- tests/hard_coded/Mmakefile	1999/10/19 04:11:43	1.67
+++ tests/hard_coded/Mmakefile	1999/10/24 15:30:26
@@ -80,6 +80,7 @@
 	qual_basic_test \
 	qual_is_test \
 	quantifier \
+	quantifier2 \
 	quoting_bug_test \
 	rational_test \
 	relation_test \
cvs diff: tests/hard_coded/quantifier2.exp is a new entry, no comparison available
cvs diff: tests/hard_coded/quantifier2.m is a new entry, no comparison available
====================
tests/hard_coded/quantifier2.exp
====================
yes
====================
tests/hard_coded/quantifier2.m
====================
:- module quantifier2.

:- interface.

:- import_module io.

:- pred main(io__state::di,io__state::uo) is det.

:- implementation.

:- import_module list, int.

:- pred testsum(list(int),int,int).
:- mode testsum(in,in,out) is semidet.

testsum([],I,0) :- I > 0.
testsum([X|L],I,X + N1) :- testsum(L,I,N1). 


:- pred foo(pred(int, int)).
:- mode foo(free->pred(in, out) is semidet) is det.

foo(testsum([1,2,3])).


main -->
	(
		{ P = lambda([I :: in, X :: out] is semidet, (I > 0, X = 6)),
		  foo(Q), 
		  J = 1,
		  (call(P,J,_X) <=> call(Q,J,_Y)) }
	->
		print("yes"), nl
	;
		print("no"), nl
	).

====================

[continued in part 2]

-- 
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.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------