[m-rev.] for review: adding promise ex declarations to the hlds with error checking

[Lars Yencken]

Hi,

This time properly boot checked ; )

===================================================================

Estimated hours taken: 150
Branches: main

Added initial error checking of promise ex declarations, and adding
the declarations into the HLDS as dummy predicates to leverage off
the error checking done for predicates (similarly to how assertions
were done). Following this, `promise_exclusive' and 
`promise_exclusive_exhaustive' declarations are added into a 
separate table in the HLDS.

assertion.m:
	Moved the pred declaration for assertion__normalise_goal
	into the interface.

goal_util.m:
	Added a predicate to get the predids of a goal or list of 
	goals.

hlds_data.m:
hlds_module.m:
	Added exclusive_table to HLDS, and operations on it.

hlds_out.m:
	Added printing of promise ex declaration error messages
	(also improves assertion error messages).

hlds_pred.m:
	Change to type `goal_type' to add constructor for general
	promise declarations (merged with assertions).

dead_proc_elim.m:
error_util.m:
intermod.m:
typecheck.m:
	Updated to handle promise declarations similarly to how
	assertions were handled.

make_hlds.m:
	Perform initial typechecking of promise ex declarations,
	then add them to the HLDS as dummy predicates.

purity.m:
post_typecheck.m:
	Post typechecking routine to add exclusivity declarations to 
	the exclusive_table.


Index: assertion.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/assertion.m,v
retrieving revision 1.14
diff -u -r1.14 assertion.m
--- assertion.m	20 Jul 2001 14:13:19 -0000	1.14
+++ assertion.m	14 Feb 2002 01:59:54 -0000
@@ -127,6 +127,14 @@
 		module_info::in, module_info::out,
 		io__state::di, io__state::uo) is det.
 
+	%
+	% assertion__normalise_goal
+	%
+	% Place a hlds_goal into a standard form.  Currently all the
+	% code does is replace conj([G]) with G.
+	%
+:- pred assertion__normalise_goal(hlds_goal::in, hlds_goal::out) is det.
+
 %-----------------------------------------------------------------------------%
 
 :- implementation.
@@ -650,14 +658,6 @@
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
-
-	%
-	% assertion__normalise_goal
-	%
-	% Place a hlds_goal into a standard form.  Currently all the
-	% code does is replace conj([G]) with G.
-	%
-:- pred assertion__normalise_goal(hlds_goal::in, hlds_goal::out) is det.
 
 assertion__normalise_goal(call(A,B,C,D,E,F) - GI, call(A,B,C,D,E,F) - GI).
 assertion__normalise_goal(generic_call(A,B,C,D) - GI, generic_call(A,B,C,D)-GI).
Index: dead_proc_elim.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/dead_proc_elim.m,v
retrieving revision 1.67
diff -u -r1.67 dead_proc_elim.m
--- dead_proc_elim.m	25 Jan 2002 08:22:47 -0000	1.67
+++ dead_proc_elim.m	14 Feb 2002 01:55:57 -0000
@@ -808,8 +808,8 @@
 			string__remove_suffix(PredName, "_init_any", _),
 			PredArity = 1
 		;
-			% Don't eliminate the clauses for assertions.
-			pred_info_get_goal_type(PredInfo, assertion)
+			% Don't eliminate the clauses for promises.
+			pred_info_get_goal_type(PredInfo, promise(_))
 		)
 	->
 		set__insert(NeededNames0, qualified(PredModule, PredName), 
Index: error_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/error_util.m,v
retrieving revision 1.15
diff -u -r1.15 error_util.m
--- error_util.m	30 Jul 2001 03:55:49 -0000	1.15
+++ error_util.m	14 Feb 2002 01:57:52 -0000
@@ -416,9 +416,9 @@
 		OrigArity is Arity - 1
 	),
 	(
-		pred_info_get_goal_type(PredInfo, assertion)
+		pred_info_get_goal_type(PredInfo, promise(PromiseType))
 	->
-		Piece = "promise"
+		Piece = promise_to_string(PromiseType)
 	;
 		string__int_to_string(OrigArity, ArityPart),
 		string__append_list([
Index: goal_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/goal_util.m,v
retrieving revision 1.71
diff -u -r1.71 goal_util.m
--- goal_util.m	26 Nov 2001 09:30:56 -0000	1.71
+++ goal_util.m	14 Feb 2002 01:26:01 -0000
@@ -149,6 +149,12 @@
 :- pred direct_subgoal(hlds_goal_expr, hlds_goal).
 :- mode direct_subgoal(in, out) is nondet.
 
+:- pred predids_from_goal(hlds_goal, list(pred_id)).
+:- mode predids_from_goal(in, out) is det.
+
+:- pred predids_from_goals(list(hlds_goal), list(pred_id)).
+:- mode predids_from_goals(in, out) is det.
+
 %-----------------------------------------------------------------------------%
 
 	% Convert a switch back into a disjunction. This is needed 
@@ -1283,5 +1289,24 @@
 		CallGoalInfo = CallGoalInfo1
 	),
 	CallGoal = Call - CallGoalInfo.
+
+%-----------------------------------------------------------------------------%
+
+predids_from_goals(Goals, PredIds) :- 
+	(
+		Goals = [],
+		PredIds = []
+	;
+		Goals = [Goal|Rest],
+		predids_from_goal(Goal, PredIds0),
+		predids_from_goals(Rest, PredIds1),
+		append(PredIds0, PredIds1, PredIds)
+	).
+
+predids_from_goal(Goal, PredIds) :-
+                % Explicit lambda expression needed since
+		% goal_calls_pred_id has multiple modes.
+	P = (pred(PredId::out) is nondet :- goal_calls_pred_id(Goal, PredId)),
+	solutions(P, PredIds).
 
 %-----------------------------------------------------------------------------%
Index: hlds_data.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_data.m,v
retrieving revision 1.63
diff -u -r1.63 hlds_data.m
--- hlds_data.m	16 Jan 2002 01:13:18 -0000	1.63
+++ hlds_data.m	14 Feb 2002 01:22:19 -0000
@@ -1038,3 +1038,70 @@
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
+
+:- interface.
+
+:- type exclusive_id	==	pred_id.
+:- type exclusive_ids	==	list(pred_id).
+
+	% 
+	% A table recording all promse_ex declarations (i.e. promise_exclusive,
+	% promise_exhaustive and promise_exclusive_exhaustive). 
+	%
+	% e.g. :- all [X]
+	% 		promise_exclusive
+	% 		some [Y] (
+	% 			p(X, Y)
+	% 		;
+	% 			q(X)
+	% 		).
+	% 
+	% promises that only one of p(X, Y) and q(X) can succeed at a time,
+	% although whichever one succeeds may have multiple solutions.
+	
+:- type exclusive_table.
+
+:- pred exclusive_table_init(exclusive_table).
+:- mode exclusive_table_init(out) is det.
+
+:- pred exclusive_table_search(exclusive_table, pred_id, exclusive_ids).
+:- mode exclusive_table_search(in, in, out) is semidet.
+
+:- pred exclusive_table_lookup(exclusive_table, pred_id, exclusive_ids).
+:- mode exclusive_table_lookup(in, in, out) is det.
+
+:- pred exclusive_table_optimize(exclusive_table, exclusive_table).
+:- mode exclusive_table_optimize(in, out) is det.
+
+:- pred exclusive_table_add(pred_id, exclusive_id, exclusive_table,
+		exclusive_table).
+:- mode exclusive_table_add(in, in, in, out) is det.
+
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- type exclusive_table		==	map(pred_id, exclusive_ids).
+
+exclusive_table_init(map__init).
+
+exclusive_table_lookup(ExclusiveTable, PredId, ExclusiveIds) :-
+	map__lookup(ExclusiveTable, PredId, ExclusiveIds).
+
+exclusive_table_search(ExclusiveTable, Id, ExclusiveIds) :-
+	map__search(ExclusiveTable, Id, ExclusiveIds).
+
+exclusive_table_optimize(ExclusiveTable0, ExclusiveTable) :-
+	map__optimize(ExclusiveTable0, ExclusiveTable).
+
+exclusive_table_add(ExclusiveId, PredId, ExclusiveTable0, ExclusiveTable) :-
+	(
+		map__search(ExclusiveTable0, PredId, ExclusiveIds)
+	->
+		map__det_update(ExclusiveTable0, PredId, 
+				[ExclusiveId|ExclusiveIds], ExclusiveTable)
+	;
+		map__det_insert(ExclusiveTable0, PredId, [ExclusiveId], 
+				ExclusiveTable)
+	).
+
Index: hlds_module.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_module.m,v
retrieving revision 1.70
diff -u -r1.70 hlds_module.m
--- hlds_module.m	25 Jan 2002 08:22:48 -0000	1.70
+++ hlds_module.m	14 Feb 2002 01:24:10 -0000
@@ -195,6 +195,13 @@
 	module_info).
 :- mode module_info_set_assertion_table(in, in, out) is det.
 
+:- pred module_info_exclusive_table(module_info, exclusive_table).
+:- mode module_info_exclusive_table(in, out) is det.
+
+:- pred module_info_set_exclusive_table(module_info, exclusive_table, 
+	module_info).
+:- mode module_info_set_exclusive_table(in, in, out) is det.
+
 :- pred module_info_ctor_field_table(module_info, ctor_field_table).
 :- mode module_info_ctor_field_table(in, out) is det.
 
@@ -503,6 +510,7 @@
 		instance_table ::		instance_table,
 		superclass_table ::		superclass_table,
 		assertion_table ::		assertion_table,
+		exclusive_table ::		exclusive_table,
 		ctor_field_table ::		ctor_field_table,
 		cell_counter ::			counter,
 					% cell count, passed into code_info
@@ -595,6 +603,7 @@
 	set__init(IndirectlyImportedModules),
 
 	assertion_table_init(AssertionTable),
+	exclusive_table_init(ExclusiveTable),
 	map__init(FieldNameTable),
 
 	map__init(NoTagTypes),
@@ -605,7 +614,7 @@
 	ModuleInfo = module(ModuleSubInfo, PredicateTable, Requests,
 		UnifyPredMap, QualifierInfo, Types, Insts, Modes, Ctors,
 		ClassTable, SuperClassTable, InstanceTable, AssertionTable,
-		FieldNameTable, counter__init(1), RecompInfo).
+		ExclusiveTable, FieldNameTable, counter__init(1), RecompInfo).
 
 %-----------------------------------------------------------------------------%
 
@@ -623,6 +632,7 @@
 module_info_instances(MI, MI ^ instance_table).
 module_info_superclasses(MI, MI ^ superclass_table).
 module_info_assertion_table(MI, MI ^ assertion_table).
+module_info_exclusive_table(MI, MI ^ exclusive_table).
 module_info_ctor_field_table(MI, MI ^ ctor_field_table).
 module_info_get_cell_counter(MI, MI ^ cell_counter).
 module_info_get_maybe_recompilation_info(MI, MI ^ maybe_recompilation_info).
@@ -644,6 +654,7 @@
 module_info_set_instances(MI, I, MI ^ instance_table := I).
 module_info_set_superclasses(MI, S, MI ^ superclass_table := S).
 module_info_set_assertion_table(MI, A, MI ^ assertion_table := A).
+module_info_set_exclusive_table(MI, PXT, MI ^ exclusive_table := PXT).
 module_info_set_ctor_field_table(MI, CF, MI ^ ctor_field_table := CF).
 module_info_set_cell_counter(MI, CC, MI ^ cell_counter := CC).
 module_info_set_maybe_recompilation_info(MI, I,
Index: hlds_out.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_out.m,v
retrieving revision 1.272
diff -u -r1.272 hlds_out.m
--- hlds_out.m	16 Jan 2002 01:13:19 -0000	1.272
+++ hlds_out.m	15 Feb 2002 00:11:13 -0000
@@ -164,10 +164,10 @@
 :- mode hlds_out__write_clause(in, in, in, in, in, in, in, in, in, in, di, uo)
 	is det.
 
-:- pred hlds_out__write_assertion(int, module_info, pred_id, prog_varset, bool,
-		list(prog_var), pred_or_func, clause, maybe_vartypes,
-		io__state, io__state).
-:- mode hlds_out__write_assertion(in, in, in, in, in, in, in, in, in, di, uo)
+:- pred hlds_out__write_promise(promise_type, int, module_info, pred_id,
+		prog_varset, bool, list(prog_var), pred_or_func, clause,
+		maybe_vartypes, io__state, io__state).
+:- mode hlds_out__write_promise(in, in, in, in, in, in, in, in, in, in, di, uo)
 	is det.
 
 	% Print out an HLDS goal. The module_info and prog_varset give
@@ -368,9 +368,9 @@
 	->
 		io__write_string("type class method implementation")
 	;
-		{ pred_info_get_goal_type(PredInfo, assertion) }
+		{ pred_info_get_goal_type(PredInfo, promise(PromiseType)) }
 	->
-		io__write_string("promise")
+		io__write_string(prog_out__promise_to_string(PromiseType))
 	;
 		hlds_out__write_simple_call_id(PredOrFunc,
 			qualified(Module, Name), Arity)
@@ -389,12 +389,42 @@
 	hlds_out__write_simple_call_id(PredOrFunc, Name, Arity).
 
 hlds_out__write_simple_call_id(PredOrFunc, Name, Arity) -->
-	hlds_out__write_pred_or_func(PredOrFunc),
-	io__write_string(" `"),
-	{ hlds_out__simple_call_id_to_sym_name_and_arity(
-		PredOrFunc - Name/Arity, SymArity) },
-	prog_out__write_sym_name_and_arity(SymArity),
-	io__write_string("'").
+		% XXX when printed, promises are differentiated from 
+		%     predicates or functions by module name, so the module 
+		%     names `promise', `promise_exclusive', etc. should be 
+		%     reserved, and their dummy predicates should have more
+		%     unusual module names
+	(
+		{ Name = unqualified(StrName) }
+	;
+		{ Name = qualified(_, StrName) }
+	),
+		% is it really a promise?
+	( { string__prefix(StrName, "promise__") } ->
+		{ Promise = promise(true) }
+	; { string__prefix(StrName, "promise_exclusive__") } ->
+		{ Promise = promise(exclusive) }
+	; { string__prefix(StrName, "promise_exhaustive__") } ->
+		{ Promise = promise(exhaustive) }
+	; { string__prefix(StrName, "promise_exclusive_exhaustive__") } ->
+		{ Promise = promise(exclusive_exhaustive) }
+	;
+		{ Promise = none }	% no, it is really a pred or func
+	),
+
+	(
+		{ Promise = promise(PromiseType) }
+	->
+		prog_out__write_promise_type(PromiseType),
+		io__write_string(" declaration")
+	;
+		hlds_out__write_pred_or_func(PredOrFunc),
+		io__write_string(" `"),
+		{ hlds_out__simple_call_id_to_sym_name_and_arity(
+			PredOrFunc - Name/Arity, SymArity) },
+		prog_out__write_sym_name_and_arity(SymArity),
+		io__write_string("'")
+	).
 
 :- pred hlds_out__simple_call_id_to_sym_name_and_arity(simple_call_id,
 		sym_name_and_arity).
@@ -913,8 +943,8 @@
 	{ hlds_out__marker_name(Marker, Name) },
 	io__write_string(Name).
 
-hlds_out__write_assertion(Indent, ModuleInfo, _PredId, VarSet, AppendVarnums,
-		HeadVars, _PredOrFunc, Clause, TypeQual) -->
+hlds_out__write_promise(PromiseType, Indent, ModuleInfo, _PredId, VarSet, 
+		AppendVarnums, HeadVars, _PredOrFunc, Clause, TypeQual) -->
 
 		% curry the varset for term_io__write_variable/4
 	{ PrintVar = lambda([VarName::in, IO0::di, IO::uo] is det,
@@ -922,14 +952,24 @@
 		) },
 
 	hlds_out__write_indent(Indent),
-	io__write_string(":- promise all["),
-	io__write_list(HeadVars, ", ", PrintVar),
-	io__write_string("] (\n"),
 
+		% print initial formatting differently for assertions
+	( { PromiseType = true } ->
+		io__write_string(":- promise all["),
+		io__write_list(HeadVars, ", ", PrintVar),
+		io__write_string("] (\n")
+	;
+		io__write_string(":- all["),
+		io__write_list(HeadVars, ", ", PrintVar),
+		io__write_string("]"),
+		mercury_output_newline(Indent),
+		prog_out__write_promise_type(PromiseType),
+		io__nl
+	),
+	
 	{ Clause = clause(_Modes, Goal, _Lang, _Context) },
 	hlds_out__write_goal_a(Goal, ModuleInfo, VarSet, AppendVarnums,
 			Indent+1, ").\n", TypeQual).
-
 
 
 hlds_out__write_clauses(Indent, ModuleInfo, PredId, VarSet, AppendVarnums,
Index: hlds_pred.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_pred.m,v
retrieving revision 1.101
diff -u -r1.101 hlds_pred.m
--- hlds_pred.m	24 Aug 2001 15:44:47 -0000	1.101
+++ hlds_pred.m	13 Feb 2002 05:11:52 -0000
@@ -239,7 +239,7 @@
 			;	clauses		
 			;	clauses_and_pragmas 
 						% both clauses and pragmas
-			;	(assertion)
+			;	promise(promise_type)
 			;	none.
 
 	% Note: `liveness' and `liveness_info' record liveness in the sense
Index: intermod.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/intermod.m,v
retrieving revision 1.111
diff -u -r1.111 intermod.m
--- intermod.m	16 Jan 2002 01:13:22 -0000	1.111
+++ intermod.m	14 Feb 2002 02:28:07 -0000
@@ -366,9 +366,9 @@
 			clause_list_is_deforestable(PredId, Clauses)
 		)
 	;
-		% assertions that are in the interface should always get
+		% promises that are in the interface should always get
 		% included in the .opt file.
-		pred_info_get_goal_type(PredInfo, assertion)
+		pred_info_get_goal_type(PredInfo, promise(_))
 	).
 
 :- pred intermod__traverse_clauses(list(clause)::in, list(clause)::out,
@@ -1371,7 +1371,7 @@
 		GoalType = clauses,
 		AppendVarNums = yes
 	;
-		GoalType = (assertion),
+		GoalType = promise(_),
 		AppendVarNums = yes
 	;
 		GoalType = none,
@@ -1458,14 +1458,14 @@
 	{ clauses_info_clauses(ClausesInfo, Clauses) },
 
 	(
-		{ pred_info_get_goal_type(PredInfo, assertion) }
+		{ pred_info_get_goal_type(PredInfo, promise(PromiseType)) }
 	->
 		(
 			{ Clauses = [Clause] }
 		->
-			hlds_out__write_assertion(0, ModuleInfo, PredId,
-					VarSet, no, HeadVars, PredOrFunc,
-					Clause, no)
+			hlds_out__write_promise(PromiseType, 0, ModuleInfo, 
+					PredId, VarSet, no, HeadVars, 
+					PredOrFunc, Clause, no)
 		;
 			{ error("intermod__write_preds: assertion not a single clause.") }
 		)
Index: make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.399
diff -u -r1.399 make_hlds.m
--- make_hlds.m	8 Feb 2002 02:26:45 -0000	1.399
+++ make_hlds.m	15 Feb 2002 03:51:23 -0000
@@ -692,9 +692,10 @@
 add_item_clause(clause(VarSet, PredOrFunc, PredName, Args, Body),
 		Status, Status, Context, Module0, Module, Info0, Info) -->
 	check_not_exported(Status, Context, "clause"),
-	{ IsAssertion = no },
+	{ GoalType = none }, 	% at this stage we only need know that it's not
+				% a promise declaration
 	module_add_clause(Module0, VarSet, PredOrFunc, PredName,
-		Args, Body, Status, Context, IsAssertion, Module, Info0, Info).
+		Args, Body, Status, Context, GoalType, Module, Info0, Info).
 add_item_clause(type_defn(_, _, _, _, _), Status, Status, _,
 				Module, Module, Info, Info) --> [].
 add_item_clause(inst_defn(_, _, _, _, _), Status, Status, _,
@@ -801,8 +802,6 @@
 	
 add_item_clause(promise(PromiseType, Goal, VarSet, UnivVars),
 		Status, Status, Context, Module0, Module, Info0, Info) -->
-	( { PromiseType = true } ->	% promise is an assertion
-
 		%
 		% If the outermost existentially quantified variables
 		% are placed in the head of the assertion, the
@@ -810,34 +809,43 @@
 		% type variables as this implicity adds a universal
 		% quantification of the typevariables needed.
 		%
-		{ term__var_list_to_term_list(UnivVars, HeadVars) },
+	{ term__var_list_to_term_list(UnivVars, HeadVars) },
+	( { \+ PromiseType = true } ->
+		check_promise_ex_decl(UnivVars, PromiseType, Goal, Context)
+	;
+		[]
+	),
+	add_promise_clause(PromiseType, HeadVars, VarSet, Goal, Context, Status,
+			Module0, Module, Info0, Info).
+
+:- pred add_promise_clause(promise_type, list(term(prog_var_type)), prog_varset,
+		goal, prog_context, import_status, module_info, module_info, 
+		qual_info, qual_info, io__state, io__state). 
+:- mode add_promise_clause(in, in, in, in, in, in, in, out, in, out, 
+		di, uo) is det.
+add_promise_clause(PromiseType, HeadVars, VarSet, Goal, Context, Status,
+		Module0, Module, Info0, Info) -->
 	{ term__context_line(Context, Line) },
 	{ term__context_file(Context, File) },
-		{ string__format("assertion__%d__%s", [i(Line), s(File)],Name)},
-
+	{ string__format(prog_out__promise_to_string(PromiseType) ++
+			"__%d__%s", [i(Line), s(File)], Name) },
 		%
-		% The assertions are recorded as a predicate whose
-		% goal_type is set to assertion.  This allows us to
-		% leverage off all the other checks in the compiler that
-		% operate on predicates.
+		% Promise declarations are recorded as a predicate with a
+		% goal_type of promise(X), where X is of promise_type. This 
+		% allows us to leverage off all the other checks in the 
+		% compiler that operate on predicates.
 		%
 		% :- promise all [A,B,R] ( R = A + B <=> R = B + A ).
 		%
 		% becomes
 		%
-		% assertion__lineno_filename(A, B, R) :-
+		% promise__lineno_filename(A, B, R) :-
 		% 	( R = A + B <=> R = B + A ).
 		%
-	{ IsAssertion = yes },
+	{ GoalType = promise(PromiseType) },
 	module_add_clause(Module0, VarSet, predicate, unqualified(Name),
-				HeadVars, Goal, Status, Context, IsAssertion, 
-				Module, Info0, Info)
-	;
-			% promise is a promise ex declaration,
-			% not yet implemented
-		{ Module0 = Module },
-		{ Info0 = Info }
-	).
+			HeadVars, Goal, Status, Context, GoalType, 
+			Module, Info0, Info).
 
 add_item_clause(nothing(_), Status, Status, _,
 	Module, Module, Info, Info) --> [].
@@ -3583,13 +3591,13 @@
 %-----------------------------------------------------------------------------%
 
 :- pred module_add_clause(module_info, prog_varset, pred_or_func, sym_name,
-		list(prog_term), goal, import_status, prog_context, bool,
+		list(prog_term), goal, import_status, prog_context, goal_type,
 		module_info, qual_info, qual_info, io__state, io__state).
 :- mode module_add_clause(in, in, in, in, in, in, in, in, in,
 		out, in, out, di, uo) is det.
 
 module_add_clause(ModuleInfo0, ClauseVarSet, PredOrFunc, PredName, Args, Body,
-			Status, Context, IsAssertion, ModuleInfo,
+			Status, Context, GoalType, ModuleInfo,
 			Info0, Info) -->
 	globals__io_lookup_bool_option(very_verbose, VeryVerbose),
 	( { VeryVerbose = yes } ->
@@ -3617,7 +3625,7 @@
 		{ PredId = PredId0 },
 		{ ModuleInfo1 = ModuleInfo0 },
 		(
-			{ IsAssertion = yes }
+			{ GoalType = promise(_) }
 		->
 			{ prog_out__sym_name_to_string(PredName, NameString) },
 			{ string__format("%s %s %s (%s).\n",
@@ -3630,10 +3638,11 @@
 			[]
 		)
 	;
-		(
-				% An assertion will not have a
+				% A promise will not have a
 				% corresponding pred declaration.
-			{ IsAssertion = yes },
+		(
+			{ GoalType = promise(_) }
+		->
 			{ term__term_list_to_var_list(Args, HeadVars) },
 			{ preds_add_implicit_for_assertion(HeadVars,
 					ModuleInfo0, PredicateTable0,
@@ -3643,8 +3652,6 @@
 			{ module_info_set_predicate_table(ModuleInfo0,
 					PredicateTable1, ModuleInfo1) }
 		;
-			{ IsAssertion = no },
-
 			preds_add_implicit_report_error(ModuleName,
 				PredOrFunc, PredName, Arity, Status, no,
 				Context, "clause", PredId,
@@ -3745,15 +3752,16 @@
 			ArgTerms, ProcIdsForThisClause, ModuleInfo2, Info1),
 		clauses_info_add_clause(Clauses0, ProcIdsForThisClause,
 			ClauseVarSet, TVarSet0, ArgTerms, Body, Context,
-			Status, PredOrFunc, Arity, IsAssertion, Goal,
+			Status, PredOrFunc, Arity, GoalType, Goal,
 			VarSet, TVarSet, Clauses, Warnings,
 			ModuleInfo2, ModuleInfo3, Info1, Info),
 		{
 		pred_info_set_clauses_info(PredInfo2, Clauses, PredInfo3),
 		(
-			IsAssertion = yes
+			GoalType = promise(PromiseType)
 		->
-			pred_info_set_goal_type(PredInfo3, assertion, PredInfo4)
+			pred_info_set_goal_type(PredInfo3, promise(PromiseType),
+					PredInfo4)
 		;
 			pred_info_set_goal_type(PredInfo3, clauses, PredInfo4)
 		),
@@ -4004,10 +4012,10 @@
 
 		{ ProcIds = [] }, % means this clause applies to _every_
 				  % mode of the procedure
-		{ IsAssertion = no },
+		{ GoalType = none },	% goal is not a promise
 		clauses_info_add_clause(ClausesInfo0, ProcIds,
 			CVarSet, TVarSet0, HeadTerms, Body, Context, Status,
-			PredOrFunc, Arity, IsAssertion, Goal,
+			PredOrFunc, Arity, GoalType, Goal,
 			VarSet, _TVarSet, ClausesInfo, Warnings,
 			ModuleInfo0, ModuleInfo, QualInfo0, QualInfo),
 
@@ -5273,14 +5281,14 @@
 :- pred clauses_info_add_clause(clauses_info::in,
 		list(proc_id)::in, prog_varset::in, tvarset::in,
 		list(prog_term)::in, goal::in, prog_context::in,
-		import_status::in, pred_or_func::in, arity::in, bool::in,
+		import_status::in, pred_or_func::in, arity::in, goal_type::in,
 		hlds_goal::out, prog_varset::out, tvarset::out,
 		clauses_info::out, list(quant_warning)::out, 
 		module_info::in, module_info::out, qual_info::in,
 		qual_info::out, io__state::di, io__state::uo) is det.
 
 clauses_info_add_clause(ClausesInfo0, ModeIds0, CVarSet, TVarSet0,
-		Args, Body, Context, Status, PredOrFunc, Arity, IsAssertion,
+		Args, Body, Context, Status, PredOrFunc, Arity, GoalType,
 		Goal, VarSet, TVarSet, ClausesInfo, Warnings, Module0, Module,
 		Info0, Info) -->
 	{ ClausesInfo0 = clauses_info(VarSet0, ExplicitVarTypes0, TVarNameMap0,
@@ -5302,7 +5310,7 @@
 			ExplicitVarTypes0, Status, Info1) },
 	{ varset__merge_subst(VarSet0, CVarSet, VarSet1, Subst) },
 	transform(Subst, HeadVars, Args, Body, VarSet1, Context, PredOrFunc,
-			Arity, IsAssertion, Goal0, VarSet, Warnings,
+			Arity, GoalType, Goal0, VarSet, Warnings,
 			transform_info(Module0, Info1),
 			transform_info(Module, Info2)),
 	{ TVarSet = Info2 ^ tvarset },
@@ -5580,7 +5588,7 @@
 	).
 
 :- pred transform(prog_substitution, list(prog_var), list(prog_term), goal,
-		prog_varset, prog_context, pred_or_func, arity, bool,
+		prog_varset, prog_context, pred_or_func, arity, goal_type,
 		hlds_goal, prog_varset, list(quant_warning),
 		transform_info, transform_info,
 		io__state, io__state).
@@ -5588,14 +5596,14 @@
 		in, out, di, uo) is det.
 
 transform(Subst, HeadVars, Args0, Body, VarSet0, Context, PredOrFunc,
-		Arity, IsAssertion, Goal, VarSet, Warnings, Info0, Info) -->
+		Arity, GoalType, Goal, VarSet, Warnings, Info0, Info) -->
 	transform_goal(Body, VarSet0, Subst, Goal1, VarSet1, Info0, Info1),
 	{ term__apply_substitution_to_list(Args0, Subst, Args) },
 		
 		% The head variables of an assertion will always be
 		% variables, so it is unnecessary to insert unifications.
 	(
-		{ IsAssertion = yes }
+		{ GoalType = promise(_) }
 	->
 		{ VarSet2 = VarSet1 },
 		{ Goal2 = Goal1 },
@@ -8413,4 +8421,144 @@
 		PragmaVars0 = []
 	).
 
+
 %-----------------------------------------------------------------------------%
+%
+% XXX promise_ex declarations
+%
+%
+
+:- type promise_ex_goal
+	--->	ok(goals)
+	;	error(string, prog_context).
+
+	% Perform error checking for a promise ex declaration.
+	% The following checks are done:
+	% 	* check for universally quantified variables
+	% 	* check if universal quantification is placed in the wrong
+	% 	  position (i.e. after the `promise_exclusive' rather than 
+	% 	  before it)
+	% 	* check that each arm of the disjunction has at most one call,
+	% 	  but otherwise has only unifications
+:- pred check_promise_ex_decl(prog_vars, promise_type, goal, prog_context, 
+		io__state, io__state).
+:- mode check_promise_ex_decl(in, in, in, in, di, uo) is det.
+check_promise_ex_decl(UnivVars, PromiseType, Goal, Context) -->
+		% are universally quantified variables present?
+	(
+		{ UnivVars = [] },
+		promise_ex_error(PromiseType, Context, "declaration has no universally quantified variables")
+	;
+		{ UnivVars = [_|_] }
+	),
+	check_promise_ex_goal(PromiseType, Goal).
+
+
+	% strip off any existential quantification, then 
+:- pred check_promise_ex_goal(promise_type, goal, io__state, io__state).
+:- mode check_promise_ex_goal(in, in, di, uo) is det.
+check_promise_ex_goal(PromiseType, GoalExpr - Context) -->
+	( { GoalExpr = some(_, Goal) } ->
+		check_promise_ex_goal(PromiseType, Goal)
+	; { GoalExpr =  ( _ ; _ ) } ->
+		{ flatten_to_disj_list(GoalExpr - Context, DisjList) },
+		{ list__map(flatten_to_cons_list, DisjList, DisjConsList) },
+		check_list_cons_list(PromiseType, DisjConsList)
+	; { GoalExpr = all(_UnivVars, Goal) } ->
+		promise_ex_error(PromiseType, Context, "universal quantification should come before the declaration name"),
+		check_promise_ex_goal(PromiseType, Goal)
+	;
+		promise_ex_error(PromiseType, Context, "goal in declaration is not a disjunction")
+	).
+
+
+:- pred flatten_to_disj_list(goal, goals).
+:- mode flatten_to_disj_list(in, out) is det.
+flatten_to_disj_list(GoalExpr - Context, GoalList) :-
+	( GoalExpr = ( GoalA ; GoalB ) ->
+		flatten_to_disj_list(GoalA, GoalListA),
+		flatten_to_disj_list(GoalB, GoalListB),
+		append(GoalListA, GoalListB, GoalList)
+	;
+		GoalList = [GoalExpr - Context]
+	).
+
+:- pred flatten_to_cons_list(goal, goals).
+:- mode flatten_to_cons_list(in, out) is det.
+flatten_to_cons_list(GoalExpr - Context, GoalList) :-
+	( GoalExpr = ( GoalA , GoalB ) ->
+		flatten_to_cons_list(GoalA, GoalListA),
+		flatten_to_cons_list(GoalB, GoalListB),
+		append(GoalListA, GoalListB, GoalList)
+	;
+		GoalList = [GoalExpr - Context]
+	).
+
+:- pred check_list_cons_list(promise_type, list(goals), io__state, io__state).
+:- mode check_list_cons_list(in, in, di, uo) is det.
+check_list_cons_list(PromiseType, DisjConsList) -->
+	(
+		{ DisjConsList = [] }
+	;
+		{ DisjConsList = [ConsList|Rest] },
+		check_cons_list(PromiseType, ConsList, no),
+		check_list_cons_list(PromiseType, Rest)
+	).
+
+:- pred check_disj_goals(promise_type, list(goals), io__state, io__state).
+:- mode check_disj_goals(in, in, di, uo) is det.
+check_disj_goals(PromiseType, GoalList0) -->
+	(
+		{ GoalList0 = [] }
+	;
+		{ GoalList0 = [Goal0|GoalList] },
+		check_cons_list(PromiseType, Goal0, no),
+		check_disj_goals(PromiseType, GoalList)
+	).
+
+
+	% check a cons list of goals in a disj, ensuring that they are all
+	% either unifications or calls
+	% only one call is allowed per cons list, as each cons list represents 
+	% one arm of the disjunction
+:- pred check_cons_list(promise_type, goals, bool, io__state, io__state).
+:- mode check_cons_list(in, in, in, di, uo) is det.
+check_cons_list(PromiseType, Goals, CallUsed) -->
+	(
+		{ Goals = [] }
+	;
+		{ Goals = [GoalExpr - Context|Rest] },
+		( { GoalExpr = unify(_, _, _) } ->
+			check_cons_list(PromiseType, Rest, CallUsed)
+		; { GoalExpr = some(_, Goal) } ->
+			check_cons_list(PromiseType, [Goal|Rest], CallUsed)
+		; { GoalExpr = call(_, _, _) } ->
+			(
+				{ CallUsed = no }
+			;
+				{ CallUsed = yes },
+				promise_ex_error(PromiseType, Context, "disjunct contains more than one call")
+			),
+			check_cons_list(PromiseType, Rest, yes)
+		;
+			promise_ex_error(PromiseType, Context, "disjunct is not a call or unification"),
+			check_cons_list(PromiseType, Rest, CallUsed)
+		)
+	).
+
+
+	% called for any promise_ex_error
+:- pred promise_ex_error(promise_type, prog_context, string, 
+		io__state, io__state).
+:- mode promise_ex_error(in, in, in, di, uo) is det.
+promise_ex_error(PromiseType, Context, Message) -->
+	io__set_exit_status(1),
+	prog_out__write_context(Context),
+	io__write_string("In " ++ 
+		prog_out__promise_to_string(PromiseType) ++ " declaration:\n"),
+	prog_out__write_context(Context),
+	io__write_string("  error: "),
+	io__write_string(Message),
+	io__nl.
+
+%------------------------------------------------------------------------------%
Index: post_typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/post_typecheck.m,v
retrieving revision 1.34
diff -u -r1.34 post_typecheck.m
--- post_typecheck.m	2 Oct 2001 13:53:56 -0000	1.34
+++ post_typecheck.m	14 Feb 2002 05:26:07 -0000
@@ -124,9 +124,9 @@
 	% Now that the assertion has finished being typechecked,
 	% remove it from further processing and store it in the
 	% assertion_table.
-:- pred post_typecheck__finish_assertion(module_info, pred_id,
+:- pred post_typecheck__finish_promise(promise_type, module_info, pred_id,
 		module_info, io__state, io__state) is det.
-:- mode post_typecheck__finish_assertion(in, in, out, di, uo) is det.
+:- mode post_typecheck__finish_promise(in, in, in, out, di, uo) is det.
 
 %-----------------------------------------------------------------------------%
 
@@ -134,7 +134,7 @@
 
 :- import_module (assertion), code_util, typecheck, clause_to_proc.
 :- import_module mode_util, inst_match, (inst), prog_util, error_util.
-:- import_module mercury_to_mercury, prog_out, hlds_out, type_util.
+:- import_module mercury_to_mercury, prog_out, hlds_out, type_util, goal_util.
 :- import_module globals, options.
 
 :- import_module map, set, assoc_list, term, require, int.
@@ -691,42 +691,94 @@
 		Errors, PredInfo1, PredInfo).
 
 	%
-	% Now that the assertion has finished being typechecked,
+	% Now that the promise has finished being typechecked,
 	% and has had all of its pred_ids identified,
-	% remove the assertion from the list of pred ids to be processed
+	% remove the promise from the list of pred ids to be processed
 	% in the future and place the pred_id associated with the
-	% assertion into the assertion table.
+	% promise into the assertion or promise_ex table.
 	% For each assertion that is in the interface, you need to check
 	% that it doesn't refer to any symbols which are local to that
 	% module.
 	% Also record for each predicate that is used in an assertion
-	% which assertion it is used in.
-	% 
-post_typecheck__finish_assertion(Module0, PredId, Module) -->
-		% store into assertion table.
-	{ module_info_assertion_table(Module0, AssertTable0) },
-	{ assertion_table_add_assertion(PredId,
-			AssertTable0, AssertionId, AssertTable) },
-	{ module_info_set_assertion_table(Module0, AssertTable, Module1) },
-		
+	% which assertion it is used in, or for a promise ex declaration
+	% record in the promise ex table the predicates used by the
+	% declaration.
+	%
+post_typecheck__finish_promise(PromiseType, Module0, PromiseId, Module) -->
+		% Store the declaration in the appropriate table and get
+		% the goal for the promise
+	{ store_promise(PromiseType, Module0, PromiseId, Module1, Goal) },
+			
 		% Remove from further processing.
-	{ module_info_remove_predid(Module1, PredId, Module2) },
+	{ module_info_remove_predid(Module1, PromiseId, Module2) },
 
-		% If the assertion is in the interface, then ensure that
+		% If the promise is in the interface, then ensure that
 		% it doesn't refer to any local symbols.
-	{ module_info_pred_info(Module2, PredId, PredInfo) },
-	{ assertion__goal(AssertionId, Module2, Goal) },
+	{ module_info_pred_info(Module2, PromiseId, PredInfo) },
+	( { pred_info_is_exported(PredInfo) } ->
+		assertion__in_interface_check(Goal, PredInfo, 
+				Module2, Module)
+	;
+		{ Module2 = Module }
+	).
+
+	% store promise declaration, normalise goal and return new
+	% module_info and the goal for further processing
+:- pred store_promise(promise_type, module_info, pred_id, module_info, 
+		hlds_goal).
+:- mode store_promise(in, in, in, out, out) is det.
+store_promise(PromiseType, Module0, PromiseId, Module, Goal) :-
 	(
-		{ pred_info_is_exported(PredInfo) }
+			% case for assertions
+		PromiseType = true,
+		module_info_assertion_table(Module0, AssertTable0),
+		assertion_table_add_assertion(PromiseId, AssertTable0, 
+				AssertionId, AssertTable),
+		module_info_set_assertion_table(Module0, AssertTable, 
+				Module1),
+		assertion__goal(AssertionId, Module1, Goal),
+		assertion__record_preds_used_in(Goal, AssertionId, Module1,
+				Module)
+	;
+			% case for exclusivity
+		PromiseType = exclusive,
+		promise_ex_goal(PromiseId, Module0, Goal),
+		predids_from_goal(Goal, PredIds),
+		module_info_exclusive_table(Module0, Table0),
+		list__foldl(exclusive_table_add(PromiseId), PredIds, Table0,
+				Table),
+		module_info_set_exclusive_table(Module0, Table, Module)
+	;
+			% case for exclusivity
+		PromiseType = exclusive_exhaustive,
+		promise_ex_goal(PromiseId, Module0, Goal),
+		predids_from_goal(Goal, PredIds),
+		module_info_exclusive_table(Module0, Table0),
+		list__foldl(exclusive_table_add(PromiseId), PredIds, Table0,
+				Table),
+		module_info_set_exclusive_table(Module0, Table, Module)
+	;
+			% case for exhaustiveness -- not yet implemented
+		PromiseType = exhaustive,
+		promise_ex_goal(PromiseId, Module0, Goal),
+		Module0 = Module
+	).
+
+:- pred promise_ex_goal(pred_id, module_info, hlds_goal).
+:- mode promise_ex_goal(in, in, out) is det.
+promise_ex_goal(ExclusiveDecl, Module, Goal) :-
+        module_info_pred_info(Module, ExclusiveDecl, PredInfo),
+        pred_info_clauses_info(PredInfo, ClausesInfo),
+        clauses_info_clauses(ClausesInfo, Clauses),
+        (
+		Clauses = [clause(_ProcIds, Goal0, _Lang, _Context)]
 	->
-		assertion__in_interface_check(Goal, PredInfo, Module2, Module3)
+		assertion__normalise_goal(Goal0, Goal)
 	;
-		{ Module3 = Module2 }
-	),
+		error("promise_ex__goal: not an promise")
+	).
+
 
-		% record which predicates are used in assertions
-	{ assertion__record_preds_used_in(Goal, AssertionId, Module3, Module) }.
-	
 %-----------------------------------------------------------------------------%
 
 :- pred check_type_of_main(pred_info, io__state, io__state).
Index: purity.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/purity.m,v
retrieving revision 1.41
diff -u -r1.41 purity.m
--- purity.m	30 Jan 2002 01:40:30 -0000	1.41
+++ purity.m	14 Feb 2002 05:41:55 -0000
@@ -392,10 +392,10 @@
 	{ module_info_set_predicate_table(ModuleInfo0, PredTable,
 					  ModuleInfo1) },
 
-	(
-		{ pred_info_get_goal_type(PredInfo0, assertion) }
-	->
-		post_typecheck__finish_assertion(ModuleInfo1,
+		% finish processing of promise declarations
+	{ pred_info_get_goal_type(PredInfo0, GoalType) },
+	( { GoalType = promise(PromiseType) } ->
+		post_typecheck__finish_promise(PromiseType, ModuleInfo1,
 				PredId, ModuleInfo2)
 	;
 		{ ModuleInfo2 = ModuleInfo1 }
Index: typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
retrieving revision 1.310
diff -u -r1.310 typecheck.m
--- typecheck.m	12 Feb 2002 05:14:07 -0000	1.310
+++ typecheck.m	13 Feb 2002 05:11:52 -0000
@@ -4565,7 +4565,7 @@
 		{ check_marker(Markers, infer_type) },
 		{ module_info_predids(ModuleInfo, ValidPredIds) },
 		{ list__member(PredId, ValidPredIds) },
-		{ \+ pred_info_get_goal_type(PredInfo, assertion) }
+		{ \+ pred_info_get_goal_type(PredInfo, promise(_)) }
 	->
 		write_inference_message(PredInfo)
 	;
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------