[m-rev.] for review: constraint propagation [1]

[Simon Taylor]

Hi,

This change was first reviewed early last year.
Below is a relative diff for constraint.m.
The full diff will be posted in another message.
The mailing list thread from last year can be found in
~stayl/constraint_mail.

Simon.


--- constraint.m.old	Thu Aug  2 22:13:26 2001
+++ constraint.m	Thu Aug  2 22:48:28 2001
@@ -1,5 +1,5 @@
 %-----------------------------------------------------------------------------%
-% Copyright (C) 2000 The University of Melbourne.
+% Copyright (C) 2001 The University of Melbourne.
 % This file may only be copied under the terms of the GNU General
 % Public License - see the file COPYING in the Mercury distribution.
 %-----------------------------------------------------------------------------%
@@ -18,17 +18,17 @@
 :- interface.
 
 :- import_module hlds_goal, hlds_module, instmap, prog_data.
-:- import_module bool, list, map, std_util.
+:- import_module bool, map.
 
-:- pred constraint__propagate_goal(hlds_goal, list(constraint),
-		hlds_goal, constraint_info, constraint_info).
-:- mode constraint__propagate_goal(in, in, out, 
-		in, out) is det.
+:- type constraint_info.
 
-:- pred constraint__propagate_conj(list(hlds_goal), list(constraint), 
-		list(hlds_goal), constraint_info, constraint_info).
-:- mode constraint__propagate_conj(in, in, out,
-		in, out) is det.
+	% constraint__propagate_constraints_in_goal pushes constraints
+	% left and inward within a single goal. Specialized versions of
+	% procedures which are called with constrained outputs are created
+	% by deforest.m.
+:- pred constraint__propagate_constraints_in_goal(hlds_goal, hlds_goal,
+		constraint_info, constraint_info).
+:- mode constraint__propagate_constraints_in_goal(in, out, in, out) is det.
 
 :- pred constraint_info_init(module_info, map(prog_var, type), prog_varset,
 		instmap, constraint_info).
@@ -38,14 +38,6 @@
 		map(prog_var, type), prog_varset, bool).
 :- mode constraint_info_deconstruct(in, out, out, out, out) is det.
 
-:- type constraint_info.
-
-	% A constraint is a goal with no outputs which can fail and
-	% always terminates, and a list of goals to construct static
-	% constants for the constraint. All the goals should have a
-	% `constraint' annotation.
-:- type constraint == pair(hlds_goal, list(hlds_goal)).
-
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
 
@@ -55,27 +47,31 @@
 :- import_module mode_util, passes_aux, code_aux, inst_match, purity.
 :- import_module options, globals.
 
-:- import_module assoc_list, require, set, string, term, varset.
+:- import_module assoc_list, list, require, set, std_util.
+:- import_module string, term, varset.
 
 %-----------------------------------------------------------------------------%
 
+constraint__propagate_constraints_in_goal(Goal0, Goal) -->
+	% We need to strip off any existing constraint markers first.
+	% Constraint markers are meant to indicate where a constraint
+	% is meant to be attached to a call, and that deforest.m should
+	% consider creating a specialized version for the call.
+	% If deforest.m rearranges the goal, the constraints may
+	% not remain next to the call.
+	{ Goal1 = strip_constraint_markers(Goal0) },
+	constraint__propagate_goal(Goal1, [], Goal).
+
+:- pred constraint__propagate_goal(hlds_goal, list(constraint),
+		hlds_goal, constraint_info, constraint_info).
+:- mode constraint__propagate_goal(in, in, out, in, out) is det.
+
 constraint__propagate_goal(Goal0, Constraints, Goal) -->
-	{ Goal0 = _ - GoalInfo0 },
-	
-	% 
-	% If the goal cannot succeed, prune away the constraints.
-	% This is necessary because the goal might not produce some
-	% of the inputs to the constraints, so reordering the constraints
-	% with the goal may cause compiler aborts later.
-	%
-	{ goal_info_get_determinism(GoalInfo0, Detism) },
-	( { determinism_components(Detism, _, at_most_zero) } ->
-		{ Goals = [Goal0] }
-	;
-		InstMap0 =^ instmap,
-		constraint__propagate_goal_2(Goal0, Constraints, Goals),
-		^ instmap := InstMap0
-	),
+	% We need to treat all single goals as conjunctions so that
+	% constraint__propagate_conj can move the constraints to the
+	% left of the goal if that is allowed.
+	{ goal_to_conj_list(Goal0, Goals0) },
+	constraint__propagate_conj(Goals0, Constraints, Goals),
 	{ Goals = [Goal1] ->
 		Goal = Goal1
 	;
@@ -86,77 +82,105 @@
 		conj_list_to_goal(Goals, GoalInfo, Goal)
 	}.
 
-:- pred constraint__propagate_goal_2(hlds_goal, list(constraint),
+:- pred constraint__propagate_conj_sub_goal(hlds_goal, list(constraint),
+		hlds_goals, constraint_info, constraint_info).
+:- mode constraint__propagate_conj_sub_goal(in, in, out, 
+		in, out) is det.
+
+constraint__propagate_conj_sub_goal(Goal0, Constraints, Goals) -->
+	{ Goal0 = GoalExpr0 - _ },
+	( { goal_is_atomic(GoalExpr0) } ->
+		[]
+	;
+		% If a non-empty list of constraints is pushed into a sub-goal,
+		% quantification, instmap_deltas and determinism need to be
+		% recomputed.
+		constraint_info_update_changed(Constraints)
+	),
+	InstMap0 =^ instmap,
+	constraint__propagate_conj_sub_goal_2(Goal0, Constraints, Goals),
+	^ instmap := InstMap0.
+
+:- pred constraint__propagate_conj_sub_goal_2(hlds_goal, list(constraint),
 		list(hlds_goal), constraint_info, constraint_info).
-:- mode constraint__propagate_goal_2(in, in, out, in, out) is det.
+:- mode constraint__propagate_conj_sub_goal_2(in, in, out, in, out) is det.
 
-constraint__propagate_goal_2(conj(Goals0) - Info, Constraints, 
+constraint__propagate_conj_sub_goal_2(conj(Goals0) - Info, Constraints, 
 		[conj(Goals) - Info]) -->
-	constraint_info_update_changed(Constraints),
 	constraint__propagate_conj(Goals0, Constraints, Goals).
 
-constraint__propagate_goal_2(disj(Goals0, SM) - Info, Constraints,
+constraint__propagate_conj_sub_goal_2(disj(Goals0, SM) - Info, Constraints,
 		[disj(Goals, SM) - Info]) -->
 	constraint__propagate_disj(Goals0, Constraints, Goals).
 
-constraint__propagate_goal_2(switch(Var, CanFail, Cases0, SM) - Info,
+constraint__propagate_conj_sub_goal_2(switch(Var, CanFail, Cases0, SM) - Info,
 		Constraints, [switch(Var, CanFail, Cases, SM) - Info]) -->
-	constraint_info_update_changed(Constraints),
 	constraint__propagate_cases(Var, Cases0, Constraints, Cases).
 	
-constraint__propagate_goal_2(
+constraint__propagate_conj_sub_goal_2(
 		if_then_else(Vars, Cond0, Then0, Else0, SM) - Info,
 		Constraints, 
 		[if_then_else(Vars, Cond, Then, Else, SM) - Info]) -->
 	InstMap0 =^ instmap,
-	constraint_info_update_changed(Constraints),
 
 	% We can't safely propagate constraints into 
-	% the condition of an if-then-else.
+	% the condition of an if-then-else, because that
+	% would change the answers generated by the procedure.
 	constraint__propagate_goal(Cond0, [], Cond),
 	constraint_info_update_goal(Cond),
 	constraint__propagate_goal(Then0, Constraints, Then),
 	^ instmap := InstMap0,
-	constraint__propagate_goal(Else0, Constraints, Else),
-	^ instmap := InstMap0.
+	constraint__propagate_goal(Else0, Constraints, Else).
 
-	% XXX propagate constraints into par_conjs - could be a little tricky.
-constraint__propagate_goal_2(par_conj(Goals0, SM) - GoalInfo, Constraints0,
+	% XXX propagate constraints into par_conjs -- this isn't
+	% possible at the moment because par_conj goals must have
+	% determinism det.
+constraint__propagate_conj_sub_goal_2(par_conj(Goals0, SM) - GoalInfo,
+		Constraints0,
 		[par_conj(Goals, SM) - GoalInfo | Constraints]) -->
+	% Propagate constraints within the goals of the conjunction.
 	% constraint__propagate_disj treats its list of goals as
 	% independent rather than specifically disjoint, so we can
 	% use it to process a list of independent parallel conjuncts.
 	constraint__propagate_disj(Goals0, [], Goals),
 	{ constraint__flatten_constraints(Constraints0, Constraints) }.
 
-constraint__propagate_goal_2(some(Vars, CanRemove, Goal0) - GoalInfo,
+constraint__propagate_conj_sub_goal_2(some(Vars, CanRemove, Goal0) - GoalInfo,
 		Constraints, [some(Vars, CanRemove, Goal) - GoalInfo]) -->
-	constraint_info_update_changed(Constraints),
 	constraint__propagate_goal(Goal0, Constraints, Goal).
 
-constraint__propagate_goal_2(not(NegGoal0) - GoalInfo, Constraints0,
+constraint__propagate_conj_sub_goal_2(not(NegGoal0) - GoalInfo, Constraints0,
 		[not(NegGoal) - GoalInfo | Constraints]) -->
-	% We can't safely propagate constraints into a negation.
+	% We can't safely propagate constraints into a negation,
+	% because that would change the answers computed by the
+	% procedure.
 	constraint__propagate_goal(NegGoal0, [], NegGoal),
 	{ constraint__flatten_constraints(Constraints0, Constraints) }.
 
-constraint__propagate_goal_2(Goal, Constraints0, [Goal | Constraints]) -->
+constraint__propagate_conj_sub_goal_2(Goal, Constraints0,
+		[Goal | Constraints]) -->
+	% constraint__propagate_conj will move the constraints
+	% to the left of the call if that is possible, so nothing
+	% needs to be done here.
 	{ Goal = call(_, _, _, _, _, _) - _ },
 	{ constraint__flatten_constraints(Constraints0, Constraints) }.
 
-constraint__propagate_goal_2(Goal, Constraints0, [Goal | Constraints]) -->
+constraint__propagate_conj_sub_goal_2(Goal, Constraints0,
+		[Goal | Constraints]) -->
 	{ Goal = generic_call(_, _, _, _) - _ },
 	{ constraint__flatten_constraints(Constraints0, Constraints) }.
 
-constraint__propagate_goal_2(Goal, Constraints0, [Goal | Constraints]) -->
-	{ Goal = pragma_c_code(_, _, _, _, _, _, _) - _ },
+constraint__propagate_conj_sub_goal_2(Goal, Constraints0,
+		[Goal | Constraints]) -->
+	{ Goal = foreign_proc(_, _, _, _, _, _, _) - _ },
 	{ constraint__flatten_constraints(Constraints0, Constraints) }.
 
-constraint__propagate_goal_2(Goal, _, _) -->
-	{ Goal = bi_implication(_, _) - _ },
-	{ error("constraint__propagate_goal_2: bi_implication") }.
+constraint__propagate_conj_sub_goal_2(Goal, _, _) -->
+	{ Goal = shorthand(_) - _ },
+	{ error("constraint__propagate_conj_sub_goal_2: shorthand") }.
 
-constraint__propagate_goal_2(Goal, Constraints0, [Goal | Constraints]) -->
+constraint__propagate_conj_sub_goal_2(Goal, Constraints0,
+		[Goal | Constraints]) -->
 	{ Goal = unify(_, _, _, _, _) - _ },
 	{ constraint__flatten_constraints(Constraints0, Constraints) }.
 
@@ -168,7 +192,7 @@
 
 constraint__flatten_constraints(Constraints0, Goals) :-
 	list__map(lambda([Constraint::in, Lists::out] is det, (
-			Constraint = Goal - Constructs,
+			Constraint = constraint(Goal, _, _, Constructs),
 			Lists = [Constructs, [Goal]]
 	)), Constraints0, GoalLists0),
 	list__condense(GoalLists0, GoalLists),
@@ -211,46 +235,115 @@
 	% in the list. Some effort is made to keep the constraints
 	% in the same order as they are encountered to increase
 	% the likelihood of folding recursive calls.
+:- pred constraint__propagate_conj(list(hlds_goal), list(constraint), 
+		list(hlds_goal), constraint_info, constraint_info).
+:- mode constraint__propagate_conj(in, in, out,
+		in, out) is det.
 
 constraint__propagate_conj(Goals0, Constraints, Goals) -->
-	InstMap0 =^ instmap,
-	ModuleInfo =^ module_info,
-	{ constraint__annotate_conj_output_vars(Goals0, ModuleInfo,
-		InstMap0, [], RevGoals1) },
-	constraint__annotate_conj_constraints(ModuleInfo, RevGoals1, 
-		Constraints, [], Goals2),
-	constraint__propagate_conj_constraints(Goals2, [], Goals).
+	( { Goals0 = [] } ->
+		{ constraint__flatten_constraints(Constraints, Goals) }
+	; { Goals0 = [Goal0], Constraints = [] } ->
+		constraint__propagate_conj_sub_goal(Goal0, [], Goals)
+	;
+		constraint_info_update_changed(Constraints),
+		InstMap0 =^ instmap,
+		ModuleInfo =^ module_info,
+		VarTypes =^ vartypes,
+		{ constraint__annotate_conj_output_vars(Goals0, ModuleInfo,
+			VarTypes, InstMap0, [], RevGoals1) },
+		constraint__annotate_conj_constraints(ModuleInfo, RevGoals1, 
+			Constraints, [], Goals2),
+		constraint__propagate_conj_constraints(Goals2, [], Goals)
+	).
 
 	% Annotate each conjunct with the variables it produces.
-:- pred constraint__annotate_conj_output_vars(list(hlds_goal), 
-		module_info, instmap, annotated_conj, annotated_conj).
-:- mode constraint__annotate_conj_output_vars(in, in, in, in, out) is det.
-
-constraint__annotate_conj_output_vars([], _, _, RevGoals, RevGoals).
-constraint__annotate_conj_output_vars([Goal | Goals], ModuleInfo, InstMap0, 
-		RevGoals0, RevGoals) :-
+:- pred constraint__annotate_conj_output_vars(list(hlds_goal), module_info,
+		vartypes, instmap, annotated_conj, annotated_conj).
+:- mode constraint__annotate_conj_output_vars(in, in, in, in, in, out) is det.
+
+constraint__annotate_conj_output_vars([], _, _, _, RevGoals, RevGoals).
+constraint__annotate_conj_output_vars([Goal | Goals], ModuleInfo, VarTypes,
+		InstMap0, RevGoals0, RevGoals) :-
 	Goal = _ - GoalInfo,
 	goal_info_get_instmap_delta(GoalInfo, InstMapDelta),
 
-	% XXX this won't work on the alias branch.
-	instmap_delta_changed_vars(InstMapDelta, ChangedVars0),
-	Bound = lambda([Var::in] is semidet, (
-			instmap__lookup_var(InstMap0, Var, InstMapInst),
-			instmap_delta_search_var(InstMapDelta, Var, DeltaInst),
-			\+ inst_matches_binding(InstMapInst,
-				DeltaInst, ModuleInfo)
-		)),
-	set__to_sorted_list(ChangedVars0, ChangedVars1),
-	list__filter(Bound, ChangedVars1, ChangedVars2),
-	set__sorted_list_to_set(ChangedVars2, ChangedVars),
 	instmap__apply_instmap_delta(InstMap0, InstMapDelta, InstMap),
-	constraint__annotate_conj_output_vars(Goals, ModuleInfo, InstMap, 
-		[Goal - ChangedVars | RevGoals0], RevGoals).
+	instmap_changed_vars(InstMap0, InstMap, VarTypes,
+		ModuleInfo, ChangedVars),
+
+	% Restrict the set of changed variables down to the set
+	% for which the new inst is not an acceptable subsitute
+	% for the old. This is done to allow reordering of a goal which
+	% uses a variable with inst `ground(shared, no)' with
+	% a constraint which just adds information, changing the inst
+	% to `bound(shared, ...)'.
+	InCompatible = (pred(Var::in) is semidet :-
+			instmap__lookup_var(InstMap0, Var, InstBefore),
+			instmap_delta_search_var(InstMapDelta, Var, InstAfter),
+			\+ inst_matches_initial(InstAfter, InstBefore,
+				map__lookup(VarTypes, Var), ModuleInfo)
+		),
+	IncompatibleInstVars = set__filter(InCompatible, ChangedVars), 
+
+	Bound = (pred(Var::in) is semidet :-
+			instmap__lookup_var(InstMap0, Var, InstBefore),
+			instmap_delta_search_var(InstMapDelta, Var, InstAfter),
+			\+ inst_matches_binding(InstAfter, InstBefore,
+				map__lookup(VarTypes, Var), ModuleInfo)
+		),
+	BoundVars = set__filter(Bound, ChangedVars),
+
+	AnnotatedConjunct = annotated_conjunct(Goal, ChangedVars, BoundVars,
+				IncompatibleInstVars),
+	constraint__annotate_conj_output_vars(Goals, ModuleInfo, VarTypes,
+		InstMap, [AnnotatedConjunct | RevGoals0], RevGoals).
 
 %-----------------------------------------------------------------------------%
 
-	% Conjunction annotated with its output variables.
-:- type annotated_conj == assoc_list(hlds_goal, set(prog_var)).
+	% Conjunction annotated with the variables each conjunct
+	% changes the instantiatedness of.
+:- type annotated_conj == list(annotated_conjunct).
+
+:- type annotated_conjunct
+	---> annotated_conjunct(
+		hlds_goal,
+
+			% All variables returned by instmap_changed_vars.
+		set(prog_var),
+
+			% All variables returned by instmap_changed_vars for
+			% which inst_matches_binding(NewInst, OldInst) fails.
+		set(prog_var),
+
+			% Variables returned by instmap_changed_vars
+			% for which the new inst cannot be substituted
+			% for the old as an input to a goal
+			% (inst_matches_initial(NewInst, OldInst) fails).
+		set(prog_var)
+	).
+
+	% A constraint is a goal with no outputs which can fail and
+	% always terminates.
+:- type constraint
+	---> constraint(
+			% The constraint itself.
+		hlds_goal,
+
+			% All variables returned by instmap_changed_vars.
+		set(prog_var),
+
+			% Variables returned by instmap_changed_vars
+			% for which the new inst cannot be substituted
+			% for the old as an input to a goal
+			% (inst_matches_initial(NewInst, OldInst) fails).
+		set(prog_var),
+		
+			% Goals to construct constants used by the constraint.
+			% (as in X = 2, Y < X). These need to be propagated
+			% with the constraint.
+		list(hlds_goal)
+	).
 
 	% Conjunction annotated with constraining goals.
 :- type constrained_conj == assoc_list(hlds_goal, list(constraint)).
@@ -270,26 +363,37 @@
 		)), Constraints1, Constraints) },
 	{ list__append(Constraints, Goals0, Goals) }.
 constraint__annotate_conj_constraints(ModuleInfo, 
-		[Goal - OutputVars | RevGoals0], 
+		[Conjunct | RevConjuncts0],
 		Constraints0, Goals0, Goals) -->
 	{ Goal = GoalExpr - GoalInfo },
+	{ goal_info_get_nonlocals(GoalInfo, NonLocals) },
+	{ Conjunct = annotated_conjunct(Goal, ChangedVars,
+			OutputVars, IncompatibleInstVars) },
 	(
 		% Propagate goals with no output variables which can fail.
+		% Propagating cc_nondet goals would be tricky, because we
+		% would need to be careful about reordering the constraints
+		% (the cc_nondet goal can't be moved before any goals
+		% which can fail).
+		% 
 		{ goal_info_get_determinism(GoalInfo, Detism) },
 		{ Detism = semidet
 		; Detism = failure
-		% ; Detism = cc_nondet	% ??
 		},
 		{ set__empty(OutputVars) },
 
+		% Don't propagate impure goals.
+		{ goal_info_is_pure(GoalInfo) },
+
 		% Don't propagate goals that can loop. 
 		{ code_aux__goal_cannot_loop(ModuleInfo, Goal) }
 	->
+		% It's a constraint, add it to the list of constraints
+		% to be attached to goals earlier in the conjunction.
 		{ Goals1 = Goals0 },
-		% Put the `constraint' feature on the goal so deforest.m
-		% knows to attempt to propagate this goal through calls.
-		{ goal_info_add_feature(GoalInfo, constraint, GoalInfo1) },
-		{ Constraints1 = [(GoalExpr - GoalInfo1) - [] | Constraints0] }
+		{ Constraint = constraint(GoalExpr - GoalInfo,
+				ChangedVars, IncompatibleInstVars, []) },
+		{ Constraints1 = [Constraint | Constraints0] }
 	;
 		%
 		% Look for a simple goal which some constraint depends
@@ -310,6 +414,15 @@
 		constraint__add_constant_construction(ConstructVar, Goal,
 			Constraints0, Constraints1)
 	;	
+		% Prune away the constraints after a goal
+		% which cannot succeed -- they can never be
+		% executed.
+		{ goal_info_get_determinism(GoalInfo, Detism) },
+		{ determinism_components(Detism, _, at_most_zero) }
+	->
+		{ Constraints1 = [] },
+		{ Goals1 = [Goal - [] | Goals0] }	
+	;
 		% Don't propagate constraints into or past impure goals.
 		{ Goal = _ - GoalInfo },
 		{ goal_info_is_impure(GoalInfo) }
@@ -319,42 +432,34 @@
 			ConstraintGoals) },
 		{ list__map(add_empty_constraints, [Goal | ConstraintGoals],
 			GoalsAndConstraints) },
-
 		{ list__append(GoalsAndConstraints, Goals0, Goals1) }
 	;
-		% Prune away the constraints after a goal
-		% which cannot succeed.
-		{ Goal = _ - GoalInfo },
-		{ goal_info_get_determinism(GoalInfo, Detism) },
-		{ determinism_components(Detism, _, at_most_zero) }
-	->
-		{ Constraints1 = [] },
-		{ Goals1 = [Goal - [] | Goals0] }	
-	;
 		% Don't move goals which can fail before a goal which
 		% can loop if `--fully-strict' is set.
-		{ module_info_globals(ModuleInfo, Globals) },
 		{ \+ code_aux__goal_cannot_loop(ModuleInfo, Goal) },
+		{ module_info_globals(ModuleInfo, Globals) },
 		{ globals__lookup_bool_option(Globals, fully_strict, yes) }
 	->
-		{ constraint__filter_dependent_constraints(OutputVars, 
-			Constraints0, [], ConstraintsToAttach,
+		{ constraint__filter_dependent_constraints(NonLocals,
+			ChangedVars, Constraints0, [], ConstraintsToAttach,
 			[], OtherConstraints) },
 		{ constraint__flatten_constraints(OtherConstraints,
 			ConstraintGoals) },
 		{ list__map(add_empty_constraints, ConstraintGoals,
 			GoalsAndConstraints) },
-		{ list__append(
-			[Goal - ConstraintsToAttach | GoalsAndConstraints],
-			Goals0, Goals1) },
+		{ Goals1 = 
+			[attach_constraints(Goal, ConstraintsToAttach)
+				| GoalsAndConstraints]
+			++ Goals0 },
 		{ Constraints1 = [] }
 	;
-		{ constraint__filter_dependent_constraints(OutputVars, 
-			Constraints0, [], ConstraintsToAttach,
+		{ constraint__filter_dependent_constraints(NonLocals,
+			OutputVars, Constraints0, [], ConstraintsToAttach,
 			[], Constraints1) },
-		{ Goals1 = [Goal - ConstraintsToAttach | Goals0] }
+		{ Goals1 = [attach_constraints(Goal, ConstraintsToAttach)
+				| Goals0] }
 	),
-	constraint__annotate_conj_constraints(ModuleInfo, RevGoals0, 
+	constraint__annotate_conj_constraints(ModuleInfo, RevConjuncts0, 
 		Constraints1, Goals1, Goals).
 
 :- pred add_empty_constraints(hlds_goal::in,
@@ -362,20 +467,43 @@
 
 add_empty_constraints(Goal, Goal - []).
 
+:- func attach_constraints(hlds_goal, list(constraint)) =
+		pair(hlds_goal, list(constraint)).
+
+attach_constraints(Goal, Constraints0) = Goal - Constraints :-
+        ( Goal = call(_, _, _, _, _, _) - _ ->
+                Constraints = list__map(
+                    (func(constraint(Goal0, B, C, Constructs0)) =
+                        constraint(add_constraint_feature(Goal0), B, C,
+                            list__map(add_constraint_feature, Constructs0))
+                    ), Constraints0)
+        ;
+                Constraints = Constraints0
+        ).
+
+:- func add_constraint_feature(hlds_goal) = hlds_goal.
+
+add_constraint_feature(Goal - GoalInfo0) = Goal - GoalInfo :-
+	goal_info_add_feature(GoalInfo0, constraint, GoalInfo).
+
+%-----------------------------------------------------------------------------%
+
+
 :- pred constraint__add_constant_construction(prog_var::in, hlds_goal::in,
 		list(constraint)::in, list(constraint)::out,
 		constraint_info::in, constraint_info::out) is det.
 
 constraint__add_constant_construction(_, _, [], []) --> [].
 constraint__add_constant_construction(ConstructVar, Construct0,
-		[Constraint0 - Constructs0 | Constraints0],
-		[Constraint - Constructs | Constraints]) -->
+		[Constraint0 | Constraints0],
+		[Constraint | Constraints]) -->
+	{ Constraint0 = constraint(ConstraintGoal0, ChangedVars,
+				IncompatibleInstVars, Constructs0) },
 	(
-		{
-		Constraint0 = _ - ConstraintInfo,
-		goal_info_get_nonlocals(ConstraintInfo, ConstraintNonLocals),
-		set__member(ConstructVar, ConstraintNonLocals)
-		}
+		{ ConstraintGoal0 = _ - ConstraintInfo },
+		{ goal_info_get_nonlocals(ConstraintInfo,
+			ConstraintNonLocals) },
+		{ set__member(ConstructVar, ConstraintNonLocals) }
 	->
 		VarSet0 =^ varset,
 		VarTypes0 =^ vartypes,
@@ -386,47 +514,70 @@
 		^ vartypes := VarTypes,
 		{ map__from_assoc_list([ConstructVar - NewVar], Subn) },
 		{ goal_util__rename_vars_in_goal(Construct0,
-			Subn, Construct1) },
-		{ Construct1 = ConstructExpr - ConstructInfo1 },
-		{ goal_info_add_feature(ConstructInfo1,
-			constraint, ConstructInfo) },
-		{ Constructs = [ConstructExpr - ConstructInfo | Constructs0] },
-		{ goal_util__rename_vars_in_goal(Constraint0,
-			Subn, Constraint) }
+			Subn, Construct) },
+		{ Constructs = [Construct | Constructs0] },
+		{ goal_util__rename_vars_in_goal(ConstraintGoal0,
+			Subn, ConstraintGoal) },
+		{ Constraint = constraint(ConstraintGoal, ChangedVars,
+				IncompatibleInstVars, Constructs) }
 	;
-		{ Constraint = Constraint0 },
-		{ Constructs = Constructs0 }
+		{ Constraint = Constraint0 }
 	),
 	constraint__add_constant_construction(ConstructVar, Construct0,
 		Constraints0, Constraints). 
 
+%-----------------------------------------------------------------------------%
+
 	% Find all constraints which depend on the
 	% output variables of the goal.
-:- pred constraint__filter_dependent_constraints(set(prog_var),
+:- pred constraint__filter_dependent_constraints(set(prog_var), set(prog_var),
 		list(constraint), list(constraint), list(constraint),
 		list(constraint), list(constraint)).
-:- mode constraint__filter_dependent_constraints(in, in, 
+:- mode constraint__filter_dependent_constraints(in, in, in,
 		in, out, in, out) is det.
 
-constraint__filter_dependent_constraints(_Vars, [], RevToAttach, ToAttach, 
-		RevOthers, Others) :-
+constraint__filter_dependent_constraints(_NonLocals, _Vars, [],
+		RevToAttach, ToAttach, RevOthers, Others) :-
 	list__reverse(RevToAttach, ToAttach),
 	list__reverse(RevOthers, Others).
-constraint__filter_dependent_constraints(GoalOutputVars, [Constraint | Goals],
-		ToAttach0, ToAttach, Others0, Others) :-
-	Constraint = Goal - _,
-	Goal = _ - GoalInfo,
-	goal_info_get_nonlocals(GoalInfo, NonLocals),
-	set__intersect(NonLocals, GoalOutputVars, Intersection),
-	( set__empty(Intersection) ->
+constraint__filter_dependent_constraints(NonLocals, GoalOutputVars,
+		[Constraint | Goals], ToAttach0, ToAttach, Others0, Others) :-
+	Constraint = constraint(ConstraintGoal, _, IncompatibleInstVars, _),
+	ConstraintGoal = _ - ConstraintGoalInfo,
+	goal_info_get_nonlocals(ConstraintGoalInfo, ConstraintNonLocals),
+	set__intersect(ConstraintNonLocals, GoalOutputVars,
+		OutputVarsUsedByConstraint),
+
+	% Don't reorder a constraint which changes the inst of
+	% a variable in such a way that the new inst is incompatible
+	% with the old inst (e.g. by losing uniqueness),
+	% with any goal which has that variable in its non-locals set.
+	%
+	% Don't reorder a constraint with another constraint which
+	% changes the instantiatedness of one of its input variables.
+	set__intersect(NonLocals, IncompatibleInstVars,
+		IncompatibleInstVarsUsedByGoal),
+	(
+		(
+			set__empty(OutputVarsUsedByConstraint),
+			set__empty(IncompatibleInstVarsUsedByGoal)
+		;
+			list__member(EarlierConstraint, ToAttach0),
+			EarlierConstraint = constraint(_,
+				EarlierChangedVars, _, _),
+			set__intersect(EarlierChangedVars, ConstraintNonLocals,
+				EarlierConstraintIntersection),
+			\+ set__empty(EarlierConstraintIntersection)
+		)
+	->
 		Others1 = [Constraint | Others0],
 		ToAttach1 = ToAttach0
 	;
 		Others1 = Others0,
 		ToAttach1 = [Constraint | ToAttach0]
 	),
-	constraint__filter_dependent_constraints(GoalOutputVars, Goals, 
-		ToAttach1, ToAttach, Others1, Others).
+	constraint__filter_dependent_constraints(NonLocals, GoalOutputVars,
+		Goals, ToAttach1, ToAttach, Others1, Others).
 	
 %-----------------------------------------------------------------------------%
 
@@ -440,7 +591,7 @@
 	{ list__reverse(RevGoals, Goals) }.
 constraint__propagate_conj_constraints([Goal0 - Constraints | Goals0],
 		RevGoals0, RevGoals) -->
-	constraint__propagate_goal_2(Goal0, Constraints, GoalList1),
+	constraint__propagate_conj_sub_goal(Goal0, Constraints, GoalList1),
 	{ list__reverse(GoalList1, RevGoalList1) },
 	{ list__append(RevGoalList1, RevGoals0, RevGoals1) },
 	constraint_info_update_goal(Goal0),
@@ -500,6 +651,53 @@
 	;
 		^ changed := yes
 	).
+
+%-----------------------------------------------------------------------------%
+
+	% Remove all `constraint' goal features from the goal_infos
+	% of all sub-goals of the given goal.
+:- func strip_constraint_markers(hlds_goal) = hlds_goal.
+
+strip_constraint_markers(Goal - GoalInfo0) =
+		strip_constraint_markers_expr(Goal) - GoalInfo :-
+	( goal_info_has_feature(GoalInfo0, constraint) ->
+		goal_info_remove_feature(GoalInfo0, constraint, GoalInfo)
+	;
+		GoalInfo = GoalInfo0
+	).
+
+:- func strip_constraint_markers_expr(hlds_goal_expr) = hlds_goal_expr.
+
+strip_constraint_markers_expr(conj(Goals)) =
+		conj(list__map(strip_constraint_markers, Goals)).
+strip_constraint_markers_expr(disj(Goals, SM)) =
+		disj(list__map(strip_constraint_markers, Goals), SM).
+strip_constraint_markers_expr(switch(Var, CanFail, Cases0, SM)) =
+		switch(Var, CanFail, Cases, SM) :-
+	Cases = list__map(
+		    (func(case(ConsId, Goal)) =
+			case(ConsId, strip_constraint_markers(Goal))
+		    ), Cases0).
+strip_constraint_markers_expr(not(Goal)) =
+		not(strip_constraint_markers(Goal)).
+strip_constraint_markers_expr(some(Vars, Remove, Goal)) =
+		some(Vars, Remove, strip_constraint_markers(Goal)).
+strip_constraint_markers_expr(if_then_else(Vars, If, Then, Else, SM)) =
+		if_then_else(Vars, strip_constraint_markers(If),
+			strip_constraint_markers(Then),
+			strip_constraint_markers(Else), SM).
+strip_constraint_markers_expr(par_conj(Goals, SM)) =
+		par_conj(list__map(strip_constraint_markers, Goals), SM).
+strip_constraint_markers_expr(Goal) = Goal :-
+	Goal = foreign_proc(_, _, _, _, _, _, _).
+strip_constraint_markers_expr(Goal) = Goal :-
+	Goal = generic_call(_, _, _, _).
+strip_constraint_markers_expr(Goal) = Goal :-
+	Goal = call(_, _, _, _, _, _).
+strip_constraint_markers_expr(Goal) = Goal :-
+	Goal = unify(_, _, _, _, _).
+strip_constraint_markers_expr(Goal) = Goal :-
+	Goal = shorthand(_).
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------