[m-rev.] for review: fix bug with impure lambda expressions
Julien Fischer
juliensf at cs.mu.OZ.AU
Wed Aug 10 18:44:51 AEST 2005
For review by Ralph or Zoltan.
Estimated hours taken: 8
Branches: main, release
Fix a bug reported by Peter Hawkins.
compiler/superhomogeneous.m:
When converting lambda expressions into superhomogeneous form,
position the compiler created unifications that correspond to
output arguments *after* the original body of the lambda.
Placing them all before the body, leads to problems if the body
is impure because mode analysis cannot reorder the unifications
over the impure goal as it needs to in order for the lambda to
be mode correct.
XXX According to a comment, intermod.m:643, we allow head
unifications to be reordered w.r.t impure goals, but this doesn't
seem to extend to lambda expressions for some reason. Actually,
the rules for reordering over impure goals should be less
strict then they currently are, at least for construction
and assignment unifications. (I'll look into this separately though).
Use unexpected/2 instead of error/1.
compiler/state_var.m:
Generalise the predicate finish_head_and_body/6 so that it works
on an arbitrary number of conjoined goals.
compiler/add_aditi.m:
compiler/add_clause.m:
Conform to the above changes.
tests/valid/Mmakefile:
tests/valid/impure_lambda_bug.m:
Test case for the above bug.
Workspace:/home/swordfish/juliensf/ws-debug
Index: compiler/add_aditi.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/add_aditi.m,v
retrieving revision 1.2
diff -u -r1.2 add_aditi.m
--- compiler/add_aditi.m 8 Aug 2005 02:33:07 -0000 1.2
+++ compiler/add_aditi.m 8 Aug 2005 02:39:33 -0000
@@ -258,7 +258,7 @@
transform_goal(ParsedGoal, Substitution, PredBody,
!VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO),
- finish_head_and_body(Context, FinalSVarMap, PredHead, PredBody,
+ finish_goals(Context, FinalSVarMap, [PredHead, PredBody],
PredGoal0, !.SInfo),
% Quantification will reduce this down to
Index: compiler/add_clause.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/add_clause.m,v
retrieving revision 1.3
diff -u -r1.3 add_clause.m
--- compiler/add_clause.m 8 Aug 2005 02:33:07 -0000 1.3
+++ compiler/add_clause.m 8 Aug 2005 02:39:33 -0000
@@ -508,7 +508,7 @@
prepare_for_body(FinalSVarMap, !VarSet, !SInfo),
transform_goal(Body0, Subst, Body, !VarSet, !ModuleInfo, !QualInfo,
!SInfo, !IO),
- finish_head_and_body(Context, FinalSVarMap, HeadGoal, Body, Goal0,
+ finish_goals(Context, FinalSVarMap, [HeadGoal, Body], Goal0,
!.SInfo),
qual_info_get_var_types(!.QualInfo, VarTypes0),
implicitly_quantify_clause_body(HeadVars, Warnings, Goal0, Goal,
Index: compiler/state_var.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/state_var.m,v
retrieving revision 1.1
diff -u -r1.1 state_var.m
--- compiler/state_var.m 26 Jul 2005 01:56:26 -0000 1.1
+++ compiler/state_var.m 4 Aug 2005 05:49:16 -0000
@@ -141,11 +141,11 @@
:- pred prepare_for_body(svar_map::out, prog_varset::in, prog_varset::out,
svar_info::in, svar_info::out) is det.
- % We have to conjoin the head and body and add unifiers to tie up all
+ % We have to conjoin the goals and add unifiers to tie up all
% the final values of the state variables to the head variables.
%
-:- pred finish_head_and_body(prog_context::in, svar_map::in,
- hlds_goal::in, hlds_goal::in, hlds_goal::out, svar_info::in) is det.
+:- pred finish_goals(prog_context::in, svar_map::in,
+ list(hlds_goal)::in, hlds_goal::out, svar_info::in) is det.
% Add some local state variables.
%
@@ -446,13 +446,14 @@
%-----------------------------------------------------------------------------%
-finish_head_and_body(Context, FinalSVarMap, Head, Body, Goal, SInfo) :-
+finish_goals(Context, FinalSVarMap, Goals0, Goal, SInfo) :-
goal_info_init(Context, GoalInfo),
- goal_to_conj_list(Head, HeadGoals),
- goal_to_conj_list(Body, BodyGoals),
+ list.map(goal_to_conj_list, Goals0, GoalsAsConjList),
Unifiers = svar_unifiers(yes(dont_warn_singleton), Context, FinalSVarMap,
SInfo ^ dot),
- conj_list_to_goal(HeadGoals ++ BodyGoals ++ Unifiers, GoalInfo, Goal).
+ Goals1 = list.condense(GoalsAsConjList),
+ Goals = Goals1 ++ Unifiers,
+ conj_list_to_goal(Goals, GoalInfo, Goal).
:- func svar_unifiers(maybe(goal_feature), prog_context, svar_map, svar_map)
= hlds_goals.
Index: compiler/superhomogeneous.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/superhomogeneous.m,v
retrieving revision 1.1
diff -u -r1.1 superhomogeneous.m
--- compiler/superhomogeneous.m 26 Jul 2005 01:56:26 -0000 1.1
+++ compiler/superhomogeneous.m 10 Aug 2005 08:34:08 -0000
@@ -12,6 +12,8 @@
% This module performs the conversion of clause bodies
% to superhomogeneous form.
+%-----------------------------------------------------------------------------%
+
:- module hlds__make_hlds__superhomogeneous.
:- interface.
@@ -28,6 +30,8 @@
:- import_module io.
:- import_module list.
+%-----------------------------------------------------------------------------%
+
:- type arg_context
---> head(pred_or_func, arity)
% the arguments in the head of the clause
@@ -101,9 +105,11 @@
io::di, io::uo) is det.
%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
:- implementation.
+:- import_module check_hlds__mode_util.
:- import_module check_hlds__purity.
:- import_module hlds__goal_util.
:- import_module hlds__make_hlds__add_clause.
@@ -124,9 +130,14 @@
:- import_module require.
:- import_module set.
:- import_module std_util.
+:- import_module string.
+:- import_module svvarset.
+:- import_module svset.
:- import_module term.
:- import_module varset.
+%-----------------------------------------------------------------------------%
+
insert_arg_unifications(HeadVars, Args0, Context, ArgContext,
!Goal, !VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO) :-
(
@@ -151,10 +162,10 @@
insert_arg_unifications_2([], [_ | _], _, _, _, _, _, _, _, !ModuleInfo,
!QualInfo, !SInfo, !IO) :-
- error("insert_arg_unifications_2: length mismatch").
+ unexpected(this_file, "insert_arg_unifications_2: length mismatch").
insert_arg_unifications_2([_ | _], [], _, _, _, _, _, _, _, !ModuleInfo,
!QualInfo, !SInfo, !IO) :-
- error("insert_arg_unifications_2: length mismatch").
+ unexpected(this_file, "insert_arg_unifications_2: length mismatch").
insert_arg_unifications_2([], [], _, _, _, !Goals, !VarSet, !ModuleInfo,
!QualInfo, !SInfo, !IO).
insert_arg_unifications_2([Var | Vars], [Arg | Args], Context, ArgContext,
@@ -219,7 +230,7 @@
!SInfo, !IO),
list__append(UnifyConj, !.Goals, !:Goals)
;
- error("insert_arg_unifications_with_supplied_contexts")
+ unexpected(this_file, "insert_arg_unifications_with_supplied_contexts")
).
:- pred insert_arg_unification(prog_var::in, prog_term::in, prog_context::in,
@@ -266,10 +277,10 @@
append_arg_unifications_2([], [_|_], _, _, _, _, _, _, _, !ModuleInfo,
!QualInfo, !SInfo, !IO) :-
- error("append_arg_unifications_2: length mismatch").
+ unexpected(this_file, "append_arg_unifications_2: length mismatch").
append_arg_unifications_2([_|_], [], _, _, _, _, _, _, _, !ModuleInfo,
!QualInfo, !SInfo, !IO) :-
- error("append_arg_unifications_2: length mismatch").
+ unexpected(this_file, "append_arg_unifications_2: length mismatch").
append_arg_unifications_2([], [], _, _, _, !List, !VarSet, !ModuleInfo,
!QualInfo, !SInfo, !IO).
append_arg_unifications_2([Var|Vars], [Arg|Args], Context, ArgContext,
@@ -703,6 +714,10 @@
ground_terms(Terms).
%-----------------------------------------------------------------------------%
+%
+% Code for building lambda expressions
+%
+
:- pred build_lambda_expression(prog_var::in, purity::in, pred_or_func::in,
lambda_eval_method::in, list(prog_term)::in, list(mode)::in,
determinism::in, goal::in, prog_context::in, unify_main_context::in,
@@ -715,39 +730,53 @@
ParsedGoal, Context, MainContext, SubContext, Goal, !VarSet,
!ModuleInfo, !QualInfo, !.SInfo, !IO) :-
%
- % In the parse tree, the lambda arguments can be any terms.
- % But in the HLDS, they must be distinct variables. So we introduce
+ % In the parse tree, the lambda arguments can be any terms, but
+ % in the HLDS they must be distinct variables. So we introduce
% fresh variables for the lambda arguments, and add appropriate
% unifications.
%
- % For example, we convert from
- % X = (func(f(A, B), c) = D :- G)
- % to
- % X = (func(H1, H2) = H3 :-
- % some [A, B] (H1 = f(A, B), H2 = c, H3 = D).
- %
- % Note that the quantification is important here.
- % That's why we need to introduce the explicit `some [...]'.
- % Variables in the argument positions are lambda-quantified,
- % so when we move them to the body, we need to make them
- % explicitly existentially quantified, to avoid capturing
- % any variables of the same name that occur outside this scope.
- %
- % For predicates, all variables occuring in the lambda arguments
- % are locally quantified to the lambda goal.
- % For functions, we need to be careful because variables in
- % arguments should similarly be quantified, but variables in
- % the function return value term (and not in the arguments)
- % should *not* be locally quantified.
+ % For example, we convert from:
%
-
+ % X = (func(f(A, B), c) = D :- Body )
+ %
+ % to:
%
- % Create fresh variables, transform the goal to HLDS,
- % and add unifications with the fresh variables.
- % We use varset__new_vars rather than make_fresh_arg_vars,
- % since for functions we need to ensure that the variable
- % corresponding to the function result term is a new variable,
- % to avoid the function result term becoming lambda-quantified.
+ % X = (func(H1, H2) = H3 :-
+ % some [A, B] (
+ % H1 = f(A, B),
+ % H2 = c,
+ % Body,
+ % H3 = D
+ % )
+ %
+ % Note that the quantification is important here. That's why we
+ % need to introduce the explicit `some [...]'. Variables in the
+ % argument positions are lambda-quantified, so when we move them to
+ % the body, we need to make them explicitly existentially quantified
+ % to avoid capturing any variables of the same name that occur
+ % outside this scope.
+ %
+ % Also, note that any introduced unifications that construct the
+ % output arguments for the lambda expression, need to occur *after*,
+ % the body of the lambda expression. This is in case the body of
+ % the lambda expression is impure, in which case the mode analyser
+ % cannot reorder the unifications; this results in a mode error.
+ %
+ % XXX the mode analyser *should* be able to reorder such unifications,
+ % especially ones that the compiler introduced itself.
+ %
+ % For predicates, all variables occurring in the lambda arguments are
+ % locally quantified to the lambda goal. For functions, we need to
+ % be careful because variables in arguments should similarly be
+ % quantified, but variables in the function return value term (and
+ % not in the arguments) should *not* be locally quantified.
+ %
+ % Create fresh variables, transform the goal to HLDS, and add
+ % unifications with the fresh variables. We use varset.new_vars
+ % rather than make_fresh_arg_vars, since for functions we need to
+ % ensure that the variable corresponding to the function result term
+ % is a new variable, to avoid the function result term becoming
+ % lambda-quantified.
%
(
illegal_state_var_func_result(PredOrFunc, Args0, StateVar)
@@ -763,26 +792,60 @@
prepare_for_lambda(!SInfo),
substitute_state_var_mappings(Args0, Args, !VarSet, !SInfo, !IO),
- list__length(Args, NumArgs),
- varset__new_vars(!.VarSet, NumArgs, LambdaVars, !:VarSet),
- map__init(Substitution),
- hlds_goal__true_goal(Head0),
+ list.length(Args, NumArgs),
+ svvarset.new_vars(NumArgs, LambdaVars, !VarSet),
+ %
+ % Partition the arguments (and their corresponding lambda variables)
+ % into two sets: those that are not output, i.e. input and unused,
+ % and those that are output.
+ %
+ (
+ partition_args_and_lambda_vars(!.ModuleInfo, Args, LambdaVars,
+ Modes, NonOutputArgs0, OutputArgs0, NonOutputLambdaVars0,
+ OutputLambdaVars0)
+ ->
+ NonOutputArgs = NonOutputArgs0,
+ OutputArgs = OutputArgs0,
+ NonOutputLambdaVars = NonOutputLambdaVars0,
+ OutputLambdaVars = OutputLambdaVars0
+ ;
+ unexpected(this_file,
+ "Mismatched lists in build_lambda_expression.")
+ ),
+
+ map.init(Substitution),
ArgContext = head(PredOrFunc, NumArgs),
-
- insert_arg_unifications(LambdaVars, Args, Context, ArgContext,
- Head0, Head, !VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO),
+ %
+ % Create the unifications that need to come before the body of
+ % the lambda expression; those corresponding to args whose mode
+ % is input or unused.
+ %
+ hlds_goal.true_goal(HeadBefore0),
+ insert_arg_unifications(NonOutputLambdaVars, NonOutputArgs,
+ Context, ArgContext, HeadBefore0, HeadBefore, !VarSet,
+ !ModuleInfo, !QualInfo, !SInfo, !IO),
+ %
+ % Create the unifications that need to come after the body of
+ % the lambda expression; those corresponding to args whose mode
+ % is output.
+ %
+ hlds_goal.true_goal(HeadAfter0),
+ insert_arg_unifications(OutputLambdaVars, OutputArgs,
+ Context, ArgContext, HeadAfter0, HeadAfter, !VarSet,
+ !ModuleInfo, !QualInfo, !SInfo, !IO),
prepare_for_body(FinalSVarMap, !VarSet, !SInfo),
transform_goal(ParsedGoal, Substitution,
Body, !VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO),
-
- finish_head_and_body(Context, FinalSVarMap,
- Head, Body, HLDS_Goal0, !.SInfo),
-
%
- % Now figure out which variables we need to
- % explicitly existentially quantify.
+ % Fix up any state variable unifications.
+ %
+ finish_goals(Context, FinalSVarMap, [HeadBefore, Body, HeadAfter],
+ HLDS_Goal0, !.SInfo),
+ %
+ % Figure out which variables we need to explicitly existentially
+ % quantify.
%
(
PredOrFunc = predicate,
@@ -791,21 +854,22 @@
PredOrFunc = function,
pred_args_to_func_args(Args, QuantifiedArgs, _ReturnValTerm)
),
- term__vars_list(QuantifiedArgs, QuantifiedVars0),
- list__sort_and_remove_dups(QuantifiedVars0, QuantifiedVars),
+ term.vars_list(QuantifiedArgs, QuantifiedVars0),
+ list.sort_and_remove_dups(QuantifiedVars0, QuantifiedVars),
goal_info_init(Context, GoalInfo),
HLDS_Goal = scope(exist_quant(QuantifiedVars), HLDS_Goal0) - GoalInfo,
-
%
- % We set the lambda nonlocals here to anything that
- % could possibly be nonlocal. Quantification will
- % reduce this down to the proper set of nonlocal arguments.
- %
- goal_util__goal_vars(HLDS_Goal, LambdaGoalVars0),
- set__delete_list(LambdaGoalVars0, LambdaVars, LambdaGoalVars1),
- set__delete_list(LambdaGoalVars1, QuantifiedVars, LambdaGoalVars2),
- set__to_sorted_list(LambdaGoalVars2, LambdaNonLocals),
+ % We set the lambda nonlocals here to anything that could
+ % possibly be nonlocal. Quantification will reduce this down to
+ % the proper set of nonlocal arguments.
+ %
+ some [!LambdaGoalVars] (
+ goal_util.goal_vars(HLDS_Goal, !:LambdaGoalVars),
+ svset.delete_list(LambdaVars, !LambdaGoalVars),
+ svset.delete_list(QuantifiedVars, !LambdaGoalVars),
+ LambdaNonLocals = set.to_sorted_list(!.LambdaGoalVars)
+ ),
make_atomic_unification(X,
lambda_goal(Purity, PredOrFunc, EvalMethod, modes_are_ok,
@@ -813,6 +877,34 @@
Context, MainContext, SubContext, Goal, !QualInfo)
).
+ % Partition the lists of arguments and variables into lists
+ % of non-output and output arguments and variables.
+ %
+ :- pred partition_args_and_lambda_vars(
+ module_info::in, list(prog_term)::in,
+ list(prog_var)::in, list(mode)::in,
+ list(prog_term)::out, list(prog_term)::out,
+ list(prog_var)::out, list(prog_var)::out) is semidet.
+
+partition_args_and_lambda_vars(_, [], [], [], [], [], [], []).
+partition_args_and_lambda_vars(ModuleInfo, [ Arg | Args ],
+ [ LambdaVar | LambdaVars ],
+ [Mode | Modes], InputArgs, OutputArgs,
+ InputLambdaVars, OutputLambdaVars) :-
+ partition_args_and_lambda_vars(ModuleInfo, Args, LambdaVars, Modes,
+ InputArgs0, OutputArgs0, InputLambdaVars0, OutputLambdaVars0),
+ ( mode_is_output(ModuleInfo, Mode) ->
+ InputArgs = InputArgs0,
+ OutputArgs = [Arg | OutputArgs0],
+ InputLambdaVars = InputLambdaVars0,
+ OutputLambdaVars = [ LambdaVar | OutputLambdaVars0 ]
+ ;
+ InputArgs = [ Arg | InputArgs0],
+ OutputArgs = OutputArgs0,
+ InputLambdaVars = [ LambdaVar | InputLambdaVars0 ],
+ OutputLambdaVars = OutputLambdaVars0
+ ).
+
:- pred check_expr_purity(purity::in, prog_context::in,
module_info::in, module_info::out, io::di, io::uo) is det.
@@ -825,3 +917,11 @@
).
%-----------------------------------------------------------------------------%
+
+:- func this_file = string.
+
+this_file = "superhomogeneous.m".
+
+%-----------------------------------------------------------------------------%
+:- end_module superhomogeneous.
+%-----------------------------------------------------------------------------%
Index: tests/valid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/valid/Mmakefile,v
retrieving revision 1.155
diff -u -r1.155 Mmakefile
--- tests/valid/Mmakefile 3 Aug 2005 12:04:46 -0000 1.155
+++ tests/valid/Mmakefile 4 Aug 2005 05:56:55 -0000
@@ -106,6 +106,7 @@
ho_unify \
id_type_bug \
implied_mode \
+ impure_lambda_bug \
indexing \
inhibit_warn_test \
inlining_bug \
Index: tests/valid/impure_lambda_bug.m
===================================================================
RCS file: tests/valid/impure_lambda_bug.m
diff -N tests/valid/impure_lambda_bug.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/valid/impure_lambda_bug.m 10 Aug 2005 08:32:24 -0000
@@ -0,0 +1,57 @@
+%
+% This is a cut-down version of a bug reported by Peter Hawkins.
+% Mercury rotd 2005-08-02 and before failed this because some of the
+% extra unifications required to convert the lambda expression to
+% superhomogenous form were put in the wrong spot if the body of the
+% lambda expression was impure. In particular the unifications for the
+% output arguments needed to be reordered by mode analysis so that they
+% occurred after whatever goal produces their RHS; in the case where the
+% body is impure so mode analysis could not do the necessary reordering.
+%
+:- module impure_lambda_bug.
+
+:- interface.
+
+:- type unit ---> unit.
+
+:- type alpha ---> alpha.
+
+:- type beta ---> beta.
+
+ % A cut down version of the original bug.
+ %
+:- pred foo((impure pred(unit, unit))::out((pred(di, uo) is det))) is det.
+
+ % A couple of other tests.
+ %
+:- pred baz((pred(alpha, beta, beta))::out(pred(out, di, uo) is det)) is det.
+:- pred func_foo((impure func(unit) = unit)::out) is det.
+:- pred with_unused((impure pred(unit, unit, unit))
+ ::out((pred(unused, di, uo) is det))) is det.
+
+:- implementation.
+
+foo(Pred) :-
+ Pred = (impure pred(!.A::di, !:A::uo) is det :-
+ impure bar(!A)
+ ).
+
+:- impure pred bar(unit, unit).
+:- mode bar(in, out) is det.
+:- mode bar(di, uo) is det.
+
+bar(!A) :- impure private_builtin.imp.
+
+baz(Pred) :-
+ Pred = (pred(R::out, A::di, B::uo) is det :-
+ A = B,
+ R = alpha
+ ).
+
+func_foo(Func) :-
+ Func = (impure func(In) = Out :- impure bar(In, Out)).
+
+with_unused(Pred) :-
+ Pred = (impure pred(_::unused, !.A::di, !:A::uo) is det :-
+ impure bar(!A)
+ ).
--------------------------------------------------------------------------
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