[m-dev.] for review: improvements/bug fixes for simplify.m

[Simon Taylor]

> > 	Don't optimize a singleton switch into a test followed
> > 	by the case goal if the constructor being tested against
> > 	is existentially quantified. This is necessary because
> > 	the code to produce the test uses type_util__get_cons_id_arg_types,
> > 	which does not correctly handle the existentially quantified
> > 	type variables or the type-infos for those type variables.
> 
> Ouch.
> 
> That change is fine, but I don't think it goes far enough.
> I think type_util__get_cons_id_arg_types should be changed to
> call error/1 if the cons_id is existentially typed, rather than
> quietly returning bogus results.  The documentation for that
> predicate should mention that limitation.  And we need to do something
> about all the other calls to it. 

Done.
 
> Also I think it would be a good idea to have a test case for this
> part of the change.

Done.

> > Index: compiler/simplify.m
> ...
> > +		    ( 
> > +			type_util__get_existq_cons_defn(ModuleInfo1,
> > +					Type, ConsId, _)
> > +		    ->
> 
> That will be a bit inefficient, because type_util__get_existq_cons_defn/4
> does quite a bit of work to construct the unused fourth argument;
> you might consider writing a predicate type_util__is_existq_cons/3.

Done.

> >  simplify__goal_2(some(Vars1, CanRemove0, Goal1), SomeInfo,
> > +		GoalExpr, GoalInfo, Info0, Info) :-
> > +	simplify_info_get_common_info(Info0, Common),
> > +	simplify__goal(Goal1, Goal2, Info0, Info1),
> > +	simplify__nested_somes(CanRemove0, Vars1, Goal2, SomeInfo, Goal),
> > +	Goal = GoalExpr - GoalInfo,
> > +	( Goal = some(_, _, _) - _ ->
> > +		% Don't increase the set of non-locals of a goal within
> > +		% a commit through common structure elimination because
> > +		% that may change the determinism.
> > +		simplify_info_set_common_info(Info1, Common, Info)
> >  	;
> > +		Info = Info1
> >  	).
> 
> >From the comment, I understand roughly what the code is trying to do,
> but it took me a long time to understand how the code (set_common_info)
> relates to the comment (don't increase the set of non-locals).
> I think it would help if you could explain in a little bit more detail
> how leaving the common_info unchanged at that point could lead
> later code to increase the set of non-locals of this goal.
 

+		% Replacing calls, constructions or deconstructions
+		% outside a commit with references to variables created
+		% inside the commit would increase the set of output
+		% variables of the goal inside the commit. This is not
+		% allowed because it could change the determinism.





Estimated hours taken: 2

compiler/simplify.m:
	Remove unnecessary explicit quantification goals before working
	out whether a goal can cause a stack flush.

	Don't increase the non-locals set of an explicit quantification
	goal through common structure elimination because that could change
	the determinism.

	Don't optimize a singleton switch into a test followed
	by the case goal if the constructor being tested against
	is existentially quantified. This is necessary because
	the code to produce the test uses type_util__get_cons_id_arg_types,
	which does not correctly handle the existentially quantified
	type variables or the type-infos for those type variables.

compiler/type_util.m:
	Add type_util__is_existq_cons, which succeeds if a constructor
	is existentially typed.

	type_util__get_cons_id_arg_types now aborts if the cons_id
	is existentially typed rather than silently giving wrong answers.

compiler/goal_util.m:
	Add a comment that goal_util__switch_to_disjunction and
	goal_util__case_to_disjunct abort on existentially typed constructors.

compiler/magic.m:
	Add an XXX comment that we should check for existentially
	typed constructors before calling goal_util__switch_to_disjunction.

tests/hard_coded/Mmakefile:
tests/hard_coded/existential_type_switch_opt.{m,exp}:
	Test case.


Index: compiler/goal_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/goal_util.m,v
retrieving revision 1.59
diff -u -u -r1.59 goal_util.m
--- goal_util.m	1999/10/25 03:48:49	1.59
+++ goal_util.m	1999/10/27 03:27:53
@@ -147,12 +147,16 @@
 
 	% Convert a switch back into a disjunction. This is needed 
 	% for the magic set transformation.
+	% This aborts if any of the constructors are existentially typed.
 :- pred goal_util__switch_to_disjunction(prog_var, list(case), instmap, 
 		list(hlds_goal), prog_varset, prog_varset, map(prog_var, type),
 		map(prog_var, type), module_info, module_info).
 :- mode goal_util__switch_to_disjunction(in, in, in, out,
 		in, out, in, out, in, out) is det.
 
+	% Convert a case into a conjunction by adding a tag test 
+	% (deconstruction unification) to the case goal.
+	% This aborts if the constructor is existentially typed.
 :- pred goal_util__case_to_disjunct(prog_var, cons_id, hlds_goal, instmap,
 		hlds_goal, prog_varset, prog_varset, map(prog_var, type),
 		map(prog_var, type), module_info, module_info).
Index: compiler/simplify.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/simplify.m,v
retrieving revision 1.73
diff -u -u -r1.73 simplify.m
--- simplify.m	1999/10/25 03:49:38	1.73
+++ simplify.m	1999/10/27 07:03:04
@@ -417,12 +417,23 @@
 		Goal1 = Goal0,
 		Info3 = Info0
 	),
-	simplify_info_maybe_clear_structs(before, Goal1, Info3, Info4),
-	Goal1 = GoalExpr1 - GoalInfo1,
-	simplify__goal_2(GoalExpr1, GoalInfo1, Goal, GoalInfo2, Info4, Info5),
-	simplify_info_maybe_clear_structs(after, Goal - GoalInfo2,
+
+	%
+	% Remove unnecessary explicit quantifications before working
+	% out whether the goal can cause a stack flush.
+	%
+	( Goal1 = some(SomeVars, CanRemove, SomeGoal1) - GoalInfo1 ->
+		simplify__nested_somes(CanRemove, SomeVars, SomeGoal1,
+			GoalInfo1, Goal2)
+	;
+		Goal2 = Goal1	
+	),
+	simplify_info_maybe_clear_structs(before, Goal2, Info3, Info4),
+	Goal2 = GoalExpr2 - GoalInfo2,
+	simplify__goal_2(GoalExpr2, GoalInfo2, Goal, GoalInfo3, Info4, Info5),
+	simplify_info_maybe_clear_structs(after, Goal - GoalInfo3,
 		Info5, Info6),
-	simplify__enforce_invariant(GoalInfo2, GoalInfo, Info6, Info).
+	simplify__enforce_invariant(GoalInfo3, GoalInfo, Info6, Info).
 
 :- pred simplify__enforce_invariant(hlds_goal_info, hlds_goal_info,
 		simplify_info, simplify_info).
@@ -571,9 +582,33 @@
 		% a possibly can_fail unification with the functor on the front.
 		cons_id_arity(ConsId, Arity),
 		(
-			SwitchCanFail = can_fail,
-			MaybeConsIds \= yes([ConsId])
+		    SwitchCanFail = can_fail,
+		    MaybeConsIds \= yes([ConsId])
 		->
+			%
+			% Don't optimize in the case of an existentially
+			% typed constructor because currently 
+			% simplify__create_test_unification does not
+			% handle the existential type variables
+			% in the types of the constructor arguments
+			% or their type-infos.
+			%
+		    simplify_info_get_var_types(Info1, VarTypes1),
+		    map__lookup(VarTypes1, Var, Type),
+		    simplify_info_get_module_info(Info1, ModuleInfo1),
+		    ( 
+			type_util__is_existq_cons(ModuleInfo1,
+					Type, ConsId)
+		    ->
+		    	Goal = switch(Var, SwitchCanFail, Cases, SM),
+			goal_info_get_nonlocals(GoalInfo0, NonLocals),
+			merge_instmap_deltas(InstMap0, NonLocals, InstMaps,
+				NewDelta, ModuleInfo1, ModuleInfo2),
+			simplify_info_set_module_info(Info1,
+				ModuleInfo2, Info4),
+			goal_info_set_instmap_delta(GoalInfo0,
+				NewDelta, GoalInfo)
+		    ;
 			simplify__create_test_unification(Var, ConsId, Arity,
 				UnifyGoal, Info1, Info2),
 
@@ -587,11 +622,9 @@
 			set__insert(NonLocals0, Var, NonLocals),
 			goal_info_get_instmap_delta(GoalInfo0, InstMapDelta0),
 			simplify_info_get_instmap(Info2, InstMap),
-			simplify_info_get_var_types(Info2, VarTypes),
-			map__lookup(VarTypes, Var, Type),
 			instmap_delta_bind_var_to_functor(Var, Type, ConsId, 	
 				InstMap, InstMapDelta0, InstMapDelta, 
-				ModuleInfo0, ModuleInfo),
+				ModuleInfo1, ModuleInfo),
 			simplify_info_set_module_info(Info2, 
 				ModuleInfo, Info3),	
 			goal_info_get_determinism(GoalInfo0, CaseDetism),
@@ -602,11 +635,12 @@
 			simplify_info_set_requantify(Info3, Info4),
 			Goal = conj(GoalList),
 			GoalInfo = CombinedGoalInfo
+		    )
 		;
-			% The var can only be bound to this cons_id, so
-			% a test is unnecessary.
-			SingleGoal = Goal - GoalInfo,
-			Info4 = Info1
+		    % The var can only be bound to this cons_id, so
+		    % a test is unnecessary.
+		    SingleGoal = Goal - GoalInfo,
+		    Info4 = Info1
 		),
 		pd_cost__eliminate_switch(CostDelta),
 		simplify_info_incr_cost_delta(Info4, CostDelta, Info)
@@ -1027,23 +1061,20 @@
 	).
 
 simplify__goal_2(some(Vars1, CanRemove0, Goal1), SomeInfo,
-		Goal, GoalInfo, Info0, Info) :-
-	simplify__goal(Goal1, Goal2, Info0, Info),
-	simplify__nested_somes(CanRemove0, Vars1, Goal2,
-		CanRemove, Vars, Goal3),
-	Goal3 = GoalExpr3 - GoalInfo3,
-	(
-		goal_info_get_determinism(GoalInfo3, Detism),
-		goal_info_get_determinism(SomeInfo, Detism),
-		CanRemove = can_remove
-	->
-		% If the inner and outer detisms match the `some'
-		% is unnecessary.
-		Goal = GoalExpr3,
-		GoalInfo = GoalInfo3
+		GoalExpr, GoalInfo, Info0, Info) :-
+	simplify_info_get_common_info(Info0, Common),
+	simplify__goal(Goal1, Goal2, Info0, Info1),
+	simplify__nested_somes(CanRemove0, Vars1, Goal2, SomeInfo, Goal),
+	Goal = GoalExpr - GoalInfo,
+	( Goal = some(_, _, _) - _ ->
+		% Replacing calls, constructions or deconstructions
+		% outside a commit with references to variables created
+		% inside the commit would increase the set of output
+		% variables of the goal inside the commit. This is not
+		% allowed because it could change the determinism.
+		simplify_info_set_common_info(Info1, Common, Info)
 	;
-		Goal = some(Vars, CanRemove, Goal3),
-		GoalInfo = SomeInfo
+		Info = Info1
 	).
 
 simplify__goal_2(Goal0, GoalInfo, Goal, GoalInfo, Info0, Info) :-
@@ -1300,10 +1331,29 @@
 
 	% replace nested `some's with a single `some',
 :- pred simplify__nested_somes(can_remove::in, list(prog_var)::in,
+		hlds_goal::in, hlds_goal_info::in, hlds_goal::out) is det.
+
+simplify__nested_somes(CanRemove0, Vars1, Goal0, OrigGoalInfo, Goal) :-
+	simplify__nested_somes_2(CanRemove0, Vars1, Goal0,
+		CanRemove, Vars, Goal1),
+	Goal1 = GoalExpr1 - GoalInfo1,
+	(
+		goal_info_get_determinism(GoalInfo1, Detism),
+		goal_info_get_determinism(OrigGoalInfo, Detism),
+		CanRemove = can_remove
+	->
+		% If the inner and outer detisms match the `some'
+		% is unnecessary.
+		Goal = GoalExpr1 - GoalInfo1
+	;
+		Goal = some(Vars, CanRemove, Goal1) - OrigGoalInfo
+	).
+
+:- pred simplify__nested_somes_2(can_remove::in, list(prog_var)::in,
 		hlds_goal::in, can_remove::out, list(prog_var)::out,
 		hlds_goal::out) is det.
 
-simplify__nested_somes(CanRemove0, Vars0, Goal0, CanRemove, Vars, Goal) :-
+simplify__nested_somes_2(CanRemove0, Vars0, Goal0, CanRemove, Vars, Goal) :-
 	( Goal0 = some(Vars1, CanRemove1, Goal1) - _ ->
 		(
 			( CanRemove0 = cannot_remove
@@ -1315,7 +1365,7 @@
 			CanRemove2 = can_remove
 		),
 		list__append(Vars0, Vars1, Vars2),
-		simplify__nested_somes(CanRemove2, Vars2, Goal1,
+		simplify__nested_somes_2(CanRemove2, Vars2, Goal1,
 			CanRemove, Vars, Goal)
 	;
 		CanRemove = CanRemove0,
@@ -1548,6 +1598,7 @@
 
 	% Create a semidet unification at the start of a singleton case
 	% in a can_fail switch.
+	% This will abort if the cons_id is existentially typed.
 :- pred simplify__create_test_unification(prog_var::in, cons_id::in, int::in,
 		hlds_goal::out, simplify_info::in, simplify_info::out) is det.
 
Index: compiler/type_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/type_util.m,v
retrieving revision 1.74
diff -u -u -r1.74 type_util.m
--- type_util.m	1999/10/15 03:45:09	1.74
+++ type_util.m	1999/10/27 03:43:34
@@ -166,6 +166,7 @@
 :- mode type_constructors(in, in, out) is semidet.
 
 	% Work out the types of the arguments of a functor.
+	% Aborts if the functor is existentially typed.
 :- pred type_util__get_cons_id_arg_types(module_info::in, (type)::in,
 		cons_id::in, list(type)::out) is det.
 
@@ -175,6 +176,9 @@
 :- pred type_util__get_existq_cons_defn(module_info::in,
 		(type)::in, cons_id::in, ctor_defn::out) is semidet.
 
+:- pred type_util__is_existq_cons(module_info::in,
+		(type)::in, cons_id::in) is semidet.
+
 	% This type is used to return information about a constructor
 	% definition, extracted from the hlds_type_defn and hlds_cons_defn
 	% data types.
@@ -660,7 +664,7 @@
 				ConsDefn = hlds_cons_defn(_, _, _, TypeId, _)
 			)),
 		list__filter(CorrectCons, ConsDefns,
-			[hlds_cons_defn(_ExistQVars0, _Constraints0, ArgTypes0,
+			[hlds_cons_defn(ExistQVars0, _Constraints0, ArgTypes0,
 				_, _)]),
 		ArgTypes0 \= []
 	->
@@ -668,28 +672,43 @@
 		map__lookup(Types, TypeId, TypeDefn),
 		hlds_data__get_type_defn_tparams(TypeDefn, TypeDefnParams),
 		term__term_list_to_var_list(TypeDefnParams, TypeDefnVars),
+
 		% XXX handle ExistQVars
+		require(unify(ExistQVars0, []),
+	"type_util__get_cons_id_arg_types: existentially typed cons_id"),
+
 		map__from_corresponding_lists(TypeDefnVars, TypeArgs, TSubst),
 		term__apply_substitution_to_list(ArgTypes0, TSubst, ArgTypes)
 	;
 		ArgTypes = []
 	).
 
-	% Given a type and a cons_id, look up the definition of that
-	% constructor; if it is existentially typed, return its definition,
-	% otherwise fail.
-type_util__get_existq_cons_defn(ModuleInfo, VarType, ConsId, CtorDefn) :-
+type_util__is_existq_cons(ModuleInfo, VarType, ConsId) :-
+	type_util__is_existq_cons(ModuleInfo, VarType, ConsId, _). 
+	
+:- pred type_util__is_existq_cons(module_info::in,
+		(type)::in, cons_id::in, hlds_cons_defn::out) is semidet.
+
+type_util__is_existq_cons(ModuleInfo, VarType, ConsId, ConsDefn) :-
 	type_to_type_id(VarType, TypeId, _TypeArgs),
 	module_info_ctors(ModuleInfo, Ctors),
 	% will fail for builtin cons_ids.
 	map__search(Ctors, ConsId, ConsDefns),
-	MatchingCons = lambda([ConsDefn::in] is semidet, (
-			ConsDefn = hlds_cons_defn(_, _, _, TypeId, _)
+	MatchingCons = lambda([ThisConsDefn::in] is semidet, (
+			ThisConsDefn = hlds_cons_defn(_, _, _, TypeId, _)
 		)),
-	list__filter(MatchingCons, ConsDefns,
-		[hlds_cons_defn(ExistQVars, Constraints, ArgTypes, _, _)]),
-	ExistQVars \= [],
+	list__filter(MatchingCons, ConsDefns, [ConsDefn]), 
+	ConsDefn = hlds_cons_defn(ExistQVars, _, _, _, _),
+	ExistQVars \= [].
+
+	% Given a type and a cons_id, look up the definition of that
+	% constructor; if it is existentially typed, return its definition,
+	% otherwise fail.
+type_util__get_existq_cons_defn(ModuleInfo, VarType, ConsId, CtorDefn) :-
+	type_util__is_existq_cons(ModuleInfo, VarType, ConsId, ConsDefn),
+	ConsDefn = hlds_cons_defn(ExistQVars, Constraints, ArgTypes, _, _),
 	module_info_types(ModuleInfo, Types),
+	type_to_type_id(VarType, TypeId, _),
 	map__lookup(Types, TypeId, TypeDefn),
 	hlds_data__get_type_defn_tvarset(TypeDefn, TypeVarSet),
 	hlds_data__get_type_defn_tparams(TypeDefn, TypeDefnParams),
Index: tests/hard_coded/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/hard_coded/Mmakefile,v
retrieving revision 1.68
diff -u -u -r1.68 Mmakefile
--- Mmakefile	1999/10/25 03:53:14	1.68
+++ Mmakefile	1999/10/27 06:15:44
@@ -35,6 +35,7 @@
 	existential_bound_tvar \
 	existential_reordering \
 	existential_type_switch \
+	existential_type_switch_opt \
 	existential_types_test \
 	eqv_type_bug \
 	error_func \
Index: tests/hard_coded/existential_type_switch_opt.exp
===================================================================
RCS file: existential_type_switch_opt.exp
diff -N existential_type_switch_opt.exp
--- /dev/null	Wed Oct 27 17:08:14 1999
+++ existential_type_switch_opt.exp	Wed Oct 27 16:13:54 1999
@@ -0,0 +1 @@
+succeeded
Index: tests/hard_coded/existential_type_switch_opt.m
===================================================================
RCS file: existential_type_switch_opt.m
diff -N existential_type_switch_opt.m
--- /dev/null	Wed Oct 27 17:08:14 1999
+++ existential_type_switch_opt.m	Wed Oct 27 16:13:54 1999
@@ -0,0 +1,47 @@
+% Regression test: rotd-1999-10-27 did not handle optimization of
+% a singleton switch on an existentially typed constructor.
+% Symptom:
+% 	Uncaught exception:
+%	Software Error: instmap_delta_from_mode_list_2
+%------------------------------------------------------------------------------%
+
+:- module existential_type_switch_opt.
+
+:- interface.
+
+:- import_module io.
+
+:- pred main(state::di, state::uo) is det.
+
+:- type maybe
+	--->	e_no
+	;	some [U] e_maybe(U)
+	;	some [T] e_yes(T)
+	.
+
+:- pred p(maybe).
+:- mode p(in) is semidet.
+%------------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module std_util.
+
+main -->
+	{ semidet_fail ->
+		X = 'new e_maybe'(2)
+	;
+		X = 'new e_yes'(1)
+	},
+	(
+		{ p(X) }
+	->
+		io__write_string("succeeded\n")
+	;
+		io__write_string("failed\n")
+	).
+
+:- pragma inline(p/1).
+p(e_no).
+p(e_yes(_)).
+
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------