[m-rev.] For review: (no attachments) Extensions to constraints based mode analysis.
Richard Fothergill
fothergill at gmail.com
Fri Jan 27 11:37:45 AEDT 2006
For review by Zoltan (and anyone interested - Ralph, Julien)
Estimated hours taken: 120.
Extend constraints based mode analysis.
Constraints on the producing and consuming goals for program
variables are now solved, and the solutions used for
conjunction reordering. The resulting HLDS is then thrown away,
after maybe being dumped (stage 33).
Extend dumping of mode analysis constraints.
Constraints are no longer dumped to file - they are displayed as
error messages when the --debug-mode-constraints is set. After
conjunction ordering, the original goal paths are printed in the
order they now appear.
(Could someone please set out for me the areas of documentation
that need to be changed to describe the altered functionality?
eg in compiler_design, etc)
compiler/options.m:
Added the option described above.
compiler/check_hlds.m:
Grouped ":- include_module"s for propagation solver
constraints based mode analysis, and included
new modules in this area - mcsolver and
ordering_mode_constraints.
compiler/mode_constraints.m:
Changes to the nature of constraint dumping - introduction
of the use of --debug-mode-constraints.
Introduction of conjunction ordering (call to module
ordering_mode_constraints).
compiler/prop_mode_constraints.m:
Changes to way constraints are dumped as described above.
Changes to the way constraint variables are created -
3D
constraint variables can now be constructed as needed
when the constraints are built.
Structural changes to make constraint generation more
natural (eg introduction of state variables, instead
of use of functions).
compiler/abstract_mode_constraints.m:
Changes to the way constraints are stored - the old
speculative code became redundant with the introduction
of rafe's solver (see mcsolver.m).
New, specialised constraint generation predicates.
Constraints are now created with a context attached,
and space was left for adding other information.
compiler/build_mode_constraints.m:
Changes to the way constraint variables are created -
constraint variables can now be constructed as needed
when the constraints are built.
Structural changes to make constraint generation more
natural (eg introduction of state variables, instead
of use of functions).
Constraints are now created with a context attached.
compiler/ordering_mode_constraints.m:
New file. Uses solutions to the producer/consumer
constraints to order conjunctions for mode analysis.
Does not yet do mode inference.
compiler/mcsolver.m:
New file. Written by rafe, modified by myself to
accomodate the rest of the mode constraints branch
(and a new constraint type). Solves mode constraints
to produce bindings for constraint variables from
producer/consumer analysis.
-Richard (richardf)
Index: compiler/abstract_mode_constraints.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/abstract_mode_constraints.m,v
retrieving revision 1.4
diff -u -r1.4 abstract_mode_constraints.m
--- compiler/abstract_mode_constraints.m 8 Aug 2005 02:57:07 -0000 1.4
+++ compiler/abstract_mode_constraints.m 24 Jan 2006 04:10:04 -0000
@@ -5,70 +5,74 @@
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%-----------------------------------------------------------------------------%
-%
+
% File: abstract_mode_constraints.m
% Main author: richardf
-%
+
% This module contains data structures designed for use with constraints
-% based mode analysis. They represent constraints between constraint
-% variables, such as those one might use to describe where a program
-% variable may be produced.
-%
+% based mode analysis. It deals specifically with constraints for
+% determining producing and consuming goals for program variables.
+
%-----------------------------------------------------------------------------%
:- module check_hlds.abstract_mode_constraints.
-
:- interface.
+:- import_module hlds.hlds_pred.
+:- import_module parse_tree.prog_data.
+
+:- import_module assoc_list.
:- import_module bool.
-:- import_module counter.
:- import_module io.
:- import_module list.
:- import_module map.
+:- import_module multi_map.
:- import_module std_util.
:- import_module term.
:- import_module varset.
%-----------------------------------------------------------------------------%
+ % `unit'-like type used to distinguish mode constraint variables.
+ %
:- type mc_type.
:- type mc_var == var(mc_type). % Constraint variable.
:- type mc_varset == varset(mc_type). % Source of constraint variables.
%-----------------------------------------------------------------------------%
%
+% Abstract Constraints
+%
+
% Data structures for storing abstract constraints. Conjunctions and
-% disjunctions can be formed. The atomic constraints between constraint
+% disjunctions can be nested. The atomic constraints between constraint
% variables are designed around the types of constraints required by
-% constraint based mode analysis. The paper "Constraint-based mode
-% analysis of Mercury" by David Overton, Zoltan Somogyi and Peter
-% Stuckey documents these mode constraints.
-%
+% producer/consumer determining in constraint based mode analysis. The
+% paper "Constraint-based mode analysis of Mercury" by David Overton,
+% Zoltan Somogyi and Peter Stuckey documents these mode constraints.
% Represents conjunctions and disjunctions between atomic
- % constraints on constraint variables. The advantage of the
- % constraints for this implementation of mode checking is that
- % they can be expressed almost entirely as variable to variable
- % constraints, with little use for the disj and conj functors of
- % this structure.
+ % constraints on constraint variables.
%
:- type constraint_formulae == list(constraint_formula).
:- type constraint_formula
---> atomic_constraint(var_constraint)
; disj(constraint_formulae)
- % Initially included for the purposes of
- % representing the mode declaration constraints,
- % which are a disjunction of conjunctions of
- % other constraints. The intended form is:
- % disj([conj(...), ..., conj(...)]) Note
- % disj([]) represents false.
+ % Primarily included for the purposes of representing mode
+ % declaration and call constraints, which are a disjunction
+ % of conjunctions of atomic constraints. The intended form
+ % is: disj([conj(...), ..., conj(...)])
+ %
+ % Note: disj([]) represents false.
; conj(constraint_formulae).
% See disj.
- % Note that conj([]) is the empty constraint, or true.
+ % Note: conj([]) is the empty constraint, or true.
-% var_constraint represents a constraint between variables
+ % var_constraint represents a boolean constraint between
+ % producer/consumer constraint variables
+ %
:- type var_constraint == var_constraint(mc_type).
:- type var_constraint(T)
---> equiv_bool(var(T), bool)
@@ -83,292 +87,430 @@
; equiv_disj(var(T), list(var(T)))
% equiv_disj(X, [Y1,...,Yn]) gives X<->OR(Y1,...,Yn)
- % XXX Thinking of making a constraint that is
- % the conjunction of equiv_disj and at_most_one
- % because they occur together so often.
; at_most_one(list(var(T)))
- % at_most_one(Xs) gives
+ % at_most_one(Xs) gives the constraint
% (all Xi, Xj in Xs).(i = j or not(Xi and Xj))
- ; at_least_one(list(var(T)))
- % at_least_one(Xs) gives OR(Xs)
-
; exactly_one(list(var(T))).
- % exactly_one(Xs) gives
- % at_least_one(Xs) and at_most_one(Xs)
+ % exactly_one(Xs) gives XOR(Xs)
- % Attempts to print the constraint_formulae it is passed in a
- % human readable format. Always puts a new line after it is finished.
+ % Maps from producer/consumer constraint variables to a boolean
+ % binding for them.
%
-:- pred pretty_print_constraints(mc_varset::in, constraint_formulae::in,
- io::di, io::uo) is det.
+:- type mc_bindings == map(mc_var, bool).
%-----------------------------------------------------------------------------%
%
-% The remainder of the code in this module is not in use! It is intended
-% to supply a basic structure for a propagation solver to deal with the
-% constraints defined above.
-%
-% Propagation would work like this: Initially constraint variables are
-% bound during constraint construction, propagation, or once all
-% possible propagation has been done, a variable may have true or false
-% arbitrarily chosen for it and the choicepoint recorded. Once a
-% variable has been bound, the propagator looks it up in the var_map
-% field of mode_constraints_info. The var_state structure will then
-% reveal which constraints this variable participates in. These
-% constraints are then looked up in the constraint_map field of
-% mode_constraints_info. Then can be refined due to the variable having
-% been bound, and may now imply new bindings on other variables. These
-% new variables can be put in a stack, queue or similar structure to be
-% bound and propagated once the first variable's constraints have been
-% fully processed.
+% Constraint collection structures.
%
-% This code is by no means complete; some speculative fields exist or
-% have been commented out. Only the basic structure and functionality
-% described above is truly intended.
-%
-
-% XXX What's lacking in this is the following:
-% Done 1) An at least one constraint, for when equiv_disj simplifies
-% 2) A good reason to keep the propagate if true/false lists
-% 3) A separate way to store lists of variable equivalences,
-% so that only one of a list of equivalent variables need
-% be used in the constraints.
-% 4) A way to store whether a variable being bound will have
-% an effect on a particular constraint - but this can change
-% without reference to a variable, so maybe not a practical idea.
-% 5) T/F lists for variables known to be true/false for all
-% possible models?
-% 6) Access and manipulation predicates.
-
-:- type mode_constraints_info --->
- mode_constraints_info(
- constraint_map :: map(constraint_id, constraint),
- % Constraining the variables in the var_map.
- var_map :: map(mc_var, var_state),
- % The variables this constraint system constrains.
+:- type constraint_and_annotation ==
+ pair(constraint_formula, constraint_annotation).
- id_counter :: counter
- % Supplies unique IDs for the constraint map.
+ % Various information about the creation of the constraint in
+ % question.
+ %
+:- type constraint_annotation
+ ---> constraint_annotation(
+ context :: prog_context
+ % Context of the goal this constraint
+ % was formed for.
+ ).
+
+ % producer/consumer constraints for a predicate.
+ %
+:- type pred_p_c_constraints --->
+ pred_constraints(
+ proc_constraints :: multi_map(proc_id, constraint_and_annotation),
+ % Stores procedure specific constraints
+ % such as mode declaration constraints.
+ pred_constraints :: assoc_list(constraint_formula,
+ constraint_annotation)
+ % Stores constraints that apply to all
+ % procedures of the predicate -
+ % typically generated from its clauses.
).
-:- type constraint_id == int.
+%-----------------------------------------------------------------------------%
+
+ % Prints the constraint_formulae it is passed in a human readable
+ % format.
+ %
+:- pred pretty_print_constraints(mc_varset::in, constraint_formulae::in,
+ io::di, io::uo) is det.
+
+ % Prints the constraint_formulae it is passed in a human readable
+ % format.
+ %
+:- pred dump_constraints_and_annotations(mc_varset::in,
+ assoc_list(constraint_formula, constraint_annotation)::in,
+ io::di, io::uo) is det.
-:- type constraint --->
- constraint(
- id :: constraint_id,
+ % Prints a list of models for the constraint system.
+ %
+:- pred pretty_print_solutions(mc_varset::in, list(mc_bindings)::in, io::di,
+ io::uo) is det.
- current :: constraint_formula_and_vars,
- % Formula modified as variables are bound.
+%-----------------------------------------------------------------------------%
- original :: constraint_formula_and_vars
+ % Initialises all the parts of a pred_p_c_constraints type.
+ %
+:- pred abstract_mode_constraints.init(pred_p_c_constraints::out) is det.
-% dead :: bool
-% % For if the current constraint is empty...
-% % don't know if this will be used.
- ).
+ % Function version if init/1.
+ %
+:- func abstract_mode_constraints.init = pred_p_c_constraints.
-:- type constraint_formula_and_vars --->
- constraint_formula_and_vars(
- constraint_formula :: constraint_formula,
- participating_vars :: list(mc_var)
- ).
+ % add_constraint(Formula, !PredConstraints) adds the constraint
+ % given by Formula to the constraint system in PredConstraints.
+ %
+:- pred abstract_mode_constraints.add_constraint(prog_context::in,
+ constraint_formula::in, pred_p_c_constraints::in,
+ pred_p_c_constraints::out) is det.
-:- type var_state --->
- var_state(
- is_bound :: maybe(var_binding),
- % If it is bound, some certain information
- % should be recorded. See var_binding type.
-
- is_constrained :: list(constrainment_info)
- % A list of the constraints that this variable
- % participates in. May include propagation tree
- % information in the form of branches for bound
- % true/false, however this may have a
- % significant cost in space.
- ).
+ % Function version of add_constraint/3.
+ %
+:- func abstract_mode_constraints.add_constraint(prog_context,
+ constraint_formula, pred_p_c_constraints) = pred_p_c_constraints.
-:- type var_binding --->
- var_binding(
- bool :: bool,
- % What the variable has been bound to.
-
- binding_constraint :: constraint_id,
- % The constraint that finally bound it.
-
- history :: list(mc_var)
- % The variables in the constraint that bound this
- % variable that had already been bound at that point
- % - their binding_constraint and history can be looked
- % at recursively to build the full history. I strongly
- % prefer this to listing the full history each time
- % a variable is bound, for space considerations.
- ).
-
-:- type constrainment_info --->
- constrainment_info(
-% variable :: mc_var,
-% % To make it clear what variable
-% % the propagation information is for.
-%
-% propagate_if_true :: list(var_binding),
-% % The history field should be empty.
-% % In the end it gets the participating
-% % variables of this constraint that
-% % have been bound.
-%
-% propagate_if_false :: list(var_binding),
+ % Adds a procedure specific constraint to the system.
+ %
+:- pred abstract_mode_constraints.add_constraint(prog_context::in, proc_id::in,
+ constraint_formula::in, pred_p_c_constraints::in,
+ pred_p_c_constraints::out) is det.
- constraint :: constraint_id
- ).
+ % pred_constraints_to_formulae rips the barebones
+ % constraints (those that apply to all procedures of a
+ % predicate) out of the pred_p_c_constraints structure
+ % and returns them as a list of constraint formulae.
+ %
+:- func abstract_mode_constraints.pred_constraints_to_formulae(
+ pred_p_c_constraints) = constraint_formulae.
- % Initiates all the parts of a mode_constraints_info type.
+ % pred_constraints_to_formulae/2 returns all constraints that
+ % apply to the given procedure from the pred_p_c_constraints,
+ % including constraints that apply to all procedures.
%
-:- pred abstract_mode_constraints.init(mode_constraints_info::out) is det.
+:- func abstract_mode_constraints.pred_constraints_to_formulae(
+ proc_id, pred_p_c_constraints) = constraint_formulae.
- % Function version if init/1.
-:- func abstract_mode_constraints.init = mode_constraints_info.
+ % pred_constraints_to_formulae_and_annotations returns constraints
+ % that apply to all procedures of a predicate as a list of pairs of
+ % constraint_formula and constraint_annotation.
+ %
+:- func pred_constraints_to_formulae_and_annotations(pred_p_c_constraints) =
+ assoc_list(constraint_formula, constraint_annotation).
- % Incorporates a new constraint into the system.
+ % pred_constraints_to_formulae_and_annotations(ProcId, PredConstraints)
+ % returns all constraints that apply to the given procedure from the
+ % pred_p_c_constraints, including constraints that apply to all
+ % procedures, with their constraint annotations, in pairs.
%
-:- pred abstract_mode_constraints.add_constraint(constraint_formula::in,
- mode_constraints_info::in, mode_constraints_info::out) is det.
+:- func pred_constraints_to_formulae_and_annotations(proc_id,
+ pred_p_c_constraints) = assoc_list(constraint_formula,
+ constraint_annotation).
- % Function version of add_constraint/3.
+ % proc_constraints_to_formulae_and_annotations(ProcId, PredConstraints)
+ % returns constraints that apply specifically to the given
+ % procedure (but not constraints that apply to all procedures).
%
-:- func abstract_mode_constraints.add_constraint(constraint_formula,
- mode_constraints_info) = mode_constraints_info.
+:- func proc_constraints_to_formulae_and_annotations(proc_id,
+ pred_p_c_constraints) = assoc_list(constraint_formula,
+ constraint_annotation).
+
+%-----------------------------------------------------------------------------%
+
+ % equiv_no(Context, MCVar, !Constraints) constrains MCVar to `no' in
+ % Constraints. Context should be the context of the goal or
+ % declaration that imposed this constraint.
+ %
+:- pred equiv_no(prog_context::in, mc_var::in, pred_p_c_constraints::in,
+ pred_p_c_constraints::out) is det.
+
+ % equivalent(Context, MCVars, !Constraints) constrains MCVars in
+ % Constraints to all take the same value. Context should be the context of
+ % the goal or declaration that imposed this constraint.
+ %
+:- pred equivalent(prog_context::in, list(mc_var)::in,
pred_p_c_constraints::in,
+ pred_p_c_constraints::out) is det.
+
+ % equiv_disj(Context, X, Ys, !Constraints) constrains X and Ys in
+ % Constraints such that (X <-> disj(Ys)) - ie if X is true at least one of
+ % Ys must be true, if X is false, all of Ys must be false. Context should
+ % be the context of the goal or declaration that imposed this constraint.
+ %
+:- pred equiv_disj(prog_context::in, mc_var::in, list(mc_var)::in,
+ pred_p_c_constraints::in, pred_p_c_constraints::out) is det.
+
+ % at_most_one(Context, MCVars, !Constraints) constrains MCVars in
+ % Constraints such that at most one of them can be true. Context should be
+ % the context of the goal or declaration that imposed this constraint.
+ %
+:- pred at_most_one(prog_context::in, list(mc_var)::in,
+ pred_p_c_constraints::in, pred_p_c_constraints::out) is det.
+
+ % not_both(Context, A, B, !Constraints) constrains mode constraint
+ % variables A and B in Constraints by the constraint (not A ^ B). Context
+ % should be the context of the goal or declaration that imposed this
+ % constraint.
+ %
+:- pred not_both(prog_context::in, mc_var::in, mc_var::in,
+ pred_p_c_constraints::in, pred_p_c_constraints::out) is det.
+
+ % exactly_one(Context, MCVars, !Constraints) constrains MCVars in
+ % Constraints such that exactly one of them is `yes'. Context should be
+ % the context of the goal or declaration that imposed this constraint.
+ %
+:- pred exactly_one(prog_context::in, list(mc_var)::in,
+ pred_p_c_constraints::in, pred_p_c_constraints::out) is det.
+
+ % xor(Context, A, B, !Constraints) constrains mode constraint variables A
+ % and B in Constraints by the constraint (A xor B), ie constrains exactly
+ % one of them to be true. Context should be the context of the goal or
+ % declaration that imposed this constraint.
+ %
+:- pred xor(prog_context::in, mc_var::in, mc_var::in, pred_p_c_constraints::in,
+ pred_p_c_constraints::out) is det.
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
:- implementation.
+:- import_module parse_tree.error_util.
+
+:- import_module int.
:- import_module string.
%-----------------------------------------------------------------------------%
+ % `unit'-like type used to distinguish mode constraint variables.
+ %
:- type mc_type ---> mc_type.
- % Initiates all the parts of a mode_constraints_info type.
+ % Initialises all the parts of a mode_constraints_info type.
%
-abstract_mode_constraints.init(ModeConstraintsInfo) :-
- % Start allocating ids from 0.
- ModeConstraintsInfo = mode_constraints_info(map.init, map.init,
- counter.init(0)).
+abstract_mode_constraints.init(pred_constraints(multi_map.init, [])).
% See the predicate version.
%
-abstract_mode_constraints.init = ModeConstraintsInfo :-
- abstract_mode_constraints.init(ModeConstraintsInfo).
+abstract_mode_constraints.init = PredConstraints :-
+ abstract_mode_constraints.init(PredConstraints).
- % Incorporates a new constraint into the system.
+ % add_constraint(Formula, !PredConstraints) adds the constraint
+ % given by Formula to the constraint system in PredConstraints.
%
-abstract_mode_constraints.add_constraint(ConstraintFormula,
- !ModeConstraintsInfo) :-
- formula_to_formula_and_vars(ConstraintFormula, Vars, FormulaAndVars),
- counter.allocate(NewID, !.ModeConstraintsInfo ^ id_counter, NewCounter),
- !:ModeConstraintsInfo = !.ModeConstraintsInfo ^ id_counter := NewCounter,
- update_vars_map_with_constrainment_info(constrainment_info(NewID),
- Vars, !ModeConstraintsInfo),
- Constraint = constraint(NewID, FormulaAndVars, FormulaAndVars),
- ConstraintMap0 = !.ModeConstraintsInfo ^ constraint_map,
- map.det_insert(ConstraintMap0, NewID, Constraint, ConstraintMap),
- !:ModeConstraintsInfo = !.ModeConstraintsInfo ^ constraint_map :=
- ConstraintMap.
+abstract_mode_constraints.add_constraint(Context,
+ ConstraintFormula, !PredConstraints) :-
+ AllProcsConstraints = !.PredConstraints ^ pred_constraints,
+ ConstraintAnnotation = constraint_annotation(Context),
+ FormulaAndAnnotation = pair(ConstraintFormula, ConstraintAnnotation),
+ !:PredConstraints = !.PredConstraints ^ pred_constraints :=
+ list.cons(FormulaAndAnnotation, AllProcsConstraints).
+
% Functional version of add_constraint/3.
%
-abstract_mode_constraints.add_constraint(CF, MCI0) = MCI :-
- abstract_mode_constraints.add_constraint(CF, MCI0, MCI).
+abstract_mode_constraints.add_constraint(Ctxt, CF, PCs0) = PCs :-
+ abstract_mode_constraints.add_constraint(Ctxt, CF, PCs0, PCs).
+
+ % add_constraint(Context, ProcId, Formula, !PredConstraints) adds the
+ % constraint given by Formula to the constraint system in
+ % PredConstraints, and associates it specificaly with procedure
+ % ProcId.
+ %
+add_constraint(Context, ProcId, ConstraintFormula, !PredConstraints) :-
+ ProcConstraints = !.PredConstraints ^ proc_constraints,
+ ConstraintAnnotation = constraint_annotation(Context),
+ FormulaAndAnnotation = pair(ConstraintFormula, ConstraintAnnotation),
+
+ !:PredConstraints = !.PredConstraints ^ proc_constraints :=
+ multi_map.add(ProcConstraints, ProcId, FormulaAndAnnotation).
+
+ % pred_constraints_to_formulae returns constraints that apply
+ % to all procedures of a predicate as a list of constraint formulae.
+ %
+pred_constraints_to_formulae(PCs) = assoc_list.keys(PCs ^ pred_constraints).
+
+ % pred_constraints_to_formulae/2 returns all constraints that
+ % apply to the given procedure from the pred_p_c_constraints,
+ % including constraints that apply to all procedures.
+ %
+pred_constraints_to_formulae(ProcId, PredConstraints) = ConstraintFormulae :-
+ ThisProcConstraints = multi_map.lookup(PredConstraints ^ proc_constraints,
+ ProcId),
+ AllProcConstraints = PredConstraints ^ pred_constraints,
+ ConstraintFormulae = assoc_list.keys(ThisProcConstraints) ++
+ assoc_list.keys(AllProcConstraints).
+
+ % pred_constraints_to_formulae_and_annotations returns constraints
+ % that apply to all procedures of a predicate as a list of pairs of
+ % constraint_formula and constraint_annotation.
+ %
+pred_constraints_to_formulae_and_annotations(PredConstraints) =
+ PredConstraints ^ pred_constraints.
+
+ % pred_constraints_to_formulae_and_annotations(PredConstraints)
+ % returns all constraints that apply to the given procedure from the
+ % pred_p_c_constraints, including constraints that apply to all
+ % procedures, with their constraint annotations, in pairs.
+ %
+pred_constraints_to_formulae_and_annotations(ProcId, PredConstraints) =
+ ConstraintFormulae :-
+ ThisProcConstraints = multi_map.lookup(PredConstraints ^ proc_constraints,
+ ProcId),
+ AllProcConstraints = PredConstraints ^ pred_constraints,
+ ConstraintFormulae = ThisProcConstraints ++ AllProcConstraints.
+
+proc_constraints_to_formulae_and_annotations(ProcId, PredConstraints) =
+ multi_map.lookup(PredConstraints ^ proc_constraints, ProcId).
+
+%-----------------------------------------------------------------------------%
+%
+% Predicates to allow easy adding of var_constraints.
+%
+
+equiv_no(Context, MCVar, !Constraints) :-
+ abstract_mode_constraints.add_constraint(Context,
+ atomic_constraint(equiv_bool(MCVar, no)), !Constraints).
+
+equivalent(Context, MCVars, !Constraints) :-
+ abstract_mode_constraints.add_constraint(Context,
+ atomic_constraint(equivalent(MCVars)), !Constraints).
+
+equiv_disj(Context, X, Ys, !Constraints) :-
+ abstract_mode_constraints.add_constraint(Context,
+ atomic_constraint(equiv_disj(X, Ys)), !Constraints).
+
+at_most_one(Context, MCVars, !Constraints) :-
+ abstract_mode_constraints.add_constraint(Context,
+ atomic_constraint(at_most_one(MCVars)), !Constraints).
+
+not_both(Context, A, B, !Constraints) :-
+ at_most_one(Context, [A, B], !Constraints).
+
+exactly_one(Context, MCVars, !Constraints) :-
+ abstract_mode_constraints.add_constraint(Context,
+ atomic_constraint(exactly_one(MCVars)), !Constraints).
+
+xor(Context, A, B, !Constraints) :-
+ exactly_one(Context, [A, B], !Constraints).
+
+%-----------------------------------------------------------------------------%
+%
+% Dumping constraints for --debug-mode-constraints
+%
+
+dump_constraints_and_annotations(Varset, ConstraintsAndAnnotations, !IO) :-
+ Indent = 0,
+ keys_and_values(ConstraintsAndAnnotations, Constraints, Annotations),
+ list.foldl_corresponding(dump_constraint(Varset, Indent), Annotations,
+ Constraints, !IO).
+
+ % Dumps a list of constraints using the same constraint annotation
+ % at indent level indicated by the int.
+ %
+:- pred dump_constraints(mc_varset::in, int::in, constraint_annotation::in,
+ constraint_formulae::in, io::di, io::uo) is det.
+
+dump_constraints(Varset, Indent, Annotation, Constraints, !IO) :-
+ list.foldl(dump_constraint(Varset, Indent, Annotation), Constraints, !IO).
+
+ % Prints one constraint_formulae to the output. The int is an
+ % indent level.
+ %
+:- pred dump_constraint(mc_varset::in, int::in, constraint_annotation::in,
+ constraint_formula::in, io::di, io::uo) is det.
+
+dump_constraint(Varset, Indent, Annotation, disj(Constraints), !IO) :-
+ Context = context(Annotation),
+ write_error_pieces_maybe_with_context(yes(Context), Indent,
+ [words("disj(")], !IO),
+ dump_constraints(Varset, Indent+1, Annotation, Constraints, !IO),
+ write_error_pieces_maybe_with_context(yes(Context), Indent,
+ [words(") end disj")], !IO).
+
+dump_constraint(Varset, Indent, Annotation, conj(Constraints), !IO) :-
+ Context = context(Annotation),
+ write_error_pieces_maybe_with_context(yes(Context), Indent,
+ [words("conj(")], !IO),
+ dump_constraints(Varset, Indent+1, Annotation, Constraints, !IO),
+ write_error_pieces_maybe_with_context(yes(Context), Indent,
+ [words(") end conj")], !IO).
+
+dump_constraint(Varset, Indent, Annotation, atomic_constraint(Constraint),
+ !IO) :-
+ dump_var_constraint(Varset, Indent, Annotation, Constraint, !IO).
+
+ % Prints a var_constraint to the output. The int is an indent level.
+ %
+:- pred dump_var_constraint(mc_varset::in, int::in, constraint_annotation::in,
+ var_constraint::in, io::di, io::uo) is det.
+
+dump_var_constraint(Varset, Indent, Annotation, equiv_bool(X, Val), !IO) :-
+ mc_var_list_to_string(Varset, [X], VarName),
+ mc_var_val_to_string(Val, ValString),
+ Context = context(Annotation),
+
+ write_error_pieces_maybe_with_context(yes(Context), Indent,
+ [words(VarName ++ " = " ++ ValString)], !IO).
+
+dump_var_constraint(Varset, Indent, Annotation, equivalent(Xs), !IO) :-
+ mc_var_list_to_string(Varset, Xs, VarsString),
+ Context = context(Annotation),
+ write_error_pieces_maybe_with_context(yes(Context), Indent,
+ [words("equivalent(" ++ VarsString ++ ")")], !IO).
+
+dump_var_constraint(Varset, Indent, Annotation, implies(X, Y), !IO) :-
+ mc_var_list_to_string(Varset, [X], XName),
+ mc_var_list_to_string(Varset, [Y], YName),
+ Context = context(Annotation),
+
+ write_error_pieces_maybe_with_context(yes(Context), Indent,
+ [words(XName ++ " -> " ++ YName)], !IO).
+
+dump_var_constraint(Varset, Indent, Annotation, equiv_disj(X, Xs), !IO) :-
+ mc_var_list_to_string(Varset, [X], XName),
+ mc_var_list_to_string(Varset, Xs, XsString),
+ Context = context(Annotation),
+ Pieces = [words(XName ++ " <-> disj(" ++ XsString ++ ")")],
+
+ write_error_pieces_maybe_with_context(yes(Context), Indent, Pieces, !IO).
+
+dump_var_constraint(Varset, Indent, Annotation, at_most_one(Xs), !IO) :-
+ mc_var_list_to_string(Varset, Xs, XsString),
+ Pieces = [words("at_most_one(" ++ XsString ++ ")")],
+ Context = context(Annotation),
+ write_error_pieces_maybe_with_context(yes(Context), Indent, Pieces, !IO).
+
+dump_var_constraint(Varset, Indent, Annotation, exactly_one(Xs), !IO) :-
+ mc_var_list_to_string(Varset, Xs, XsString),
+ Pieces = [words("exactly_one(" ++ XsString ++ ")")],
+ Context = context(Annotation),
+ write_error_pieces_maybe_with_context(yes(Context), Indent, Pieces, !IO).
+
+ % mc_var_list_to_string(Varset, MCVars, MCVarsString)
+ % Makes a comma separated list of MCVars as a string.
+ %
+:- pred mc_var_list_to_string(mc_varset::in, list(mc_var)::in,
+ string::out) is det.
+
+mc_var_list_to_string(_Varset, [], "").
+mc_var_list_to_string(Varset, [MCVar], VarName) :-
+ varset.lookup_name(Varset, MCVar, VarName).
+mc_var_list_to_string(Varset, [MCVar1, MCVar2 | MCVars],
+ VarName ++ ", " ++ VarNames) :-
+ varset.lookup_name(Varset, MCVar1, VarName),
+ mc_var_list_to_string(Varset, [MCVar2 | MCVars], VarNames).
+
+ % Makes a string representation of an mc_var binding.
+ %
+:- pred mc_var_val_to_string(bool::in, string::out) is det.
+
+mc_var_val_to_string(yes, "yes").
+mc_var_val_to_string(no, "no").
- % update_vars_map_with_constrainment_info adds the supplied
- % constrainment_info to the list of constraints associated with each of
- % the variables supplied in the mode_constraints_info structure.
- %
-:- pred update_vars_map_with_constrainment_info(constrainment_info::in,
- list(mc_var)::in,
- mode_constraints_info::in, mode_constraints_info::out) is det.
-
-update_vars_map_with_constrainment_info(_ConstrainmentInfo, [], !MCI).
-update_vars_map_with_constrainment_info(ConstrainmentInfo, [Var | Vars],
- !MCI) :-
- ( map.search(!.MCI ^ var_map, Var, OldVarState) ->
- CInfoList = [ConstrainmentInfo | OldVarState ^ is_constrained],
- VarState = OldVarState ^ is_constrained := CInfoList,
- !:MCI = !.MCI ^ var_map :=
- map.det_update(!.MCI ^ var_map, Var, VarState)
- ;
- VarState = var_state(no, [ConstrainmentInfo]),
- !:MCI = !.MCI ^ var_map :=
- map.det_insert(!.MCI ^ var_map, Var, VarState)
- ),
- update_vars_map_with_constrainment_info(ConstrainmentInfo, Vars, !MCI).
-
- % formula_to_formula_and_vars makes the list Vars of variables that
- % appear in Formula and packages Formula and Vars together in
- % FormulaAndVars.
- %
-:- pred formula_to_formula_and_vars(constraint_formula::in, list(mc_var)::out,
- constraint_formula_and_vars::out) is det.
-
-formula_to_formula_and_vars(Formula, Vars, FormulaAndVars) :-
- formula_to_vars(Formula, Vars),
- FormulaAndVars = constraint_formula_and_vars(Formula, Vars).
-
- % Sub section of the formula_to_formula_and_vars predicate, Vars is the
- % variables that appear in Formula.
- %
-:- pred formula_to_vars(constraint_formula::in, list(mc_var)::out) is det.
-
-formula_to_vars(Formula, Vars) :-
- Formula = atomic_constraint(VarConstraint),
- var_constraint_to_vars(VarConstraint, Vars).
-formula_to_vars(Formula, Vars) :-
- Formula = disj(Formulae),
- list.foldr(
- (pred(Formula1::in, Vars1::in, VarsNew::out) is det :-
- formula_to_vars(Formula1, Vars2),
- append(Vars2, Vars1, VarsNew)
- ),
- Formulae, [], Vars).
-formula_to_vars(Formula, Vars) :-
- Formula = conj(Formulae),
- list.foldr(formula_to_vars_accumulate, Formulae, [], Vars).
-
-:- pred formula_to_vars_accumulate(constraint_formula::in,
- list(mc_var)::in, list(mc_var)::out) is det.
-
-formula_to_vars_accumulate(Formula, !Vars) :-
- formula_to_vars(Formula, NewVars),
- append(NewVars, !Vars).
-
- % var_constraint_to_vars takes a constraint between variables as input
- % and gives a list of those variables as output.
- %
-:- pred var_constraint_to_vars(var_constraint::in, list(mc_var)::out) is det.
-
-var_constraint_to_vars(equiv_bool(Var, _B), [Var]).
-var_constraint_to_vars(equivalent(Vars), Vars).
-var_constraint_to_vars(implies(V1, V2), [V1, V2]).
-var_constraint_to_vars(equiv_disj(Var, Vars), [Var | Vars]).
-var_constraint_to_vars(at_most_one(Vars), Vars).
-var_constraint_to_vars(at_least_one(Vars), Vars).
-var_constraint_to_vars(exactly_one(Vars), Vars).
-
-% Some thoughts:
-% add_constraint or similar pred adds the specified constraint (making
-% sure that the variables in it are added if need be, and updated with a
-% link to that constraint. What to do if one or more of the variables
-% are already bound? Still put in the original - so that you can always
-% know that if you put something in it will be there, but also put in an
-% updated version according to the bindings? This seems like a good
-% idea, though it forces propagation...
-% Any predicate that edits constraints leaves the 'original' as it is,
-% and only modifies the 'current' branch - eg replacing one var with an
-% equivalent etc.
%-----------------------------------------------------------------------------%
%
@@ -447,11 +589,6 @@
pretty_print_mc_vars(VarSet, Xs, !IO),
io.write_string(")", !IO).
-pretty_print_var_constraint(VarSet, at_least_one(Xs), !IO) :-
- io.write_string("at_least_one(", !IO),
- pretty_print_mc_vars(VarSet, Xs, !IO),
- io.write_string(")", !IO).
-
pretty_print_var_constraint(VarSet, exactly_one(Xs), !IO) :-
io.write_string("exactly_one(", !IO),
pretty_print_mc_vars(VarSet, Xs, !IO),
@@ -482,3 +619,34 @@
io.write_string(", ", !IO),
pretty_print_mc_vars(VarSet, Vars, !IO)
).
+
+%-----------------------------------------------------------------------------%
+
+ % Prints a list of models for the constraint system.
+ %
+pretty_print_solutions(VarSet, Solutions, !IO) :-
+ list.foldl2(pretty_print_bindings(VarSet), Solutions, 0, _, !IO).
+
+ % Prints the variable bindings of this solution, one per line.
+ %
+:- pred pretty_print_bindings(mc_varset::in, mc_bindings::in,
int::in, int::out,
+ io::di, io::uo) is det.
+
+pretty_print_bindings(VarSet, Bindings, N, N + 1, !IO) :-
+ io.write_string("Solution " ++ string.from_int(N) ++ ":\n{\n", !IO),
+ Variables = map.keys(Bindings),
+ list.foldl((pred(Var::in, IO0::di, IO::uo) is det :-
+ io.write_string(" ", IO0, IO1),
+ io.write_string(varset.lookup_name(VarSet, Var), IO1, IO2),
+ io.write_string(" = ", IO2, IO3),
+ map.lookup(Bindings, Var, Value),
+ io.print(Value, IO3, IO4),
+ io.nl(IO4, IO)
+ ),
+ Variables, !IO),
+ io.write_string("}\n", !IO).
+
+
+%----------------------------------------------------------------------------%
+:- end_module abstract_mode_constraints.
+%----------------------------------------------------------------------------%
Index: compiler/build_mode_constraints.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/build_mode_constraints.m,v
retrieving revision 1.7
diff -u -r1.7 build_mode_constraints.m
--- compiler/build_mode_constraints.m 28 Oct 2005 02:09:58 -0000 1.7
+++ compiler/build_mode_constraints.m 25 Jan 2006 03:58:16 -0000
@@ -5,18 +5,17 @@
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%-----------------------------------------------------------------------------%
-%
+
% File: build_mode_constraints.m
% Main author: richardf
-%
+
% This module contains predicates and data structures needed for
% traversing the HLDS and building a list of abstract constraint formulae to
% describe variable producers in a Mercury program.
-%
+
%-----------------------------------------------------------------------------%
:- module check_hlds.build_mode_constraints.
-
:- interface.
:- import_module check_hlds.abstract_mode_constraints.
@@ -24,8 +23,6 @@
:- import_module hlds.hlds_goal.
:- import_module hlds.hlds_pred.
:- import_module hlds.hlds_module.
-% :- import_module hlds.inst_graph.
-% % Needed if converting for partial instantiation.
:- import_module parse_tree.prog_data.
:- import_module bimap.
@@ -34,24 +31,35 @@
%-----------------------------------------------------------------------------%
- % XXX Change to include more information? This will just be a
- % list of constraints representing the conjunction of them. When
- % a solver is written, a more elaborate data structure with
- % update functions will no doubt be needed - at that time
- % constraints should be passed as state variables.
- %
% This represents the conjunction of the constraints it
- % contains.
+ % contains (which typically will refer to only one predicate).
%
-:- type mode_constraints == constraint_formulae.
+:- type mode_constraints == pred_p_c_constraints.
+
+ % A store of information about mode constraint variables
+ % associated with constraints based mode analysis of a module
+ % (not just of a single predicate).
+ %
+:- type mc_var_info
+ ---> mc_var_info(
+ mc_varset :: mc_varset,
+ % Produces constraint variables
+ % for producer/consumer constraints.
+
+ rep_var_map :: mc_var_map
+ % Bimap between constraint variables
+ % and the abstract representation
+ % of the proposition they represent.
+ ).
+
% A map between the constraint variables (mc_var) and what they
- % represent ie that some program variable is produced at some
- % goal path (for a particular predicate).
+ % represent ie the proposition that some program variable is
+ % produced at some goal path (for a particular predicate).
%
- % This provides a quick way of looking up the constraint
- % variable we need when we want to constrain the position in
- % which a program variable can be produced.
+ % This provides a quick way of looking up the constraint variable we
+ % need when we want to constrain the position in which a program
+ % variable can be produced.
%
:- type mc_var_map == bimap(mc_rep_var, mc_var).
@@ -63,7 +71,7 @@
%
:- type nonlocals == set(prog_var).
- % In order to uniquely distinguish prog_var that may not be
+ % In order to uniquely distinguish a prog_var that may not be
% unique amongst predicates, this data structure is used to
% specify the predicate to which this prog_var is intended to
% apply.
@@ -72,99 +80,114 @@
% An abstract representation of a mode constraint variable.
%
- % It represents the constraint variable that determines whether
- % the program variable specified is produced at the goal path
- % specified.
+ % ProgVar `in` PredId, `at` GoalPath represents the constraint
+ % variable of the proposition that ProgVar is produced at
+ % goal GoalPath in predicate PredId.
%
:- type mc_rep_var ---> mc_prog_var `at` goal_path.
- % Provides a nice way to display constraint variables - just
- % convert to the relevant mc_rep_var using the mc_var_map and
- % then convert to a string using this. It comes out in format
- % "ProgVarName.GoalPath"
+%-----------------------------------------------------------------------------%
+
+ % rep_var_to_string(ProgVarset, ProgVar `in` PredId `at` GoalPath)
+ %
+ % returns a string representation of the constraint variable with
+ % the abstract representation given, in format "ProgVarName.GoalPath" -
+ % the ProgVarset should have the ProgVarName in it for ProgVar,
+ % and should therefore be taken from predicate PredId.
%
:- func rep_var_to_string(prog_varset, mc_rep_var) = (string).
- % For each head variable of each predicate in the supplied SCC,
- % this predicate adds to the varset the constraint variable for
- % HeadVariable `in` PredId `at` []. In other words, it creates
- % the constraint variables that describe whether or not a head
- % variable is produced by a call to the predicate. At the same
- % time it records in the mc_var_map the position and program
- % variable to which the new constraint variable corresponds.
+ % add_mc_vars_for_scc_heads(ModuleInfo, SCC, !VarInfo)
+ %
+ % For each HeadVariable of each predicate PredId, in the supplied
+ % SCC, this predicate adds to VarInfo the constraint variable for
+ % HeadVariable `in` PredId `at` []. In other words, it creates the
+ % constraint variables that describe whether or not a head variable
+ % is produced by a call to the predicate.
+ %
+ % (We do this all at once because intra-SCC calls refer to the
+ % production of program variables at the head of the callee,
+ % and the caller doesn't neccessarily have access to the
+ % relevant prog_varset to create the necessary constraint
+ % variables.)
%
:- pred add_mc_vars_for_scc_heads(module_info::in, list(pred_id)::in,
- mc_varset::in, mc_varset::out, mc_var_map::in, mc_var_map::out) is det.
+ mc_var_info::in, mc_var_info::out) is det.
- % Makes sure that the necessary constraint variables exist to
- % create goal constraints for all goal types except predicate
- % calls.
- %
- % At this stage, constraint variables are created at a goal for
- % each variable in the nonlocal set of that goal - other
- % variables are either local and must be produced at the current
- % path or do not occur in the goal and so are not produced at
- % the current path.
- %
- % Note that in order to produce constraints for a goal,
- % constraint variables for the head variables of called
- % predicates with no declared modes are needed as well as these
- % goal constraint variables, so before constraints are built for
- % any predicate in an SCC add_mc_vars_for_scc_heads should be
- % called for that whole SCC.
+ % add_mc_vars_for_goal(PredId, ProgVarset, Goal, !VarInfo)
+ %
+ % For each nonlocal of Goal, makes sure a constraint variable exists
+ % in VarInfo representing the proposition that the nonlocal is
+ % produced at that Goal. Other variables are either local and must
+ % be produced at the current path or do not occur in the goal and so
+ % are not produced at the current path (although some such
+ % constraint variables are created later so as to simplify
+ % constraint generation).
+ %
+ % NOTE: this predicate *does* recurse on subgoals.
%
:- pred add_mc_vars_for_goal(pred_id::in, prog_varset::in, hlds_goal::in,
- mc_varset::in, mc_varset::out, mc_var_map::in, mc_var_map::out) is det.
+ mc_var_info::in, mc_var_info::out) is det.
% mode_decls_constraints(ModuleInfo, VarMap, PredId, Decls,
- % HeadVarsList, Constraints)
+ % HeadVarsList, Constraints)
%
% Constraints is the disjunction of the constraints for
% individual declared modes being satisfied. ie
% disj([ConstraintsForMode1, ..., ConstraintsForModen])
%
- % Note that if Decls is an empty list, this is interpreted as
- % there being no modes for which the predicate can be executed
- % and the returned constraints are [disj([])] which cannot be
- % satisfied. Mode declarations for predicates with no declared
- % modes should not be handled by this - they must be handled
- % elsewhere.
- %
% The constraints for a predicate with declared modes is the
% disjunction of the constraints for each declared mode. If,
% according to the mode declaration, a variable is not initially
- % free then it cannot be produced by a call to this predicate;
- % if a variable is initially free and becomes not free then it
- % is produced by the predicate. Otherwise it is free -> free
- % and is not produced.
+ % free then it is constrained so that it cannot be produced by a
+ % call to this predicate; if a variable is initially free and
+ % becomes not free then it is constrained so as to be produced by
+ % the predicate. Otherwise it is free -> free and is constrained
+ % so as to not be produced.
+ %
+ % NOTE: if Decls is an empty list, this is interpreted as
+ % there being no modes for which the predicate can be executed
+ % and the returned constraints are [disj([])] which cannot be
+ % satisfied. Predicates with mode inference requested should
+ % not be handled by this.
%
:- pred mode_decls_constraints(module_info::in, mc_var_map::in,
pred_id::in, list(list(mer_mode))::in, list(args)::in,
+ constraint_formulae::out) is det.
+
+ % add_clauses_constraints(ModuleInfo, PredId, PredInfo, !VarInfo,
+ % !Constraints)
+ %
+ % Adds to Constraints the constraints for the body of predicate
+ % PredId, from the module described in ModuleInfo. (PredInfo should
+ % be the unpacked info for PredId from ModuleInfo, and VarInfo is
+ % included to keep track of mode constraint variables for that
+ % module.)
+ %
+:- pred add_clauses_constraints(module_info::in, pred_id::in, pred_info::in,
+ mc_var_info::in, mc_var_info::out, mode_constraints::in,
mode_constraints::out) is det.
- % In the event that type_info arguments have been added to a
- % predicate call's arguments/headvars, but the modes have not
- % been edited to reflect this, extra in modes need to be added
- % to the front of the mode declaration to account for this.
- %
- % XXX This predicate shouldn't be needed, but if you're getting
- % map_corresponding errors for the use of lists of different
- % lengths it would be worthwhile modifying any calls to
- % mode_decl predicates with this so that the headvars list and
- % mode declarations are the same length.
- % Unfortunately this predicate relies the type_info arguments
- % being added to the front of the arg list, and assumes that
- % they are all specifically of mode in as given by function
- % prog_tree.prog_mode.in_mode
-:- pred add_sufficient_in_modes_for_type_info_args(args::in,
- list(mer_mode)::in, list(mer_mode)::out) is det.
+ % add_mode_decl_constraints(ModuleInfo, PredId, ProcId,
+ % Decl, Args, !VarInfo, !Constraints)
+ %
+ % Constrains (in the Constraints) the production of Args at the head
+ % of predicate PredId when called in mode ProcId with declaration
+ % Decl. If, according to the mode declaration, a variable is not
+ % initially free then it is constrained so that it cannot be
+ % produced by a call to this predicate; if a variable is initially
+ % free and becomes not free then it is constrained so as to be
+ % produced by the predicate. Otherwise it is free -> free and is
+ % constrained so as to not be produced.
+ %
+:- pred add_mode_decl_constraints(module_info::in, pred_id::in, proc_id::in,
+ list(mer_mode)::in, args::in, mc_var_info::in, mc_var_info::out,
+ mode_constraints::in, mode_constraints::out) is det.
- % goal_expr_constraints generates the constraints that apply to
- % a given goal_expr at a given goal path.
+ % Creates a new mc_var_info structure (with no mode constraint
+ % variables stored in it).
%
-:- pred goal_expr_constraints( module_info::in, mc_var_map::in,
- pred_id::in, hlds_goal_expr::in, goal_path::in, nonlocals::in,
- mode_constraints::out) is det.
+:- func var_info_init = mc_var_info.
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
@@ -195,67 +218,86 @@
%-----------------------------------------------------------------------------%
-add_mc_vars_for_scc_heads(_ModuleInfo, [], !Varset, !VarMap).
-add_mc_vars_for_scc_heads(ModuleInfo, [PredId | PredIds], !Varset, !VarMap) :-
+:- type conj_constraints_info
+ ---> conj_constraints_info(
+ locals_positions :: conjunct_production_map,
+ % Keys are program variables local to the
+ % conjunction. They are mapped to constraint
+ % variables representing the proposition that they
+ % are produced at each conjunct, but only for
+ % conjuncts they appear in/are nonlocal to.
+
+ nonlocals_positions :: conjunct_production_map
+ % Keys are program variables nonlocal to the
+ % conjunction. They are mapped to constraint
+ % variables representing the proposition that they
+ % are produced at each conjunct, but only for
+ % conjuncts they appear in/are nonlocal to.
+ ).
+
+ % Map from program variables to corresponding constraint variables.
+ % The constraint variables should represent a set of propositions
+ % that the program variable they are mapped from is produced at
+ % some conjunct in a single conjunction.
+ %
+ % ie if multi_map.member(ConjunctProductionMap, ProgVar, MCVar)
+ % then MCVar should represent the proposition that ProgVar is
+ % produced at some specific conjunct, and all such `MCVar's should
+ % refer to the same conjuction.
+ %
+:- type conjunct_production_map == multi_map(prog_var, mc_var).
+
+%-----------------------------------------------------------------------------%
+
+add_mc_vars_for_scc_heads(ModuleInfo, PredIds, !VarInfo) :-
+ list.foldl(add_mc_vars_for_pred_head(ModuleInfo), PredIds, !VarInfo).
+
+ % add_mc_vars_for_pred_head(ModuleInfo, PredId, !VarInfo)
+ %
+ % For each HeadVariable of predicate PredId this predicate adds to
+ % VarInfo the constraint variable for HeadVariable `in` PredId `at`
+ % []. In other words, it creates the constraint variables that
+ % describe whether or not a head variable is produced by a call to
+ % the predicate.
+ %
+:- pred add_mc_vars_for_pred_head(module_info::in, pred_id::in,
+ mc_var_info::in, mc_var_info::out) is det.
+
+add_mc_vars_for_pred_head(ModuleInfo, PredId, !VarInfo) :-
module_info_pred_info(ModuleInfo, PredId, PredInfo),
pred_info_clauses_info(PredInfo, ClausesInfo),
clauses_info_headvars(ClausesInfo, Headvars),
clauses_info_varset(ClausesInfo, ProgVarset),
- list.foldl2(add_mc_var_for_pred_head(PredId, ProgVarset), Headvars,
- !Varset, !VarMap),
- add_mc_vars_for_scc_heads(ModuleInfo, PredIds, !Varset, !VarMap).
- % XXX This potentially needs to be performed for the
- % headvars in the proc_infos associated with a predicate
- % as well, since the mode declaration constraints refer
- % to them, however at this point in time they should be
- % the same as the headvars in the clauses_info
-
- % Makes sure a constraint variable exists to say that the
- % supplied program variable is produced by the predicate in
- % which it exists.
- %
- % Just checks that the constraint variable in question doesn't
- % already exist, and then gets a new one from the varset and
- % adds it to the varmap if it doesn't.
- %
-:- pred add_mc_var_for_pred_head(pred_id::in, prog_varset::in, prog_var::in,
- mc_varset::in, mc_varset::out, mc_var_map::in, mc_var_map::out) is det.
-
-add_mc_var_for_pred_head(PredId, ProgVarset, HeadVar, !Varset, !VarMap) :-
- RepVar = (HeadVar `in` PredId) `at` [],
- ( bimap.search(!.VarMap, RepVar, _MCVar) ->
- true
- ;
- svvarset.new_named_var(rep_var_to_string(ProgVarset, RepVar),
- NewMCvar, !Varset),
- svbimap.det_insert(RepVar, NewMCvar, !VarMap)
- ).
+ list.foldl(add_mc_var_for_pred_head(ProgVarset, PredId), Headvars,
+ !VarInfo).
-add_mc_vars_for_goal(PredId, ProgVarset, GoalExpr - GoalInfo,
- !Varset, !VarMap) :-
+
+ % add_mc_var_for_pred_head(ProgVarset, PredId, ProgVar, !VarInfo)
+ %
+ % For ProgVar, a head variable of predicate PredId, this predicate
+ % adds to VarInfo the constraint variable for ProgVar `in` PredId
+ % `at` []. In other words, it creates the constraint variable that
+ % describes whether or not ProgVar is produced by a call to the
+ % predicate. ProgVarset should contain ProgVar, and a string name
+ % for it.
+ %
+:- pred add_mc_var_for_pred_head(prog_varset::in, pred_id::in, prog_var::in,
+ mc_var_info::in, mc_var_info::out) is det.
+
+add_mc_var_for_pred_head(ProgVarset, PredId, HeadVar, !VarInfo) :-
+ prog_var_at_path(ProgVarset, PredId, HeadVar, [], _, !VarInfo).
+
+add_mc_vars_for_goal(PredId, ProgVarset, GoalExpr - GoalInfo, !VarInfo) :-
goal_info_get_nonlocals(GoalInfo, Nonlocals),
goal_info_get_goal_path(GoalInfo, GoalPath),
- {!:Varset, !:VarMap} = set.fold(
- (func(Nonlocal, {Vset0, Vmap0}) = {Vset, Vmap} :-
- RepVar = (Nonlocal `in` PredId) `at` GoalPath,
- ( bimap.search(Vmap0, RepVar, _) ->
- Vset = Vset0,
- Vmap = Vmap0
- ;
- varset.new_named_var(Vset0,
- rep_var_to_string(ProgVarset, RepVar), NewMCvar, Vset),
- bimap.det_insert(Vmap0, RepVar, NewMCvar, Vmap)
- )
- ),
- Nonlocals,
- {!.Varset, !.VarMap}
- ),
+ set.to_sorted_list(Nonlocals, NlsList),
+ prog_vars_at_path(ProgVarset, PredId, NlsList, GoalPath, _, !VarInfo),
+
% Switch on GoalExpr for recursion
(
GoalExpr = conj(Goals),
- list.foldl2(add_mc_vars_for_goal(PredId, ProgVarset), Goals,
- !Varset, !VarMap)
+ list.foldl(add_mc_vars_for_goal(PredId, ProgVarset), Goals, !VarInfo)
;
GoalExpr = call(_, _, _, _, _, _)
;
@@ -263,24 +305,21 @@
;
GoalExpr = switch(_, _, Cases),
Goals = list.map(func(case(_, Goal)) = Goal, Cases),
- list.foldl2(add_mc_vars_for_goal(PredId, ProgVarset), Goals,
- !Varset, !VarMap)
+ list.foldl(add_mc_vars_for_goal(PredId, ProgVarset), Goals, !VarInfo)
;
GoalExpr = unify(_, _, _, _, _)
;
GoalExpr = disj(Goals),
- list.foldl2(add_mc_vars_for_goal(PredId, ProgVarset), Goals,
- !Varset, !VarMap)
+ list.foldl(add_mc_vars_for_goal(PredId, ProgVarset), Goals, !VarInfo)
;
GoalExpr = not(Goal),
- add_mc_vars_for_goal(PredId, ProgVarset, Goal, !Varset, !VarMap)
+ add_mc_vars_for_goal(PredId, ProgVarset, Goal, !VarInfo)
; GoalExpr = scope(_, Goal),
- add_mc_vars_for_goal(PredId, ProgVarset, Goal, !Varset, !VarMap)
+ add_mc_vars_for_goal(PredId, ProgVarset, Goal, !VarInfo)
;
GoalExpr = if_then_else(_, Cond, Then, Else),
Goals = [Cond, Then, Else],
- list.foldl2(add_mc_vars_for_goal(PredId, ProgVarset), Goals,
- !Varset, !VarMap)
+ list.foldl(add_mc_vars_for_goal(PredId, ProgVarset), Goals, !VarInfo)
;
GoalExpr = foreign_proc(_, _, _, _, _, _)
;
@@ -300,335 +339,451 @@
%-----------------------------------------------------------------------------%
- % Goal_constraints gives the mode constraints for the supplied hlds_goal.
+add_clauses_constraints(ModuleInfo, PredId, PredInfo, !VarInfo,
+ !Constraints) :-
+ pred_info_clauses_info(PredInfo, ClausesInfo),
+ clauses_info_headvars(ClausesInfo, HeadVars),
+ clauses_info_clauses_only(ClausesInfo, Clauses),
+ clauses_info_varset(ClausesInfo, ProgVarset),
+
+ (
+ % If the clause list is empty, then there are no
+ % goals to produce constraints for.
+ Clauses = []
+ ;
+ Clauses = [FirstClause|_],
+
+ % Use the first clause for the context of the top level
+ % goal constraints.
+ Context = clause_context(FirstClause),
+
+ % All clauses are considered for all procedures.
+ % though some may not be applicable, overall the
+ % waste should not be large.
+ Goals = list.map((func(clause(_, Body, _, _)) = Body), Clauses),
+
+ list.foldl(add_mc_vars_for_goal(PredId, ProgVarset),
+ Goals, !VarInfo),
+
+ % Temporarily form the disjunction implied by the goal path
+ % annotations.
+ MainGoal = disj(Goals),
+ HeadGoalPath = [],
+ Nonlocals = set.list_to_set(HeadVars),
+ add_goal_expr_constraints(ModuleInfo, ProgVarset, PredId, MainGoal,
+ Context, HeadGoalPath, Nonlocals, !VarInfo, !Constraints)
+ ).
+
+%-----------------------------------------------------------------------------%
+
+ % add_goal_constraints(ModuleInfo, ProgVarset, PredId, Goal,
+ % !VarInfo, !Constraints)
+ %
+ % Adds goal constraints to Constraints to describe the producing and
+ % consuming goals for program variables nonlocal to Goal in
+ % predicate PredId of the module described in ModuleInfo.
+ % VarInfo is used to keep track of the meaning of any constraint
+ % variables used.
%
-:- pred goal_constraints(module_info::in, mc_var_map::in, pred_id::in,
- hlds_goal::in, mode_constraints::out) is det.
+:- pred add_goal_constraints(module_info::in, prog_varset::in, pred_id::in,
+ hlds_goal::in, mc_var_info::in, mc_var_info::out, mode_constraints::in,
+ mode_constraints::out) is det.
-goal_constraints(ModuleInfo, VarMap, PredId, GoalExpr - GoalInfo,
- Constraints) :-
+add_goal_constraints(ModuleInfo, ProgVarset, PredId, GoalExpr - GoalInfo,
+ !VarInfo, !Constraints) :-
goal_info_get_nonlocals(GoalInfo, Nonlocals),
goal_info_get_goal_path(GoalInfo, GoalPath),
- goal_expr_constraints(ModuleInfo, VarMap, PredId, GoalExpr, GoalPath,
- Nonlocals, Constraints).
-
-goal_expr_constraints(ModuleInfo, VarMap, PredId,
- conj(Goals), GoalPath, Nonlocals, Constraints) :-
- list.map(
- goal_constraints(ModuleInfo, VarMap, PredId),
- Goals, ConjunctConstraints
- ),
- Constraints0 = list.condense(ConjunctConstraints),
- list.foldl(
- fold_local_var_into_conj_constraints(VarMap, LocalsPositions),
- multi_map.keys(LocalsPositions),
- Constraints0, Constraints1
- ),
- list.foldl(
- fold_nonlocal_var_into_conj_constraints(VarMap, PredId,
- NonlocalsPositions, GoalPath),
- multi_map.keys(NonlocalsPositions),
- % Nonlocal variables that are nonlocals to subgoals.
- Constraints1, Constraints
- ),
-
- EmptyMultiMap = multi_map.init,
- list.foldl2(fold_goal_into_var_position_maps(VarMap, PredId, Nonlocals),
- Goals, EmptyMultiMap, LocalsPositions,
- % A map from each local variable to
- % its corresponding constraint
- % variables for the paths at each of
- % the conjuncts it is non-local to,
- % if such conjuncts exist. (If a
- % variable is local to one conjunct we
- % need not deal with it here).
- EmptyMultiMap, NonlocalsPositions
- % A map from each non-local variable
- % to its corresponding constraint
- % variables at the paths of each of the
- % conjuncts it is non-local to. Note
- % that all non-local variables should
- % appear in this map, since if a
- % variable is in the non-local set of a
- % conjunction it ought to be in the
- % non-local set of at least one of the
- % conjuncts.
- ).
-
-goal_expr_constraints(ModuleInfo, VarMap, PredId,
- call(CalledPred, _ProcID, Args, _Builtin, _UnifyContext, _Name),
- GoalPath, _Nonlocals, Constraints) :-
- module_info_pred_info(ModuleInfo, CalledPred, PredInfo),
- pred_info_procedures(PredInfo, ProcTable),
- map.values(ProcTable, ProcInfos),
- list.filter_map(
- (pred(PInfo::in, MDecl::out) is semidet :-
- proc_info_maybe_declared_argmodes(PInfo, yes(_)),
- proc_info_argmodes(PInfo, MDecl)
- ),
- ProcInfos,
- ArgModeDecls
- ),
- (
- % No modes declared, must be in the same SCC as
- % the calling predicate.
- ArgModeDecls = [],
-
- % Get the head variables of the called pred.
- pred_info_clauses_info(PredInfo, ClausesInfo),
- clauses_info_headvars(ClausesInfo, HeadVars),
-
- call_headvar_constraints( VarMap, GoalPath, PredId, Args, CalledPred,
- HeadVars, Constraints)
- ;
- % At least one declared mode
- ArgModeDecls = [_| _],
-
-% list.map(
-% add_sufficient_in_modes_for_type_info_args(Args),
-% ArgModeDecls,
-% FullArgModeDecls
-% ), % XXX type_info args should be at the start and
-% % should be 'in' so that is what this predicate
-% % adds however, I am not happy with it.
+ goal_info_get_context(GoalInfo, Context),
+ add_goal_expr_constraints(ModuleInfo, ProgVarset, PredId,
GoalExpr, Context,
+ GoalPath, Nonlocals, !VarInfo, !Constraints).
+
+ % add_goal_expr_constraints(ModuleInfo, ProgVarset, PredId, GoalExpr,
+ % Context, GoalPath, Nonlocals, !VarInfo, !Constraints)
+ %
+ % Adds goal constraints to Constraints to describe the producing and
+ % consuming goals for Nonlocals, with respect to GoalExpr and its
+ % subgoals.
+ % Context and GoalPath refer to the position of GoalExpr, in the
+ % source file for the module described in ModuleInfo, and in the
+ % body of predicate PredId respectively.
+ % VarInfo is used to keep track of the meaning of any constraint
+ % variables used. ProgVarset should contain string names for
+ % all of the variables in Nonlocals.
+ %
+:- pred add_goal_expr_constraints(module_info::in, prog_varset::in,
+ pred_id::in, hlds_goal_expr::in, prog_context::in, goal_path::in,
+ nonlocals::in, mc_var_info::in, mc_var_info::out, mode_constraints::in,
+ mode_constraints::out) is det.
- call_mode_decls_constraints(ModuleInfo, VarMap, PredId, ArgModeDecls,
- GoalPath, Args, Constraints)
+add_goal_expr_constraints(ModuleInfo, ProgVarset, PredId,
+ conj(Goals), Context, GoalPath, Nonlocals, !VarInfo, !Constraints) :-
+ list.foldl(add_goal_nonlocals_to_conjunct_production_maps(VarMap, PredId,
+ Nonlocals), Goals, conj_constraints_info_init, ConjConstraintsInfo),
+ VarMap = rep_var_map(!.VarInfo),
+
+ list.foldl2(add_goal_constraints(ModuleInfo, ProgVarset, PredId),
+ Goals, !VarInfo, !Constraints),
+ map.foldl(add_local_var_conj_constraints(Context),
+ locals_positions(ConjConstraintsInfo), !Constraints),
+ map.foldl2(add_nonlocal_var_conj_constraints(ProgVarset, PredId,
+ Context, GoalPath), nonlocals_positions(ConjConstraintsInfo),
+ !VarInfo, !Constraints).
+
+
+add_goal_expr_constraints(ModuleInfo, ProgVarset, CallerPredId, GoalExpr,
+ Context, GoalPath, _Nonlocals, !VarInfo, !Constraints) :-
+ GoalExpr = call(CalleePredId, _, Args, _, _, _),
+ module_info_pred_info(ModuleInfo, CalleePredId, CalleePredInfo),
+
+ ( pred_info_infer_modes(CalleePredInfo) ->
+ % No modes declared so just constrain the hearvars
+ pred_info_clauses_info(CalleePredInfo, CalleeClausesInfo),
+ clauses_info_headvars(CalleeClausesInfo, CalleeHeadVars),
+ add_call_headvar_constraints(ProgVarset, Context, GoalPath,
+ CallerPredId, Args, CalleePredId, CalleeHeadVars,
+ !VarInfo, !Constraints)
+ ;
+ % At least one declared mode
+ pred_info_procedures(CalleePredInfo, CalleeProcTable),
+ map.values(CalleeProcTable, CalleeProcInfos),
+ list.map(proc_info_argmodes, CalleeProcInfos, CalleeArgModeDecls),
+ add_call_mode_decls_constraints(ModuleInfo, ProgVarset, Context,
+ CallerPredId, CalleeArgModeDecls, GoalPath, Args, !VarInfo,
+ !Constraints)
).
-goal_expr_constraints(_ModuleInfo, _VarMap, _PredId,
- generic_call(_, _, _, _), _GoalPath, _Nonlocals, _Constraints) :-
- % XXX Need to do something here.
- sorry(this_file, "generic_call NYI.").
-
-goal_expr_constraints(_ModuleInfo, _VarMap, _PredId,
- switch(_, _, _), _GoalPath, _Nonlocals, _Constraints) :-
+add_goal_expr_constraints(_ModuleInfo, _ProgVarset, _PredId,
+ generic_call(Details, _, _, _), _Context, _GoalPath,
+ _Nonlocals, !VarInfo, !Constraints) :-
% XXX Need to do something here.
- sorry(this_file, "switch NYI.").
+ (
+ % XXX Need to do something here.
+ Details = higher_order(_, _, _, _),
+ sorry(this_file, "higher_order generic_call")
+ ;
+ % XXX Need to do something here.
+ Details = class_method(_, _, _, _),
+ sorry(this_file, "class_method generic_call")
+ ;
+ % No mode constraints
+ Details = cast(_)
+ ;
+ % XXX Need to do something here.
+ Details = aditi_builtin(_, _),
+ sorry(this_file, "class_method generic_call")
+ ).
-goal_expr_constraints(_ModuleInfo, VarMap, PredId,
- unify(LHSvar, RHS, _Mode, _Kind, _Context),
- GoalPath, _Nonlocals, Constraints) :-
+add_goal_expr_constraints(_ModuleInfo, _ProgVarset, _PredId,
+ switch(_, _, _), _Context, _GoalPath, _Nonlocals, _, _, _, _) :-
+ unexpected(this_file, "switch").
+
+add_goal_expr_constraints(_ModuleInfo, ProgVarset, PredId,
+ unify(LHSvar, RHS, _Mode, _Kind, _UnifyContext),
+ GoalContext, GoalPath, _Nonlocals, !VarInfo, !Constraints) :-
+ prog_var_at_path(ProgVarset, PredId, LHSvar, GoalPath,
+ LHSvarProducedHere, !VarInfo),
(
RHS = var(RHSvar),
% Goal: LHSvar = RHSvar
% At most one of the left and right hand sides of a unification
% is produced at the unification.
- Constraints = [
- atomic_constraint(at_most_one([
- prog_var_at_path(VarMap, PredId, GoalPath, LHSvar),
- prog_var_at_path(VarMap, PredId, GoalPath, RHSvar)
- ]))
- ]
+ prog_var_at_path(ProgVarset, PredId, RHSvar, GoalPath,
+ RHSvarProducedHere, !VarInfo),
+ not_both(GoalContext, LHSvarProducedHere, RHSvarProducedHere,
+ !Constraints)
;
RHS = functor(_Functor, _IsExistConstr, Args),
- LHSproducedHere = prog_var_at_path(
- VarMap, PredId, GoalPath, LHSvar
- ),
- ArgsProducedHere =
- list.map(prog_var_at_path(VarMap, PredId, GoalPath), Args),
+ prog_vars_at_path(ProgVarset, PredId, Args, GoalPath,
+ ArgsProducedHere, !VarInfo),
(
ArgsProducedHere = [OneArgProducedHere, _Two| _],
% Goal: LHSvar = functor(Args)
% (a): If one arg is produced here, then they all are.
% (b): At most one side of the unification is produced.
- Constraints = [
- atomic_constraint(equivalent(ArgsProducedHere)),
- atomic_constraint(
- at_most_one([LHSproducedHere, OneArgProducedHere]))
- ]
+ equivalent(GoalContext, ArgsProducedHere, !Constraints),
+ not_both(GoalContext, LHSvarProducedHere, OneArgProducedHere,
+ !Constraints)
;
ArgsProducedHere = [OneArgProducedHere],
% Goal: LHSvar = functor(Arg)
% At most one side of the unification is produced.
- Constraints = [
- atomic_constraint(
- at_most_one([LHSproducedHere, OneArgProducedHere]))
- ]
+ not_both(GoalContext, LHSvarProducedHere, OneArgProducedHere,
+ !Constraints)
;
- ArgsProducedHere = [],
+ ArgsProducedHere = []
% Goal: LHSvar = functor
% In this case, LHSvar need not be produced
% - it could be a test, so no constraints.
- Constraints = []
)
;
RHS = lambda_goal(_, _, _, _, _, _, _, _, _),
- sorry(this_file, "unify with lambda goal NYI")
+ sorry(this_file, "unify with lambda goal")
).
-goal_expr_constraints(ModuleInfo, VarMap, PredId,
- disj(Goals), GoalPath, Nonlocals, Constraints) :-
-
- nonlocals_at_path_and_subpaths(
- VarMap, PredId, GoalPath, DisjunctGoalPaths,
- Nonlocals, NonlocalsHere, NonlocalsAtDisjuncts
- ),
- list.map(
- pred(_GExpr - GInfo::in, GPath::out) is det :-
- goal_info_get_goal_path(GInfo, GPath),
- Goals,
- DisjunctGoalPaths
- ),
-
- list.map(goal_constraints(ModuleInfo, VarMap, PredId),
- Goals, DisjunctConstraints),
-
- Constraints = list.condense([
- list.map_corresponding(
- func(X, Ys) = atomic_constraint(equivalent([X | Ys])),
- % A variable bound at any disjunct is bound for the disjunct
- % as a whole. If a variable can be bound at one conjunct
- % it must be able to be bound at any.
- NonlocalsHere, NonlocalsAtDisjuncts
- ) |
- DisjunctConstraints
- ]).
+add_goal_expr_constraints(ModuleInfo, ProgVarset, PredId,
+ disj(Goals), Context, GoalPath, Nonlocals, !VarInfo, !Constraints) :-
+ nonlocals_at_path_and_subpaths(ProgVarset, PredId, GoalPath,
+ DisjunctGoalPaths, Nonlocals, NonlocalsHere, NonlocalsAtDisjuncts,
+ !VarInfo),
+
+ list.map(snd, Goals, GoalInfos),
+ list.map(goal_info_get_goal_path, GoalInfos, DisjunctGoalPaths),
+
+ list.foldl2(add_goal_constraints(ModuleInfo, ProgVarset, PredId),
+ Goals, !VarInfo, !Constraints),
+
+ % A variable bound at any disjunct is bound for the disjunction
+ % as a whole. If a variable can be bound at one disjunct
+ % it must be able to be bound at any.
+ EquivVarss = list.map_corresponding(list.cons, NonlocalsHere,
+ NonlocalsAtDisjuncts),
+ list.foldl(equivalent(Context), EquivVarss, !Constraints).
-goal_expr_constraints(ModuleInfo, VarMap, PredId,
- not(Goal), GoalPath, Nonlocals, Constraints) :-
+add_goal_expr_constraints(ModuleInfo, ProgVarset, PredId,
+ not(Goal), Context, GoalPath, Nonlocals, !VarInfo, !Constraints) :-
Goal = _ - NegatedGoalInfo,
goal_info_get_goal_path(NegatedGoalInfo, NegatedGoalPath),
- NonlocalsConstraintVars = set.fold(
- func(Nonlocal, MCVars) = [
- prog_var_at_path(VarMap, PredId, GoalPath, Nonlocal),
- prog_var_at_path(VarMap, PredId, NegatedGoalPath, Nonlocal)
- |
- MCVars
- ],
- Nonlocals,
- []
- ),
- goal_constraints(
- ModuleInfo, VarMap, PredId, Goal, NegatedGoalConstraints
- ),
- Constraints = list.foldl(
- func(MCVar, Cnstrnts) = [
- atomic_constraint(equiv_bool(MCVar, no))|
- % The variables non-local to the negation are not to be
- % produced at the negation or any deeper.
- Cnstrnts
- ],
- NonlocalsConstraintVars,
- NegatedGoalConstraints
- ).
-
-goal_expr_constraints(ModuleInfo, VarMap, PredId,
- scope(_Reason, Goal),
- GoalPath, Nonlocals, Constraints) :-
+ VarMap = rep_var_map(!.VarInfo),
+ NonlocalsAtPath = set.fold(cons_prog_var_at_path(VarMap, PredId, GoalPath),
+ Nonlocals, []),
+ NonlocalsConstraintVars = set.fold(cons_prog_var_at_path(VarMap, PredId,
+ NegatedGoalPath), Nonlocals, NonlocalsAtPath),
+
+ add_goal_constraints(ModuleInfo, ProgVarset, PredId, Goal, !VarInfo,
+ !Constraints),
+
+ % The variables non-local to the negation are not to be
+ % produced at the negation or any deeper, so we constrain
+ % their mode constraint variables for these positions to `no'.
+ list.foldl(equiv_no(Context), NonlocalsConstraintVars, !Constraints).
+
+add_goal_expr_constraints(ModuleInfo, ProgVarset, PredId,
+ scope(_Reason, Goal), Context, GoalPath, Nonlocals, !VarInfo,
+ !Constraints) :-
Goal = _ - SomeGoalInfo,
goal_info_get_goal_path(SomeGoalInfo, SomeGoalPath),
- Constraints = set.fold(
- func(NL, NLConstraints) = [
- % If a program variable is produced by the sub-goal of the some
- % statement, it is produced at the main goal as well.
- atomic_constraint(equivalent([
- prog_var_at_path(VarMap, PredId, GoalPath, NL),
- prog_var_at_path(VarMap, PredId, SomeGoalPath, NL)
- ])) | NLConstraints],
- Nonlocals, SomeGoalConstraints),
- goal_constraints(ModuleInfo, VarMap, PredId, Goal, SomeGoalConstraints).
-
-goal_expr_constraints(ModuleInfo, VarMap, PredId,
- if_then_else(ExistVars, If, Then, Else),
- GoalPath, Nonlocals, Constraints) :-
+
+ % If a program variable is produced by the sub-goal of the some
+ % statement, it is produced at the main goal as well
+ % - here we pair up equivalent mode constraint vars and
+ % then constrain them to reflect this.
+ NonlocalsList = set.to_sorted_list(Nonlocals),
+ prog_vars_at_path(ProgVarset, PredId, NonlocalsList, GoalPath,
+ NonlocalsHere, !VarInfo),
+ prog_vars_at_path(ProgVarset, PredId, NonlocalsList, SomeGoalPath,
+ NonlocalsAtSubGoal, !VarInfo),
+ EquivVarss = list.map_corresponding(
+ func(NlAtPath, NlAtSubPath) = [NlAtPath, NlAtSubPath],
+ NonlocalsHere, NonlocalsAtSubGoal),
+ list.foldl(equivalent(Context), EquivVarss, !Constraints),
+
+ add_goal_constraints(ModuleInfo, ProgVarset, PredId, Goal, !VarInfo,
+ !Constraints).
+
+add_goal_expr_constraints(ModuleInfo, ProgVarset, PredId,
+ if_then_else(ExistVars, If, Then, Else),
+ Context, GoalPath, Nonlocals, !VarInfo, !Constraints) :-
If = _ - IfInfo, Then = _ - ThenInfo, Else = _ - ElseInfo,
goal_info_get_goal_path(IfInfo, CondPath),
goal_info_get_goal_path(ThenInfo, ThenPath),
goal_info_get_goal_path(ElseInfo, ElsePath),
- NonlocalsHere = list.map(prog_var_at_path(VarMap, PredId, GoalPath),
- NonlocalsList),
- NonlocalsAtCond = list.map(prog_var_at_path(VarMap, PredId, CondPath),
- NonlocalsList),
- NonlocalsAtThen = list.map(prog_var_at_path(VarMap, PredId, ThenPath),
- NonlocalsList),
- NonlocalsAtElse = list.map(prog_var_at_path(VarMap, PredId, ElsePath),
- NonlocalsList),
+ prog_vars_at_path(ProgVarset, PredId, NonlocalsList, GoalPath,
+ NonlocalsHere, !VarInfo),
+ prog_vars_at_path(ProgVarset, PredId, NonlocalsList, CondPath,
+ NonlocalsAtCond, !VarInfo),
+ prog_vars_at_path(ProgVarset, PredId, NonlocalsList, ThenPath,
+ NonlocalsAtThen, !VarInfo),
+ prog_vars_at_path(ProgVarset, PredId, NonlocalsList, ElsePath,
+ NonlocalsAtElse, !VarInfo),
NonlocalsList = set.to_sorted_list(Nonlocals),
+ %
% The existentially quantified variables shared between the condition
% and the then-part have special constraints.
- LocalAndSharedAtCond = list.map(prog_var_at_path(VarMap, PredId, CondPath),
- ExistVars),
- LocalAndSharedAtThen = list.map(prog_var_at_path(VarMap, PredId, ThenPath),
- ExistVars),
-
- goal_constraints(ModuleInfo, VarMap, PredId, If, IfConstraints),
- goal_constraints(ModuleInfo, VarMap, PredId, Then, ThenConstraints),
- goal_constraints(ModuleInfo, VarMap, PredId, Else, ElseConstraints),
-
- Constraints = list.condense([
- list.map_corresponding3(
- func(NLHere, NLAtThen, NLAtElse) =
- % If a variable is to be produced at this path,
- % the then and else parts must be able to produce it.
- atomic_constraint(equivalent([NLHere, NLAtThen, NLAtElse])),
- NonlocalsHere, NonlocalsAtThen, NonlocalsAtElse),
- % No nonlocal is produced in the condition.
- list.map(func(Cond) = atomic_constraint(equiv_bool(Cond, no)),
- NonlocalsAtCond),
- % XXX Do we want this, or do we just constrain 'Cond true and 'Then
- % false? Maybe a local variable shared between the condition and
- % then-part should always be bound in the condition, but I'm not sure
- % about the possibility of checking the variable's type in the Cond
- % and then binding it in the Then...
- list.map_corresponding(
- (func(LocalAtCond, LocalAtThen) =
- atomic_constraint(exactly_one([LocalAtCond, LocalAtThen]))),
- LocalAndSharedAtCond, LocalAndSharedAtThen),
- IfConstraints, ThenConstraints, ElseConstraints]).
-
-goal_expr_constraints(ModuleInfo, VarMap, PredId,
- foreign_proc(_, CalledPred, ProcID, ForeignArgs, _, _),
- GoalPath, _Nonlocals, Constraints) :-
+ %
+ goal_info_get_nonlocals(IfInfo, IfNonlocals),
+ goal_info_get_nonlocals(ThenInfo, ThenNonlocals),
+ list.filter(set.contains(IfNonlocals), ExistVars, NonlocalToIf),
+ list.filter(set.contains(ThenNonlocals), NonlocalToIf, LocalAndShared),
+ prog_vars_at_path(ProgVarset, PredId, LocalAndShared, CondPath,
+ LocalAndSharedAtCond, !VarInfo),
+ prog_vars_at_path(ProgVarset, PredId, LocalAndShared, ThenPath,
+ LocalAndSharedAtThen, !VarInfo),
+
+ add_goal_constraints(ModuleInfo, ProgVarset, PredId, If, !VarInfo,
+ !Constraints),
+ add_goal_constraints(ModuleInfo, ProgVarset, PredId, Then, !VarInfo,
+ !Constraints),
+ add_goal_constraints(ModuleInfo, ProgVarset, PredId, Else, !VarInfo,
+ !Constraints),
+
+ % If a variable is to be produced at this path,
+ % the then and else parts must be able to produce it.
+ % Here we group constraint variables into lists to be
+ % constrained equivalent to reflect this.
+ EquivVarss = list.map_corresponding3(func(A, B, C) = [A, B, C],
+ NonlocalsHere, NonlocalsAtThen, NonlocalsAtElse),
+ list.foldl(equivalent(Context), EquivVarss, !Constraints),
+
+ % No nonlocal is produced in the condition.
+ list.foldl(equiv_no(Context), NonlocalsAtCond, !Constraints),
+
+ % In case the program variable appears in the nonlocal set
+ % of the condition, but its value is not used, we do not
+ % simply constrain LocalAtCond = yes and LocalAtThen = no.
+ % Instead we constrain exactly one of them to be yes.
+ list.foldl_corresponding(xor(Context), LocalAndSharedAtCond,
+ LocalAndSharedAtThen, !Constraints).
+
+add_goal_expr_constraints(ModuleInfo, ProgVarset, PredId,
+ foreign_proc(_, CalledPred, ProcId, ForeignArgs, _, _),
+ Context, GoalPath, _Nonlocals, !VarInfo, !Constraints) :-
CallArgs = list.map(foreign_arg_var, ForeignArgs),
- module_info_pred_proc_info(ModuleInfo, CalledPred, ProcID, _, ProcInfo),
+ module_info_pred_proc_info(ModuleInfo, CalledPred, ProcId, _, ProcInfo),
( proc_info_maybe_declared_argmodes(ProcInfo, yes(_OrigDecl)) ->
proc_info_argmodes(ProcInfo, Decl),
-% add_sufficient_in_modes_for_type_info_args(
-% CallArgs,
-% Decl,
-% FullDecl
-% ), % XXX type_info args should be at the start and
-% % should be 'in' so that is what this predicate
-% % adds however, I am not happy with it.
% This pred should strip the disj(conj()) for the single declaration.
- call_mode_decls_constraints(ModuleInfo, VarMap, PredId, [Decl],
- GoalPath, CallArgs, Constraints)
+ add_call_mode_decls_constraints(ModuleInfo, ProgVarset, Context,
+ PredId, [Decl], GoalPath, CallArgs, !VarInfo, !Constraints)
;
unexpected(this_file, "no mode declaration for foreign proc")
).
-goal_expr_constraints(_ModuleInfo, _VarMap, _PredId,
- par_conj(_Goals), _GoalPath, _Nonlocals, _Constraints) :-
- % XXX What to do here?
- sorry(this_file, "NYI par_conj").
-
-goal_expr_constraints(_ModuleInfo, _VarMap, _PredId,
- shorthand(_ShorthandGoalExpr), _GoalPath, _Nonlocals, _Constraints) :-
- % Shorthand goals not exist at this point in compilation.
+add_goal_expr_constraints(_ModuleInfo, _ProgVarset, _PredId,
+ par_conj(_Goals), _Context, _GoalPath, _Nonlocals, _, _, _, _) :-
+ % XXX Need to do something here.
+ sorry(this_file, "par_conj").
+
+add_goal_expr_constraints(_ModuleInfo, _ProgVarset, _PredId,
+ shorthand(_ShorthandGoalExpr), _Context, _GoalPath, _Nonlocals,
+ _, _, _, _) :-
+ % Shorthand goals should not exist at this point in compilation.
unexpected(this_file, "shorthand goal").
+add_mode_decl_constraints(ModuleInfo, PredId, ProcId, Decl, Args,
+ !VarInfo, !Constraints) :-
+ module_info_proc_info(ModuleInfo, PredId, ProcId, ProcInfo),
+ proc_info_varset(ProcInfo, ProgVarset),
+ proc_info_context(ProcInfo, Context),
+
+ prog_vars_at_path(ProgVarset, PredId, Args, [], ArgsAtHead, !VarInfo),
+
+ DeclConstraints = mode_decl_constraints(ModuleInfo, ArgsAtHead, Decl),
+
+ list.foldl(abstract_mode_constraints.add_constraint(Context, ProcId),
+ DeclConstraints, !Constraints).
+
+%-----------------------------------------------------------------------------%
+
+var_info_init = mc_var_info(varset.init, bimap.init).
+
%-----------------------------------------------------------------------------%
+ % prog_var_at_path(ProgVarset, PredId, ProgVar, GoalPath, MCVar, !VarInfo)
+ %
+ % MCVar is the constraint variable corresponding to the proposition
+ % that ProgVar is created at GoalPath in predicate PredId,
+ % it is created if necessary and stored in VarInfo (in which
+ % case we need a string name of ProgVar in ProgVarset).
+ %
+:- pred prog_var_at_path(prog_varset::in, pred_id::in, prog_var::in,
+ goal_path::in, mc_var::out, mc_var_info::in, mc_var_info::out) is det.
+
+prog_var_at_path(ProgVarset, PredId, ProgVar, GoalPath, MCVar, !VarInfo) :-
+ !.VarInfo = mc_var_info(MCVarset0, VarMap0),
+ ensure_prog_var_at_path(ProgVarset, PredId, GoalPath, ProgVar,
+ MCVarset0, MCVarset, VarMap0, VarMap),
+ MCVar = prog_var_at_path(VarMap, PredId, GoalPath, ProgVar),
+ !:VarInfo = mc_var_info(MCVarset, VarMap).
+
+ % prog_var_at_paths(ProgVarset, PredId, ProgVar, GoalPaths, MCVars,
+ % !VarInfo)
+ %
+ % MCVars are the constraint variables corresponding to propositions
+ % that ProgVar is created at GoalPath in predicate PredId, for each
+ % GoalPath in GoalPaths. The constraint variables are created if
+ % necessary and stored in VarInfo (in which case we need a string
+ % name of ProgVar in ProgVarset).
+ %
+:- pred prog_var_at_paths(prog_varset::in, pred_id::in, prog_var::in,
+ list(goal_path)::in, list(mc_var)::out, mc_var_info::in,
+ mc_var_info::out) is det.
+
+prog_var_at_paths(ProgVarset, PredID, ProgVar, GoalPaths, MCVars, !VarInfo) :-
+ list.map_foldl(prog_var_at_path(ProgVarset, PredID, ProgVar),
+ GoalPaths, MCVars, !VarInfo).
+
+ % prog_vars_at_path(ProgVarset, PredId, ProgVars, GoalPath, MCVars,
+ % !VarInfo)
+ %
+ % MCVars are the constraint variables corresponding to propositions
+ % that ProgVar is created at GoalPath in predicate PredId, for each
+ % ProgVar in ProgVars. They are created if necessary and stored in
+ % VarInfo (in which case we will need a string name for ProgVar from
+ % ProgVarset).
+ %
+:- pred prog_vars_at_path(prog_varset::in, pred_id::in, list(prog_var)::in,
+ goal_path::in, list(mc_var)::out, mc_var_info::in, mc_var_info::out)
+ is det.
+
+prog_vars_at_path(ProgVarset, PredId, ProgVars, GoalPath, MCVars, !VarInfo) :-
+ list.map_foldl(
+ (pred(ProgVar::in, MCVar::out, !.VarInfo::in, !:VarInfo::out) is det :-
+ prog_var_at_path(ProgVarset, PredId, ProgVar, GoalPath, MCVar,
+ !VarInfo)
+ ), ProgVars, MCVars, !VarInfo).
+
+ % ensure_prog_var_at_path(ProgVarset, PredId, GoalPath, ProgVar,
+ % !Varset, !VarMap)
+ %
+ % Adds, if necessary, to Varset and VarMap the constraint variable
+ % and its abstract representation that represents the proposition
+ % that ProgVar is produced at GoalPath in PredId (in some mode
+ % of execution). ProgVarset should contain a string name for ProgVar.
+ %
+:- pred ensure_prog_var_at_path(prog_varset::in, pred_id::in, goal_path::in,
+ prog_var::in, mc_varset::in, mc_varset::out, mc_var_map::in,
+ mc_var_map::out) is det.
+
+ensure_prog_var_at_path(ProgVarset, PredId, GoalPath, ProgVar,
+ !Varset, !VarMap) :-
+ RepVar = (ProgVar `in` PredId) `at` GoalPath,
+ ( bimap.search(!.VarMap, RepVar, _) ->
+ true
+ ;
+ MCVarName = rep_var_to_string(ProgVarset, RepVar),
+ svvarset.new_named_var(MCVarName, NewMCVar, !Varset),
+ svbimap.det_insert(RepVar, NewMCVar, !VarMap)
+ ).
+
% prog_var_at_path(VarMap, PredId, GoalPath, ProgVar) = ConstraintVar:
%
- % consults the map to get the constraint variable ConstraintVar that says
- % that ProgVar is produced at GoalPath. The lookup function will report
- % an error if the key (ProgVar `in` PredId) `at` GoalPath does not exist
- % in the map.
+ % Consults the VarMap to get the constraint variable ConstraintVar
+ % that represents the proposition that ProgVar is produced at
+ % GoalPath in predicate PredId. The lookup function will report an
+ % error if the key (ProgVar `in` PredId) `at` GoalPath does not
+ % exist in the map.
%
:- func prog_var_at_path(mc_var_map, pred_id, goal_path, prog_var) = (mc_var).
prog_var_at_path(VarMap, PredId, GoalPath, ProgVar) =
bimap.lookup(VarMap, ((ProgVar `in` PredId) `at` GoalPath)).
+ % Retrieves the mode constraint var as per prog_var_at_path, but
+ % attaches it to the list supplied rather than return it directly.
+ %
+:- func cons_prog_var_at_path(mc_var_map, pred_id, goal_path, prog_var,
+ list(mc_var)) = list(mc_var).
+
+cons_prog_var_at_path(VarMap, PredId, GoalPath, ProgVar, MCVars) =
+ [ prog_var_at_path(VarMap, PredId, GoalPath, ProgVar) | MCVars].
+
% prog_var_at_paths(VarMap, GoalPaths, ProgVar) = ConstraintVars
- % consults the map to form a list of the constraint variables
- % that say that ProgVar is produced at each of the paths in
+ % consults the map to form a list of the constraint variable
+ % propositions that ProgVar is produced at each of the paths in
% GoalPaths respectively. The lookup function will report an
% error if the key (ProgVar `in` PredId) `at` GoalPath does not
% exist in the map for any of the 'GoalPath's in GoalPaths.
@@ -638,44 +793,51 @@
prog_var_at_paths(VarMap, PredId, GoalPaths, ProgVar) =
list.map(
- func(GoalPath) = bimap.lookup(VarMap,
- (ProgVar `in` PredId) `at` GoalPath),
- GoalPaths
- ).
+ func(GoalPath) = prog_var_at_path(VarMap, PredId, GoalPath, ProgVar),
+ GoalPaths).
- % nonlocals_at_path_and_subpaths(VarMap, GoalPath,
- % SubPaths, Nonlocals, NonlocalsAtPath, NonlocalsAtSubPaths)
- % consults the VarMap to find constraint variables associated
+ % nonlocals_at_path_and_subpaths(ProgVarset, GoalPath, SubPaths,
+ % Nonlocals, NonlocalsAtPath, NonlocalsAtSubPaths, !VarInfo)
+ %
+ % consults the VarInfo to find constraint variables associated
% with each of the program variables in the Nonlocals set for a
% GoalPath eg a conjunction and its SubPaths (ie the individual
% conjuncts), although it doesn't check that the SubPaths are
% indeed subpaths of GoalPath. Nonlocals are converted to a
- % sorted set, so the Nth entry of NonlocalsAtPath and the Nth
+ % sorted list so the Nth entry of NonlocalsAtPath and the Nth
% entry of NonlocalsAtSubPaths are respectively the constraint
% variable at the goal and a list of the constraint variables
% for the subgoals, for the same program variable.
%
-:- pred nonlocals_at_path_and_subpaths(
- mc_var_map::in, pred_id::in, goal_path::in, list(goal_path)::in,
- nonlocals::in, list(mc_var)::out, list(list(mc_var))::out) is det.
-
-nonlocals_at_path_and_subpaths(VarMap, PredId, GoalPath, SubPaths, Nonlocals,
- NonlocalsAtPath, NonlocalsAtSubPaths) :-
- NonlocalsAtPath = list.map(prog_var_at_path(VarMap, PredId, GoalPath),
- NonlocalsList),
- NonlocalsAtSubPaths = list.map(prog_var_at_paths(VarMap, PredId, SubPaths),
- NonlocalsList),
+:- pred nonlocals_at_path_and_subpaths(prog_varset::in, pred_id::in,
+ goal_path::in, list(goal_path)::in, nonlocals::in, list(mc_var)::out,
+ list(list(mc_var))::out, mc_var_info::in, mc_var_info::out) is det.
+
+nonlocals_at_path_and_subpaths(ProgVarset, PredId, GoalPath, SubPaths,
+ Nonlocals, NonlocalsAtPath, NonlocalsAtSubPaths, !VarInfo) :-
+ prog_vars_at_path(ProgVarset, PredId, NonlocalsList, GoalPath,
+ NonlocalsAtPath, !VarInfo),
+ list.map_foldl(
+ (pred(Nl::in, NlAtSubPaths::out, !.VInfo::in, !:VInfo::out) is det :-
+ prog_var_at_paths(ProgVarset, PredId, Nl, SubPaths,
+ NlAtSubPaths, !VInfo)
+ ), NonlocalsList, NonlocalsAtSubPaths, !VarInfo),
NonlocalsList = set.to_sorted_list(Nonlocals).
%----------------------------------------------------------------------------%
-mode_decls_constraints(
- ModuleInfo, VarMap, PredId, Decls, HeadVarsList, Constraints) :-
- ConstraintsList = list.map_corresponding(
- mode_decl_constraints(ModuleInfo),
+mode_decls_constraints(ModuleInfo, VarMap, PredId, Decls, HeadVarsList,
+ Constraints) :-
+
+ % Transform each headvar into the constraint variable representing
+ % the proposition that it is produced at the empty goal path (ie
+ % that it is produced by a call to the predicate).
+ HeadVarsMCVars =
list.map(list.map(prog_var_at_path(VarMap, PredId, [])), HeadVarsList),
- Decls
- ),
+ % Make the constraints for each declaration.
+ ConstraintsList = list.map_corresponding(
+ mode_decl_constraints(ModuleInfo), HeadVarsMCVars, Decls),
+
Constraints0 = list.condense(ConstraintsList),
( Constraints0 = [conj(OneModeOnlyConstraints)] ->
Constraints = OneModeOnlyConstraints
@@ -683,18 +845,24 @@
Constraints = [disj(Constraints0)]
).
- % call_mode_decls_constraints(ModuleInfo, VarMap, CallingPred,
- % Decls, GoalPath, CallArgs, Constraints)
+ % add_call_mode_decls_constraints(ModuleInfo, ProgVarset, Context,
+ % CallingPred, Decls, GoalPath, CallArgs, !VarInfo, !Constraints)
%
- % Returns
- % disj([ConstraintsForMode1, ..., ConstraintsForModen])
+ % Adds the following to the mode_constraints:
+ % disj([ConstraintsForMode1, ..., ConstraintsForModeN])
+ % with context Context, and goal path GoalPath (of the position of
+ % the call). ConstraintsForModei are the constraints for when the
+ % callee is called in the ith mode of Decls.
+ % Assumes CallArgs to be the program variables from CallingPred
+ % that are to be used as arguments for the called predicate.
+ % Uses and stores constraint variables in VarInfo, finding
+ % the string names for program variables in ProgVarset.
%
% Note that if Decls is an empty list, this is interpreted as
% there being no modes for which the predicate can be executed
% and the returned constraints are [disj([])] which cannot be
- % satisfied. Predicate calls for predicates with no declared
- % modes should not be handled by this - they must be handled
- % elsewhere.
+ % satisfied. Predicate calls for callee predicates with no declared
+ % modes should not be handled by this.
%
% The constraints for a (call to a) predicate with declared
% modes is the disjunction of the constraints for each declared
@@ -704,175 +872,215 @@
% then it is produced by the predicate. Otherwise it is free ->
% free and is not produced.
%
-:- pred call_mode_decls_constraints(module_info::in,
- mc_var_map::in, pred_id::in, list(list(mer_mode))::in,
- goal_path::in, args::in, mode_constraints::out) is det.
-
-call_mode_decls_constraints(ModuleInfo, VarMap, CallingPred, Decls, GoalPath,
- CallArgs, Constraints) :-
- CallArgsHere = list.map(prog_var_at_path(VarMap, CallingPred, GoalPath),
- CallArgs),
- Constraints0 =
- list.condense(list.map(mode_decl_constraints(ModuleInfo, CallArgsHere),
- Decls)),
- ( Constraints0 = [conj(OneModeOnlyConstraints)] ->
- Constraints = OneModeOnlyConstraints
+:- pred add_call_mode_decls_constraints(module_info::in,
+ prog_varset::in, prog_context::in, pred_id::in, list(list(mer_mode))::in,
+ goal_path::in, args::in, mc_var_info::in, mc_var_info::out,
+ mode_constraints::in, mode_constraints::out) is det.
+
+add_call_mode_decls_constraints(ModuleInfo, ProgVarset, CallContext,
+ CallingPred, Decls, GoalPath, CallArgs, !VarInfo, !Constraints) :-
+ prog_vars_at_path(ProgVarset, CallingPred, CallArgs, GoalPath,
+ CallArgsHere, !VarInfo),
+ ConstraintFormulae = list.condense(list.map(
+ mode_decl_constraints(ModuleInfo, CallArgsHere),
+ Decls)),
+ ( ConstraintFormulae = [conj(OneModeOnlyConstraints)] ->
+ list.foldl(abstract_mode_constraints.add_constraint(CallContext),
+ OneModeOnlyConstraints, !Constraints)
;
- Constraints = [disj(Constraints0)]
+ abstract_mode_constraints.add_constraint(CallContext,
+ disj(ConstraintFormulae), !Constraints)
).
% mode_decl_constraints(ModuleInfo, ConstraintVars, ArgModes)
- % looks at each mode to see if its variable is produced, and
- % creates constraints for the corresponding constraint variables
- % accordingly.
+ % looks at each mode in ArgModes to see if its variable is produced,
+ % and creates constraints for the corresponding constraint variable
+ % in ConstraintVars accordingly.
%
:- func mode_decl_constraints(module_info, list(mc_var), list(mer_mode)) =
- mode_constraints.
+ constraint_formulae.
mode_decl_constraints(ModuleInfo, ConstraintVars, ArgModes) =
[conj(list.map_corresponding(
- (func(CVar, Mode) =
- atomic_constraint(equiv_bool(CVar, IsProduced)) :-
- mode_util.mode_get_insts(ModuleInfo, Mode, InitialInst, FinalInst),
- (
- % Already produced.
- not inst_match.inst_is_free(ModuleInfo, InitialInst)
- ->
- IsProduced = no % Not produced here.
- ;
- % free -> non-free
- not inst_match.inst_is_free( ModuleInfo, FinalInst)
- ->
- IsProduced = yes % Produced here.
- ;
- IsProduced = no % free -> free
- % Not produced here.
- )
- ),
- ConstraintVars,
- ArgModes
- ))].
-
-add_sufficient_in_modes_for_type_info_args(Args, Decl, FullDecl) :-
- NumArgs = list.length(Args),
- NumArgModes = list.length(Decl),
- Diff = NumArgs - NumArgModes,
- ( Diff = 0 ->
- FullDecl = Decl
- ; Diff > 0 ->
- FullDecl = list.append(list.duplicate(Diff, prog_mode.in_mode), Decl)
- ;
- unexpected(this_file, "Too many mode declared args.m")
- ).
-
- % call_headvar_constraints(HeadVars, VarMap, GoalPath, CallArgs,
- % Constraints)
- % Forms constraints that mean any call arg will be produced if
- % the corresponding headvar is produced by the main goal of the
- % called predicate.
+ single_mode_constraints(ModuleInfo), ConstraintVars, ArgModes))].
+
+ % single_mode_constraints(ModuleInfo, MCVar, Mode) returns a
+ % constraint on MCVar such that the program variable it
+ % refers to should change instantiation according to Mode
+ % at the goal path it refers to.
+ %
+:- func single_mode_constraints(module_info, mc_var, mer_mode) =
+ constraint_formula.
+
+single_mode_constraints(ModuleInfo, MCVar, Mode) =
+ atomic_constraint(equiv_bool(MCVar, IsProduced)) :-
+ mode_util.mode_get_insts(ModuleInfo, Mode, InitialInst, FinalInst),
+ (
+ % Already produced?
+ not inst_match.inst_is_free(ModuleInfo, InitialInst)
+ ->
+ IsProduced = no % Not produced here.
+ ;
+ % free -> non-free
+ not inst_match.inst_is_free(ModuleInfo, FinalInst)
+ ->
+ IsProduced = yes % Produced here.
+ ;
+ % free -> free
+ IsProduced = no % Not produced here.
+ ).
+
+ % add_call_headvar_constraints(ProgVarset, Context, GoalPath, Caller,
+ % CallArgs, Callee, HeadVars, CallArgs, !VarInfo, !Constraints)
+ %
+ % Forms constraints that, when satisfied, mean any call arg will be
+ % produced if the corresponding headvar is produced by the main goal
+ % of the called predicate.
+ % The constraints are annotated with Context, which should be the
+ % context of the call goal in the original program.
%
% This should not be used if a mode declaration is supplied, as
% it means a predicate can only be used in a single mode
- % throughout a whole SCC.
+ % throughout the whole body of the calling predicate.
%
-:- pred call_headvar_constraints(mc_var_map::in, goal_path::in,
- pred_id::in, args::in, pred_id::in, args::in,
- mode_constraints::out) is det.
-
-call_headvar_constraints(VarMap, GoalPath,
- CallingPred, CallArgs, CalledPred, HeadVars, Constraints) :-
- HeadVarsAtHome = list.map(prog_var_at_path(VarMap, CalledPred, []),
- HeadVars),
- CallArgsHere = list.map( prog_var_at_path(VarMap, CallingPred, GoalPath),
- CallArgs),
- Constraints = list.map_corresponding(
- (func(HeadVarThere, CallArgHere) =
- atomic_constraint(equivalent([HeadVarThere, CallArgHere]))
- ),
- HeadVarsAtHome, CallArgsHere
- ).
+:- pred add_call_headvar_constraints(prog_varset::in, prog_context::in,
+ goal_path::in, pred_id::in, args::in, pred_id::in, args::in,
+ mc_var_info::in, mc_var_info::out, mode_constraints::in,
+ mode_constraints::out) is det.
+
+add_call_headvar_constraints(ProgVarset, Context, GoalPath, CallerPredId,
+ CallArgs, CalleePredId, CalleeHeadVars, !VarInfo, !Constraints) :-
+ prog_vars_at_path(ProgVarset, CalleePredId, CalleeHeadVars, [],
+ HeadVarsAtHead, !VarInfo),
+ prog_vars_at_path(ProgVarset, CallerPredId, CallArgs, GoalPath,
+ CallArgsHere, !VarInfo),
+
+ % If the head var is produced by the body of the callee, then the
+ % corresponding argument variable is produced at the goal path
+ % of the call.
+ EquivVarss = list.map_corresponding(func(A, B) = [A, B],
+ HeadVarsAtHead, CallArgsHere),
+ list.foldl(equivalent(Context), EquivVarss, !Constraints).
%-----------------------------------------------------------------------------%
- % At times we want constraint variables at the sub-paths of a
- % goal (eg conjunction/disjunction) but only at the paths in
- % which the corresponding program variable occurs and is
- % non-local. This predicate builds two maps - one for variables
- % non-local to the parent goal and one for those local to it.
- % They map program variables that are non-local to the sub-goals
- % to the constraint variables associated with them being
- % produced at each of the goal paths in which they appear.
+ % add_goal_nonlocals_to_conjunct_production_maps(VarMap, PredId,
+ % Nonlocals, Goal, !ConjConstraintsInfo)
%
-:- pred fold_goal_into_var_position_maps(
+ % Assumes Goal is a conjunct of a conjunction with nonlocal
+ % variables Nonlocals, in predicate PredId. Adds the nonlocal
+ % variables from Goal to ConjConstraintsInfo according to whether
+ % they are local or nonlocal to the conjunction as a whole. The
+ % constraint variable propositions that the nonlocals of Goal are
+ % produced at Goal are associated with their corresponding program
+ % variable in ConjConstraintsInfo. These constraint variables are
+ % found in VarMap.
+ %
+:- pred add_goal_nonlocals_to_conjunct_production_maps(
mc_var_map::in, pred_id::in, nonlocals::in, hlds_goal::in,
- multi_map(prog_var, mc_var)::in, multi_map(prog_var, mc_var)::out,
- multi_map(prog_var, mc_var)::in, multi_map(prog_var, mc_var)::out) is det.
+ conj_constraints_info::in, conj_constraints_info::out) is det.
-fold_goal_into_var_position_maps(VarMap, PredId, Nonlocals,
- _SubGoalExpr - SubGoalInfo, !LocalsMap, !NonlocalsMap) :-
+add_goal_nonlocals_to_conjunct_production_maps(VarMap, PredId, Nonlocals,
+ _SubGoalExpr - SubGoalInfo, !ConjConstraintsInfo) :-
goal_info_get_nonlocals(SubGoalInfo, SubGoalNonlocals),
goal_info_get_goal_path(SubGoalInfo, SubGoalPath),
+
+ % These are variables nonlocal to the conjunction that
+ % appear in this particular conjunct.
Nonlocal = set.intersect(SubGoalNonlocals, Nonlocals),
- % Note that if any variable in Nonlocals does not
- % appear in the nonlocal set of any conjunct then
- % this is simply due a conservative estimate on the
- % non-locals of the conjunction and we can't form
- % reliable constraints for it anyway (XXX although we
- % might want to consider constraining it to false
- % considering as it can't be produced at this goal path)
+
+ % These are variables local to the conjunction that
+ % are non-local to this particular conjunct.
Local = set.difference(SubGoalNonlocals, Nonlocals),
- % Note this is the local variables that
- % are non-local to this particular sub-goal
- set.fold(fold_variable_into_var_position_map(VarMap, PredId, SubGoalPath),
- Local, !LocalsMap),
- set.fold(fold_variable_into_var_position_map(VarMap, PredId, SubGoalPath),
- Nonlocal, !NonlocalsMap).
-
- % A subsection of fold_goal_into_var_position_maps, puts into
- % the map the key ProgVar with the constraint variable that says
- % ProgVar is bound at GoalPath.
+
+ some [!LocalsMap, !NonlocalsMap] (
+ !:LocalsMap = !.ConjConstraintsInfo ^ locals_positions,
+ !:NonlocalsMap = !.ConjConstraintsInfo ^ nonlocals_positions,
+
+ set.fold(add_variable_to_conjunct_production_map(VarMap, PredId,
+ SubGoalPath), Local, !LocalsMap),
+ set.fold(add_variable_to_conjunct_production_map(VarMap, PredId,
+ SubGoalPath), Nonlocal, !NonlocalsMap),
+
+ !:ConjConstraintsInfo = !.ConjConstraintsInfo ^ locals_positions :=
+ !.LocalsMap,
+ !:ConjConstraintsInfo = !.ConjConstraintsInfo ^ nonlocals_positions :=
+ !.NonlocalsMap
+ ).
+
+ % add_variable_to_conjunct_production_map(VarMap, PredId, GoalPath
+ % ProgVar, !ConjunctProductionMap)
+ %
+ % A subsection of add_goal_nonlocals_to_conjunct_production_maps,
+ % puts into the ConjunctProductionMap the key ProgVar with the
+ % constraint variable found in VarMap, that represents the
+ % proposition that ProgVar is bound at GoalPath in predicate PredId.
%
-:- pred fold_variable_into_var_position_map(
+:- pred add_variable_to_conjunct_production_map(
mc_var_map::in, pred_id::in, goal_path::in, prog_var::in,
- multi_map(prog_var, mc_var)::in, multi_map(prog_var, mc_var)::out) is det.
+ conjunct_production_map::in, conjunct_production_map::out) is det.
-fold_variable_into_var_position_map(VarMap, PredId, GoalPath, ProgVar, !Map) :-
+add_variable_to_conjunct_production_map(VarMap, PredId, GoalPath, ProgVar,
+ !ConjunctProductionMap) :-
MCVar = prog_var_at_path(VarMap, PredId, GoalPath, ProgVar),
- svmulti_map.set(ProgVar, MCVar, !Map).
+ svmulti_map.set(ProgVar, MCVar, !ConjunctProductionMap).
+
+ % add_nonlocal_var_conj_constraints(ProgVarset, PredId, Context, GoalPath,
+ % ProgVar, ProgVarAtConjuncts, !VarInfo, !Constraints)
+ %
+ % Adds conjunction constraints concerning ProgVar, a variable
+ % in predicate PredID, to Constraints. The conjunction should
+ % exist at the position indicated by GoalPath in the predicate,
+ % and have context Context in the source file. ProgVarset should
+ % contain a string name for ProgVar.
+ % ProgVar should be a variable in the nonlocal set of the conjunction,
+ % and as such may be produced outside it. Therefore the constraints
+ % will be that ProgVar is produced at "at most one" of the conjuncts.
+ % ProgVarAtConjuncts should contain the constraint variable
+ % propositions that ProgVar is produced at a conjunct for each
+ % conjunct in which it appears.
+ %
+:- pred add_nonlocal_var_conj_constraints(prog_varset::in, pred_id::in,
+ prog_context::in, goal_path::in, prog_var::in, list(mc_var)::in,
+ mc_var_info::in, mc_var_info::out, mode_constraints::in,
+ mode_constraints::out) is det.
+
+add_nonlocal_var_conj_constraints(ProgVarset, PredId, Context, GoalPath,
+ ProgVar, ProgVarAtConjuncts, !VarInfo, !Constraints) :-
+
+ equiv_disj(Context, ProgVarAtGoalPath, ProgVarAtConjuncts, !Constraints),
+ at_most_one(Context, ProgVarAtConjuncts, !Constraints),
+
+ prog_var_at_path(ProgVarset, PredId, ProgVar, GoalPath, ProgVarAtGoalPath,
+ !VarInfo).
- % This predicate adds the constraints for a variable in the
- % non-local set of a conjunction (to other previously
- % constructed constraints). The NonLocalsMap should provide the
- % list of constraint variables representing the program variable
- % being produced at each conjunct it appears in respectively.
- %
-:- pred fold_nonlocal_var_into_conj_constraints(mc_var_map::in,
- pred_id::in, multi_map(prog_var, mc_var)::in, goal_path::in,
- prog_var::in, mode_constraints::in, mode_constraints::out) is det.
-
-fold_nonlocal_var_into_conj_constraints(VarMap, PredId, NonlocalsMap,
- GoalPath, ProgVar, !Constraints) :-
- NewConstraints = [atomic_constraint(equiv_disj(ProgVarAtGoalPath, Xs)),
- atomic_constraint(at_most_one(Xs))],
- list.append(NewConstraints, !Constraints),
- ProgVarAtGoalPath = prog_var_at_path(VarMap, PredId, GoalPath, ProgVar),
- Xs = multi_map.lookup(NonlocalsMap, ProgVar).
-
- % This predicate adds the constraints for a variable in the
- % non-local set of a conjunct but not nonlocal to the
- % conjunction as a whole, to the constraints supplied. The
- % NonLocalsMap should provide the list of constraint variables
- % representing the program variable being produced at each
- % conjunct it appears in respectively.
- %
-:- pred fold_local_var_into_conj_constraints(
- mc_var_map::in, multi_map(prog_var, mc_var)::in,
- prog_var::in, mode_constraints::in, mode_constraints::out) is det.
-fold_local_var_into_conj_constraints(_VarMap, LocalsMap, ProgVar,
+ % add_local_var_conj_constraints(Context, ProgVar, MCVars, !Constraints)
+ %
+ % Adds conjunct constraints relating to ProgVar, to Constraints.
+ % ProgVar should be local to the conjunction, and MCVars should
+ % represent propositions that ProgVar is produced at conjuncts, for
+ % each conjunct that ProgVar is nonlocal to. Context should be
+ % the location in the source file that the conjunction in question
+ % came from.
+ %
+ % The constraints are: the program variable must be produced at
+ % exactly one conjunct.
+ %
+:- pred add_local_var_conj_constraints(prog_context::in, prog_var::in,
+ list(mc_var)::in, mode_constraints::in, mode_constraints::out) is det.
+
+add_local_var_conj_constraints(Context, _ProgVar, ProgVarAtConjuncts,
!Constraints) :-
- list.cons(atomic_constraint(exactly_one(Xs)), !Constraints),
- Xs = multi_map.lookup(LocalsMap, ProgVar).
+ exactly_one(Context, ProgVarAtConjuncts, !Constraints).
+
+ % Initialises the conj_constraints_info_structure.
+ %
+:- func conj_constraints_info_init = conj_constraints_info.
+
+conj_constraints_info_init =
+ conj_constraints_info(multi_map.init, multi_map.init).
+
%-----------------------------------------------------------------------------%
Index: compiler/check_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/check_hlds.m,v
retrieving revision 1.10
diff -u -r1.10 check_hlds.m
--- compiler/check_hlds.m 12 Oct 2005 23:51:34 -0000 1.10
+++ compiler/check_hlds.m 25 Jan 2006 04:41:54 -0000
@@ -38,8 +38,6 @@
% Mode analysis
%:- module mode_analysis.
- :- include_module abstract_mode_constraints.
- :- include_module build_mode_constraints.
:- include_module delay_info.
:- include_module inst_match.
:- include_module inst_util.
@@ -53,9 +51,18 @@
:- include_module modecheck_call.
:- include_module modecheck_unify.
:- include_module modes.
- :- include_module prop_mode_constraints.
:- include_module unify_proc.
:- include_module unique_modes.
+
+ % XXX This doesn't belong here but we don't know where it's home is at
+ % the moment.
+ %
+ :- include_module abstract_mode_constraints.
+ :- include_module build_mode_constraints.
+ :- include_module mcsolver.
+ :- include_module ordering_mode_constraints.
+ :- include_module prop_mode_constraints.
+
%:- end_module mode_analysis.
% Indexing and determinism analysis
Index: compiler/mode_constraints.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mode_constraints.m,v
retrieving revision 1.18
diff -u -r1.18 mode_constraints.m
--- compiler/mode_constraints.m 17 Nov 2005 15:57:24 -0000 1.18
+++ compiler/mode_constraints.m 23 Jan 2006 04:03:00 -0000
@@ -6,7 +6,7 @@
% Public License - see the file COPYING in the Mercury distribution.
%-----------------------------------------------------------------------------%
-% File: mode_constraint.m.
+% File: mode_constraints.m.
% Main author: dmo.
% This module implements the top level of the algorithm described in the
@@ -19,6 +19,8 @@
:- module check_hlds__mode_constraints.
:- interface.
+:- import_module check_hlds.abstract_mode_constraints.
+:- import_module check_hlds.prop_mode_constraints.
:- import_module hlds.hlds_module.
:- import_module io.
@@ -27,14 +29,21 @@
:- pred process_module(module_info::in, module_info::out,
io::di, io::uo) is det.
+ % dump_abstract_constraints(ModuleInfo, Varset, PredConstraintsMap, !IO)
+ %
+ % Dumps the constraints in the PredConstraintsMap to file
+ % modulename.mode_constraints
+ %
+:- pred dump_abstract_constraints(module_info::in, mc_varset::in,
+ pred_constraints_map::in, io::di, io::uo) is det.
+
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
:- implementation.
-:- import_module check_hlds.prop_mode_constraints.
-:- import_module check_hlds.abstract_mode_constraints.
:- import_module check_hlds.build_mode_constraints.
+:- import_module check_hlds.ordering_mode_constraints.
:- import_module check_hlds.goal_path.
:- import_module check_hlds.mode_constraint_robdd.
@@ -104,9 +113,10 @@
get_predicate_sccs(!.ModuleInfo, SCCs),
- % Stage 1: Process SCCs bottom-up to determine variable producers.
(
New = no,
+
+ % Stage 1: Process SCCs bottom-up to determine variable producers.
list__foldl3(process_scc(Simple), SCCs,
!ModuleInfo, map__init, PredConstraintMap, !IO),
@@ -125,34 +135,66 @@
clear_caches(!IO)
;
New = yes,
- list__foldl3(prop_mode_constraints__process_scc(!.ModuleInfo), SCCs,
- varset.init, ConstraintVarset,
- bimap.init, _ConstraintVarMap,
- map.init, AbstractModeConstraints
- ),
- hlds_module.module_info_get_name(!.ModuleInfo, ModuleName),
+ % Stage 1: Process SCCs bottom-up to determine constraints on
+ % variable producers and consumers.
+ list__foldl3(prop_mode_constraints__process_scc,
+ SCCs, !ModuleInfo, var_info_init, VarInfo,
+ map.init, AbstractModeConstraints),
+
+ globals__io_lookup_bool_option(debug_mode_constraints, Debug, !IO),
+ ( Debug = yes,
+ ConstraintVarset = mc_varset(VarInfo),
+ pretty_print_pred_constraints_map(!.ModuleInfo, ConstraintVarset,
+ AbstractModeConstraints, !IO)
+ ;
+ Debug = no
+ ),
- CreateDirectories = yes,
- parse_tree.modules.module_name_to_file_name(ModuleName,
- ".mode_constraints", CreateDirectories, FileName, !IO),
- OutputFile = FileName,
+ % Stage 2: Order conjunctions based on solutions to
+ % the producer-consumer constraints.
+ ModuleInfo0 = !.ModuleInfo,
+ ConstraintVarMap = rep_var_map(VarInfo),
+ promise_equivalent_solutions [ModuleInfo1] (
+ mode_reordering(AbstractModeConstraints, ConstraintVarMap, SCCs,
+ ModuleInfo0, ModuleInfo1)
+ ),
+ !:ModuleInfo = ModuleInfo1,
- io.open_output(OutputFile, IOResult, !IO),
(
- IOResult = ok(OutputStream),
- io.set_output_stream(OutputStream, OldOutStream, !IO),
- pretty_print_pred_constraints_map(!.ModuleInfo, ConstraintVarset,
- AbstractModeConstraints, !IO),
- io.set_output_stream(OldOutStream, _, !IO),
- io.close_output(OutputStream, !IO)
+ Debug = yes,
+ list.foldl(ordering_mode_constraints.dump_goal_paths(!.ModuleInfo),
+ SCCs, !IO)
;
- IOResult = error(_),
- unexpected(this_file,
- "failed to open " ++ FileName ++ " for output.")
+ Debug = no
)
+
+ ).
+
+dump_abstract_constraints(ModuleInfo, ConstraintVarset, ModeConstraints,
+ !IO) :-
+
+ hlds_module.module_info_get_name(ModuleInfo, ModuleName),
+ CreateDirectories = yes,
+ parse_tree.modules.module_name_to_file_name(ModuleName,
+ ".mode_constraints", CreateDirectories, FileName, !IO),
+ OutputFile = FileName,
+
+ io.open_output(OutputFile, IOResult, !IO),
+ (
+ IOResult = ok(OutputStream),
+ io.set_output_stream(OutputStream, OldOutStream, !IO),
+ pretty_print_pred_constraints_map(ModuleInfo, ConstraintVarset,
+ ModeConstraints, !IO),
+ io.set_output_stream(OldOutStream, _, !IO),
+ io.close_output(OutputStream, !IO)
+ ;
+ IOResult = error(_),
+ unexpected(this_file,
+ "failed to open " ++ FileName ++ " for output.")
).
+
:- pred process_scc(bool::in, list(pred_id)::in,
module_info::in, module_info::out,
pred_constraint_map::in, pred_constraint_map::out, io::di, io::uo) is det.
Index: compiler/options.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/options.m,v
retrieving revision 1.490
diff -u -r1.490 options.m
--- compiler/options.m 25 Jan 2006 04:51:50 -0000 1.490
+++ compiler/options.m 25 Jan 2006 05:36:13 -0000
@@ -137,6 +137,7 @@
; debug_make
; debug_closure
; debug_trail_usage
+ ; debug_mode_constraints
% Output options
; make_short_interface
@@ -881,7 +882,8 @@
debug_stack_opt - int(-1),
debug_make - bool(no),
debug_closure - bool(no),
- debug_trail_usage - bool(no)
+ debug_trail_usage - bool(no),
+ debug_mode_constraints - bool(no)
]).
option_defaults_2(output_option, [
% Output Options (mutually exclusive)
@@ -1585,6 +1587,7 @@
long_option("debug-make", debug_make).
long_option("debug-closure", debug_closure).
long_option("debug-trail-usage", debug_trail_usage).
+long_option("debug-mode-constraints", debug_mode_constraints).
% output options (mutually exclusive)
long_option("generate-source-file-mapping",
@@ -2902,6 +2905,11 @@
"--debug-trail-usage",
"\tOutput detailed debugging traces of the `--analyse-trail-usage'",
"\toption."
+% The mode constraints code is still experimental so this option is
+% currently commented out.
+% "--debug-mode-constraints",
+% "\tOutput detailed debugging traces of the
`--prop-mode-constraints'",
+% "\toption."
]).
:- pred options_help_output(io::di, io::uo) is det.
Index: compiler/prop_mode_constraints.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prop_mode_constraints.m,v
retrieving revision 1.5
diff -u -r1.5 prop_mode_constraints.m
--- compiler/prop_mode_constraints.m 28 Nov 2005 04:11:52 -0000 1.5
+++ compiler/prop_mode_constraints.m 24 Jan 2006 03:56:17 -0000
@@ -9,15 +9,11 @@
% File: prop_mode_constraints.m.
% Main author: richardf.
-% This module provides an alternate process_scc predicate for the
-% mode_constraints module that builds the new abstract constraint data
-% structures intended for a propagation solver. It deals only with the
-% simple constraint system, described in the paper "Constraint-based
-% mode analysis of Mercury" by David Overton, Zoltan Somogyi and Peter
-% Stuckey.
-
-% XXX That paper is the main documentation of the concepts
-% behind the algorithm as well as the algorithm itself.
+% XXX This module essentially serves as interface between the
+% pre-existing mode_constraints module and the new
+% abstract_mode_constraints and build_mode_constraints modules.
+% Ultimately its contents should probably be moved into those
+% modules respectively.
%-----------------------------------------------------------------------------%
@@ -26,7 +22,6 @@
:- import_module check_hlds.abstract_mode_constraints.
:- import_module check_hlds.build_mode_constraints.
-
:- import_module hlds.hlds_module.
:- import_module hlds.hlds_pred.
@@ -36,24 +31,32 @@
%-----------------------------------------------------------------------------%
- % This predicate adds to the pred_constraints_map the mode declaration and
- % goal constraints for each of the predicates in the provided SCC. Any
- % required constraint variables are added to the mc_varset and mc_var_map.
- % Calls to predicates with no mode declaration require head variable
- % constraint variables, so these are produced first for all preds in the
- % SCC before goal constraints.
- %
-:- pred process_scc(module_info::in, list(pred_id)::in,
- mc_varset::in, mc_varset::out, mc_var_map::in, mc_var_map::out,
- pred_constraints_map::in, pred_constraints_map::out) is det.
-
% Storing constraints by predicate.
%
:- type pred_constraints_map == map(pred_id, mode_constraints).
+%-----------------------------------------------------------------------------%
+
+ % process_scc(SCC, !ModuleInfo, !Varset, !VarMap, !PredConstraintsMap),
+ %
+ % For each predicate in SCC:
+ % Adds producer/consumer constraints to PredConstraintsMap,
+ % Adds goal path annotations to its clauses in ModuleInfo,
+ % Adds any constraint variables it requires to Varset and VarMap
+ %
+:- pred process_scc(list(pred_id)::in, module_info::in, module_info::out,
+ mc_var_info::in, mc_var_info::out, pred_constraints_map::in,
+ pred_constraints_map::out) is det.
+
+ % Checks whether a predicate has been imported according to the
+ % status_is_imported pred in the hlds_pred module.
+ %
+:- pred module_info_pred_status_is_imported(module_info::in, pred_id::in)
+ is semidet.
+
% Writes in human readable form to the current output stream the
- % information in the pred_constraints_map, indicating which predicate each
- % set of constraints applies to.
+ % information in the pred_constraints_map, indicating which
+ % predicate each set of constraints applies to.
%
:- pred pretty_print_pred_constraints_map(module_info::in, mc_varset::in,
pred_constraints_map::in, io::di, io::uo) is det.
@@ -64,11 +67,13 @@
:- implementation.
:- import_module check_hlds.goal_path.
+:- import_module check_hlds.mcsolver.
:- import_module check_hlds.mode_constraint_robdd.
:- import_module check_hlds.mode_ordering.
:- import_module check_hlds.mode_util.
:- import_module hlds.hhf.
:- import_module hlds.hlds_data.
+:- import_module hlds.hlds_error_util.
:- import_module hlds.hlds_goal.
:- import_module hlds.inst_graph.
:- import_module hlds.passes_aux.
@@ -76,6 +81,7 @@
:- import_module libs.globals.
:- import_module libs.options.
:- import_module mode_robdd.
+:- import_module parse_tree.error_util.
:- import_module parse_tree.prog_data.
:- import_module parse_tree.prog_mode.
:- import_module parse_tree.modules.
@@ -89,7 +95,6 @@
:- import_module robdd.
:- import_module set.
:- import_module sparse_bitset.
-:- import_module std_util.
:- import_module string.
:- import_module svmap.
:- import_module term.
@@ -98,153 +103,148 @@
%-----------------------------------------------------------------------------%
-process_scc(ModuleInfo, SCC0, !Varset, !VarMap, !Constraints) :-
- % Process only predicates from this module
- list.filter(
- (pred(PredId::in) is semidet :-
- module_info_pred_info(ModuleInfo, PredId, PredInfo),
- ( pred_info_is_imported(PredInfo)
- ; pred_info_is_pseudo_imported(PredInfo)
- )
- ),
- SCC0,
- _,
- SCC
- ),
-
- % Prepares the solver variables for the home path of
- % each predicate of the SCC - needed for calls to
- % predicates in the same SCC that do not have mode
- % declarations.
- add_mc_vars_for_scc_heads(ModuleInfo, SCC, !Varset, !VarMap),
-
- % Now go through the SCC and add the constraint
- % variables and then constraints predicate by predicate
- list.foldl3(process_pred(ModuleInfo), SCC, !Varset, !VarMap, !Constraints).
+process_scc(SCC0, !ModuleInfo, !VarInfo, !Constraints) :-
+ % Process only predicates from this module
+ list.filter(module_info_pred_status_is_imported(!.ModuleInfo),
+ SCC0, _, SCC),
+
+ % Prepare the solver variables for the home path of
+ % each predicate of the SCC - needed for calls to
+ % predicates in the same SCC that do not have mode
+ % declarations.
+ add_mc_vars_for_scc_heads(!.ModuleInfo, SCC, !VarInfo),
+
+ % Now go through the SCC and add the constraint
+ % variables and then constraints predicate by predicate
+ list.foldl3(process_pred, SCC, !ModuleInfo, !VarInfo, !Constraints).
- % Performs a number of tasks for one predicate:
+ % process_pred(PredId, !ModuleInfo, !Varset, !VarMap, !Constraints)
+ %
+ % Performs a number of tasks for predicate PredId:
% 1) Fills out the goal_path information in the
- % module_info structure
- % 2) Adds constraint variables for program variables
- % corresponding to any location at which they are
- % nonlocal
- % 3) Adds mode declaration constraints
- % 4) Adds goal constraints
+ % ModuleInfo structure
+ % 2) Adds producer/consumer constraint variables for program
+ % variables corresponding to any location at which they are
+ % nonlocal to Varset and VarMap. (Elsewhere is is clear as to
+ % whether they are produced or consumed.)
+ % 3) Adds mode declaration constraints to Constraints
+ % 4) Adds goal constraints to Constraints
%
% NOTE: it relies on the head variables for any predicate
- % without mode declarations that is called to have the
- % constraint variables corresponding to [] to already be in the
- % mc_var_map
- %
-:- pred process_pred(module_info::in, pred_id::in,
- mc_varset::in, mc_varset::out, mc_var_map::in, mc_var_map::out,
- pred_constraints_map::in, pred_constraints_map::out) is det.
+ % without mode declarations that is called by this one (PredId)
+ % to have the constraint variables corresponding to the empty
+ % goal path (ie the whole body of the predicate) to already be
+ % in VarMap (and therefore Varset).
+ %
+:- pred process_pred(pred_id::in, module_info::in, module_info::out,
+ mc_var_info::in, mc_var_info::out, pred_constraints_map::in,
+ pred_constraints_map::out) is det.
+
+process_pred(PredId, !ModuleInfo, !VarInfo, !Constraints) :-
+ module_info_pred_info(!.ModuleInfo, PredId, PredInfo0),
+ process_pred(!.ModuleInfo, PredId, PredInfo0, PredInfo, !VarInfo,
+ !Constraints),
+ module_info_set_pred_info(PredId, PredInfo, !ModuleInfo).
-process_pred(ModuleInfo, PredId, !Varset, !VarMap, !Constraints) :-
- module_info_pred_info(ModuleInfo, PredId, PredInfo),
- process_pred(ModuleInfo, PredId, PredInfo, !Varset, !VarMap,
- !Constraints).
-
- % The working part of process_pred/8 - just with the pred_info
- % unpacked from the module_info
+ % The working part of process_pred/8 - just with the PredInfo
+ % unpacked from the ModuleInfo.
%
:- pred process_pred(module_info::in, pred_id::in, pred_info::in,
- mc_varset::in, mc_varset::out, mc_var_map::in, mc_var_map::out,
- pred_constraints_map::in, pred_constraints_map::out) is det.
+ pred_info::out, mc_var_info::in, mc_var_info::out,
+ pred_constraints_map::in, pred_constraints_map::out)
+ is det.
-process_pred(ModuleInfo, PredId, PredInfo0, !Varset, !VarMap, !Constraints) :-
-
- % XXX Currently the constraints simply say that if a
- % variable is bound at a disjunct it is bound at the
- % disjunction by making the relevant variables
- % equivalent. Setting GoalPathOptimisation to yes will
- % cause the disjucts to be given the same path as the
- % disjunction, so that the relevant constraint variables
- % will not need to be constrained equivalent - they will
- % be the same variable. It will do the same for other
- % path types with similar equivalence constraints -
- % refer to the goal_path module for a more detailed
- % description.
- GoalPathOptimisation = no,
-
- % XXX If we want the goal path info to be retained, then
- % ModuleInfo needs to be a state variable and to be
- % updated with the new PredInfo, but for now, this will
- % do.
+process_pred(ModuleInfo, PredId, !PredInfo, !VarInfo, !Constraints) :-
goal_path.fill_slots_in_clauses(ModuleInfo, GoalPathOptimisation,
- PredInfo0, PredInfo),
+ !PredInfo),
- pred_info_procedures(PredInfo, ProcTable),
- % Needed for defined modes.
- pred_info_clauses_info(PredInfo, ClausesInfo),
- clauses_info_headvars(ClausesInfo, HeadVars),
- clauses_info_clauses_only(ClausesInfo, Clauses),
- clauses_info_varset(ClausesInfo, ProgVarset),
- Goals = list.map((func(clause(_, ClauseBody, _, _)) = ClauseBody),
- Clauses),
-
- % Here build goal constraint vars.
- list.foldl2(add_mc_vars_for_goal(PredId, ProgVarset),
- Goals, !Varset, !VarMap),
-
- % Here check for mode declarations and add apppropriate
- % constraints.
- map.values(ProcTable, ProcInfos),
-
- list.filter_map(
- (pred(ProcInfo::in, (ProcHVars - ArgModes)::out) is semidet :-
- proc_info_maybe_declared_argmodes(
- ProcInfo,
- yes(_OriginalArgModes)
- ),
- proc_info_argmodes(ProcInfo, ArgModes),
- proc_info_headvars(ProcInfo, ProcHVars)
-% add_sufficient_in_modes_for_type_info_args(
-% ProcHVars, ArgModes0, ArgModes
-% ) % XXX type_info args should be at the
- % start and should be 'in' so that is
- % what this predicate adds however, I am
- % not happy with it.
- ),
- ProcInfos,
- HeadVarArgModesPairs
- ),
%
- % Pair up the any existing arg mode declarations with
- % their corresponding head variables from the proc_infos.
+ % If mode inference requested, just add constraints for the clause body,
+ % otherwise, process the predicate for each of the procedures.
%
- (
- HeadVarArgModesPairs = [], % No declared modes, no constraints
- ModeDeclConstraints = []
- ;
- HeadVarArgModesPairs = [_|_], % Some declared modes
- mode_decls_constraints(ModuleInfo, !.VarMap, PredId,
- list.map(snd, HeadVarArgModesPairs),
- list.map(fst, HeadVarArgModesPairs),
- ModeDeclConstraints)
- ),
- %
- % This builds the constraints for this predicate. Note
- % that the main goal may need to be temporarily formed
- % by putting clauses into a disjunction. The goal paths
- % added by goal_path.fill_slots_in_clauses reflect this
- % disjunction.
- %
- (
- Goals = [],
- GoalConstraints = []
- % If the clause list is empty, then there are no
- % goals to produce constraints for.
+ ( pred_info_infer_modes(!.PredInfo) ->
+ add_clauses_constraints(ModuleInfo, PredId, !.PredInfo, !VarInfo,
+ abstract_mode_constraints.init, BodyConstraints),
+ svmap.set(PredId, BodyConstraints, !Constraints)
;
- Goals = [_| _],
- MainGoal = disj(Goals),
- MainGoalPath = [],
- Nonlocals = set.list_to_set(HeadVars),
- goal_expr_constraints(ModuleInfo, !.VarMap, PredId, MainGoal,
- MainGoalPath, Nonlocals, GoalConstraints)
+ process_mode_declared_pred(ModuleInfo, PredId, !.PredInfo,
+ !VarInfo, !Constraints)
),
- PredConstraints = list.append(ModeDeclConstraints, GoalConstraints),
- svmap.det_insert(PredId, PredConstraints, !Constraints).
+
+ % XXX Currently the constraints simply say that if a
+ % variable is bound at a disjunct it is bound at the
+ % disjunction by making the relevant variables
+ % equivalent. Setting GoalPathOptimisation to yes will
+ % cause the disjucts to be given the same path as the
+ % disjunction, so that the relevant constraint variables
+ % will not need to be constrained equivalent - they will
+ % be the same variable. It will do the same for other
+ % path types with similar equivalence constraints -
+ % refer to the goal_path module for a more detailed
+ % description.
+ GoalPathOptimisation = no.
+
+ % process_mode_declared_pred(ModuleInfo, PredId, PredInfo, !VarInfo,
+ % !PredConstraintsMap)
+ %
+ % Uses the clauses and mode declarations in PredInfo (which should
+ % be for predicate PredId taken from ModuleInfo) to create
+ % producer/consumer constraints for program variables in predicate
+ % PredId and stores them in PredConstraintsMap. VarInfo is updated
+ % with any constraint variables used.
+ %
+:- pred process_mode_declared_pred(module_info::in, pred_id::in,
+ pred_info::in, mc_var_info::in, mc_var_info::out,
+ pred_constraints_map::in, pred_constraints_map::out)
+ is det.
+
+process_mode_declared_pred(ModuleInfo, PredId, PredInfo, !VarInfo,
+ !PredConstraintsMap) :-
+
+ ProcIds = pred_info_all_procids(PredInfo),
+
+ add_clauses_constraints(ModuleInfo, PredId, PredInfo, !VarInfo,
+ abstract_mode_constraints.init, BodyConstr),
+
+ % Store procedure specific constraints in the constraints structure
+ list.map(pred_info_proc_info(PredInfo), ProcIds, ProcInfos),
+ list.foldl2_corresponding(
+ process_mode_declared_proc(ModuleInfo, PredId),
+ ProcIds, ProcInfos, !VarInfo, BodyConstr, FullConstraints),
+
+ svmap.set(PredId, FullConstraints, !PredConstraintsMap).
+
+ % process_mode_declared_proc(ModuleInfo, PredId, ProcId,
+ % ProcInfo, !VarInfo, !PredConstraints)
+ %
+ % Adds constraints based on the mode declaration in
+ % ProcInfo to PredConstraints structure, associating them
+ % specifically with ProcId. Relies on the constraint variables
+ % associated with the head variables of PredId at the empty goal
+ % path being stored in VarInfo.
+ %
+:- pred process_mode_declared_proc(module_info::in,
+ pred_id::in, proc_id::in, proc_info::in, mc_var_info::in,
+ mc_var_info::out, mode_constraints::in, mode_constraints::out) is det.
+
+process_mode_declared_proc(ModuleInfo, PredId, ProcId, ProcInfo, !VarInfo,
+ !PredConstraints) :-
+
+ proc_info_argmodes(ProcInfo, ArgModes),
+ proc_info_headvars(ProcInfo, Args),
+
+ add_mode_decl_constraints(ModuleInfo, PredId, ProcId, ArgModes, Args,
+ !VarInfo, !PredConstraints).
+
+module_info_pred_status_is_imported(ModuleInfo, PredId) :-
+ module_info_pred_info(ModuleInfo, PredId, PredInfo),
+
+ % The following used because pred_info_is_imported/2 is not
+ % as comprehensive as status_is_imported/2.
+ pred_info_import_status(PredInfo, Status),
+ status_is_imported(Status, yes).
+
+%----------------------------------------------------------------------------%
% Put the constraints to the current output stream in human
% readable format. It titles each pred's constraints with a
@@ -255,14 +255,9 @@
ModuleInfo, ConstraintVarset, PredConstraintsMap, !IO) :-
ConstrainedPreds = map.keys(PredConstraintsMap),
list.foldl(
- pretty_print_pred_constraints(
- ModuleInfo,
- ConstraintVarset,
- PredConstraintsMap
- ),
- ConstrainedPreds,
- !IO
- ).
+ pretty_print_pred_constraints(ModuleInfo, ConstraintVarset,
+ PredConstraintsMap),
+ ConstrainedPreds, !IO).
% Puts the constraints for the specified predicate from the
% pred_constraints_map to the current output stream in human
@@ -273,21 +268,40 @@
pretty_print_pred_constraints(ModuleInfo, ConstraintVarset,
PredConstraintsMap, PredId, !IO) :-
- io.write_string("\nConstraints for pred ", !IO),
+ % Start with a blank line.
+ write_error_pieces_plain([fixed("")], !IO),
+
hlds_module.module_info_pred_info(ModuleInfo, PredId, PredInfo),
- ModuleName = hlds_pred.pred_info_module(PredInfo),
- PredName = hlds_pred.pred_info_name(PredInfo),
- CreateDirectories = no,
- parse_tree.modules.module_name_to_file_name(
- ModuleName, "." ++ PredName,
- CreateDirectories,
- FullPredNameString, !IO
- ),
- io.write_string(FullPredNameString ++ ":\n", !IO),
+ write_error_pieces_plain([words("Constraints for")] ++
+ describe_one_pred_info_name(should_module_qualify, PredInfo) ++
+ [suffix(":")], !IO),
map.lookup(PredConstraintsMap, PredId, PredConstraints),
- abstract_mode_constraints.pretty_print_constraints(ConstraintVarset,
- PredConstraints, !IO).
+ FormulaeAndAnnotations = pred_constraints_to_formulae_and_annotations(
+ PredConstraints),
+ abstract_mode_constraints.dump_constraints_and_annotations(
+ ConstraintVarset, FormulaeAndAnnotations, !IO),
+ list.foldl(pretty_print_proc_constraints(ModuleInfo, ConstraintVarset,
+ PredConstraints, PredId), pred_info_all_procids(PredInfo), !IO).
+
+ % Puts the constraints specific to the procedure indicated from
+ % the pred_p_c_constraints to the current output stream in human
+ % readable format.
+ %
+:- pred pretty_print_proc_constraints(module_info::in, mc_varset::in,
+ pred_p_c_constraints::in, pred_id::in, proc_id::in, io::di, io::uo) is det.
+
+pretty_print_proc_constraints(ModuleInfo, ConstraintVarset, PredConstraints,
+ PredId, ProcId, !IO) :-
+ % Start with a blank line.
+ write_error_pieces_plain([fixed("")], !IO),
+
+ write_error_pieces_plain(describe_one_proc_name(ModuleInfo,
+ should_module_qualify, proc(PredId, ProcId)) ++ [suffix(":")], !IO),
+ FormulaeAndAnnotations =
+ proc_constraints_to_formulae_and_annotations(ProcId, PredConstraints),
+ abstract_mode_constraints.dump_constraints_and_annotations(
+ ConstraintVarset, FormulaeAndAnnotations, !IO).
%----------------------------------------------------------------------------%
:- end_module prop_mode_constraints.
Index: compiler/ordering_mode_constraints.m (new file)
===================================================================
%-----------------------------------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et
%-----------------------------------------------------------------------------%
% Copyright (C) 2005 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.
%-----------------------------------------------------------------------------%
% File: ordering_mode_constraints.m.
% Main author: richardf.
% This module contains code for ordering conjuncts in a predicate
% according to variable producer consumer relationships and
% other mode analysis constraints.
%-----------------------------------------------------------------------------%
:- module check_hlds.ordering_mode_constraints.
:- interface.
:- import_module check_hlds.build_mode_constraints.
:- import_module check_hlds.prop_mode_constraints.
:- import_module hlds.hlds_pred.
:- import_module hlds.hlds_module.
:- import_module int.
:- import_module io.
:- import_module list.
:- import_module set.
%-----------------------------------------------------------------------------%
% Original position in a conjunction. Count starts at one.
%
:- type conjunct_id == int.
:- type mode_ordering_constraints == list(mode_ordering_constraint).
% Mode ordering constraints.
%
:- type mode_ordering_constraint
---> lt(
first :: conjunct_id, % Typically the producer
second :: conjunct_id % Typically the consumer
).
% Store for the ordering constraints for one conjunction.
%
:- type ordering_constraints_info --->
ordering_constraints_info(
num_conjuncts :: int,
% The number of conjucts in this conjunction
constraints :: set(mode_ordering_constraint)
% Constraints on the conjuncts.
).
%-----------------------------------------------------------------------------%
% mode_reordering(Constraints, VarMap, SCCs, !ModuleInfo) orders
% conjunctions for each predicate in SCCs in the ModuleInfo
% according to the modes implied by the producer/consumer
% constraints in Constraints. All constraint variables relevant to
% the predicates in SCCs should be stored in the VarMap.
%
:- pred mode_reordering(pred_constraints_map::in, mc_var_map::in,
list(list(pred_id))::in, module_info::in, module_info::out) is cc_multi.
% dump_goal_paths(ModuleInfo, PredIds, !IO)
%
% Dumps the goal paths of each goal in the order they appear for each
% predicate in PredIds for the purposes of visually checking re-ordering.
%
:- pred dump_goal_paths(module_info::in, list(pred_id)::in, io::di, io::uo)
is det.
%-----------------------------------------------------------------------------%
% ordering_init(N) creates a new ordering constraint system for
% a conjunction with N conjuncts.
%
:- func ordering_init(int) = ordering_constraints_info.
% add_ordering_constraint(Constraint, !OCI) adds Constraint
% to the ordering constraints store. It fails if it immediately
% detects a contradiction (at the moment, this means it has
% detected a loop in the producer/consumer dependency graph).
%
:- pred add_ordering_constraint(mode_ordering_constraint::in,
ordering_constraints_info::in, ordering_constraints_info::out) is semidet.
% add_lt_constraint(A, B, !OCI) constrains conjunct A to come
% before conjunct B, in the constraints store.
%
:- pred add_lt_constraint(conjunct_id::in, conjunct_id::in,
ordering_constraints_info::in, ordering_constraints_info::out) is semidet.
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
:- implementation.
:- import_module check_hlds.abstract_mode_constraints.
:- import_module check_hlds.clause_to_proc.
:- import_module check_hlds.mcsolver.
:- import_module hlds.hlds_error_util.
:- import_module hlds.hlds_goal.
:- import_module libs.compiler_util.
:- import_module mdbcomp.prim_data.
:- import_module parse_tree.error_util.
:- import_module parse_tree.prog_data.
:- import_module bimap.
:- import_module bool.
:- import_module std_util.
:- import_module string.
:- import_module multi_map.
:- import_module map.
:- import_module svset.
%-----------------------------------------------------------------------------%
% A map from program variables to related producer/consumer
% constraint variables' abstract representations. The constraint
% variables should each represent the proposition that the
% program variable is produced at some particular conjunct, all
% in the one conjunction.
%
:- type prog_var_at_conjuncts_map == multi_map(prog_var, mc_rep_var).
%-----------------------------------------------------------------------------%
%
% Predicate reordering
%
mode_reordering(PredConstraintsMap, VarMap, SCCs, !ModuleInfo) :-
(
list.foldl(scc_reordering(PredConstraintsMap, VarMap), SCCs,
!ModuleInfo)
->
true
;
% XXX Until mode inference is complete and the final
% structure of this module is decided this is all that
% can be done.
sorry(this_file, "mode ordering failure")
).
% scc_reording(PredConstraintsMap, VarMap, SCC, !ModuleInfo)
%
% Copies the clauses of predicates in SCC into the body goal of their
% procedures and performs conjunction reordering according to the
% producer consumer constraints in PredConstraintsMap.
%
:- pred scc_reordering(pred_constraints_map::in, mc_var_map::in,
list(pred_id)::in, module_info::in, module_info::out) is nondet.
scc_reordering(PredConstraintsMap, VarMap, SCC0, !ModuleInfo) :-
% Process only predicates from this module
list.filter(module_info_pred_status_is_imported(!.ModuleInfo),
SCC0, _, SCC),
list.filter(
(pred(PredID::in) is semidet :-
module_info_pred_info(!.ModuleInfo, PredID, PredInfo),
pred_info_infer_modes(PredInfo)
), SCC, PredsToInfer, PredsToCheck),
( PredsToInfer \= [] ->
% XXX GIVE UP FOR NOW!!!!
sorry(this_file, "mode inference")
;
true
),
list.foldl(pred_reordering(PredConstraintsMap, VarMap), PredsToCheck,
!ModuleInfo).
% pred_reordering(PredConstraintsMap, VarMap, PredID, !ModuleInfo)
% applies mode reordering to conjunctions in the body goal of the
% predicate PredID for each procedure in that predicate.
%
:- pred pred_reordering(pred_constraints_map::in, mc_var_map::in,
pred_id::in, module_info::in, module_info::out) is nondet.
pred_reordering(PredConstraintsMap, VarMap, PredID, !ModuleInfo) :-
module_info_pred_info(!.ModuleInfo, PredID, PredInfo0),
( pred_info_infer_modes(PredInfo0) ->
% XXX GIVE UP FOR NOW!!!! In reality, execution shouldn't
% reach here if the pred is to be mode inferred, should it?
sorry(this_file, "mode inference constraints")
;
% XXX Maybe move this outside of this predicate - then
% the predicate can assume that the correct procedures
% have been created and that they have the correct bodies.
copy_module_clauses_to_procs([PredID], !ModuleInfo),
module_info_pred_info(!.ModuleInfo, PredID, PredInfo1),
PredConstraints = map.lookup(PredConstraintsMap, PredID),
ProcIDs = pred_info_all_procids(PredInfo1),
list.foldl(proc_reordering(PredConstraints, VarMap, PredID), ProcIDs,
PredInfo1, PredInfo),
module_info_set_pred_info(PredID, PredInfo, !ModuleInfo)
).
% proc_reordering(PredConstraints, VarMap, PredID, ProcID, !PredInfo)
%
% Orders conjunctions in procedure ProcID of predicate PredID, according
% to the producer consumer constraints in PredConstraints. The procedure
% with the modified body goal replaces its original in PredInfo.
%
:- pred proc_reordering(pred_p_c_constraints::in, mc_var_map::in, pred_id::in,
proc_id::in, pred_info::in, pred_info::out) is nondet.
proc_reordering(PredConstraints, VarMap, PredID, ProcID, !PredInfo) :-
pred_info_proc_info(!.PredInfo, ProcID, ProcInfo0),
proc_info_goal(ProcInfo0, Goal0),
ConstraintFormulae = pred_constraints_to_formulae(ProcID, PredConstraints),
PrepConstraints0 = new_prep_cstrts,
prepare_abstract_constraints(ConstraintFormulae, PrepConstraints0,
PrepConstraints1),
SolverConstraints = make_solver_cstrts(PrepConstraints1),
mcsolver.solve(SolverConstraints, Bindings),
goal_reordering(PredID, VarMap, Bindings, Goal0, Goal),
proc_info_set_goal(Goal, ProcInfo0, ProcInfo),
pred_info_set_proc_info(ProcID, ProcInfo, !PredInfo).
%-----------------------------------------------------------------------------%
%
% Conjunction reordering
%
% goal_reordering(PredID, VarMap, Bindings, !Goal) applies mode
% reordering to conjunctions in Goal (from predicate PredID) and its
% children. VarMap should contain all producer/consumer constraint
% variables relevant to said conjunctions, and Bindings should
% contain bindings for them.
%
:- pred goal_reordering(pred_id::in, mc_var_map::in, mc_bindings::in,
hlds_goal::in, hlds_goal::out) is semidet.
goal_reordering(PredID, VarMap, Bindings, GoalExpr0 - GoalInfo,
GoalExpr - GoalInfo) :-
goal_expr_reordering(PredID, VarMap, Bindings, GoalExpr0, GoalExpr).
% goal_expr_reordering(PredID, VarMap, Bindings, !GoalExpr) applies
% mode reordering to conjunctions in GoalExpr (from predicate
% PredID) and its children. VarMap should contain all
% producer/consumer constraint variables relevant to said
% conjunctions, and Bindings should contain bindings for them.
%
:- pred goal_expr_reordering(pred_id::in, mc_var_map::in, mc_bindings::in,
hlds_goal_expr::in, hlds_goal_expr::out) is semidet.
goal_expr_reordering(PredID, VarMap, Bindings, conj(Goals0), conj(Goals)) :-
% Build constraints for this conjunction.
make_conjuncts_nonlocal_repvars(PredID, Goals0, RepVarMap),
conjunct_ordering_constraints(VarMap, Bindings, RepVarMap,
ordering_init(list.length(Goals0)), OrderingConstraintsInfo),
% Then solve the constraints and reorder.
minimum_reordering(OrderingConstraintsInfo, Order),
list.map(list.index1_det(Goals0), Order, Goals1),
% Then recurse on the reordered goals
list.map(goal_reordering(PredID, VarMap, Bindings), Goals1, Goals).
% goal_expr_reordering for atomic goals, and ones that shouldn't
% exist yet.
%
goal_expr_reordering(_PredID, _VarMap, _Bindings, GoalExpr, GoalExpr) :-
(
GoalExpr = call(_, _, _, _, _, _)
;
GoalExpr = generic_call(_, _, _, _)
;
GoalExpr = unify(_, _, _, _, _)
;
GoalExpr = foreign_proc(_, _, _, _, _, _)
;
GoalExpr = shorthand(_),
unexpected(this_file, "shorthand goal")
;
GoalExpr = switch(_, _, _),
unexpected(this_file, "switch")
).
goal_expr_reordering(PredID, VarMap, Bindings, disj(Goals0), disj(Goals)) :-
list.map(goal_reordering(PredID, VarMap, Bindings), Goals0, Goals).
goal_expr_reordering(PredID, VarMap, Bindings, not(Goal0), not(Goal)) :-
goal_reordering(PredID, VarMap, Bindings, Goal0, Goal).
goal_expr_reordering(PredID, VarMap, Bindings, scope(Reason, Goal0),
scope(Reason, Goal)) :-
goal_reordering(PredID, VarMap, Bindings, Goal0, Goal).
goal_expr_reordering(PredID, VarMap, Bindings,
if_then_else(Vars, If0, Then0, Else0),
if_then_else(Vars, If, Then, Else)) :-
goal_reordering(PredID, VarMap, Bindings, If0, If),
goal_reordering(PredID, VarMap, Bindings, Then0, Then),
goal_reordering(PredID, VarMap, Bindings, Else0, Else).
goal_expr_reordering(PredID, VarMap, Bindings, par_conj(Goals0),
par_conj(Goals)) :-
list.map(goal_reordering(PredID, VarMap, Bindings), Goals0, Goals).
%-----------------------------------------------------------------------------%
% ordering_init(N) creates a new ordering constraint system for
% a conjunction with N conjuncts.
%
ordering_init(N) = ordering_constraints_info(N, set.init).
%-----------------------------------------------------------------------------%
% add_ordering_constraint(Constraint, OCI0, OCI) adds Constraint
% to the ordering constraints store. It fails if it immediately
% detects a contradiction (at the moment, this means it has
% detected a loop in the producer consumer dependency graph - eg
% the conjunction:
% (p(A, B), p(B, C), p(C, A)) where p is pred(in, out)).
%
% NOTE: behaviour when constrained conjuncts are outside the
% possible range is undefined.
%
add_ordering_constraint(Constraint, !OCI) :-
( set.member(Constraint, !.OCI ^ constraints) ->
true
;
constraint_transitive_closure(!.OCI, Constraint, NewConstraints),
% No cycles. (lt(X, X) is a contradiction)
set.empty(set.filter(pred(lt(X, X)::in) is semidet, NewConstraints)),
!:OCI = !.OCI ^ constraints :=
set.union(NewConstraints, !.OCI ^ constraints)
).
% constraint_transitive_closure(OCI, Constraint, NewConstraints)
% returns a list of constraints in NewConstraints containing
% Constraint itself, and also all constraints which must be added to
% OCI to maintain a transitive closure of partial ordering
% constraints.
%
:- pred constraint_transitive_closure(ordering_constraints_info::in,
mode_ordering_constraint::in, set(mode_ordering_constraint)::out) is det.
constraint_transitive_closure(OCI, Constraint, NewConstraints) :-
Constraints = OCI ^ constraints,
Constraint = lt(From, To),
ComesBefore = set.filter_map(
func(lt(B, F)::in) = (B::out) is semidet :- F = From, Constraints),
ComesAfter = set.filter_map(
func(lt(T, A)::in) = (A::out) is semidet :- T = To, Constraints),
% Each conjunct in the ComesBefore set and the From conjunct must
% precede the To conjunct and each of the conjuncts in the
% ComesAfter set.
set.fold(insert_lt_constraints(set.insert(ComesAfter, To)),
set.insert(ComesBefore, From), set.init, NewConstraints).
% insert_lt_constraints(Bs, A, !Cs) adds a lt(A, B) constraint to
% the set of constraints Cs for each conjunct_id B in set Bs.
% Note the reversed order of Bs and A.
%
:- pred insert_lt_constraints(set(conjunct_id)::in, conjunct_id::in,
set(mode_ordering_constraint)::in, set(mode_ordering_constraint)::out)
is det.
insert_lt_constraints(Bs, A, !Cs) :-
set.fold(insert_lt_constraint(A), Bs, !Cs).
% insert_lt_constraint(A, B, !Cs) adds a lt(A, B) constraint to the set
% of constraints.
%
:- pred insert_lt_constraint(conjunct_id::in, conjunct_id::in,
set(mode_ordering_constraint)::in, set(mode_ordering_constraint)::out)
is det.
insert_lt_constraint(A, B, !Cs) :-
svset.insert(lt(A, B), !Cs).
%-----------------------------------------------------------------------------%
add_lt_constraint(A, B, !OCI) :-
add_ordering_constraint(lt(A, B), !OCI).
%-----------------------------------------------------------------------------%
% make_conjuncts_nonlocal_repvars(PredID, Goals, RepvarMap)
%
% The keys of RepvarMap are the program variables nonlocal
% to Goals. Each is mapped to the mc_rep_var representation
% of the proposition that it is produced at a Goal for every
% Goal it is nonlocal to in Goals.
%
:- pred make_conjuncts_nonlocal_repvars(pred_id::in, hlds_goals::in,
prog_var_at_conjuncts_map::out) is det.
make_conjuncts_nonlocal_repvars(PredID, Goals, RepvarMap) :-
list.foldl(make_conjunct_nonlocal_repvars(PredID), Goals,
multi_map.init, RepvarMap).
% See make_conjuncts_nonlocal_repvars; acts on a single conjunct.
%
:- pred make_conjunct_nonlocal_repvars(pred_id::in, hlds_goal::in,
prog_var_at_conjuncts_map::in,
prog_var_at_conjuncts_map::out) is det.
make_conjunct_nonlocal_repvars(PredID, Goal, !RepvarMap) :-
GoalInfo = snd(Goal),
goal_info_get_nonlocals(GoalInfo, NonLocals),
goal_info_get_goal_path(GoalInfo, GoalPath),
set.fold(
(pred(NL::in, RMap0::in, RMap::out) is det :-
multi_map.set(RMap0, NL, NL `in` PredID `at` GoalPath, RMap)
),
NonLocals, !RepvarMap).
%-----------------------------------------------------------------------------%
% conjunct_ordering_constraints(VarMap, Bindings, RepVarMap, !OCInfo)
%
% Adds ordering constraints based on producer/consumer analysis of
% variables nonlocal to conjuncts in a single conjunction, to the
% OCInfo.
%
% For the conjunction in question, RepVarMap should contain any
% program variable nonlocal to any conjunct. The program variables
% should be mapped to any constraint variable concerning them
% related to any of the conjuncts in the conjunction. (Actually,
% they will be mapped to an abstract rep_var representing this
% constraint variable, and the VarMap is required to look up
% the constraint variable using the rep_var.) Bindings should
% contain bindings for all such constraint variables.
%
:- pred conjunct_ordering_constraints(mc_var_map::in, mc_bindings::in,
prog_var_at_conjuncts_map::in, ordering_constraints_info::in,
ordering_constraints_info::out) is semidet.
conjunct_ordering_constraints(VarMap, Bindings, RepVarMap, !OCInfo) :-
map.foldl(prog_var_ordering_constraints(VarMap, Bindings),
RepVarMap, !OCInfo).
% prog_var_ordering_constraints(VarMap, Bindings, ProgVar, RepVars,
% !OCInfo)
%
% Adds ordering constraints for a conjunction to OCInfo.
% Specifically, those relating to which conjuncts produce and which
% consume the variable ProgVar. See conjunct_ordering_constraints
% for details.
%
:- pred prog_var_ordering_constraints(mc_var_map::in, mc_bindings::in,
prog_var::in, list(mc_rep_var)::in,
ordering_constraints_info::in, ordering_constraints_info::out) is semidet.
prog_var_ordering_constraints(VarMap, Bindings, _ProgVar, RepVars, !OCInfo) :-
list.filter(produced_at_path(VarMap, Bindings), RepVars,
ProgVarAtProducers, ProgVarAtConsumers),
(
ProgVarAtProducers = [] % Variable not produced here
% - no constraints.
;
ProgVarAtProducers = [RepVar], % Should be only one producer
First = get_position_in_conj(RepVar),
list.map(get_position_in_conj, ProgVarAtConsumers, Laters),
list.foldl(add_lt_constraint(First), Laters, !OCInfo)
).
% produced_at_path(VarMap, Bindings, ProgVar `at` GoalPath `in` _)
% succeeds if ProgVar is produced at GoalPath, according to the
% solution to the producer/consumer constraint solutions in Bindings.
%
:- pred produced_at_path(mc_var_map::in, mc_bindings::in, mc_rep_var::in)
is semidet.
produced_at_path(VarMap, Bindings, RepVar) :-
map.lookup(Bindings, bimap.lookup(VarMap, RepVar)) = yes.
% get_position_in_conj(RepVar) fails if the deepest level of the
% goalpath in RepVar is not a conjunction, otherwise it returns
% the number of the conjunct the RepVar refers to.
%
:- func get_position_in_conj(mc_rep_var::in) = (conjunct_id::out) is semidet.
get_position_in_conj(_ProgVar `in` _PredID `at` [conj(N) | _]) = N.
% Predicate version of get_position_in_conj
%
:- pred get_position_in_conj(mc_rep_var::in, conjunct_id::out) is semidet.
get_position_in_conj(RepVar, ConjID) :-
ConjID = get_position_in_conj(RepVar).
%-----------------------------------------------------------------------------%
% minimum_reordering(OCI, Order)
%
% Order is a minimum re-ordering of conjuncts, conforming to the
% constraints in OCI. The values of the conjunct_ids returned represent
% the original position of a conjunct, the position of the conjunct_id
% in the Order represents the new position of the conjunct.
%
% Fails if no reordering conforms with the constraints.
%
:- pred minimum_reordering(ordering_constraints_info::in,
list(conjunct_id)::out) is semidet.
minimum_reordering(OCI, Order) :-
% % Heavy handed - a topological sort can more easily be used to
% % achieve minimum reordering.
% original_order_constraints(OCI ^ num_conjuncts, OriginalOrderConstraints),
% constrain_if_possible(OriginalOrderConstraints, OCI0, OCI1),
Conjuncts = set.from_sorted_list(1 `..` OCI ^ num_conjuncts),
topological_sort_min_reordering(OCI ^ constraints, Conjuncts, Order).
% original_order_constraints(N, MOCs) produces a list of constraints MOCs
% that describe a complete order for N conjuncts, such that they are not
% reordered at all from their original positions.
%
:- pred original_order_constraints(int::in,
mode_ordering_constraints::out) is det.
original_order_constraints(N, MOCs) :-
complete_order_constraints(1 `..` N, MOCs).
% complete_order_constraints(Xs) produces a list of constraints
% that describe a compete order for Xs such that it is not reordered
% at all.
%
:- pred complete_order_constraints(list(conjunct_id)::in,
mode_ordering_constraints::out) is det.
complete_order_constraints(Xs, MOCs) :-
add_complete_order_constraints(Xs, set.init, MOCs0),
MOCs = set.to_sorted_list(MOCs0).
% add_complete_order_constraints(Xs, !MOCs) adds a list of constraints
% that describe a compete order for Xs such that it is not reordered
% at all.
%
:- pred add_complete_order_constraints(list(conjunct_id)::in,
set(mode_ordering_constraint)::in,
set(mode_ordering_constraint)::out) is det.
add_complete_order_constraints([], !MOCs).
add_complete_order_constraints([Conjunct | Conjuncts], !MOCs) :-
list.foldl(insert_lt_constraint(Conjunct), Conjuncts, !MOCs),
add_complete_order_constraints(Conjuncts, !MOCs).
% constraint_if_possible(Constraints, !OCI)
%
% Adds the given Constraints to the constraints info OCI, but only
% if no direct contradiction is found.
%
:- pred constrain_if_possible(mode_ordering_constraints::in,
ordering_constraints_info::in, ordering_constraints_info::out) is det.
constrain_if_possible([] , !OCI).
constrain_if_possible([Constraint | Constraints], !OCI) :-
( add_ordering_constraint(Constraint, !OCI) ->
constrain_if_possible(Constraints, !OCI)
;
constrain_if_possible(Constraints, !OCI)
).
%-----------------------------------------------------------------------------%
% topological_sort_min_reordering(Constraints, Conjuncts, Ordering)
%
% Succeeds if Ordering is a minimum re-ordering of Conjuncts
% consistent with the system of Constraints.
%
:- pred topological_sort_min_reordering(set(mode_ordering_constraint)::in,
set(conjunct_id)::in, list(conjunct_id)::out) is semidet.
topological_sort_min_reordering(Constraints0, Conjuncts0, Ordering) :-
NotFirst = set.map(func(lt(_From, To)) = To, Constraints0),
CantidatesForFirst = set.difference(Conjuncts0, NotFirst),
( set.remove_least(CantidatesForFirst, First, _) ->
% Remove First from the system.
set.remove(Conjuncts0, First, Conjuncts),
Constraints = set.filter(
(pred(lt(From, _To)::in) is semidet :- From \= First),
Constraints0),
% Order the rest, then put First at the head.
topological_sort_min_reordering(Constraints, Conjuncts, Ordering0),
Ordering = [First | Ordering0]
;
% No cantidates for First, so we are only done if there
% were no nodes (conjuncts) left to begin with.
set.empty(Conjuncts0),
Ordering = []
).
%-----------------------------------------------------------------------------%
dump_goal_paths(ModuleInfo, PredIds0, !IO) :-
% Process only predicates from this module
list.filter(module_info_pred_status_is_imported(ModuleInfo),
PredIds0, _, PredIds),
list.foldl(dump_pred_goal_paths(ModuleInfo), PredIds, !IO).
% dump_pred_goal_paths(ModuleInfo, PredId, !IO)
%
% Dumps the goal paths of each goal in the order they appear for
% predicate PredId for the purposes of visually checking re-ordering.
%
:- pred dump_pred_goal_paths(module_info::in, pred_id::in, io::di, io::uo)
is det.
dump_pred_goal_paths(ModuleInfo, PredId, !IO) :-
module_info_pred_info(ModuleInfo, PredId, PredInfo),
pred_info_procedures(PredInfo, ProcTable),
ProcIds = map.keys(ProcTable),
% Start with a blank line
write_error_pieces_plain([fixed("")], !IO),
PredHeaderFormat = [words("Goal paths for")] ++
describe_one_pred_info_name(should_module_qualify, PredInfo) ++
[suffix("."), nl],
write_error_pieces_plain(PredHeaderFormat, !IO),
(
ProcIds = [],
pred_info_clauses_info(PredInfo, ClausesInfo),
clauses_info_clauses_only(ClausesInfo, Clauses),
Goals = list.map(func(Clause) = clause_body(Clause), Clauses),
Indent = 0,
list.foldl(dump_goal_goal_paths(Indent), Goals, !IO)
;
ProcIds = [_ | _],
list.foldl(dump_proc_goal_paths(ProcTable), ProcIds, !IO)
).
% dump_proc_goal_paths(ProcTable, ProcId, !IO)
%
% Dumps the goal paths of each goal in the order they appear for
% procedure ProcId for the purposes of visually checking re-ordering.
%
:- pred dump_proc_goal_paths(proc_table::in, proc_id::in, io::di, io::uo)
is det.
dump_proc_goal_paths(ProcTable, ProcId, !IO) :-
ProcIdString = string.from_int(proc_id_to_int(ProcId)),
ProcHeaderFormat = [words("mode"), words(ProcIdString),
suffix(":")],
write_error_pieces_plain(ProcHeaderFormat, !IO),
map.lookup(ProcTable, ProcId, ProcInfo),
proc_info_goal(ProcInfo, Goal),
Indent = 0,
dump_goal_goal_paths(Indent, Goal, !IO).
% dump_goal_goal_paths(Indent, Goal, !IO)
%
% Dumps the goal paths for this goal at the indent depth Indent, then
% recurses for each sub-goal at one further level of indent,
% in the order they appear, for the purposes of visually checking
% re-ordering.
%
:- pred dump_goal_goal_paths(int::in, hlds_goal::in, io::di, io::uo)
is det.
dump_goal_goal_paths(Indent, GoalExpr - GoalInfo, !IO) :-
goal_info_get_goal_path(GoalInfo, GoalPath),
goal_path_to_string(GoalPath, GoalPathString),
GoalPathFormat = [words(GoalPathString), nl],
write_error_pieces_maybe_with_context(no, Indent, GoalPathFormat, !IO),
dump_goal_expr_goal_paths(Indent+1, GoalExpr, !IO).
% dump_goal_expr_goal_paths(Indent, GoalExpr, !IO)
%
% Dumps the goal paths for each sub-goal in GoalExpr at level of indent
% Indent, in the order they appear, and for each of their sub-goals in
% turn, for the purposes of visually checking reordering.
%
:- pred dump_goal_expr_goal_paths(int::in, hlds_goal_expr::in, io::di, io::uo)
is det.
dump_goal_expr_goal_paths(_Indent, GoalExpr, !IO) :-
%
% Do nothing for atomic goals.
%
(
GoalExpr = call(_, _, _, _, _, _)
;
GoalExpr = generic_call(_, _, _, _)
;
GoalExpr = unify(_, _, _, _, _)
;
GoalExpr = foreign_proc(_, _, _, _, _, _)
).
dump_goal_expr_goal_paths(_Indent, GoalExpr, !IO) :-
%
% Call unexpected/2 for unexpected goals.
%
(
GoalExpr = switch(_, _, _),
unexpected(this_file, "switch")
;
GoalExpr = shorthand(_),
unexpected(this_file, "shorthand")
).
dump_goal_expr_goal_paths(Indent, GoalExpr, !IO) :-
GoalExpr = conj(Goals),
list.foldl(dump_goal_goal_paths(Indent), Goals, !IO).
dump_goal_expr_goal_paths(Indent, GoalExpr, !IO) :-
GoalExpr = disj(Goals),
list.foldl(dump_goal_goal_paths(Indent), Goals, !IO).
dump_goal_expr_goal_paths(Indent, GoalExpr, !IO) :-
GoalExpr = not(Goal),
dump_goal_goal_paths(Indent, Goal, !IO).
dump_goal_expr_goal_paths(Indent, GoalExpr, !IO) :-
GoalExpr = scope(_, Goal),
dump_goal_goal_paths(Indent, Goal, !IO).
dump_goal_expr_goal_paths(Indent, GoalExpr, !IO) :-
GoalExpr = if_then_else(_, IfGoal, ThenGoal, ElseGoal),
Goals = [IfGoal, ThenGoal, ElseGoal],
list.foldl(dump_goal_goal_paths(Indent), Goals, !IO).
dump_goal_expr_goal_paths(Indent, GoalExpr, !IO) :-
GoalExpr = par_conj(Goals),
list.foldl(dump_goal_goal_paths(Indent), Goals, !IO).
%-----------------------------------------------------------------------------%
:- func this_file = string.
this_file = "ordering_mode_constraints.m".
%-----------------------------------------------------------------------------%
:- end_module ordering_mode_constraints.
%-----------------------------------------------------------------------------%
Index: compiler/mcsolver.m (new file)
===================================================================
%-----------------------------------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et
%-----------------------------------------------------------------------------%
% Copyright (C) 2004-2005 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.
%-----------------------------------------------------------------------------%
%
% File: mcsolver.m
% Main authors: rafe, richardf
%
% Original author:
% Ralph Becket <rafe at cs.mu.oz.au>
% Fri Dec 31 14:45:18 EST 2004
%
% A constraint solver targetted specifically at David Overton's
% constraint-based mode analysis.
%
%-----------------------------------------------------------------------------%
:- module check_hlds__mcsolver.
:- interface.
:- import_module check_hlds.abstract_mode_constraints.
:- import_module bool.
:- import_module list.
:- import_module std_util.
:- type var == abstract_mode_constraints.mc_var.
:- type vars == list(var).
% Convenient abbreviations
% Structure in which to collect constraints.
%
:- type prep_cstrts.
% Structure on which the solver operates.
%
:- type solver_cstrts.
% We start by collecting our constraints together in a prep_cstrts
% structure, before preparing them for the solver.
%
:- func new_prep_cstrts = prep_cstrts.
% Prepares the constraints described in abstract_mode_constraints.m
% appropriately.
%
:- pred prepare_abstract_constraints(constraint_formulae::in, prep_cstrts::in,
prep_cstrts::out) is det.
% NOTE: where possible, prepare_abstract_constraints/3 should be used
% rather than this predicate.
%
:- pred equivalent(var::in, var::in, prep_cstrts::in, prep_cstrts::out) is det.
% NOTE: where possible, prepare_abstract_constraints/3 should be used
% rather than this predicate.
%
:- pred equivalent(list(var)::in, prep_cstrts::in, prep_cstrts::out) is det.
% NOTE: where possible, prepare_abstract_constraints/3 should be used
% rather than this predicate.
%
:- pred implies(var::in, var::in, prep_cstrts::in, prep_cstrts::out) is det.
% NOTE: where possible, prepare_abstract_constraints/3 should be used
% rather than this predicate.
%
:- pred not_both(var::in, var::in, prep_cstrts::in, prep_cstrts::out) is det.
% NOTE: where possible, prepare_abstract_constraints/3 should be used
% rather than this predicate.
%
:- pred different(var::in, var::in, prep_cstrts::in, prep_cstrts::out) is det.
% NOTE: where possible, prepare_abstract_constraints/3 should be used
% rather than this predicate.
%
:- pred assign(var::in, bool::in, prep_cstrts::in, prep_cstrts::out) is det.
% NOTE: where possible, prepare_abstract_constraints/3 should be used
% rather than this predicate.
%
:- pred equivalent_to_disjunction(var::in, vars::in,
prep_cstrts::in, prep_cstrts::out) is det.
% NOTE: where possible, prepare_abstract_constraints/3 should be used
% rather than this predicate.
%
:- pred at_most_one(vars::in, prep_cstrts::in, prep_cstrts::out) is det.
% NOTE: where possible, prepare_abstract_constraints/3 should be used
% rather than this predicate.
%
:- pred exactly_one(vars::in, prep_cstrts::in, prep_cstrts::out) is det.
% NOTE: where possible, prepare_abstract_constraints/3 should be used
% rather than this predicate.
%
:- pred disjunction_of_assignments(list(list(pair(var, bool)))::in,
prep_cstrts::in, prep_cstrts::out) is det.
% Convert the set of constraints for use by the solver.
%
:- func make_solver_cstrts(prep_cstrts) = solver_cstrts.
% Nondeterministically enumerate solutions to the constraints.
%
:- pred solve(solver_cstrts::in, mc_bindings::out) is nondet.
% For debugging purposes only.
% :- pred main(io :: di, io :: uo) is det.
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
:- implementation.
:- import_module libs.compiler_util.
:- import_module eqvclass.
:- import_module exception.
:- import_module int.
:- import_module list.
:- import_module map.
:- import_module multi_map.
:- import_module set.
:- import_module std_util.
:- import_module string.
%-----------------------------------------------------------------------------%
% Assignment constraints.
%
:- type assgt ---> (var == bool).
:- type assgts == list(assgt).
% Binary implication constraints. (Not a logical implication,
% just a unidirectional propagation path).
%
:- type impl ---> assgt `implies` assgt.
:- type impls == list(impl).
% Complex constraints.
%
:- type complex_cstrt ---> eqv_disj(var, vars)
% var <-> OR(vars)
; at_most_one(vars)
; exactly_one(vars)
; disj_of_assgts(list(assgts)).
% Each element of the list is a
% list of assignments which should
% occur concurrently.
:- type complex_cstrts == list(complex_cstrt).
% Map from a variable to the complex constraints it participates
% in.
%
:- type complex_cstrt_map == multi_map(var, complex_cstrt).
% A propagation graph is an optimised representation of a set
% of binary implication constraints. It is comprised of a pair
% of mappings from vars to consequent assignments, where the
% LHS of the pair is the mapping when the var in question is
% bound to `yes' and the RHS is the mapping when the var in
% question is bound to `no'.
%
:- type prop_graph == pair(multi_map(var, assgt)).
% We keep track of variables known to be equivalent in order
% to reduce the number of variables we have to worry about
% when solving the constraints.
%
:- type eqv_vars == eqvclass(var).
% This type is just used to collect constraints before
% we prepare them for use by the solver.
%
:- type prep_cstrts
---> prep_cstrts(
prep_eqv_vars :: eqv_vars,
prep_assgts :: assgts,
prep_impls :: impls,
prep_complex_cstrts :: complex_cstrts
).
% This type just holds the various constraints passed to
% the solver. We separate constraints into four classes:
%
% - necessary equivalences are handled by renaming vars in
% an equivalence class to a single member of the equivalence
% class;
% - necessary assignments are dealt with after equivalence
% renaming;
% - the prop_graph represents the graph of binary implications,
% allowing propagation from assignments;
% - complex constraints, such as eqv_disj and at_most_one, which
% are attached to each variable in the complex constraint and
% tested after propagation through the prop_graph. Where
% possible, binary implications that follow from complex
% constraints are added to the prop_graph in order to simplify
% testing the complex constraints.
%
% TODO:
%
% - We should consider adding backjumping if performance is an issue.
%
:- type solver_cstrts
---> solver_cstrts(
vars :: vars,
eqv_vars :: eqv_vars,
assgts :: assgts,
prop_graph :: prop_graph,
complex_cstrt_map :: complex_cstrt_map
).
%-----------------------------------------------------------------------------%
new_prep_cstrts = prep_cstrts(eqvclass.init, [], [], []).
%-----------------------------------------------------------------------------%
% Prepares the constraints described in abstract_mode_constraints.m
% appropriately.
%
prepare_abstract_constraints(Constraints, !PCs) :-
list.foldl(prepare_abstract_constraint, Constraints, !PCs).
% Prepares a constraint (as described in abstract_mode_constraints.m)
% appropriately.
%
:- pred prepare_abstract_constraint(constraint_formula::in, prep_cstrts::in,
prep_cstrts::out) is det.
prepare_abstract_constraint(atomic_constraint(VarConstraint), PCs0, PCs) :-
prepare_var_constraint(VarConstraint, PCs0, PCs).
prepare_abstract_constraint(conj(Formulae), !PCs) :-
prepare_abstract_constraints(Formulae, !PCs).
prepare_abstract_constraint(disj(Formulae), !PCs) :-
( if
% Build var - bool pairs assuming structure
% disj(conj(assgts), conj(assgts, ...), otherwise fail.
list.map(
( pred(conj(Fls)::in, VarValPairs::out) is semidet :-
list.map((pred(atomic_constraint(equiv_bool(Var, Val))::in,
(Var - Val)::out) is semidet), Fls, VarValPairs)
),
Formulae, DisjOfAssgts)
then
disjunction_of_assignments(DisjOfAssgts, !PCs)
else
compiler_util.sorry(this_file, "Disjuction of constraints."
++ " - general case.")
).
% Prepares an atomic constraint (as described in
% abstract_mode_constraints.m) appropriately.
%
:- pred prepare_var_constraint(var_constraint::in, prep_cstrts::in,
prep_cstrts::out) is det.
prepare_var_constraint(equiv_bool(Var, Value), !PCs) :-
assign(Var, Value, !PCs).
prepare_var_constraint(equivalent(Vars), !PCs) :-
equivalent(Vars, !PCs).
prepare_var_constraint(implies(Var1, Var2), !PCs) :-
implies(Var1, Var2, !PCs).
prepare_var_constraint(equiv_disj(X, Ys), !PCs) :-
equivalent_to_disjunction(X, Ys, !PCs).
prepare_var_constraint(at_most_one(Vars), !PCs) :-
at_most_one(Vars, !PCs).
prepare_var_constraint(exactly_one(Vars), !PCs) :-
exactly_one(Vars, !PCs).
%-----------------------------------------------------------------------------%
equivalent(X, Y, PCs0, PCs) :-
PCs = PCs0 ^ prep_eqv_vars :=
ensure_equivalence(PCs0 ^ prep_eqv_vars, X, Y).
%-----------------------------------------------------------------------------%
equivalent([], PCs, PCs).
equivalent([X | Xs], PCs0, PCs) :-
list.foldl(equivalent(X), Xs, PCs0, PCs).
%-----------------------------------------------------------------------------%
implies(X, Y, PCs0, PCs) :-
PCs = PCs0 ^ prep_impls := [ (X == yes) `implies` (Y == yes),
(Y == no) `implies` (X == no)
| PCs0 ^ prep_impls ].
%-----------------------------------------------------------------------------%
not_both(X, Y, PCs0, PCs) :-
PCs = PCs0 ^ prep_impls := [ (X == yes) `implies` (Y == no),
(Y == yes) `implies` (X == no)
| PCs0 ^ prep_impls ].
%-----------------------------------------------------------------------------%
different(X, Y, PCs0, PCs) :-
PCs = PCs0 ^ prep_impls := [ (X == yes) `implies` (Y == no),
(X == no) `implies` (Y == yes),
(Y == yes) `implies` (X == no),
(Y == no) `implies` (X == yes)
| PCs0 ^ prep_impls ].
%-----------------------------------------------------------------------------%
assign(X, V, PCs0, PCs) :-
PCs = PCs0 ^ prep_assgts := [(X == V) | PCs0 ^ prep_assgts].
%-----------------------------------------------------------------------------%
equivalent_to_disjunction(X, Ys, PCs0, PCs) :-
( if Ys = [] then
assign(X, no, PCs0, PCs)
else if Ys = [Y] then
equivalent(X, Y, PCs0, PCs)
else
PCs = PCs0 ^ prep_complex_cstrts :=
[eqv_disj(X, Ys) | PCs0 ^ prep_complex_cstrts]
).
%-----------------------------------------------------------------------------%
at_most_one(Xs, PCs0, PCs) :-
( if Xs = [X, Y] then
not_both(X, Y, PCs0, PCs)
else if Xs = [_, _, _ | _] then
PCs = PCs0 ^ prep_complex_cstrts :=
[at_most_one(Xs) | PCs0 ^ prep_complex_cstrts]
else
PCs = PCs0
).
%-----------------------------------------------------------------------------%
exactly_one(Xs, PCs0, PCs) :-
( if Xs = [X] then
assign(X, yes, PCs0, PCs)
else if Xs = [_, _ | _] then
PCs = PCs0 ^ prep_complex_cstrts :=
[exactly_one(Xs) | PCs0 ^ prep_complex_cstrts]
else
PCs = PCs0
).
%-----------------------------------------------------------------------------%
disjunction_of_assignments(DisjOfAssgts, PCs0, PCs) :-
Assgtss =
list.map(list.map(func((Var - Value)) = (Var == Value)), DisjOfAssgts),
PCs = PCs0 ^ prep_complex_cstrts :=
[disj_of_assgts(Assgtss) | PCs0 ^ prep_complex_cstrts].
%-----------------------------------------------------------------------------%
make_solver_cstrts(PCs) = SCs:-
% Simplify away equivalences.
%
Eqvs = PCs ^ prep_eqv_vars,
Assgts =
map(
func(X == V) = (eqv_var(Eqvs, X) == V),
PCs ^ prep_assgts
),
Impls =
map(
func((X == VX) `implies` (Y == VY)) =
((eqv_var(Eqvs, X) == VX) `implies` (eqv_var(Eqvs, Y) == VY)),
PCs ^ prep_impls
),
ComplexCstrts =
map(eqv_complex_cstrt(Eqvs), PCs ^ prep_complex_cstrts),
% Construct the propagation graph.
%
PropGraph =
foldl(
func(((X == VX) `implies` (Y == VY)), YesPG - NoPG) =
( if VX = yes then set(YesPG, X, (Y == VY)) - NoPG
else YesPG - set(NoPG, X, (Y == VY))
),
Impls,
multi_map.init - multi_map.init
),
% Construct the complex constraints map.
%
ComplexCstrtsMap =
foldl(
func(ComplexCstrt, CCM) =
foldl(
func(Z, CCMa) = multi_map.set(CCMa, Z, ComplexCstrt),
complex_cstrt_vars(ComplexCstrt),
CCM
),
ComplexCstrts,
multi_map.init
),
% Find the set of variables we have to solve for.
%
AssgtVars =
foldl(
func((X == _V), Vars) = [X | Vars],
Assgts,
[]
),
AndImplVars =
foldl(
func((X == _VX) `implies` (Y == _VY), Vars) = [X, Y | Vars],
Impls,
AssgtVars
),
AndComplexCstrtVars =
foldl(
func(ComplexCstrt, Vars) =
complex_cstrt_vars(ComplexCstrt) ++ Vars,
ComplexCstrts,
AndImplVars
),
AllVars = sort_and_remove_dups(AndComplexCstrtVars),
% Make the solver constraints record.
%
SCs = solver_cstrts(AllVars, Eqvs, Assgts, PropGraph, ComplexCstrtsMap).
% eqv_var(Eqvs, Var) returns a representative member of all the
% variables equivalent to Var (in Eqvs)
%
:- func eqv_var(eqv_vars, var) = var.
eqv_var(Eqvs, X) = eqvclass.get_minimum_element(Eqvs, X).
% eqv_vars(Eqvs, Vars) just maps eqv_var to each Var in Vars.
%
:- func eqv_vars(eqv_vars, vars) = vars.
eqv_vars(Eqvs, Xs) = map(eqv_var(Eqvs), Xs).
% Returns all the variables that participate in this constraint.
%
:- func complex_cstrt_vars(complex_cstrt) = vars.
complex_cstrt_vars(eqv_disj(X, Ys)) = [X | Ys].
complex_cstrt_vars(at_most_one(Xs)) = Xs.
complex_cstrt_vars(exactly_one(Xs)) = Xs.
complex_cstrt_vars(disj_of_assgts(Assgtss)) =
list.foldl(list.foldl(func((V == _), Vs) = [V | Vs]), Assgtss, []).
% Replaces all the variables in the supplied constraint with
% a representative variable from those constrained to be
% equivalent to the original.
%
:- func eqv_complex_cstrt(eqv_vars, complex_cstrt) = complex_cstrt.
eqv_complex_cstrt(Eqvs, eqv_disj(X, Ys)) =
eqv_disj(eqv_var(Eqvs, X), eqv_vars(Eqvs, Ys)).
eqv_complex_cstrt(Eqvs, at_most_one(Xs)) =
at_most_one(eqv_vars(Eqvs, Xs)).
eqv_complex_cstrt(Eqvs, exactly_one(Xs)) =
exactly_one(eqv_vars(Eqvs, Xs)).
eqv_complex_cstrt(Eqvs, disj_of_assgts(Assgtss)) =
disj_of_assgts(list.map(
list.map(func((Var == Val)) = (eqv_var(Eqvs, Var) == Val)),
Assgtss
)).
%-----------------------------------------------------------------------------%
% Succeeds if Bindings satisfies the constraints SCs.
%
solve(SCs, Bindings) :-
solve(SCs, map.init, Bindings0),
bind_equivalent_vars(SCs, Bindings0, Bindings).
% unsafe.io(nl).
% solve(SCs, Bs0, Bs) succeeds if Bs satisfies the constraints SCs,
% given that Bs0 is known to not conflict with any of the constraints
% in SCs.
%
:- pred solve(solver_cstrts::in, mc_bindings::in, mc_bindings::out) is nondet.
solve(SCs, Bs0, Bs) :-
solve_assgts(SCs, SCs ^ assgts, Bs0, Bs1),
solve_vars(SCs, SCs ^ vars, Bs1, Bs).
% Propagates the binding for every variable that has been
% solved for to every variable it is equivalent to.
%
:- pred bind_equivalent_vars(solver_cstrts::in, mc_bindings::in,
mc_bindings::out) is det.
bind_equivalent_vars(SCs, !Bindings) :-
Equivalences = SCs ^ eqv_vars,
list.foldl(
( pred(Var::in, Binds0::in, Binds::out) is det :-
EquivVars = set.to_sorted_list(get_equivalent_elements(
Equivalences, Var)),
map.lookup(Binds0, Var, Val),
bind_all(EquivVars, Val, Binds0, Binds)
),
map.keys(!.Bindings), !Bindings).
% bind_all(Vars, Val, !Bindings) Binds Var to Val in Bindings for
% every Var in Vars.
%
:- pred bind_all(vars::in, bool::in, mc_bindings::in, mc_bindings::out) is det.
bind_all(Vars, Val, !Bindings) :-
list.foldl(
( pred(Var::in, Binds0::in, Binds::out) is det :-
map.set(Binds0, Var, Val, Binds)
),
Vars, !Bindings).
%-----------------------------------------------------------------------------%
% solve_assgts(SCs, Assgts, Bs0, Bs) attempts to perform each variable
% binding in Assgts, propagating the results when called for.
%
:- pred solve_assgts(solver_cstrts::in, assgts::in,
mc_bindings::in, mc_bindings::out) is semidet.
solve_assgts(SCs, Assgts, Bs0, Bs) :-
list.foldl(solve_assgt(SCs), Assgts, Bs0, Bs).
% solve_assgt(SCs, (X == V), Bs0, Bs) attempts to bind variable X
% to value V. It propagates the results if it succeeds.
%
:- pred solve_assgt(solver_cstrts::in, assgt::in, mc_bindings::in,
mc_bindings::out) is semidet.
solve_assgt(SCs, (X == V), Bs0, Bs) :-
( if Bs0 ^ elem(X) = V0 then
% ( if V \= V0 then unsafe.io(write_string(X ++ " conflict")) else true ),
V = V0,
Bs = Bs0
else
% unsafe.io(write_string(".")),
Bs1 = Bs0 ^ elem(X) := V,
Assgts = SCs ^ prop_graph ^ var_consequents(X, V),
solve_assgts(SCs, Assgts, Bs1, Bs2),
ComplexCstrts = SCs ^ complex_cstrt_map ^ var_complex_cstrts(X),
solve_complex_cstrts(SCs, X, V, ComplexCstrts, Bs2, Bs)
).
%-----------------------------------------------------------------------------%
% solve_complex_cstrts(SCs, X, V, ComplexCstrts, Bs0, Bs) succeeds
% if the binding (X == V) (which should already have been added to
% Bs0) is consistant with the complex constraints variable X
% participates in in SCs. It also propagates results where
% appropriate.
%
:- pred solve_complex_cstrts(solver_cstrts::in, var::in, bool::in,
complex_cstrts::in, mc_bindings::in, mc_bindings::out) is semidet.
solve_complex_cstrts(SCs, X, V, ComplexCstrts, Bs0, Bs) :-
list.foldl(solve_complex_cstrt(SCs, X, V), ComplexCstrts, Bs0, Bs).
% solve_complex_cstrt(SCs, X, V, ComplexCstrt, Bs0, Bs) succeeds
% if the binding (X == V) (which should already have been added to
% Bs0) is consistant with ComplexCstrt (in which X should
% participate in in SCs). It also propagates results where
% appropriate.
%
:- pred solve_complex_cstrt(solver_cstrts::in, var::in, bool::in,
complex_cstrt::in, mc_bindings::in, mc_bindings::out) is semidet.
solve_complex_cstrt(SCs, X, V, eqv_disj(Y, Zs), Bs0, Bs) :-
( if X = Y then
(
V = yes,
% unsafe.io(write_string("1<")),
not all_no(Bs0, Zs),
Bs = Bs0
;
V = no,
% unsafe.io(write_string("0<")),
solve_assgts(SCs, map(func(Z) = (Z == no), Zs), Bs0, Bs)
)
else /* X in Zs */
(
V = yes,
% unsafe.io(write_string(">1")),
solve_assgt(SCs, (Y == yes), Bs0, Bs)
;
V = no,
% unsafe.io(write_string(">0")),
( if all_no(Bs0, Zs)
then solve_assgt(SCs, (Y == no), Bs0, Bs)
else Bs = Bs0
)
)
).
solve_complex_cstrt(SCs, X, V, at_most_one(Ys0), Bs0, Bs) :-
(
V = no,
Bs = Bs0
;
V = yes,
list.delete_first(Ys0, X, Ys),
solve_assgts(SCs, map(func(Y) = (Y == no), Ys), Bs0, Bs)
).
solve_complex_cstrt(SCs, X, V, exactly_one(Ys0), Bs0, Bs) :-
(
V = no,
% A variable in Ys0 uniquely not bound to 'no' is bound to
% yes. Fails if all Ys0 are 'no'.
Ys = list.filter(
(pred(Y0::in) is semidet :- not map.search(Bs0, Y0, no)), Ys0),
(
Ys = [Y],
solve_assgts(SCs, [(Y == yes)], Bs0, Bs)
;
Ys = [_, _| _],
Bs = Bs0
)
;
V = yes,
list.delete_first(Ys0, X, Ys),
solve_assgts(SCs, map(func(Y) = (Y == no), Ys), Bs0, Bs)
).
solve_complex_cstrt(SCs, X, V, disj_of_assgts(Assgtss), Bs0, Bs) :-
% Filter for the assignments compatable with binding X to V
list.filter(
(pred(Assgts::in) is semidet :-
list.member((X == bool.not(V)), Assgts)
),
Assgtss,_Conflicts, NotConflicting),
%
% If only one set of assignments is possible now, make them.
% If none are possible, fail.
%
(
NotConflicting = [Assignments],
solve_assgts(SCs, Assignments, Bs0, Bs)
;
NotConflicting = [_, _ | _],
Bs = Bs0
).
%-----------------------------------------------------------------------------%
% PropGraph ^ var_consequents(X, V) returns the assignments
% directly entailed by biding X to V.
%
:- func prop_graph ^ var_consequents(var, bool) = assgts.
(YesPG - _NoPG) ^ var_consequents(X, yes) =
( if YesPG ^ elem(X) = Assgts then Assgts else [] ).
(_YesPG - NoPG) ^ var_consequents(X, no ) =
( if NoPG ^ elem(X) = Assgts then Assgts else [] ).
%-----------------------------------------------------------------------------%
% ComplexCstrtMap ^ var_complex_cstrts(X) returns the complex
% constraints, if any, that variable X participates in.
%
:- func complex_cstrt_map ^ var_complex_cstrts(var) = complex_cstrts.
ComplexCstrtMap ^ var_complex_cstrts(X) =
( if ComplexCstrtMap ^ elem(X) = CmplxCstrts then CmplxCstrts else [] ).
%-----------------------------------------------------------------------------%
% solve_vars(SCs, Vars, Bs0, Bs) non-deterministically assigns a value
% to each of Vars and propagates results, looking for a solution
% to SCs.
%
:- pred solve_vars(solver_cstrts::in, vars::in, mc_bindings::in,
mc_bindings::out) is nondet.
solve_vars(SCs, Vars, Bs0, Bs) :-
list.foldl(solve_var(SCs), Vars, Bs0, Bs).
:- pred solve_var(solver_cstrts::in, var::in, mc_bindings::in,
mc_bindings::out) is nondet.
solve_var(SCs, X, Bs0, Bs) :-
( if contains(Bs0, X) then
Bs = Bs0
else
( V = yes ; V = no ),
% unsafe.io(write_string("\n" ++ X ++ " = ")), unsafe.io(print(V)),
solve_assgt(SCs, (X == V), Bs0, Bs)
).
%-----------------------------------------------------------------------------%
% all_yes(Bs, Xs) succeeds if Bs indicates all Xs are bound to yes
%
:- pred all_yes(mc_bindings::in, vars::in) is semidet.
all_yes(_, []).
all_yes(Bs, [X | Xs]) :-
Bs ^ elem(X) = yes,
all_yes(Bs, Xs).
% all_no(Bs, Xs) succeeds if Bs indicates all Xs are bound to no
%
:- pred all_no(mc_bindings::in, vars::in) is semidet.
all_no(_, []).
all_no(Bs, [X | Xs]) :-
Bs ^ elem(X) = no,
all_no(Bs, Xs).
%-----------------------------------------------------------------------------%
% main(!IO) :-
%
% NameBindingss = solutions(solve(append_simple)),
%
% io.nl(!IO),
% io.write_list(NameBindingss, "\n\n", io.print, !IO),
% io.nl(!IO).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
:- func this_file = string.
this_file = "mcsolver.m".
%-----------------------------------------------------------------------------%
:- end_module mcsolver.
%-----------------------------------------------------------------------------%
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------
More information about the reviews
mailing list