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

[Lars Yencken]

Hi Fergus,

Thanks for reviewing my diff. Here's the relative diff.

Lars

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

--- error_util.m
+++ error_util.m
@@ -421 +421 @@
-		Piece = promise_to_string(PromiseType)
+		Piece = "`" ++ promise_to_string(PromiseType) ++ "' declaration"
--- goal_util.m
+++ goal_util.m
@@ -151,0 +152 @@
+	% returns all the predids that are used within a goal
@@ -154 +155,2 @@
-
+	
+	% returns all the predids that are used in a list of goals
@@ -1300 +1302 @@
-		Goals = [Goal|Rest],
+		Goals = [Goal | Rest],
@@ -1303 +1305 @@
-		append(PredIds0, PredIds1, PredIds)
+		PredIds = PredIds0 ++ PredIds1
--- hlds_data.m
+++ hlds_data.m
@@ -1044,3 +1043,0 @@
-:- type exclusive_id	==	pred_id.
-:- type exclusive_ids	==	list(pred_id).
-
@@ -1048,2 +1045,2 @@
-	% 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). 
@@ -1060,2 +1057,10 @@
-	% 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).
+
@@ -1063,0 +1069 @@
+	% initialise the exclusive_table
@@ -1066,0 +1073,2 @@
+	% search the exclusive table and return the list of exclusivity
+	% declarations that use the predicate given by pred_id
@@ -1069,0 +1078,2 @@
+	% as for search, but aborts if no exclusivity declarations are
+	% found
@@ -1072,0 +1083 @@
+	% optimises the exclusive_table
@@ -1075,0 +1087,2 @@
+	% add to the exclusive table that pred_id is used in the
+	% exclusivity declaration exclusive_id
@@ -1084 +1097,3 @@
-:- type exclusive_table		==	map(pred_id, exclusive_ids).
+:- import_module multi_map.
+
+:- type exclusive_table		==	multi_map(pred_id, exclusive_id).
@@ -1086 +1101,2 @@
-exclusive_table_init(map__init).
+exclusive_table_init(ExclusiveTable) :-
+	multi_map__init(ExclusiveTable).
@@ -1089 +1105 @@
-	map__lookup(ExclusiveTable, PredId, ExclusiveIds).
+	multi_map__lookup(ExclusiveTable, PredId, ExclusiveIds).
@@ -1092 +1108 @@
-	map__search(ExclusiveTable, Id, ExclusiveIds).
+	multi_map__search(ExclusiveTable, Id, ExclusiveIds).
@@ -1095 +1111 @@
-	map__optimize(ExclusiveTable0, ExclusiveTable).
+	multi_map__optimize(ExclusiveTable0, ExclusiveTable).
@@ -1099 +1115 @@
-		map__search(ExclusiveTable0, PredId, ExclusiveIds)
+		multi_map__contains(ExclusiveTable0, PredId)
@@ -1101,2 +1117,2 @@
-		map__det_update(ExclusiveTable0, PredId, 
-				[ExclusiveId|ExclusiveIds], ExclusiveTable)
+		multi_map__det_update(ExclusiveTable0, PredId, ExclusiveId, 
+				ExclusiveTable)
@@ -1104 +1120 @@
-		map__det_insert(ExclusiveTable0, PredId, [ExclusiveId], 
+		multi_map__det_insert(ExclusiveTable0, PredId, ExclusiveId, 
--- hlds_out.m
+++ hlds_out.m
@@ -373 +373,2 @@
-		io__write_string(prog_out__promise_to_string(PromiseType))
+		io__write_string("`" ++ prog_out__promise_to_string(PromiseType)
+					++ "' declaration")
@@ -417,0 +419 @@
+		io__write_string("`"),
@@ -419 +421 @@
-		io__write_string(" declaration")
+		io__write_string("' declaration")
@@ -958 +960 @@
-		io__write_string(":- promise all["),
+		io__write_string(":- promise all ["),
@@ -962 +964 @@
-		io__write_string(":- all["),
+		io__write_string(":- all ["),
--- make_hlds.m
+++ make_hlds.m
@@ -805,7 +805,7 @@
-		%
-		% 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.
+	%
@@ -813 +813,3 @@
-	( { \+ PromiseType = true } ->
+	
+	% extra error checking for promise ex declarations
+	( { PromiseType \= true } ->
@@ -817,0 +820,2 @@
+
+	% add as dummy predicate
@@ -8427,2 +8431 @@
-% XXX promise_ex declarations
-%
+% promise ex error checking
@@ -8429,0 +8433,9 @@
+% 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
@@ -8431,12 +8443 @@
-:- 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
@@ -8452 +8453 @@
-		{ UnivVars = [_|_] }
+		{ UnivVars = [_ | _] }
@@ -8456,2 +8457,3 @@
-
-	% 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
@@ -8465,2 +8467,2 @@
-		{ 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)
@@ -8474 +8476,2 @@
-
+	% turns the goal of a promise ex declaration into a list of goals,
+	% where each goal is an arm of the disjunction
@@ -8481 +8484 @@
-		append(GoalListA, GoalListB, GoalList)
+		GoalList = GoalListA ++ GoalListB
@@ -8486,3 +8489,5 @@
-:- 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) :-
@@ -8490,3 +8495,3 @@
-		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
@@ -8497,3 +8502,5 @@
-:- 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) -->
@@ -8503,3 +8510,3 @@
-		{ 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)
@@ -8508,19 +8515,5 @@
-:- 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) -->
@@ -8530 +8523 @@
-		{ Goals = [GoalExpr - Context|Rest] },
+		{ Goals = [GoalExpr - Context | Rest] },
@@ -8532 +8525 @@
-			check_cons_list(PromiseType, Rest, CallUsed)
+			check_disj_arm(PromiseType, Rest, CallUsed)
@@ -8534 +8527 @@
-			check_cons_list(PromiseType, [Goal|Rest], CallUsed)
+			check_disj_arm(PromiseType, [Goal | Rest], CallUsed)
@@ -8542 +8535 @@
-			check_cons_list(PromiseType, Rest, yes)
+			check_disj_arm(PromiseType, Rest, yes)
@@ -8545 +8538 @@
-			check_cons_list(PromiseType, Rest, CallUsed)
+			check_disj_arm(PromiseType, Rest, CallUsed)
@@ -8550 +8543 @@
-	% called for any promise_ex_error
+	% called for any error in the above checks
@@ -8555,8 +8548,8 @@
-	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).
--- post_typecheck.m
+++ post_typecheck.m
@@ -731,3 +731,4 @@
-	(
-			% case for assertions
-		PromiseType = true,
+	( 
+		% case for assertions
+		PromiseType = true
+	->
@@ -743,11 +744,7 @@
-			% 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
+		)
+	->
@@ -759,0 +757 @@
+
@@ -761,2 +759 @@
-			% case for exhaustiveness -- not yet implemented
-		PromiseType = exhaustive,
+		% case for exhaustiveness -- XXX not yet implemented
@@ -766,0 +764 @@
+	% get the goal from a promise_ex declaration
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------