[m-rev.] diff: avoid spurious infinite recursion warning

[Fergus Henderson]

Estimated hours taken: 1
Branches: main

compiler/simplify.m:
	Avoid issuing warnings about infinite recursion in the case
	when the recursive call involves input arguments whose inst
	is `any', since such warnings may be spurious.

tests/valid/Mmakefile:
tests/valid/Mercury.options:
tests/valid/solv.m:
	Regression test.

Workspace: /home/ceres/fjh/mercury
Index: compiler/simplify.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/simplify.m,v
retrieving revision 1.119
diff -u -d -r1.119 simplify.m
--- compiler/simplify.m	29 May 2003 18:17:15 -0000	1.119
+++ compiler/simplify.m	13 Oct 2003 02:20:56 -0000
@@ -1282,6 +1282,29 @@
 		simplify__input_args_are_equiv(Args, HeadVars, ArgModes,
 			CommonInfo1, ModuleInfo1),
 
+		%
+		% Don't warn if the input arguments' modes initial insts
+		% contain `any' insts, since the arguments might have become
+		% more constrained before the recursive call, in which case
+		% the recursion might eventually terminate.
+		%
+		% XXX The following check will only warn if the inputs are
+		% all fully ground; i.e. we won't warn in the case of
+		% partially instantiated insts such as list_skel(free).
+		% Still, it is better to miss warnings in that rare and
+		% unsupported case rather than to issue spurious warnings
+		% in cases involving `any' insts.  We should only warn about
+		% definite nontermination here, not possible nontermination;
+		% warnings about possible nontermination should only be given
+		% if the termination analysis pass is enabled.
+		%
+		all [ArgMode] (
+			(list__member(ArgMode, ArgModes),
+			 mode_is_input(ModuleInfo1, ArgMode))
+		=>
+			mode_is_fully_input(ModuleInfo1, ArgMode)
+		),
+
 		% 
 		% Don't count procs using minimal evaluation as they 
 		% should always terminate if they have a finite number
Index: tests/valid/Mercury.options
===================================================================
RCS file: /home/mercury1/repository/tests/valid/Mercury.options,v
retrieving revision 1.9
diff -u -d -r1.9 Mercury.options
--- tests/valid/Mercury.options	26 Jul 2003 07:19:08 -0000	1.9
+++ tests/valid/Mercury.options	13 Oct 2003 02:23:49 -0000
@@ -84,6 +84,7 @@
 MCFLAGS-simplify_bug		= -O-1
 MCFLAGS-simplify_bug2		= -O3
 MCFLAGS-spurious_purity_warning	= --halt-at-warn
+MCFLAGS-solv			= --halt-at-warn
 MCFLAGS-tuple_eqv               = --smart-recompilation
 MCFLAGS-two_way_unif		= -O-1
 MCFLAGS-type_inf_ambig_test	= --infer-all
Index: tests/valid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/valid/Mmakefile,v
retrieving revision 1.130
diff -u -d -r1.130 Mmakefile
--- tests/valid/Mmakefile	25 Jul 2003 02:27:37 -0000	1.130
+++ tests/valid/Mmakefile	13 Oct 2003 02:22:58 -0000
@@ -164,6 +164,7 @@
 	simplify_bug \
 	simplify_bug2 \
 	soln_context \
+	solv \
 	some_switch \
 	spurious_purity_warning \
 	stack_alloc \
Index: tests/valid/solv.m
===================================================================
RCS file: tests/valid/solv.m
diff -N tests/valid/solv.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/valid/solv.m	13 Oct 2003 02:28:39 -0000
@@ -0,0 +1,118 @@
+%-----------------------------------------------------------------------------%
+
+% This test case is a regression test to check that we don't
+% issue a spurious warning about infinite recursion in recursive
+% procedures such as label/1 whose inputs initial inst contains `any'.
+
+%-----------------------------------------------------------------------------%
+
+% This module is an example of how to write a finite domain solver.
+
+:- module solv.
+:- interface.
+:- import_module io, list, int.
+
+% :- type fd_var.	% For Mercury versions < rotd-25-07-03
+:- solver type fd_var.  % For Mercury versions > rotd-25-07-03
+
+	% initialize an unconstrained fd_var
+:- pred init_any(fd_var).
+:- mode init_any(free >> any) is det.
+
+	% unify an fd_var with an int
+:- pred fd_var == int.
+:- mode in == out is det.
+:- mode (any >> ground) == in is semidet.
+
+	% constrain an fd_var to be greater than the specified int
+:- pred fd_var > int.
+:- mode in(any) > in is semidet.
+
+	% constrain an fd_var to be less than the specified int
+:- pred fd_var < int.
+:- mode in(any) < in is semidet.
+
+	% Given a list of constrained fd_vars, nondeterminstically
+	% find bindings for the variables that meet those constraints.
+	% The output list here will be the same as the input list,
+	% but with ground values for all the variables.
+:- pred labeling(list(fd_var), list(fd_var)).
+:- mode labeling(in(list_skel(any)), out) is nondet.
+
+	% Given a list of constrained fd_vars, 
+	% print out all possible bindings for the variables
+	% that meet those constraints.  The order in which
+	% the solutions will be printed is unspecified.
+:- pred print_labeling(list(fd_var), io__state, io__state).
+:- mode print_labeling(in(list_skel(any)), di, uo) is cc_multi.
+
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+:- import_module std_util.
+
+:- solver type fd_var
+	---> fd_var(c_pointer).
+
+print_labeling(Vars) -->
+	unsorted_aggregate(labeling(Vars), print_solution).
+
+:- pred print_solution(list(fd_var), io__state, io__state).
+:- mode print_solution(in, di, uo) is det.
+
+print_solution(Vars) -->
+	io__print("Here's a solution: "),
+	io__write_list(Vars, ", ", print_var),
+	io__nl.
+
+:- pred print_var(fd_var, io__state, io__state).
+:- mode print_var(in, di, uo) is det.
+print_var(Var) -->
+	{ Var == Val }, % convert ground fd_var to int
+	io__write_int(Val).
+
+labeling([], []).
+labeling([V | Vs0], [V | Vs]) :-
+	label(V),
+	labeling(Vs0, Vs).
+
+:- pred label(fd_var).
+:- mode label(any >> ground) is nondet.
+:- pragma promise_pure(label/1).
+
+label(V) :-
+	impure solver_min_domain(V, Min),
+	impure solver_max_domain(V, Max),
+	(if Min = Max then
+		promise_ground(V)
+	else
+		( V == Min
+		; V > Min,
+		  label(V)
+		)
+	).
+
+:- pred promise_ground(fd_var).
+:- mode promise_ground(any >> ground) is det.
+
+:- pragma foreign_proc("C", promise_ground(X :: any >> ground),
+	[promise_pure, will_not_call_mercury, thread_safe],
+	"/* assert(X->min == X->max); */").
+
+:- impure pred solver_min_domain(fd_var, int).
+:-        mode solver_min_domain(in(any), out) is det.
+
+:- impure pred solver_max_domain(fd_var, int).
+:-        mode solver_max_domain(in(any), out) is det.
+
+%-----------------------------------------------------------------------------%
+
+% Implementing the following is left as an exercise for the reader...
+:- external(init_any/1).
+:- external(solver_min_domain/2).
+:- external(solver_max_domain/2).
+:- external((==)/2).
+:- external((>)/2).
+:- external((<)/2).
+
+%-----------------------------------------------------------------------------%

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------