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

