[m-dev.] Comments on commenting?

[Richard James FOTHERGILL]

Before I finish with this, I was hoping someone could give some constructive 
criticism on my comments - what should I add/remove and most importantly what 
needs rewording (there may be a lot of that).

Come to think of it, I havn't added any comments to mode_constraints.m,
the only changes are to incorporate  my code, but I'll include a diff anyway so 
you can see where my code fits in. The modules I've done
are new_mode_constraints, build_mode_constraints and abstract_mode_constraints.



Cheers,
-richardf





Index: mode_constraints.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mode_constraints.m,v
retrieving revision 1.4
diff -r1.4 mode_constraints.m
25a26,29
> :- import_module check_hlds.new_mode_constraints.
> :- import_module check_hlds.abstract_mode_constraints.
> :- import_module check_hlds.build_mode_constraints.
> 
44a49,50
> :- import_module parse_tree.prog_io.
> :- import_module parse_tree.modules.
48c54
< :- import_module robdd, term, string, assoc_list, sparse_bitset.
---
> :- import_module robdd, term, string, assoc_list, sparse_bitset, bimap.
71a78
> 	globals__io_lookup_bool_option(new_mode_constraints, New, !IO),
77,90c84,110
< 	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,
> 			[], AbstractModeConstraints
> 		),
92c112,135
< 	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),
> 			abstract_mode_constraints.pretty_print_constraints(
> 				ConstraintVarset,
> 				AbstractModeConstraints,
> 				!IO
> 			),
> 			io.set_output_stream(OldOutStream, _, !IO),
> 			io.close_output(OutputStream, !IO)
> 		;	IOResult = error(_)
> 				% XXX What to do here?
> 		)
> 	).





%-----------------------------------------------------------------------------%
% 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.

:- pred process_scc(
 	module_info::in, list(pred_id)::in,
 	mc_varset::in, mc_varset::out,
 	mc_var_map::in, mc_var_map::out,
 	mode_constraints::in, mode_constraints::out
 	) 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 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 varset, term_io.
:- import_module gc.

process_scc(ModuleInfo, SCC, !Varset, !VarMap, !Constraints) :-

 		% 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,
 	mode_constraints::in, mode_constraints::out
 	) is det.

process_pred(ModuleInfo, PredID, !Varset, !VarMap, !Constraints) :-
 	module_info_pred_info(ModuleInfo, PredID, PredInfo0),


 		% 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(ProgVarset), Goals, !Varset, !VarMap),

 		% Here check for mode declarations and add apppropriate
 		% constraints.
 	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 declared modes, no constraints
 		ModeDeclConstraints = []
 	;	ArgModeDecls = [_|_],	% Some declared modes
 		call_mode_decls_constraints(
 			ModuleInfo,
 			ArgModeDecls,
 			!.VarMap,
 			MainGoalPath,
 			HeadVars,
 			ModeDeclConstraints
 		)
 	),
 	!:Constraints = list.append(ModeDeclConstraints, !.Constraints),
 		% Don't worry too much about this append - the mode
 		% declaration constraints should be a singleton list at most.


 		% This builds the constraints for this predicate. Note that the
 		% main goal may need to be temporarily formed by putting
 		% clauses into a disjunction. XXX However, the conversion to
 		% hhf should make this unnecessary, in which case change to a
 		% call to goal_constraints for what should be a singleton list,
 		% Goals.
 	MainGoal = disj(Goals),
 	MainGoalPath = [],
 	Nonlocals = set.list_to_set(HeadVars),
 	goal_expr_constraints(
 		ModuleInfo, !.VarMap, MainGoal,
 		MainGoalPath, Nonlocals, GoalConstraints
 	),
 	!:Constraints = list.append(GoalConstraints, !.Constraints).
 		% XXX This append is wasteful. Consider expanding all the
 		% constraints predicates in build_mode_constraints
 		% to use state variables for constraints, and fold rather
 		% than append.





build_mode_constraints.m
(I should include the filename in the comment header)



%-----------------------------------------------------------------------------%
% 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.
%-----------------------------------------------------------------------------%
%
% 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


:- 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.
 	%
 	% 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).


 	% 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 --->
 	prog_var `at` goal_path.


 	% For each head variable of each predicate in the supplied SCC, this
 	% predicate adds to the varset the constraint variable for
 	% HeadVariable `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(
 	prog_varset::in,
 	hlds_goal::in,
 	mc_varset::in, mc_varset::out,
 	mc_var_map::in, mc_var_map::out
 	) is det.



 	% call_mode_decls_constraints(ModuleInfo, Decls, VarMap, GoalPath,
 	% 	CallArgs, Constraints) 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 cannont 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, list(list(mode))::in,
 	mc_var_map::in, goal_path::in, args::in, mode_constraints::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,
 	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(ProgVarset),
 		Headvars,
 		!Varset,
 		!VarMap
 	),
 	add_mc_vars_for_scc_heads(ModuleInfo, PredIDs, !Varset, !VarMap).


 	% 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(
 	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(ProgVarset, HeadVar, !Varset, !VarMap) :-
 	RepVar = HeadVar `at` [],
 	(	bimap.search(!.VarMap, RepVar, _)
 	->	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(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 `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(ProgVarset),
 			Goals,
 			!Varset,
 			!VarMap
 		)
 	;	GoalExpr = call(_, _, _, _, _, _)
 			% XXX The headvars of the called pred?
 			% Maybe not - this predicate is concerned cheifly
 			% with the current goal paths - let the headvars
 			% have their constraint variables defined in a
 			% separate predicate (and do them All first before
 			% building constraints for a particular predicate).
 	;	GoalExpr = generic_call(_, _, _, _)
 	;	GoalExpr = switch(_, _, Cases),
 		Goals = list.map(func(case(_, Goal)) = Goal, Cases),
 		list.foldl2(
 			add_mc_vars_for_goal(ProgVarset),
 			Goals,
 			!Varset,
 			!VarMap
 		)
 	;	GoalExpr = unify(_, _, _, _, _)
 	;	GoalExpr = disj(Goals),
 		list.foldl2(
 			add_mc_vars_for_goal(ProgVarset),
 			Goals,
 			!Varset,
 			!VarMap
 		)
 	;	GoalExpr = not(Goal),
 		add_mc_vars_for_goal(ProgVarset, Goal, !Varset, !VarMap)
 	;	GoalExpr = some(_, _, Goal),
 		add_mc_vars_for_goal(ProgVarset, Goal, !Varset, !VarMap)
 	;	GoalExpr = if_then_else(_, Cond, Then, Else),
 		Goals = [Cond, Then, Else],
 		list.foldl2(
 			add_mc_vars_for_goal(ProgVarset),
 			Goals,
 			!Varset,
 			!VarMap
 		)
 	;	GoalExpr = foreign_proc(_, _, _, _, _, _)
 	;	GoalExpr = par_conj(_Goals)
%		list.foldl2(
%			add_mc_vars_for_goal(ProgVarset),
%			Goals,
%			!Varset,
%			!VarMap
%		)	% XXX Not dealing with this?
 	;	GoalExpr = shorthand(_ShorthandGoalExpr)
 	).



 	% 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 at GoalPath"
 	%
:- func rep_var_to_string(prog_varset::in, mc_rep_var::in) =
 	(string::out) is det.

rep_var_to_string(ProgVarset, ProgVar `at` GoalPath) = RepString :-
 	goal_path_to_string(GoalPath, GoalPathString),
 	varset.lookup_name(ProgVarset, ProgVar, 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,
 	hlds_goal::in,
 	mode_constraints::out
 	) is det.

goal_constraints(ModuleInfo, VarMap, GoalExpr - GoalInfo, Constraints) :-
 	goal_info_get_nonlocals(GoalInfo, Nonlocals),
 	goal_info_get_goal_path(GoalInfo, GoalPath),
 	goal_expr_constraints(
 		ModuleInfo,
 		VarMap,
 		GoalExpr,
 		GoalPath,
 		Nonlocals,
 		Constraints
 	).




 	% Goal:
 	% G1, ..., Gn where Goals = [G1, ..., Gn]
 	%
goal_expr_constraints(ModuleInfo, VarMap,
 	conj(Goals), GoalPath, Nonlocals, Constraints) :-

 	list.map(
 		goal_constraints(ModuleInfo, VarMap),
 		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,
 			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, 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,
 	call(PredID, _ProcID, Args, _Builtin, _UnifyContext, _Name),
 	GoalPath, _Nonlocals, Constraints) :-

 		% Get the declared modes (if any exist)
 	module_info_pred_info(ModuleInfo, PredID, 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(
 			HeadVars, VarMap, GoalPath, Args, Constraints
 		)
 	;	ArgModeDecls = [_| _],
 			% At least one declared mode
 		call_mode_decls_constraints(
 			ModuleInfo,
 			ArgModeDecls,
 			VarMap,
 			GoalPath,
 			Args,
 			Constraints
 		)
 	).

 	% XXX Need to do something here. Constraints maybe, or maybe an error.
 	%
goal_expr_constraints(_ModuleInfo, _VarMap,
 	generic_call(_, _, _, _), _GoalPath, _Nonlocals, []).


 	% XXX Need to do something here. Constraints maybe, or maybe an error.
 	%
goal_expr_constraints(_ModuleInfo, _VarMap,
 	switch(_, _, _), _GoalPath, _Nonlocals, []).

 	% Unification Goals
 	%
goal_expr_constraints(_ModuleInfo, VarMap,
 	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, GoalPath, LHSvar),
 				prog_var_at_path(VarMap, 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, GoalPath, LHSvar),
 		ArgsProducedHere =
 			list.map(prog_var_at_path(VarMap, GoalPath), Args),
 		(	ArgsProducedHere = [FirstArgProducedHere| _],
 				% 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,
 					FirstArgProducedHere
 				]))		% 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(_, _, _, _, _, _, _, _, _),
 			% XXX To be completed.
 		Constraints = []
 	).




 	% Goal:
 	% G1; ...; Gn where Goals = [G1, ..., Gn]
 	%
goal_expr_constraints(ModuleInfo, VarMap,
 	disj(Goals), GoalPath, Nonlocals, Constraints) :-

 	nonlocals_at_path_and_subpaths(
 		VarMap, 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),
 		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,
 	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, GoalPath, Nonlocal),
 			prog_var_at_path(VarMap, NegatedGoalPath, Nonlocal)|
 			MCVars
 		],
 		Nonlocals,
 		[]
 	),
 	goal_constraints(ModuleInfo, VarMap, 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,
 	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, GoalPath, NL),
 				prog_var_at_path(VarMap, 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, Goal, SomeGoalConstraints).



 	% Goal:
 	% If -> Then; Else
 	%
goal_expr_constraints(ModuleInfo, VarMap,
 	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, GoalPath),
 		NonlocalsList
 	),
 	NonlocalsAtCond = list.map(
 		prog_var_at_path(VarMap, CondPath),
 		NonlocalsList
 	),
 	NonlocalsAtThen = list.map(
 		prog_var_at_path(VarMap, ThenPath),
 		NonlocalsList
 	),
 	NonlocalsAtElse = list.map(
 		prog_var_at_path(VarMap, 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, CondPath),
 		ExistVars
 	),
 	LocalAndSharedAtThen = list.map(
 		prog_var_at_path(VarMap, ThenPath),
 		ExistVars
 	),

 	goal_constraints(ModuleInfo, VarMap, If, IfConstraints),
 	goal_constraints(ModuleInfo, VarMap, Then, ThenConstraints),
 	goal_constraints(ModuleInfo, VarMap, 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,
 	foreign_proc(_, PredID, ProcID, ForeignArgs, _, _),
 	GoalPath, _Nonlocals, Constraints) :-
 	CallArgs = list.map(foreign_arg_var, ForeignArgs),
 	module_info_pred_proc_info(ModuleInfo, PredID, ProcID, _, ProcInfo),
 	(	proc_info_maybe_declared_argmodes(ProcInfo, yes(Decl))
 	->	call_mode_decls_constraints(
 			ModuleInfo,
 			[Decl],
 			VarMap,
 			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,
 	par_conj(_Goals), _GoalPath, _Nonlocals, []).


 	% Shorthand goals. Should not exist at this point in compilation.
 	%
 	% XXX What sort of error message?
goal_expr_constraints(_ModuleInfo, _VarMap,
 	shorthand(_ShorthandGoalExpr), _GoalPath, _Nonlocals, []).



%-----------------------------------------------------------------------------%



 	% prog_var_at_path(VarMap, 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 `at` GoalPath does not exist in the map.
 	% :- func prog_var_at_path(mc_var_map, goal_path, prog_var) = (mc_var).
prog_var_at_path(VarMap, GoalPath, ProgVar) =
 	bimap.lookup(VarMap, (ProgVar `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 `at` GoalPath does not exist in the map for any of the
 	% 'GoalPath's in GoalPaths.
 	%
:- func prog_var_at_paths(mc_var_map, list(goal_path), prog_var) =
 	list(mc_var).
prog_var_at_paths(VarMap, GoalPaths, ProgVar) =
 	list.map(
 		func(GoalPath) = bimap.lookup(VarMap, ProgVar `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, 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, GoalPath, SubPaths, Nonlocals,
 	NonlocalsAtPath, NonlocalsAtSubPaths) :-
 	NonlocalsAtPath = list.map(
 		prog_var_at_path(VarMap, GoalPath),
 		NonlocalsList
 	),
 	NonlocalsAtSubPaths = list.map(
 		prog_var_at_paths(VarMap, SubPaths),
 		NonlocalsList
 	),
 	NonlocalsList = set.to_sorted_list(Nonlocals).



%----------------------------------------------------------------------------%



call_mode_decls_constraints(
 	ModuleInfo, Decls, VarMap, GoalPath, CallArgs, Constraints) :-
 	CallArgsHere = list.map(
 		prog_var_at_path(VarMap, 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
 	))].



 	% 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(args::in, mc_var_map::in, 
goal_path::in,
 	args::in, mode_constraints::out) is det.

call_headvar_constraints(HeadVars, VarMap, GoalPath, CallArgs, Constraints) :-
 	HeadVarsHere = list.map(
 		prog_var_at_path(VarMap, GoalPath),
 		HeadVars
 	),
 	CallArgsHere = list.map(
 		prog_var_at_path(VarMap, GoalPath),
 		CallArgs
 	),
 	Constraints = list.map_corresponding(
 		(func(HeadVarHere, CallArgHere) =
 			atomic_constraint(equivalent(
 				[HeadVarHere, CallArgHere]
 			))
 		),
 		HeadVarsHere,
 		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, 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, 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)
 	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, SubGoalPath),
 		Local,
 		!LocalsMap
 	),
 	set.fold(
 		fold_variable_into_var_position_map(VarMap, 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, 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, GoalPath, ProgVar, !Map) :-
 	MCVar = prog_var_at_path(VarMap, 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, 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, NonlocalsMap, GoalPath, ProgVar, !Constraints) :-
 	!:Constraints = [
 		atomic_constraint(equiv_disj(ProgVarAtGoalPath, Xs)),
 		atomic_constraint(at_most_one(Xs))|
 		!.Constraints
 	],
 	ProgVarAtGoalPath = prog_var_at_path(VarMap, 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).







abstract_mode_constraints.m
(I should include the filename in the comment header).



%-----------------------------------------------------------------------------%
% 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.
%-----------------------------------------------------------------------------%
%
% 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(", !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(", !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).





--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------