[m-rev.] for review: predicate equivalence type and inst declarations

[Simon Taylor]

On 13-Mar-2002, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> On 11-Mar-2002, Simon Taylor <stayl at cs.mu.OZ.AU> wrote:
> > Index: NEWS
> ...
> > +* Predicate and function types and modes can now be defined in terms of
> > +  higher-order predicate and function types and insts.
> 
> Maybe the following would be better?
> 
> * Predicate and function type declarations and mode declarations
>   can now use higher-order predicate and function types and insts,
>   rather than explicitly listing the types and modes of the arguments.

* Predicate and function type and mode declarations can now be expressed
  in terms of higher-order predicate and function types and insts, rather
  than explicitly listing the argument types and modes. 
 
> > This is useful
> > +  where several predicates or functions must have the the same type and
> > +  mode signature.
> > +
> > +  For example:
> > +	:- type foldl_pred(T, U) == pred(T, U, U).
> > +	:- inst foldl_pred == pred(in, in, out) is det.
> 
> You need parentheses around the `pred(in, in, out) is det' part.

Done.
 
> > Index: compiler/equiv_type.m
> 
> The documentation at the top of this module should be changed
> to explain the new functionality.
> 
> It should also be mentioned in compiler/notes/compiler_design.html.

Done.

> > Index: compiler/make_hlds.m
> > +	;
> > +		% equiv_type.m should have either set the pred_or_func
> > +		% or removed the item from the list.
> > +		{ error(
> > +		"add_item_decl_pass_1: no pred_or_func on mode declaration") }
> > +	).
> 
> It would be nicer to use unexpected/2 rather than error/1 here.

> > +			{ error(
> > +	"module_add_class_method: no pred_or_func on mode declaration") }
> > +		)
> 
> Likewise here.

Done.
 
> > Index: compiler/mercury_to_mercury.m
> > ===================================================================
> >  mercury_output_item(UnqualifiedItemNames,
> >  		pred_or_func(TypeVarSet, InstVarSet, ExistQVars,
> > -			PredOrFunc, PredName0, TypesAndModes, Det,
> > +			PredOrFunc, PredName0, TypesAndModes,
> > +			WithType, WithInst, Det,
> >  			_Cond, Purity, ClassContext),
> >  		Context) -->
> >  	{ maybe_unqualify_sym_name(UnqualifiedItemNames, PredName0, PredName) },
> >  	maybe_output_line_number(Context),
> >  	(
> > -		{ PredOrFunc = predicate },
> > -		mercury_format_pred_decl(TypeVarSet, InstVarSet, ExistQVars,
> > -			PredName, TypesAndModes, Det, Purity,
> > -			ClassContext, Context,
> > +		(
> > +			{ PredOrFunc = predicate }
> > +		;
> > +			{ PredOrFunc = function },
> > +			{ WithType = yes(_) }
> > +		)
> 
> Why do functions without a withtype declaration get treated differently?
> A brief comment here would help.
> 
> Also it might be clear to invert the condition of the if-then-else.

Done.

> > @@ -1751,7 +1788,15 @@
> >  		add_string("(")
> >  	),
> >  	add_purity_prefix(Purity),
> > -	add_string("pred "),
> > +
> > +	(
> > +		{ PredOrFunc = predicate },
> > +		add_string("pred ")
> > +	;
> > +		{ PredOrFunc = function },
> > +		add_string("func ")
> > +	),
> 
> Use hlds_out__pred_or_func_to_str.

Done.
 
> > Index: compiler/prog_data.m
> > ===================================================================
> > RCS file: /home/mercury1/repository/mercury/compiler/prog_data.m,v
> > retrieving revision 1.80
> > diff -u -u -r1.80 prog_data.m
> > --- compiler/prog_data.m	7 Mar 2002 08:30:16 -0000	1.80
> > +++ compiler/prog_data.m	7 Mar 2002 14:27:49 -0000
> > +		%	The WithType and WithInst fields are set to `no' by
> > +		%	equiv_type.m unless there was an error in the
> > +		%	`with_type` and `with_inst` annotations.
> 
> I suggest making the comment a bit more explicit, e.g. something along
> the lines of this:

Done.
 
> > Index: compiler/prog_io.m
> ...
> > +	    ( MaybeDeterminism = yes(_), WithInst = yes(_) ->
> > +		R = error("`with_inst` and determinism both specified", Body)
> > +	    ; MaybeDeterminism = yes(_), WithType = yes(_) ->
> > +		R = error("`with_type` and determinism both specified", Body)
> > +	    ; WithInst = yes(_), WithType = no ->
> > +		R = error("`with_inst` specified without `with_type`", Body)
> ...
> > +		Result = error("`with_inst` and determinism both specified",
> > +				Body)
> ...
> > +			WithInst = error("invalid inst in `with_inst`",
> > +					Inst1)
> ...
> > +				Result = error(
> > +	"`with_inst` specified, but function arguments don't have modes",
> > +					FuncTerm)
> 
> There should be test cases for all these errors.

Done.
 
> > Index: doc/reference_manual.texi
> > ===================================================================
> > RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
> > retrieving revision 1.243
> > diff -u -u -r1.243 reference_manual.texi
> > --- doc/reference_manual.texi	5 Mar 2002 16:55:14 -0000	1.243
> > +++ doc/reference_manual.texi	6 Mar 2002 14:35:44 -0000
> > @@ -1555,6 +1555,31 @@
> >  :- func length(list(T)) = int.
> >  @end example
> >  
> > +A predicate or function can by declared to have a given higher-order
> > +type by using `with_type` in the type declaration.
> 
> The concept "higher-order type" has not been introduced yet
> at this point in the language reference manual.

I've moved the pointer to "Higher-order" to just after "higher-order type".

> > +:- pred p(int) `with_type` foldl_pred(T, U).
> > +:- pred f(int) `with_type` foldl_func(T, U).
> 
> s/pred f/func f/

Done.
 
> > + at end example
> > +
> > + at noindent
> > +is equivalent to
> > +
> > + at example
> > +:- pred p(int, T, U, U).
> > +:- pred f(int, T, U) = U.
> > + at end example
> 
> This is definition-by-example.

No more than the rest of this section.

> >  Type variables in predicate and function declarations
> >  are implicitly universally quantified by default;
> >  that is, the predicate or function may be called with arguments
> > @@ -2029,6 +2054,30 @@
> >  @example
> >  :- func length(list(T)::in) = (int::out).
> >  :- pred append(list(T)::in, list(T)::in, list(T)::out).
> > +
> > +:- pred p `with_type` foldl_pred(T, U) `with_inst` foldl_pred.
> > + at end example
> 
> This example occurs before `with_inst` has been discussed.
> It would be better to delete the example with `with_inst` here,
> and instead put it at the end of the section explaining `with_inst`.

Done.

> > + at example
> > +:- mode p(in, in, in, out) is det.
> > +:- mode f(in, in, in) = out is det.
> >  @end example
> 
> This uses `is det', which has not been explained yet.

I've added a pointer to the "Determinism" chapter.

> I think it might be best to move all the discussion of `with_type`
> and `with_inst` into the "Higher order" chapter, and just have
> a forward reference to it from this section.

I disagree. All the methods for declaring predicate and function
types and modes should be in the one place.
 
> > Index: library/std_util.m
> > ===================================================================
> The name in the comment is wrong: s/may_maybe/map_foldl_maybe/

> Also, I suggest s/foldl/fold/g
> 
> Finally, it seems silly to put `map_fold_maybe' in the standard
> library without having `fold_maybe'.

All done.




Estimated hours taken: 40
Branches: main

Allow declarations of the form
:- pred p `with_type` higher_order_type `with_inst` higher_order_inst.

XXX We should allow `with_inst` annotations on higher-order terms.

compiler/prog_data.m:
	Add fields to `pred_or_func' and `pred_or_func_mode'
	items to hold the `with_type` and `with_inst` annotations.

compiler/prog_io.m:
compiler/prog_io_typeclass.m:
	Parse the annotations.

compiler/module_qual.m:
	Module qualify the annotations.

compiler/equiv_type.m:
	Expand away `with_type` and `with_inst`. Report errors.

	Strip items containing errors from the item list.

	Record smart recompilation dependencies on the types and
	modes expanded. Also record a dependency on the arity of
	predicate and function declarations before expansion.

	Use error_util for error messages.

compiler/mercury_to_mercury.m:
	Write `with_type` and `with_inst` annotations to interface files.

compiler/make_hlds.m:
	Ignore `with_type` and `with_inst` fields in predicate and
	function declarations.

compiler/recompilation.m:
	Changes to allow equiv_type.m to record dependencies on
	arbitrary items, not just types.

compiler/recompilation_usage.m:
compiler/recompilation_check.m:
	Allow searches in the sets of used predicates and functions using
	name, not name and arity, as the key. This is needed because
	the actual arity of a predicate defined using `with_type` is
	not known when writing the interface files.

compiler/recompilation_version.m:
	Handle `with_inst` and `with_type`.

	Pragmas now need to be recorded in the version_numbers even
	if there is no matching `:- pred' or `:- func' declaration --
	the pragma may apply to a predicate or function declared using
	`with_type`.

compiler/modules.m:
	Document why with_type can't be handled properly on `main/2'
	(this only affects the IL backend).

compiler/mode_util.m:
	Export inst_subsitute_arg_list for use by equiv_type.m.

compiler/error_util.m:
	Add predicate `pred_or_func_to_string'.

library/std_util.m:
	Add std_util__map_foldl_maybe and std_util__map_foldl2_maybe,
	which are like list__map_foldl and list__map_foldl2, but 
	apply to the item stored in a value of type std_util__maybe.

NEWS:
doc/reference_manual.texi:
	Document the new syntax and library predicates.

tests/invalid/Mmakefile:
tests/invalid/with_type.m:
tests/invalid/with_type.err_exp:
tests/recompilation/TESTS:
tests/recompilation/unchanged_with_type_nr*:
tests/recompilation/with_type_re*:
	Test cases.

tests/invalid/errors1.err_exp:
tests/invalid/type_loop.err_exp:
tests/invalid/vars_in_wrong_places.err_exp:
	Update expected output.

diff -u NEWS NEWS
--- NEWS
+++ NEWS
@@ -6,6 +6,7 @@
 
 Changes to the Mercury language:
 * Improved support for higher-order functions.
+* Predicate and function equivalence type and mode declarations.
 * Support for defining predicates or functions
   using different clauses for different modes.
 * Support for Haskell-like "@" expressions.
@@ -28,14 +29,24 @@
 
 Changes to the Mercury language:
 
-* Predicate and function types and modes can now be defined in terms of
-  higher-order predicate and function types and insts.  This is useful
+* Predicate and function type and mode declarations can now be expressed
+  in terms of higher-order predicate and function types and insts, rather
+  than explicitly listing the argument types and modes.  This is useful
   where several predicates or functions must have the the same type and
   mode signature.
 
   For example:
 	:- type foldl_pred(T, U) == pred(T, U, U).
-	:- inst foldl_pred == pred(in, in, out) is det.
+	:- inst foldl_pred == (pred(in, in, out) is det).
 	:- pred p `with_type` foldl_pred(T, U) `with_inst` foldl_pred.
  
   For more information see the "Predicate and function type declarations"
@@ -184,11 +186,11 @@
   comparison of values of type `tm' whose `tm_dst' fields are identical
   is equivalent to comparison of the times those values represent.
 
-* We've added predicates `std_util__map_maybe/3',
-  `std_util__map_foldl_maybe/5' and `std_util__map_foldl2_maybe/7',
-  and function `std_util__map_maybe/2' which are analogous to
-  `list__map', `list__map_foldl' and `list__map_foldl2', but which
-  work on the value stored in a term of type `std_util__maybe'.
+* std_util.m now contains predicates and functions `map_maybe',
+  `fold_maybe', `map_fold_maybe' and `map_fold2_maybe', which are
+  analogues of `list__map', `list__foldl', `list__map_foldl' and
+  `list__map_foldl2' operating on values of type `maybe' instead
+  of `list'.
 
 * We've added a predicate to io.m to return the last modification time
   of a file (io__file_modification_time).
diff -u compiler/equiv_type.m compiler/equiv_type.m
--- compiler/equiv_type.m
+++ compiler/equiv_type.m
@@ -5,7 +5,8 @@
 %-----------------------------------------------------------------------------%
 
 % This module contains a parse-tree to parse-tree transformation
-% that expands equivalence types.
+% that expands equivalence types. It also expands away `with_type`
+% and `with_inst` annotations on predicate and function type declarations.
 
 % main author: fjh
 
@@ -22,13 +23,17 @@
 	% First it builds up a map from type_ctor to the equivalent type.
 	% Then it traverses through the list of items, expanding all types. 
 	% This has the effect of eliminating all the equivalence types
-	% from the source code. Error messages are generated for any
-	% circular equivalence types.
+	% from the source code.
 	%
-	% For items not defined in the current module, record the
-	% equivalence types expanded while processing each item
-	% in the recompilation_info. This is needed for smart
-	% recompilation.
+	% `with_type` and `with_inst` annotations on predicate and
+	% function type declarations are also expaneded.
+	%
+	% Error messages are generated for any circular equivalence types
+	% and invalid `with_type` and `with_inst` annotations.
+	%
+	% For items not defined in the current module, the items expanded
+	% while processing each item are recorded in the recompilation_info,
+	% for use by smart recompilation.
 :- pred equiv_type__expand_eqv_types(module_name, list(item_and_context),
 		list(item_and_context), bool, eqv_map,
 		maybe(recompilation_info), maybe(recompilation_info),
diff -u compiler/make_hlds.m compiler/make_hlds.m
--- compiler/make_hlds.m
+++ compiler/make_hlds.m
@@ -255,7 +255,7 @@
 	;
 		% equiv_type.m should have either set the pred_or_func
 		% or removed the item from the list.
-		{ error(
+		{ unexpected(this_file,
 		"add_item_decl_pass_1: no pred_or_func on mode declaration") }
 	).
 
@@ -2577,7 +2577,7 @@
 		;
 			% equiv_type.m should have either set the
 			% pred_or_func or removed the item from the list.
-			{ error(
+			{ unexpected(this_file,
 	"module_add_class_method: no pred_or_func on mode declaration") }
 		)
 	).
@@ -8522,5 +8522,8 @@
 		words(Message)
 		] },
 	error_util__write_error_pieces(Context, 0, ErrorPieces).
+
+:- func this_file = string.
+this_file = "make_hlds.m".
 
 %------------------------------------------------------------------------------%
diff -u compiler/mercury_to_mercury.m compiler/mercury_to_mercury.m
--- compiler/mercury_to_mercury.m
+++ compiler/mercury_to_mercury.m
@@ -425,23 +425,22 @@
 	{ maybe_unqualify_sym_name(UnqualifiedItemNames, PredName0, PredName) },
 	maybe_output_line_number(Context),
 	(
-		(
-			{ PredOrFunc = predicate }
-		;
-			{ PredOrFunc = function },
-			{ WithType = yes(_) }
-		)
+		% Function declarations using `with_type` have the same
+		% format as predicate declarations, but with `func' instead
+		% of `pred'.
+		{ PredOrFunc = function },
+		{ WithType = no }
 	->
-		mercury_format_pred_or_func_decl(PredOrFunc, TypeVarSet,
-			InstVarSet, ExistQVars, PredName, TypesAndModes,
-			WithType, WithInst, Det, Purity, ClassContext, Context,
-			":- ", ".\n", ".\n")
-	;
 		{ pred_args_to_func_args(TypesAndModes, FuncTypesAndModes,
 				RetTypeAndMode) },
 		mercury_format_func_decl(TypeVarSet, InstVarSet, ExistQVars,
 			PredName, FuncTypesAndModes, RetTypeAndMode, Det,
 			Purity, ClassContext, Context, ":- ", ".\n", ".\n")
+	;
+		mercury_format_pred_or_func_decl(PredOrFunc, TypeVarSet,
+			InstVarSet, ExistQVars, PredName, TypesAndModes,
+			WithType, WithInst, Det, Purity, ClassContext, Context,
+			":- ", ".\n", ".\n")
 	).
 
 mercury_output_item(UnqualifiedItemNames,
@@ -451,21 +450,17 @@
 	{ maybe_unqualify_sym_name(UnqualifiedItemNames, PredName0, PredName) },
 	maybe_output_line_number(Context),
 	(
-		{
-			PredOrFunc = no
-		;
-			PredOrFunc = yes(predicate)
-		;
-			PredOrFunc = yes(function),
-			WithInst = yes(_)
-		}
+		% Function mode declarations using `with_type` have
+		% the same format as predicate mode declarations.
+		{ PredOrFunc = yes(function) },
+		{ WithInst = no }
 	->
-		mercury_output_pred_mode_decl(VarSet, PredName, Modes,
-			WithInst, MaybeDet, Context)
-	;
 		{ pred_args_to_func_args(Modes, FuncModes, RetMode) },
 		mercury_output_func_mode_decl(VarSet, PredName,
 			FuncModes, RetMode, MaybeDet, Context)
+	;
+		mercury_output_pred_mode_decl(VarSet, PredName, Modes,
+			WithInst, MaybeDet, Context)
 	).
 
 mercury_output_item(_, module_defn(VarSet, ModuleDefn), Context) -->
@@ -749,19 +744,12 @@
 		% `:- typeclass declaration'.
 		{ unqualify_name(Name0, Name) },
 		(
-			(
-				{ PredOrFunc = predicate }
-			;
-				{ PredOrFunc = function },
-				{ WithType = yes(_) }
-			)
+			% Function declarations using `with_type` have the
+			% same format as predicate declarations, but with
+			% `func' instead of `pred'.
+			{ PredOrFunc = function },
+			{ WithType = no }
 		->
-			mercury_format_pred_or_func_decl(PredOrFunc,
-				TypeVarSet, InstVarSet, ExistQVars,
-				unqualified(Name), TypesAndModes,
-				WithType, WithInst, Detism, Purity,
-				ClassContext, Context, "", ",\n\t", "")
-		;
 			{ pred_args_to_func_args(TypesAndModes,
 				FuncTypesAndModes, RetTypeAndMode) },
 			mercury_format_func_decl(TypeVarSet, InstVarSet,
@@ -769,6 +757,12 @@
 				FuncTypesAndModes, RetTypeAndMode,
 				Detism, Purity, ClassContext, Context,
 				"", ",\n\t", "")
+		;
+			mercury_format_pred_or_func_decl(PredOrFunc,
+				TypeVarSet, InstVarSet, ExistQVars,
+				unqualified(Name), TypesAndModes,
+				WithType, WithInst, Detism, Purity,
+				ClassContext, Context, "", ",\n\t", "")
 		)
 	;
 		{ Method = pred_or_func_mode(VarSet, PredOrFunc,
@@ -779,23 +773,19 @@
 		% `:- typeclass declaration'.
 		{ unqualify_name(Name0, Name) },
 		(
-			(
-				{ PredOrFunc = no }
-			;
-				{ PredOrFunc = yes(predicate) }
-			;
-				{ PredOrFunc = yes(function) },
-				{ WithInst = yes(_) }
-			)
+			% Function mode declarations using `with_type` have
+			% the same format as predicate mode declarations.
+			{ PredOrFunc = yes(function) },
+			{ WithInst = no }
 		->
-			mercury_format_pred_or_func_mode_decl_2(VarSet,
-				unqualified(Name), Modes,
-				WithInst, Detism, Context, "", "")
-		;
 			{ pred_args_to_func_args(Modes, FuncModes, RetMode) },
 			mercury_format_func_mode_decl_2(VarSet,
 				unqualified(Name), FuncModes, RetMode,
 				Detism, Context, "", "")
+		;
+			mercury_format_pred_or_func_mode_decl_2(VarSet,
+				unqualified(Name), Modes,
+				WithInst, Detism, Context, "", "")
 		)
 	).
 
@@ -1792,13 +1782,9 @@
 	),
 	add_purity_prefix(Purity),
 
-	(
-		{ PredOrFunc = predicate },
-		add_string("pred ")
-	;
-		{ PredOrFunc = function },
-		add_string("func ")
-	),
+	{ hlds_out__pred_or_func_to_str(PredOrFunc, PredOrFuncStr) },
+	add_string(PredOrFuncStr),
+	add_string(" "),
 
 	(
 		{ Types = [Type | Rest] }
diff -u compiler/module_qual.m compiler/module_qual.m
--- compiler/module_qual.m
+++ compiler/module_qual.m
@@ -552,8 +552,8 @@
 		Info1) },
 	qualify_types_and_modes(TypesAndModes0, TypesAndModes, Info1, Info2),
 	qualify_class_constraints(Constraints0, Constraints, Info2, Info3),
-	map_foldl2_maybe(qualify_type, WithType0, WithType, Info3, Info4),
-	map_foldl2_maybe(qualify_inst, WithInst0, WithInst, Info4, Info).
+	map_fold2_maybe(qualify_type, WithType0, WithType, Info3, Info4),
+	map_fold2_maybe(qualify_inst, WithInst0, WithInst, Info4, Info).
 
 module_qualify_item(
 		pred_or_func_mode(A, PredOrFunc, SymName, Modes0,
@@ -566,7 +566,7 @@
 		pred_or_func_mode(PredOrFunc, SymName- Arity) - Context,
 		Info1) },
 	qualify_mode_list(Modes0, Modes, Info1, Info2),
-	map_foldl2_maybe(qualify_inst, WithInst0, WithInst, Info2, Info).
+	map_fold2_maybe(qualify_inst, WithInst0, WithInst, Info2, Info).
 
 module_qualify_item(pragma(Pragma0) - Context, pragma(Pragma) - Context,
 						Info0, Info, yes) -->
@@ -1058,8 +1058,8 @@
 		MQInfo0, MQInfo1),
 	qualify_class_constraints(ClassContext0, ClassContext, 
 		MQInfo1, MQInfo2),
-	map_foldl2_maybe(qualify_type, WithType0, WithType, MQInfo2, MQInfo3),
-	map_foldl2_maybe(qualify_inst, WithInst0, WithInst, MQInfo3, MQInfo).
+	map_fold2_maybe(qualify_type, WithType0, WithType, MQInfo2, MQInfo3),
+	map_fold2_maybe(qualify_inst, WithInst0, WithInst, MQInfo3, MQInfo).
 qualify_class_method(
 		pred_or_func_mode(Varset, PredOrFunc, Name, Modes0,
 			WithInst0, MaybeDet, Cond, Context), 
@@ -1068,7 +1068,7 @@
 		MQInfo0, MQInfo
 		) -->
 	qualify_mode_list(Modes0, Modes, MQInfo0, MQInfo1),
-	map_foldl2_maybe(qualify_inst, WithInst0, WithInst, MQInfo1, MQInfo).
+	map_fold2_maybe(qualify_inst, WithInst0, WithInst, MQInfo1, MQInfo).
 
 :- pred qualify_instance_body(sym_name::in, instance_body::in, 
 	instance_body::out) is det. 
diff -u compiler/prog_data.m compiler/prog_data.m
--- compiler/prog_data.m
+++ compiler/prog_data.m
@@ -68,22 +68,19 @@
 		%	ArgTypesAndModes, WithType, WithInst, Determinism,
 		%	Cond, Purity, TypeClassContext
 		%
-		%	The WithType and WithInst fields are set to `no' by
-		%	equiv_type.m unless there was an error in the
-		%	`with_type` and `with_inst` annotations.
+		%	The WithType and WithInst fields hold the `with_type`
+		% 	and `with_inst` annotations, which are syntactic
+		%	sugar that is expanded by equiv_type.m
+		%	equiv_type.m will set these fields to `no'.
 
 	; 	pred_or_func_mode(inst_varset, maybe(pred_or_func), sym_name,
 			list(mode), maybe(inst), maybe(determinism), condition)
 		%       VarNames, PredOrFunc, PredName, ArgModes, WithInst,
 		%	Determinism, Cond
 		%
-		% 	For mode declarations using `with_inst` we don't
-		%	know whether it's a predicate or function until
-		%	we've expanded the inst.
-		%
-		%	The WithInst field is set to `no' by
-		%	equiv_type.m unless there was an error in the
-		%	`with_type` and `with_inst` annotations.
+		%	The WithInst field holds the `with_inst` annotation,
+		%	which is syntactic sugar that is expanded by
+		%	equiv_type.m. equiv_type.m will set the field to `no'.
 
 	;	pragma(pragma_type)
 
@@ -534,13 +531,13 @@
 			condition, purity, class_constraints, prog_context)
 		%       TypeVarNames, InstVarNames,
 		%	ExistentiallyQuantifiedTypeVars,
-		%	PredOrFunc, PredName, ArgTypes, Determinism, Cond
-		%	Purity, ClassContext, Context
+		%	PredOrFunc, PredName, ArgTypes, WithType, Determinism,
+		%	Cond, Purity, ClassContext, Context
 
 	; 	pred_or_func_mode(inst_varset, maybe(pred_or_func), sym_name,
 			list(mode), maybe(inst), maybe(determinism),
 			condition, prog_context)
-		%       InstVarNames, PredOrFunc, PredName, ArgModes,
+		%       InstVarNames, MaybePredOrFunc, PredName, ArgModes,
 		%	Determinism, WithInst, Cond
 		%	Context
 		%
diff -u compiler/prog_io.m compiler/prog_io.m
--- compiler/prog_io.m
+++ compiler/prog_io.m
@@ -1384,19 +1384,17 @@
 		R = error("`with_inst` specified without `with_type`", Body)
 	    ;
 		(
-		    (
-			PredOrFunc = predicate
-		    ;
-			PredOrFunc = function,
-			WithType = yes(_)
-		    )
+		    % Function declarations with `with_type` annotations have
+		    % the same form as predicate declarations.
+		    PredOrFunc = function,
+		    WithType = no
 		->
+		    process_func(ModuleName, VarSet, Body, Condition,
+				MaybeDeterminism, Attributes, R)
+		;
 		    process_pred_or_func(PredOrFunc, ModuleName, VarSet,
 		    		Body, Condition, WithType, WithInst,
 				MaybeDeterminism, Attributes, R)
-		;
-		    process_func(ModuleName, VarSet, Body, Condition,
-				WithInst, MaybeDeterminism, Attributes, R)
 		)
 	    )
 	;
@@ -1544,7 +1542,7 @@
 			WithInst = ok(yes(Inst))
 		;
 			WithInst = error("invalid inst in `with_inst`",
-					Inst1)
+					Body0)
 		),
 		Body = Body1
 	;
@@ -2136,28 +2134,26 @@
 	% parse a `:- func p(...)' declaration
 
 :- pred process_func(module_name, varset, term, condition,
-		maybe(inst), maybe(determinism), decl_attrs, maybe1(item)).
-:- mode process_func(in, in, in, in, in, in, in, out) is det.
+		maybe(determinism), decl_attrs, maybe1(item)).
+:- mode process_func(in, in, in, in, in, in, out) is det.
 
-process_func(ModuleName, VarSet, Term, Cond, WithInst, MaybeDet,
-		Attributes0, Result) :-
+process_func(ModuleName, VarSet, Term, Cond, MaybeDet, Attributes0, Result) :-
 	get_class_context(ModuleName, Attributes0, Attributes, MaybeContext),
 	(
 		MaybeContext = ok(ExistQVars, Constraints),
-		process_func_2(ModuleName, VarSet, Term, Cond,
-			WithInst, MaybeDet, ExistQVars,
-			Constraints, Attributes, Result) 
+		process_func_2(ModuleName, VarSet, Term, Cond, MaybeDet,
+			ExistQVars, Constraints, Attributes, Result) 
 	;
 		MaybeContext = error(String, ErrorTerm),
 		Result = error(String, ErrorTerm)
 	).
 
 :- pred process_func_2(module_name, varset, term, condition,
-	maybe(inst), maybe(determinism), existq_tvars,
-	class_constraints, decl_attrs, maybe1(item)).
-:- mode process_func_2(in, in, in, in, in, in, in, in, in, out) is det.
+	maybe(determinism), existq_tvars, class_constraints,
+	decl_attrs, maybe1(item)).
+:- mode process_func_2(in, in, in, in, in, in, in, in, out) is det.
 
-process_func_2(ModuleName, VarSet, Term, Cond, WithInst, MaybeDet, 
+process_func_2(ModuleName, VarSet, Term, Cond, MaybeDet, 
 		ExistQVars, Constraints, Attributes, Result) :-
 	(
 		Term = term__functor(term__atom("="),
@@ -2165,20 +2161,19 @@
 	->
 		parse_implicitly_qualified_term(ModuleName, FuncTerm, Term,
 			"`:- func' declaration", R),
-		process_func_3(R, FuncTerm, ReturnTypeTerm, VarSet, WithInst,
-				MaybeDet, Cond, ExistQVars, Constraints,
-				Attributes, Result)
+		process_func_3(R, FuncTerm, ReturnTypeTerm, VarSet, MaybeDet,
+			Cond, ExistQVars, Constraints, Attributes, Result)
 	;
 		Result = error("`=' expected in `:- func' declaration", Term)
 	).
 
 
-:- pred process_func_3(maybe_functor, term, term, varset, maybe(inst),
+:- pred process_func_3(maybe_functor, term, term, varset,
 		maybe(determinism), condition, existq_tvars,
 		class_constraints, decl_attrs, maybe1(item)).
-:- mode process_func_3(in, in, in, in, in, in, in, in, in, in, out) is det.
+:- mode process_func_3(in, in, in, in, in, in, in, in, in, out) is det.
 
-process_func_3(ok(F, As0), FuncTerm, ReturnTypeTerm, VarSet0, WithInst,
+process_func_3(ok(F, As0), FuncTerm, ReturnTypeTerm, VarSet0,
 		MaybeDet, Cond, ExistQVars, ClassContext,
 		Attributes0, Result) :-
 	( convert_type_and_mode_list(As0, As) ->
@@ -2201,21 +2196,13 @@
 		"function result has mode, but function arguments don't",
 					FuncTerm)
 			;
-				As = [type_only(_) | _],
-				WithInst = yes(_)
-			->
-				Result = error(
-	"`with_inst` specified, but function arguments don't have modes",
-					FuncTerm)
-			;
 				get_purity(Attributes0, Purity, Attributes),
 				varset__coerce(VarSet0, TVarSet),
 				varset__coerce(VarSet0, IVarSet),
 				list__append(As, [ReturnType], Args),
 				Result0 = ok(pred_or_func(TVarSet, IVarSet,
-					ExistQVars, function, F, Args,
-					no, WithInst, MaybeDet, Cond,
-					Purity, ClassContext)),
+					ExistQVars, function, F, Args, no, no,
+					MaybeDet, Cond, Purity, ClassContext)),
 				check_no_attributes(Result0, Attributes,
 					Result)
 			)
@@ -2229,7 +2216,7 @@
 			"syntax error in arguments of `:- func' declaration",
 					FuncTerm)
 	).
-process_func_3(error(M, T), _, _, _, _, _, _, _, _, _, error(M, T)).
+process_func_3(error(M, T), _, _, _, _, _, _, _, _, error(M, T)).
 
 %-----------------------------------------------------------------------------%
 
diff -u doc/reference_manual.texi doc/reference_manual.texi
--- doc/reference_manual.texi
+++ doc/reference_manual.texi
@@ -1556,11 +1556,10 @@
 @end example
 
 A predicate or function can by declared to have a given higher-order
-type by using `with_type` in the type declaration.  This is useful
-where several predicates or functions need to have the same type
-signature, which often occurs for typeclass method implementations
-(@pxref{Type classes}, and for predicates to be passed as higher-order
-terms (@pxref{Higher-order}). 
+type (@pxref{Higher-order}) by using `with_type` in the type declaration.
+This is useful where several predicates or functions need to have the
+same type signature, which often occurs for typeclass method implementations
+(@pxref{Type classes}), and for predicates to be passed as higher-order terms.
 
 For example,
 
@@ -1569,7 +1568,7 @@
 :- type foldl_func(T, U) == (func(T, U) = U).
 
 :- pred p(int) `with_type` foldl_pred(T, U).
-:- pred f(int) `with_type` foldl_func(T, U).
+:- func f(int) `with_type` foldl_func(T, U).
 @end example
 
 @noindent
@@ -2048,19 +2047,9 @@
 :- mode length(out(listskel)) = in.
 @end example
 
-If a predicate or function has only one mode, the @samp{pred} and @samp{mode}
-declaration can be combined:
-
- at example
-:- func length(list(T)::in) = (int::out).
-:- pred append(list(T)::in, list(T)::in, list(T)::out).
-
-:- pred p `with_type` foldl_pred(T, U) `with_inst` foldl_pred.
- at end example
-
 As for type declarations, a predicate or function can be defined
-to have a given higher-order inst by using `with_inst` in the
-mode declaration.
+to have a given higher-order inst (@pxref{Higher-order modes} by using
+`with_inst` in the mode declaration.
 
 For example,
 
@@ -2078,6 +2067,19 @@
 @example
 :- mode p(in, in, in, out) is det.
 :- mode f(in, in, in) = out is det.
+ at end example
+
+ at noindent
+(@samp{is det} is explained in @ref{Determinism}.)
+
+If a predicate or function has only one mode, the @samp{pred} and @samp{mode}
+declaration can be combined:
+
+ at example
+:- func length(list(T)::in) = (int::out).
+:- pred append(list(T)::in, list(T)::in, list(T)::out).
+
+:- pred p `with_type` foldl_pred(T, U) `with_inst` foldl_pred.
 @end example
 
 If there is no mode declaration for a function, the compiler assumes
diff -u library/std_util.m library/std_util.m
--- library/std_util.m
+++ library/std_util.m
@@ -102,20 +102,31 @@
 	%
 :- func map_maybe(func(T) = U, maybe(T)) = maybe(U).
 
-	% map_maybe(P, yes(Value0), yes(Value), Acc0, Acc) :-
+	% fold_maybe(P, yes(Value), Acc0, Acc) :- P(Value, Acc0, Acc).
+	% fold_maybe(_, no, Acc, Acc).
+:- pred fold_maybe(pred(T, U, U), maybe(T), U, U).
+:- mode fold_maybe(pred(in, in, out) is det, in, in, out) is det.
+:- mode fold_maybe(pred(in, in, out) is semidet, in, in, out) is semidet.
+:- mode fold_maybe(pred(in, di, uo) is det, in, di, uo) is det.
+
+	% fold_maybe(F, yes(Value), Acc0) = F(Acc0).
+	% fold_maybe(_, no, Acc) = Acc.
+:- func fold_maybe(func(T, U) = U, maybe(T), U) = U.
+
+	% map_fold_maybe(P, yes(Value0), yes(Value), Acc0, Acc) :-
 	%       P(Value, Value, Acc0, Acc).
-	% map_maybe(_, no, no, Acc, Acc).
+	% map_fold_maybe(_, no, no, Acc, Acc).
 	%
-:- pred map_foldl_maybe(pred(T, U, Acc, Acc), maybe(T), maybe(U), Acc, Acc).
-:- mode map_foldl_maybe(pred(in, out, in, out) is det, in, out, in, out) is det.
-:- mode map_foldl_maybe(pred(in, out, di, uo) is det, in, out, di, uo) is det.
+:- pred map_fold_maybe(pred(T, U, Acc, Acc), maybe(T), maybe(U), Acc, Acc).
+:- mode map_fold_maybe(pred(in, out, in, out) is det, in, out, in, out) is det.
+:- mode map_fold_maybe(pred(in, out, di, uo) is det, in, out, di, uo) is det.
 
 	% As above, but with two accumulators.
-:- pred map_foldl2_maybe(pred(T, U, Acc1, Acc1, Acc2, Acc2),
+:- pred map_fold2_maybe(pred(T, U, Acc1, Acc1, Acc2, Acc2),
 		maybe(T), maybe(U), Acc1, Acc1, Acc2, Acc2).
-:- mode map_foldl2_maybe(pred(in, out, in, out, in, out) is det, in, out,
+:- mode map_fold2_maybe(pred(in, out, in, out, in, out) is det, in, out,
 		in, out, in, out) is det.
-:- mode map_foldl2_maybe(pred(in, out, in, out, di, uo) is det,
+:- mode map_fold2_maybe(pred(in, out, in, out, di, uo) is det,
 		in, out, in, out, di, uo) is det.
 
 %-----------------------------------------------------------------------------%
@@ -737,12 +748,18 @@
 map_maybe(_, no) = no.
 map_maybe(F, yes(T)) = yes(F(T)).
 
-map_foldl_maybe(_, no, no, Acc, Acc).
-map_foldl_maybe(P, yes(T0), yes(T), Acc0, Acc) :-
+fold_maybe(P, yes(Value), Acc0, Acc) :- P(Value, Acc0, Acc).
+fold_maybe(_, no, Acc, Acc).
+
+fold_maybe(F, yes(Value), Acc0) = F(Value, Acc0).
+fold_maybe(_, no, Acc) = Acc.
+
+map_fold_maybe(_, no, no, Acc, Acc).
+map_fold_maybe(P, yes(T0), yes(T), Acc0, Acc) :-
 	P(T0, T, Acc0, Acc).
 
-map_foldl2_maybe(_, no, no, A, A, B, B).
-map_foldl2_maybe(P, yes(T0), yes(T), A0, A, B0, B) :-
+map_fold2_maybe(_, no, no, A, A, B, B).
+map_fold2_maybe(P, yes(T0), yes(T), A0, A, B0, B) :-
 	P(T0, T, A0, A, B0, B).
 
 /****
only in patch2:
--- compiler/notes/compiler_design.html	13 Mar 2002 01:01:14 -0000	1.73
+++ compiler/notes/compiler_design.html	13 Mar 2002 16:25:23 -0000
@@ -254,6 +254,9 @@
 
 <li> expansion of equivalence types (equiv_type.m) <br>
 
+	`with_type` and `with_inst` annotations on predicate
+	and function type and mode declarations are also expanded.
+
 	This is really part of type-checking, but is done
 	on the item_list rather than on the HLDS because it
 	turned out to be much easier to implement that way.
only in patch2:
--- compiler/modules.m	12 Mar 2002 16:32:49 -0000	1.222
+++ compiler/modules.m	13 Mar 2002 15:21:10 -0000
@@ -4697,9 +4697,21 @@
 	%
 	(
 		list__member(Item, Items),
-		Item = pred_or_func(_, _, _, predicate,
-				Name, [_, _], _, _, _, _) - _,
-		unqualify_name(Name, "main")
+		Item = pred_or_func(_, _, _, predicate, Name,
+			[_, _], WithType, _, _, _, _, _) - _,
+		unqualify_name(Name, "main"),
+
+		% XXX We should allow `main/2' to be declared using
+		% `with_type`, but equivalences haven't been expanded
+		% at this point. The `has_main' field is only used for
+		% some special case handling of the module containing
+		% main for the IL backend (we generate a `.exe' file
+		% rather than a `.dll' file). This would arguably be
+		% better done by generating a `.dll' file as normal,
+		% and a separate `.exe' file containing initialization
+		% code and a call to `main/2', as we do with the `_init.c'
+		% file in the C backend.
+		WithType = no
 	->
 		HasMain = has_main
 	;
Index: tests/invalid/with_type.err_exp
===================================================================
RCS file: tests/invalid/with_type.err_exp
diff -N tests/invalid/with_type.err_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/with_type.err_exp	14 Mar 2002 16:00:05 -0000
@@ -0,0 +1,18 @@
+with_type.m:024: Error: `with_inst` and determinism both specified: with_type_4(_1 :: in, list(_2) :: in).
+with_type.m:027: Error: `with_inst` specified without `with_type`: with_type_5(_1 :: in, list(_2) :: in).
+with_type.m:030: Error: invalid inst in `with_inst`: with_inst(with_type(with_type_6(_1 :: in, list(_2) :: in), map_pred(string, string)), pred(in, in, out) is foo).
+with_type.m:032: Error: `with_inst` specified without argument modes: with_type_7(_1, list(_2)).
+with_type.m:012: In type declaration for predicate `with_type:with_type_1':
+with_type.m:012:   error: expected higher order predicate type after
+with_type.m:012:   `with_type`.
+with_type.m:013: In mode declaration for `with_type:with_type_1':
+with_type.m:013:   error: expected higher order inst after `with_inst`.
+with_type.m:018: In type declaration for function `with_type:with_type_2':
+with_type.m:018:   error: expected higher order function type after
+with_type.m:018:   `with_type`.
+with_type.m:021: In type declaration for predicate `with_type:with_type_3':
+with_type.m:021:   error: the `with_type` and `with_inst` annotations are
+with_type.m:021:   incompatible.
+with_type.m:019: Error: mode declaration for function `with_type:with_type_2/3'
+with_type.m:019:   without preceding `func' declaration.
+For more information, try recompiling with `-E'.
Index: tests/invalid/with_type.m
===================================================================
RCS file: tests/invalid/with_type.m
diff -N tests/invalid/with_type.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/with_type.m	14 Mar 2002 16:00:03 -0000
@@ -0,0 +1,33 @@
+:- module with_type.
+
+:- interface.
+
+:- import_module list.
+
+:- type map_pred(T, U) == pred(T, U).
+:- inst map_pred = (pred(in, out) is det).
+:- type foldl_pred(T, U) == pred(T, U, U).
+:- inst foldl_pred = (pred(in, in, out) is det).
+
+:- pred with_type_1(T, list(_)) `with_type` int.
+:- mode with_type_1(in, in) `with_inst` ground.
+
+:- type map_func(T, U) == (func(T) = U).
+:- inst map_func = (func(in) = out is det).
+
+:- func with_type_2(T, list(_)) `with_type` map_pred(string, string).
+:- mode with_type_2(in, in) `with_inst` map_func.
+
+:- pred with_type_3(T::in, list(_)::in) `with_type` map_pred(string, string)
+				`with_inst` foldl_pred.
+
+:- pred with_type_4(T::in, list(_)::in) `with_type` map_pred(string, string)
+				`with_inst` foldl_pred is det.
+
+:- pred with_type_5(T::in, list(_)::in) `with_inst` foldl_pred.
+
+:- pred with_type_6(T::in, list(_)::in) `with_type` map_pred(string, string)
+				`with_inst` (pred(in, in, out) is foo).
+
+:- pred with_type_7(T, list(_)) `with_type` map_pred(string, string)
+				`with_inst` foldl_pred.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------