[m-rev.] For review: change the way we handle inst any non-locals in negated contexts (again)

Julien Fischer juliensf at cs.mu.OZ.AU
Wed Dec 14 00:53:20 AEDT 2005


On Tue, 13 Dec 2005, Ralph Becket wrote:

> Estimated hours taken: 16
> Branches: main
>
> Undo my recent changes to purity error checking in the context of inst any
> non-locals in negated contexts.
>
> Implement a better way of handling the problem, as discussed on the mailing
> list.  The new solution is to require that any goals featuring inst any
> non-locals in a negated context must appear in a
> promise_{pure,semipure,impure} context.  This is something of a compromise:
> on the one hand it does require that the condition be explicitly recognised
> by the programmer; on the other, it does not require that the "offending" goals
> be individually identified (this is partly for pragmatic reasons: the earlier
> approach required a plethora of awkward impurity declarations on goals that
> would otherwise be considered completely pure).
>
> COMPILEr/mode_errors.m:
> 	Remove purity_error_should_be_impure and purity_error_wrongly_impure
> 	data constructors; add purity_error_should_be_in_promise_purity_scope.
>
> compiler/mode_info.m:
> 	Replace the in_negated_context field with the in_promise_purity_scope
> 	field.
>
> compiler/modecheck_call.m:
> compiler/modecheck_unify.m:
> 	Back out my previous change.
>
> compiler/modes.m:
> 	Record a purity error if a non-local inst any variable appears
> 	in a negation or the condition of an if-then-else goal.
>
> compiler/purity.m:
> compiler/unique_modes.m:
> 	Back out my previous change.
>
> doc/reference_manual.texi:
> 	Document the new purity rules for inst any non-locals in negated
> 	contexts.
>
> tests/debugger/solver_test.m:
> tests/hard_coded/any_free_unify.m:
> tests/invalid/any_passed_as_ground.m:
> tests/invalid/any_to_ground_in_ite_cond.m:
> tests/invalid/anys_in_negated_contexts.err_exp:
> tests/invalid/anys_in_negated_contexts.m:
> tests/invalid/purity/impure_func_t7.err_exp:
> tests/invalid/purity/impure_func_t7.m:
> 	Fix up error cases to use the new syntax.
>

You'll also need to check the parts of extras that use solver types.

...

> @@ -1092,35 +1093,33 @@
>
>  %-----------------------------------------------------------------------------%
>
> -:- func purity_error_should_be_impure_to_specs(mode_info::in,
> -        list(prog_var)::in) = (list(error_msg_spec)::out(error_msg_specs))
> -        is det.
> -
> -purity_error_should_be_impure_to_specs(ModeInfo, Vars) = Specs :-
> -    mode_info_get_context(ModeInfo, Context),
> -    mode_info_get_varset(ModeInfo, VarSet),
> -    Pieces = [
> -        words("purity error: goal should be impure because it appears"),
> -        words("in a negated context, but involves the following variables"),
> -        words("whose insts contain `any':"),
> -        words(mercury_vars_to_string(Vars, VarSet, no))
> -    ],
> -    Specs = [
> -        mode_info_context_to_spec(ModeInfo),
> -        error_msg_spec(no, Context, 0, Pieces)
> -    ].
> -
> -%-----------------------------------------------------------------------------%
> -
> -:- func purity_error_wrongly_impure_to_specs(mode_info::in, purity::in) =
> +:- func purity_error_should_be_in_promise_purity_scope_to_specs(
> +        negated_context_desc::in, mode_info::in, prog_var::in) =
>          (list(error_msg_spec)::out(error_msg_specs)) is det.
>
> -purity_error_wrongly_impure_to_specs(ModeInfo, Purity) = Specs :-
> +purity_error_should_be_in_promise_purity_scope_to_specs(NegCtxtDesc,
> +        ModeInfo, Var) = Specs :-
>      mode_info_get_context(ModeInfo, Context),
> -    Pieces = [
> -        words("purity error: goal is marked as impure, but is actually"),
> -        words(if Purity = purity_pure then "pure" else "semipure")
> -    ],
> +    mode_info_get_varset(ModeInfo, VarSet),
> +    (
> +        NegCtxtDesc = if_then_else,
> +        Pieces = [
> +            words("purity error: if-then-else"),
> +            words("should be inside a promise_purity"),
> +            words("scope because non-local variable"),
> +            words(mercury_var_to_string(Var, VarSet, no)),
> +            words("has inst any and appears in the condition.")
> +        ]
> +    ;
> +        NegCtxtDesc = negation,
> +        Pieces = [
> +            words("purity error: negation"),
> +            words("should be inside a promise_purity"),
> +            words("scope because non-local variable"),
> +            words(mercury_var_to_string(Var, VarSet, no)),
> +            words("has inst any and appears in the body.")
> +        ]
> +    ),
>      Specs = [
>          mode_info_context_to_spec(ModeInfo),
>          error_msg_spec(no, Context, 0, Pieces)
> @@ -1139,7 +1138,8 @@
>          words("purity error: lambda should be impure because it"),
>          words("contains the following non-local variables"),
>          words("whose insts contain `any':"),
> -        words(mercury_vars_to_string(Vars, VarSet, no))
> +        words(mercury_vars_to_string(Vars, VarSet, no)),
> +        suffix("."), nl
>      ],
>      Specs = [
>          mode_info_context_to_spec(ModeInfo),
> Index: compiler/mode_info.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/mode_info.m,v
> retrieving revision 1.79
> diff -u -r1.79 mode_info.m
> --- compiler/mode_info.m	28 Nov 2005 04:11:49 -0000	1.79
> +++ compiler/mode_info.m	9 Dec 2005 00:04:57 -0000
> @@ -120,7 +120,7 @@
>  :- pred mode_info_get_warnings(mode_info::in, list(mode_warning_info)::out)
>      is det.
>  :- pred mode_info_get_need_to_requantify(mode_info::in, bool::out) is det.
> -:- pred mode_info_get_in_negated_context(mode_info::in, bool::out) is det.
> +:- pred mode_info_get_in_promise_purity_scope(mode_info::in, bool::out) is det.
>  :- pred mode_info_get_num_errors(mode_info::in, int::out) is det.
>  :- pred mode_info_get_liveness(mode_info::in, set(prog_var)::out) is det.
>  :- pred mode_info_get_varset(mode_info::in, prog_varset::out) is det.
> @@ -169,7 +169,7 @@
>      mode_info::in, mode_info::out) is det.
>  :- pred mode_info_set_need_to_requantify(bool::in,
>      mode_info::in, mode_info::out) is det.
> -:- pred mode_info_set_in_negated_context(bool::in,
> +:- pred mode_info_set_in_promise_purity_scope(bool::in,
>      mode_info::in, mode_info::out) is det.
>  :- pred mode_info_add_live_vars(set(prog_var)::in,
>      mode_info::in, mode_info::out) is det.
> @@ -320,8 +320,11 @@
>                  % after mode analysis finishes.
>                  need_to_requantify      :: bool,
>
> -                % Set to `yes' if we are in a negated context.
> -                in_negated_context      :: bool
> +                % Set to `yes' if we are in a promise_<purity> scope.  This
> +                % information is needed to check that potentially impure
> +                % uses of inst any non-locals in negated contexts are
> +                % properly acknowledged by the programmer.
> +                in_promise_purity_scope :: bool
>              ).
>
>  :- type mode_info
> @@ -473,7 +476,8 @@
>  mode_info_get_errors(MI, MI ^ errors).
>  mode_info_get_warnings(MI, MI ^ mode_sub_info ^ warnings).
>  mode_info_get_need_to_requantify(MI, MI ^ mode_sub_info ^ need_to_requantify).
> -mode_info_get_in_negated_context(MI, MI ^ mode_sub_info ^ in_negated_context).
> +mode_info_get_in_promise_purity_scope(MI,
> +    MI ^ mode_sub_info ^ in_promise_purity_scope).
>  mode_info_get_delay_info(MI, MI ^ delay_info).
>  mode_info_get_live_vars(MI, MI ^ live_vars).
>  mode_info_get_nondet_live_vars(MI, MI ^ nondet_live_vars).
> @@ -498,8 +502,8 @@
>      MI ^ mode_sub_info ^ warnings := Warnings).
>  mode_info_set_need_to_requantify(NTRQ, MI,
>      MI ^ mode_sub_info ^ need_to_requantify := NTRQ).
> -mode_info_set_in_negated_context(INC, MI,
> -    MI ^ mode_sub_info ^ in_negated_context := INC).
> +mode_info_set_in_promise_purity_scope(INC, MI,
> +    MI ^ mode_sub_info ^ in_promise_purity_scope := INC).
>  mode_info_set_delay_info(DelayInfo, MI, MI ^ delay_info := DelayInfo).
>  mode_info_set_live_vars(LiveVarsList, MI, MI ^ live_vars := LiveVarsList).
>  mode_info_set_nondet_live_vars(NondetLiveVars, MI,
> Index: compiler/modecheck_call.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/modecheck_call.m,v
> retrieving revision 1.64
> diff -u -r1.64 modecheck_call.m
> --- compiler/modecheck_call.m	28 Nov 2005 04:11:49 -0000	1.64
> +++ compiler/modecheck_call.m	9 Dec 2005 02:21:14 -0000
> @@ -105,7 +105,7 @@
>  %-----------------------------------------------------------------------------%
>
>  modecheck_call_pred(PredId, DeterminismKnown, ProcId0, TheProcId,
> -        ArgVars0, ArgVars, GoalInfo, ExtraGoals, !ModeInfo) :-
> +        ArgVars0, ArgVars, _GoalInfo, ExtraGoals, !ModeInfo) :-
>      mode_info_get_may_change_called_proc(!.ModeInfo, MayChangeCalledProc),
>      mode_info_get_preds(!.ModeInfo, Preds),
>      mode_info_get_module_info(!.ModeInfo, ModuleInfo),
> @@ -125,42 +125,8 @@
>
>      compute_arg_offset(PredInfo, ArgOffset),
>      pred_info_get_markers(PredInfo, Markers),
> -
>      mode_info_get_instmap(!.ModeInfo, InstMap),
> -    AnyVars =
> -        list__filter(var_inst_contains_any(ModuleInfo, InstMap), ArgVars0),
> -
>      (
> -        % If we are in a negated context and one or more vars have
> -        % inst any then this call is required to be marked impure
> -        % since it may violate referential transparency.
> -        %
> -        mode_info_get_in_negated_context(!.ModeInfo, yes),
> -        \+ goal_info_is_impure(GoalInfo),
> -        AnyVars \= []
> -    ->
> -        set__init(WaitingVars),
> -        mode_info_error(WaitingVars, purity_error_should_be_impure(AnyVars),
> -            !ModeInfo),
> -        TheProcId = invalid_proc_id,
> -        ArgVars = ArgVars0,
> -        ExtraGoals = no_extra_goals
> -    ;
> -        % Report a purity error if a pred call is erroneously marked as impure
> -        % in a negated context.
> -        %
> -        mode_info_get_in_negated_context(!.ModeInfo, yes),
> -        goal_info_is_impure(GoalInfo),
> -        AnyVars = [],
> -        Purity \= purity_impure
> -    ->
> -        set__init(WaitingVars),
> -        mode_info_error(WaitingVars, purity_error_wrongly_impure(Purity),
> -            !ModeInfo),
> -        TheProcId = invalid_proc_id,
> -        ArgVars = ArgVars0,
> -        ExtraGoals = no_extra_goals
> -    ;
>          % In order to give better diagnostics, we handle the cases where there
>          % are zero or one modes for the called predicate specially.
>          %
> Index: compiler/modecheck_unify.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/modecheck_unify.m,v
> retrieving revision 1.94
> diff -u -r1.94 modecheck_unify.m
> --- compiler/modecheck_unify.m	28 Nov 2005 04:11:49 -0000	1.94
> +++ compiler/modecheck_unify.m	9 Dec 2005 01:39:00 -0000
> @@ -98,58 +98,6 @@
>  modecheck_unification(X, RHS, Unification0, UnifyContext, UnifyGoalInfo0,
>          Unify, !ModeInfo, !IO) :-
>      (
> -        mode_info_get_in_negated_context(!.ModeInfo, yes),
> -        (
> -            RHS = var(Y),
> -            Vars = [Y]
> -        ;
> -            RHS = functor(_, _, Vars)
> -        ),
> -        mode_info_get_module_info(!.ModeInfo, ModuleInfo),
> -        mode_info_get_instmap(!.ModeInfo, InstMap),
> -        AnyVars =
> -            list__filter(var_inst_contains_any(ModuleInfo, InstMap), Vars)
> -            % If this unification is in a negated context, but doesn't
> -            % have an `impure' annotation, then none of the variables
> -            % involved are allowed to have inst any.
> -            %
> -    ->
> -        (
> -            AnyVars = [_ | _],
> -            (
> -                goal_info_is_impure(UnifyGoalInfo0)
> -            ->
> -                modecheck_unification_2(X, RHS, Unification0, UnifyContext,
> -                    UnifyGoalInfo0, Unify, !ModeInfo, !IO)
> -            ;
> -                set__init(WaitingVars),
> -                mode_info_error(WaitingVars,
> -                    purity_error_should_be_impure(AnyVars), !ModeInfo),
> -                Unify = conj([])
> -            )
> -        ;
> -            AnyVars = [],
> -            (
> -                goal_info_is_pure(UnifyGoalInfo0)
> -            ->
> -                modecheck_unification_2(X, RHS, Unification0, UnifyContext,
> -                    UnifyGoalInfo0, Unify, !ModeInfo, !IO)
> -            ;
> -                set__init(WaitingVars),
> -                mode_info_error(WaitingVars,
> -                    purity_error_wrongly_impure(purity_pure), !ModeInfo),
> -                Unify = conj([])
> -            )
> -        )
> -    ;
> -        mode_info_get_in_negated_context(!.ModeInfo, no),
> -        \+ goal_info_is_pure(UnifyGoalInfo0)
> -    ->
> -        set__init(WaitingVars),
> -        mode_info_error(WaitingVars,
> -            purity_error_wrongly_impure(purity_pure), !ModeInfo),
> -        Unify = conj([])
> -    ;
>              % If this is a lambda unification containing some inst any
>              % nonlocals, then the lambda should be marked as impure.
>              %
> Index: compiler/modes.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/modes.m,v
> retrieving revision 1.322
> diff -u -r1.322 modes.m
> --- compiler/modes.m	28 Nov 2005 04:11:49 -0000	1.322
> +++ compiler/modes.m	13 Dec 2005 01:03:14 -0000
> @@ -1356,10 +1356,7 @@
>      %
>      mode_info_lock_vars(if_then_else, NonLocals, !ModeInfo),
>      mode_info_add_live_vars(ThenVars, !ModeInfo),
> -    mode_info_get_in_negated_context(!.ModeInfo, InNegatedContext0),
> -    mode_info_set_in_negated_context(yes, !ModeInfo),
>      modecheck_goal(Cond0, Cond, !ModeInfo, !IO),
> -    mode_info_set_in_negated_context(InNegatedContext0, !ModeInfo),
>      mode_info_get_instmap(!.ModeInfo, InstMapCond),
>      mode_info_remove_live_vars(ThenVars, !ModeInfo),
>      mode_info_unlock_vars(if_then_else, NonLocals, !ModeInfo),
> @@ -1384,6 +1381,18 @@
>      instmap__merge(NonLocals, [InstMapThen, InstMapElse], if_then_else,
>          !ModeInfo),
>      Goal = if_then_else(Vars, Cond, Then, Else),
> +    mode_info_get_instmap(!.ModeInfo, InstMap),
> +    (
> +        mode_info_get_in_promise_purity_scope(!.ModeInfo, no)
> +    ->
> +        goal_get_nonlocals(Cond, CondNonLocals0),
> +        CondNonLocals =
> +            set__to_sorted_list(CondNonLocals0 `intersect` NonLocals),
> +        check_no_inst_any_vars(if_then_else, CondNonLocals,
> +            InstMap0, InstMap, !ModeInfo)
> +    ;
> +        true
> +    ),
>      mode_checkpoint(exit, "if-then-else", !ModeInfo, !IO).
>
>  modecheck_goal_expr(not(SubGoal0), GoalInfo0, not(SubGoal), !ModeInfo, !IO) :-
> @@ -1407,13 +1416,20 @@
>      % that the negation does not bind them.
>      %
>      mode_info_lock_vars(negation, NonLocals, !ModeInfo),
> -    mode_info_get_in_negated_context(!.ModeInfo, InNegatedContext0),
> -    mode_info_set_in_negated_context(yes, !ModeInfo),
>      modecheck_goal(SubGoal0, SubGoal, !ModeInfo, !IO),
> -    mode_info_set_in_negated_context(InNegatedContext0, !ModeInfo),
>      mode_info_set_live_vars(LiveVars0, !ModeInfo),
>      mode_info_unlock_vars(negation, NonLocals, !ModeInfo),
>      mode_info_set_instmap(InstMap0, !ModeInfo),
> +    (
> +        mode_info_get_in_promise_purity_scope(!.ModeInfo, no)
> +    ->
> +        goal_info_get_nonlocals(GoalInfo0, NegNonLocals),
> +        instmap__init_unreachable(Unreachable),
> +        check_no_inst_any_vars(negation, set__to_sorted_list(NegNonLocals),
> +            InstMap0, Unreachable, !ModeInfo)
> +    ;
> +        true
> +    ),
>      mode_checkpoint(exit, "not", !ModeInfo, !IO).
>
>  modecheck_goal_expr(scope(Reason, SubGoal0), _GoalInfo, GoalExpr,
> @@ -1459,6 +1475,14 @@
>              mode_checkpoint(exit, "scope", !ModeInfo, !IO),
>              SubGoal = GoalExpr - _
>          )
> +    ; Reason = promise_purity(_Implicit, _Purity) ->
> +        mode_info_get_in_promise_purity_scope(!.ModeInfo, InPPScope),
> +        mode_info_set_in_promise_purity_scope(yes, !ModeInfo),
> +        mode_checkpoint(enter, "scope", !ModeInfo, !IO),
> +        modecheck_goal(SubGoal0, SubGoal, !ModeInfo, !IO),
> +        mode_checkpoint(exit, "scope", !ModeInfo, !IO),
> +        GoalExpr = scope(Reason, SubGoal),
> +        mode_info_set_in_promise_purity_scope(InPPScope, !ModeInfo)
>      ;
>          mode_checkpoint(enter, "scope", !ModeInfo, !IO),
>          modecheck_goal(SubGoal0, SubGoal, !ModeInfo, !IO),
> @@ -1624,6 +1648,35 @@
>      % these should have been expanded out by now
>      unexpected(this_file, "modecheck_goal_expr: unexpected shorthand").
>
> +
> +    % If the condition of a negation or if-then-else contains any inst any

I suggest: "some inst any" rather than "any inst any"

> +    % non-locals (a potential referential transparency violation)
> +    % we need to check that the programmer has recognised the
> +    % possibility and placed the if-then-else in a promise_<purity>
> +    % scope.
> +    %
> +:- pred check_no_inst_any_vars(negated_context_desc::in, prog_vars::in,
> +        instmap::in, instmap::in, mode_info::in, mode_info::out) is det.
> +
> +check_no_inst_any_vars(_, [], _, _, !ModeInfo).
> +
> +check_no_inst_any_vars(NegCtxtDesc, [NonLocal | NonLocals], InstMap0, InstMap,
> +        !ModeInfo) :-
> +    (
> +        (   instmap__lookup_var(InstMap0, NonLocal, Inst)
> +        ;   instmap__lookup_var(InstMap,  NonLocal, Inst)
> +        ),
> +        mode_info_get_module_info(!.ModeInfo, ModuleInfo),
> +        inst_contains_any(ModuleInfo, Inst)
> +    ->
> +        mode_info_error(make_singleton_set(NonLocal),
> +            purity_error_should_be_in_promise_purity_scope(NegCtxtDesc,
> +            NonLocal), !ModeInfo)
> +    ;
> +        check_no_inst_any_vars(NegCtxtDesc, NonLocals, InstMap0, InstMap,
> +            !ModeInfo)
> +    ).
> +
>  append_extra_goals(no_extra_goals, ExtraGoals, ExtraGoals).
>  append_extra_goals(extra_goals(BeforeGoals, AfterGoals),
>          no_extra_goals, extra_goals(BeforeGoals, AfterGoals)).
> Index: compiler/purity.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/purity.m,v
> retrieving revision 1.86
> diff -u -r1.86 purity.m
> --- compiler/purity.m	18 Nov 2005 06:13:37 -0000	1.86
> +++ compiler/purity.m	13 Dec 2005 07:42:30 -0000
> @@ -5,34 +5,18 @@

You appear to be backing out parts of changes not related to your
purity changes below (in particular you are backing some (all?) of
r1.85 - which is why some of the calls to unexpected/2 are being changed
back to error/1).


>  % This file may only be copied under the terms of the GNU General
>  % Public License - see the file COPYING in the Mercury distribution.
>  %-----------------------------------------------------------------------------%
> -
> -% File: purity.m.
> +%
> +% File:     purity.m
>  % Authors:  scachte (Peter Schachte, main author and designer of purity system)
>  %           trd (modifications for impure functions)
> -%           rafe (modifications for solver goals in negated contexts)
> -
>  % Purpose:  handle `impure' and `promise_pure' declarations;
>  %           finish off type checking.
> -
> -% The main purpose of this module is check the consistency of the `impure' and
> -% `promise_pure' (etc.) declarations, and to thus report error messages if the
> -% program is not "purity-correct".  This includes treating procedures with
> -% different clauses for different modes as impure, unless promised pure.
> -%
> -% There is a special case to do with solver type goals in negated contexts.
> -% A pure goal taking solver type arguments with inst any may be used to
> -% break referential transparency if it appears in a negated context.  The
> -% canonical example is `X < Y, not(X >= Y)' vs `not(X >= Y), X < Y' where
> -% (<) and (>=) impose inequality constraints on solver variables.  If X
> -% and Y are initially free then the first goal ordering will succeed, but the
> -% second ordering will fail.  To get around this problem we require solver
> -% goals in negated contexts with inst any arguments to be marked as `impure'.
> -% This means that this module should not report purity warnings for calls
> -% marked as impure in negated contexts when those calls are to non-impure
> -% predicates or functions.  Instead this aspect of purity checking must be
> -% deferred until mode analysis which is when information about the insts of
> -% variables is available.  (Note: the above also applies to lambdas containing
> -% non-local inst any variables.)
> +%
> +% The main purpose of this module is check the consistency of the
> +% `impure' and `promise_pure' (etc.) declarations, and to thus report
> +% error messages if the program is not "purity-correct".
> +% This includes treating procedures with different clauses for
> +% different modes as impure, unless promised pure.
>  %
>  % This module also calls post_typecheck.m to perform the final parts of
>  % type analysis, including resolution of predicate and function overloading
> @@ -135,20 +119,20 @@
>
>  :- import_module hlds.hlds_module.
>  :- import_module hlds.hlds_pred.
> +:- import_module parse_tree.prog_data.
>
>  :- import_module bool.
>  :- import_module io.
>
> -%-----------------------------------------------------------------------------%
> -
> -    % Purity check a whole module.  Also do the post-typecheck stuff described
> -    % above, and eliminate double negations and calls to
> -    % `private_builtin.unsafe_type_cast/2'.  The first argument specifies
> -    % whether there were any type errors (if so, we suppress some diagnostics
> -    % in post_typecheck.m because they are usually spurious).  The third
> -    % argument specifies whether post_typecheck.m detected any errors that
> -    % would cause problems for later passes (if so, we stop compilation after
> -    % this pass).
> +    % Purity check a whole module.  Also do the post-typecheck stuff
> +    % described above, and eliminate double negations and calls
> +    % to `private_builtin.unsafe_type_cast/2'.
> +    % The first argument specifies whether there were any type
> +    % errors (if so, we suppress some diagnostics in post_typecheck.m
> +    % because they are usually spurious).
> +    % The third argument specifies whether post_typecheck.m detected
> +    % any errors that would cause problems for later passes
> +    % (if so, we stop compilation after this pass).
>      %
>  :- pred puritycheck(bool::in, bool::out, module_info::in, module_info::out,
>      io::di, io::uo) is det.
> @@ -163,6 +147,12 @@
>  :- pred repuritycheck_proc(module_info::in, pred_proc_id::in, pred_info::in,
>      pred_info::out) is det.
>
> +    % Give an error message for unifications marked impure/semipure
> +    % that are not function calls (e.g. impure X = 4)
> +    %
> +:- pred impure_unification_expr_error(prog_context::in, purity::in,
> +    io::di, io::uo) is det.
> +
>  :- implementation.
>
>  :- import_module check_hlds.clause_to_proc.
> @@ -196,6 +186,7 @@
>  :- import_module int.
>  :- import_module list.
>  :- import_module map.
> +:- import_module require.
>  :- import_module set.
>  :- import_module std_util.
>  :- import_module string.
> @@ -205,7 +196,6 @@
>  %-----------------------------------------------------------------------------%
>  %
>  % Public Predicates
> -%
>
>  puritycheck(FoundTypeError, PostTypecheckError, !HLDS, !IO) :-
>      globals__io_lookup_bool_option(statistics, Statistics, !IO),
> @@ -290,7 +280,7 @@
>      module_info::in, int::out, io::di, io::uo) is det.
>
>  puritycheck_pred(PredId, !PredInfo, ModuleInfo, NumErrors, !IO) :-
> -    pred_info_get_purity(!.PredInfo, DeclPurity),
> +    pred_info_get_purity(!.PredInfo, DeclPurity) ,
>      pred_info_get_promised_purity(!.PredInfo, PromisedPurity),
>      some [!ClausesInfo] (
>          pred_info_clauses_info(!.PredInfo, !:ClausesInfo),
> @@ -300,13 +290,12 @@
>          clauses_info_varset(!.ClausesInfo, VarSet0),
>          RunPostTypecheck = yes,
>          PurityInfo0 = purity_info(ModuleInfo, RunPostTypecheck,
> -            !.PredInfo, VarTypes0, VarSet0, [], dont_make_implicit_promises,
> -            no),
> +            !.PredInfo, VarTypes0, VarSet0, [], dont_make_implicit_promises),
>          pred_info_get_goal_type(!.PredInfo, GoalType),
>          compute_purity(GoalType, Clauses0, Clauses, ProcIds,
>              purity_pure, Purity, PurityInfo0, PurityInfo),
>          PurityInfo = purity_info(_, _, !:PredInfo,
> -            VarTypes, VarSet, RevMessages, _, _),
> +            VarTypes, VarSet, RevMessages, _),
>          clauses_info_set_vartypes(VarTypes, !ClausesInfo),
>          clauses_info_set_varset(VarSet, !ClausesInfo),
>          Messages = list__reverse(RevMessages),
> @@ -351,9 +340,9 @@
>      proc_info_varset(ProcInfo0, VarSet0),
>      RunPostTypeCheck = no,
>      PurityInfo0 = purity_info(ModuleInfo, RunPostTypeCheck,
> -        !.PredInfo, VarTypes0, VarSet0, [], dont_make_implicit_promises, no),
> +        !.PredInfo, VarTypes0, VarSet0, [], dont_make_implicit_promises),
>      compute_goal_purity(Goal0, Goal, Bodypurity, PurityInfo0, PurityInfo),
> -    PurityInfo = purity_info(_, _, !:PredInfo, VarTypes, VarSet, _, _, _),
> +    PurityInfo = purity_info(_, _, !:PredInfo, VarTypes, VarSet, _, _),
>      proc_info_set_goal(Goal, ProcInfo0, ProcInfo1),
>      proc_info_set_vartypes(VarTypes, ProcInfo1, ProcInfo2),
>      proc_info_set_varset(VarSet, ProcInfo2, ProcInfo),
> @@ -417,8 +406,7 @@
>  compute_purity(GoalType, [Clause0 | Clauses0], [Clause | Clauses], ProcIds,
>          !Purity, !Info) :-
>      Clause0 = clause(Ids, Body0 - Info0, Lang, Context),
> -    compute_expr_purity(Body0, Body, Info0, Bodypurity, !Info),
> -    add_goal_info_purity_feature(Bodypurity, Info0, Info),
> +    compute_expr_purity(Body0, Body, Info0, Bodypurity0, !Info),
>      % If this clause doesn't apply to all modes of this procedure,
>      % i.e. the procedure has different clauses for different modes,
>      % then we must treat it as impure.
> @@ -434,7 +422,9 @@
>      ;
>          Clausepurity = purity_impure
>      ),
> -    !:Purity = worst_purity(!.Purity, worst_purity(Bodypurity, Clausepurity)),
> +    worst_purity(Bodypurity0, Clausepurity) = Bodypurity,
> +    add_goal_info_purity_feature(Bodypurity, Info0, Info),
> +    !:Purity = worst_purity(!.Purity, Bodypurity),
>      Clause = clause(Ids, Body - Info, Lang, Context),
>      compute_purity(GoalType, Clauses0, Clauses, ProcIds, !Purity, !Info).
>
> @@ -454,20 +444,11 @@
>  :- pred compute_expr_purity(hlds_goal_expr::in, hlds_goal_expr::out,
>      hlds_goal_info::in, purity::out, purity_info::in, purity_info::out) is det.
>
> -compute_expr_purity(GoalExpr0, GoalExpr, GoalInfo0, ActualPurity, !Info) :-
> -    compute_expr_purity_2(GoalExpr0, GoalExpr, GoalInfo0, InferredPurity,
> -        !Info),
> -    infer_goal_info_purity(GoalInfo0, DeclPurity),
> -    ActualPurity = worst_purity(DeclPurity, InferredPurity).
> -
> -:- pred compute_expr_purity_2(hlds_goal_expr::in, hlds_goal_expr::out,
> -    hlds_goal_info::in, purity::out, purity_info::in, purity_info::out) is det.
> -
> -compute_expr_purity_2(conj(Goals0), conj(Goals), _, Purity, !Info) :-
> +compute_expr_purity(conj(Goals0), conj(Goals), _, Purity, !Info) :-
>      compute_goals_purity(Goals0, Goals, purity_pure, Purity, !Info).
> -compute_expr_purity_2(par_conj(Goals0), par_conj(Goals), _, Purity, !Info) :-
> +compute_expr_purity(par_conj(Goals0), par_conj(Goals), _, Purity, !Info) :-
>      compute_goals_purity(Goals0, Goals, purity_pure, Purity, !Info).
> -compute_expr_purity_2(Goal0, Goal, GoalInfo, ActualPurity, !Info) :-
> +compute_expr_purity(Goal0, Goal, GoalInfo, ActualPurity, !Info) :-
>      Goal0 = call(PredId0, ProcId, Vars, BIState, UContext, Name0),
>      RunPostTypecheck = !.Info ^ run_post_typecheck,
>      PredInfo = !.Info ^ pred_info,
> @@ -497,7 +478,7 @@
>      goal_info_get_context(GoalInfo, CallContext),
>      perform_goal_purity_checks(CallContext, PredId,
>          DeclaredPurity, ActualPurity, !Info).
> -compute_expr_purity_2(generic_call(GenericCall0, Args, Modes0, Det),
> +compute_expr_purity(generic_call(GenericCall0, Args, Modes0, Det),
>          GoalExpr, GoalInfo, Purity, !Info) :-
>      (
>          GenericCall0 = higher_order(_, Purity, _, _),
> @@ -537,10 +518,10 @@
>          ),
>          GoalExpr = generic_call(GenericCall, Args, Modes, Det)
>      ).
> -compute_expr_purity_2(switch(Var, Canfail, Cases0),
> +compute_expr_purity(switch(Var, Canfail, Cases0),
>          switch(Var, Canfail, Cases), _, Purity, !Info) :-
>      compute_cases_purity(Cases0, Cases, purity_pure, Purity, !Info).
> -compute_expr_purity_2(Unif0, GoalExpr, GoalInfo, ActualPurity, !Info) :-
> +compute_expr_purity(Unif0, GoalExpr, GoalInfo, ActualPurity, !Info) :-
>      Unif0 = unify(Var, RHS0, Mode, Unification, UnifyContext),
>      (
>          RHS0 = lambda_goal(LambdaPurity, F, EvalMethod,
> @@ -559,7 +540,7 @@
>              FixModes = modes_need_fixing,
>              (
>                  EvalMethod = lambda_normal,
> -                unexpected(this_file, "compute_expr_purity_2: modes need " ++
> +                error("compute_expr_purity: modes need " ++
>                      "fixing for normal lambda_goal")
>              ;
>                  EvalMethod = lambda_aditi_bottom_up,
> @@ -575,6 +556,16 @@
>          GoalExpr = unify(Var, RHS, Mode, Unification, UnifyContext),
>          % the unification itself is always pure,
>          % even if the lambda expression body is impure
> +        infer_goal_info_purity(GoalInfo, DeclaredPurity),
> +        (
> +            DeclaredPurity \= purity_pure
> +        ->
> +            goal_info_get_context(GoalInfo, Context),
> +            Message = impure_unification_expr_error(Context, DeclaredPurity),
> +            purity_info_add_message(error(Message), !Info)
> +        ;
> +            true
> +        ),
>          ActualPurity = purity_pure
>      ;
>          RHS0 = functor(ConsId, _, Args)
> @@ -609,22 +600,19 @@
>          GoalExpr = Unif0,
>          ActualPurity = purity_pure
>      ).
> -compute_expr_purity_2(disj(Goals0), disj(Goals), _, Purity, !Info) :-
> +compute_expr_purity(disj(Goals0), disj(Goals), _, Purity, !Info) :-
>      compute_goals_purity(Goals0, Goals, purity_pure, Purity, !Info).
> -compute_expr_purity_2(not(Goal0), NotGoal, GoalInfo0, Purity, !Info) :-
> +compute_expr_purity(not(Goal0), NotGoal, GoalInfo0, Purity, !Info) :-
>      % Eliminate double negation.
>      negate_goal(Goal0, GoalInfo0, NotGoal0),
>      ( NotGoal0 = not(Goal1) - _GoalInfo1 ->
> -        InNegatedContext0 = !.Info ^ in_negated_context,
> -        !:Info = !.Info ^ in_negated_context := yes,
>          compute_goal_purity(Goal1, Goal, Purity, !Info),
> -        !:Info = !.Info ^ in_negated_context := InNegatedContext0,
>          NotGoal = not(Goal)
>      ;
>          compute_goal_purity(NotGoal0, NotGoal1, Purity, !Info),
>          NotGoal1 = NotGoal - _
>      ).
> -compute_expr_purity_2(scope(Reason, Goal0), scope(Reason, Goal),
> +compute_expr_purity(scope(Reason, Goal0), scope(Reason, Goal),
>          _, Purity, !Info) :-
>      (
>          Reason = exist_quant(_),
> @@ -654,21 +642,14 @@
>          Reason = from_ground_term(_),
>          compute_goal_purity(Goal0, Goal, Purity, !Info)
>      ).
> -compute_expr_purity_2(if_then_else(Vars, Cond0, Then0, Else0),
> +compute_expr_purity(if_then_else(Vars, Cond0, Then0, Else0),
>          if_then_else(Vars, Cond, Then, Else), _, Purity, !Info) :-
> -        % The condition is in a negated context.
> -        %
> -    InNegatedContext0 = !.Info ^ in_negated_context,
> -    !:Info = !.Info ^ in_negated_context := yes,
>      compute_goal_purity(Cond0, Cond, Purity1, !Info),
> -    !:Info = !.Info ^ in_negated_context := InNegatedContext0,
> -        % The Then and Else goals are not.
> -        %
>      compute_goal_purity(Then0, Then, Purity2, !Info),
>      compute_goal_purity(Else0, Else, Purity3, !Info),
>      worst_purity(Purity1, Purity2) = Purity12,
>      worst_purity(Purity12, Purity3) = Purity.
> -compute_expr_purity_2(ForeignProc0, ForeignProc, _, Purity, !Info) :-
> +compute_expr_purity(ForeignProc0, ForeignProc, _, Purity, !Info) :-
>      ForeignProc0 = foreign_proc(_, _, _, _, _, _),
>      Attributes = ForeignProc0 ^ foreign_attr,
>      PredId = ForeignProc0 ^ foreign_pred_id,
> @@ -686,9 +667,9 @@
>          Purity = purity(Attributes)
>      ).
>
> -compute_expr_purity_2(shorthand(_), _, _, _, !Info) :-
> +compute_expr_purity(shorthand(_), _, _, _, !Info) :-
>      % These should have been expanded out by now.
> -    unexpected(this_file, "compute_expr_purity_2: unexpected shorthand").
> +    error("compute_expr_purity: unexpected shorthand").
>

See my comments regarding r1.85 of purity.m above.

Cheers,
Julien.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------



More information about the reviews mailing list