[m-rev.] fix det unification regression

[Fergus Henderson]

Estimated hours taken: 3
Branches: main

Fix a recently introduced bug which caused the compiler to sometimes report
determinism errors in automatically-generated unification procedures.

compiler/unify_proc.m:
	Disable the optimization to the way that we generate clauses for
	unification procedures which Zoltan added recently, because it
	breaks determinism analysis.

tests/general/Mmakefile.
tests/general/det_complicated_unify2.m:
tests/general/det_complicated_unify2.exp:
	Add a new test case showing the problem.  This is a variant of
	det_complicated_unify.m in which the type involved is a d.u. type
	rather than an enumeration.  Mercury 0.11 passes this test case,
	Zoltan's change broke it, and the patch to unify_proc.m above
	ensures that we pass it again.

Workspace: /home/ceres/fjh/mercury
Index: compiler/unify_proc.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/unify_proc.m,v
retrieving revision 1.131
diff -u -d -r1.131 unify_proc.m
--- compiler/unify_proc.m	15 Jan 2004 07:36:18 -0000	1.131
+++ compiler/unify_proc.m	12 Feb 2004 03:55:41 -0000
@@ -1171,10 +1171,23 @@
 %	__Unify__(X, Y) :-
 %		(
 %			X = a1,
+% #if 0
 %			Y = X
+%			% Actually, to avoid infinite recursion,
+%			% the above unification is done as type int:
+%			%	CastX = unsafe_cast(X) `with_type` int,
+%			%	CastY = unsafe_cast(Y) `with_type` int,
+%			%	CastX = CastY
+% #else
+%			Y = a1
+% #endif
 %		;
 %			X = a2,
-%			Y = X
+% #if 0
+%			Y = X	% Likewise, done as type int
+% #else
+%			Y = a2
+% #endif
 %		;
 %			X = b(X1),
 %			Y = b(Y2),
@@ -1191,12 +1204,21 @@
 %			X3 = Y3
 %		).
 %
-% Note that in the disjuncts handling constants, we want to unify Y with X,
-% not with the constant. This allows dupelim to take the code fragments
-% implementing the switch arms for constants and eliminate all but one of them.
+% Note that in the disjuncts handling constants, we want to unify Y with X
+% (as shown in the "#if 0 ... #else" parts), not with the constant
+% (as shown in the "#else" ... "#endif" parts).
+% Doing this allows dupelim to take the code fragments implementing
+% the switch arms for constants and eliminate all but one of them.
 % This can be a significant code size saving for types with lots of constants,
 % such as the one representing Aditi bytecodes, which can lead to significant
 % reductions in C compilation time.
+% XXX But the optimization doesn't work, because it breaks determinism
+% analysis.  In particular, if X and Y both have insts `bound(a2)', then
+% determinism analysis will infer that the unification can't fail and thus
+% that the procedure is det, but casting to int loses the binding information,
+% and so mode and determinism analysis can't tell that CastX = CastY is det.
+% (See e.g. tests/general/det_complicated_unify2.m.)
+% Hence this optimization is currently disabled.
 
 :- pred unify_proc__generate_du_unify_clauses(list(constructor), prog_var,
 		prog_var, prog_context, list(clause),
@@ -1211,6 +1233,8 @@
 	list__length(ArgTypes, FunctorArity),
 	FunctorConsId = cons(FunctorName, FunctorArity),
 	(
+		% XXX This optimization disabled, see XXX comment above.
+		semidet_fail,
 		ArgTypes = [],
 		can_compare_constants_as_ints(!.Info) = yes
 	->
Index: tests/general/det_complicated_unify2.exp
===================================================================
RCS file: tests/general/det_complicated_unify2.exp
diff -N tests/general/det_complicated_unify2.exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/general/det_complicated_unify2.exp	12 Feb 2004 04:02:08 -0000
@@ -0,0 +1 @@
+worked
Index: tests/general/det_complicated_unify2.m
===================================================================
RCS file: tests/general/det_complicated_unify2.m
diff -N tests/general/det_complicated_unify2.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/general/det_complicated_unify2.m	12 Feb 2004 03:45:16 -0000
@@ -0,0 +1,30 @@
+% This tests that the compiler handles deterministic complicated
+% unifications on enums and compound types correctly.
+% (Version 0.4 of the compiler failed this test.)
+
+:- module det_complicated_unify2.
+:- interface.
+:- import_module io.
+
+:- pred main(io__state::di, io__state::uo) is det.
+
+:- implementation.
+
+:- type foo ---> foo(bar).
+:- type foo2 ---> foo2(bar) ; yyy(int).
+:- type bar ---> bar ; zzz(int).
+
+main -->
+	{ p(foo(bar),foo(bar)), p2(foo2(bar),foo2(bar)), q(bar, bar) },
+	io__write_string("worked\n").
+
+:- pred p(foo::in(bound(foo(bound(bar)))), foo::in(bound(foo(bound(bar)))))
+	is det.
+p(X, X).
+
+:- pred p2(foo2::in(bound(foo2(bound(bar)))),
+	foo2::in(bound(foo2(bound(bar))))) is det.
+p2(X, X).
+
+:- pred q(bar::in(bound(bar)), bar::in(bound(bar))) is det.
+q(X, X).

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------