for review: fix bug in scoping for higher order terms

[Fergus Henderson]

The following change addresses the problem discussed in this thread.
I'd appreciate any comments, particularly regarding the documentation.

--------------------

Estimated hours taken: 4

Fix some problems with quantification of lambda expressions.

doc/reference_manual.texi:
	Document the new rules for quantification of lambda expressions.

compiler/make_hlds.m:
	Implement the new rules for quantification of lambda expressions:
	ensure that all variables in arguments of predicate or function
	lambda expressions are locally quantified, but that variables
	in the return value term of function lambda expressions are
	not locally quantified.
	
compiler/quantification.m:
	Add a comment about quantification of lambda expressions.
	Also, in `rename_apart', check for and optimize the case
	where no renaming is needed.

Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.130
diff -u -r1.130 reference_manual.texi
--- reference_manual.texi	1999/03/10 20:23:51	1.130
+++ reference_manual.texi	1999/03/11 00:43:37
@@ -721,15 +721,16 @@
 A lambda expression is a compound term of one of the following forms
 
 @example
-lambda([Var1::Mode1, Var2::Mode2, @dots{}] is Det, Goal)
-pred(Var1::Mode1, Var2::Mode2, @dots{}) is Det :- Goal
-pred(Var1::Mode1, Var2::Mode2, @dots{}, DCGMode0, DCGMode1) is Det --> DCGGoal
-func(Var1::Mode1, Var2::Mode2, @dots{}) = (Var::Mode) is Det :- Goal
-func(Var1, Var2, @dots{}) = Var :- Goal
+lambda([Arg1::Mode1, Arg2::Mode2, @dots{}] is Det, Goal)
+pred(Arg1::Mode1, Arg2::Mode2, @dots{}) is Det :- Goal
+pred(Arg1::Mode1, Arg2::Mode2, @dots{}, DCGMode0, DCGMode1) is Det --> DCGGoal
+func(Arg1::Mode1, Arg2::Mode2, @dots{}) = (Result::Mode) is Det :- Goal
+func(Arg1, Arg2, @dots{}) = Result :- Goal
 @end example
 
 @noindent
-where Var1, Var2, @dots{} are zero or more variables,
+where Arg1, Arg2, @dots{} are zero or more data-terms,
+Result is a data-term,
 Mode1, Mode2, @dots{} are zero or more modes (@pxref{Modes}),
 DCGMode0 and DCGMode1 are modes (@pxref{Modes}),
 Det is a determinism (@pxref{Determinism}),
@@ -739,7 +740,16 @@
 if it is not specified, then @samp{:- true} is assumed.
 A lambda expression denotes a higher-order predicate or function term
 whose value is the predicate or function of the specified arguments
-determined by the specified goal.
+determined by the specified goal.  
+A lambda expression introduces a new scope: any variables occuring in
+the arguments Arg1, Arg2, ... are locally quantified, i.e.
+any occurrences of variables with that name in the lambda
+expression are considered to name a different variable than any
+variables with the same name that occur outside of the
+lambda expression.  For variables which occur in Result or Goal,
+but not in the arguments, the usual Mercury rules for implicit
+quantification apply (@pxref{Implicit Quantification}).
+
 The form of lambda expression using @samp{-->} as its top level functor
 is a syntactic abbreviation: an expression of the form
Index: compiler/make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.284
diff -u -r1.284 make_hlds.m
--- make_hlds.m	1999/03/10 21:26:27	1.284
+++ make_hlds.m	1999/03/11 00:07:08
@@ -4522,25 +4522,82 @@
 :- mode build_lambda_expression(in, in, in, in, in, in, in,
 		in, in, in, out, out, in, out, di, uo) is det.
 
-build_lambda_expression(X, PredOrFunc, Vars1, Modes, Det, ParsedGoal, VarSet1,
+build_lambda_expression(X, PredOrFunc, Args, Modes, Det, ParsedGoal, VarSet0,
 		Context, MainContext, SubContext, Goal, VarSet,
 		Info1, Info) -->
-	{ make_fresh_arg_vars(Vars1, VarSet1, Vars, VarSet2) },
+	%
+	% 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.
+	%
+
+	%
+	% 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.
+	%
+	{ list__length(Args, NumArgs) },
+	{ varset__new_vars(VarSet0, NumArgs, LambdaVars, VarSet1) },
 	{ map__init(Substitution) },
-	transform_goal(ParsedGoal, VarSet2, Substitution,
-			HLDS_Goal0, VarSet3, Info1, Info2),
-	insert_arg_unifications(Vars, Vars1, Context, head, no,
-		HLDS_Goal0, VarSet3, HLDS_Goal, VarSet, Info2, Info),
+	transform_goal(ParsedGoal, VarSet1, Substitution,
+			HLDS_Goal0, VarSet2, Info1, Info2),
+	insert_arg_unifications(LambdaVars, Args, Context, head, no,
+		HLDS_Goal0, VarSet2, HLDS_Goal1, VarSet, Info2, Info),
 
-		 % quantification will reduce this down to
-		 % the proper set of nonlocal arguments.
-	{ goal_util__goal_vars(HLDS_Goal, LambdaGoalVars0) }, 
-	{ set__delete_list(LambdaGoalVars0, Vars, LambdaGoalVars1) },
+	%
+	% Now figure out which variables we need to explicitly existentially
+	% quantify.
+	%
+	{
+		PredOrFunc = predicate,
+		QuantifiedArgs = Args
+	;
+		PredOrFunc = function,
+		pred_args_to_func_args(Args, QuantifiedArgs, _ReturnValTerm),
+	},
+	{ term__vars_list(QuantifiedArgs, QuantifiedVars0) },
+	{ list__sort_and_remove_dups(QuantifiedVars0, QuantifiedVars) },
 
-	{ set__to_sorted_list(LambdaGoalVars1, LambdaNonLocals) },
+	{ goal_info_init(GoalInfo0) }
+	{ goal_info_set_context(GoalInfo0, Context, GoalInfo) },
+	{ HLDS_Goal = some(QuantifiedVars, HLDS_Goal1) - 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) },
 
 	{ create_atomic_unification(X,
-		lambda_goal(PredOrFunc, LambdaNonLocals, Vars, 
+		lambda_goal(PredOrFunc, LambdaNonLocals, LambdaVars, 
 			Modes, Det, HLDS_Goal),
 		Context, MainContext, SubContext, Goal) }.
 
Index: compiler/quantification.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/quantification.m,v
retrieving revision 1.62
diff -u -r1.62 quantification.m
--- quantification.m	1998/11/20 04:09:06	1.62
+++ quantification.m	1999/03/10 23:46:35
@@ -366,7 +366,12 @@
 			LambdaVars, Modes, Det, Goal),
 		Unification
 		) -->
-
+	%
+	% Note: make_hlds.m has already done most of the hard work
+	% for lambda expressions.  At this point, LambdaVars0
+	% should in fact be guaranteed to be fresh distinct
+	% variables.  However, the code below does not assume this.
+	%
 	quantification__get_outside(OutsideVars0),
 	{ set__list_to_set(LambdaVars0, QVars) },
 		% Figure out which variables have overlapping scopes
@@ -720,27 +725,32 @@
 :- mode quantification__rename_apart(in, out, in, out, in, out) is det.
 
 quantification__rename_apart(RenameSet, RenameMap, Goal0, Goal) -->
-	{ set__to_sorted_list(RenameSet, RenameList) },
-	quantification__get_varset(Varset0),
-	quantification__get_vartypes(VarTypes0),
-	{ map__init(RenameMap0) },
-	{ goal_util__create_variables(RenameList,
-		Varset0, VarTypes0, RenameMap0, VarTypes0, Varset0,
-			% ^ Accumulator		^ Reference ^Var names
-		Varset, VarTypes, RenameMap) },
-	{ goal_util__rename_vars_in_goal(Goal0, RenameMap, Goal) },
-	quantification__set_varset(Varset),
-	quantification__set_vartypes(VarTypes).
+	( { set__is_empty(RenameSet) } ->
+		{ map__init(RenameMap) },
+		{ Goal = Goal0 }
+	;
+		{ set__to_sorted_list(RenameSet, RenameList) },
+		quantification__get_varset(Varset0),
+		quantification__get_vartypes(VarTypes0),
+		{ map__init(RenameMap0) },
+		{ goal_util__create_variables(RenameList,
+			Varset0, VarTypes0, RenameMap0, VarTypes0, Varset0,
+				% ^ Accumulator		^ Reference ^Var names
+			Varset, VarTypes, RenameMap) },
+		{ goal_util__rename_vars_in_goal(Goal0, RenameMap, Goal) },
+		quantification__set_varset(Varset),
+		quantification__set_vartypes(VarTypes)
 /****
-	We don't need to add the newly created vars to the seen vars
-	because we won't find them anywhere else in the enclosing goal.
-	This is a performance improvement because it keeps the size of
-	the seen var set down.
-	quantification__get_seen(SeenVars0),
-	{ map__values(RenameMap, NewVarsList) },
-	{ set__insert_list(SeenVars0, NewVarsList, SeenVars) },
-	quantification__set_seen(SeenVars).
-***/
+		We don't need to add the newly created vars to the seen vars
+		because we won't find them anywhere else in the enclosing goal.
+		This is a performance improvement because it keeps the size of
+		the seen var set down.
+		quantification__get_seen(SeenVars0),
+		{ map__values(RenameMap, NewVarsList) },
+		{ set__insert_list(SeenVars0, NewVarsList, SeenVars) },
+		quantification__set_seen(SeenVars).
+****/
+	).
 
 %-----------------------------------------------------------------------------%
 
 

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.