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

[Lars Yencken]

Here's the new full diff.

Lars

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


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	19 Feb 2002 01:41:29 -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) ++ "' declaration"
 	;
 		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	19 Feb 2002 04:48:40 -0000
@@ -149,6 +149,14 @@
 :- pred direct_subgoal(hlds_goal_expr, hlds_goal).
 :- mode direct_subgoal(in, out) is nondet.
 
+	% returns all the predids that are used within a goal
+:- pred predids_from_goal(hlds_goal, list(pred_id)).
+:- mode predids_from_goal(in, out) is det.
+	
+	% returns all the predids that are used in a list of goals
+:- 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 +1291,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),
+		PredIds = PredIds0 ++ PredIds1
+	).
+
+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	19 Feb 2002 05:22:10 -0000
@@ -1038,3 +1038,86 @@
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
+
+:- interface.
+
+	% 
+	% A table recording exclusivity declarations (i.e. promise_exclusive
+	% 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. See
+	% notes/promise_ex.html for details of the declarations.
+	%
+
+	% an exclusive_id is the pred_id of an exclusivity declaration,
+	% and is useful in distinguishing between the arguments of the
+	% operations below on the exclusive_table
+:- type exclusive_id	==	pred_id.
+:- type exclusive_ids	==	list(pred_id).
+
+:- type exclusive_table.
+
+	% initialise the exclusive_table
+:- pred exclusive_table_init(exclusive_table).
+:- mode exclusive_table_init(out) is det.
+
+	% search the exclusive table and return the list of exclusivity
+	% declarations that use the predicate given by pred_id
+:- pred exclusive_table_search(exclusive_table, pred_id, exclusive_ids).
+:- mode exclusive_table_search(in, in, out) is semidet.
+
+	% as for search, but aborts if no exclusivity declarations are
+	% found
+:- pred exclusive_table_lookup(exclusive_table, pred_id, exclusive_ids).
+:- mode exclusive_table_lookup(in, in, out) is det.
+
+	% optimises the exclusive_table
+:- pred exclusive_table_optimize(exclusive_table, exclusive_table).
+:- mode exclusive_table_optimize(in, out) is det.
+
+	% add to the exclusive table that pred_id is used in the
+	% exclusivity declaration exclusive_id
+:- pred exclusive_table_add(pred_id, exclusive_id, exclusive_table,
+		exclusive_table).
+:- mode exclusive_table_add(in, in, in, out) is det.
+
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module multi_map.
+
+:- type exclusive_table		==	multi_map(pred_id, exclusive_id).
+
+exclusive_table_init(ExclusiveTable) :-
+	multi_map__init(ExclusiveTable).
+
+exclusive_table_lookup(ExclusiveTable, PredId, ExclusiveIds) :-
+	multi_map__lookup(ExclusiveTable, PredId, ExclusiveIds).
+
+exclusive_table_search(ExclusiveTable, Id, ExclusiveIds) :-
+	multi_map__search(ExclusiveTable, Id, ExclusiveIds).
+
+exclusive_table_optimize(ExclusiveTable0, ExclusiveTable) :-
+	multi_map__optimize(ExclusiveTable0, ExclusiveTable).
+
+exclusive_table_add(ExclusiveId, PredId, ExclusiveTable0, ExclusiveTable) :-
+	(
+		multi_map__contains(ExclusiveTable0, PredId)
+	->
+		multi_map__det_update(ExclusiveTable0, PredId, ExclusiveId, 
+				ExclusiveTable)
+	;
+		multi_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	19 Feb 2002 23:36:53 -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,10 @@
 	->
 		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)
+					++ "' declaration")
 	;
 		hlds_out__write_simple_call_id(PredOrFunc,
 			qualified(Module, Name), Arity)
@@ -389,12 +390,43 @@
 	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) }
+	->
+		io__write_string("`"),
+		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 +945,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 +954,25 @@
 		) },
 
 	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),
+		mercury_output_newline(Indent),
+		io__write_string("(\n")
+	),
+	
 	{ 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	19 Feb 2002 04:52:05 -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,43 +802,54 @@
 	
 add_item_clause(promise(PromiseType, Goal, VarSet, UnivVars),
 		Status, Status, Context, Module0, Module, Info0, Info) -->
-	( { PromiseType = true } ->	% promise is an assertion
+	%
+	% If the outermost universally quantified variables
+	% are placed in the head of the dummy predicate, the
+	% typechecker will avoid warning about unbound
+	% type variables as this implicity adds a universal
+	% quantification of the typevariables needed.
+	%
+	{ term__var_list_to_term_list(UnivVars, HeadVars) },
+	
+	% extra error checking for promise ex declarations
+	( { PromiseType \= true } ->
+		check_promise_ex_decl(UnivVars, PromiseType, Goal, Context)
+	;
+		[]
+	),
 
-		%
-		% If the outermost existentially quantified variables
-		% are placed in the head of the assertion, the
-		% typechecker will avoid warning about unbound
-		% type variables as this implicity adds a universal
-		% quantification of the typevariables needed.
-		%
-		{ term__var_list_to_term_list(UnivVars, HeadVars) },
+	% add as dummy predicate
+	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 +3595,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 +3629,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 +3642,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 +3656,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 +3756,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 +4016,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 +5285,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 +5314,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 +5592,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 +5600,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 +8425,133 @@
 		PragmaVars0 = []
 	).
 
+
 %-----------------------------------------------------------------------------%
+%
+% promise ex error checking
+%
+% The following predicates are used to perform extra error checking specific
+% to promise ex declarations (see notes/promise_ex.html). Currently, the 
+% following checks are performed:
+% 	* 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 its goal is a disjunction and that each arm of the 
+% 	  disjunction has at most one call, and otherwise has only unifications
+
+	% perform above checks on a promise ex declaration
+:- 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).
+
+	% check for misplaced universal quantification, otherwise find the
+	% disjunction, flatten it out into list form and perform further
+	% checks
+:- 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_conj_list, DisjList, DisjConsList) },
+		check_disjunction(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")
+	).
+
+	% turns the goal of a promise ex declaration into a list of goals,
+	% where each goal is an arm of the 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),
+		GoalList = GoalListA ++ GoalListB
+	;
+		GoalList = [GoalExpr - Context]
+	).
+
+	% takes a goal representing an arm of a disjunction and turn it into
+	% a list of conjunct goals
+:- pred flatten_to_conj_list(goal, goals).
+:- mode flatten_to_conj_list(in, out) is det.
+flatten_to_conj_list(GoalExpr - Context, GoalList) :-
+	( GoalExpr = ( GoalA , GoalB ) ->
+		flatten_to_conj_list(GoalA, GoalListA),
+		flatten_to_conj_list(GoalB, GoalListB),
+		GoalList = GoalListA ++ GoalListB
+	;
+		GoalList = [GoalExpr - Context]
+	).
+
+	% taking a list of arms of the disjunction, check each arm
+	% individually
+:- pred check_disjunction(promise_type, list(goals), io__state, io__state).
+:- mode check_disjunction(in, in, di, uo) is det.
+check_disjunction(PromiseType, DisjConsList) -->
+	(
+		{ DisjConsList = [] }
+	;
+		{ DisjConsList = [ConsList | Rest] },
+		check_disj_arm(PromiseType, ConsList, no),
+		check_disjunction(PromiseType, Rest)
+	).
+
+	% only one goal in an arm is allowed to be a call, the rest must be 
+	% unifications
+:- pred check_disj_arm(promise_type, goals, bool, io__state, io__state).
+:- mode check_disj_arm(in, in, in, di, uo) is det.
+check_disj_arm(PromiseType, Goals, CallUsed) -->
+	(
+		{ Goals = [] }
+	;
+		{ Goals = [GoalExpr - Context | Rest] },
+		( { GoalExpr = unify(_, _, _) } ->
+			check_disj_arm(PromiseType, Rest, CallUsed)
+		; { GoalExpr = some(_, Goal) } ->
+			check_disj_arm(PromiseType, [Goal | Rest], CallUsed)
+		; { GoalExpr = call(_, _, _) } ->
+			(
+				{ CallUsed = no }
+			;
+				{ CallUsed = yes },
+				promise_ex_error(PromiseType, Context, "disjunct contains more than one call")
+			),
+			check_disj_arm(PromiseType, Rest, yes)
+		;
+			promise_ex_error(PromiseType, Context, "disjunct is not a call or unification"),
+			check_disj_arm(PromiseType, Rest, CallUsed)
+		)
+	).
+
+
+	% called for any error in the above checks
+:- 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) -->
+	{ ErrorPieces = [
+		words("In"),
+		fixed("`" ++ prog_out__promise_to_string(PromiseType) ++ "' declaration:"),
+		nl,
+		words("error:"),
+		words(Message)
+		] },
+	error_util__write_error_pieces(Context, 0, ErrorPieces).
+
+%------------------------------------------------------------------------------%
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	19 Feb 2002 01:29:11 -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,92 @@
 		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) },
-	(
-		{ pred_info_is_exported(PredInfo) }
+	{ 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) :-
+	( 
+		% case for assertions
+		PromiseType = true
 	->
-		assertion__in_interface_check(Goal, PredInfo, Module2, Module3)
+		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)
 	;
-		{ Module3 = Module2 }
-	),
+		% case for exclusivity
+		(
+			PromiseType = exclusive
+		;
+			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 -- XXX not yet implemented
+		promise_ex_goal(PromiseId, Module0, Goal),
+		Module0 = Module
+	).
+
+	% get the goal from a promise_ex declaration
+:- 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__normalise_goal(Goal0, Goal)
+	;
+		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
--------------------------------------------------------------------------