for review: switch detection & implicit quantification

[Fergus Henderson]

Hi,

Any objections to this change?

--------------------

Fix a problem reported by Baudouin Le Charlier <ble at info.fundp.ac.be>
where switch detection was getting confused by explicit existential
quantifications.

compiler/switch_detection.m:
	When detecting switches, traverse through some/2 goals.
	Also simplify the code a bit.

tests/valid/Mmakefile:
tests/valid/some_switch.m:
	Regression test for the above change.

Index: switch_detection.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/switch_detection.m,v
retrieving revision 1.80
diff -u -r1.80 switch_detection.m
--- switch_detection.m	1998/02/12 01:17:49	1.80
+++ switch_detection.m	1998/05/11 19:59:03
@@ -369,15 +369,12 @@
 
 partition_disj_trial([], _Var, Left, Left, Cases, Cases).
 partition_disj_trial([Goal0 | Goals], Var, Left0, Left, Cases0, Cases) :-
-	goal_to_conj_list(Goal0, ConjList0),
-	Goal0 = _ - GoalInfo,
 	map__init(Substitution),
-	find_bind_var_for_switch(ConjList0, Substitution, Var,
-			ConjList, _NewSubstitution, MaybeFunctor),
+	find_bind_var_for_switch(Goal0, Substitution, Var,
+			Goal, _NewSubstitution, MaybeFunctor),
 	(
 		MaybeFunctor = yes(Functor),
 		Left1 = Left0,
-		conj_list_to_goal(ConjList, GoalInfo, Goal),
 		( map__search(Cases0, Functor, DisjList0) ->
 			DisjList1 = [Goal | DisjList0],
 			map__det_update(Cases0, Functor, DisjList1, Cases1)
@@ -392,8 +389,10 @@
 	),
 	partition_disj_trial(Goals, Var, Left1, Left, Cases1, Cases).
 
-	% find_bind_var_for_switch(Goals0, Subst0, Var, Goals, Subst,
-	%	MaybeFunctor):
+	% find_bind_var_for_switch(Goal0, Subst0, Var, Goal, Subst,
+	%		MaybeFunctor):
+	% conj_find_bind_var_for_switch(Goals0, Subst0, Var, Goals, Subst,
+	%		MaybeFunctor):
 	%	Searches through Goals0 looking for a deconstruction
 	%	unification with `Var'. If found, sets `MaybeFunctor'
 	% 	to `yes(Functor)', where Functor is the
@@ -403,25 +402,20 @@
 	%	`MaybeFunctor' to `no', and computes `Subst' as the
 	%	resulting substitution from interpreting through the goal.
 
-:- pred find_bind_var_for_switch(list(hlds_goal), substitution, var,
-	list(hlds_goal), substitution, maybe(cons_id)).
+:- pred find_bind_var_for_switch(hlds_goal, substitution, var,
+	hlds_goal, substitution, maybe(cons_id)).
 :- mode find_bind_var_for_switch(in, in, in, out, out, out) is det.
 
-find_bind_var_for_switch([], Substitution, _Var, [], Substitution, no).
-find_bind_var_for_switch([Goal0 - GoalInfo | Goals0], Substitution0, Var,
-		[Goal - GoalInfo | Goals], Substitution, MaybeFunctor) :-
-	( Goal0 = conj(SubGoals0) ->
-		find_bind_var_for_switch(SubGoals0, Substitution0, Var,
-			SubGoals, Substitution1, MaybeFunctor1),
-		Goal = conj(SubGoals),
-		( MaybeFunctor1 = yes(_) ->
-			Goals = Goals0,
-			Substitution = Substitution1,
-			MaybeFunctor = MaybeFunctor1
-		;
-			find_bind_var_for_switch(Goals0, Substitution1, Var,
-				Goals, Substitution, MaybeFunctor)
-		)
+find_bind_var_for_switch(Goal0 - GoalInfo, Substitution0, Var,
+		Goal - GoalInfo, Substitution, MaybeFunctor) :-
+	( Goal0 = some(Vars, SubGoal0) ->
+		find_bind_var_for_switch(SubGoal0, Substitution0, Var,
+			SubGoal, Substitution, MaybeFunctor),
+		Goal = some(Vars, SubGoal)
+	; Goal0 = conj(SubGoals0) ->
+		conj_find_bind_var_for_switch(SubGoals0, Substitution0, Var,
+			SubGoals, Substitution, MaybeFunctor),
+		Goal = conj(SubGoals)
 	; Goal0 = unify(A, B, C, UnifyInfo0, E) ->
 			% check whether the unification is a deconstruction
 			% unification on Var or a variable aliased to Var
@@ -440,26 +434,41 @@
 			UnifyInfo = deconstruct(UnifyVar, Functor, F, G,
 				cannot_fail),
 			Goal = unify(A, B, C, UnifyInfo, E),
-			Goals = Goals0,
 			Substitution = Substitution0
 		;
 			% otherwise abstractly interpret the unification
-			% and continue
+			MaybeFunctor = no,
 			Goal = Goal0,
 			( interpret_unify(A, B, Substitution0, Substitution1) ->
-				Substitution2 = Substitution1
+				Substitution = Substitution1
 			;
 				% the unification must fail - just ignore it
-				Substitution2 = Substitution0
-			),
-			find_bind_var_for_switch(Goals0, Substitution2, Var,
-				Goals, Substitution, MaybeFunctor)
+				Substitution = Substitution0
+			)
 		)
 	;
 		Goal = Goal0,
-		Goals = Goals0,
 		Substitution = Substitution0,
 		MaybeFunctor = no
+	).
+
+:- pred conj_find_bind_var_for_switch(list(hlds_goal), substitution, var,
+	list(hlds_goal), substitution, maybe(cons_id)).
+:- mode conj_find_bind_var_for_switch(in, in, in, out, out, out) is det.
+
+conj_find_bind_var_for_switch([], Substitution, _Var, [], Substitution, no).
+conj_find_bind_var_for_switch([Goal0 | Goals0], Substitution0, Var,
+		[Goal | Goals], Substitution, MaybeFunctor) :-
+	find_bind_var_for_switch(Goal0,
+		Substitution0, Var,
+		Goal, Substitution1, MaybeFunctor1),
+	( MaybeFunctor1 = yes(_) ->
+		Goals = Goals0,
+		Substitution = Substitution1,
+		MaybeFunctor = MaybeFunctor1
+	;
+		conj_find_bind_var_for_switch(Goals0, Substitution1, Var,
+			Goals, Substitution, MaybeFunctor)
 	).
 
 :- pred cases_to_switch(sorted_case_list, var, map(var, type), hlds_goal_info,
Index: ../tests/valid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/valid/Mmakefile,v
retrieving revision 1.14
diff -u -r1.14 Mmakefile
--- Mmakefile	1998/03/30 13:25:04	1.14
+++ Mmakefile	1998/05/11 19:59:04
@@ -78,6 +78,7 @@
 	shape_type.m \
 	simplify_bug.m \
 	soln_context.m \
+	some_switch.m \
 	stack_alloc.m \
 	subtype_switch.m \
 	switches.m \
Index: ../tests/valid/some_switch.m
===================================================================
RCS file: some_switch.m
diff -N some_switch.m
--- /dev/null	Wed May 28 10:49:58 1997
+++ some_switch.m	Tue May 12 06:00:25 1998
@@ -0,0 +1,18 @@
+% Test of switch detection with explicit existential quantification.
+
+:- module some_switch.
+:- interface.
+
+:- type nat ---> o ; s(nat).
+
+:- func add(nat,nat) = nat.
+:- mode add(in,in)   = in  is semidet.
+:- mode add(out,out) = in  is multi.
+:- mode add(in,in)   = out is det.
+
+:- implementation.
+           
+add(X,Y) = Z :-
+   (         ( X=o    , Z=Y ) ;
+   some [Xp] ( X=s(Xp), Z=s(add(Xp,Y)) ) ).
+

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