[m-rev.] For review: make impure goals with inst any vars in negated contexts

Ralph Becket rafe at cs.mu.OZ.AU
Fri Oct 28 14:02:25 AEST 2005


Estimated hours taken: 10
Branches: main

Require impurity annotations on goals in negated contexts or lambdas
containing non-local inst any variables.  Such goals can violate referential
transparency, even though they might otherwise be considered pure.

NEWS:
	Mention the new change.

compiler/inst_util.m:
	Add utility preds inst_contains_any/2 and var_inst_contains_any/3.

compiler/mode_errors.m:
	Add three new mode errors to cover the new cases.

compiler/mode_info.m:
	Add field `in_negated_context' to the mode_info.

compiler/modecheck_call.m:
compiler/modecheck_unify.m:
	Perform purity checks for goals in negated contexts containing inst any
	non-locals or lambdas containing inst any non-locals.

compiler/modes.m:
	Add negated context tracking.

compiler/purity.m:
	Defer purity checking on goals in negated contexts because we
	don't have inst information at the time purity analysis is run.

compiler/unique_modes.m:
	We now have to include the goal_info in calls to modecheck_call_pred.

doc/reference_manual.texi:
	Document the new requirement.

tests/invalid/Mmakefile:
tests/invalid/anys_in_negated_contexts.err_exp:
tests/invalid/anys_in_negated_contexts.m:
	Add a test case.

Index: NEWS
===================================================================
RCS file: /home/mercury1/repository/mercury/NEWS,v
retrieving revision 1.391
diff -u -r1.391 NEWS
--- NEWS	26 Oct 2005 05:04:12 -0000	1.391
+++ NEWS	28 Oct 2005 03:33:07 -0000
@@ -5,6 +5,8 @@
 ==========
 
 Changes to the Mercury language:
+* Goals in negated contexts using inst any non-local variables or lambda
+  expressions containing inst any non-locals must now be marked as impure.
 * The Mercury typeclass system now supports functional dependencies.
 * We now have support for optional module initialisation and finalisation.
 * We now have support for impure module-local mutable variables.
Index: compiler/inst_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/inst_util.m,v
retrieving revision 1.42
diff -u -r1.42 inst_util.m
--- compiler/inst_util.m	28 Oct 2005 02:10:10 -0000	1.42
+++ compiler/inst_util.m	28 Oct 2005 03:28:27 -0000
@@ -41,6 +41,7 @@
 :- interface.
 
 :- import_module hlds.hlds_module.
+:- import_module hlds.instmap.
 :- import_module parse_tree.prog_data.
 
 :- import_module bool.
@@ -108,6 +109,15 @@
 :- pred inst_contains_nonstandard_func_mode(module_info::in, mer_inst::in)
     is semidet.
 
+    % Succeed iff the inst is any or contains any.
+    %
+:- pred inst_contains_any(module_info::in, (mer_inst)::in) is semidet.
+
+    % Succeed iff the given var's inst is any or contains any.
+    %
+:- pred var_inst_contains_any(module_info::in, instmap::in, prog_var::in)
+    is semidet.
+
     % Succeed iff the first argument is a function pred_inst_info
     % whose mode does not match the standard func mode.
     %
@@ -1677,6 +1687,38 @@
 
 %-----------------------------------------------------------------------------%
 
+inst_contains_any(ModuleInfo, Inst) :-
+    set__init(Expansions),
+    inst_contains_any_2(ModuleInfo, Inst, Expansions).
+
+
+:- pred inst_contains_any_2(module_info::in, (mer_inst)::in,
+        set(inst_name)::in) is semidet.
+
+inst_contains_any_2(_ModuleInfo, any(_), _Expansions).
+
+inst_contains_any_2(ModuleInfo, bound(_, BoundInsts), Expansions) :-
+    list__member(functor(_, Insts), BoundInsts),
+    list__member(Inst, Insts),
+    inst_contains_any_2(ModuleInfo, Inst, Expansions).
+
+inst_contains_any_2(_ModuleInfo, inst_var(_), _Expansions) :-
+    error("internal error: uninstantiated inst parameter").
+
+inst_contains_any_2(ModuleInfo, defined_inst(InstName), Expansions0) :-
+    \+ set__member(InstName, Expansions0),
+    Expansions = set__insert(Expansions0, InstName),
+    inst_lookup(ModuleInfo, InstName, Inst),
+    inst_contains_any_2(ModuleInfo, Inst, Expansions).
+
+%-----------------------------------------------------------------------------%
+
+solver_var_inst_contains_any(ModuleInfo, VarTypes, Instmap, Var) :-
+    instmap__lookup_var(Instmap, Var, Inst),
+    inst_contains_any(ModuleInfo, Inst).
+
+%-----------------------------------------------------------------------------%
+
 pred_inst_info_is_nonstandard_func_mode(ModuleInfo, PredInstInfo) :-
     PredInstInfo = pred_inst_info(function, ArgModes, _),
     Arity = list__length(ArgModes),
Index: compiler/mode_errors.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mode_errors.m,v
retrieving revision 1.94
diff -u -r1.94 mode_errors.m
--- compiler/mode_errors.m	28 Oct 2005 02:10:23 -0000	1.94
+++ compiler/mode_errors.m	28 Oct 2005 03:05:28 -0000
@@ -125,10 +125,24 @@
             % schedule_culprit gives the reason why they couldn't be scheduled.
 
     ;       mode_error_final_inst(int, prog_var, mer_inst, mer_inst,
-                final_inst_error).
+                final_inst_error)
             % One of the head variables did not have the expected final inst
             % on exit from the proc.
 
+    ;       purity_error_should_be_impure(list(prog_var))
+            % A goal in a negated context contains vars with inst any was
+            % not marked impure, as it should be.
+
+    ;       purity_error_wrongly_impure(purity)
+            % A goal in a negated context was erroneously marked as impure.
+            % The purity argument specifies what purity the goal has.
+
+    ;       purity_error_lambda_should_be_impure(list(prog_var)).
+            % A lambda term containing inst any non-locals should have been
+            % declared impure, but hasn't been (executing such a lambda may
+            % further constrain the inst any variables, thereby violating
+            % referential transparency).
+
 :- type schedule_culprit
     --->    goal_itself_was_impure
     ;       goals_followed_by_impure_goal(hlds_goal)
@@ -329,6 +343,15 @@
         ModeError = mode_error_final_inst(ArgNum, Var, VarInst, Inst, Reason),
         Specs = mode_error_final_inst_to_specs(ModeInfo, ArgNum, Var, VarInst,
             Inst, Reason)
+    ;
+        ModeError = purity_error_should_be_impure(Vars),
+        Specs = purity_error_should_be_impure_to_specs(ModeInfo, Vars)
+    ;
+        ModeError = purity_error_wrongly_impure(Purity),
+        Specs = purity_error_wrongly_impure_to_specs(ModeInfo, Purity)
+    ;
+        ModeError = purity_error_lambda_should_be_impure(Vars),
+        Specs = purity_error_lambda_should_be_impure_to_specs(ModeInfo, Vars)
     ).
 
 :- func mode_warning_to_specs(mode_info::in, mode_warning_info::in)
@@ -1069,6 +1092,62 @@
 
 %-----------------------------------------------------------------------------%
 
+:- 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) =
+        (list(error_msg_spec)::out(error_msg_specs)) is det.
+
+purity_error_wrongly_impure_to_specs(ModeInfo, Purity) = 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")
+    ],
+    Specs = [
+        mode_info_context_to_spec(ModeInfo),
+        error_msg_spec(no, Context, 0, Pieces)
+    ].
+
+%-----------------------------------------------------------------------------%
+
+:- func purity_error_lambda_should_be_impure_to_specs(mode_info::in,
+        list(prog_var)::in) = (list(error_msg_spec)::out(error_msg_specs))
+        is det.
+
+purity_error_lambda_should_be_impure_to_specs(ModeInfo, Vars) = Specs :-
+    mode_info_get_context(ModeInfo, Context),
+    mode_info_get_varset(ModeInfo, VarSet),
+    Pieces = [
+        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))
+    ],
+    Specs = [
+        mode_info_context_to_spec(ModeInfo),
+        error_msg_spec(no, Context, 0, Pieces)
+    ].
+
+%-----------------------------------------------------------------------------%
+
 maybe_report_error_no_modes(PredId, PredInfo, ModuleInfo, !IO) :-
     pred_info_import_status(PredInfo, ImportStatus),
     ( ImportStatus = local ->
Index: compiler/mode_info.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mode_info.m,v
retrieving revision 1.77
diff -u -r1.77 mode_info.m
--- compiler/mode_info.m	28 Oct 2005 02:10:23 -0000	1.77
+++ compiler/mode_info.m	28 Oct 2005 03:05:28 -0000
@@ -122,6 +122,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_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.
@@ -171,6 +172,8 @@
     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,
+    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.
 :- pred mode_info_remove_live_vars(set(prog_var)::in,
@@ -318,7 +321,10 @@
 
                 % Set to `yes' if we need to requantify the procedure body
                 % after mode analysis finishes.
-                need_to_requantify      :: bool
+                need_to_requantify      :: bool,
+
+                % Set to `yes' if we are in a negated context.
+                in_negated_context      :: bool
             ).
 
 :- type mode_info
@@ -443,9 +449,11 @@
     CheckingExtraGoals = no,
     MayInitSolverVars = yes,
     NeedToRequantify = no,
+    InNegatedContext = no,
 
     ModeSubInfo = mode_sub_info(ProcId, VarSet, Unreachable, Changed,
-        CheckingExtraGoals, InstMapping0, WarningList, NeedToRequantify),
+        CheckingExtraGoals, InstMapping0, WarningList, NeedToRequantify,
+        InNegatedContext),
 
     ModeInfo = mode_info(ModuleInfo, PredId, VarTypes, Debug,
         Context, ModeContext, InstMapping0, LockedVars, DelayInfo,
@@ -468,6 +476,7 @@
 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_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).
@@ -492,6 +501,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_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.62
diff -u -r1.62 modecheck_call.m
--- compiler/modecheck_call.m	28 Oct 2005 02:10:24 -0000	1.62
+++ compiler/modecheck_call.m	28 Oct 2005 03:05:28 -0000
@@ -36,7 +36,8 @@
 
 :- pred modecheck_call_pred(pred_id::in, maybe(determinism)::in,
     proc_id::in, proc_id::out, list(prog_var)::in, list(prog_var)::out,
-    extra_goals::out, mode_info::in, mode_info::out) is det.
+    hlds_goal_info::in, extra_goals::out, mode_info::in, mode_info::out)
+    is det.
 
 :- pred modecheck_higher_order_call(pred_or_func::in, prog_var::in,
     list(prog_var)::in, list(prog_var)::out, list(mer_mode)::out,
@@ -100,7 +101,7 @@
 :- import_module varset.
 
 modecheck_call_pred(PredId, DeterminismKnown, ProcId0, TheProcId,
-        ArgVars0, ArgVars, 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),
@@ -121,9 +122,44 @@
     compute_arg_offset(PredInfo, ArgOffset),
     pred_info_get_markers(PredInfo, Markers),
 
-    % In order to give better diagnostics, we handle the cases where there are
-    % zero or one modes for the called predicate specially.
+    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.
+        %
         ProcIds = [],
         \+ check_marker(Markers, infer_modes)
     ->
@@ -141,7 +177,6 @@
         TheProcId = ProcId,
         map__lookup(Procs, ProcId, ProcInfo),
 
-        %
         % Check that `ArgsVars0' have livenesses which match the
         % expected livenesses.
         %
@@ -150,7 +185,6 @@
         modecheck_var_list_is_live(ArgVars0, ProcArgLives0,
             NeedExactMatch, ArgOffset, !ModeInfo),
 
-        %
         % Check that `ArgsVars0' have insts which match the expected
         % initial insts, and set their new final insts (introducing
         % extra unifications for implied modes, if necessary).
@@ -194,7 +228,6 @@
                 ArgVars = ArgVars0,
                 WaitingVars = set__list_to_set(ArgVars),
                 ExtraGoals = no_extra_goals,
-                mode_info_get_instmap(!.ModeInfo, InstMap),
                 instmap__lookup_vars(ArgVars, InstMap, ArgInsts),
                 mode_info_set_call_arg_context(0, !ModeInfo),
                 mode_info_error(WaitingVars,
@@ -213,6 +246,7 @@
         mode_info_set_errors(Errors, !ModeInfo)
     ).
 
+
 modecheck_higher_order_call(PredOrFunc, PredVar, Args0, Args, Modes, Det,
         ExtraGoals, !ModeInfo) :-
     %
Index: compiler/modecheck_unify.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modecheck_unify.m,v
retrieving revision 1.92
diff -u -r1.92 modecheck_unify.m
--- compiler/modecheck_unify.m	28 Oct 2005 02:10:24 -0000	1.92
+++ compiler/modecheck_unify.m	28 Oct 2005 03:05:28 -0000
@@ -88,7 +88,95 @@
 
 %-----------------------------------------------------------------------------%
 
-modecheck_unification(X, var(Y), Unification0, UnifyContext, UnifyGoalInfo0,
+    % We first have to check that if a unification occurs in a negated
+    % context with an inst any argument then it has an explicit `impure'
+    % annotation.
+    %
+    % With lambdas, the lambda itself must be marked as impure if it includes
+    % any inst any nonlocals (executing such a lambda may have the side effect
+    % of constraining a nonlocal solver variable).
+    %
+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.
+            %
+        RHS = lambda_goal(Purity, _, _, _, NonLocals, _, _, _, _),
+        Purity \= purity_impure,
+        mode_info_get_module_info(!.ModeInfo, ModuleInfo),
+        mode_info_get_instmap(!.ModeInfo, InstMap),
+        AnyVars = list__filter(var_inst_contains_any(ModuleInfo, InstMap),
+            NonLocals),
+        AnyVars = [_ | _]
+    ->
+        set__init(WaitingVars),
+        mode_info_error(WaitingVars,
+            purity_error_lambda_should_be_impure(AnyVars), !ModeInfo),
+        Unify = conj([])
+    ;
+        modecheck_unification_2(X, RHS, Unification0, UnifyContext,
+            UnifyGoalInfo0, Unify, !ModeInfo, !IO)
+    ).
+
+
+:- pred modecheck_unification_2(prog_var::in, unify_rhs::in, unification::in,
+    unify_context::in, hlds_goal_info::in, hlds_goal_expr::out,
+    mode_info::in, mode_info::out, io::di, io::uo) is det.
+
+modecheck_unification_2(X, var(Y), Unification0, UnifyContext, UnifyGoalInfo0,
         Unify, !ModeInfo, !IO) :-
     mode_info_get_module_info(!.ModeInfo, ModuleInfo0),
     mode_info_get_var_types(!.ModeInfo, VarTypes),
@@ -178,7 +266,7 @@
         Unify = unify(X, var(Y), Modes, Unification, UnifyContext)
     ).
 
-modecheck_unification(X0, functor(ConsId0, IsExistConstruction, ArgVars0),
+modecheck_unification_2(X0, functor(ConsId0, IsExistConstruction, ArgVars0),
         Unification0, UnifyContext, GoalInfo0, Goal, !ModeInfo, !IO) :-
     mode_info_get_module_info(!.ModeInfo, ModuleInfo0),
     mode_info_get_var_types(!.ModeInfo, VarTypes0),
@@ -220,7 +308,7 @@
         mode_info_set_var_types(VarTypes, !ModeInfo),
 
         % Modecheck this unification in its new form.
-        modecheck_unification(X0, Functor0, Unification0, UnifyContext,
+        modecheck_unification_2(X0, Functor0, Unification0, UnifyContext,
             GoalInfo0, Goal, !ModeInfo, !IO)
     ;
         % It's not a higher-order pred unification - just
@@ -230,7 +318,7 @@
             UnifyContext, GoalInfo0, Goal, !ModeInfo, !IO)
     ).
 
-modecheck_unification(X, LambdaGoal, Unification0, UnifyContext, _GoalInfo,
+modecheck_unification_2(X, LambdaGoal, Unification0, UnifyContext, _GoalInfo,
         unify(X, RHS, Mode, Unification, UnifyContext), !ModeInfo, !IO) :-
     LambdaGoal = lambda_goal(Purity, PredOrFunc, EvalMethod, _,
         ArgVars, Vars, Modes0, Det, Goal0),
@@ -379,7 +467,7 @@
                 mode_error_non_local_lambda_var(BadVar, BadInst), !ModeInfo)
         ;
             unexpected(this_file,
-                "modecheck_unification(lambda): very strange var")
+                "modecheck_unification_2(lambda): very strange var")
         ),
             % Return any old garbage.
         RHS = lambda_goal(Purity, PredOrFunc, EvalMethod, modes_are_ok,
Index: compiler/modes.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modes.m,v
retrieving revision 1.320
diff -u -r1.320 modes.m
--- compiler/modes.m	28 Oct 2005 02:10:24 -0000	1.320
+++ compiler/modes.m	28 Oct 2005 04:00:25 -0000
@@ -1358,7 +1358,10 @@
     %
     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),
@@ -1406,7 +1409,10 @@
     % 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),
@@ -1474,7 +1480,7 @@
     mode_info_get_instmap(!.ModeInfo, InstMap0),
     DeterminismKnown = no,
     modecheck_call_pred(PredId, DeterminismKnown, ProcId0, ProcId,
-        Args0, Args, ExtraGoals, !ModeInfo),
+        Args0, Args, GoalInfo0, ExtraGoals, !ModeInfo),
 
     mode_info_get_module_info(!.ModeInfo, ModuleInfo),
     mode_info_get_predid(!.ModeInfo, CallerPredId),
@@ -1602,7 +1608,7 @@
     mode_info_set_call_context(call(call(CallId)), !ModeInfo),
     ArgVars0 = list__map(foreign_arg_var, Args0),
     modecheck_call_pred(PredId, DeterminismKnown, ProcId0, ProcId,
-        ArgVars0, ArgVars, ExtraGoals, !ModeInfo),
+        ArgVars0, ArgVars, GoalInfo, ExtraGoals, !ModeInfo),
 
     % zs: The assignment to Pragma looks wrong: instead of Args0,
     % I think we should use Args after the following call:
@@ -2567,7 +2573,7 @@
 hlds_goal_from_delayed_goal(delayed_goal(_WaitingVars, _ModeError, Goal)) =
     Goal.
 
-    % Check whether there are any delayed goals (other than headvar
+    % Check whether there are any delayed goals (other than 
     % unifications) at the point where we are about to schedule an impure goal.
     % If so, that is an error. Headvar unifications are allowed to be delayed
     % because in the case of output arguments, they cannot be scheduled
@@ -2596,7 +2602,7 @@
         !ImpurityErrors, !ModeInfo, !IO),
     mode_info_get_delay_info(!.ModeInfo, DelayInfo2),
     delay_info__enter_conj(DelayInfo2, DelayInfo3),
-    redelay_goals(HeadVarUnificationGoals, DelayInfo3, DelayInfo),
+    redelay_goals(UnificationGoals, DelayInfo3, DelayInfo),
     mode_info_set_delay_info(DelayInfo, !ModeInfo),
     (
         NonHeadVarUnificationGoals = []
@@ -2613,7 +2619,6 @@
 
 :- pred filter_headvar_unification_goals(list(prog_var)::in,
     list(delayed_goal)::in, list(delayed_goal)::out,
-    list(delayed_goal)::out) is det.
 
 filter_headvar_unification_goals(HeadVars, DelayedGoals,
         HeadVarUnificationGoals, NonHeadVarUnificationGoals) :-
Index: compiler/purity.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/purity.m,v
retrieving revision 1.81
diff -u -r1.81 purity.m
--- compiler/purity.m	28 Oct 2005 02:10:31 -0000	1.81
+++ compiler/purity.m	28 Oct 2005 04:01:06 -0000
@@ -9,6 +9,7 @@
 % 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.
 %
@@ -18,6 +19,21 @@
 % 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.)
+%
 % This module also calls post_typecheck.m to perform the final parts of
 % type analysis, including resolution of predicate and function overloading
 % (see the comments in that file).
@@ -331,12 +347,13 @@
         clauses_info_varset(!.ClausesInfo, VarSet0),
         RunPostTypecheck = yes,
         PurityInfo0 = purity_info(ModuleInfo, RunPostTypecheck,
-            !.PredInfo, VarTypes0, VarSet0, [], dont_make_implicit_promises),
+            !.PredInfo, VarTypes0, VarSet0, [], dont_make_implicit_promises,
+            no),
         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),
@@ -381,9 +398,9 @@
     proc_info_varset(ProcInfo0, VarSet0),
     RunPostTypeCheck = no,
     PurityInfo0 = purity_info(ModuleInfo, RunPostTypeCheck,
-        !.PredInfo, VarTypes0, VarSet0, [], dont_make_implicit_promises),
+        !.PredInfo, VarTypes0, VarSet0, [], dont_make_implicit_promises, no),
     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),
@@ -464,9 +481,8 @@
         Clausepurity = purity_impure
     ),
     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),
+    Clause = clause(Ids, Body - Info0, Lang, Context),
     compute_purity(GoalType, Clauses0, Clauses, ProcIds, !Purity, !Info).
 
 :- pred applies_to_all_modes(clause::in, list(proc_id)::in) is semidet.
@@ -637,7 +653,10 @@
     % 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),
@@ -675,7 +694,14 @@
     ).
 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,
@@ -845,7 +871,11 @@
     ).
 
     % Peform purity checking of the actual and declared purity,
-    % and check that promises are consistent.
+    % and check that promises are consistent.  There is one
+    % exception to this rule: an otherwise pure atomic goal must
+    % be marked as `impure' if it has an inst any argument and
+    % occurs in a negated context (see the comments at the top
+    % of this file).
     %
     % ActualPurity: The inferred purity of the goal
     % DeclaredPurity: The declared purity of the goal
@@ -873,6 +903,14 @@
     ->
         true
     ;
+        % If DeclaredPurity is impure and this is in a negated context
+        % then we have to defer this purity check until mode checking
+        % when we know whether the vars have inst any or not.
+        DeclaredPurity = purity_impure,
+        !.Info ^ in_negated_context = yes
+    ->
+        true
+    ;
         % Don't require purity annotations on calls in
         % compiler-generated code.
         is_unify_or_compare_pred(PredInfo)
@@ -908,7 +946,14 @@
 
 compute_goal_purity(Goal0 - GoalInfo0, Goal - GoalInfo, Purity, !Info) :-
     compute_expr_purity(Goal0, Goal, GoalInfo0, Purity, !Info),
-    add_goal_info_purity_feature(Purity, GoalInfo0, GoalInfo).
+    (
+        !.Info ^ in_negated_context = yes,
+        infer_goal_info_purity(GoalInfo0, purity_impure)
+    ->
+        GoalInfo = GoalInfo0
+    ;
+        add_goal_info_purity_feature(Purity, GoalInfo0, GoalInfo)
+    ).
 
     % Compute the purity of a list of hlds_goals.  Since the purity of a
     % disjunction is computed the same way as the purity of a conjunction,
@@ -1240,11 +1285,15 @@
                 vartypes            :: vartypes,
                 varset              :: prog_varset,
                 messages            :: post_typecheck_messages,
-                implicit_purity     :: implicit_purity_promise
+                implicit_purity     :: implicit_purity_promise,
                                     % If this is make_implicit_promises then
                                     % purity annotations are optional in the
                                     % current scope and purity warnings/errors
                                     % should not be generated.
+                in_negated_context  :: bool
+                                    % This is `yes' iff the current goal
+                                    % is in a negation or the condition
+                                    % of an if-then-else.
             ).
 
 :- pred purity_info_add_message(post_typecheck_message::in,
Index: compiler/unique_modes.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/unique_modes.m,v
retrieving revision 1.98
diff -u -r1.98 unique_modes.m
--- compiler/unique_modes.m	28 Oct 2005 02:10:42 -0000	1.98
+++ compiler/unique_modes.m	28 Oct 2005 03:05:30 -0000
@@ -446,13 +446,13 @@
     mode_checkpoint(exit, "generic_call", !ModeInfo, !IO).
 
 check_goal_2(call(PredId, ProcId0, Args, Builtin, CallContext,
-        PredName), _GoalInfo0, Goal, !ModeInfo, !IO) :-
+        PredName), GoalInfo0, Goal, !ModeInfo, !IO) :-
     sym_name_to_string(PredName, PredNameString),
     string__append("call ", PredNameString, CallString),
     mode_checkpoint(enter, CallString, !ModeInfo, !IO),
     mode_info_get_call_id(!.ModeInfo, PredId, CallId),
     mode_info_set_call_context(call(call(CallId)), !ModeInfo),
-    check_call(PredId, ProcId0, Args, ProcId, !ModeInfo),
+    check_call(PredId, ProcId0, Args, GoalInfo0, ProcId, !ModeInfo),
     Goal = call(PredId, ProcId, Args, Builtin, CallContext, PredName),
     mode_info_unset_call_context(!ModeInfo),
     mode_checkpoint(exit, "call", !ModeInfo, !IO).
@@ -483,14 +483,14 @@
     mode_checkpoint(exit, "switch", !ModeInfo, !IO).
 
 check_goal_2(foreign_proc(Attributes, PredId, ProcId0, Args, ExtraArgs,
-        PragmaCode), _GoalInfo, Goal, !ModeInfo, !IO) :-
+        PragmaCode), GoalInfo0, Goal, !ModeInfo, !IO) :-
     % To modecheck a pragma_c_code, we just modecheck the proc for
     % which it is the goal.
     mode_checkpoint(enter, "foreign_proc", !ModeInfo, !IO),
     mode_info_get_call_id(!.ModeInfo, PredId, CallId),
     mode_info_set_call_context(call(call(CallId)), !ModeInfo),
     ArgVars = list__map(foreign_arg_var, Args),
-    check_call(PredId, ProcId0, ArgVars, ProcId, !ModeInfo),
+    check_call(PredId, ProcId0, ArgVars, GoalInfo0, ProcId, !ModeInfo),
     Goal = foreign_proc(Attributes, PredId, ProcId, Args, ExtraArgs,
         PragmaCode),
     mode_info_unset_call_context(!ModeInfo),
@@ -500,10 +500,10 @@
     % These should have been expanded out by now.
     unexpected(this_file, "check_goal_2: unexpected shorthand").
 
-:- pred check_call(pred_id::in, proc_id::in, list(prog_var)::in, proc_id::out,
-    mode_info::in, mode_info::out) is det.
+:- pred check_call(pred_id::in, proc_id::in, list(prog_var)::in,
+    hlds_goal_info::in, proc_id::out, mode_info::in, mode_info::out) is det.
 
-check_call(PredId, ProcId0, ArgVars, ProcId, !ModeInfo) :-
+check_call(PredId, ProcId0, ArgVars, GoalInfo, ProcId, !ModeInfo) :-
     % Set the error list to empty for use below
     % (saving the old error list and instmap in variables).
     mode_info_get_errors(!.ModeInfo, OldErrors),
@@ -561,7 +561,7 @@
         mode_info_set_instmap(InstMap0, !ModeInfo),
         proc_info_inferred_determinism(ProcInfo, Determinism),
         modecheck_call_pred(PredId, yes(Determinism), ProcId0, ProcId,
-            ArgVars, NewArgVars, ExtraGoals, !ModeInfo),
+            ArgVars, NewArgVars, GoalInfo, ExtraGoals, !ModeInfo),
 
         (
             NewArgVars = ArgVars,
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.334
diff -u -r1.334 reference_manual.texi
--- doc/reference_manual.texi	20 Oct 2005 01:49:08 -0000	1.334
+++ doc/reference_manual.texi	28 Oct 2005 03:26:50 -0000
@@ -2166,7 +2166,7 @@
 * Abstract solver type declarations::
 * Solver type definitions::
 * Implementing solver types::
-* Solver type constraints and negated contexts::
+* Solver types and negated contexts::
 * Polymorphic solver types::
 @end menu
 
@@ -2348,18 +2348,16 @@
 program).
 @end itemize
 
- at node Solver type constraints and negated contexts
- at subsection Solver type constraints and negated contexts
+ at node Solver types and negated contexts
+ at subsection Solver types and negated contexts
 
-It is (a currently unchecked) error to place a constraint on a solver
-type variable in a negated context.  The reason for this is that the
-compiler does not understand what constraints mean and therefore it
-cannot enforce their negation outside a negated context.
-
-For this reason, soundness of a program is not guaranteed if constraints
-are placed on solver type variables inside negations or the conditions of
-if-then-else goals.  Particular care is needed since unification is a primary
-form of constraint.
+Referential transparency can be violated if a non-local solver type variable
+with inst @code{any} is used in a negated context (i.e., the body of a negated
+goal or the condition of an if-then-else) or in a lambda expression.  Programs
+are therefore required to place @code{impure} annotations on such goals or
+lambda expressions, even if they would normally be considered pure.  This
+impurity propagates through the enclosing goal structure as specified in
+ at ref{Impurity}.
 
 @node Polymorphic solver types
 @subsection Polymorphic solver types
Index: tests/invalid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/Mmakefile,v
retrieving revision 1.183
diff -u -r1.183 Mmakefile
--- tests/invalid/Mmakefile	28 Oct 2005 02:11:02 -0000	1.183
+++ tests/invalid/Mmakefile	28 Oct 2005 03:05:38 -0000
@@ -38,6 +38,7 @@
 	any_passed_as_ground \
 	any_should_not_match_bound \
 	any_to_ground_in_ite_cond \
+	anys_in_negated_contexts \
 	assert_in_interface \
 	bad_finalise_decl \
 	bad_initialise_decl \
Index: tests/invalid/anys_in_negated_contexts.err_exp
===================================================================
RCS file: tests/invalid/anys_in_negated_contexts.err_exp
diff -N tests/invalid/anys_in_negated_contexts.err_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/anys_in_negated_contexts.err_exp	28 Oct 2005 02:30:29 -0000
@@ -0,0 +1,28 @@
+anys_in_negated_contexts.m:035: In clause for `bad_if_then_else1(ia, out)':
+anys_in_negated_contexts.m:035:   in call to predicate
+anys_in_negated_contexts.m:035:   `anys_in_negated_contexts.ia/1':
+anys_in_negated_contexts.m:035:   purity error: goal should be impure because
+anys_in_negated_contexts.m:035:   it appears in a negated context, but involves
+anys_in_negated_contexts.m:035:   the following variables whose insts contain
+anys_in_negated_contexts.m:035:   `any': X
+anys_in_negated_contexts.m:043: In clause for `bad_if_then_else2(ia, out)':
+anys_in_negated_contexts.m:043:   in call to predicate
+anys_in_negated_contexts.m:043:   `anys_in_negated_contexts.ig/1':
+anys_in_negated_contexts.m:043:   purity error: goal is marked as impure, but
+anys_in_negated_contexts.m:043:   is actually pure
+anys_in_negated_contexts.m:056: In clause for `bad_negation1(ia)':
+anys_in_negated_contexts.m:056:   in call to predicate
+anys_in_negated_contexts.m:056:   `anys_in_negated_contexts.ia/1':
+anys_in_negated_contexts.m:056:   purity error: goal should be impure because
+anys_in_negated_contexts.m:056:   it appears in a negated context, but involves
+anys_in_negated_contexts.m:056:   the following variables whose insts contain
+anys_in_negated_contexts.m:056:   `any': X
+anys_in_negated_contexts.m:061: In clause for `bad_negation2(ia)':
+anys_in_negated_contexts.m:061:   in call to predicate
+anys_in_negated_contexts.m:061:   `anys_in_negated_contexts.ig/1':
+anys_in_negated_contexts.m:061:   purity error: goal is marked as impure, but
+anys_in_negated_contexts.m:061:   is actually pure
+anys_in_negated_contexts.m:082: In clause for `bad_lambda(in)':
+anys_in_negated_contexts.m:082:   purity error: lambda should be impure because
+anys_in_negated_contexts.m:082:   it contains the following non-local variables
+anys_in_negated_contexts.m:082:   whose insts contain `any': Y
Index: tests/invalid/anys_in_negated_contexts.m
===================================================================
RCS file: tests/invalid/anys_in_negated_contexts.m
diff -N tests/invalid/anys_in_negated_contexts.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/anys_in_negated_contexts.m	28 Oct 2005 02:29:46 -0000
@@ -0,0 +1,103 @@
+%-----------------------------------------------------------------------------%
+% anys_in_negated_contexts.m
+% Ralph Becket <rafe at cs.mu.OZ.AU>
+% Wed Oct 19 18:29:50 EST 2005
+% vim: ft=mercury ts=4 sw=4 et wm=0 tw=0
+%
+%-----------------------------------------------------------------------------%
+
+:- module anys_in_negated_contexts.
+
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module std_util.
+
+:- pred good_if_then_else(T::ia, int::out) is det.
+
+good_if_then_else(X, Y) :-
+    ( if   impure ia(X), ig(3)
+      then Y = 1
+      else Y = 2
+    ).
+
+:- pred bad_if_then_else1(T::ia, int::out) is det.
+
+bad_if_then_else1(X, Y) :-
+    ( if   ia(X), ig(3)
+      then Y = 1
+      else Y = 2
+    ).
+
+:- pred bad_if_then_else2(T::ia, int::out) is det.
+
+bad_if_then_else2(X, Y) :-
+    ( if   impure ia(X), impure ig(3)
+      then Y = 1
+      else Y = 2
+    ).
+
+:- pred good_negation(T::ia) is semidet.
+
+good_negation(X) :-
+    not (impure ia(X), ig(3)).
+
+:- pred bad_negation1(T::ia) is semidet.
+
+bad_negation1(X) :-
+    not (ia(X), ig(3)).
+
+:- pred bad_negation2(T::ia) is semidet.
+
+bad_negation2(X) :-
+    not (impure ia(X), impure ig(3)).
+
+:- pred pure_pred_mode_specific_clauses(int).
+:- mode pure_pred_mode_specific_clauses(in) is semidet.
+:- mode pure_pred_mode_specific_clauses(out) is det.
+:- pragma promise_pure(pure_pred_mode_specific_clauses/1).
+
+pure_pred_mode_specific_clauses(42::in).
+pure_pred_mode_specific_clauses(11::out).
+
+:- impure pred good_lambda(int::in) is semidet.
+
+good_lambda(X) :-
+    oa(Y),
+    P = (impure pred(Z::in) is semidet :- Y = Z),
+    impure P(X).
+
+:- pred bad_lambda(int::in) is semidet.
+
+bad_lambda(X) :-
+    oa(Y),
+    P = (pred(Z::in) is semidet :- Y = Z),
+    P(X).
+
+:- pred ia(T::ia) is semidet.
+
+ia(_) :-
+    semidet_succeed.
+
+:- pred ig(T::in) is semidet.
+
+ig(_) :-
+    semidet_succeed.
+
+:- pred oa(int::oa) is det.
+
+oa(42).
+
+main(!IO) :-
+    io.print("Hello, World!\n", !IO).
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
--------------------------------------------------------------------------
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