[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