[m-rev.] for review: new termination analyser (part 2 of 6)

[Mark Brown]

On 24-Mar-2005, Julien Fischer <juliensf at cs.mu.OZ.AU> wrote:
> 
> ===================================================================
> RCS file: compiler/lp_rational.m
> diff -N compiler/lp_rational.m
> --- /dev/null	1 Jan 1970 00:00:00 -0000
> +++ compiler/lp_rational.m	23 Mar 2005 22:47:32 -0000

> +%-----------------------------------------------------------------------------%
> +%
> +% file: lp_rational.m
> +% main authors: conway, juliensf, vjteag.
> +%
> +% This module contains code for creating and manipulating systems of rational
> +% linear arithmetic constraints.  It provides the following operations:
> +%
> +% * optimization (using the simplex method)
> +%
> +% * projection (using Fourier elimination).
> +%
> +% * an entailment test (using the above linear optimizer above.)

Remove one of the "above"s.

> +:- func lp_rational.simplify_constraints(constraints) = constraints.

This needs documentation.

> +    % substitute_vars(VarsA, VarsB, Constraints0) = Constraints.
> +    % If length(VarsA) \= length(VarsB) then an exception is thrown.

You should state what the function does (that is, do occurrences of VarsA
get replaced with VarsB or vice-versa).

> +    % NOTE: this does does not always detect that a constraint
> +    % set is inconsistent, so callers to this procedure may need
> +    % to do a consistency check on the result if they require
> +    % the resulting system of constraints to be consistent.

s/does does/does/

> +%------------------------------------------------------------------------------%
> +%
> +% Entailment.
> +%
> +
> +:- type entailment_result
> +    --->    entailed
> +    ;       not_entailed
> +    ;       inconsistent.
> +
> +    % entailed(Vars , Vars):

The arguments here aren't right.

> +    % Determines if the constraint `C' is implied by the set of
> +    % constraints `Cs'. Uses the simplex method to find the point `P'
> +    % satisfying `Cs' which maximizes (if `C' contains '=<') or minimizes
> +    % (if `C' contains '>=') a function parallel to `C'.
> +    % Then tests if `P' satisfies `C'.
> +    % This assumes that all the variables are non-negative.
> +    % Throws an exception if `Cs' is inconsistent.
> +    %
> +:- pred lp_rational.entailed(lp_varset::in, constraints::in,
> +    constraint::in) is semidet.
> +
> +:- func lp_rational.entailed(lp_varset, constraints, constraint) =
> +    entailment_result.

The function needs a comment.  Does it ever return 'inconsistent', or
throw an exception?

> +%------------------------------------------------------------------------------%
> +%
> +% Stuff for intermodule optimization.
> +%
> +
> +    % A function that converts an lp_var into a string.
> +    %
> +:- type output_var == (func(lp_var) = string).
> +:- inst output_var == (func(in) = out is det).
> +
> +    % Write out the constraints in a form we can read in using the
> +    % term parser from the standard library.
> +    %
> +:- pred lp_rational.output_constraints(output_var::in(output_var),
> +    constraints::in, io::di, io::uo) is det.

You may no longer need the output_var inst, since it is the default.

> +nonneg_constr(lte([_ - (-rat.one)], rat.zero)).
> +nonneg_constr(gte(_, _)) :-
> +    throw("nonneg_constr/1: get.").

s/get/gte encountered/

> +    % Sort the list of terms in ascending order by variable
> +    % and then multiply through so that the first term has a
> +    % coefficient of one or negative one.  If the first argument
> +    % is `yes' then we multiply through by the reciprocal of the
> +    % absolute value of the coefficient, otherwise we multiply through
> +    % by the value.

s/by the value/by the reciprocal of the value/

> +    % Succeeds iff the constraint is implied by the
> +    % assumption that all variables are non-negative *and* the constraint
> +    % is not one used to force non-negativity of the variables.
> +    %
> +:- pred obvious_constraint(constraint::in) is semidet.
> +
> +obvious_constraint(lte(Terms, Constant)) :-
> +    Constant >= rat.zero,
> +    list.length(Terms) >= 2,
> +    all [Term] list.member(Term, Terms) => snd(Term) < zero.

Technically, that should be 'snd(Term) =< zero', although it doesn't really
matter since there shouldn't be zero coefficients anyway.

> +
> +obvious_constraint(gte(Terms, Constant)) :-
> +    Constant =< rat.zero,
> +    list.length(Terms) >= 2,
> +    all [Term] list.member(Term, Terms) => snd(Term) > zero.

Similarly here.

> +%------------------------------------------------------------------------------%
> +%
> +% Predicates for eliminating equations from the constraints.
> +% (Gaussian elimination)
> +%
> +
> +% Split the constraints into a set of inequalities and a set of
> +% equalities.  For every variable in the set of target variables (ie.
> +% those we are eliminating), check if there is at least one equality
> +% that contains that variable.  If then substitute the value of that
> +% variable into the other constraints.

s/If then/If so then/

You should state what happens if there are no equalities containing that
variable.

> +    % The `Flag' argument is `yes' if a one or more substitutions was made,

s/if a one/if one/
s/was/were/

> +fourier_elimination([], _, _, _, Matrix, yes(Matrix)).
> +fourier_elimination(Vars @ [Var0 | Vars0], Varset, MaybeThreshold, !.Step,
> +        Matrix0, Result) :-
> +    %
> +    % Use Duffin's heuristic to try and find a "nice" variable eliminate.

s/variable eliminate/variable to eliminate/

> +    % normalize_vector(Var, Terms0, Const0, Terms, Const).
> +    % Converts a vector, broken up into `Terms0' and `Const0', into a
> +    % parallel one where the coefficient of `Var' is +/- one.
> +    % Throws an exception if the map contains a zero coefficient for `Var'.

This comment is a bit misleading.  You should reword it to be more like the
comment above normalize_constraint/3.

> +%------------------------------------------------------------------------------%
> +%------------------------------------------------------------------------------%
> +%
> +% Entailment test.
> +%
> +
> +    % entailed(C, Cs, Vars).

The arguments aren't right here, either.

> +    % Determines if the constraint `C' is implied by the set of
> +    % constraints `Cs'.  Uses the simplex method to find the point `P'
> +    % satisfying `Cs' which maximizes (or minimizes if `C' contains `>=' )
> +    % a function parallel to `C'.  Then tests whether `P' satisfies `C'.
> +    % This assumes that all the variables are non-negative.

This whole comment should be merged with the one in the interface.

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