[m-rev.] for review: rewrite of the state variable transformation

Julien Fischer juliensf at csse.unimelb.edu.au
Fri Mar 4 03:38:30 AEDT 2011


On Wed, 2 Mar 2011, Zoltan Somogyi wrote:

> A rewrite of the state variable transformation from the ground up.
>
> The initial aim was to avoid situations (encountered in the g12 project)
> in which the old state variable transformation generated code that
> did not satisfy the mode checker, due to unnecessary unifications.
> The new system tries hard to minimize the number of unifications added to the
> program. It does this by relying extensively on the idea that in a branched
> structure such as an disjunction, if two branches both update the same state
> variable, and the variables representing the last state of the state variable
> in the two branches are (say) X and Y, and we pick X to represent the current
> state after the disjunction, then we don't have to put the assignment X := Y
> into the second branch; instead, we can RENAME Y to X in that branch.
> To avoid renaming a goal several times (for itself, for its parent, for its
> grandparent etc), we delay all renamings until the end, when we do it all
> in one traversal.
>
> The old state var system was opaque and hard to understand, partly because
> its basic operations did different things in different contexts. The new system
> is a much more direct expression of the intuitive meaning of state variables;
> it keeps track of their state much as the programmer writing the original code
> would. It should therefore be significantly easier to understand and to modify
> in the future.
>
> The new system can also detect more kinds of errors in the use of state
> variables. For example it can discover that some branches of a disjunction or
> if-then-else set the initial value of a state variable and some do not.
> This is ok if the non-setting-branch cannot succeed; if it can, then it is
> a bug. We therefore generate messages about such branches, but print them
> only if mode analysis finds a bug in the procedure, since in that case,
> the lack of initialization may be the cause of the bug.
>
> doc/reference_manual.texi:
> 	Replaced an old example that didn't know what it was talking about,
> 	and thoroughly confused the issue of what is legal use of state
> 	variables and what is not.
>
> compiler/state_var.m:
> 	Rewrite this module along the lines mentioned above.
>
> compiler/options.m:
> 	Add two new options. One, warn-state-var-shadowing, controls whether
> 	we generate warnings for one state var shadowing another (which
> 	G12 has lots of). The other, --allow-defn-for-builtins, is for
> 	developers only; it is needed to bootstrap changes that add new
> 	builtins. I needed this for a form of the state variable transformation
> 	that used calls to a new builtin predicate to copy the values of state
> 	this one.

The end of that last sentence doesn't make any sense.

...

> %-----------------------------------------------------------------------------%
> % vim: ft=mercury ts=4 sw=4 et
> %-----------------------------------------------------------------------------%
> % Copyright (C) 2005-2011 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: state_var.m.

...

> %-----------------------------------------------------------------------------%
> %
> % Handle disjunctions. The algorithm we use has two passes over the disjuncts.
> %
> % - Pass 1 computes finds out, for each state variable known at the start of

Delete one of "computes" or "finds out".

> %   the disjunction, whether it was updated by any arms, and if yes, it picks
> %   the fina, prog_var from one of the updated arms to represent the state var

s/fina/final/

> %   after the disjunction.
> %
> % - Pass two processes the arms to ensure that the picked prog_var represents
> %   the final value of the state variable in all the arms. In arms that do not
> %   update the state variable, it introduces unifications to copy the initial
> %   value of the state var to be the final value. In arms that do update the
> %   state var, it schedules the prog_var representing the final value in
> %   that arm to be renamed to the picked prog_var.
>
> svar_finish_disjunction(_Context, DisjStates, Disjs, !VarSet,
>        StateBefore, StateAfter, !Store) :-

...

> Index: compiler/goal_expr_to_goal.m
> ===================================================================
> RCS file: compiler/goal_expr_to_goal.m
> diff -N compiler/goal_expr_to_goal.m
> --- /dev/null	1 Jan 1970 00:00:00 -0000
> +++ compiler/goal_expr_to_goal.m	1 Mar 2011 06:30:38 -0000

...

> +:- pred transform_goal_expr_to_goal(loc_kind::in, goal_expr::in,
> +    prog_context::in, prog_var_renaming::in, hlds_goal::out,
> +    num_added_goals::out,
> +    svar_state::in, svar_state::out, svar_store::in, svar_store::out,
> +    prog_varset::in, prog_varset::out,
> +    module_info::in, module_info::out, qual_info::in, qual_info::out,
> +    list(error_spec)::in, list(error_spec)::out) is det.
> +

...


> +    ;
> +        Expr = not_expr(SubExpr0),
> +        % svar_prepare_for_negation(Context, BeforeOutsideState,
> +        %     BeforeInsideState),
> +        % transform_goal_expr_context_to_goal(SubExpr0, Renaming, SubGoal,
> +        %     !:NumAdded, BeforeInsideState, AfterInsideState, !SVarStore,
> +        %     !VarSet, !ModuleInfo, !QualInfo, !Specs),
> +        % svar_finish_negation(BeforeOutsideState, AfterInsideState,
> +        %     AfterOutsideState),
> +        % !:SVarState = AfterOutsideState,

Add a comment explaining what this commented out code is for.
(Presumably it implements the behaviour where outside state variables
are readonly inside a negation.)

> +        BeforeOutsideState = !.SVarState,
> +        transform_goal_expr_context_to_goal(LocKind, SubExpr0, Renaming,
> +            SubGoal, !:NumAdded, !.SVarState, _, !SVarStore,
> +            !VarSet, !ModuleInfo, !QualInfo, !Specs),
> +        !:SVarState = BeforeOutsideState,
> +        GoalExpr = negation(SubGoal),
> +        goal_info_init(GoalInfo),
> +        Goal = hlds_goal(GoalExpr, GoalInfo)

...

> +    ;
> +        Expr = equivalent_expr(P0, Q0),
> +        % `P <=> Q' is defined as `(P => Q), (Q => P)',
> +        % but that transformation must not be done until after quantification,
> +        % lest the duplication of the goals concerned affect the implicit
> +        % quantification of the variables inside them.
> +
> +        SVarStateBefore = !.SVarState,
> +        transform_goal_expr_context_to_goal(LocKind, P0, Renaming, P,
> +            NumAddedP, !SVarState, !SVarStore, !VarSet,
> +            !ModuleInfo, !QualInfo, !Specs),
> +        transform_goal_expr_context_to_goal(LocKind, Q0, Renaming, Q,
> +            NumAddedQ, !.SVarState, _, !SVarStore, !VarSet,
> +            !ModuleInfo, !QualInfo, !Specs),
> +        % XXX different from before

What does that XXX mean?

> +        !:SVarState = SVarStateBefore,
> +        !:NumAdded = NumAddedP + NumAddedQ,
> +        GoalExpr = shorthand(bi_implication(P, Q)),
> +        goal_info_init(GoalInfo),
> +        Goal = hlds_goal(GoalExpr, GoalInfo)
> +    ;
> +        Expr = event_expr(EventName, Args0),
> +        expand_bang_states(Args0, Args1),
> +        % XXX svar_prepare_for_call(!SInfo),

These XXX svar_prepare_for_call are sprinkled throughout the remainder
of this predicate, add a note the first one explaining them.

> +        rename_vars_in_term_list(need_not_rename, Renaming, Args1, Args),
> +        make_fresh_arg_vars(Args, HeadVars, !VarSet, !SVarState, !Specs),
> +        list.length(HeadVars, Arity),
> +        list.duplicate(Arity, in_mode, Modes),
> +        goal_info_init(Context, GoalInfo),
> +        Details = event_call(EventName),
> +        GoalExpr0 = generic_call(Details, HeadVars, Modes, detism_det),
> +        Goal0 = hlds_goal(GoalExpr0, GoalInfo),
> +        CallId = generic_call_id(gcid_event_call(EventName)),
> +        insert_arg_unifications(HeadVars, Args, Context, ac_call(CallId),
> +            Goal0, Goal, !:NumAdded, !SVarState, !SVarStore, !VarSet,
> +            !ModuleInfo, !QualInfo, !Specs),
> +        svar_finish_atomic_goal(LocKind, !SVarState)
> +    ;
> +        Expr = call_expr(Name, Args0, Purity),
> +        expand_bang_states(Args0, Args1),
> +        (
> +            Name = unqualified("\\="),
> +            Args1 = [LHS, RHS]
> +        ->
> +            % XXX svar_prepare_for_call(!SVarState),
> +            % `LHS \= RHS' is defined as `not (LHS = RHS)'
> +            TransformedExpr = not_expr(unify_expr(LHS, RHS, Purity) - Context),
> +            transform_goal_expr_to_goal(LocKind, TransformedExpr, Context,
> +                Renaming, Goal, !:NumAdded, !SVarState, !SVarStore, !VarSet,
> +                !ModuleInfo, !QualInfo, !Specs)
> +        ;
> +            % check for a state var record assignment:
> +            % !Var ^ field := Value
> +            Name = unqualified(":="),
> +            Args1 = [LHS0, RHS0],
> +            LHS0 = functor(atom("^"), [StateVar0, Remainder],
> +                FieldListContext),
> +            StateVar0 = functor(atom("!"), Args @ [variable(_, _)],
> +                StateVarContext)
> +        ->
> +            % !Var ^ field := Value is defined as
> +            % !:Var = !.Var ^ field := Value.
> +            LHS = functor(atom("!:"), Args, StateVarContext),
> +            StateVar = functor(atom("!."), Args, StateVarContext),
> +            FieldList = functor(atom("^"), [StateVar, Remainder],
> +                FieldListContext),
> +            RHS = functor(atom(":="), [FieldList, RHS0], Context),
> +            TransformedExpr = unify_expr(LHS, RHS, Purity),
> +            transform_goal_expr_to_goal(LocKind, TransformedExpr, Context,
> +                Renaming, Goal, !:NumAdded, !SVarState, !SVarStore, !VarSet,
> +                !ModuleInfo, !QualInfo, !Specs)
> +        ;
> +            % check for a DCG field access goal:
> +            % get: Field =^ field
> +            % set: ^ field := Field
> +            ( Name = unqualified(Operator) ),
> +            ( Operator = "=^"
> +            ; Operator = ":="
> +            )
> +        ->
> +            rename_vars_in_term_list(need_not_rename, Renaming, Args1, Args2),
> +            transform_dcg_record_syntax(LocKind, Operator, Args2, Context,
> +                Goal, !:NumAdded, !SVarState, !SVarStore, !VarSet,
> +                !ModuleInfo, !QualInfo, !Specs)
> +        ;
> +            % XXX svar_prepare_for_call(!SInfo),
> +            rename_vars_in_term_list(need_not_rename, Renaming, Args1, Args),
> +            make_fresh_arg_vars(Args, HeadVars, !VarSet, !SVarState, !Specs),
> +            list.length(Args, Arity),
> +            (
> +                % Check for a higher-order call,
> +                % i.e. a call to either call/N or ''/N.
> +                ( Name = unqualified("call")
> +                ; Name = unqualified("")
> +                ),
> +                HeadVars = [PredVar | RealHeadVars]
> +            ->
> +                % Initialize some fields to junk.
> +                Modes = [],
> +                Det = detism_erroneous,
> +
> +                GenericCall = higher_order(PredVar, Purity, pf_predicate,
> +                    Arity),
> +                Call = generic_call(GenericCall, RealHeadVars, Modes, Det),
> +
> +                hlds_goal.generic_call_id(GenericCall, CallId)
> +            ;
> +                % Initialize some fields to junk.
> +                PredId = invalid_pred_id,
> +                ModeId = invalid_proc_id,
> +
> +                MaybeUnifyContext = no,
> +                Call = plain_call(PredId, ModeId, HeadVars, not_builtin,
> +                    MaybeUnifyContext, Name),
> +                CallId =
> +                    plain_call_id(simple_call_id(pf_predicate, Name, Arity))
> +            ),
> +            goal_info_init(Context, GoalInfo0),
> +            goal_info_set_purity(Purity, GoalInfo0, GoalInfo),
> +            Goal0 = hlds_goal(Call, GoalInfo),
> +
> +            record_called_pred_or_func(pf_predicate, Name, Arity, !QualInfo),
> +            insert_arg_unifications(HeadVars, Args, Context, ac_call(CallId),
> +                Goal0, Goal, !:NumAdded, !SVarState, !SVarStore, !VarSet,
> +                !ModuleInfo, !QualInfo, !Specs)
> +        ),
> +        svar_finish_atomic_goal(LocKind, !SVarState)
> +    ;

...

> Index: compiler/hlds_goal.m
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/mercury/compiler/hlds_goal.m,v
> retrieving revision 1.221
> diff -u -b -r1.221 hlds_goal.m
> --- compiler/hlds_goal.m	13 Jan 2011 00:36:52 -0000	1.221
> +++ compiler/hlds_goal.m	26 Feb 2011 18:33:23 -0000

...

> +%-----------------------------------------------------------------------------%
> +%
> +% Incremental rename predicates.
> +%
> +
> +incremental_rename_vars_in_goal(Subn0, SubnUpdates, Goal0, Goal) :-
> +    Goal0 = hlds_goal(GoalExpr0, GoalInfo0),
> +    GoalId = goal_info_get_goal_id(GoalInfo0),
> +    ( map.search(SubnUpdates, GoalId, GoalSubns) ->
> +        trace [compiletime(flag("statevar-subn")), io(!IO)] (
> +            GoalId = goal_id(GoalIdNum),
> +            io.format("Goal id %d has substitutions\n", [i(GoalIdNum)], !IO),
> +            io.write(GoalSubns, !IO),
> +            io.nl(!IO)
> +        ),
> +        % XXX map.det_insert_from_assoc_list(Subn0, GoalSubns, Subn)

What is the above XXX supposed to mean?

> +        list.foldl(follow_subn_until_fixpoint, GoalSubns, Subn0, Subn)
> +    ;
> +        Subn = Subn0
> +    ),
> +    incremental_rename_vars_in_goal_expr(Subn, SubnUpdates,
> +        GoalExpr0, GoalExpr),
> +    rename_vars_in_goal_info(need_not_rename, Subn, GoalInfo0, GoalInfo),
> +    Goal = hlds_goal(GoalExpr, GoalInfo).
> +

...

> Index: doc/reference_manual.texi
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/mercury/doc/reference_manual.texi,v
> retrieving revision 1.458
> diff -u -b -r1.458 reference_manual.texi
> --- doc/reference_manual.texi	7 Jan 2011 06:58:38 -0000	1.458
> +++ doc/reference_manual.texi	27 Feb 2011 11:23:16 -0000
> @@ -1000,15 +1000,15 @@
> next.

...

> @@ -1019,20 +1019,39 @@
> referred to as @samp{!. at var{X}} (unless the enclosing @var{X} is masked
> by a more local state variable of the same name.)
>
> -For instance, the following goal employing an if-then-else expression
> +For instance, the following clause employing a lambda expression
> @example
> -	p((if q(!@var{X}), r(!@var{X}) then @var{A} else @var{B}), !@var{X})
> +        p(@var{A}, @var{B}, !@var{S}) :-
> +                F = (pred(@var{C}::in, @var{D}::out) is det :-
> +                        q(@var{C}, @var{D}, !@var{S})
> +                ),
> +                ( F(@var{A}, @var{E}) ->
> +                        @var{B} = @var{E}
> +                ;
> +                        @var{B} = @var{A}
> +                ).
> @end example
> @noindent
> -is illegal because it implicitly refers to @samp{!:@var{X}} in the condition
> -of the if-then-else expression.  However
> - at example
> -	p((if some[!@var{X}] (q(!@var{X}), r(!@var{X})) then @var{A} else @var{B}), !@var{X})
> +is illegal because
> +it implicitly refers to @samp{!:@var{S}} inside the lambda expression.
> +However
> + at example
> +        p(@var{A}, @var{B}, !@var{S}) :-
> +                F = (pred(@var{C}::in, @var{D}::out, !. at var{S}::in, !:@var{S}::out) is det :-
> +                        q(@var{C}, @var{D}, !@var{S})
> +                ),
> +                ( F(@var{A}, @var{E}, !@var{S}) ->
> +                        @var{B} = @var{E}
> +                ;
> +                        @var{B} = @var{A}
> +                ).
> @end example
> @noindent
> -is acceptable because the state variable @var{X} is locally scoped to the
> -condition and then-goal of the if-then-else expression, hence @samp{!:@var{X}}
> -may appear therein.
> +is acceptable because the state variable @var{S} accessed
> +inside the lambda expression is locally scoped to the lambda expression
> +(shadowing the state variable of the same name outside the lambda expression),
> +and the lambda expression may refer to
> +the text version of a local state variable.

s/text/next/

The change appears okay otherwise.

Julien.
--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to:       mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions:          mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------



More information about the reviews mailing list