[m-rev.] diff: bug fix on mode-constraints branch

[David Overton]

Estimated hours taken: 1
Branches: mode-constraints

Fix a bug where goal_paths were not being handled consistently in the
constraint-based mode analyser.  In some places, `disj', `neg',
`ite_else' and `exist' components were being removed from the start of
the goal_path, while in other places they were not.  This change ensures
consistency by removing these components at the start of the goal_path
at the point where it is first inserted into the goal_info.

compiler/goal_path.m:
	Add a Boolean argument to `goal_path__fill_slots_in_clauses'
	which, if true, will cause prefixes consisting of `disj', `neg',
	`ite_else' and `exist' components to be removed from all
	computed goal_paths before they are inserted into the
	goal_infos.  Use record syntax for the `slot_info' type.

compiler/mode_constraints.m:
	Pass the new argument to `goal_path__fill_slots_in_clauses'.

compiler/mode_constraint_robdd.m:
	Remove now-redundant code which removed the goal_path components
	in some cases but was not used consistently.

Index: goal_path.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/goal_path.m,v
retrieving revision 1.12.10.6
diff -u -r1.12.10.6 goal_path.m
--- goal_path.m	16 Aug 2002 06:40:42 -0000	1.12.10.6
+++ goal_path.m	9 Sep 2002 03:34:40 -0000
@@ -13,15 +13,23 @@
 
 :- interface.
 
+:- import_module bool.
 :- import_module hlds__hlds_pred, hlds__hlds_module, hlds__hlds_goal.
 
 :- pred goal_path__fill_slots(proc_info::in, module_info::in, proc_info::out)
 	is det.
 
 	% Fill in the goal_paths for goals in the clauses_info of the predicate.
-	% Clauses are given goal paths `disj(1)', ...,  `disj(N)'.
+	% Clauses are given goal paths `disj(1)', ...,  `disj(N)'.  If the bool
+	% argument is true then the goal paths are stored in a form where any
+	% prefix consisting of `disj(_)', `neg', `exist(_)' and `ite_else'
+	% components is removed.  This is used to optimise the constraint-based
+	% mode analysis where the instantiatedness of a variable at such a goal
+	% path is always equivalent to its instantiatedness at the parent goal
+	% path.
+
 :- pred goal_path__fill_slots_in_clauses(pred_info::in, module_info::in,
-	pred_info::out) is det.
+	bool::in, pred_info::out) is det.
 
 :- pred goal_path__fill_slots_in_goal(hlds_goal::in, vartypes::in,
 		module_info::in, hlds_goal::out) is det.
@@ -35,8 +43,9 @@
 
 :- type slot_info
 	--->	slot_info(
-			vartypes,
-			module_info
+			vartypes			:: vartypes,
+			module_info			:: module_info,
+			omit_mode_equiv_prefix	 	:: bool
 		).
 
 goal_path__fill_slots(Proc0, ModuleInfo, Proc) :-
@@ -46,11 +55,14 @@
 	goal_path__fill_slots_in_goal(Goal0, VarTypes, ModuleInfo, Goal),
 	proc_info_set_goal(Proc0, Goal, Proc).
 
-goal_path__fill_slots_in_clauses(PredInfo0, ModuleInfo, PredInfo) :-
+goal_path__fill_slots_in_clauses(PredInfo0, ModuleInfo, OmitModeEquivPrefix,
+		PredInfo) :-
 	pred_info_clauses_info(PredInfo0, ClausesInfo0),
 	clauses_info_clauses(ClausesInfo0, Clauses0),
 	clauses_info_vartypes(ClausesInfo0, VarTypes),
-	SlotInfo = slot_info(VarTypes, ModuleInfo),
+	SlotInfo ^ vartypes = VarTypes,
+	SlotInfo ^ module_info = ModuleInfo,
+	SlotInfo ^ omit_mode_equiv_prefix = OmitModeEquivPrefix,
 	list__map_foldl(
 		(pred(clause(A, Goal0, C, D)::in, clause(A, Goal, C, D)::out,
 				N::in, (N + 1)::out) is det :-
@@ -60,14 +72,24 @@
 	pred_info_set_clauses_info(PredInfo0, ClausesInfo, PredInfo).
 
 goal_path__fill_slots_in_goal(Goal0, VarTypes, ModuleInfo, Goal) :-
-	SlotInfo = slot_info(VarTypes, ModuleInfo),
+	SlotInfo ^ vartypes = VarTypes,
+	SlotInfo ^ module_info = ModuleInfo,
+	SlotInfo ^ omit_mode_equiv_prefix = no,
 	fill_goal_slots(Goal0, [], SlotInfo, Goal).
 
 :- pred fill_goal_slots(hlds_goal::in, goal_path::in, slot_info::in,
 	hlds_goal::out) is det.
 
 fill_goal_slots(Expr0 - Info0, Path0, SlotInfo, Expr - Info) :-
-	goal_info_set_goal_path(Info0, Path0, Info),
+	( SlotInfo ^ omit_mode_equiv_prefix = yes ->
+		list__takewhile((pred(Step::in) is semidet :-
+			( Step = disj(_) ; Step = neg ; Step = exist(_) 
+			; Step = ite_else )),
+		    Path0, _, Path)
+	;
+		Path = Path0
+	),
+	goal_info_set_goal_path(Info0, Path, Info),
 	fill_expr_slots(Expr0, Info, Path0, SlotInfo, Expr).
 
 :- pred fill_expr_slots(hlds_goal_expr::in, hlds_goal_info::in, goal_path::in,
@@ -82,7 +104,8 @@
 	fill_disj_slots(Goals0, Path0, 0, SlotInfo, Goals).
 fill_expr_slots(switch(Var, B, Cases0), _, Path0, SlotInfo,
 		switch(Var, B, Cases)) :-
-	SlotInfo = slot_info(VarTypes, ModuleInfo),
+	VarTypes = SlotInfo ^ vartypes,
+	ModuleInfo = SlotInfo ^ module_info,
 	map__lookup(VarTypes, Var, Type),
 	(
 		type_util__switch_type_num_functors(ModuleInfo, Type,
Index: mode_constraint_robdd.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/Attic/mode_constraint_robdd.m,v
retrieving revision 1.1.2.11
diff -u -r1.1.2.11 mode_constraint_robdd.m
--- mode_constraint_robdd.m	27 Mar 2002 06:27:40 -0000	1.1.2.11
+++ mode_constraint_robdd.m	9 Sep 2002 03:28:16 -0000
@@ -187,7 +187,7 @@
 		RobddVar = Info0 ^ zero_var,
 		Info = Info0
 	;
-		RepVar = remove_goal_path_branches(RepVar0),
+		RepVar = RepVar0,
 		LambdaPath = Info0^lambda_path,
 		Key = key(RepVar, PredId, LambdaPath),
 		( bimap__search(Info0^varmap, Key, RobddVar0) ->
@@ -201,31 +201,7 @@
 	).
 
 mode_constraint_var(Info, RepVar) = bimap__lookup(Info^varmap, Key) :-
-	Key = key(remove_goal_path_branches(RepVar), Info^pred_id,
-			Info^lambda_path).
-
-:- func remove_goal_path_branches(rep_var) = rep_var.
-
-remove_goal_path_branches(RepVar) =
-	(
-		RepVar = ProgVar `at` Path0,
-		list__takewhile((pred(Step::in) is semidet :-
-			( Step = disj(_) ; Step = neg ; Step = exist(_) 
-			; Step = ite_else )),
-		    Path0, _, Path)
-	->
-		% Variables in each branch of a branched goal are always
-		% equivalent.  Likewise, a variable in a negated or
-		% existentially quantified goal will always be equivalent to the
-		% variable in the parent goal.  This means we can use the same
-		% mode_constraint_var for each of these equivalent variables,
-		% avoiding adding lots of equivalence constraints to the ROBDD.
-		% This is a good thing since equivalence constraints tend to
-		% cause exponential explosions in ROBDDs.
-		ProgVar `at` Path
-	;
-		RepVar
-	).
+	Key = key(RepVar, Info^pred_id, Info^lambda_path).
 
 enter_lambda_goal(GoalPath) -->
 	LambdaPath0 =^ lambda_path,
Index: mode_constraints.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/Attic/mode_constraints.m,v
retrieving revision 1.1.2.25
diff -u -r1.1.2.25 mode_constraints.m
--- mode_constraints.m	16 Aug 2002 06:41:38 -0000	1.1.2.25
+++ mode_constraints.m	9 Sep 2002 03:35:40 -0000
@@ -167,8 +167,18 @@
 
 	save_min_var_for_pred(PredId),
 
+	% Variables in each branch of a branched goal are always equivalent.
+	% Likewise, a variable in a negated or existentially quantified goal
+	% will always be equivalent to the variable in the parent goal.  This
+	% means we can use the same mode_constraint_var for each of these
+	% equivalent variables, avoiding adding lots of equivalence constraints
+	% to the ROBDD.  This is a good thing since equivalence constraints tend
+	% to cause exponential explosions in ROBDDs.  We achieve this by passing
+	% `OmitModeEquivPrefix = yes' to `goal_path__fill_slots_in_clauses'.
+
+	{ OmitModeEquivPrefix = yes },
 	{ goal_path__fill_slots_in_clauses(PredInfo0, ModuleInfo0,
-		PredInfo1) },
+		OmitModeEquivPrefix, PredInfo1) },
 
 	{ pred_info_clauses_info(PredInfo1, ClausesInfo0) },
 	{ clauses_info_headvars(ClausesInfo0, HeadVars) },
-- 
David Overton                  Uni of Melbourne     +61 3 8344 9159
dmo at cs.mu.oz.au                Monash Uni (Clayton) +61 3 9905 5779
http://www.cs.mu.oz.au/~dmo    Mobile Phone         +61 4 0337 4393
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------