[m-dev.] for review: fix det inference bug for unifications

[Peter Ross]

Hi,

For Fergus to review.


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



Estimated hours taken: 5

Fix bug where unification of two variables with identical bound inst
lists were incorrectly being inferred det.

tests/warnings/Mmakefile:
tests/warnings/det_infer_warning.exp:
tests/warnings/det_infer_warning.m:
    Test case to exercise the bug.

mercury/compiler/inst_util.m:
    Handle bound inst lists of length > 1 correctly.


Index: tests/warnings/Mmakefile
===================================================================
RCS file: /home/staff/zs/imp/tests/warnings/Mmakefile,v
retrieving revision 1.4
diff -u -b -r1.4 Mmakefile
--- Mmakefile	1998/10/28 09:49:33	1.4
+++ Mmakefile	1999/06/22 05:50:21
@@ -5,6 +5,7 @@
 #-----------------------------------------------------------------------------#
 
 PROGS=	\
+	det_infer_warning \
 	double_underscore \
 	duplicate_call \
 	inf_recursion_lambda \
Index: tests/warnings/det_infer_warning.exp
===================================================================
RCS file: det_infer_warning.exp
diff -N det_infer_warning.exp
--- /dev/null	Thu Mar  4 04:20:11 1999
+++ det_infer_warning.exp	Tue Jun 22 15:49:47 1999
@@ -0,0 +1,3 @@
+det_infer_warning.m:014: In `test2':
+det_infer_warning.m:014:   warning: determinism declaration could be tighter.
+det_infer_warning.m:014:   Declared `semidet', inferred `det'.
Index: tests/warnings/det_infer_warning.m
===================================================================
RCS file: det_infer_warning.m
diff -N det_infer_warning.m
--- /dev/null	Thu Mar  4 04:20:11 1999
+++ det_infer_warning.m	Tue Jun 22 15:50:28 1999
@@ -0,0 +1,44 @@
+% Tests that abstractly_unify_bound_inst_list handles the case of
+% different length bound_inst lists where all the cons_ids are the same
+% correctly.
+% Should give a warning that determinism of test2 is inferred det, and
+% not give a warning at all for test.
+
+:- module det_infer_warning.
+
+:- interface.
+
+:- type two ---> true;false.
+
+:- pred test is semidet.
+:- pred test2 is semidet.
+
+:- implementation.
+
+:- import_module require.
+
+test :-
+	(
+		cond(true)
+	->
+		RA = true
+	;
+		RA = false
+	),
+	(
+		cond(false)
+	->
+		RB = true
+	;
+		RB = false
+	),
+	RA = RB.
+
+test2 :-
+	RA = true,
+	RB = true,
+	RA = RB.
+
+:- pred cond(two::in) is semidet.
+
+cond(true).
Index: mercury/compiler/inst_util.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/inst_util.m,v
retrieving revision 1.11
diff -u -b -r1.11 inst_util.m
--- inst_util.m	1998/03/03 17:34:41	1.11
+++ inst_util.m	1999/06/22 05:30:09
@@ -102,7 +102,7 @@
 
 :- implementation.
 :- import_module hlds_data, inst_match, mode_util, det_analysis.
-:- import_module bool, std_util, require, map, list, set.
+:- import_module bool, std_util, require, map, list, set, int.
 
 	% Abstractly unify two insts.
 
@@ -517,7 +517,7 @@
 abstractly_unify_bound_inst_list(Live, Xs, Ys, Real, ModuleInfo0, L, Det,
 		ModuleInfo) :-
 	abstractly_unify_bound_inst_list_2(Live, Xs, Ys, Real,
-		ModuleInfo0, L, Det0, ModuleInfo),
+		ModuleInfo0, 0, L, Det0, ModuleInfo),
 	( L = [] ->
 		det_par_conjunction_detism(Det0, erroneous, Det)
 	;
@@ -525,24 +525,34 @@
 	).
 
 :- pred abstractly_unify_bound_inst_list_2(is_live, list(bound_inst),
-		list(bound_inst), unify_is_real, module_info,
+		list(bound_inst), unify_is_real, module_info, int,
 		list(bound_inst), determinism, module_info).
-:- mode abstractly_unify_bound_inst_list_2(in, in, in, in, in,
+:- mode abstractly_unify_bound_inst_list_2(in, in, in, in, in, in,
 		out, out, out) is semidet.
 
-abstractly_unify_bound_inst_list_2(_, [], [], _, ModuleInfo, [], det,
-		ModuleInfo).
-abstractly_unify_bound_inst_list_2(_, [], [_|_], _, M, [], semidet, M).
-abstractly_unify_bound_inst_list_2(_, [_|_], [], _, M, [], semidet, M).
+abstractly_unify_bound_inst_list_2(_, [], [], _, ModuleInfo, N, [], Det,
+		ModuleInfo) :-
+	(
+			% The only time an abstract unification should
+			% be det, is when both of the bound_inst lists
+			% are of length one and have the same cons_ids.
+		N = 1
+	->
+		Det = det
+	;
+		Det = semidet
+	).
+abstractly_unify_bound_inst_list_2(_, [], [_|_], _, M, _, [], semidet, M).
+abstractly_unify_bound_inst_list_2(_, [_|_], [], _, M, _, [], semidet, M).
 abstractly_unify_bound_inst_list_2(Live, [X|Xs], [Y|Ys], Real, ModuleInfo0,
-		L, Det, ModuleInfo) :-
+		N, L, Det, ModuleInfo) :-
 	X = functor(ConsIdX, ArgsX),
 	Y = functor(ConsIdY, ArgsY),
 	( ConsIdX = ConsIdY ->
 		abstractly_unify_inst_list(ArgsX, ArgsY, Live, Real,
 			ModuleInfo0, Args, Det1, ModuleInfo1),
 		abstractly_unify_bound_inst_list_2(Live, Xs, Ys, Real,
-					ModuleInfo1, L1, Det2, ModuleInfo),
+					ModuleInfo1, N+1, L1, Det2, ModuleInfo),
 
 		% If the unification of the two cons_ids is guaranteed
 		% not to succeed, don't include it in the list.
@@ -556,10 +566,10 @@
 	;
 		( compare(<, ConsIdX, ConsIdY) ->
 			abstractly_unify_bound_inst_list_2(Live, Xs, [Y|Ys],
-				Real, ModuleInfo0, L, Det1, ModuleInfo)
+				Real, ModuleInfo0, N+1, L, Det1, ModuleInfo)
 		;
 			abstractly_unify_bound_inst_list_2(Live, [X|Xs], Ys,
-				Real, ModuleInfo0, L, Det1, ModuleInfo)
+				Real, ModuleInfo0, N+1, L, Det1, ModuleInfo)
 		),
 		det_par_conjunction_detism(Det1, semidet, Det)
 	).

----
 +----------------------------------------------------------------------+
 | Peter Ross      M Sci/Eng Melbourne Uni                              |
 | petdr at cs.mu.oz.au  WWW: www.cs.mu.oz.au/~petdr/ ph: +61 3 9344 9158  |
 +----------------------------------------------------------------------+
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------