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

[Lars Yencken]

Ok, here's the proper relative diff, fixing also the missing '('.

Lars

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

diff -u error_util.m error_util.m
--- error_util.m
+++ error_util.m
@@ -418,7 +418,7 @@
 	(
 		pred_info_get_goal_type(PredInfo, promise(PromiseType))
 	->
-		Piece = promise_to_string(PromiseType)
+		Piece = "`" ++ promise_to_string(PromiseType) ++ "' declaration"
 	;
 		string__int_to_string(OrigArity, ArityPart),
 		string__append_list([
diff -u goal_util.m goal_util.m
--- goal_util.m
+++ goal_util.m
@@ -149,9 +149,11 @@
 :- 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.
 
@@ -1297,10 +1299,10 @@
 		Goals = [],
 		PredIds = []
 	;
-		Goals = [Goal|Rest],
+		Goals = [Goal | Rest],
 		predids_from_goal(Goal, PredIds0),
 		predids_from_goals(Rest, PredIds1),
-		append(PredIds0, PredIds1, PredIds)
+		PredIds = PredIds0 ++ PredIds1
 	).
 
 predids_from_goal(Goal, PredIds) :-
diff -u hlds_data.m hlds_data.m
--- hlds_data.m
+++ hlds_data.m
@@ -1041,12 +1041,9 @@
 
 :- 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). 
+	% A table recording exclusivity declarations (i.e. promise_exclusive
+	% and promise_exclusive_exhaustive). 
 	%
 	% e.g. :- all [X]
 	% 		promise_exclusive
@@ -1057,22 +1054,38 @@
 	% 		).
 	% 
 	% promises that only one of p(X, Y) and q(X) can succeed at a time,
-	% although whichever one succeeds may have multiple solutions.
-	
+	% 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.
@@ -1081,27 +1094,30 @@
 
 :- implementation.
 
-:- type exclusive_table		==	map(pred_id, exclusive_ids).
+:- import_module multi_map.
+
+:- type exclusive_table		==	multi_map(pred_id, exclusive_id).
 
-exclusive_table_init(map__init).
+exclusive_table_init(ExclusiveTable) :-
+	multi_map__init(ExclusiveTable).
 
 exclusive_table_lookup(ExclusiveTable, PredId, ExclusiveIds) :-
-	map__lookup(ExclusiveTable, PredId, ExclusiveIds).
+	multi_map__lookup(ExclusiveTable, PredId, ExclusiveIds).
 
 exclusive_table_search(ExclusiveTable, Id, ExclusiveIds) :-
-	map__search(ExclusiveTable, Id, ExclusiveIds).
+	multi_map__search(ExclusiveTable, Id, ExclusiveIds).
 
 exclusive_table_optimize(ExclusiveTable0, ExclusiveTable) :-
-	map__optimize(ExclusiveTable0, ExclusiveTable).
+	multi_map__optimize(ExclusiveTable0, ExclusiveTable).
 
 exclusive_table_add(ExclusiveId, PredId, ExclusiveTable0, ExclusiveTable) :-
 	(
-		map__search(ExclusiveTable0, PredId, ExclusiveIds)
+		multi_map__contains(ExclusiveTable0, PredId)
 	->
-		map__det_update(ExclusiveTable0, PredId, 
-				[ExclusiveId|ExclusiveIds], ExclusiveTable)
+		multi_map__det_update(ExclusiveTable0, PredId, ExclusiveId, 
+				ExclusiveTable)
 	;
-		map__det_insert(ExclusiveTable0, PredId, [ExclusiveId], 
+		multi_map__det_insert(ExclusiveTable0, PredId, ExclusiveId, 
 				ExclusiveTable)
 	).
 
diff -u hlds_out.m hlds_out.m
--- hlds_out.m
+++ hlds_out.m
@@ -370,7 +370,8 @@
 	;
 		{ pred_info_get_goal_type(PredInfo, promise(PromiseType)) }
 	->
-		io__write_string(prog_out__promise_to_string(PromiseType))
+		io__write_string("`" ++ prog_out__promise_to_string(PromiseType)
+					++ "' declaration")
 	;
 		hlds_out__write_simple_call_id(PredOrFunc,
 			qualified(Module, Name), Arity)
@@ -415,8 +416,9 @@
 	(
 		{ Promise = promise(PromiseType) }
 	->
+		io__write_string("`"),
 		prog_out__write_promise_type(PromiseType),
-		io__write_string(" declaration")
+		io__write_string("' declaration")
 	;
 		hlds_out__write_pred_or_func(PredOrFunc),
 		io__write_string(" `"),
@@ -955,16 +957,17 @@
 
 		% print initial formatting differently for assertions
 	( { PromiseType = true } ->
-		io__write_string(":- promise all["),
+		io__write_string(":- promise all ["),
 		io__write_list(HeadVars, ", ", PrintVar),
 		io__write_string("] (\n")
 	;
-		io__write_string(":- all["),
+		io__write_string(":- all ["),
 		io__write_list(HeadVars, ", ", PrintVar),
 		io__write_string("]"),
 		mercury_output_newline(Indent),
 		prog_out__write_promise_type(PromiseType),
-		io__nl
+		mercury_output_newline(Indent),
+		io__write_string("(\n")
 	),
 	
 	{ Clause = clause(_Modes, Goal, _Lang, _Context) },
diff -u make_hlds.m make_hlds.m
--- make_hlds.m
+++ make_hlds.m
@@ -802,19 +802,23 @@
 	
 add_item_clause(promise(PromiseType, Goal, VarSet, UnivVars),
 		Status, Status, Context, Module0, Module, Info0, Info) -->
-		%
-		% 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.
-		%
+	%
+	% 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) },
-	( { \+ PromiseType = true } ->
+	
+	% extra error checking for promise ex declarations
+	( { PromiseType \= true } ->
 		check_promise_ex_decl(UnivVars, PromiseType, Goal, Context)
 	;
 		[]
 	),
+
+	% add as dummy predicate
 	add_promise_clause(PromiseType, HeadVars, VarSet, Goal, Context, Status,
 			Module0, Module, Info0, Info).
 
@@ -8424,22 +8428,19 @@
 
 %-----------------------------------------------------------------------------%
 %
-% XXX promise_ex declarations
-%
+% 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
 
-:- 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
+	% 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.
@@ -8449,12 +8450,13 @@
 		{ UnivVars = [] },
 		promise_ex_error(PromiseType, Context, "declaration has no universally quantified variables")
 	;
-		{ UnivVars = [_|_] }
+		{ UnivVars = [_ | _] }
 	),
 	check_promise_ex_goal(PromiseType, Goal).
 
-
-	% strip off any existential quantification, then 
+	% 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) -->
@@ -8462,8 +8464,8 @@
 		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)
+		{ 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)
@@ -8471,67 +8473,58 @@
 		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),
-		append(GoalListA, GoalListB, GoalList)
+		GoalList = GoalListA ++ GoalListB
 	;
 		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) :-
+	% 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_cons_list(GoalA, GoalListA),
-		flatten_to_cons_list(GoalB, GoalListB),
-		append(GoalListA, GoalListB, GoalList)
+		flatten_to_conj_list(GoalA, GoalListA),
+		flatten_to_conj_list(GoalB, GoalListB),
+		GoalList = GoalListA ++ GoalListB
 	;
 		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) -->
+	% 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_cons_list(PromiseType, ConsList, no),
-		check_list_cons_list(PromiseType, Rest)
+		{ DisjConsList = [ConsList | Rest] },
+		check_disj_arm(PromiseType, ConsList, no),
+		check_disjunction(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) -->
+	% 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] },
+		{ Goals = [GoalExpr - Context | Rest] },
 		( { GoalExpr = unify(_, _, _) } ->
-			check_cons_list(PromiseType, Rest, CallUsed)
+			check_disj_arm(PromiseType, Rest, CallUsed)
 		; { GoalExpr = some(_, Goal) } ->
-			check_cons_list(PromiseType, [Goal|Rest], CallUsed)
+			check_disj_arm(PromiseType, [Goal | Rest], CallUsed)
 		; { GoalExpr = call(_, _, _) } ->
 			(
 				{ CallUsed = no }
@@ -8539,26 +8532,26 @@
 				{ CallUsed = yes },
 				promise_ex_error(PromiseType, Context, "disjunct contains more than one call")
 			),
-			check_cons_list(PromiseType, Rest, yes)
+			check_disj_arm(PromiseType, Rest, yes)
 		;
 			promise_ex_error(PromiseType, Context, "disjunct is not a call or unification"),
-			check_cons_list(PromiseType, Rest, CallUsed)
+			check_disj_arm(PromiseType, Rest, CallUsed)
 		)
 	).
 
 
-	% called for any promise_ex_error
+	% 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) -->
-	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.
+	{ ErrorPieces = [
+		words("In"),
+		fixed("`" ++ prog_out__promise_to_string(PromiseType) ++ "' declaration:"),
+		nl,
+		words("error:"),
+		words(Message)
+		] },
+	error_util__write_error_pieces(Context, 0, ErrorPieces).
 
 %------------------------------------------------------------------------------%
diff -u post_typecheck.m post_typecheck.m
--- post_typecheck.m
+++ post_typecheck.m
@@ -728,9 +728,10 @@
 		hlds_goal).
 :- mode store_promise(in, in, in, out, out) is det.
 store_promise(PromiseType, Module0, PromiseId, Module, Goal) :-
-	(
-			% case for assertions
-		PromiseType = true,
+	( 
+		% case for assertions
+		PromiseType = true
+	->
 		module_info_assertion_table(Module0, AssertTable0),
 		assertion_table_add_assertion(PromiseId, AssertTable0, 
 				AssertionId, AssertTable),
@@ -740,30 +741,27 @@
 		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,
+		% 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 -- not yet implemented
-		PromiseType = exhaustive,
+		% 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) :-
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------