[m-rev.] for review: restore writing promises to .opt files
Peter Wang
novalazy at gmail.com
Tue Jul 10 12:38:24 AEST 2012
Branches: main
Restore writing promises to `.opt' files.
Also some cosmetic changes relating to promises.
compiler/intermod.m:
Predicates representing promises have the `infer_modes' flag set
(not actually necessary), causing promises not to be written out to
`.opt' files. Add an exception for promises.
Improve code style.
compiler/add_clause.m:
Add a comment about the `infer_modes' flag.
compiler/assertion.m:
Use a shared predicate in `record_preds_used_in' and add a sanity
check.
Improve code style.
compiler/hlds_out_util.m:
Use the location of a promise declaration in `pred_id_to_string'.
compiler/hlds_pred.m:
Add a helper predicate `pred_info_is_promise'.
Put `is_unify_or_compare_pred' in the same relative position as
its declaration.
compiler/dead_proc_elim.m:
compiler/hlds_error_util.m:
compiler/typecheck.m:
Use `pred_info_is_promise'.
doc/reference_manual.texi:
Update some commented-out out documentation.
diff --git a/compiler/add_clause.m b/compiler/add_clause.m
index fb77dc0..6e9bded 100644
--- a/compiler/add_clause.m
+++ b/compiler/add_clause.m
@@ -257,6 +257,8 @@ module_add_clause(ClauseVarSet, PredOrFunc, PredName, Args0, Body, Status,
% Check if there are still no modes for the predicate, and
% if so, set the `infer_modes' flag for that predicate.
+ % (Predicates representing promises do not need mode inference
+ % so the flag could be omitted for them.)
ProcIds = pred_info_all_procids(!.PredInfo),
(
diff --git a/compiler/assertion.m b/compiler/assertion.m
index 73d0aaf..449c968 100644
--- a/compiler/assertion.m
+++ b/compiler/assertion.m
@@ -202,20 +202,10 @@ is_associativity_assertion(Module, AssertId, CallVars,
UniversiallyQuantifiedVars = goal_info_get_nonlocals(GoalInfo),
- % There may or may not be a some [] depending on whether
- % the user explicity qualified the call or not.
- (
- P = hlds_goal(scope(_, hlds_goal(conj(plain_conj, PCalls0), _)), _),
- Q = hlds_goal(scope(_, hlds_goal(conj(plain_conj, QCalls0), _)), _)
- ->
- PCalls = PCalls0,
- QCalls = QCalls0
- ;
- P = hlds_goal(conj(plain_conj, PCalls), _PGoalInfo),
- Q = hlds_goal(conj(plain_conj, QCalls), _QGoalInfo)
- ),
+ get_conj_goals(P, PCalls),
+ get_conj_goals(Q, QCalls),
promise_equivalent_solutions [AssociativeVars, OutputVar] (
- associative(PCalls, QCalls, UniversiallyQuantifiedVars, CallVars,
+ associative(PCalls, QCalls, UniversiallyQuantifiedVars, CallVars,
AssociativeVars - OutputVar)
).
@@ -251,11 +241,11 @@ associative(PCalls, QCalls, UniversiallyQuantifiedVars, CallVars,
(AB - ABC) - (BC - ABC)]),
assoc_list.from_corresponding_lists(Vs, CallVars, AssocList),
- list.filter((pred(X-_Y::in) is semidet :- X = AB),
+ list.filter((pred(X - _Y::in) is semidet :- X = AB),
AssocList, [_AB - OutputVar]),
- list.filter((pred(X-_Y::in) is semidet :- X = A),
+ list.filter((pred(X - _Y::in) is semidet :- X = A),
AssocList, [_A - CallVarA]),
- list.filter((pred(X-_Y::in) is semidet :- X = B),
+ list.filter((pred(X - _Y::in) is semidet :- X = B),
AssocList, [_B - CallVarB]).
% reorder(Ps, Qs, Ls, Rs):
@@ -292,8 +282,8 @@ process_one_side(Goals, UniversiallyQuantifiedVars, PredId,
LinkingVar, Vars0, VarsA),
% Filter out all the invariant arguments, and then make sure that
- % their is only 3 arguments left.
- list.filter((pred(X-Y::in) is semidet :- not X = Y), Vars0, Vars),
+ % there are only 3 arguments left.
+ list.filter((pred(X - Y::in) is semidet :- X \= Y), Vars0, Vars),
list.length(Vars, number_of_associative_vars).
:- func number_of_associative_vars = int.
@@ -308,21 +298,11 @@ is_update_assertion(Module, AssertId, _PredId, CallVars, StateA - StateB) :-
goal_is_equivalence(hlds_goal(GoalExpr, GoalInfo), P, Q),
UniversiallyQuantifiedVars = goal_info_get_nonlocals(GoalInfo),
- % There may or may not be an explicit some [Vars] there,
- % as quantification now works correctly.
- (
- P = hlds_goal(scope(_, hlds_goal(conj(plain_conj, PCalls0), _)), _),
- Q = hlds_goal(scope(_, hlds_goal(conj(plain_conj, QCalls0), _)), _)
- ->
- PCalls = PCalls0,
- QCalls = QCalls0
- ;
- P = hlds_goal(conj(plain_conj, PCalls), _PGoalInfo),
- Q = hlds_goal(conj(plain_conj, QCalls), _QGoalInfo)
- ),
-
- solutions.solutions(update(PCalls, QCalls,
- UniversiallyQuantifiedVars, CallVars), [StateA - StateB | _]).
+ get_conj_goals(P, PCalls),
+ get_conj_goals(Q, QCalls),
+ solutions.solutions(
+ update(PCalls, QCalls, UniversiallyQuantifiedVars, CallVars),
+ [StateA - StateB | _]).
% compose(S0, A, SA), compose(SB, A, S),
% compose(SA, B, S) <=> compose(S0, B, SB)
@@ -339,7 +319,7 @@ update(PCalls, QCalls, UniversiallyQuantifiedVars, CallVars,
SB, PairsR, _),
assoc_list.from_corresponding_lists(PairsL, PairsR, Pairs0),
- list.filter((pred(X-Y::in) is semidet :- X \= Y), Pairs0, Pairs),
+ list.filter((pred(X - Y::in) is semidet :- X \= Y), Pairs0, Pairs),
list.length(Pairs) = 2,
% If you read the predicate documentation, you will note that
@@ -350,9 +330,9 @@ update(PCalls, QCalls, UniversiallyQuantifiedVars, CallVars,
list.perm(Pairs, [(S0 - SA) - (SB - S0), (SA - S) - (S - SB)]),
assoc_list.from_corresponding_lists(Vs, CallVars, AssocList),
- list.filter((pred(X-_Y::in) is semidet :- X = S0),
+ list.filter((pred(X - _Y::in) is semidet :- X = S0),
AssocList, [_S0 - StateA]),
- list.filter((pred(X-_Y::in) is semidet :- X = SA),
+ list.filter((pred(X - _Y::in) is semidet :- X = SA),
AssocList, [_SA - StateB]).
%-----------------------------------------------------------------------------%
@@ -372,11 +352,13 @@ update(PCalls, QCalls, UniversiallyQuantifiedVars, CallVars,
process_two_linked_calls(Goals, UniversiallyQuantifiedVars, PredId,
LinkingVar, Vars, VarsA) :-
- Goals = [hlds_goal(plain_call(PredId, _, VarsA, _, _, _), _),
- hlds_goal(plain_call(PredId, _, VarsB, _, _, _), _)],
+ Goals = [
+ hlds_goal(plain_call(PredId, _, VarsA, _, _, _), _),
+ hlds_goal(plain_call(PredId, _, VarsB, _, _, _), _)
+ ],
% Determine the linking variable, L. By definition it must be
- % existentially quantified and member of both variable lists.
+ % existentially quantified and a member of both variable lists.
CommonVars = list_to_set(VarsA) `intersect` list_to_set(VarsB),
set_of_var.is_singleton(
set_of_var.difference(CommonVars, UniversiallyQuantifiedVars),
@@ -437,6 +419,28 @@ predicate_call(Goal, PredId) :-
).
%-----------------------------------------------------------------------------%
+
+:- pred get_conj_goals(hlds_goal::in, list(hlds_goal)::out) is semidet.
+
+get_conj_goals(Goal0, ConjList) :-
+ % The user may have explicitly quantified the goals.
+ ignore_exist_quant_scope(Goal0, Goal),
+ Goal = hlds_goal(conj(plain_conj, ConjList), _).
+
+:- pred ignore_exist_quant_scope(hlds_goal::in, hlds_goal::out) is det.
+
+ignore_exist_quant_scope(Goal0, Goal) :-
+ Goal0 = hlds_goal(GoalExpr0, _Context),
+ (
+ GoalExpr0 = scope(Reason, Goal1),
+ Reason = exist_quant(_)
+ ->
+ Goal = Goal1
+ ;
+ Goal = Goal0
+ ).
+
+%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
assert_id_goal(Module, AssertId, Goal) :-
@@ -446,10 +450,14 @@ assert_id_goal(Module, AssertId, Goal) :-
pred_info_get_clauses_info(PredInfo, ClausesInfo),
clauses_info_get_clauses_rep(ClausesInfo, ClausesRep, _ItemNumbers),
get_clause_list(ClausesRep, Clauses),
- ( Clauses = [Clause] ->
+ (
+ Clauses = [Clause],
Goal0 = Clause ^ clause_body,
normalise_goal(Goal0, Goal)
;
+ ( Clauses = []
+ ; Clauses = [_, _ | _]
+ ),
unexpected($module, $pred, "goal is not an assertion")
).
@@ -643,10 +651,13 @@ equal_goals_cases([CaseA | CaseAs], [CaseB | CaseBs], !Subst) :-
%-----------------------------------------------------------------------------%
record_preds_used_in(Goal, AssertId, !Module) :-
- % Explicit lambda expression needed since goal_calls_pred_id
- % has multiple modes.
- P = (pred(PredId::out) is nondet :- goal_calls_pred_id(Goal, PredId)),
- solutions.solutions(P, PredIds),
+ predids_from_goal(Goal, PredIds),
+ % Sanity check.
+ ( list.member(invalid_pred_id, PredIds) ->
+ unexpected($module, $pred, "invalid pred_id")
+ ;
+ true
+ ),
list.foldl(update_pred_info(AssertId), PredIds, !Module).
%-----------------------------------------------------------------------------%
diff --git a/compiler/dead_proc_elim.m b/compiler/dead_proc_elim.m
index 7554086..c63c708 100644
--- a/compiler/dead_proc_elim.m
+++ b/compiler/dead_proc_elim.m
@@ -1109,7 +1109,7 @@ dead_pred_elim_initialize(PredId, DeadInfo0, DeadInfo) :-
PredArity = 1
;
% Don't eliminate the clauses for promises.
- pred_info_get_goal_type(PredInfo, goal_type_promise(_))
+ pred_info_is_promise(PredInfo, _)
)
->
set_tree234.insert(qualified(PredModule, PredName), !NeededNames),
diff --git a/compiler/hlds_error_util.m b/compiler/hlds_error_util.m
index aa5eef8..8c2008d 100644
--- a/compiler/hlds_error_util.m
+++ b/compiler/hlds_error_util.m
@@ -162,7 +162,7 @@ describe_one_pred_info_name(ShouldModuleQualify, PredInfo) = Pieces :-
)
; check_marker(Markers, marker_class_instance_method) ->
Pieces = [words("type class method implementation")]
- ; pred_info_get_goal_type(PredInfo, goal_type_promise(PromiseType)) ->
+ ; pred_info_is_promise(PredInfo, PromiseType) ->
Pieces = [words("`" ++ promise_to_string(PromiseType) ++ "'"),
words("declaration")]
;
diff --git a/compiler/hlds_out_util.m b/compiler/hlds_out_util.m
index b4d19a2..3e53470 100644
--- a/compiler/hlds_out_util.m
+++ b/compiler/hlds_out_util.m
@@ -218,6 +218,7 @@
:- import_module assoc_list.
:- import_module int.
:- import_module map.
+:- import_module require.
:- import_module string.
:- import_module term_io.
:- import_module varset.
@@ -288,20 +289,22 @@ pred_id_to_string(ModuleInfo, PredId) = Str :-
" for `", ClassStr, "(", TypeStrs, ")'"
])
;
+ Origin = origin_assertion(FileName, LineNumber),
+ ( pred_info_is_promise(PredInfo, PromiseType) ->
+ Str = string.format("`%s' declaration (%s:%d)",
+ [s(prog_out.promise_to_string(PromiseType)),
+ s(FileName), i(LineNumber)])
+ ;
+ unexpected($module, $pred, "origin_assertion")
+ )
+ ;
( Origin = origin_transformed(_, _, _)
- ; Origin = origin_assertion(_, _)
; Origin = origin_created(_)
; Origin = origin_lambda(_, _, _)
; Origin = origin_user(_)
),
- pred_info_get_goal_type(PredInfo, GoalType),
- ( GoalType = goal_type_promise(PromiseType) ->
- Str = "`" ++ prog_out.promise_to_string(PromiseType)
- ++ "' declaration"
- ;
- Str = simple_call_id_to_string(PredOrFunc,
- qualified(Module, Name), Arity)
- )
+ Str = simple_call_id_to_string(PredOrFunc,
+ qualified(Module, Name), Arity)
)
;
% The predicate has been deleted, so we print what we can.
diff --git a/compiler/hlds_pred.m b/compiler/hlds_pred.m
index cc85f0c..e1b932a 100644
--- a/compiler/hlds_pred.m
+++ b/compiler/hlds_pred.m
@@ -3213,8 +3213,15 @@ pred_info_is_field_access_function(ModuleInfo, PredInfo) :-
%
:- func builtin_state(module_info, pred_id, pred_id, proc_id) = builtin_state.
+ % Succeeds iff PredInfo represents a promise of the given type.
+ %
+:- pred pred_info_is_promise(pred_info::in, promise_type::out) is semidet.
+
:- implementation.
+is_unify_or_compare_pred(PredInfo) :-
+ pred_info_get_origin(PredInfo, origin_special_pred(_)). % XXX bug
+
pred_info_is_builtin(PredInfo) :-
ModuleName = pred_info_module(PredInfo),
PredName = pred_info_name(PredInfo),
@@ -3260,8 +3267,8 @@ is_inline_builtin(ModuleName, PredName, ProcId, Arity) :-
prog_varset_init(VarSet) :- varset.init(VarSet).
-is_unify_or_compare_pred(PredInfo) :-
- pred_info_get_origin(PredInfo, origin_special_pred(_)). % XXX bug
+pred_info_is_promise(PredInfo, PromiseType) :-
+ pred_info_get_goal_type(PredInfo, goal_type_promise(PromiseType)).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
diff --git a/compiler/intermod.m b/compiler/intermod.m
index 842c8f5..13f780e 100644
--- a/compiler/intermod.m
+++ b/compiler/intermod.m
@@ -367,9 +367,8 @@ should_be_processed(ProcessLocalPreds, PredId, PredInfo, TypeSpecForcePreds,
clause_list_is_deforestable(PredId, Clauses)
)
;
- % Promises that are in the interface should always get included
- % in the .opt file.
- pred_info_get_goal_type(PredInfo, goal_type_promise(_))
+ % Allow promises to be written.
+ pred_info_is_promise(PredInfo, _)
).
% If the clauses contains foreign code which requires an external
@@ -647,7 +646,9 @@ add_proc_2(PredId, DoWrite, !Info) :-
% to output declarations for them to the `.opt' file, since they
% will be recreated every time anyway.
- is_unify_or_compare_pred(PredInfo)
+ ( is_unify_or_compare_pred(PredInfo)
+ ; pred_info_is_promise(PredInfo, _)
+ )
->
DoWrite = yes
;
@@ -1761,15 +1762,27 @@ intermod_write_preds(OutInfo, ModuleInfo, [PredId | PredIds], !IO) :-
clauses_info_get_vartypes(ClausesInfo, VarTypes),
get_clause_list(ClausesRep, Clauses),
- ( pred_info_get_goal_type(PredInfo, goal_type_promise(PromiseType)) ->
- ( Clauses = [Clause] ->
+ pred_info_get_goal_type(PredInfo, GoalType),
+ (
+ GoalType = goal_type_promise(PromiseType),
+ (
+ Clauses = [Clause],
+ AppendVarNums = no,
write_promise(OutInfo, PromiseType, 0, ModuleInfo,
- PredId, VarSet, no, HeadVars, PredOrFunc, Clause,
+ PredId, VarSet, AppendVarNums, HeadVars, PredOrFunc, Clause,
no_varset_vartypes, !IO)
;
+ ( Clauses = []
+ ; Clauses = [_, _ | _]
+ ),
unexpected($module, $pred, "assertion not a single clause.")
)
;
+ ( GoalType = goal_type_clause
+ ; GoalType = goal_type_foreign
+ ; GoalType = goal_type_clause_and_foreign
+ ; GoalType = goal_type_none
+ ),
pred_info_get_typevarset(PredInfo, TypeVarset),
MaybeVarTypes = varset_vartypes(TypeVarset, VarTypes),
list.foldl(
diff --git a/compiler/typecheck.m b/compiler/typecheck.m
index 8cd9184..55c08c4 100644
--- a/compiler/typecheck.m
+++ b/compiler/typecheck.m
@@ -280,7 +280,7 @@ construct_type_inference_messages(ModuleInfo, ValidPredIdSet,
(
check_marker(Markers, marker_infer_type),
set_tree234.contains(ValidPredIdSet, PredId),
- \+ pred_info_get_goal_type(PredInfo, goal_type_promise(_))
+ not pred_info_is_promise(PredInfo, _)
->
Spec = construct_type_inference_message(PredInfo),
!:Specs = [Spec | !.Specs]
diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
index bc273f9..9c89355 100644
--- a/doc/reference_manual.texi
+++ b/doc/reference_manual.texi
@@ -3697,14 +3697,14 @@ And there are a variety of other applications.
@c it is the responsibility of the programmer to ensure overall correctness.
@c The behaviour of programs with incorrect laws is undefined.
@c
- at c A new law is introduced with the @samp{:- assertion} declaration.
+ at c A new law is introduced with the @samp{:- promise} declaration.
@c
- at c Here are some examples of @samp{:- assertion} declarations.
+ at c Here are some examples of @samp{:- promise} declarations.
@c The following example declares the function @samp{+} to be commutative.
@c
@c @example
- at c :- assertion
- at c all [A,B,R] (
+ at c :- promise all [A, B, R]
+ at c (
@c R = A + B
@c <=>
@c R = B + A
@@ -3720,11 +3720,11 @@ And there are a variety of other applications.
@c associative.
@c
@c @example
- at c :- assertion
- at c all [A,B,C,ABC] (
- at c (some [AB] (append(A, B, AB), append(AB, C, ABC)))
+ at c :- promise all [A, B, C, ABC]
+ at c (
+ at c ( some [AB] (append(A, B, AB), append(AB, C, ABC)) )
@c <=>
- at c (some [BC] (append(B, C, BC), append(A, BC, ABC)))
+ at c ( some [BC] (append(B, C, BC), append(A, BC, ABC)) )
@c ).
@c @end example
--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to: mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions: mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------
More information about the reviews
mailing list