[m-rev.] For review: new constraint based mode analysis
Richard James FOTHERGILL
richardf at students.cs.mu.OZ.AU
Tue Feb 8 15:58:05 AEDT 2005
For review by anyone.
Estimated hours taken: 100
Branches: Main
These changes provide the framework for a new approach to constraints based
mode analysis. They build constraints for simple mercury programs (sorry,
no higher order unifications), and can later be extended to handle all
applicable hlds goals. They have been designed with the intention that
they would be solved, for example, by a propagation based constraint solver,
and the information used for producing a partial order on conjuncts and
for mode analysis of a mercury program.
compiler/new_mode_constraints.m
This module serves as an interface between the existing
mode_constraints module which asks for constraints for an SCC, and
build_mode_constraints, which only handles goals. Simply put, it takes
an SCC and hands it to build_mode_constraints one predicate at a time.
It produces the mode constraints for that SCC, and the constraint
variables necessary to do so.
compiler/build_mode_constraints.m
This module creates the constraint variables and constraints needed for
the new constraints based mode analysis. It traverses the hlds_goal
data structure recursively to form mode constraints for a goal. The
constraints it builds are the simplified form - they do not deal with
partial instantiation. They are also incomplete, as no constraints are
produced for higher order unifications, parallel conjunctions, switches
etc.
A rough description of the constraints can be found in chapter six of
David Overton's disseration, "Precise and Expressive Mode Systems for
Typed Logic Programming Languages."
compiler/abstract_mode_constraints.m
This module contains data structures that represent mode constraints.
They have been chosen so as to minimise complication for the types of
constraints most often created by mode analysis. There is also a
predicate here for displaying the constraints/printing to file.
compiler/check_hlds.m:
Added :- include_module statements for new modules
check_hlds.abstract_mode_constraints,
check_hlds.build_mode_constraints and
check_hlds.new_mode_constraints.
compiler/mode_constraints.m
mode_constraints.process_module now switches on the global
bool option new_mode_constraints. If the option is true,
it passes control over to new_mode_constraints.process_scc
instead of its own process_scc, then outputs the results
to a file named after the module being processed with the
extension .mode_constraints
compiler/options.m
New option inclued --new-mode-constraints. Note that the
new mode constraints material is an offshoot of the original,
so to run it both --mode-constraints and --new-mode-constraints
must be specified.
compiler/notes/compiler_design.html
Added a description of various parts of the new constraints
based mode analysis work.
cvs diff: Diffing .
cvs diff: Diffing analysis
cvs diff: Diffing bench
cvs diff: Diffing bench/progs
cvs diff: Diffing bench/progs/compress
cvs diff: Diffing bench/progs/icfp2000
cvs diff: Diffing bench/progs/icfp2001
cvs diff: Diffing bench/progs/nuc
cvs diff: Diffing bench/progs/ray
cvs diff: Diffing bench/progs/tree234
cvs diff: Diffing bindist
cvs diff: Diffing boehm_gc
cvs diff: Diffing boehm_gc/Mac_files
cvs diff: Diffing boehm_gc/cord
cvs diff: Diffing boehm_gc/cord/private
cvs diff: Diffing boehm_gc/doc
cvs diff: Diffing boehm_gc/include
cvs diff: Diffing boehm_gc/include/private
cvs diff: Diffing boehm_gc/tests
cvs diff: Diffing browser
cvs diff: Diffing bytecode
cvs diff: Diffing bytecode/test
cvs diff: Diffing compiler
Index: compiler/abstract_mode_constraints.m
===================================================================
RCS file: compiler/abstract_mode_constraints.m
diff -N compiler/abstract_mode_constraints.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/abstract_mode_constraints.m 3 Feb 2005 05:49:41 -0000
@@ -0,0 +1,572 @@
+%-----------------------------------------------------------------------------%
+% 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: 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.
+%
+
+
+
+:- module check_hlds.abstract_mode_constraints.
+
+:- interface.
+
+:- type mc_type.
+
+:- import_module term, list, bool, map, counter.
+:- import_module std_util, varset, io.
+
+% XXX change to mc_var throughout
+:- type mc_var == var(mc_type). % Constraint variable.
+:- type mc_varset == varset(mc_type). % Source of constraint variables
+ % And their names.
+:- type vars(T) == list(var(T)).
+
+
+%-----------------------------------------------------------------------------%
+%
+% Data structures for storing abstract constraints. Conjunctions and
+% disjunctions can be formed. 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.
+%
+
+
+ % 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. It should be noted that
+ % the intention is to only use the conj constructor as a child of disj
+ % - and a constraint_formulae list on its own could be considered a
+ % conjunction of its elements.
+ %
+:- 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.
+ ; conj(constraint_formulae)
+ % See disj.
+ % Note that conj([]) is the empty constraint, or true.
+.
+
+
+% var_constraint represents a constraint between variables
+:- type var_constraint == var_constraint(mc_type).
+:- type var_constraint(T)
+ ---> equiv_bool(var(T), bool)
+ % equiv_bool(X, yes) gives the constraint (X)
+ % equiv_bool(X, no) gives the constraint not(X)
+ ; equivalent(vars(T))
+ % equivalent(Xs) gives (all Xi, Xj in Xs).(Xi<->Xj)
+ ; implies(var(T), var(T))
+ % implies(X, Y) gives X->Y
+ ; equiv_disj(var(T), vars(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(vars(T))
+ % at_most_one(Xs) gives
+ % (all Xi, Xj in Xs).(i = j or not(Xi and Xj))
+ ; at_least_one(vars(T))
+ % at_least_one(Xs) gives OR(Xs)
+ ; exactly_one(vars(T))
+ % exactly_one(Xs) gives
+ % at_least_one(Xs) and at_most_one(Xs)
+.
+
+
+
+
+ % Attempts to print the constraint_formulae it is passed in a human
+ % readable format. Always puts a new line after it is finished.
+ %
+:- pred pretty_print_constraints(
+ mc_varset::in, constraint_formulae::in, io::di, io::uo
+ ) is det.
+
+
+
+%-----------------------------------------------------------------------------%
+%
+% 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 inthe 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.
+%
+% 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(var(mc_type), var_state),
+ % The variables this constraint system constrains
+ id_counter :: counter
+ % Supplies unique IDs for the constraint map.
+ ).
+
+
+:- type constraint_id == int.
+
+:- type constraint --->
+ constraint(
+ id :: constraint_id,
+ current :: constraint_formula_and_vars,
+ % Formula modified as variables are bound.
+ original :: constraint_formula_and_vars
+% dead :: bool
+% % for if the current constraint is empty... don't
+% % know if this will be used
+ ).
+
+:- type constraint_formula_and_vars --->
+ constraint_formula_and_vars(
+ constraint_formula :: constraint_formula,
+ participating_vars :: vars(mc_type)
+ ).
+
+
+
+:- 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.
+ ).
+
+:- 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(var(mc_type))
+ % 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 :: var(mc_type),
+% % 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),
+ constraint :: constraint_id
+ ).
+
+
+
+
+% Initiates all the parts of a mode_constraints_info type.
+:- pred abstract_mode_constraints.init(mode_constraints_info::out) is det.
+
+% Functional version if init/1.
+:- func abstract_mode_constraints.init = (mode_constraints_info::out) is det.
+
+% Incorporates a new constraint into the system.
+:- pred abstract_mode_constraints.add_constraint(
+ constraint_formula::in,
+ mode_constraints_info::in,
+ mode_constraints_info::out
+ ) is det.
+
+% Functional version of add_constraint/3.
+:- func abstract_mode_constraints.add_constraint(
+ constraint_formula::in,
+ mode_constraints_info::in
+ ) = (mode_constraints_info::out) is det.
+
+
+
+:- implementation.
+
+
+:- import_module string.
+
+:- type mc_type --->
+ mc_type.
+
+
+% Initiates all the parts of a mode_constraints_info type.
+abstract_mode_constraints.init(ModeConstraintsInfo) :-
+ ModeConstraintsInfo = mode_constraints_info(
+ map.init,
+ map.init,
+ counter.init(0) % Start allocating ids from 0
+ ).
+
+% See the predicate version.
+abstract_mode_constraints.init = ModeConstraintsInfo :-
+ abstract_mode_constraints.init(ModeConstraintsInfo).
+
+
+% Incorporates a new constraint into the system.
+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
+ ),
+ !:ModeConstraintsInfo =
+ !.ModeConstraintsInfo ^ constraint_map :=
+ map.det_insert(
+ !.ModeConstraintsInfo ^ constraint_map,
+ NewID,
+ constraint(NewID, FormulaAndVars, FormulaAndVars)
+ ).
+
+
+
+% Functional version of add_constraint/3.
+abstract_mode_constraints.add_constraint(CF, MCI0) = MCI :-
+ abstract_mode_constraints.add_constraint(CF, MCI0, MCI).
+
+
+
+
+% 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, vars(mc_type)::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, VarState1)
+ -> CInfoList = [ConstrainmentInfo| VarState1 ^ is_constrained],
+ VarState = VarState1 ^ 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,
+ vars(mc_type)::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, vars(mc_type)::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(
+ (pred(Formula1::in, Vars1::in, VarsNew::out) is det :-
+ formula_to_vars(Formula1, Vars2),
+ append(Vars2, Vars1, VarsNew)
+ ),
+ Formulae,
+ [],
+ 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, vars(mc_type)::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.
+
+
+
+
+%-----------------------------------------------------------------------------%
+%
+% Pretty printing predicates for the formulae type, and others
+%
+
+
+
+pretty_print_constraints(Varset, Constraints, !IO) :-
+ pretty_print_constraints(
+ Varset,
+ Constraints,
+ "", % Extra argument for indent.
+ !IO
+ ).
+
+ % Same as before, but with an indent argument used to indent
+ % conjunctions and disjunctions of constraints.
+ %
+:- pred pretty_print_constraints(
+ mc_varset::in,
+ constraint_formulae::in,
+ string::in,
+ io::di,
+ io::uo
+ ) is det.
+
+pretty_print_constraints(_Varset, [], _Indent, !IO).
+pretty_print_constraints(Varset, [Constr|Constrs], Indent, !IO) :-
+ pretty_print_constraint(Varset, Constr, Indent, !IO),
+ pretty_print_constraints(Varset, Constrs, Indent, !IO).
+
+
+ % Prints one constraint_formulae to the output stream. Always puts
+ % a new line at the end.
+ %
+:- pred pretty_print_constraint(
+ mc_varset::in,
+ constraint_formula::in,
+ string::in,
+ io::di,
+ io::uo
+ ) is det.
+
+pretty_print_constraint(Varset, disj(Constraints), Indent, !IO) :-
+ io.print(Indent, !IO),
+ io.print("disj(\n", !IO),
+ pretty_print_constraints(
+ Varset, Constraints, "\t" ++ Indent, !IO),
+ io.print(Indent, !IO),
+ io.print(") end disj", !IO),
+ io.nl(!IO).
+
+pretty_print_constraint(Varset, conj(Constraints), Indent, !IO) :-
+ io.print(Indent, !IO),
+ io.print("conj(\n", !IO),
+ pretty_print_constraints(
+ Varset, Constraints, "\t" ++ Indent, !IO),
+ io.print(Indent, !IO),
+ io.print(") end conj", !IO),
+ io.nl(!IO).
+
+pretty_print_constraint(
+ Varset, atomic_constraint(Constraint), Indent, !IO) :-
+ io.print(Indent, !IO),
+ pretty_print_var_constraint(Varset, Constraint, !IO),
+ io.nl(!IO).
+
+ % Prints a var_constraint to the screen. No indents, no line return.
+ %
+:- pred pretty_print_var_constraint(
+ mc_varset::in,
+ var_constraint::in,
+ io::di,
+ io::uo
+ ) is det.
+
+pretty_print_var_constraint(Varset, equiv_bool(X, TF), !IO) :-
+ pretty_print_mc_var(Varset, X, !IO),
+ io.print(" = ", !IO),
+ io.print(TF, !IO).
+
+pretty_print_var_constraint(Varset, equivalent(Xs), !IO) :-
+ io.print("equivalent(", !IO),
+ pretty_print_mc_vars(Varset, Xs, !IO),
+ io.print(")", !IO).
+
+pretty_print_var_constraint(Varset, implies(X, Y), !IO) :-
+ pretty_print_mc_var(Varset, X, !IO),
+ io.print(" -> ", !IO),
+ pretty_print_mc_var(Varset, Y, !IO).
+
+pretty_print_var_constraint(Varset, equiv_disj(X, Xs), !IO) :-
+ pretty_print_mc_var(Varset, X, !IO),
+ io.print(" <-> disj(", !IO),
+ pretty_print_mc_vars(Varset, Xs, !IO),
+ io.print(")", !IO).
+
+pretty_print_var_constraint(Varset, at_most_one(Xs), !IO) :-
+ io.print("at_most_one(", !IO),
+ pretty_print_mc_vars(Varset, Xs, !IO),
+ io.print(")", !IO).
+
+pretty_print_var_constraint(Varset, at_least_one(Xs), !IO) :-
+ io.print("at_least_one(", !IO),
+ pretty_print_mc_vars(Varset, Xs, !IO),
+ io.print(")", !IO).
+
+pretty_print_var_constraint(Varset, exactly_one(Xs), !IO) :-
+ io.print("exactly_one(", !IO),
+ pretty_print_mc_vars(Varset, Xs, !IO),
+ io.print(")", !IO).
+
+
+ % Prints a constraint var to the screen. No indents, no line return.
+ % Simply uses the variable's name from the varset.
+ %
+:- pred pretty_print_mc_var(
+ mc_varset::in,
+ mc_var::in,
+ io::di,
+ io::uo
+ ) is det.
+
+pretty_print_mc_var(Varset, Var, !IO) :-
+ varset.lookup_name(Varset, Var, VarName),
+ io.print(VarName, !IO).
+
+
+
+ % Prints a comma separated list of constraint variables.
+ %
+:- pred pretty_print_mc_vars(
+ mc_varset::in,
+ list(mc_var)::in,
+ io::di,
+ io::uo
+ ) is det.
+
+pretty_print_mc_vars(_Varset, [], !IO).
+pretty_print_mc_vars(Varset, [Var| Tail], !IO) :-
+ pretty_print_mc_var(Varset, Var, !IO),
+ pretty_print_mc_vars_tail(Varset, Tail, !IO).
+
+ % Prints a comma separated list of constraint variables under
+ % the assumption that at least one has already been printed
+ % - ie prints a divider then prints the rest of the list.
+ % If there is no more list it does nothing.
+ %
+:- pred pretty_print_mc_vars_tail(
+ mc_varset::in,
+ list(mc_var)::in,
+ io::di,
+ io::uo
+ ) is det.
+
+pretty_print_mc_vars_tail(_Varset, [], !IO).
+pretty_print_mc_vars_tail(Varset, [Var| Vars], !IO) :-
+ io.print(", ", !IO),
+ pretty_print_mc_vars(Varset, [Var| Vars], !IO).
+
+
+
+
+
Index: compiler/build_mode_constraints.m
===================================================================
RCS file: compiler/build_mode_constraints.m
diff -N compiler/build_mode_constraints.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/build_mode_constraints.m 8 Feb 2005 03:35:23 -0000
@@ -0,0 +1,1092 @@
+%-----------------------------------------------------------------------------%
+% 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: build_mode_constraints.m
+% Main author: richardf
+%
+% This module contains predicates and data structures needed for traversing
+% hlds and building a list of abstract constraint formulae to describe
+% variable producers in a mercury program.
+%
+
+
+% XXX Change tabs to 4-spaces would make things neater.
+
+
+:- module check_hlds.build_mode_constraints.
+
+:- interface.
+
+
+
+:- import_module check_hlds.abstract_mode_constraints.
+
+:- 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, list, set.
+
+
+ % 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.
+ %
+:- type mode_constraints == constraint_formulae.
+
+
+ % 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).
+ %
+ % 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).
+
+
+ % Just a conveniently descriptive name.
+ %
+:- type args == list(prog_var).
+
+
+ % Just a conveniently descriptive name.
+ %
+:- type nonlocals == set(prog_var).
+
+ % In order to uniquely distinguish 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.
+ %
+:- type mc_prog_var --->
+ prog_var `in` pred_id.
+
+
+ % 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.
+ %
+:- 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"
+ %
+:- 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.
+ %
+:- 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.
+
+
+ % 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.
+ %
+:- 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.
+
+
+
+
+ % mode_decls_constraints(ModuleInfo, VarMap, PredID,
+ % Decls, HeadVarsList, Constraints)
+ %
+ % Constraints is the disjuction 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.
+ %
+:- pred mode_decls_constraints(module_info::in, mc_var_map::in,
+ pred_id::in, list(list(mode))::in,
+ list(args)::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
+ % is a hack to solve an error in call_mode_decls_constraints,
+ % and may not keep working. It 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 prog_tree.prog_mode.in_mode
+:- pred add_sufficient_in_modes_for_type_info_args(
+ args::in, list(mode)::in, list(mode)::out
+ ) is det.
+
+
+ % goal_expr_constraints generates the constraints that apply to a given
+ % goal_expr at a given goal path.
+ %
+:- 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.
+
+:- implementation.
+
+:- import_module check_hlds.goal_path.
+:- import_module check_hlds.mode_util.
+:- import_module check_hlds.inst_match.
+:- import_module hlds__hlds_data.
+:- import_module hlds__passes_aux.
+:- import_module parse_tree__prog_mode.
+:- import_module transform_hlds__dependency_graph.
+
+
+:- import_module bool, gc, int, map, multi_map, require, sparse_bitset.
+:- import_module std_util, string, term, term_io, varset.
+
+
+add_mc_vars_for_scc_heads(_ModuleInfo, [], !Varset, !VarMap).
+add_mc_vars_for_scc_heads(ModuleInfo, [PredID| PredIDs], !Varset, !VarMap) :-
+ 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
+ ; varset.new_named_var(
+ !.Varset,
+ rep_var_to_string(ProgVarset, RepVar),
+ NewMCvar,
+ !:Varset
+ ),
+ bimap.det_insert(!.VarMap, RepVar, NewMCvar, !:VarMap)
+ ).
+
+
+
+add_mc_vars_for_goal(
+ PredID, ProgVarset, GoalExpr - GoalInfo, !Varset, !VarMap) :-
+ 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}
+ ),
+ % Switch on GoalExpr for recursion
+ ( GoalExpr = conj(Goals),
+ list.foldl2(
+ add_mc_vars_for_goal(PredID, ProgVarset),
+ Goals,
+ !Varset,
+ !VarMap
+ )
+ ; GoalExpr = call(_, _, _, _, _, _)
+ ; GoalExpr = generic_call(_, _, _, _)
+ ; GoalExpr = switch(_, _, Cases),
+ Goals = list.map(func(case(_, Goal)) = Goal, Cases),
+ list.foldl2(
+ add_mc_vars_for_goal(PredID, ProgVarset),
+ Goals,
+ !Varset,
+ !VarMap
+ )
+ ; GoalExpr = unify(_, _, _, _, _)
+ ; GoalExpr = disj(Goals),
+ list.foldl2(
+ add_mc_vars_for_goal(PredID, ProgVarset),
+ Goals,
+ !Varset,
+ !VarMap
+ )
+ ; GoalExpr = not(Goal),
+ add_mc_vars_for_goal(
+ PredID, ProgVarset, Goal, !Varset, !VarMap
+ )
+ ; GoalExpr = some(_, _, Goal),
+ add_mc_vars_for_goal(
+ PredID, ProgVarset, Goal, !Varset, !VarMap
+ )
+ ; GoalExpr = if_then_else(_, Cond, Then, Else),
+ Goals = [Cond, Then, Else],
+ list.foldl2(
+ add_mc_vars_for_goal(PredID, ProgVarset),
+ Goals,
+ !Varset,
+ !VarMap
+ )
+ ; GoalExpr = foreign_proc(_, _, _, _, _, _)
+ ; GoalExpr = par_conj(_Goals)
+ ; GoalExpr = shorthand(_ShorthandGoalExpr)
+ ).
+
+
+
+rep_var_to_string(ProgVarset, (ProgVar `in` _) `at` GoalPath) = RepString :-
+ goal_path_to_string(GoalPath, GoalPathString),
+ varset.lookup_name(ProgVarset, ProgVar, ProgVarString),
+ ( GoalPathString = ""
+ -> RepString = ProgVarString
+ ; RepString = ProgVarString ++ "." ++ GoalPathString
+ ).
+
+
+%-----------------------------------------------------------------------------
+
+
+ % goal_constraints gives the mode constraints for the supplied
+ % hlds_goal
+ %
+:- pred goal_constraints(
+ module_info::in,
+ mc_var_map::in,
+ pred_id::in,
+ hlds_goal::in,
+ mode_constraints::out
+ ) is det.
+
+goal_constraints(
+ ModuleInfo, VarMap, PredID, GoalExpr - GoalInfo, 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:
+ % G1, ..., Gn where Goals = [G1, ..., Gn]
+ %
+goal_expr_constraints(ModuleInfo, VarMap, PredID,
+ conj(Goals), GoalPath, Nonlocals, Constraints) :-
+
+ list.map(
+ goal_constraints(ModuleInfo, VarMap, PredID),
+ Goals, ConjunctConstraints
+ ),
+ Constraints0 = list.condense(ConjunctConstraints),
+ foldl(
+ fold_local_var_into_conj_constraints(VarMap, LocalsPositions),
+ multi_map.keys(LocalsPositions),
+ Constraints0, Constraints1
+ ),
+ 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.
+ ).
+
+
+
+ % Pred Call
+ %
+goal_expr_constraints(ModuleInfo, VarMap, PredID,
+ call(CalledPred, _ProcID, Args, _Builtin, _UnifyContext, _Name),
+ GoalPath, _Nonlocals, Constraints) :-
+
+ % Get the declared modes (if any exist)
+ module_info_pred_info(ModuleInfo, CalledPred, PredInfo),
+ pred_info_procedures(PredInfo, ProcTable),
+ map.values(ProcTable, ProcInfos),
+ list.map(proc_info_maybe_declared_argmodes, ProcInfos, MaybeArgModes),
+ list.filter_map(
+ (pred(yes(X)::in, X::out) is semidet),
+ MaybeArgModes,
+ ArgModeDecls
+ ),
+
+ ( ArgModeDecls = [],
+ % No modes declared, must be in the same SCC as the
+ % calling predicate.
+
+ % 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
+ )
+ ; ArgModeDecls = [_| _],
+ % At least one declared mode
+
+ 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.
+
+ call_mode_decls_constraints(
+ ModuleInfo,
+ VarMap,
+ PredID,
+ FullArgModeDecls,
+ GoalPath,
+ Args,
+ Constraints
+ )
+ ).
+
+ % XXX Need to do something here.
+ %
+goal_expr_constraints(_ModuleInfo, _VarMap, _PredID,
+ generic_call(_, _, _, _), _GoalPath, _Nonlocals, _Constraints) :-
+ error("build_mode_constraints.m: "
+ ++ "sorry, generic_call not implemented.").
+
+
+ % XXX Need to do something here.
+ %
+goal_expr_constraints(_ModuleInfo, _VarMap, _PredID,
+ switch(_, _, _), _GoalPath, _Nonlocals, _Constraints) :-
+ error("build_mode_constraints.m: "
+ ++ "sorry, switch not implemented.").
+
+ % Unification Goals
+ %
+goal_expr_constraints(_ModuleInfo, VarMap, PredID,
+ unify(LHSvar, RHS, _Mode, _Kind, _Context),
+ GoalPath, _Nonlocals, Constraints) :-
+ ( RHS = var(RHSvar),
+ % Goal: LHSvar = RHSvar
+ Constraints = [
+ atomic_constraint(at_most_one([
+ prog_var_at_path(
+ VarMap, PredID, GoalPath, LHSvar
+ ),
+ prog_var_at_path(
+ VarMap, PredID, GoalPath, RHSvar
+ )
+ ])) % At most one of the left and right hand
+ % sides of a unification is produced
+ % at the unification.
+ ]
+ ; 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
+ ),
+ ( ArgsProducedHere = [OneArgProducedHere, _Two| _],
+ % Goal: LHSvar = functor(Args)
+ Constraints = [
+ atomic_constraint(
+ equivalent(ArgsProducedHere)
+ ), % If one arg is produced here,
+ % then they all are.
+ atomic_constraint(at_most_one([
+ LHSproducedHere,
+ OneArgProducedHere
+ ])) % At most one side of the
+ % unification is produced.
+ ]
+ ; ArgsProducedHere = [OneArgProducedHere],
+ % Goal: LHSvar = functor(Arg)
+ Constraints = [
+ atomic_constraint(at_most_one([
+ LHSproducedHere,
+ OneArgProducedHere
+ ])) % At most one side of the
+ % unification is produced.
+ ]
+ ; ArgsProducedHere = [],
+ % Goal: LHSvar = functor
+ % In this case, LHSvar need not be produced
+ % - it could be a test, so no constraints.
+ Constraints = []
+ )
+
+ ; RHS = lambda_goal(_, _, _, _, _, _, _, _, _),
+ error("build_mode_constraints.m: "
+ ++ "sorry, unify with lambda_goal not implemented.")
+ ).
+
+
+
+
+ % Goal:
+ % G1; ...; Gn where Goals = [G1, ..., Gn]
+ %
+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
+ ]).
+
+
+
+ % Goal:
+ % not (Goal)
+ %
+goal_expr_constraints(ModuleInfo, VarMap, PredID,
+ not(Goal), GoalPath, Nonlocals, 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:
+ % some Xs Goal
+ %
+goal_expr_constraints(ModuleInfo, VarMap, PredID,
+ some(_ExistVars, _CanRemove, Goal),
+ GoalPath, Nonlocals, Constraints) :-
+ Goal = _ - SomeGoalInfo,
+ goal_info_get_goal_path(SomeGoalInfo, SomeGoalPath),
+ Constraints = set.fold(
+ func(NL, NLConstraints) = [
+ atomic_constraint(equivalent([
+ prog_var_at_path(VarMap, PredID, GoalPath, NL),
+ prog_var_at_path(
+ VarMap, PredID, SomeGoalPath, NL
+ )
+ ]))| % If a program variable is produced
+ % by the sub-goal of the some
+ % statement, it is produced at the
+ % main goal as well.
+ NLConstraints
+ ],
+ Nonlocals,
+ SomeGoalConstraints % Include the constraints from the
+ % recursive call on the sub-goal.
+ ),
+ goal_constraints(
+ ModuleInfo, VarMap, PredID, Goal, SomeGoalConstraints
+ ).
+
+
+
+ % Goal:
+ % If -> Then; Else
+ %
+goal_expr_constraints(ModuleInfo, VarMap, PredID,
+ if_then_else(ExistVars, If, Then, Else),
+ GoalPath, Nonlocals, 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
+ ),
+ 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) =
+ atomic_constraint(equivalent(
+ [NLHere, NLAtThen, NLAtElse]
+ )), % If a variable is to be produced
+ % at this path the then and else
+ % parts must be able to produce it.
+ NonlocalsHere,
+ NonlocalsAtThen,
+ NonlocalsAtElse
+ ),
+ list.map(
+ func(Cond) = atomic_constraint(equiv_bool(Cond, no)),
+ NonlocalsAtCond
+ ), % No nonlocal is produced in the condition.
+ list.map_corresponding(
+ (func(LocalAtCond, LocalAtThen) =
+ atomic_constraint(exactly_one(
+ [LocalAtCond, LocalAtThen]
+ ))
+ ),
+ LocalAndSharedAtCond,
+ LocalAndSharedAtThen
+ ), % 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 posibility of checking the variable's
+ % type in the Cond and then binding it in the Then...
+ IfConstraints,
+ ThenConstraints,
+ ElseConstraints
+
+ ]).
+
+ % Foreign procedure
+ %
+goal_expr_constraints(ModuleInfo, VarMap, PredID,
+ foreign_proc(_, CalledPred, ProcID, ForeignArgs, _, _),
+ GoalPath, _Nonlocals, Constraints) :-
+ CallArgs = list.map(foreign_arg_var, ForeignArgs),
+ module_info_pred_proc_info(ModuleInfo, CalledPred, ProcID, _, ProcInfo),
+ ( proc_info_maybe_declared_argmodes(ProcInfo, yes(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.
+ call_mode_decls_constraints(
+ ModuleInfo,
+ VarMap,
+ PredID,
+ [FullDecl],
+ GoalPath,
+ CallArgs,
+ Constraints
+ ) % This pred should strip the disj(conj()) for the
+ % single declaration.
+ ; Constraints = []
+ % XXX Should this be an error?
+ ).
+
+
+ % Parallel conjunction
+ %
+ % XXX What to do here?
+ %
+goal_expr_constraints(_ModuleInfo, _VarMap, _PredID,
+ par_conj(_Goals), _GoalPath, _Nonlocals, _Constraints) :-
+ error("build_mode_constraints.m: "
+ ++ "sorry, par_conj not implemented").
+
+
+ % Shorthand goals. Should not exist at this point in compilation.
+ %
+goal_expr_constraints(_ModuleInfo, _VarMap, _PredID,
+ shorthand(_ShorthandGoalExpr), _GoalPath, _Nonlocals, _Constraints) :-
+ error("build_mode_constraints.m: shorthand goal").
+
+
+
+%-----------------------------------------------------------------------------%
+
+
+
+ % 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.
+ %
+:- 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)).
+
+ % 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 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.
+ %
+:- func prog_var_at_paths(mc_var_map, pred_id, list(goal_path), prog_var) =
+ list(mc_var).
+prog_var_at_paths(VarMap, PredID, GoalPaths, ProgVar) =
+ list.map(
+ func(GoalPath) = bimap.lookup(
+ VarMap,
+ (ProgVar `in` PredID) `at` GoalPath
+ ),
+ GoalPaths
+ ).
+
+ % nonlocals_at_path_and_subpaths(VarMap, GoalPath, SubPaths, Nonlocals,
+ % NonlocalsAtPath, NonlocalsAtSubPaths)
+ % consults the VarMap 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 conjunts), 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 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
+ ),
+ NonlocalsList = set.to_sorted_list(Nonlocals).
+
+
+
+
+%----------------------------------------------------------------------------%
+
+mode_decls_constraints(
+ ModuleInfo, VarMap, PredID, Decls, HeadVarsList, Constraints) :-
+ ConstraintsList = list.map_corresponding(
+ mode_decl_constraints(ModuleInfo),
+ list.map(
+ list.map(prog_var_at_path(VarMap, PredID, [])),
+ HeadVarsList
+ ),
+ Decls
+ ),
+ Constraints0 = list.condense(ConstraintsList),
+ ( Constraints0 = [conj(OneModeOnlyConstraints)]
+ -> Constraints = OneModeOnlyConstraints
+ ; Constraints = [disj(Constraints0)]
+ ).
+
+
+
+
+ % call_mode_decls_constraints(ModuleInfo, VarMap, CallingPred,
+ % Decls, GoalPath, CallArgs, Constraints)
+ %
+ % Returns
+ % 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. Predicate calls for predicates with no declared modes
+ % should not be handled by this - they must be handled elsewhere.
+ %
+ % The constraints for a (call to 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 goal; 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.
+ %
+:- pred call_mode_decls_constraints(module_info::in,
+ mc_var_map::in, pred_id::in, list(list(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
+ ; Constraints = [disj(Constraints0)]
+ ).
+
+
+
+ % 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.
+ %
+:- func mode_decl_constraints(module_info::in, list(mc_var)::in,
+ list(mode)::in) = (mode_constraints::out) is det.
+
+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
+ ),
+ ( not inst_match.inst_is_free(
+ ModuleInfo,
+ InitialInst
+ ) % Already produced.
+ -> IsProduced = no % Not produced here.
+ ; not inst_match.inst_is_free(
+ ModuleInfo,
+ FinalInst
+ ) % free -> non-free
+ -> 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
+ )
+ ; error("build_mode_constraints.m: Too many mode declared args.")
+ ).
+
+
+
+
+
+ % 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.
+ %
+ % 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.
+ %
+:- 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
+ ).
+
+%-----------------------------------------------------------------------------%
+
+ % 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.
+ %
+:- pred fold_goal_into_var_position_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.
+fold_goal_into_var_position_maps(VarMap, PredID, Nonlocals,
+ _SubGoalExpr - SubGoalInfo, !LocalsMap, !NonlocalsMap) :-
+ goal_info_get_nonlocals(SubGoalInfo, SubGoalNonlocals),
+ goal_info_get_goal_path(SubGoalInfo, SubGoalPath),
+ 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)
+ 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.
+ %
+:- pred fold_variable_into_var_position_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 .
+fold_variable_into_var_position_map(
+ VarMap, PredID, GoalPath, ProgVar, !Map) :-
+ MCVar = prog_var_at_path(VarMap, PredID, GoalPath, ProgVar),
+ multi_map.set(!.Map, ProgVar, MCVar, !:Map).
+
+
+ % 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) :-
+ !:Constraints = [
+ atomic_constraint(equiv_disj(ProgVarAtGoalPath, Xs)),
+ atomic_constraint(at_most_one(Xs))|
+ !.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, !Constraints) :-
+ !:Constraints = [
+ atomic_constraint(exactly_one(Xs))|
+ !.Constraints
+ ],
+ Xs = multi_map.lookup(LocalsMap, ProgVar).
Index: compiler/check_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/check_hlds.m,v
retrieving revision 1.7
diff -u -r1.7 check_hlds.m
--- compiler/check_hlds.m 19 Jan 2005 03:10:29 -0000 1.7
+++ compiler/check_hlds.m 1 Feb 2005 04:13:34 -0000
@@ -35,6 +35,8 @@
% 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.
@@ -48,6 +50,7 @@
:- include_module modecheck_call.
:- include_module modecheck_unify.
:- include_module modes.
+ :- include_module new_mode_constraints.
:- include_module unify_proc.
:- include_module unique_modes.
%:- end_module mode_analysis.
Index: compiler/mode_constraints.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mode_constraints.m,v
retrieving revision 1.4
diff -u -r1.4 mode_constraints.m
--- compiler/mode_constraints.m 19 Jan 2005 03:10:46 -0000 1.4
+++ compiler/mode_constraints.m 8 Feb 2005 03:04:04 -0000
@@ -23,6 +23,10 @@
:- implementation.
+:- import_module check_hlds.new_mode_constraints.
+:- import_module check_hlds.abstract_mode_constraints.
+:- import_module check_hlds.build_mode_constraints.
+
:- import_module check_hlds__goal_path.
:- import_module check_hlds__mode_constraint_robdd.
:- import_module check_hlds__mode_ordering.
@@ -42,10 +46,12 @@
:- import_module mode_robdd__tfeirn.
:- import_module parse_tree__prog_data.
:- import_module parse_tree__prog_mode.
+:- import_module parse_tree.prog_io.
+:- import_module parse_tree.modules.
:- import_module transform_hlds__dependency_graph.
:- import_module list, map, std_util, bool, set, multi_map, require, int.
-:- import_module robdd, term, string, assoc_list, sparse_bitset.
+:- import_module robdd, term, string, assoc_list, sparse_bitset, bimap.
:- import_module varset, term_io.
:- import_module gc.
@@ -69,27 +75,68 @@
mode_constraints__process_module(!ModuleInfo, !IO) :-
module_info_predids(!.ModuleInfo, PredIds),
globals__io_lookup_bool_option(simple_mode_constraints, Simple, !IO),
+ globals__io_lookup_bool_option(new_mode_constraints, New, !IO),
list__foldl2(hhf__process_pred(Simple), PredIds, !ModuleInfo, !IO),
get_predicate_sccs(!.ModuleInfo, SCCs),
% Stage 1: Process SCCs bottom-up to determine variable producers.
- list__foldl3(mode_constraints__process_scc(Simple), SCCs,
- !ModuleInfo, map__init, PredConstraintMap, !IO),
-
- % Stage 2: Process SCCs top-down to determine execution order of
- % conjuctions and which modes are needed for each predicate.
- mode_ordering(PredConstraintMap, list__reverse(SCCs),
- !ModuleInfo, !IO),
-
- % Stage 3, which would turn the results of the mode analysis into goal
- % annotations that the rest of the compiler can understand, doesn't
- % exist yet. The whole point of this way of doing mode analysis is
- % to gain extra expressive power (e.g. partially instantiated data
- % structures), and the rest of the compiler doesn't handle the extra
- % expressive power yet.
+ (
+ New = no,
+ list__foldl3(mode_constraints__process_scc(Simple), SCCs,
+ !ModuleInfo, map__init, PredConstraintMap, !IO),
+
+ % Stage 2: Process SCCs top-down to determine execution order of
+ % conjuctions and which modes are needed for each predicate.
+ mode_ordering(PredConstraintMap, list__reverse(SCCs),
+ !ModuleInfo, !IO),
+
+ % Stage 3, which would turn the results of the mode analysis
+ % into goal annotations that the rest of the compiler can
+ % understand, doesn't exist yet. The whole point of this way of
+ % doing mode analysis is to gain extra expressive power (e.g.
+ % partially instantiated data structures), and the rest of the
+ % compiler doesn't handle the extra expressive power yet.
+
+ clear_caches(!IO)
+ ;
+ New = yes,
+ list__foldl3(
+ new_mode_constraints__process_scc(!.ModuleInfo),
+ SCCs,
+ varset.init, ConstraintVarset,
+ bimap.init, _ConstraintVarMap,
+ map.init, AbstractModeConstraints
+ ),
- clear_caches(!IO).
+ hlds_module.module_info_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,
+ AbstractModeConstraints,
+ !IO
+ ),
+ io.set_output_stream(OldOutStream, _, !IO),
+ io.close_output(OutputStream, !IO)
+ ;
+ IOResult = error(_),
+ error("mode_constraints.m: failed to open " ++
+ FileName ++ " for output.")
+ )
+ ).
:- pred mode_constraints__process_scc(bool::in, list(pred_id)::in,
module_info::in, module_info::out,
Index: compiler/new_mode_constraints.m
===================================================================
RCS file: compiler/new_mode_constraints.m
diff -N compiler/new_mode_constraints.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ compiler/new_mode_constraints.m 8 Feb 2005 03:17:10 -0000
@@ -0,0 +1,308 @@
+%-----------------------------------------------------------------------------%
+% 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: new_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. 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.
+%
+
+:- module check_hlds.new_mode_constraints.
+:- interface.
+
+:- import_module hlds__hlds_module.
+:- import_module check_hlds.build_mode_constraints.
+:- import_module check_hlds.abstract_mode_constraints.
+:- import_module hlds.hlds_pred.
+:- import_module list, map, io.
+
+
+
+
+ % 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).
+
+ % 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.
+ %
+:- pred pretty_print_pred_constraints_map(
+ module_info::in,
+ mc_varset::in,
+ pred_constraints_map::in,
+ io::di, io::uo
+ ) is det.
+
+
+:- implementation.
+
+
+:- import_module check_hlds__goal_path.
+:- 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_goal.
+:- import_module hlds__hlds_pred.
+:- import_module hlds__inst_graph.
+:- import_module hlds__passes_aux.
+:- import_module libs__globals.
+:- import_module libs__options.
+:- import_module mode_robdd.
+:- import_module parse_tree__prog_data.
+:- import_module parse_tree__prog_mode.
+:- import_module parse_tree.modules.
+:- import_module transform_hlds__dependency_graph.
+
+:- import_module map, std_util, bool, set, multi_map, require, int.
+:- import_module robdd, term, string, assoc_list, sparse_bitset.
+:- import_module bimap, varset, term_io.
+:- import_module gc.
+
+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
+ foldl3(process_pred(ModuleInfo), SCC, !Varset, !VarMap, !Constraints).
+
+
+
+
+
+ % Performs a number of tasks for one predicate:
+ % 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
+ %
+ % 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.
+
+
+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
+ %
+:- 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.
+
+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 disjuction 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.
+ goal_path.fill_slots_in_clauses(ModuleInfo, GoalPathOptimisation,
+ PredInfo0, PredInfo),
+
+ pred_info_procedures(PredInfo, ProcTable),
+ % Needed for defined modes.
+ pred_info_clauses_info(PredInfo, ClausesInfo),
+ clauses_info_headvars(ClausesInfo, HeadVars),
+ clauses_info_clauses(ClausesInfo, Clauses),
+ clauses_info_varset(ClausesInfo, ProgVarset),
+ Goals = list.map(
+ func(clause(_, ClauseBody, _, _)) = ClauseBody,
+ Clauses
+ ),
+
+ % Here build goal constraint vars.
+ 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(ArgModes0)
+ ),
+ 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_info's.
+
+ ( 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.
+ ;
+ Goals = [_| _],
+ MainGoal = disj(Goals),
+ MainGoalPath = [],
+ Nonlocals = set.list_to_set(HeadVars),
+ goal_expr_constraints(
+ ModuleInfo, !.VarMap, PredID, MainGoal,
+ MainGoalPath, Nonlocals, GoalConstraints
+ )
+ ),
+ PredConstraints = list.append(ModeDeclConstraints, GoalConstraints),
+ map.det_insert(!.Constraints, PredID, PredConstraints, !:Constraints).
+
+
+
+
+ % Put the constraints to the current output stream in human readable
+ % format. It titles each pred's constraints with a module
+ % qualification based on the default filename for the module followed
+ % by the predicate's name.
+ %
+pretty_print_pred_constraints_map(
+ ModuleInfo, ConstraintVarset, PredConstraintsMap, !IO) :-
+ ConstrainedPreds = map.keys(PredConstraintsMap),
+ list.foldl(
+ 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
+ % readable format.
+ %
+:- pred pretty_print_pred_constraints(
+ module_info::in, mc_varset::in, pred_constraints_map::in,
+ pred_id::in, io::di, io::uo
+ ) is det.
+
+pretty_print_pred_constraints(
+ ModuleInfo, ConstraintVarset, PredConstraintsMap, PredID, !IO) :-
+ io.print("\nConstraints for pred ", !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.print(FullPredNameString, !IO),
+ io.print(":\n", !IO),
+
+ map.lookup(
+ PredConstraintsMap,
+ PredID,
+ PredConstraints
+ ),
+ abstract_mode_constraints.pretty_print_constraints(
+ ConstraintVarset,
+ PredConstraints,
+ !IO
+ ).
Index: compiler/options.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/options.m,v
retrieving revision 1.441
diff -u -r1.441 options.m
--- compiler/options.m 27 Jan 2005 03:38:09 -0000 1.441
+++ compiler/options.m 1 Feb 2005 02:24:02 -0000
@@ -174,6 +174,7 @@
; dump_rl_bytecode
; mode_constraints
; simple_mode_constraints
+ ; new_mode_constraints
; benchmark_modes
; benchmark_modes_repeat
; sign_assembly
@@ -843,6 +844,7 @@
dump_rl_bytecode - bool(no),
mode_constraints - bool(no),
simple_mode_constraints - bool(no),
+ new_mode_constraints - bool(no),
benchmark_modes - bool(no),
benchmark_modes_repeat - int(1),
sign_assembly - bool(no),
@@ -1504,6 +1506,7 @@
long_option("generate-schemas", generate_schemas).
long_option("mode-constraints", mode_constraints).
long_option("simple-mode-constraints", simple_mode_constraints).
+long_option("new-mode-constraints", new_mode_constraints).
long_option("benchmark-modes", benchmark_modes).
long_option("benchmark-modes-repeat", benchmark_modes_repeat).
cvs diff: Diffing compiler/notes
Index: compiler/notes/compiler_design.html
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/notes/compiler_design.html,v
retrieving revision 1.96
diff -u -r1.96 compiler_design.html
--- compiler/notes/compiler_design.html 22 Jan 2005 06:10:54 -0000 1.96
+++ compiler/notes/compiler_design.html 2 Feb 2005 04:44:43 -0000
@@ -657,6 +657,24 @@
</ul>
<p>
+<dt> new constraint based mode analysis
+
+ <dd> This is an new alternative
+ for the constraint based mode analysis algorithm.
+ It works by building a system of boolean constraints
+ about where variables can be bound,
+ but does not solve those constraints as yet.
+
+ <ul>
+ <li> new_mode_constraints.m is the interface to the old
+ mode_constraints.m. It builds constraints for an SCC.
+ <li> build_mode_constraints.m is the module that traverses a predicate
+ to build constraints for it.
+ <li> abstract_mode_constraints.m describes data structures for the
+ constraints themselves.
+ </ul>
+ <p>
+
<dt> indexing and determinism analysis
<dd>
cvs diff: Diffing debian
cvs diff: Diffing deep
cvs diff: Diffing deep_profiler
cvs diff: Diffing deep_profiler/notes
cvs diff: Diffing detail
cvs diff: Diffing doc
cvs diff: Diffing extras
cvs diff: Diffing extras/aditi
cvs diff: Diffing extras/cgi
cvs diff: Diffing extras/complex_numbers
cvs diff: Diffing extras/complex_numbers/samples
cvs diff: Diffing extras/complex_numbers/tests
cvs diff: Diffing extras/concurrency
cvs diff: Diffing extras/concurrency/samples
cvs diff: Diffing extras/concurrency/samples/midi
cvs diff: Diffing extras/concurrency/tests
cvs diff: Diffing extras/curs
cvs diff: Diffing extras/curs/samples
cvs diff: Diffing extras/curses
cvs diff: Diffing extras/curses/sample
cvs diff: Diffing extras/dynamic_linking
cvs diff: Diffing extras/error
cvs diff: Diffing extras/exceptions
cvs diff: Diffing extras/graphics
cvs diff: Diffing extras/graphics/easyx
cvs diff: Diffing extras/graphics/easyx/samples
cvs diff: Diffing extras/graphics/mercury_glut
cvs diff: Diffing extras/graphics/mercury_opengl
cvs diff: Diffing extras/graphics/mercury_tcltk
cvs diff: Diffing extras/graphics/samples
cvs diff: Diffing extras/graphics/samples/calc
cvs diff: Diffing extras/graphics/samples/gears
cvs diff: Diffing extras/graphics/samples/maze
cvs diff: Diffing extras/graphics/samples/pent
cvs diff: Diffing extras/lazy_evaluation
cvs diff: Diffing extras/lazy_evaluation/examples
cvs diff: Diffing extras/lex
cvs diff: Diffing extras/lex/samples
cvs diff: Diffing extras/lex/tests
cvs diff: Diffing extras/logged_output
cvs diff: Diffing extras/moose
cvs diff: Diffing extras/moose/samples
cvs diff: Diffing extras/moose/tests
cvs diff: Diffing extras/morphine
cvs diff: Diffing extras/morphine/non-regression-tests
cvs diff: Diffing extras/morphine/scripts
cvs diff: Diffing extras/morphine/source
cvs diff: Diffing extras/odbc
cvs diff: Diffing extras/opium_m
cvs diff: Diffing extras/opium_m/non-regression-tests
cvs diff: Diffing extras/opium_m/scripts
cvs diff: Diffing extras/opium_m/source
cvs diff: Diffing extras/posix
cvs diff: Diffing extras/quickcheck
cvs diff: Diffing extras/quickcheck/tutes
cvs diff: Diffing extras/references
cvs diff: Diffing extras/references/samples
cvs diff: Diffing extras/references/tests
cvs diff: Diffing extras/stream
cvs diff: Diffing extras/trailed_update
cvs diff: Diffing extras/trailed_update/samples
cvs diff: Diffing extras/trailed_update/tests
cvs diff: Diffing extras/xml
cvs diff: Diffing extras/xml/samples
cvs diff: Diffing extras/xml_stylesheets
cvs diff: Diffing java
cvs diff: Diffing java/library
cvs diff: Diffing java/runtime
cvs diff: Diffing library
cvs diff: Diffing lp_solve
cvs diff: Diffing lp_solve/lp_examples
cvs diff: Diffing mdbcomp
cvs diff: Diffing profiler
cvs diff: Diffing quickcheck
cvs diff: Diffing quickcheck/tutes
cvs diff: Diffing readline
cvs diff: Diffing readline/doc
cvs diff: Diffing readline/examples
cvs diff: Diffing readline/shlib
cvs diff: Diffing readline/support
cvs diff: Diffing robdd
cvs diff: Diffing runtime
cvs diff: Diffing runtime/GETOPT
cvs diff: Diffing runtime/machdeps
cvs diff: Diffing samples
cvs diff: Diffing samples/c_interface
cvs diff: Diffing samples/c_interface/c_calls_mercury
cvs diff: Diffing samples/c_interface/cplusplus_calls_mercury
cvs diff: Diffing samples/c_interface/mercury_calls_c
cvs diff: Diffing samples/c_interface/mercury_calls_cplusplus
cvs diff: Diffing samples/c_interface/mercury_calls_fortran
cvs diff: Diffing samples/c_interface/simpler_c_calls_mercury
cvs diff: Diffing samples/c_interface/simpler_cplusplus_calls_mercury
cvs diff: Diffing samples/diff
cvs diff: Diffing samples/muz
cvs diff: Diffing samples/rot13
cvs diff: Diffing samples/solutions
cvs diff: Diffing samples/tests
cvs diff: Diffing samples/tests/c_interface
cvs diff: Diffing samples/tests/c_interface/c_calls_mercury
cvs diff: Diffing samples/tests/c_interface/cplusplus_calls_mercury
cvs diff: Diffing samples/tests/c_interface/mercury_calls_c
cvs diff: Diffing samples/tests/c_interface/mercury_calls_cplusplus
cvs diff: Diffing samples/tests/c_interface/mercury_calls_fortran
cvs diff: Diffing samples/tests/c_interface/simpler_c_calls_mercury
cvs diff: Diffing samples/tests/c_interface/simpler_cplusplus_calls_mercury
cvs diff: Diffing samples/tests/diff
cvs diff: Diffing samples/tests/muz
cvs diff: Diffing samples/tests/rot13
cvs diff: Diffing samples/tests/solutions
cvs diff: Diffing samples/tests/toplevel
cvs diff: Diffing scripts
cvs diff: Diffing tools
cvs diff: Diffing trace
cvs diff: Diffing trax
cvs diff: Diffing trial
cvs diff: Diffing util
cvs diff: Diffing vim
cvs diff: Diffing vim/after
cvs diff: Diffing vim/ftplugin
cvs diff: Diffing vim/syntax
--------------------------------------------------------------------------
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