% This should give people an idea for where and what I am up to. It basically % sets out a plan for changes to the mode constraints module. Comments welcome. % If you want a better explanation just ask :) % The mode_constraints module contains a new approach to mode analysis set % out by dmo in chapter six of his thesis "Precise and Expressive Mode Systems % for Typed Logic Programming Languages" and the paper "Constriant based mode % analysis of Mercury" both available on the papers page of the mercury % website. % % It associates each program variable a set of boolean variables describing % where it has been bound and where it is free, and builds constraints % between all such variables based on the program. By solving these constraints % it can form a partial order for all goals in a conjunct infer modes and % check declarations. (The next step is to order then conjuncts, but that is % beyond the scope of my work). % % Mercury code for building constriants and solving them using ROBDDs already % exists, however this has proved to be an order of magnitude slower than the % existing mode analysis system. It has been hypothesised that a propagation % based solver using less generic constraints more specific to the types % of constraints mode analysis deals with can do a better job. % % In the first case, I intend to work with existing code to build more % abstract constraints for mode analysis. The constraints will take the % form of the data structure mc_constraint(T) set out below. % % Once this is done the constraints can be converted to various forms and % solved with existing solvers for testing purposes. % % The final goal will be to build a propagation based solver that deals with % these new constraints. The rough form this will take is described below % with some example data structures that would form the core of the approach. % :- module mc_structure. :- interface. :- import_module term, list, bool. :- type mc_type. :- type vars(T) == list(var(T)). %------------------------------------------------------------------------------ % % These I have set forth for the construction of constraints % :- type mc_constraints == mc_constraints(mc_type). :- type mc_constraints(T) == list(mc_constraint(T)). :- type mc_constraint == mc_constraint(mc_type). % This set of constraints is designed to completely represent all the % constraints for mode analysis in chapter 6 of the aforementioned thesis % and the paper on constraint mode analysis. They are complicated enough % that I won't go into them here, but for those who are familiar with the % work, you may want to check that these will cover all cases. :- type mc_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(A, B) gives A->B ; equiv_disj(var(T), vars(T)) % equiv_disj(X, [Y1,...,Yn]) gives X<->OR(Y1,...,Yn) ; at_most_one(vars(T)) % at_most_one(Xs) gives % (all Xi, Xj in Xs).(i = j or not(Xi and Xj)) ; disj(mc_constraints(T)) % This has been 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 fail or false . ; conj(mc_constraints(T)) % See disj. % Note that conj([]) is the empty constraint, or true. . %------------------------------------------------------------------------------ % % The following are intended for the solver. % % Here is the basic functioning of the solver. Constraints should be built % and annotated with the variables that participate in them. Each constraint % is given a unique id to identify it. Variables are similarly annotated with % the constraints that refer to them. % % Whenever a variable is bound its effect is propagated in the following % manner: % ConstraintInfo^var_map is consulted to find the constraints this variable % occured in. The binding of this variable may imply many other bindings % based on these constraints, and these should be made and their propagation % scheduled. It may also result in the simplifying of a constraint, and or % the construction of new annotations, the details of which are to be % decided. If the constraints are found to be inconsistant with the binding, % either backtracking is required or a mode error has occured. % % % The idea is that initially the constraints will imply that a certain set % of variables should be bound immediately. This can be done and the % propagation for each scheduled and performed, possibly resulting in more % propagation and so on and so forth. Once all that can be bound like this % can be, there are a number of options. The obvious is to start creating % choicepoints by binding single variables arbitrarily, propagating the % results, and repeating until all variables are bound and consistant with % constraints. The forced backtracking of solutions() could be used to find % all such solutions. In this case greater speed may be accomplished by % choosing to bind the variable which has most constraints associated % with it. A different approach might be to take all the variables constrained % to true or false in one branch of a disjunctive constraint, and bind them % as a lump (the choice of branch being another choicepoint). This could % result in more propagation than the most-constrained-single-variable % approach. Futhermore, if the program is segmented into parts (SCCs) as it % currently is, calls to already processed SCCs can be used to bind a large % number of variables taken out of one of the solution sets of for that SCC % (the choice of solution set being another choicepoint). :- type mc_binary_annotation == mc_binary_annotation(mc_type). :- type mc_binary_annotation(T) ---> binding_implication(var(T), bool, var(T), bool). % binding_implication(X, Xval, Y, Yval) indicates that % if X has been bound to Xval, this can by propagated % by binding Y to Yval :- type constraint_id == int. :- type constraint == constraint(mc_type). % Note the potential to slip the binary constraint annotations in here as % a new field. I havn't done it yet as I'm not sure yet whether they'll % be used or not. :- type constraint(T) ---> constraint( mc_constraint :: mc_constraint(T), % The original constraint cur_mc_constraint :: mc_constraint(T), % As bindings are made, propagation can be % performed not just through variables but through % constraints, simplifying them. participating_vars :: vars(T), cur_participating_vars :: vars(T), id :: constraint_id ). :- type var_state ---> var_state( is_bound :: maybe(bool), is_constrained :: list(constraint_id) ). :- import_module counter. :- type constraint_info ---> constraint_info( constraint_map :: map(constraint_id, constraint(mc_type)), % Stores the constraints. Maps them to their ids var_map :: map(var(mc_type), var_state), % Maps each variable to the constraints it % participates in, and whether it is bound counter :: counter % To keep track of constraint_id's as the constraints % are added. ). :- implementation. :- type mc_type ---> mc_type. % % -richardf % r.fothergill@ugrad.unimelb.edu.au -------------------------------------------------------------------------- mercury-developers mailing list Post messages to: mercury-developers@cs.mu.oz.au Administrative Queries: owner-mercury-developers@cs.mu.oz.au Subscriptions: mercury-developers-request@cs.mu.oz.au --------------------------------------------------------------------------