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

[Fergus Henderson]

On 15-Feb-2002, Lars Yencken <lljy at students.cs.mu.oz.au> wrote:
> +++ 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.

These need to be documented.
Our Mercury coding guidelines say that all procedures which
are exported from a module should be documented.

> +predids_from_goals(Goals, PredIds) :- 
> +	(
> +		Goals = [],
> +		PredIds = []
> +	;
> +		Goals = [Goal|Rest],
> +		predids_from_goal(Goal, PredIds0),
> +		predids_from_goals(Rest, PredIds1),
> +		append(PredIds0, PredIds1, PredIds)
> +	).

It's a little clearer to use the infix `++' function.

> Index: hlds_data.m
> +++ hlds_data.m	14 Feb 2002 01:22:19 -0000
> @@ -1038,3 +1038,70 @@
>  
>  %-----------------------------------------------------------------------------%
>  %-----------------------------------------------------------------------------%
> +
> +:- interface.

There should be a comment at the start explaining what this part
of the module is about.

> +:- type exclusive_id	==	pred_id.
> +:- type exclusive_ids	==	list(pred_id).

There should be a comment explaining what an exclusive_id represents.

> +	% 
> +	% 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.

The documentation about what a promise_ex declaration is would be
better placed at the start of this section.
There should also be a pointer to compiler/notes/promise_ex.html.

> +:- 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.

These procedures should be documented.

> +%-----------------------------------------------------------------------------%
> +
> +:- 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)
> +	).

Is there any particular reason why you didn't use
`multi_map' rather than `map'?

> Index: hlds_out.m
...
> +		% 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
> +	),

You should output "all [" rather than "all[" (in both places).

Also it looks like the output for promise_ex declarations
is missing a `('.

> @@ -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

You should fix up the indentation of this clause.

> @@ -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 } ->

Write that as `( { PromiseType \= true } ->'

> @@ -8413,4 +8421,144 @@
...
> +%
> +% XXX promise_ex declarations
> +%
> +%
> +
> +:- type promise_ex_goal
> +	--->	ok(goals)
> +	;	error(string, prog_context).

The XXX comment here should be replaced with a comment
that explains what the `promise_ex_goal' type represents
and how it is used (perhaps with a pointer to compiler/notes/promise_ex.html).

> +	% strip off any existential quantification, then 
> +:- pred check_promise_ex_goal(promise_type, goal, io__state, io__state).

That comment is unfinished.

> +:- 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]
> +	).

What is "cons_list" supposed to mean here?
I think you need s/cons_list/conj_list/g

Also a brief comment saying what the predicate is supposed to do
would help.

> +:- 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)
> +	).

Likewise here.

> +	% 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) -->

Likewise here too.

> +	(
> +		{ Goals = [] }
> +	;
> +		{ Goals = [GoalExpr - Context|Rest] },

s/|/ | /

> +	% 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.

You should provide more explanations for each of the error messages,
and output them if the verbose_errors option is set.

There should be single quotes around the declaration type,
i.e. output

	In `promise_exclusive' declaration:

rather than

	In promise_exclusive declaration:

Also the error messages should ideally be output with write_error_pieces
from error_util.m.

> Index: post_typecheck.m
...
> +	% 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 exclusivity
> +		PromiseType = exclusive_exhaustive,

The comment there doesn't match the code.

> +		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
> +	).

Add "XXX" before "not yet implemented".

Otherwise that looks good.  Please post both a full and a relative diff
when you've addressed these changes.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------