[m-rev.] for review: parsing and pretty printing of promise ex declarations

Lars Yencken lljy at students.cs.mu.oz.au
Fri Feb 1 13:40:39 AEDT 2002


Estimated hours taken: 50
Branches: main

Added parsing and pretty printing of new promise ex declarations.

To avoid confusion:
	- a `promise ex declaration' refers to one of the new
	  promise_exclusive, promise_exhaustive or
	  promise_exclusive_exhaustive declarations
	- an `assertion' refers to one of the old `:- promise' 
	  declarations
	- a `promise' refers to a declaration of either of the above
	  types, and should be used when it concerns both of them

library/ops.m:
	Added the new operators to op_table.

compiler/prog_io.m:
	Added clauses to enter promise ex declarations into the parse
	tree.

compiler/prog_out.m:
	Added predicates useful in outputting promise declarations.

compiler/prog_data.m:
	Changed assertion constructor in type item to a more gereral
	promise constructor to be used for assertions and promise ex
	declarations. Added the type promise_type to differentiate
	between different promise declarations.

compiler/mercury_to_mercury.m:
	Added clauses to output promise items, including assertions
	and promise ex declarations.

compiler/make_hlds.m:
compiler/module_qual.m:
compiler/modules.m:
compiler/recompilation_check.m:
compiler/recompilation_version.m:
	Updated to reflect change in item type.


Index: compiler/make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.398
diff -u -b -r1.398 make_hlds.m
--- compiler/make_hlds.m	30 Jan 2002 01:40:24 -0000	1.398
+++ compiler/make_hlds.m	1 Feb 2002 01:14:54 -0000
@@ -253,7 +253,8 @@
 
 add_item_decl_pass_1(pragma(_), _, Status, Module, Status, Module) --> [].
 
-add_item_decl_pass_1(assertion(_, _), _, Status, Module, Status, Module) --> [].
+add_item_decl_pass_1(promise(_, _, _, _), _, Status, Module, Status, Module)
+	--> [].
 
 add_item_decl_pass_1(module_defn(_VarSet, ModuleDefn), Context,
 		Status0, Module0, Status, Module) -->
@@ -609,7 +610,8 @@
 		)
 	}.
 
-add_item_decl_pass_2(assertion(_, _), _, Status, Module, Status, Module) --> [].
+add_item_decl_pass_2(promise(_, _, _, _), _, Status, Module, Status, Module) 
+	--> [].
 add_item_decl_pass_2(clause(_, _, _, _, _), _, Status, Module, Status,
 		Module) --> [].
 add_item_decl_pass_2(inst_defn(_, _, _, _, _), _, Status, Module,
@@ -796,8 +798,10 @@
 		{ Module = Module0 },
 		{ Info = Info0 }	
 	).
-add_item_clause(assertion(Goal0, VarSet),
+	
+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
@@ -806,19 +810,10 @@
 		% type variables as this implicity adds a universal
 		% quantification of the typevariables needed.
 		%
-	(
-		{ Goal0 = all(Vars, AllGoal) - _Context }
-	->
-		{ term__var_list_to_term_list(Vars, HeadVars) },
-		{ Goal = AllGoal }
-	;
-		{ HeadVars = [] },
-		{ Goal = Goal0 }
-	),
-
+		{ term__var_list_to_term_list(UnivVars, HeadVars) },
 	{ term__context_line(Context, Line) },
 	{ term__context_file(Context, File) },
-	{ string__format("assertion__%d__%s", [i(Line), s(File)], Name) },
+		{ string__format("assertion__%d__%s", [i(Line), s(File)],Name)},
 
 		%
 		% The assertions are recorded as a predicate whose
@@ -835,8 +830,14 @@
 		%
 	{ IsAssertion = yes },
 	module_add_clause(Module0, VarSet, predicate, unqualified(Name),
-			HeadVars, Goal, Status, Context, IsAssertion, Module,
-			Info0, Info).
+				HeadVars, Goal, Status, Context, IsAssertion, 
+				Module, Info0, Info)
+	;
+			% promise is a promise ex declaration,
+			% not yet implemented
+		{ Module0 = Module },
+		{ Info0 = Info }
+	).
 
 add_item_clause(nothing(_), Status, Status, _,
 	Module, Module, Info, Info) --> [].
@@ -3279,7 +3280,7 @@
 	PredName = unqualified(Name),
 	special_pred_info(SpecialPredId, Type, Name, ArgTypes, ArgModes, Det),
 	special_pred_name_arity(SpecialPredId, _, _, Arity),
-	Cond = true,
+	Cond `with_type` condition = true,
 	clauses_info_init(Arity, ClausesInfo0),
 	adjust_special_pred_status(Status0, SpecialPredId, Status),
 	map__init(Proofs),
Index: compiler/mercury_to_mercury.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_to_mercury.m,v
retrieving revision 1.202
diff -u -b -r1.202 mercury_to_mercury.m
--- compiler/mercury_to_mercury.m	25 Jan 2002 05:57:35 -0000	1.202
+++ compiler/mercury_to_mercury.m	1 Feb 2002 01:17:40 -0000
@@ -613,9 +613,18 @@
 			"check_termination")
 	).
 
-mercury_output_item(_, assertion(Goal, VarSet), _) -->
-	io__write_string(":- promise "),
+mercury_output_item(_, promise(PromiseType, Goal, VarSet, UnivVars), _) -->
 	{ Indent = 1 },
+	( { PromiseType = true } ->
+		io__write_string(":- promise ")
+	;
+		io__write_string(":- all ["),
+		{ AppendVarNum = no },
+		mercury_output_vars(UnivVars, VarSet, AppendVarNum),
+		io__write_string("]"),
+		mercury_output_newline(Indent),
+		prog_out__write_promise_type(PromiseType)
+	),
 	mercury_output_newline(Indent),
 	mercury_output_goal(Goal, VarSet, Indent),
 	io__write_string(".\n").
@@ -682,6 +691,13 @@
 	),
 	io__write_string(".\n").
 
+:- func mercury_to_string_promise_type(promise_type) = string.
+mercury_to_string_promise_type(exclusive) = "promise_exclusive".
+mercury_to_string_promise_type(exhaustive) = "promise_exhaustive".
+mercury_to_string_promise_type(exclusive_exhaustive) = 
+		"promise_exclusive_exhaustive".
+mercury_to_string_promise_type(true) = "promise".
+	
 %-----------------------------------------------------------------------------%
 
 :- pred output_class_methods(list(class_method), io__state, io__state).
Index: compiler/module_qual.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/module_qual.m,v
retrieving revision 1.71
diff -u -b -r1.71 module_qual.m
--- compiler/module_qual.m	12 Dec 2001 00:30:09 -0000	1.71
+++ compiler/module_qual.m	1 Feb 2002 01:19:09 -0000
@@ -260,7 +260,8 @@
 	;
 		Info = Info0
 	).
-collect_mq_info_2(assertion(Goal, _ProgVarSet), Info0, Info) :-
+collect_mq_info_2(promise(_PromiseType, Goal, _ProgVarSet, _UnivVars), Info0, 
+		Info) :-
 	process_assert(Goal, SymNames, Success),
 	(
 		Success = yes,
@@ -276,7 +277,7 @@
 			), 
 			SymNames, Info0, Info)
 	;
-			% Any unqualified symbol in the assertion might
+			% Any unqualified symbol in the promise might
 			% come from *any* of the imported modules.
 			% There's no way for us to tell which ones.  So
 			% we conservatively assume that it uses all of
@@ -568,8 +569,8 @@
 						Info0, Info, yes) -->
 	{ mq_info_set_error_context(Info0, (pragma) - Context, Info1) },
 	qualify_pragma(Pragma0, Pragma, Info1, Info).
-module_qualify_item(assertion(G, V) - Context, assertion(G, V) - Context,
-						Info, Info, yes) --> [].
+module_qualify_item(promise(T, G, V, U) - Context, 
+		promise(T, G, V, U) - Context, Info, Info, yes) --> [].
 module_qualify_item(nothing(A) - Context, nothing(A) - Context,
 						Info, Info, yes) --> [].
 module_qualify_item(typeclass(Constraints0, Name, Vars, Interface0, VarSet) -
Index: compiler/modules.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modules.m,v
retrieving revision 1.213
diff -u -b -r1.213 modules.m
--- compiler/modules.m	30 Jan 2002 05:08:44 -0000	1.213
+++ compiler/modules.m	1 Feb 2002 00:28:16 -0000
@@ -1062,7 +1062,7 @@
 strip_assertions([], []).
 strip_assertions([Item - Context | Rest], Items) :-
 	( 
-		Item = assertion(_, _)
+		Item = promise(true, _, _, _)
 	->
 		strip_assertions(Rest, Items)
 	; 
Index: compiler/prog_data.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_data.m,v
retrieving revision 1.76
diff -u -b -r1.76 prog_data.m
--- compiler/prog_data.m	30 Jan 2002 01:40:29 -0000	1.76
+++ compiler/prog_data.m	1 Feb 2002 02:28:32 -0000
@@ -73,7 +73,9 @@
 
 	;	pragma(pragma_type)
 
-	;	assertion(goal, prog_varset)
+	;	promise(promise_type, goal, prog_varset, prog_vars)
+		% 	PromiseType, PromiseClause, ProgVariables, 
+		% 	UniversallyQuantifiedVars
 
 	;	typeclass(list(class_constraint), class_name, list(tvar),
 			class_interface, tvarset)
@@ -89,6 +91,12 @@
 		% used for items that should be ignored (e.g.
 		% NU-Prolog `when' declarations, which are silently
 		% ignored for backwards compatibility).
+
+:- type promise_type
+	--->	exclusive
+	;	exhaustive
+	;	exclusive_exhaustive
+	; 	(true).
 
 :- type type_and_mode	
 	--->	type_only(type)
Index: compiler/prog_io.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io.m,v
retrieving revision 1.197
diff -u -b -r1.197 prog_io.m
--- compiler/prog_io.m	16 Jul 2001 08:21:04 -0000	1.197
+++ compiler/prog_io.m	1 Feb 2002 00:28:16 -0000
@@ -856,7 +856,7 @@
 
 :- type decl_attribute
 	--->	purity(purity)
-	;	quantifier(quantifier_type, list(tvar))
+	;	quantifier(quantifier_type, list(var))
 	;	constraints(quantifier_type, term).
 		% the term here is the (not yet parsed) list of constraints
 
@@ -1136,9 +1136,24 @@
 	check_no_attributes(Result0, Attributes, Result).
 
 process_decl(ModuleName, VarSet, "promise", Assertion, Attributes, Result):-
-	parse_assertion(ModuleName, VarSet, Assertion, Result0),
+	parse_promise(ModuleName, true, VarSet, Assertion, Attributes, Result0),
 	check_no_attributes(Result0, Attributes, Result).
 
+process_decl(ModuleName, VarSet, "promise_exclusive", PromiseGoal, Attributes,
+		Result):-
+	parse_promise(ModuleName, exclusive, VarSet, PromiseGoal, Attributes, 
+			Result).
+
+process_decl(ModuleName, VarSet, "promise_exhaustive", PromiseGoal, Attributes,
+		Result):-
+	parse_promise(ModuleName, exhaustive, VarSet, PromiseGoal, Attributes, 
+			Result).
+
+process_decl(ModuleName, VarSet, "promise_exclusive_exhaustive", PromiseGoal, 
+		Attributes, Result):-
+	parse_promise(ModuleName, exclusive_exhaustive, VarSet, PromiseGoal, 
+		Attributes, Result).
+
 process_decl(ModuleName, VarSet, "typeclass", Args, Attributes, Result):-
 	parse_typeclass(ModuleName, VarSet, Args, Result0),
 	check_no_attributes(Result0, Attributes, Result).
@@ -1203,13 +1218,11 @@
 		constraints(univ, Constraints), Decl).
 parse_decl_attribute("=>", [Decl, Constraints],
 		constraints(exist, Constraints), Decl).
-parse_decl_attribute("some", [TVars0, Decl],
+parse_decl_attribute("some", [TVars, Decl],
 		quantifier(exist, TVarsList), Decl) :-
-	term__coerce(TVars0, TVars),
 	parse_list_of_vars(TVars, TVarsList).
-parse_decl_attribute("all", [TVars0, Decl],
+parse_decl_attribute("all", [TVars, Decl],
 		quantifier(univ, TVarsList), Decl) :-
-	term__coerce(TVars0, TVars),
 	parse_list_of_vars(TVars, TVarsList).
 
 :- pred check_no_attributes(maybe1(item), decl_attrs, maybe1(item)).
@@ -1239,14 +1252,17 @@
 
 %-----------------------------------------------------------------------------%
 
-	% parse the assertion declaration. 
-:- pred parse_assertion(module_name, varset, list(term), maybe1(item)).
-:- mode parse_assertion(in, in, in, out) is semidet.
-
-parse_assertion(_ModuleName, VarSet, [AssertionTerm], Result) :-
-	varset__coerce(VarSet, ProgVarSet),
-	parse_goal(AssertionTerm, ProgVarSet, AssertGoal, AssertVarSet),
-	Result = ok(assertion(AssertGoal, AssertVarSet)).
+:- pred parse_promise(module_name, promise_type, varset, list(term), decl_attrs,
+		maybe1(item)).
+:- mode parse_promise(in, in, in, in, in, out) is semidet.
+parse_promise(ModuleName, PromiseType, VarSet, [Term], Attributes, Result) :-
+		% get universally quantified variables
+	get_quant_vars(univ, ModuleName, Attributes, [], _, UnivVars0),
+	list__map(term__coerce_var, UnivVars0, UnivVars),
+	
+	varset__coerce(VarSet, ProgVarSet0),
+	parse_goal(Term, ProgVarSet0, PromiseGoal, ProgVarSet),
+	Result = ok(promise(PromiseType, PromiseGoal, ProgVarSet, UnivVars)).
 
 %-----------------------------------------------------------------------------%
 
@@ -1876,10 +1892,11 @@
 	% error message.)
 
 	list__reverse(RevAttributes0, Attributes0),
-	get_quant_tvars(univ, ModuleName, Attributes0, [],
+	get_quant_vars(univ, ModuleName, Attributes0, [],
 					Attributes1, _UnivQVars),
-	get_quant_tvars(exist, ModuleName, Attributes1, [],
-					Attributes2, ExistQVars),
+	get_quant_vars(exist, ModuleName, Attributes1, [],
+					Attributes2, ExistQVars0),
+	list__map(term__coerce_var, ExistQVars0, ExistQVars),
 	get_constraints(univ, ModuleName, Attributes2,
 					Attributes3, MaybeUnivConstraints),
 	get_constraints(exist, ModuleName, Attributes3,
@@ -1900,21 +1917,21 @@
 	ok(UnivConstraints), ok(ExistConstraints), ExistQVars,
 	ok(ExistQVars, constraints(UnivConstraints, ExistConstraints))).
 
-:- pred get_quant_tvars(quantifier_type, module_name, decl_attrs, list(tvar),
-		decl_attrs, list(tvar)).
-:- mode get_quant_tvars(in, in, in, in, out, out) is det.
-
-get_quant_tvars(QuantType, ModuleName, Attributes0, TVars0,
-		Attributes, TVars) :-
-	(	
-		Attributes0 = [quantifier(QuantType, TVars1) - _ | Attributes1]
-	->
-		list__append(TVars0, TVars1, TVars2),
-		get_quant_tvars(QuantType, ModuleName, Attributes1, TVars2,
-			Attributes, TVars)
+:- pred get_quant_vars(quantifier_type, module_name, decl_attrs, list(var),
+		decl_attrs, list(var)).
+:- mode get_quant_vars(in, in, in, in, out, out) is det.
+
+get_quant_vars(QuantType, ModuleName, Attributes0, Vars0,
+		Attributes, Vars) :-
+	(	
+		Attributes0 = [quantifier(QuantType, Vars1) - _ | Attributes1]
+	->
+		list__append(Vars0, Vars1, Vars2),
+		get_quant_vars(QuantType, ModuleName, Attributes1, Vars2,
+			Attributes, Vars)
 	;
 		Attributes = Attributes0,
-		TVars = TVars0
+		Vars = Vars0
 	).
 
 :- pred get_constraints(quantifier_type, module_name, decl_attrs, decl_attrs, 
Index: compiler/prog_out.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_out.m,v
retrieving revision 1.44
diff -u -b -r1.44 prog_out.m
--- compiler/prog_out.m	13 Jan 2000 06:16:59 -0000	1.44
+++ compiler/prog_out.m	1 Feb 2002 00:28:16 -0000
@@ -86,6 +86,14 @@
 		io__state, io__state).
 :- mode prog_out__write_list(in, pred(in, di, uo) is det, di, uo) is det.
 
+:- pred prog_out__write_promise_type(promise_type, io__state, io__state).
+:- mode prog_out__write_promise_type(in, di, uo) is det.
+
+:- func prog_out__promise_to_string(promise_type) = string.
+:- mode prog_out__promise_to_string(in) = out is det.
+:- mode prog_out__promise_to_string(out) = in is semidet.
+:- mode prog_out__promise_to_string(out) = out is multi.
+
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
 
@@ -273,6 +281,16 @@
 	call(Writer, Import).
 prog_out__write_list([], _) -->
 	{ error("prog_out__write_module_list") }.
+
+prog_out__promise_to_string(true) = "promise".
+prog_out__promise_to_string(exclusive) = "promise_exclusive".
+prog_out__promise_to_string(exhaustive) =  "promise_exhaustive".
+prog_out__promise_to_string(exclusive_exhaustive) = 
+		"promise_exclusive_exhaustive".
+
+prog_out__write_promise_type(PromiseType) -->
+	io__write_string(prog_out__promise_to_string(PromiseType)).
+
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
Index: compiler/recompilation_check.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/recompilation_check.m,v
retrieving revision 1.6
diff -u -b -r1.6 recompilation_check.m
--- compiler/recompilation_check.m	4 Nov 2001 14:42:55 -0000	1.6
+++ compiler/recompilation_check.m	1 Feb 2002 00:28:16 -0000
@@ -906,7 +906,7 @@
 		VersionNumbers, PredOrFunc, Name, Args).
 check_for_ambiguities(_, _, _, pred_or_func_mode(_, _, _, _, _, _) - _) --> [].
 check_for_ambiguities(_, _, _, pragma(_) - _) --> [].
-check_for_ambiguities(_, _, _, assertion(_, _) - _) --> [].
+check_for_ambiguities(_, _, _, promise(_, _, _, _) - _) --> [].
 check_for_ambiguities(_, _, _, module_defn(_, _) - _) --> [].
 check_for_ambiguities(_, _, _, instance(_, _, _, _, _, _) - _) --> [].
 check_for_ambiguities(_, _, _, nothing(_) - _) --> [].
Index: compiler/recompilation_version.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/recompilation_version.m,v
retrieving revision 1.11
diff -u -b -r1.11 recompilation_version.m
--- compiler/recompilation_version.m	5 Jan 2002 11:59:56 -0000	1.11
+++ compiler/recompilation_version.m	1 Feb 2002 00:28:16 -0000
@@ -432,7 +432,7 @@
 	% We need to handle these separately because some pragmas
 	% may affect a predicate and a function.
 item_to_item_id_2(pragma(_), no).
-item_to_item_id_2(assertion(_, _), no).
+item_to_item_id_2(promise(_, _, _, _), no).
 item_to_item_id_2(Item, yes(item_id((typeclass), ClassName - ClassArity))) :-
 	Item = typeclass(_, ClassName, ClassVars, _, _),
 	list__length(ClassVars, ClassArity).	
@@ -552,8 +552,8 @@
 	% doesn't work with inter-module optimization yet.
 item_is_unchanged(clause(_VarSet, PorF, SymName, Args, Goal), Item2) =
 		( Item2 = clause(_, PorF, SymName, Args, Goal) -> yes ; no ).
-item_is_unchanged(assertion(Goal, _VarSet), Item2) =
-		( Item2 = assertion(Goal, _) -> yes ; no ).
+item_is_unchanged(promise(PromiseType, Goal, _, UnivVars), Item2) =
+		( Item2 = promise(PromiseType, Goal, _, UnivVars) -> yes ; no ).
 
 	% We do need to compare the variable names in `:- pragma type_spec'
 	% declarations because the names of the variables are used
Index: library/ops.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/ops.m,v
retrieving revision 1.38
diff -u -b -r1.38 ops.m
--- library/ops.m	10 Dec 2001 06:11:33 -0000	1.38
+++ library/ops.m	1 Feb 2002 00:28:16 -0000
@@ -330,6 +330,10 @@
 ops__op_table("pragma", before, fx, 1199).	% Mercury extension
 ops__op_table("pred", before, fx, 800).		% Mercury/NU-Prolog extension
 ops__op_table("promise", before, fx, 1199).	% Mercury extension
+ops__op_table("promise_exclusive", before, fy, 950). % Mercury extension 
+ops__op_table("promise_exhaustive", before, fy, 950). % Mercury extension 
+ops__op_table("promise_exclusive_exhaustive", before, fy, 950). 
+						% Mercury extension 
 ops__op_table("rem", after, xfx, 400).		% Standard ISO Prolog
 ops__op_table("rule", before, fx, 1199).	% NU-Prolog extension
 ops__op_table("semipure", before, fy, 800).	% Mercury extension
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------



More information about the reviews mailing list