diff: det_report.m: report error for nondet functions

[Fergus Henderson]

Hi,

Zoltan, can you please review this one?

compiler/det_report.m:
	Report an error if a "forward" mode of a function,
	(a mode for which all the arguments are fully input)
	has determinism nondet, multi, cc_nondet or cc_multi.
	Such functions should be illegal because they break
	referential transparency.

doc/reference_manual.texi:
	Document the above change.

tests/invalid/Mmake:
tests/invalid/multisoln_func.m:
	Test cases for the above change.

Index: det_report.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/det_report.m,v
retrieving revision 1.36
diff -u -r1.36 det_report.m
--- det_report.m	1997/07/01 04:03:50	1.36
+++ det_report.m	1997/07/03 13:59:03
@@ -168,7 +168,60 @@
 	;
 		{ ModuleInfo2 = ModuleInfo1 }
 	),
-	global_checking_pass(Rest, ModuleInfo2, ModuleInfo).
+	% Functions can only have more than one solution if it is a
+	% non-standard mode.  Otherwise, they would not be referentially
+	% transparent.  (Nondeterministic "functions" like C's `rand()'
+	% function are not allowed.)
+	(
+		% if it is a mode for a function...
+		{ pred_info_get_is_pred_or_func(PredInfo, function) },
+		% ... that can succeed more than once ...
+		{ determinism_components(InferredDetism, _CanFail, NumSolns) },
+		{ NumSolns \= at_most_zero },
+		{ NumSolns \= at_most_one },
+		% ... but for which all the arguments are input ...
+		{ proc_info_argmodes(ProcInfo, PredArgModes) },
+		{ pred_args_to_func_args(PredArgModes,
+			FuncArgModes, _FuncResultMode) },
+		{ \+ (
+			list__member(FuncArgMode, FuncArgModes),
+			\+ mode_is_fully_input(ModuleInfo2, FuncArgMode)
+		  )
+	 	} 
+	->
+		% ... then it is an error.
+		{ pred_info_name(PredInfo, PredName) },
+		{ proc_info_context(ProcInfo, FuncContext) },
+		prog_out__write_context(FuncContext),
+		io__write_string("Error: invalid determinism for `"),
+		report_pred_name_mode(function, PredName, PredArgModes),
+		io__write_string("':\n"),
+		prog_out__write_context(FuncContext),
+		io__write_string(
+			"  the primary mode for a function cannot be `"),
+		mercury_output_det(InferredDetism),
+		io__write_string(
+			"'.\n"),
+		globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
+		( { VerboseErrors = yes } ->
+			io__write_strings([
+"\tIn Mercury, a function is supposed to be a true mathematical function\n",
+"\tof its arguments; that is, the value of the function's result should\n",
+"\tbe determined only by the values of its arguments.\n",
+"\t(Allowing functions to have more than one result for the same\n",
+"\targuments would break referential transparency.)\n",
+"\tMost likely, this procedure should be a predicate, not a function.\n"
+			])
+		;
+			[]
+		),
+		{ module_info_incr_errors(ModuleInfo2,
+			ModuleInfo3) }
+		
+	;
+		{ ModuleInfo3 = ModuleInfo2 }
+	),
+	global_checking_pass(Rest, ModuleInfo3, ModuleInfo).
 
 det_check_lambda(DeclaredDetism, InferredDetism, Goal, GoalInfo, DetInfo,
 		Msgs) :-

Index: ../doc/reference_manual.texi
===================================================================
RCS file: /home/staff/zs/imp/mercury/doc/reference_manual.texi,v
retrieving revision 1.50
diff -u -r1.50 reference_manual.texi
--- reference_manual.texi	1997/04/22 03:11:57	1.50
+++ reference_manual.texi	1997/07/03 14:25:18
@@ -1515,6 +1515,14 @@
 If you want to write a partial function, i.e. one whose determinism
 is @samp{semidet}, then you must explicitly declare the mode and determinism.
 
+In Mercury, a function is supposed to be a true mathematical function
+of its arguments; that is, the value of the function's result should
+be determined only by the values of its arguments.  Hence, for
+any mode of a function that specifies that all the arguments are fully
+input (i.e. for which the initial inst of all the arguments is a ground inst),
+the determinism of that mode can only be
+ at samp{det}, @samp{semidet}, @samp{erroneous}, or @samp{failure}.
+
 The determinism categories form this lattice:
 
 @example

Index: Mmake
===================================================================
RCS file: /home/staff/zs/imp/tests/invalid/Mmake,v
retrieving revision 1.18
diff -u -r1.18 Mmake
--- Mmake	1997/06/27 04:05:20	1.18
+++ Mmake	1997/07/03 13:57:28
@@ -23,6 +23,7 @@
 	modes_erroneous.m \
 	mostly_uniq1.m \
 	mostly_uniq2.m \
+	multisoln_func.m \
 	occurs.m \
 	pragma_c_code_and_clauses1.m \
 	pragma_c_code_and_clauses2.m \
@@ -38,6 +39,8 @@
 #	prog_io_erroneous.m \
 #	qualified_cons_id2.m \
 #	types.m
+
+MCFLAGS-multisoln_func	=	--infer-types
 
 DEPS=		$(SOURCES:%.m=%.dep)
 DEPENDS=	$(SOURCES:%.m=%.depend)

:- module multisoln_func.
:- interface.
:- import_module io.

:- pred main(io__state::di, io__state::uo) is det.

:- implementation.
:- import_module int, list, std_util.

main --> [].

:- func f(int) = list(int).
:- mode f(in) = out is cc_multi.	% illegal

f(X) = L :-
	unsorted_solutions((pred(Y::out) is multi :- Y = X ; Y = X + 1), L).

:- func test = int.
:- mode test = out is cc_multi.	% illegal

test = 123.
test = 456.

% test type inference

:- mode test2 = out is multi.	% illegal
test2 = 123.
test2 = 456.

:- mode test3(in) = out is nondet.	% illegal
test3(1) = 123.
test3(1) = 456.

:- mode test3b(in) = out is cc_nondet.	% illegal
test3b(1) = 123.
test3b(1) = 456.

% this one is legal
:- func test4(int::out) = (int::out) is multi.
test4(1) = 1.
test4(2) = 2.

% this one is legal
:- func test5(int::out) = (int::in) is cc_nondet.
test5(1) = 42.
test5(2) = 42.

multisoln_func.m:026: Inferred :- func test2 = int.
multisoln_func.m:030: Inferred :- func test3(int) = int.
multisoln_func.m:034: Inferred :- func test3b(int) = int.
multisoln_func.m:013: Error: invalid determinism for `f(in) = out'.
multisoln_func.m:013:   The primary mode for a function cannot be `cc_multi'.
multisoln_func.m:019: Error: invalid determinism for `test = out'.
multisoln_func.m:019:   The primary mode for a function cannot be `cc_multi'.
multisoln_func.m:026: Error: invalid determinism for `test2 = out'.
multisoln_func.m:026:   The primary mode for a function cannot be `multi'.
multisoln_func.m:030: Error: invalid determinism for `test3(in) = out'.
multisoln_func.m:030:   The primary mode for a function cannot be `nondet'.
multisoln_func.m:034: Error: invalid determinism for `test3b(in) = out'.
multisoln_func.m:034:   The primary mode for a function cannot be `cc_nondet'.
For more information, try recompiling with `-E'.

-- 
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.