[m-rev.] for review: improve checking of `any' in negated context

David Overton dmo at cs.mu.OZ.AU
Wed May 28 13:32:49 AEST 2003


On Wed, May 28, 2003 at 01:28:30PM +1000, Fergus Henderson wrote:
> Could you please post a new full diff?


Index: compiler/inst_match.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/inst_match.m,v
retrieving revision 1.52
diff -u -r1.52 inst_match.m
--- compiler/inst_match.m	15 Mar 2003 03:08:53 -0000	1.52
+++ compiler/inst_match.m	28 May 2003 03:30:46 -0000
@@ -123,6 +123,16 @@
 	% inst_matches_final into a single predicate inst_matches(When, ...)
 	% where When is either `initial' or `final'.
 
+	% inst_is_at_least_as_instantiated(InstA, InstB, Type, ModuleInfo)
+	% 	succeeds iff InstA is at least as instantiated as InstB.  This
+	% 	defines a partial order which is the same as
+	% 	inst_matches_initial except that uniqueness comparisons are
+	% 	reversed and we don't allow
+	% 	inst_is_at_least_as_instantiated(any, any).  
+
+:- pred inst_is_at_least_as_instantiated(inst, inst, type, module_info).
+:- mode inst_is_at_least_as_instantiated(in, in, in, in) is semidet.
+
 :- pred unique_matches_initial(uniqueness, uniqueness).
 :- mode unique_matches_initial(in, in) is semidet.
 
@@ -323,11 +333,16 @@
 
 :- type expansions == set(pair(inst)).
 
+:- type uniqueness_comparison
+	--->	match
+	;	instantiated.
+
 :- type inst_match_info
 	--->	inst_match_info(
 			module_info	:: module_info,
 			expansions	:: expansions,
-			maybe_sub	:: maybe(inst_var_sub)
+			maybe_sub	:: maybe(inst_var_sub),
+			uniqueness_comparison	:: uniqueness_comparison
 		).
 
 :- func sub(inst_match_info) = inst_var_sub is semidet.
@@ -342,7 +357,8 @@
 
 :- func init_inst_match_info(module_info) = inst_match_info.
 
-init_inst_match_info(ModuleInfo) = inst_match_info(ModuleInfo, Exp, no) :-
+init_inst_match_info(ModuleInfo) = inst_match_info(ModuleInfo, Exp, no, match)
+		:-
 	set__init(Exp).
 
 :- pred inst_matches_initial_2(inst, inst, maybe(type), 
@@ -400,23 +416,26 @@
 	% occur in `Expansions'.
 
 inst_matches_initial_4(any(UniqA), any(UniqB), _, I, I) :-
-	unique_matches_initial(UniqA, UniqB).
+	I ^ uniqueness_comparison = match,
+	compare_uniqueness(I ^ uniqueness_comparison, UniqA, UniqB).
 inst_matches_initial_4(any(_), free, _, I, I).
 inst_matches_initial_4(free, any(_), _, I, I).
 inst_matches_initial_4(free, free, _, I, I).
 inst_matches_initial_4(bound(UniqA, ListA), any(UniqB), _, Info, Info) :-
-	unique_matches_initial(UniqA, UniqB),
-	bound_inst_list_matches_uniq(ListA, UniqB, Info^module_info).
+	compare_uniqueness(Info ^ uniqueness_comparison, UniqA, UniqB),
+	compare_bound_inst_list_uniq(Info ^ uniqueness_comparison,
+		ListA, UniqB, Info^module_info).
 inst_matches_initial_4(bound(_Uniq, _List), free, _, I, I).
 inst_matches_initial_4(bound(UniqA, ListA), bound(UniqB, ListB), Type,
 		Info0, Info) :-
-	unique_matches_initial(UniqA, UniqB),
+	compare_uniqueness(Info0 ^ uniqueness_comparison, UniqA, UniqB),
 	bound_inst_list_matches_initial(ListA, ListB, Type, Info0, Info).
 inst_matches_initial_4(bound(UniqA, ListA), ground(UniqB, none), _,
 		Info, Info) :-
-	unique_matches_initial(UniqA, UniqB),
+	compare_uniqueness(Info ^ uniqueness_comparison, UniqA, UniqB),
 	bound_inst_list_is_ground(ListA, Info^module_info),
-	bound_inst_list_matches_uniq(ListA, UniqB, Info^module_info).
+	compare_bound_inst_list_uniq(Info ^ uniqueness_comparison,
+		ListA, UniqB, Info^module_info).
 inst_matches_initial_4(bound(Uniq, List), abstract_inst(_,_), _, Info, Info) :-
 	Uniq = unique,
 	bound_inst_list_is_ground(List, Info^module_info),
@@ -429,20 +448,20 @@
 		Info, Info) :-
 	\+ ground_inst_info_is_nonstandard_func_mode(GroundInstInfoA,
 		Info^module_info),
-	unique_matches_initial(UniqA, UniqB).
+	compare_uniqueness(Info ^ uniqueness_comparison, UniqA, UniqB).
 inst_matches_initial_4(ground(_Uniq, _PredInst), free, _, I, I).
 inst_matches_initial_4(ground(UniqA, _GII_A), bound(UniqB, ListB), MaybeType,
 		Info0, Info) :-
 	MaybeType = yes(Type),
 		% We can only check this case properly if the type is known.
-	unique_matches_initial(UniqA, UniqB),
+	compare_uniqueness(Info0 ^ uniqueness_comparison, UniqA, UniqB),
 	bound_inst_list_is_complete_for_type(set__init, Info0^module_info,
 		ListB, Type),
 	ground_matches_initial_bound_inst_list(UniqA, ListB, yes(Type),
 		Info0, Info).
 inst_matches_initial_4(ground(UniqA, GroundInstInfoA),
 		ground(UniqB, GroundInstInfoB), Type, Info0, Info) :-
-	unique_matches_initial(UniqA, UniqB),
+	compare_uniqueness(Info0 ^ uniqueness_comparison, UniqA, UniqB),
 	ground_inst_info_matches_initial(GroundInstInfoA, GroundInstInfoB,
 		UniqB, Type, Info0, Info).
 inst_matches_initial_4(ground(_UniqA, none), abstract_inst(_,_),_,_,_) :-
@@ -701,6 +720,22 @@
 
 %-----------------------------------------------------------------------------%
 
+	% Determine what kind of uniqueness comparison we are doing and then do
+	% it.
+	% If we are doing a "match" then call unique_matches_initial to do the
+	% comparison.
+	% If we are comparing "instantiatedness" then the uniqueness comparison
+	% is the reverse of when we are doing a match so call
+	% unique_matches_initial with the arguments reversed.
+
+:- pred compare_uniqueness(uniqueness_comparison, uniqueness, uniqueness).
+:- mode compare_uniqueness(in, in, in) is semidet.
+
+compare_uniqueness(match, InstA, InstB) :-
+	unique_matches_initial(InstA, InstB).
+compare_uniqueness(instantiated, InstA, InstB) :-
+	unique_matches_initial(InstB, InstA).
+
 unique_matches_initial(unique, _).
 unique_matches_initial(mostly_unique, mostly_unique).
 unique_matches_initial(mostly_unique, shared).
@@ -718,6 +753,15 @@
 
 %-----------------------------------------------------------------------------%
 
+:- pred compare_bound_inst_list_uniq(uniqueness_comparison, list(bound_inst),
+		uniqueness, module_info).
+:- mode compare_bound_inst_list_uniq(in, in, in, in) is semidet.
+
+compare_bound_inst_list_uniq(match, List, Uniq, ModuleInfo) :-
+	bound_inst_list_matches_uniq(List, Uniq, ModuleInfo).
+compare_bound_inst_list_uniq(instantiated, List, Uniq, ModuleInfo) :-
+	uniq_matches_bound_inst_list(Uniq, List, ModuleInfo).
+
 :- pred bound_inst_list_matches_uniq(list(bound_inst), uniqueness,
 					module_info).
 :- mode bound_inst_list_matches_uniq(in, in, in) is semidet.
@@ -970,6 +1014,11 @@
 			% check that [X|Xs] matches_final Ys.
 		bound_inst_list_matches_final([X|Xs], Ys, MaybeType)
 	).
+
+inst_is_at_least_as_instantiated(InstA, InstB, Type, ModuleInfo) :-
+	Info = init_inst_match_info(ModuleInfo) ^ 
+			uniqueness_comparison := instantiated,
+	inst_matches_initial_2(InstA, InstB, yes(Type), Info, _).
 
 inst_matches_binding(InstA, InstB, Type, ModuleInfo) :-
 	Info0 = init_inst_match_info(ModuleInfo),
Index: compiler/modecheck_unify.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modecheck_unify.m,v
retrieving revision 1.57
diff -u -r1.57 modecheck_unify.m
--- compiler/modecheck_unify.m	13 May 2003 23:56:17 -0000	1.57
+++ compiler/modecheck_unify.m	28 May 2003 03:30:46 -0000
@@ -93,8 +93,10 @@
 		Inst = UnifyInst,
 		Det = Det1,
 		mode_info_set_module_info(ModeInfo0, ModuleInfo1, ModeInfo1),
-		modecheck_set_var_inst(X, Inst, ModeInfo1, ModeInfo2),
-		modecheck_set_var_inst(Y, Inst, ModeInfo2, ModeInfo3),
+		modecheck_set_var_inst(X, Inst, yes(InstOfY),
+			ModeInfo1, ModeInfo2),
+		modecheck_set_var_inst(Y, Inst, yes(InstOfX),
+			ModeInfo2, ModeInfo3),
 		ModeOfX = (InstOfX -> Inst),
 		ModeOfY = (InstOfY -> Inst),
 		mode_info_get_var_types(ModeInfo3, VarTypes),
@@ -111,8 +113,8 @@
 			% that could cause an invalid call to
 			% `unify_proc__request_unify'
 		Inst = not_reached,
-		modecheck_set_var_inst(X, Inst, ModeInfo1, ModeInfo2),
-		modecheck_set_var_inst(Y, Inst, ModeInfo2, ModeInfo),
+		modecheck_set_var_inst(X, Inst, no, ModeInfo1, ModeInfo2),
+		modecheck_set_var_inst(Y, Inst, no, ModeInfo2, ModeInfo),
 			% return any old garbage
 		Unification = assign(X, Y),
 		ModeOfX = (InstOfX -> Inst),
@@ -386,7 +388,7 @@
 				X, ArgVars, PredOrFunc,
 				RHS0, Unification0, ModeInfo1,
 				RHS, Unification, ModeInfo2),
-		modecheck_set_var_inst(X, Inst, ModeInfo2, ModeInfo)
+		modecheck_set_var_inst(X, Inst, no, ModeInfo2, ModeInfo)
 	;
 		set__list_to_set([X], WaitingVars),
 		mode_info_error(WaitingVars,
@@ -399,7 +401,7 @@
 			% that could cause an invalid call to
 			% `unify_proc__request_unify'
 		Inst = not_reached,
-		modecheck_set_var_inst(X, Inst, ModeInfo1, ModeInfo),
+		modecheck_set_var_inst(X, Inst, no, ModeInfo1, ModeInfo),
 		ModeOfX = (InstOfX -> Inst),
 		ModeOfY = (InstOfY -> Inst),
 		Mode = ModeOfX - ModeOfY,
@@ -514,8 +516,10 @@
 		ModeOfX = (InstOfX -> Inst),
 		ModeOfY = (InstOfY -> Inst),
 		Mode = ModeOfX - ModeOfY,
-		modecheck_set_var_inst(X, Inst, ModeInfo2, ModeInfo3),
-		( bind_args(Inst, ArgVars0, ModeInfo3, ModeInfo4) ->
+		modecheck_set_var_inst(X, Inst, no,
+			ModeInfo2, ModeInfo3),
+		NoArgInsts = list__duplicate(length(ArgVars0), no),
+		( bind_args(Inst, ArgVars0, NoArgInsts, ModeInfo3, ModeInfo4) ->
 			ModeInfo = ModeInfo4
 		;
 			error("bind_args failed")
@@ -544,10 +548,12 @@
 			inst_expand_and_remove_constrained_inst_vars(
 				ModuleInfo1, InstOfX, InstOfX1),
 			list__length(ArgVars0, Arity),
-			get_arg_insts(InstOfX1, InstConsId, Arity, InstOfXArgs),
-			get_mode_of_args(Inst, InstOfXArgs, ModeOfXArgs0)
+			get_arg_insts(InstOfX1, InstConsId, Arity,
+				InstOfXArgs0),
+			get_mode_of_args(Inst, InstOfXArgs0, ModeOfXArgs0)
 		->
-			ModeOfXArgs = ModeOfXArgs0
+			ModeOfXArgs = ModeOfXArgs0,
+			InstOfXArgs = InstOfXArgs0
 		;
 			error("get_(inst/mode)_of_args failed")
 		),
@@ -559,8 +565,13 @@
 		split_complicated_subunifies(Unification1, ArgVars0,
 				Unification, ArgVars, ExtraGoals1,
 				ModeInfo3, ModeInfo4),
-		modecheck_set_var_inst(X, Inst, ModeInfo4, ModeInfo5),
-		( bind_args(Inst, ArgVars, ModeInfo5, ModeInfo6) ->
+		modecheck_set_var_inst(X, Inst, yes(InstOfY),
+			ModeInfo4, ModeInfo5),
+		UnifyArgInsts = list__map(func(I) = yes(I), InstOfXArgs),
+		(
+			bind_args(Inst, ArgVars, UnifyArgInsts,
+				ModeInfo5, ModeInfo6)
+		->
 			ModeInfo = ModeInfo6
 		;
 			error("bind_args failed")
@@ -582,8 +593,9 @@
 		ModeOfX = (InstOfX -> Inst),
 		ModeOfY = (InstOfY -> Inst),
 		Mode = ModeOfX - ModeOfY,
-		modecheck_set_var_inst(X, Inst, ModeInfo2, ModeInfo3),
-		( bind_args(Inst, ArgVars0, ModeInfo3, ModeInfo4) ->
+		modecheck_set_var_inst(X, Inst, no, ModeInfo2, ModeInfo3),
+		NoArgInsts = list__duplicate(length(ArgVars0), no),
+		( bind_args(Inst, ArgVars0, NoArgInsts, ModeInfo3, ModeInfo4) ->
 			ModeInfo = ModeInfo4
 		;
 			error("bind_args failed")
@@ -1235,41 +1247,44 @@
 
 %-----------------------------------------------------------------------------%
 
-:- pred bind_args(inst, list(prog_var), mode_info, mode_info).
-:- mode bind_args(in, in, mode_info_di, mode_info_uo) is semidet.
+:- pred bind_args(inst, list(prog_var), list(maybe(inst)),
+		mode_info, mode_info).
+:- mode bind_args(in, in, in, mode_info_di, mode_info_uo) is semidet.
 
-bind_args(not_reached, _) -->
+bind_args(not_reached, _, _) -->
 	{ instmap__init_unreachable(InstMap) },
 	mode_info_set_instmap(InstMap).
-bind_args(ground(Uniq, none), Args) -->
-	ground_args(Uniq, Args).
-bind_args(bound(_Uniq, List), Args) -->
+bind_args(ground(Uniq, none), Args, UnifyArgInsts) -->
+	ground_args(Uniq, Args, UnifyArgInsts).
+bind_args(bound(_Uniq, List), Args, UnifyArgInsts) -->
 	( { List = [] } ->
 		% the code is unreachable
 		{ instmap__init_unreachable(InstMap) },
 		mode_info_set_instmap(InstMap)
 	;
 		{ List = [functor(_, InstList)] },
-		bind_args_2(Args, InstList)
+		bind_args_2(Args, InstList, UnifyArgInsts)
 	).
-bind_args(constrained_inst_vars(_, Inst), Args) -->
-	bind_args(Inst, Args).
+bind_args(constrained_inst_vars(_, Inst), Args, UnifyArgInsts) -->
+	bind_args(Inst, Args, UnifyArgInsts).
 
-:- pred bind_args_2(list(prog_var), list(inst), mode_info, mode_info).
-:- mode bind_args_2(in, in, mode_info_di, mode_info_uo) is semidet.
+:- pred bind_args_2(list(prog_var), list(inst), list(maybe(inst)),
+		mode_info, mode_info).
+:- mode bind_args_2(in, in, in, mode_info_di, mode_info_uo) is semidet.
+
+bind_args_2([], [], []) --> [].
+bind_args_2([Arg | Args], [Inst | Insts], [UnifyArgInst | UnifyArgInsts]) -->
+	modecheck_set_var_inst(Arg, Inst, UnifyArgInst),
+	bind_args_2(Args, Insts, UnifyArgInsts).
+
+:- pred ground_args(uniqueness, list(prog_var), list(maybe(inst)),
+		mode_info, mode_info).
+:- mode ground_args(in, in, in, mode_info_di, mode_info_uo) is semidet.
 
-bind_args_2([], []) --> [].
-bind_args_2([Arg | Args], [Inst | Insts]) -->
-	modecheck_set_var_inst(Arg, Inst),
-	bind_args_2(Args, Insts).
-
-:- pred ground_args(uniqueness, list(prog_var), mode_info, mode_info).
-:- mode ground_args(in, in, mode_info_di, mode_info_uo) is det.
-
-ground_args(_Uniq, []) --> [].
-ground_args(Uniq, [Arg | Args]) -->
-	modecheck_set_var_inst(Arg, ground(Uniq, none)),
-	ground_args(Uniq, Args).
+ground_args(_Uniq, [], []) --> [].
+ground_args(Uniq, [Arg | Args], [UnifyArgInst | UnifyArgInsts]) -->
+	modecheck_set_var_inst(Arg, ground(Uniq, none), UnifyArgInst),
+	ground_args(Uniq, Args, UnifyArgInsts).
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/modes.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modes.m,v
retrieving revision 1.268
diff -u -r1.268 modes.m
--- compiler/modes.m	26 May 2003 09:00:02 -0000	1.268
+++ compiler/modes.m	28 May 2003 03:30:46 -0000
@@ -138,7 +138,7 @@
 :- import_module parse_tree__inst.
 :- import_module parse_tree__prog_data.
 
-:- import_module bool, list, io.
+:- import_module bool, list, io, std_util.
 
 	% modecheck(HLDS0, HLDS, UnsafeToContinue):
 	% Perform mode inference and checking for a whole module.
@@ -234,8 +234,20 @@
 :- mode modecheck_var_has_inst_list(in, in, in, in, out, mode_info_di, mode_info_uo)
 	is det.
 
-:- pred modecheck_set_var_inst(prog_var, inst, mode_info, mode_info).
-:- mode modecheck_set_var_inst(in, in, mode_info_di, mode_info_uo) is det.
+	% modecheck_set_var_inst(Var, Inst, MaybeUInst, ModeInfo0, ModeInfo).
+	% 	Assign the given Inst to the given Var, after checking that
+	% 	it is okay to do so.  If the inst to be assigned is the
+	% 	result of an abstract unification then the MaybeUInst
+	% 	argument should be the initial inst of the _other_ side of
+	% 	the unification.  This allows more precise (i.e. less
+	% 	conservative) checking in the case that Inst contains `any'
+	% 	components and Var is locked (i.e. is a nonlocal variable in
+	% 	a negated context).  Where the inst is not the result of an
+	% 	abstract unification then MaybeUInst should be `no'.
+
+:- pred modecheck_set_var_inst(prog_var, inst, maybe(inst),
+			mode_info, mode_info).
+:- mode modecheck_set_var_inst(in, in, in, mode_info_di, mode_info_uo) is det.
 
 :- pred modecheck_set_var_inst_list(list(prog_var), list(inst), list(inst),
 		int, list(prog_var), extra_goals, mode_info, mode_info).
@@ -1721,7 +1733,7 @@
 		% record the fact that Var was bound to ConsId in the instmap
 	{ list__duplicate(AdjustedArity, free, ArgInsts) },
 	modecheck_set_var_inst(Var,
-		bound(unique, [functor(ConsId, ArgInsts)])).
+		bound(unique, [functor(ConsId, ArgInsts)]), no).
 
 %-----------------------------------------------------------------------------%
 
@@ -1945,11 +1957,12 @@
 		instmap__lookup_var(InstMap0, Var0, VarInst0),
 		handle_implied_mode(Var0, VarInst0, InitialInst,
 		 	Var, ExtraGoals0, ExtraGoals, ModeInfo0, ModeInfo1),
-		modecheck_set_var_inst(Var0, FinalInst, ModeInfo1, ModeInfo2),
+		modecheck_set_var_inst(Var0, FinalInst, no,
+			ModeInfo1, ModeInfo2),
 		( Var = Var0 ->
 			ModeInfo = ModeInfo2
 		;
-			modecheck_set_var_inst(Var, FinalInst,
+			modecheck_set_var_inst(Var, FinalInst, no,
 				ModeInfo2, ModeInfo)
 		)
 	;
@@ -1959,11 +1972,11 @@
 	).
 
 	% Note that there are two versions of modecheck_set_var_inst,
-	% one with arity 7 and one with arity 4.
+	% one with arity 7 and one with arity 5.
 	% The former is used for predicate calls, where we may need
 	% to introduce unifications to handle calls to implied modes.
 
-modecheck_set_var_inst(Var0, FinalInst, ModeInfo00, ModeInfo) :-
+modecheck_set_var_inst(Var0, FinalInst, MaybeUInst, ModeInfo00, ModeInfo) :-
 	mode_info_get_instmap(ModeInfo0, InstMap0),
 	mode_info_get_parallel_vars(PVars0, ModeInfo00, ModeInfo0),
 	( instmap__is_reachable(InstMap0) ->
@@ -1982,6 +1995,8 @@
 			error("modecheck_set_var_inst: unify_inst failed")
 		),
 		mode_info_set_module_info(ModeInfo0, ModuleInfo, ModeInfo1),
+		mode_info_get_var_types(ModeInfo1, VarTypes),
+		map__lookup(VarTypes, Var0, Type),
 		(
 			% if the top-level inst of the variable is not_reached,
 			% then the instmap as a whole must be unreachable
@@ -1993,8 +2008,6 @@
 			% If we haven't added any information and
 			% we haven't bound any part of the var, then
 			% the only thing we can have done is lose uniqueness.
-			mode_info_get_var_types(ModeInfo1, VarTypes),
-			map__lookup(VarTypes, Var0, Type),
 			inst_matches_initial(Inst0, Inst, Type, ModuleInfo)
 		->
 			instmap__set(InstMap0, Var0, Inst, InstMap),
@@ -2004,8 +2017,6 @@
 			% lost some uniqueness, or bound part of the var.
 			% The call to inst_matches_binding will succeed
 			% only if we haven't bound any part of the var.
-			mode_info_get_var_types(ModeInfo1, VarTypes),
-			map__lookup(VarTypes, Var0, Type),
 			inst_matches_binding(Inst, Inst0, Type, ModuleInfo)
 		->
 			% We've just added some information
@@ -2018,8 +2029,22 @@
 				ModeInfo2, ModeInfo3)
 		;
 			% We've bound part of the var.  If the var was locked,
-			% then we need to report an error.
-			mode_info_var_is_locked(ModeInfo1, Var0, Reason0)
+			% then we need to report an error...
+			mode_info_var_is_locked(ModeInfo1, Var0, Reason0),
+			\+ (
+				% ...unless the goal is a unification and the
+				% var was unified with something no more
+				% instantiated than itself.
+				% This allows for the case of `any = free', for
+				% example. The call to
+				% inst_matches_binding, above will fail for the
+				% var with mode `any >> any' however, it should
+				% be allowed because it has only been unified
+				% with a free variable.
+				MaybeUInst = yes(UInst),
+				inst_is_at_least_as_instantiated(Inst, UInst,
+					Type, ModuleInfo)
+			)
 		->
 			set__singleton_set(WaitingVars, Var0),
 			mode_info_error(WaitingVars,
Index: tests/hard_coded/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/hard_coded/Mmakefile,v
retrieving revision 1.197
diff -u -r1.197 Mmakefile
--- tests/hard_coded/Mmakefile	7 May 2003 06:42:43 -0000	1.197
+++ tests/hard_coded/Mmakefile	28 May 2003 03:30:47 -0000
@@ -7,6 +7,7 @@
 ORDINARY_PROGS=	\
 	address_of_builtins \
 	agg \
+	any_free_unify \
 	bidirectional \
 	brace \
 	builtin_inst_rename \
Index: tests/hard_coded/any_free_unify.exp
===================================================================
RCS file: tests/hard_coded/any_free_unify.exp
diff -N tests/hard_coded/any_free_unify.exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/any_free_unify.exp	28 May 2003 03:30:47 -0000
@@ -0,0 +1 @@
+yes
Index: tests/hard_coded/any_free_unify.m
===================================================================
RCS file: tests/hard_coded/any_free_unify.m
diff -N tests/hard_coded/any_free_unify.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/any_free_unify.m	28 May 2003 03:30:47 -0000
@@ -0,0 +1,33 @@
+:- module any_free_unify.
+
+:- interface.
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+
+:- implementation.
+
+:- import_module std_util, list, bool.
+
+main -->
+	{ test_any_free_unify([], Result1) },
+	io__print(Result1), io__nl.
+
+:- pred test_any_free_unify(list(int), bool).
+:- mode test_any_free_unify(in(list_skel(any)), out) is det.
+
+% In the unification in the condition of the if-then-else, the variable
+% List has an inst which includes `any' components.  Normally, we can't
+% check whether `any' has become further instantiated over a goal so we
+% do not allow it in a negated context.  However, in this case, the
+% `any' component is unified with `free' so we know that it cannot have
+% become further instantiated.  Therefore we should allow the
+% unification in the condition.
+
+test_any_free_unify(List, Result) :-
+	( List = [_ | _] ->
+		Result = no
+	;
+		Result = yes
+	).

-- 
David Overton                  Uni of Melbourne     +61 3 8344 1354
dmo at cs.mu.oz.au                Monash Uni (Clayton) +61 3 9905 5779
http://www.cs.mu.oz.au/~dmo    Mobile Phone         +61 4 0337 4393
--------------------------------------------------------------------------
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