Diff: Better handling of failure unifications

Andrew Bromage bromage at cs.mu.oz.au
Thu Aug 21 13:18:37 AEST 1997


G'day all.

Fergus, you've seen most of it already, but could you please review
it anyway?

Thnaks.

Cheers,
Andrew Bromage


Estimated hours taken: 8

Better handling of abstract unification of insts which always fail.

compiler/det_analysis.m:
	New predicate det_par_conjunction_detism/3 to compute the
	determinism of parallel conjunctions (or virtual parallel
	conjunctions).

compiler/hlds_data.m:
	Make the ground_inst_table store the determinism of the
	grounding operation.  The reason for this is that
	make_ground_inst* now returns the determinism of the
	grounding operation, and so it makes sense to store the
	determinisms along with cached groundings to avoid
	recomputing them.

compiler/inst_util.m:
	Add a new argument to return the determinism of the
	unification/grounding to the following predicates:

		abstractly_unify_inst_functor
		abstractly_unify_bound_inst_list
		abstractly_unify_bound_inst_list_lives
		abstractly_unify_inst_list_lives
		make_ground_inst_list_lives
		make_ground_inst_list
		make_ground_inst
		make_ground_bound_inst_list

	This is to make it easier to locate unifications which
	cannot succeed.

compiler/instmap.m:
	If you attempt to insert a not_reached into an instmap, the
	entire instmap becomes unreachable.

compiler/modecheck_unify.m:
	Slight reorganisation of code dealing with var-functor
	unifications.  Simple optimisations have been moved to
	modecheck_unify_functor.

	All unifications which definitely fail are now optimised
	to `fail'.

compiler/mode_util.m:
	Minor change to support the alteration to the ground_inst_table
	above.

tests/valid/Mmake:
tests/valid/empty_bound_inst_list.m:
	Test case.


Index: compiler/det_analysis.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/det_analysis.m,v
retrieving revision 1.119
diff -u -r1.119 det_analysis.m
--- det_analysis.m	1997/07/27 15:00:10	1.119
+++ det_analysis.m	1997/08/19 06:46:44
@@ -79,6 +79,9 @@
 :- pred det_conjunction_detism(determinism, determinism, determinism).
 :- mode det_conjunction_detism(in, in, out) is det.
 
+:- pred det_par_conjunction_detism(determinism, determinism, determinism).
+:- mode det_par_conjunction_detism(in, in, out) is det.
+
 :- pred det_disjunction_maxsoln(soln_count, soln_count, soln_count).
 :- mode det_disjunction_maxsoln(in, in, out) is det.
 
@@ -715,6 +718,18 @@
 		det_conjunction_maxsoln(MaxSolnA, MaxSolnB, MaxSoln),
 		determinism_components(Detism, CanFail, MaxSoln)
 	).
+
+% Figuring out the determinism of a parallel conjunction is much
+% easier than for a sequential conjunction, since you simply
+% ignore the case where the second goal is unreachable.  Just do
+% a normal solution count.
+
+det_par_conjunction_detism(DetismA, DetismB, Detism) :-
+	determinism_components(DetismA, CanFailA, MaxSolnA),
+	determinism_components(DetismB, CanFailB, MaxSolnB),
+	det_conjunction_canfail(CanFailA, CanFailB, CanFail),
+	det_conjunction_maxsoln(MaxSolnA, MaxSolnB, MaxSoln),
+	determinism_components(Detism, CanFail, MaxSoln).
 
 % For the at_most_zero, at_most_one, at_most_many,
 % we're just doing abstract interpretation to count
Index: compiler/hlds_data.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/hlds_data.m,v
retrieving revision 1.15
diff -u -r1.15 hlds_data.m
--- hlds_data.m	1997/07/27 15:00:28	1.15
+++ hlds_data.m	1997/08/14 06:35:50
@@ -331,7 +331,7 @@
 
 :- type merge_inst_table ==	map(pair(inst), maybe_inst).
 
-:- type ground_inst_table == 	map(inst_name, maybe_inst).
+:- type ground_inst_table == 	map(inst_name, maybe_inst_det).
 
 :- type shared_inst_table == 	map(inst_name, maybe_inst).
 
Index: compiler/inst_util.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/inst_util.m,v
retrieving revision 1.2
diff -u -r1.2 inst_util.m
--- inst_util.m	1997/07/27 15:00:37	1.2
+++ inst_util.m	1997/08/20 06:13:15
@@ -44,8 +44,8 @@
 
 :- pred abstractly_unify_inst_functor(is_live, inst, cons_id, list(inst),
 				list(is_live), unify_is_real, module_info,
-				inst, module_info).
-:- mode abstractly_unify_inst_functor(in, in, in, in, in, in, in, out, out)
+				inst, determinism, module_info).
+:- mode abstractly_unify_inst_functor(in, in, in, in, in, in, in, out, out, out)
 	is semidet.
 
 	% Compute the inst that results from abstractly unifying
@@ -85,7 +85,7 @@
 %-----------------------------------------------------------------------------%
 
 :- implementation.
-:- import_module hlds_data, inst_match, mode_util.
+:- import_module hlds_data, inst_match, mode_util, det_analysis.
 :- import_module bool, std_util, require, map, list, set.
 
 	% Abstractly unify two insts.
@@ -111,7 +111,8 @@
 				% it must be semidet somewhere else too.
 			Det = det
 		),
-		ModuleInfo = ModuleInfo0
+		ModuleInfo = ModuleInfo0,
+		Inst1 = Inst0
 	;
 			% insert ThisInstPair into the table with value
 			% `unknown'
@@ -124,19 +125,28 @@
 		inst_expand(ModuleInfo0, InstB, InstB2),
 		abstractly_unify_inst_2(Live, InstA2, InstB2, UnifyIsReal,
 			ModuleInfo1, Inst0, Det, ModuleInfo2),
+
+			% If this unification cannot possible succeed,
+			% the correct inst is not_reached.
+		( determinism_components(Det, _, at_most_zero) ->
+			Inst1 = not_reached
+		;
+			Inst1 = Inst0
+		),
+
 			% now update the value associated with ThisInstPair
 		module_info_insts(ModuleInfo2, InstTable2),
 		inst_table_get_unify_insts(InstTable2, UnifyInsts2),
-		map__det_update(UnifyInsts2, ThisInstPair, known(Inst0, Det),
+		map__det_update(UnifyInsts2, ThisInstPair, known(Inst1, Det),
 			UnifyInsts),
 		inst_table_set_unify_insts(InstTable2, UnifyInsts, InstTable),
 		module_info_set_insts(ModuleInfo2, InstTable, ModuleInfo)
 	),
 		% avoid expanding recursive insts
-	( inst_contains_instname(Inst0, ModuleInfo, ThisInstPair) ->
+	( inst_contains_instname(Inst1, ModuleInfo, ThisInstPair) ->
 		Inst = defined_inst(ThisInstPair)
 	;
-		Inst = Inst0
+		Inst = Inst1
 	).
 
 :- pred abstractly_unify_inst_2(is_live, inst, inst, unify_is_real, module_info,
@@ -215,10 +225,11 @@
 	unify_uniq(dead, Real, Det, UniqX, UniqY, Uniq).
 
 abstractly_unify_inst_3(live, bound(UniqX, BoundInsts0), ground(UniqY, _),
-		Real, M0, bound(Uniq, BoundInsts), semidet, M) :-
+		Real, M0, bound(Uniq, BoundInsts), Det, M) :-
 	unify_uniq(dead, Real, semidet, UniqX, UniqY, Uniq),
 	make_ground_bound_inst_list(BoundInsts0, live, UniqY, Real, M0,
-			BoundInsts, M).
+			BoundInsts, Det1, M),
+	det_par_conjunction_detism(Det1, semidet, Det).
 
 /*** abstract insts not supported
 abstractly_unify_inst_3(live, bound(Uniq, List), abstract_inst(_,_), Real, M,
@@ -232,10 +243,11 @@
 	unify_uniq(live, Real, det, unique, Uniq0, Uniq).
 
 abstractly_unify_inst_3(live, ground(UniqX, yes(_)), bound(UniqY, BoundInsts0),
-		Real, M0, bound(Uniq, BoundInsts), semidet, M) :-
+		Real, M0, bound(Uniq, BoundInsts), Det, M) :-
 	unify_uniq(dead, Real, semidet, UniqX, UniqY, Uniq),
 	make_ground_bound_inst_list(BoundInsts0, live, UniqX, Real, M0,
-			BoundInsts, M).
+			BoundInsts, Det1, M),
+	det_par_conjunction_detism(Det1, semidet, Det).
 
 abstractly_unify_inst_3(live, ground(UniqA, yes(PredInstA)),
 				ground(UniqB, _MaybePredInstB), Real, M,
@@ -254,12 +266,7 @@
 
 abstractly_unify_inst_3(live, ground(Uniq, no), Inst0, Real, M0,
 				Inst, Det, M) :-
-	( inst_is_free(M0, Inst0) ->
-		Det = det
-	;
-		Det = semidet
-	),
-	make_ground_inst(Inst0, live, Uniq, Real, M0, Inst, M).
+	make_ground_inst(Inst0, live, Uniq, Real, M0, Inst, Det, M).
 
 % abstractly_unify_inst_3(live, abstract_inst(_,_), free,       _, _, _, _, _)
 %       :- fail.
@@ -304,10 +311,11 @@
 	unify_uniq(dead, Real, Det, UniqX, UniqY, Uniq).
 
 abstractly_unify_inst_3(dead, bound(UniqX, BoundInsts0), ground(UniqY, _),
-			Real, M0, bound(Uniq, BoundInsts), semidet, M) :-
+			Real, M0, bound(Uniq, BoundInsts), Det, M) :-
 	unify_uniq(dead, Real, semidet, UniqX, UniqY, Uniq),
 	make_ground_bound_inst_list(BoundInsts0, dead, UniqY, Real, M0,
-					BoundInsts, M).
+					BoundInsts, Det1, M),
+	det_par_conjunction_detism(Det1, semidet, Det).
 
 /***** abstract insts aren't really supported
 abstractly_unify_inst_3(dead, bound(Uniq, List), abstract_inst(N,As),
@@ -327,10 +335,11 @@
 				ground(Uniq, yes(PredInst)), det, M).
 
 abstractly_unify_inst_3(dead, ground(UniqA, yes(_)), bound(UniqB, BoundInsts0),
-			Real, M0, bound(Uniq, BoundInsts), semidet, M) :-
+			Real, M0, bound(Uniq, BoundInsts), Det, M) :-
 	unify_uniq(dead, Real, semidet, UniqA, UniqB, Uniq),
 	make_ground_bound_inst_list(BoundInsts0, dead, UniqA, Real, M0,
-					BoundInsts, M).
+					BoundInsts, Det1, M),
+	det_par_conjunction_detism(Det1, semidet, Det).
 
 abstractly_unify_inst_3(dead, ground(UniqA, yes(PredInstA)),
 				ground(UniqB, _MaybePredInstB), Real, M,
@@ -341,12 +350,7 @@
 
 abstractly_unify_inst_3(dead, ground(Uniq, no), Inst0, Real, M0,
 				Inst, Det, M) :-
-	( inst_is_free(M0, Inst0) ->
-		Det = det
-	;
-		Det = semidet
-	),
-	make_ground_inst(Inst0, dead, Uniq, Real, M0, Inst, M).
+	make_ground_inst(Inst0, dead, Uniq, Real, M0, Inst, Det, M).
 
 /***** abstract insts aren't really supported
 abstractly_unify_inst_3(dead, abstract_inst(N,As), bound(List), Real,
@@ -389,11 +393,7 @@
 		Z, Det1, ModuleInfo1),
 	abstractly_unify_inst_list(Xs, Ys, Live, Real, ModuleInfo1,
 		Zs, Det2, ModuleInfo),
-	( Det1 = semidet ->
-		Det = semidet
-	;
-		Det = Det2
-	).
+	det_par_conjunction_detism(Det1, Det2, Det).
 
 %-----------------------------------------------------------------------------%
 
@@ -402,62 +402,65 @@
 	% with a functor.
 
 abstractly_unify_inst_functor(Live, InstA, ConsId, ArgInsts, ArgLives,
-		Real, ModuleInfo0, Inst, ModuleInfo) :-
+		Real, ModuleInfo0, Inst, Det, ModuleInfo) :-
 	inst_expand(ModuleInfo0, InstA, InstA2),
 	abstractly_unify_inst_functor_2(Live, InstA2, ConsId, ArgInsts,
-			ArgLives, Real, ModuleInfo0, Inst, ModuleInfo).
+			ArgLives, Real, ModuleInfo0, Inst, Det, ModuleInfo).
 
 :- pred abstractly_unify_inst_functor_2(is_live, inst, cons_id, list(inst),
 			list(is_live), unify_is_real, module_info,
-			inst, module_info).
-:- mode abstractly_unify_inst_functor_2(in, in, in, in, in, in, in, out, out)
-	is semidet.
+			inst, determinism, module_info).
+:- mode abstractly_unify_inst_functor_2(in, in, in, in, in, in, in,
+			out, out, out) is semidet.
 
 	% XXX need to handle `any' insts
 
 abstractly_unify_inst_functor_2(live, not_reached, _, _, _, _, M,
-			not_reached, M).
+			not_reached, erroneous, M).
 
 abstractly_unify_inst_functor_2(live, free, ConsId, Args0, ArgLives, _Real,
 			ModuleInfo0,
-			bound(unique, [functor(ConsId, Args)]), ModuleInfo) :-
+			bound(unique, [functor(ConsId, Args)]), det,
+			ModuleInfo) :-
 	inst_list_is_ground_or_any_or_dead(Args0, ArgLives, ModuleInfo0),
 	maybe_make_shared_inst_list(Args0, ArgLives, ModuleInfo0,
 			Args, ModuleInfo).
 
 abstractly_unify_inst_functor_2(live, bound(Uniq, ListX), ConsId, Args,
-				ArgLives, Real, M0, bound(Uniq, List), M) :-
+			ArgLives, Real, M0, bound(Uniq, List), Det, M) :-
 	abstractly_unify_bound_inst_list_lives(ListX, ConsId, Args, ArgLives,
-					Real, M0, List, M).
+					Real, M0, List, Det, M).
 
 abstractly_unify_inst_functor_2(live, ground(Uniq, _), ConsId, ArgInsts,
-		ArgLives, Real, M0, Inst, M) :-
+		ArgLives, Real, M0, Inst, Det, M) :-
 	make_ground_inst_list_lives(ArgInsts, live, ArgLives, Uniq, Real, M0,
-		GroundArgInsts, M),
+		GroundArgInsts, Det, M),
 	Inst = bound(Uniq, [functor(ConsId, GroundArgInsts)]).
 
-% abstractly_unify_inst_functor_2(live, abstract_inst(_,_), _, _, _, _, _, _) :-
+% abstractly_unify_inst_functor_2(live, abstract_inst(_,_), _, _, _, _, _,
+%		_, _) :-
 %       fail.
 
 abstractly_unify_inst_functor_2(dead, not_reached, _, _, _, _, M,
-					not_reached, M).
+					not_reached, erroneous, M).
 
 abstractly_unify_inst_functor_2(dead, free, ConsId, Args, _ArgLives, _Real, M,
-			bound(unique, [functor(ConsId, Args)]), M).
+			bound(unique, [functor(ConsId, Args)]), det, M).
 
 abstractly_unify_inst_functor_2(dead, bound(Uniq, ListX), ConsId, Args,
-			_ArgLives, Real, M0, bound(Uniq, List), M) :-
+			_ArgLives, Real, M0, bound(Uniq, List), Det, M) :-
 	ListY = [functor(ConsId, Args)],
 	abstractly_unify_bound_inst_list(dead, ListX, ListY, Real, M0,
-		List, _, M).
+		List, Det, M).
 
 abstractly_unify_inst_functor_2(dead, ground(Uniq, _), ConsId, ArgInsts,
-		_ArgLives, Real, M0, Inst, M) :-
+		_ArgLives, Real, M0, Inst, Det, M) :-
 	make_ground_inst_list(ArgInsts, dead, Uniq, Real, M0,
-		GroundArgInsts, M),
+		GroundArgInsts, Det, M),
 	Inst = bound(Uniq, [functor(ConsId, GroundArgInsts)]).
 
-% abstractly_unify_inst_functor_2(dead, abstract_inst(_,_), _, _, _, _, _, _) :-
+% abstractly_unify_inst_functor_2(dead, abstract_inst(_,_), _, _, _, _,
+%		_, _, _) :-
 %       fail.
 
 %-----------------------------------------------------------------------------%
@@ -479,69 +482,92 @@
 :- mode abstractly_unify_bound_inst_list(in, in, in, in, in,
 		out, out, out) is semidet.
 
-abstractly_unify_bound_inst_list(_, [], [], _, ModuleInfo, [], det, ModuleInfo).
-abstractly_unify_bound_inst_list(_, [], [_|_], _, M, [], semidet, M).
-abstractly_unify_bound_inst_list(_, [_|_], [], _, M, [], semidet, M).
-abstractly_unify_bound_inst_list(Live, [X|Xs], [Y|Ys], Real, ModuleInfo0,
+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),
+	( L = [] ->
+		det_par_conjunction_detism(Det0, erroneous, Det)
+	;
+		Det = Det0
+	).
+
+:- pred abstractly_unify_bound_inst_list_2(is_live, list(bound_inst),
+		list(bound_inst), unify_is_real, module_info,
+		list(bound_inst), determinism, module_info).
+:- mode abstractly_unify_bound_inst_list_2(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(Live, [X|Xs], [Y|Ys], Real, ModuleInfo0,
 		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),
-		L = [functor(ConsIdX, Args) | L1],
-		abstractly_unify_bound_inst_list(Live, Xs, Ys, Real,
+		abstractly_unify_bound_inst_list_2(Live, Xs, Ys, Real,
 					ModuleInfo1, L1, Det2, ModuleInfo),
-		( Det1 = semidet ->
-		    Det = semidet
+
+		% If the unification of the two cons_ids is guaranteed
+		% not to succeed, don't include it in the list.
+		( determinism_components(Det1, _, at_most_zero) ->
+			L = L1,
+			Det = Det2
 		;
-		    Det = Det2
+			L = [functor(ConsIdX, Args) | L1],
+			det_par_conjunction_detism(Det1, Det2, Det)
 		)
 	;
-		Det = semidet,
 		( compare(<, ConsIdX, ConsIdY) ->
-			abstractly_unify_bound_inst_list(Live, Xs, [Y|Ys],
-				Real, ModuleInfo0, L, _, ModuleInfo)
+			abstractly_unify_bound_inst_list_2(Live, Xs, [Y|Ys],
+				Real, ModuleInfo0, L, Det1, ModuleInfo)
 		;
-			abstractly_unify_bound_inst_list(Live, [X|Xs], Ys,
-				Real, ModuleInfo0, L, _, ModuleInfo)
-		)
+			abstractly_unify_bound_inst_list_2(Live, [X|Xs], Ys,
+				Real, ModuleInfo0, L, Det1, ModuleInfo)
+		),
+		det_par_conjunction_detism(Det1, semidet, Det)
 	).
 
 :- pred abstractly_unify_bound_inst_list_lives(list(bound_inst), cons_id,
 	list(inst), list(is_live), unify_is_real, module_info,
-	list(bound_inst), module_info).
-:- mode abstractly_unify_bound_inst_list_lives(in, in, in, in, in, in, out, out)
-	is semidet.
+	list(bound_inst), determinism, module_info).
+:- mode abstractly_unify_bound_inst_list_lives(in, in, in, in, in, in,
+	out, out, out) is semidet.
 
 abstractly_unify_bound_inst_list_lives([], _, _, _, _, ModuleInfo,
-					[], ModuleInfo).
+					[], failure, ModuleInfo).
 abstractly_unify_bound_inst_list_lives([X|Xs], ConsIdY, ArgsY, LivesY, Real,
-		ModuleInfo0, L, ModuleInfo) :-
+		ModuleInfo0, L, Det, ModuleInfo) :-
 	X = functor(ConsIdX, ArgsX),
 	(
 		ConsIdX = ConsIdY
 	->
 		abstractly_unify_inst_list_lives(ArgsX, ArgsY, LivesY, Real,
-			ModuleInfo0, Args, ModuleInfo),
+			ModuleInfo0, Args, Det, ModuleInfo),
 		L = [functor(ConsIdX, Args)]
 	;
 		abstractly_unify_bound_inst_list_lives(Xs, ConsIdY, ArgsY,
-				LivesY, Real, ModuleInfo0, L, ModuleInfo)
+			LivesY, Real, ModuleInfo0, L, Det, ModuleInfo)
 	).
 
 :- pred abstractly_unify_inst_list_lives(list(inst), list(inst), list(is_live),
-			unify_is_real, module_info, list(inst), module_info).
-:- mode abstractly_unify_inst_list_lives(in, in, in, in, in, out, out)
+	unify_is_real, module_info, list(inst), determinism, module_info).
+:- mode abstractly_unify_inst_list_lives(in, in, in, in, in, out, out, out)
 	is semidet.
 
-abstractly_unify_inst_list_lives([], [], [], _, ModuleInfo, [], ModuleInfo).
+abstractly_unify_inst_list_lives([], [], [], _, ModuleInfo,
+		[], det, ModuleInfo).
 abstractly_unify_inst_list_lives([X|Xs], [Y|Ys], [Live|Lives], Real,
-		ModuleInfo0, [Z|Zs], ModuleInfo) :-
+		ModuleInfo0, [Z|Zs], Det, ModuleInfo) :-
 	abstractly_unify_inst(Live, X, Y, Real, ModuleInfo0,
-			Z, _Det, ModuleInfo1),
+			Z, Det1, ModuleInfo1),
 	abstractly_unify_inst_list_lives(Xs, Ys, Lives, Real, ModuleInfo1,
-			Zs, ModuleInfo).
+			Zs, Det2, ModuleInfo),
+	det_par_conjunction_detism(Det1, Det2, Det).
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
@@ -643,64 +669,69 @@
 %-----------------------------------------------------------------------------%
 
 :- pred make_ground_inst_list_lives(list(inst), is_live, list(is_live),
-				uniqueness, unify_is_real,
-				module_info, list(inst), module_info).
-:- mode make_ground_inst_list_lives(in, in, in, in, in, in, out, out)
+			uniqueness, unify_is_real,
+			module_info, list(inst), determinism, module_info).
+:- mode make_ground_inst_list_lives(in, in, in, in, in, in, out, out, out)
 				is semidet.
 
-make_ground_inst_list_lives([], _, _, _, _, ModuleInfo, [], ModuleInfo).
+make_ground_inst_list_lives([], _, _, _, _, ModuleInfo, [], det, ModuleInfo).
 make_ground_inst_list_lives([Inst0 | Insts0], Live, [ArgLive | ArgLives],
-		Uniq, Real, ModuleInfo0, [Inst | Insts], ModuleInfo) :-
+		Uniq, Real, ModuleInfo0, [Inst | Insts], Det, ModuleInfo) :-
 	( Live = live, ArgLive = live ->
 		BothLive = live
 	;
 		BothLive = dead
 	),
 	make_ground_inst(Inst0, BothLive, Uniq, Real, ModuleInfo0,
-		Inst, ModuleInfo1),
+		Inst, Det1, ModuleInfo1),
 	make_ground_inst_list_lives(Insts0, Live, ArgLives, Uniq, Real,
-		ModuleInfo1, Insts, ModuleInfo).
+		ModuleInfo1, Insts, Det2, ModuleInfo),
+	det_par_conjunction_detism(Det1, Det2, Det).
 
 :- pred make_ground_inst_list(list(inst), is_live, uniqueness, unify_is_real,
-				module_info, list(inst), module_info).
-:- mode make_ground_inst_list(in, in, in, in, in, out, out) is semidet.
+			module_info, list(inst), determinism, module_info).
+:- mode make_ground_inst_list(in, in, in, in, in, out, out, out) is semidet.
 
-make_ground_inst_list([], _, _, _, ModuleInfo, [], ModuleInfo).
+make_ground_inst_list([], _, _, _, ModuleInfo, [], det, ModuleInfo).
 make_ground_inst_list([Inst0 | Insts0], Live, Uniq, Real, ModuleInfo0,
-		[Inst | Insts], ModuleInfo) :-
+		[Inst | Insts], Det, ModuleInfo) :-
 	make_ground_inst(Inst0, Live, Uniq, Real, ModuleInfo0,
-		Inst, ModuleInfo1),
+		Inst, Det1, ModuleInfo1),
 	make_ground_inst_list(Insts0, Live, Uniq, Real, ModuleInfo1,
-		Insts, ModuleInfo).
+		Insts, Det2, ModuleInfo),
+	det_par_conjunction_detism(Det1, Det2, Det).
 
 % abstractly unify an inst with `ground' and calculate the new inst
 % and the determinism of the unification.
 
 :- pred make_ground_inst(inst, is_live, uniqueness, unify_is_real, module_info,
-				inst, module_info).
-:- mode make_ground_inst(in, in, in, in, in, out, out) is semidet.
+				inst, determinism, module_info).
+:- mode make_ground_inst(in, in, in, in, in, out, out, out) is semidet.
 
-make_ground_inst(not_reached, _, _, _, M, not_reached, M).
-make_ground_inst(any(Uniq0), IsLive, Uniq1, Real, M, ground(Uniq, no), M) :-
+make_ground_inst(not_reached, _, _, _, M, not_reached, erroneous, M).
+make_ground_inst(any(Uniq0), IsLive, Uniq1, Real, M, ground(Uniq, no),
+		semidet, M) :-
 	unify_uniq(IsLive, Real, semidet, Uniq0, Uniq1, Uniq).
-make_ground_inst(free, IsLive, Uniq0, Real, M, ground(Uniq, no), M) :-
+make_ground_inst(free, IsLive, Uniq0, Real, M, ground(Uniq, no), det, M) :-
 	unify_uniq(IsLive, Real, det, unique, Uniq0, Uniq).
 make_ground_inst(free(T), IsLive, Uniq0, Real, M,
-		defined_inst(typed_ground(Uniq, T)), M) :-
+		defined_inst(typed_ground(Uniq, T)), det, M) :-
 	unify_uniq(IsLive, Real, det, unique, Uniq0, Uniq).
 make_ground_inst(bound(Uniq0, BoundInsts0), IsLive, Uniq1, Real, M0,
-		bound(Uniq, BoundInsts), M) :-
+		bound(Uniq, BoundInsts), Det, M) :-
 	unify_uniq(dead, Real, semidet, Uniq0, Uniq1, Uniq),
 	make_ground_bound_inst_list(BoundInsts0, IsLive, Uniq1, Real, M0,
-					BoundInsts, M).
+					BoundInsts, Det1, M),
+	det_par_conjunction_detism(Det1, semidet, Det).
 make_ground_inst(ground(Uniq0, _PredInst), _IsLive, Uniq1, Real, M,
-		ground(Uniq, no), M) :-
+		ground(Uniq, no), semidet, M) :-
 	unify_uniq(dead, Real, semidet, Uniq0, Uniq1, Uniq).
-make_ground_inst(inst_var(_), _, _, _, _, _, _) :-
+make_ground_inst(inst_var(_), _, _, _, _, _, _, _) :-
 	error("free inst var").
-make_ground_inst(abstract_inst(_,_), _, _, _, M, ground(shared, no), M).
+make_ground_inst(abstract_inst(_,_), _, _, _, M, ground(shared, no),
+		semidet, M).
 make_ground_inst(defined_inst(InstName), IsLive, Uniq, Real, ModuleInfo0,
-			Inst, ModuleInfo) :-
+			Inst, Det, ModuleInfo) :-
 		% check whether the inst name is already in the
 		% ground_inst table
 	module_info_insts(ModuleInfo0, InstTable0),
@@ -709,10 +740,16 @@
 	(
 		map__search(GroundInsts0, GroundInstKey, Result)
 	->
-		( Result = known(GroundInst0) ->
-			GroundInst = GroundInst0
+		( Result = known(GroundInst0, Det0) ->
+			GroundInst = GroundInst0,
+			Det = Det0
 		;
-			GroundInst = defined_inst(GroundInstKey)
+			GroundInst = defined_inst(GroundInstKey),
+			Det = det
+				% We can safely assume this is det, since
+				% if it were semidet, we would have noticed
+				% this in the process of unfolding the
+				% definition.
 		),
 		ModuleInfo = ModuleInfo0
 	;
@@ -729,15 +766,15 @@
 		inst_lookup(ModuleInfo1, InstName, Inst0),
 		inst_expand(ModuleInfo1, Inst0, Inst1),
 		make_ground_inst(Inst1, IsLive, Uniq, Real, ModuleInfo1,
-				GroundInst, ModuleInfo2),
+				GroundInst, Det, ModuleInfo2),
 
 		% now that we have determined the resulting Inst, store
-		% the appropriate value `known(GroundInst)' in the ground_inst
-		% table
+		% the appropriate value `known(GroundInst, Det)' in the
+		% ground_inst table
 		module_info_insts(ModuleInfo2, InstTable2),
 		inst_table_get_ground_insts(InstTable2, GroundInsts2),
-		map__det_update(GroundInsts2, GroundInstKey, known(GroundInst),
-			GroundInsts),
+		map__det_update(GroundInsts2, GroundInstKey,
+			known(GroundInst, Det), GroundInsts),
 		inst_table_set_ground_insts(InstTable2, GroundInsts,
 			InstTable),
 		module_info_set_insts(ModuleInfo2, InstTable, ModuleInfo)
@@ -750,18 +787,20 @@
 	).
 
 :- pred make_ground_bound_inst_list(list(bound_inst), is_live, uniqueness,
-		unify_is_real, module_info, list(bound_inst), module_info).
-:- mode make_ground_bound_inst_list(in, in, in, in, in, out, out) is semidet.
+	unify_is_real, module_info, list(bound_inst), determinism, module_info).
+:- mode make_ground_bound_inst_list(in, in, in, in, in,
+	out, out, out) is semidet.
 
-make_ground_bound_inst_list([], _, _, _, ModuleInfo, [], ModuleInfo).
+make_ground_bound_inst_list([], _, _, _, ModuleInfo, [], det, ModuleInfo).
 make_ground_bound_inst_list([Bound0 | Bounds0], IsLive, Uniq, Real, ModuleInfo0,
-			[Bound | Bounds], ModuleInfo) :-
+			[Bound | Bounds], Det, ModuleInfo) :-
 	Bound0 = functor(ConsId, ArgInsts0),
 	make_ground_inst_list(ArgInsts0, IsLive, Uniq, Real, ModuleInfo0,
-				ArgInsts, ModuleInfo1),
+				ArgInsts, Det1, ModuleInfo1),
 	Bound = functor(ConsId, ArgInsts),
 	make_ground_bound_inst_list(Bounds0, IsLive, Uniq, Real, ModuleInfo1,
-				Bounds, ModuleInfo).
+				Bounds, Det2, ModuleInfo),
+	det_par_conjunction_detism(Det1, Det2, Det).
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/instmap.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/instmap.m,v
retrieving revision 1.13
diff -u -r1.13 instmap.m
--- instmap.m	1997/07/27 15:00:38	1.13
+++ instmap.m	1997/08/18 06:58:50
@@ -368,14 +368,22 @@
 	map__set(InstMapping0, Var, Inst, InstMapping).
 
 instmap_delta_set(unreachable, _Var, _Inst, unreachable).
-instmap_delta_set(reachable(InstMapping0), Var, Inst,
-		reachable(InstMapping)) :-
-	map__set(InstMapping0, Var, Inst, InstMapping).
+instmap_delta_set(reachable(InstMapping0), Var, Inst, Instmap) :-
+	( Inst = not_reached ->
+		Instmap = unreachable
+	;
+		map__set(InstMapping0, Var, Inst, InstMapping),
+		Instmap = reachable(InstMapping)
+	).
 
 instmap_delta_insert(unreachable, _Var, _Inst, unreachable).
-instmap_delta_insert(reachable(InstMapping0), Var, Inst,
-		reachable(InstMapping)) :-
-	map__det_insert(InstMapping0, Var, Inst, InstMapping).
+instmap_delta_insert(reachable(InstMapping0), Var, Inst, Instmap) :-
+	( Inst = not_reached ->
+		Instmap = unreachable
+	;
+		map__det_insert(InstMapping0, Var, Inst, InstMapping),
+		Instmap = reachable(InstMapping)
+	).
 
 %-----------------------------------------------------------------------------%
 
@@ -433,7 +441,8 @@
 	list__duplicate(Arity, free, ArgInsts),
 	(
 		abstractly_unify_inst_functor(dead, Inst0, ConsId, ArgInsts, 
-			ArgLives, real_unify, ModuleInfo0, Inst1, ModuleInfo1)
+			ArgLives, real_unify, ModuleInfo0, Inst1, _Det,
+			ModuleInfo1)
 	->
 		ModuleInfo = ModuleInfo1,
 		Inst = Inst1
Index: compiler/mode_util.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/mode_util.m,v
retrieving revision 1.96
diff -u -r1.96 mode_util.m
--- mode_util.m	1997/07/27 15:01:07	1.96
+++ mode_util.m	1997/08/14 07:08:11
@@ -436,7 +436,7 @@
 		module_info_insts(ModuleInfo, InstTable),
 		inst_table_get_ground_insts(InstTable, GroundInstTable),
 		map__lookup(GroundInstTable, InstName, MaybeInst),
-		( MaybeInst = known(Inst0) ->
+		( MaybeInst = known(Inst0, _) ->
 			Inst = Inst0
 		;
 			Inst = defined_inst(InstName)
Index: compiler/modecheck_unify.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/modecheck_unify.m,v
retrieving revision 1.20
diff -u -r1.20 modecheck_unify.m
--- modecheck_unify.m	1997/07/27 15:01:08	1.20
+++ modecheck_unify.m	1997/08/20 06:07:00
@@ -309,45 +309,10 @@
 		% It's not a higher-order pred unification - just
 		% call modecheck_unify_functor to do the ordinary thing.
 		%
-		mode_info_get_instmap(ModeInfo0, InstMap0),
 		modecheck_unify_functor(X0, TypeOfX,
-			ConsId0, ArgVars0, Unification0, ExtraGoals, Mode,
-			ConsId, ArgVars, Unification, ModeInfo0, ModeInfo),
-		%
-		% Optimize away construction of unused terms by
-		% replacing the unification with `true'.
-		%
-		(
-			Unification = construct(ConstructTarget, _, _, _),
-			mode_info_var_is_live(ModeInfo, ConstructTarget, dead)
-		->
-			Goal = conj([])
-		;
-			Functor = functor(ConsId, ArgVars),
-			Unify = unify(X, Functor, Mode, Unification,
-				UnifyContext),
-			X = X0,
-			%
-			% modecheck_unification sometimes needs to introduce
-			% new goals to handle complicated sub-unifications
-			% in deconstructions.  But this should never happen
-			% during unique mode analysis.
-			% (If it did, the code would be wrong since it
-			% wouldn't have the correct determinism annotations.)
-			%
-			(
-				HowToCheckGoal = check_unique_modes,
-				ExtraGoals \= [] - []
-			->
-				error("unique_modes.m: re-modecheck of unification encountered complicated sub-unifies")
-			;
-				true
-			),
-
-			handle_extra_goals(Unify, ExtraGoals, GoalInfo0,
-						[X0|ArgVars0], [X|ArgVars],
-						InstMap0, ModeInfo, Goal)
-		)
+			ConsId0, ArgVars0, Unification0, UnifyContext,
+			HowToCheckGoal, GoalInfo0,
+			Goal, ModeInfo0, ModeInfo)
 	).
 
 modecheck_unification(X, lambda_goal(PredOrFunc, Vars, Modes0, Det, Goal0),
@@ -488,14 +453,14 @@
 	).
 
 :- pred modecheck_unify_functor(var, (type), cons_id, list(var), unification,
-			pair(list(hlds_goal)), pair(mode), cons_id, list(var),
-			unification, mode_info, mode_info).
-:- mode modecheck_unify_functor(in, in, in, in, in, out, out, out, out, out,
-			mode_info_di, mode_info_uo) is det.
+			unify_context, how_to_check_goal, hlds_goal_info,
+			hlds_goal_expr, mode_info, mode_info).
+:- mode modecheck_unify_functor(in, in, in, in, in, in, in, in,
+			out, mode_info_di, mode_info_uo) is det.
 
 modecheck_unify_functor(X, TypeOfX, ConsId0, ArgVars0, Unification0,
-			ExtraGoals, Mode, ConsId, ArgVars, Unification,
-			ModeInfo0, ModeInfo) :-
+			UnifyContext, HowToCheckGoal, GoalInfo0,
+			Goal, ModeInfo0, ModeInfo) :-
 	mode_info_get_module_info(ModeInfo0, ModuleInfo0),
 	list__length(ArgVars0, Arity),
 	(
@@ -531,6 +496,7 @@
 			ModeInfo0, ModeInfo1
 		),
 		Inst = not_reached,
+		Det = erroneous,
 			% If we get an error, set the inst to not_reached
 			% to avoid cascading errors
 			% But don't call categorize_unification, because
@@ -552,9 +518,10 @@
 	;
 		abstractly_unify_inst_functor(LiveX, InstOfX, ConsId,
 			InstArgs, LiveArgs, real_unify, ModuleInfo0,
-			UnifyInst, ModuleInfo1)
+			UnifyInst, Det1, ModuleInfo1)
 	->
 		Inst = UnifyInst,
+		Det = Det1,
 		mode_info_set_module_info(ModeInfo0, ModuleInfo1, ModeInfo1),
 		ModeOfX = (InstOfX -> Inst),
 		ModeOfY = (InstOfY -> Inst),
@@ -579,8 +546,8 @@
 				Unification0, ModeInfo1,
 				Unification1, ModeInfo2),
 		split_complicated_subunifies(Unification1, ArgVars0,
-					Unification, ArgVars, ExtraGoals,
-					ModeInfo2, ModeInfo3),
+				Unification, ArgVars, ExtraGoals,
+				ModeInfo2, ModeInfo3),
 		modecheck_set_var_inst(X, Inst, ModeInfo3, ModeInfo4),
 		( bind_args(Inst, ArgVars, ModeInfo4, ModeInfo5) ->
 			ModeInfo = ModeInfo5
@@ -600,6 +567,7 @@
 			% that could cause an invalid call to
 			% `unify_proc__request_unify'
 		Inst = not_reached,
+		Det = erroneous,
 		ModeOfX = (InstOfX -> Inst),
 		ModeOfY = (InstOfY -> Inst),
 		Mode = ModeOfX - ModeOfY,
@@ -613,6 +581,48 @@
 		Unification = Unification0,
 		ArgVars = ArgVars0,
 		ExtraGoals = [] - []
+	),
+
+	%
+	% Optimize away construction of unused terms by
+	% replacing the unification with `true'.  Optimize
+	% away unifications which always fail by replacing
+	% them with `fail'.
+	%
+	(
+		Unification = construct(ConstructTarget, _, _, _),
+		mode_info_var_is_live(ModeInfo, ConstructTarget, dead)
+	->
+		Goal = conj([])
+	;
+		Det = failure
+	->
+		map__init(Empty),
+		Goal = disj([], Empty)
+	;
+		Functor = functor(ConsId, ArgVars),
+		Unify = unify(X, Functor, Mode, Unification,
+			UnifyContext),
+		X = X0,
+		%
+		% modecheck_unification sometimes needs to introduce
+		% new goals to handle complicated sub-unifications
+		% in deconstructions.  But this should never happen
+		% during unique mode analysis.
+		% (If it did, the code would be wrong since it
+		% wouldn't have the correct determinism annotations.)
+		%
+		(
+			HowToCheckGoal = check_unique_modes,
+			ExtraGoals \= [] - []
+		->
+			error("unique_modes.m: re-modecheck of unification encountered complicated sub-unifies")
+		;
+			true
+		),
+		handle_extra_goals(Unify, ExtraGoals, GoalInfo0,
+					[X0|ArgVars0], [X|ArgVars],
+					InstMap0, ModeInfo, Goal)
 	).
 
 %-----------------------------------------------------------------------------%
@@ -826,6 +836,8 @@
 	% because otherwise determinism analysis assumes they can fail.
 	% The optimization of assignments to dead variables may be
 	% necessary to stop the code generator from getting confused.)
+	% Optimize away unifications which always fail by replacing
+	% them with `fail'.
 	%
 	(
 		Unification = assign(AssignTarget, _),
@@ -838,6 +850,11 @@
 	->
 		Unify = conj([])
 	;
+		Det = failure
+	->
+		map__init(Empty),
+		Unify = disj([], Empty)
+	;
 		Unify = unify(X, var(Y), ModeOfX - ModeOfY, Unification,
 				UnifyContext)
 	).
@@ -894,14 +911,14 @@
 % be deterministic or semideterministic.
 
 :- pred categorize_unify_var_functor(mode, list(mode), list(mode), var,
-		cons_id, list(var), map(var, type), unification, mode_info,
-		unification, mode_info).
+		cons_id, list(var), map(var, type),
+		unification, mode_info, unification, mode_info).
 :- mode categorize_unify_var_functor(in, in, in, in, in, in, in, in,
 			mode_info_di, out, mode_info_uo) is det.
 
 categorize_unify_var_functor(ModeOfX, ModeOfXArgs, ArgModes0,
-		X, NewConsId, ArgVars, VarTypes, Unification0, ModeInfo0,
-		Unification, ModeInfo) :-
+		X, NewConsId, ArgVars, VarTypes,
+		Unification0, ModeInfo0, Unification, ModeInfo) :-
 	mode_info_get_module_info(ModeInfo0, ModuleInfo),
 	map__lookup(VarTypes, X, TypeOfX),
 	% if we are re-doing mode analysis, preserve the existing cons_id
Index: tests/valid/Mmake
===================================================================
RCS file: /home/staff/zs/imp/tests/valid/Mmake,v
retrieving revision 1.51
diff -u -r1.51 Mmake
--- Mmake	1997/08/10 21:20:36	1.51
+++ Mmake	1997/08/14 02:40:15
@@ -24,6 +24,7 @@
 	double_vn.m \
 	easy_nondet_test.m \
 	easy_nondet_test_2.m \
+	empty_bound_inst_list.m \
 	empty_switch.m \
 	error.m \
 	fail_ite.m \

New File: tests/valid/empty_bound_inst_list.m
===================================================================
:- module empty_bound_inst_list.

:- interface.

:- pred p is failure.

:- implementation.
:- import_module std_util.

:- type some_functors ---> foo ; bar ; baz.

p :-
	( Y = yes(bar), Z = foo
	; Y = yes(baz), Z = foo
	),
	Y = yes(Z).




More information about the developers mailing list