[m-rev.] for review: promise_equivalent_solution_sets
Zoltan Somogyi
zs at cs.mu.OZ.AU
Tue Mar 21 11:33:16 AEDT 2006
For review by anyone. I am particularly looking for feedback on the
documentation and on whether we should keep the error named
nested_promise_eqv_solution_sets in det_report.m.
Zoltan.
Add a new goal form, as discussed on our mailing lists:
promise_equivalent_solution_sets [Vars] (
arbitrary [Vars1] Goal1,
arbitrary [Vars2] Goal2,
...
)
NEWS:
Mention the new goal form.
doc/reference_manual.texi:
Document the new goal form.
library/ops.m:
Add "promise_equivalent_solution_sets" and "arbitrary" as new
operators.
compiler/prog_item.m:
Add a parse_tree representation of new constructs.
Change the representation of goal forms in the parse tree to avoid
using punctuation marks as function symbols, to avoid function symbols
that need quoting, and to avoid ambiguity with hlds_goal_expr.
Delete the obsolete if_then (no else) goal form.
compiler/hlds_goal.m:
Provide a HLDS representation of the new constructs.
compiler/det_analysis.m:
Implement the rules for processing the new constructs.
compiler/det_report.m:
Implement the messages for the errors that can occur with the
new constructs.
Add quotes around `promise_equivalent_solutions' in an existing error
message, for consistency.
compiler/prog_io_goal.m:
Parse the new goal constructs.
compiler/add_clause.m:
compiler/hlds_out.m:
compiler/make_hlds_passes.m:
compiler/make_hlds_warn.m:
compiler/mercury_to_mercury.m:
compiler/module_qual.m:
compiler/pd_util.m:
compiler/prog_io.m:
compiler/prog_io_dcg.m:
compiler/prog_io_goal.m:
compiler/prog_util.m:
compiler/saved_vars.m:
compiler/simplify.m:
Conform to the changes to prog_item.m and hlds_goal.m.
tests/hard_coded/one_member.{m,exp}:
New test case to test the proper functioning of the new construct.
tests/invalid/one_member.{m,err_exp}:
New test case to test the kinds of errors that can occur when using
the new construct.
tests/hard_coded/Mmakefile:
tests/invalid/Mmakefile:
Enable the new test cases.
tests/invalid/promise_equivalent_solutions_test.err_exp:
Expect quotes around an old construct name, after the change to
det_report.m.
cvs diff: Diffing .
Index: NEWS
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/NEWS,v
retrieving revision 1.404
diff -u -b -r1.404 NEWS
--- NEWS 20 Mar 2006 06:13:33 -0000 1.404
+++ NEWS 20 Mar 2006 23:59:50 -0000
@@ -8,7 +8,7 @@
* The Mercury typeclass system now supports functional dependencies.
* A new language construct allows programmers to promise that any given
goal is pure or semipure.
-* A new language construct allows programmers to promise that all solutions
+* Two new language constructs allow programmers to promise that all solutions
of a given goal are equivalent with respect to the relevant equality
theories.
* We now have support for optional module initialisation and finalisation.
@@ -36,7 +36,7 @@
involving single-solution contexts.
* We have significantly improved the compiler's performance on predicates
with many clauses.
- * We have deleted the old --split-c-files option, as it conflicted with the
+* We have deleted the old --split-c-files option, as it conflicted with the
implementation of module initialisation and finalisation.
Portability Improvements:
@@ -114,6 +114,63 @@
promise_equivalent_solutions goal will be det if Goal is cc_multi,
and that the promise_equivalent_solutions goal will be semidet if Goal
is cc_nondet.
+
+ A related language construct allows programmers to promise that although
+ the solutions of a given goal are not necessarily equivalent with respect
+ to the relevant equality theories, it is nevertheless immaterial which one
+ is chosen in a particular context. The language construct is the `arbitrary'
+ goal, and The context is established by a `promise_equivalent_solution_sets'
+ goal. Consider a type representing maps from keys to values which is
+ implemented using 2-3 trees. In such a type, the precise shape of the tree
+ doesn't matter; two trees should be considered equal if they contain the same
+ set of keys and map them to the same values:
+
+ :- type tree23(K, V)
+ ---> two(tree23(K, V), K, V, tree23(K, V)
+ ; three(tree23(K, K, V, tree23(K, V), K, V, tree23(K, V))
+ where equality is tree23_equal
+ and comparison is tree23_compare.
+
+ Two values of e.g. type tree23(int, string) may differ in their top level
+ function symbol even through they denote the same map. Deconstructing a
+ value of such a type may therefore theoretically yield either "two" or
+ "three" as the top level function symbol, although in practice which one
+ you get is determined by the concrete structure of the term. Unifications
+ of such values with specific function symbols are therefore permitted only
+ in committed choice contexts. Unfortunately, one cannot simply put the
+ deconstruction into the scope of a promise_equivalent_solutions goal,
+ since the solutions are not equivalent in all contexts. However, the
+ solutions will be equivalent in *some* contexts. Consider this function
+ to count the number of key-value pairs in the map:
+
+ count(Tree) = Count :-
+ promise_equivalent_solution_sets [Count] (
+ (
+ arbitrary [Tree1, Tree2] (
+ Tree = two(Tree1, _Key, _Value, Tree2)
+ ),
+ Count = 1 + count(Tree1) + count(Tree2)
+ ;
+ arbitrary [Tree1, Tree2, Tree3] (
+ Tree = three(Tree1, _Key1, _Value1, Tree2,
+ _Key2, _Value2, Tree3)
+ ),
+ Count = 2 + count(Tree1) + count(Tree2) + count(Tree3)
+ )
+ ).
+
+ The construct `arbitrary [Tree1, Tree2] Goal', where Goal computes Tree1
+ and Tree2, tells the compiler that it is OK to commit to the first solution
+ of Goal, because regardless of whether the goal succeeds and if so with
+ which values of Tree1 and Tree2, the set of solutions of the surrounding
+ `promise_equivalent_solution_sets [Count] Goal' will not be affected.
+ Regardless of whether Tree is bound to "two" or "three", the body of count
+ will compute the right value for Count.
+
+ A goal of the form `arbitrary [Vars] Goal' will be det if Goal is cc_multi,
+ and it will be semidet if Goal is cc_nondet. Goals of that form may occur
+ only inside `promise_equivalent_solution_sets' goals. There is no restriction
+ on the determinism of `promise_equivalent_solution_sets' goals.
* We have added support for optional module initialisation. See the
"Module initialisation" section of the Mercury Language Reference
cvs diff: Diffing analysis
cvs diff: Diffing bindist
cvs diff: Diffing boehm_gc
cvs diff: Diffing boehm_gc/Mac_files
cvs diff: Diffing boehm_gc/cord
cvs diff: Diffing boehm_gc/cord/private
cvs diff: Diffing boehm_gc/doc
cvs diff: Diffing boehm_gc/include
cvs diff: Diffing boehm_gc/include/private
cvs diff: Diffing boehm_gc/tests
cvs diff: Diffing browser
cvs diff: Diffing bytecode
cvs diff: Diffing compiler
Index: compiler/add_clause.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/add_clause.m,v
retrieving revision 1.17
diff -u -b -r1.17 add_clause.m
--- compiler/add_clause.m 17 Mar 2006 01:40:10 -0000 1.17
+++ compiler/add_clause.m 20 Mar 2006 09:17:08 -0000
@@ -533,33 +533,35 @@
module_info::in, module_info::out, qual_info::in, qual_info::out,
svar_info::in, svar_info::out, io::di, io::uo) is det.
-transform_goal_2(fail, _, _, disj([]) - GoalInfo, !VarSet, !ModuleInfo,
+transform_goal_2(fail_expr, _, _, disj([]) - GoalInfo, !VarSet, !ModuleInfo,
!QualInfo, !SInfo, !IO) :-
goal_info_init(GoalInfo),
prepare_for_next_conjunct(set.init, !VarSet, !SInfo).
-transform_goal_2(true, _, _, conj(plain_conj, []) - GoalInfo, !VarSet,
+transform_goal_2(true_expr, _, _, conj(plain_conj, []) - GoalInfo, !VarSet,
!ModuleInfo, !QualInfo, !SInfo, !IO) :-
goal_info_init(GoalInfo),
prepare_for_next_conjunct(set.init, !VarSet, !SInfo).
-transform_goal_2(all(Vars0, Goal0), Context, Subst, Goal, !VarSet, !ModuleInfo,
- !QualInfo, !SInfo, !IO) :-
+transform_goal_2(all_expr(Vars0, Goal0), Context, Subst, Goal, !VarSet,
+ !ModuleInfo, !QualInfo, !SInfo, !IO) :-
% Convert `all [Vars] Goal' into `not some [Vars] not Goal'.
- TransformedGoal = not(some(Vars0, not(Goal0) - Context) - Context),
+ TransformedGoal = not_expr(some_expr(Vars0, not_expr(Goal0) - Context)
+ - Context),
transform_goal_2(TransformedGoal, Context, Subst, Goal, !VarSet,
!ModuleInfo, !QualInfo, !SInfo, !IO).
-transform_goal_2(all_state_vars(StateVars, Goal0), Context, Subst,
+transform_goal_2(all_state_vars_expr(StateVars, Goal0), Context, Subst,
Goal, !VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO) :-
transform_goal_2(
- not(some_state_vars(StateVars, not(Goal0) - Context) - Context),
+ not_expr(some_state_vars_expr(StateVars,
+ not_expr(Goal0) - Context) - Context),
Context, Subst, Goal, !VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO).
-transform_goal_2(some(Vars0, Goal0), _, Subst,
+transform_goal_2(some_expr(Vars0, Goal0), _, Subst,
scope(exist_quant(Vars), Goal) - GoalInfo,
!VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO) :-
substitute_vars(Vars0, Subst, Vars),
transform_goal(Goal0, Subst, Goal, !VarSet, !ModuleInfo, !QualInfo,
!SInfo, !IO),
goal_info_init(GoalInfo).
-transform_goal_2(some_state_vars(StateVars0, Goal0), _, Subst,
+transform_goal_2(some_state_vars_expr(StateVars0, Goal0), _, Subst,
scope(exist_quant(Vars), Goal) - GoalInfo,
!VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO) :-
BeforeSInfo = !.SInfo,
@@ -569,29 +571,43 @@
!SInfo, !IO),
finish_local_state_vars(StateVars, Vars, BeforeSInfo, !SInfo),
goal_info_init(GoalInfo).
-transform_goal_2(promise_purity(Implicit, Purity, Goal0), _, Subst,
+transform_goal_2(promise_purity_expr(Implicit, Purity, Goal0), _, Subst,
scope(promise_purity(Implicit, Purity), Goal) - GoalInfo,
!VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO) :-
transform_goal(Goal0, Subst, Goal, !VarSet, !ModuleInfo, !QualInfo,
!SInfo, !IO),
goal_info_init(GoalInfo).
transform_goal_2(
- promise_equivalent_solutions(Vars0, DotSVars0, ColonSVars0, Goal0),
+ promise_equivalent_solutions_expr(Vars0, DotSVars0, ColonSVars0,
+ Goal0),
Context, Subst,
scope(promise_solutions(Vars, equivalent_solutions), Goal) - GoalInfo,
!VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO) :-
- substitute_vars(Vars0, Subst, Vars1),
- substitute_vars(DotSVars0, Subst, DotSVars1),
- convert_dot_state_vars(Context, DotSVars1, DotSVars, !VarSet, !SInfo, !IO),
- transform_goal(Goal0, Subst, Goal, !VarSet, !ModuleInfo, !QualInfo,
- !SInfo, !IO),
- goal_info_init(GoalInfo),
- substitute_vars(ColonSVars0, Subst, ColonSVars1),
- convert_dot_state_vars(Context, ColonSVars1, ColonSVars, !VarSet,
- !SInfo, !IO),
- Vars = Vars1 ++ DotSVars ++ ColonSVars.
-transform_goal_2(if_then_else(Vars0, StateVars0, Cond0, Then0, Else0), Context,
- Subst, if_then_else(Vars, Cond, Then, Else) - GoalInfo,
+ transform_promise_eqv_goal(Vars0, DotSVars0, ColonSVars0, Subst, Context,
+ Vars, Goal0, Goal, GoalInfo, !VarSet, !ModuleInfo, !QualInfo, !SInfo,
+ !IO).
+transform_goal_2(
+ promise_equivalent_solution_sets_expr(Vars0, DotSVars0, ColonSVars0,
+ Goal0),
+ Context, Subst,
+ scope(promise_solutions(Vars, equivalent_solution_sets), Goal)
+ - GoalInfo,
+ !VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO) :-
+ transform_promise_eqv_goal(Vars0, DotSVars0, ColonSVars0, Subst, Context,
+ Vars, Goal0, Goal, GoalInfo, !VarSet, !ModuleInfo, !QualInfo, !SInfo,
+ !IO).
+transform_goal_2(
+ promise_equivalent_solution_arbitrary_expr(Vars0,
+ DotSVars0, ColonSVars0, Goal0),
+ Context, Subst,
+ scope(promise_solutions(Vars, equivalent_solution_sets_arbitrary),
+ Goal) - GoalInfo,
+ !VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO) :-
+ transform_promise_eqv_goal(Vars0, DotSVars0, ColonSVars0, Subst, Context,
+ Vars, Goal0, Goal, GoalInfo, !VarSet, !ModuleInfo, !QualInfo, !SInfo,
+ !IO).
+transform_goal_2(if_then_else_expr(Vars0, StateVars0, Cond0, Then0, Else0),
+ Context, Subst, if_then_else(Vars, Cond, Then, Else) - GoalInfo,
!VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO) :-
BeforeSInfo = !.SInfo,
substitute_vars(Vars0, Subst, Vars),
@@ -610,20 +626,15 @@
goal_info_init(Context, GoalInfo),
finish_if_then_else(Context, Then1, Then, Else1, Else,
BeforeSInfo, AfterCondSInfo, AfterThenSInfo, !SInfo, !VarSet).
-transform_goal_2(if_then(Vars0, StateVars, A0, B0), Context, Subst,
- Goal, !VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO) :-
- transform_goal_2(
- if_then_else(Vars0, StateVars, A0, B0, true - Context),
- Context, Subst, Goal, !VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO).
-transform_goal_2(not(A0), _, Subst, Goal, !VarSet, !ModuleInfo, !QualInfo,
+transform_goal_2(not_expr(A0), _, Subst, Goal, !VarSet, !ModuleInfo, !QualInfo,
!SInfo, !IO) :-
BeforeSInfo = !.SInfo,
transform_goal(A0, Subst, A, !VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO),
goal_info_init(GoalInfo),
Goal = not(A) - GoalInfo,
finish_negation(BeforeSInfo, !SInfo).
-transform_goal_2((A0, B0), _, Subst, Goal, !VarSet, !ModuleInfo, !QualInfo,
- !SInfo, !IO) :-
+transform_goal_2(conj_expr(A0, B0), _, Subst, Goal, !VarSet, !ModuleInfo,
+ !QualInfo, !SInfo, !IO) :-
get_rev_conj(A0, Subst, [], R0, !VarSet, !ModuleInfo, !QualInfo,
!SInfo, !IO),
get_rev_conj(B0, Subst, R0, R, !VarSet, !ModuleInfo, !QualInfo,
@@ -631,8 +642,8 @@
L = list.reverse(R),
goal_info_init(GoalInfo),
conj_list_to_goal(L, GoalInfo, Goal).
-transform_goal_2((A0 & B0), _, Subst, Goal, !VarSet, !ModuleInfo, !QualInfo,
- !SInfo, !IO) :-
+transform_goal_2(par_conj_expr(A0, B0), _, Subst, Goal, !VarSet, !ModuleInfo,
+ !QualInfo, !SInfo, !IO) :-
get_rev_par_conj(B0, Subst, [], R0, !VarSet, !ModuleInfo, !QualInfo,
!SInfo, !IO),
get_rev_par_conj(A0, Subst, R0, R, !VarSet, !ModuleInfo, !QualInfo,
@@ -640,20 +651,20 @@
L = list.reverse(R),
goal_info_init(GoalInfo),
par_conj_list_to_goal(L, GoalInfo, Goal).
-transform_goal_2((A0 ; B0), Context, Subst, Goal, !VarSet, !ModuleInfo,
+transform_goal_2(disj_expr(A0, B0), Context, Subst, Goal, !VarSet, !ModuleInfo,
!QualInfo, !SInfo, !IO) :-
get_disj(B0, Subst, [], L0, !VarSet, !ModuleInfo, !QualInfo, !.SInfo, !IO),
get_disj(A0, Subst, L0, L1, !VarSet, !ModuleInfo, !QualInfo, !.SInfo, !IO),
finish_disjunction(Context, !.VarSet, L1, L, !:SInfo),
goal_info_init(Context, GoalInfo),
disj_list_to_goal(L, GoalInfo, Goal).
-transform_goal_2(implies(P, Q), Context, Subst, Goal, !VarSet, !ModuleInfo,
- !QualInfo, !SInfo, !IO) :-
+transform_goal_2(implies_expr(P, Q), Context, Subst, Goal, !VarSet,
+ !ModuleInfo, !QualInfo, !SInfo, !IO) :-
% `P => Q' is defined as `not (P, not Q)'
- TransformedGoal = not( (P, not(Q) - Context) - Context ),
+ TransformedGoal = not_expr(conj_expr(P, not_expr(Q) - Context) - Context),
transform_goal_2(TransformedGoal, Context, Subst, Goal, !VarSet,
!ModuleInfo, !QualInfo, !SInfo, !IO).
-transform_goal_2(equivalent(P0, Q0), _, Subst, Goal, !VarSet, !ModuleInfo,
+transform_goal_2(equivalent_expr(P0, Q0), _, Subst, Goal, !VarSet, !ModuleInfo,
!QualInfo, !SInfo, !IO) :-
%
% `P <=> Q' is defined as `(P => Q), (Q => P)',
@@ -668,7 +679,7 @@
transform_goal(Q0, Subst, Q, !VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO),
Goal = shorthand(bi_implication(P, Q)) - GoalInfo,
finish_equivalence(BeforeSInfo, !SInfo).
-transform_goal_2(call(Name, Args0, Purity), Context, Subst, Goal, !VarSet,
+transform_goal_2(call_expr(Name, Args0, Purity), Context, Subst, Goal, !VarSet,
!ModuleInfo, !QualInfo, !SInfo, !IO) :-
Args1 = expand_bang_state_var_args(Args0),
(
@@ -677,8 +688,9 @@
->
prepare_for_call(!SInfo),
% `LHS \= RHS' is defined as `not (LHS = RHS)'
- transform_goal_2(not(unify(LHS, RHS, Purity) - Context), Context,
- Subst, Goal, !VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO),
+ transform_goal_2(not_expr(unify_expr(LHS, RHS, Purity) - Context),
+ Context, Subst, Goal, !VarSet, !ModuleInfo, !QualInfo, !SInfo,
+ !IO),
finish_call(!VarSet, !SInfo)
;
% check for a DCG field access goal:
@@ -734,7 +746,7 @@
Goal0, Goal, !VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO),
finish_call(!VarSet, !SInfo)
).
-transform_goal_2(unify(A0, B0, Purity), Context, Subst, Goal, !VarSet,
+transform_goal_2(unify_expr(A0, B0, Purity), Context, Subst, Goal, !VarSet,
!ModuleInfo, !QualInfo, !SInfo, !IO) :-
% It is an error for the left or right hand side of a
% unification to be !X (it may be !.X or !:X, however).
@@ -753,6 +765,26 @@
finish_call(!VarSet, !SInfo)
).
+:- pred transform_promise_eqv_goal(prog_vars::in, prog_vars::in, prog_vars::in,
+ prog_substitution::in, prog_context::in, prog_vars::out,
+ goal::in, hlds_goal::out, hlds_goal_info::out,
+ prog_varset::in, prog_varset::out, module_info::in, module_info::out,
+ qual_info::in, qual_info::out, svar_info::in, svar_info::out,
+ io::di, io::uo) is det.
+
+transform_promise_eqv_goal(Vars0, DotSVars0, ColonSVars0, Subst, Context, Vars,
+ Goal0, Goal, GoalInfo, !VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO) :-
+ substitute_vars(Vars0, Subst, Vars1),
+ substitute_vars(DotSVars0, Subst, DotSVars1),
+ convert_dot_state_vars(Context, DotSVars1, DotSVars, !VarSet, !SInfo, !IO),
+ transform_goal(Goal0, Subst, Goal, !VarSet, !ModuleInfo, !QualInfo,
+ !SInfo, !IO),
+ goal_info_init(GoalInfo),
+ substitute_vars(ColonSVars0, Subst, ColonSVars1),
+ convert_dot_state_vars(Context, ColonSVars1, ColonSVars, !VarSet,
+ !SInfo, !IO),
+ Vars = Vars1 ++ DotSVars ++ ColonSVars.
+
:- pred convert_dot_state_vars(prog_context::in, prog_vars::in, prog_vars::out,
prog_varset::in, prog_varset::out, svar_info::in, svar_info::out,
io::di, io::uo) is det.
@@ -963,7 +995,7 @@
get_rev_conj(Goal, Subst, RevConj0, RevConj, !VarSet, !ModuleInfo, !QualInfo,
!SInfo, !IO) :-
- ( Goal = (A,B) - _Context ->
+ ( Goal = conj_expr(A, B) - _Context ->
get_rev_conj(A, Subst, RevConj0, RevConj1,
!VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO),
get_rev_conj(B, Subst, RevConj1, RevConj,
@@ -987,7 +1019,7 @@
get_rev_par_conj(Goal, Subst, RevParConj0, RevParConj, !VarSet, !ModuleInfo,
!QualInfo, !SInfo, !IO) :-
- ( Goal = (A & B) - _Context ->
+ ( Goal = par_conj_expr(A, B) - _Context ->
get_rev_par_conj(A, Subst, RevParConj0, RevParConj1,
!VarSet, !ModuleInfo, !QualInfo, !SInfo, !IO),
get_rev_par_conj(B, Subst, RevParConj1, RevParConj,
@@ -1011,7 +1043,7 @@
get_disj(Goal, Subst, Disj0, Disj, !VarSet, !ModuleInfo, !QualInfo, SInfo,
!IO) :-
- ( Goal = (A;B) - _Context ->
+ ( Goal = disj_expr(A, B) - _Context ->
get_disj(B, Subst, Disj0, Disj1, !VarSet, !ModuleInfo, !QualInfo,
SInfo, !IO),
get_disj(A, Subst, Disj1, Disj, !VarSet, !ModuleInfo, !QualInfo,
Index: compiler/det_analysis.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/det_analysis.m,v
retrieving revision 1.188
diff -u -b -r1.188 det_analysis.m
--- compiler/det_analysis.m 24 Feb 2006 07:11:09 -0000 1.188
+++ compiler/det_analysis.m 20 Mar 2006 11:20:23 -0000
@@ -60,6 +60,7 @@
:- import_module io.
:- import_module list.
+:- import_module std_util.
%-----------------------------------------------------------------------------%
@@ -81,14 +82,17 @@
module_info::out, globals::in, determinism::out, determinism::out,
list(context_det_msg)::out) is det.
+:- type pess_info % short for promise_equivalent_solution_sets_info
+ ---> pess_info(prog_vars, prog_context).
+
% Infers the determinism of `Goal0' and returns this in `Detism'.
% It annotates the goal and all its subgoals with their determinism
% and returns the annotated goal in `Goal'.
%
:- pred det_infer_goal(hlds_goal::in, hlds_goal::out, instmap::in,
- soln_context::in, list(failing_context)::in, det_info::in,
- determinism::out, list(failing_context)::out, list(context_det_msg)::out)
- is det.
+ soln_context::in, list(failing_context)::in, maybe(pess_info)::in,
+ det_info::in, determinism::out,
+ list(failing_context)::out, list(context_det_msg)::out) is det.
% Work out how many solutions are needed for a given determinism.
%
@@ -122,7 +126,6 @@
:- import_module bool.
:- import_module map.
:- import_module set.
-:- import_module std_util.
:- import_module string.
:- import_module term.
@@ -256,7 +259,7 @@
proc_info_get_initial_instmap(Proc0, !.ModuleInfo, InstMap0),
proc_info_vartypes(Proc0, VarTypes),
det_info_init(!.ModuleInfo, VarTypes, PredId, ProcId, Globals, DetInfo),
- det_infer_goal(Goal0, Goal, InstMap0, SolnContext, [], DetInfo,
+ det_infer_goal(Goal0, Goal, InstMap0, SolnContext, [], no, DetInfo,
InferDetism, _, !:Msgs),
% Take the worst of the old and inferred detisms. This is needed to prevent
@@ -342,7 +345,8 @@
%-----------------------------------------------------------------------------%
det_infer_goal(Goal0 - GoalInfo0, Goal - GoalInfo, InstMap0, !.SolnContext,
- RightFailingContexts, DetInfo, Detism, GoalFailingContexts, !:Msgs) :-
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo, Detism,
+ GoalFailingContexts, !:Msgs) :-
goal_info_get_nonlocals(GoalInfo0, NonLocalVars),
goal_info_get_instmap_delta(GoalInfo0, InstmapDelta),
@@ -377,7 +381,8 @@
% relevant equality theory, we want to prune away all but one
% of those solutions.
- ScopeReason = promise_solutions(_, _)
+ ScopeReason = promise_solutions(_, PromiseEqvSolnsKind),
+ promise_eqv_solutions_kind_prunes(PromiseEqvSolnsKind) = yes
)
->
Prune = yes
@@ -386,8 +391,8 @@
),
det_infer_goal_2(Goal0, Goal1, GoalInfo0, InstMap0, !.SolnContext,
- RightFailingContexts, DetInfo, InternalDetism0, GoalFailingContexts,
- !:Msgs),
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo,
+ InternalDetism0, GoalFailingContexts, !:Msgs),
determinism_components(InternalDetism0, InternalCanFail, InternalSolns0),
(
@@ -483,15 +488,23 @@
Goal = Goal1
).
+:- func promise_eqv_solutions_kind_prunes(promise_solutions_kind) = bool.
+
+promise_eqv_solutions_kind_prunes(equivalent_solutions) = yes.
+promise_eqv_solutions_kind_prunes(equivalent_solution_sets) = no.
+promise_eqv_solutions_kind_prunes(equivalent_solution_sets_arbitrary) = yes.
+
%-----------------------------------------------------------------------------%
:- pred det_infer_goal_2(hlds_goal_expr::in, hlds_goal_expr::out,
hlds_goal_info::in, instmap::in, soln_context::in,
- list(failing_context)::in, det_info::in, determinism::out,
- list(failing_context)::out, list(context_det_msg)::out) is det.
+ list(failing_context)::in, maybe(pess_info)::in, det_info::in,
+ determinism::out, list(failing_context)::out, list(context_det_msg)::out)
+ is det.
det_infer_goal_2(GoalExpr0, GoalExpr, GoalInfo, InstMap0, SolnContext,
- RightFailingContexts, DetInfo, Detism, GoalFailingContexts, !:Msgs) :-
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo, Detism,
+ GoalFailingContexts, !:Msgs) :-
(
GoalExpr0 = conj(ConjType, Goals0),
(
@@ -499,38 +512,38 @@
% The determinism of a conjunction is the worst case of the
% determinism of the goals of that conjuction.
det_infer_conj(Goals0, Goals, InstMap0, SolnContext,
- RightFailingContexts, DetInfo, Detism, [], GoalFailingContexts,
- !:Msgs)
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo,
+ Detism, [], GoalFailingContexts, !:Msgs)
;
ConjType = parallel_conj,
det_infer_par_conj(Goals0, Goals, GoalInfo, InstMap0, SolnContext,
- RightFailingContexts, DetInfo, Detism, GoalFailingContexts,
- !:Msgs)
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo,
+ Detism, GoalFailingContexts, !:Msgs)
),
GoalExpr = conj(ConjType, Goals)
;
GoalExpr0 = disj(Goals0),
det_infer_disj(Goals0, Goals, GoalInfo, InstMap0, SolnContext,
- RightFailingContexts, DetInfo, Detism, GoalFailingContexts,
- !:Msgs),
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo,
+ Detism, GoalFailingContexts, !:Msgs),
GoalExpr = disj(Goals)
;
GoalExpr0 = switch(Var, SwitchCanFail, Cases0),
det_infer_switch(Var, SwitchCanFail, Cases0, Cases, GoalInfo, InstMap0,
- SolnContext, RightFailingContexts, DetInfo, Detism,
- GoalFailingContexts, !:Msgs),
+ SolnContext, RightFailingContexts, MaybePromiseEqvSolutionSets,
+ DetInfo, Detism, GoalFailingContexts, !:Msgs),
GoalExpr = switch(Var, SwitchCanFail, Cases)
;
GoalExpr0 = call(PredId, ProcId0, Args, Builtin, UnifyContext, Name),
det_infer_call(PredId, ProcId0, ProcId, GoalInfo, SolnContext,
- RightFailingContexts, DetInfo, Detism, GoalFailingContexts,
- !:Msgs),
+ RightFailingContexts, DetInfo,
+ Detism, GoalFailingContexts, !:Msgs),
GoalExpr = call(PredId, ProcId, Args, Builtin, UnifyContext, Name)
;
GoalExpr0 = generic_call(GenericCall, _ArgVars, _Modes, CallDetism),
det_infer_generic_call(GenericCall, CallDetism, GoalInfo, SolnContext,
- RightFailingContexts, DetInfo, Detism, GoalFailingContexts,
- !:Msgs),
+ RightFailingContexts, DetInfo,
+ Detism, GoalFailingContexts, !:Msgs),
GoalExpr = GoalExpr0
;
GoalExpr0 = unify(LHS, RHS0, Mode, Unify, UnifyContext),
@@ -541,19 +554,21 @@
;
GoalExpr0 = if_then_else(Vars, Cond0, Then0, Else0),
det_infer_if_then_else(Cond0, Cond, Then0, Then, Else0, Else,
- InstMap0, SolnContext, RightFailingContexts, DetInfo, Detism,
+ InstMap0, SolnContext, RightFailingContexts,
+ MaybePromiseEqvSolutionSets, DetInfo, Detism,
GoalFailingContexts, !:Msgs),
GoalExpr = if_then_else(Vars, Cond, Then, Else)
;
GoalExpr0 = not(Goal0),
- det_infer_not(Goal0, Goal, GoalInfo, InstMap0, DetInfo, Detism,
+ det_infer_not(Goal0, Goal, GoalInfo, InstMap0,
+ MaybePromiseEqvSolutionSets, DetInfo, Detism,
GoalFailingContexts, !:Msgs),
GoalExpr = not(Goal)
;
GoalExpr0 = scope(Reason, Goal0),
det_infer_scope(Reason, Goal0, Goal, GoalInfo, InstMap0, SolnContext,
- RightFailingContexts, DetInfo, Detism, GoalFailingContexts,
- !:Msgs),
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo,
+ Detism, GoalFailingContexts, !:Msgs),
GoalExpr = scope(Reason, Goal)
;
GoalExpr0 = foreign_proc(Attributes, PredId, ProcId, _Args, _ExtraArgs,
@@ -571,14 +586,15 @@
%-----------------------------------------------------------------------------%
:- pred det_infer_conj(list(hlds_goal)::in, list(hlds_goal)::out, instmap::in,
- soln_context::in, list(failing_context)::in, det_info::in,
- determinism::out, list(failing_context)::in, list(failing_context)::out,
- list(context_det_msg)::out) is det.
+ soln_context::in, list(failing_context)::in, maybe(pess_info)::in,
+ det_info::in, determinism::out, list(failing_context)::in,
+ list(failing_context)::out, list(context_det_msg)::out) is det.
det_infer_conj([], [], _InstMap0, _SolnContext, _RightFailingContexts,
- _DetInfo, det, !ConjFailingContexts, []).
+ _MaybePromiseEqvSolutionSets, _DetInfo, det, !ConjFailingContexts, []).
det_infer_conj([Goal0 | Goals0], [Goal | Goals], InstMap0, SolnContext,
- RightFailingContexts, DetInfo, Detism, !ConjFailingContexts, Msgs) :-
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo, Detism,
+ !ConjFailingContexts, Msgs) :-
% We should look to see when we get to a not_reached point
% and optimize away the remaining elements of the conjunction.
% But that optimization is done in the code generator anyway.
@@ -589,8 +605,8 @@
% First, process the second and subsequent conjuncts.
update_instmap(Goal0, InstMap0, InstMap1),
det_infer_conj(Goals0, Goals, InstMap1, SolnContext,
- RightFailingContexts, DetInfo, TailDetism, !ConjFailingContexts,
- TailMsgs),
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo,
+ TailDetism, !ConjFailingContexts, TailMsgs),
determinism_components(TailDetism, TailCanFail, _TailMaxSolns),
% Next, work out whether the first conjunct is in a first_soln context
@@ -608,7 +624,8 @@
),
% Process the first conjunct.
det_infer_goal(Goal0, Goal, InstMap0, HeadSolnContext,
- !.ConjFailingContexts ++ RightFailingContexts, DetInfo, HeadDetism,
+ !.ConjFailingContexts ++ RightFailingContexts,
+ MaybePromiseEqvSolutionSets, DetInfo, HeadDetism,
GoalFailingContexts, HeadMsgs),
% Finally combine the results computed above.
@@ -618,14 +635,16 @@
:- pred det_infer_par_conj(list(hlds_goal)::in, list(hlds_goal)::out,
hlds_goal_info::in, instmap::in, soln_context::in,
- list(failing_context)::in, det_info::in, determinism::out,
- list(failing_context)::out, list(context_det_msg)::out) is det.
+ list(failing_context)::in, maybe(pess_info)::in, det_info::in,
+ determinism::out, list(failing_context)::out, list(context_det_msg)::out)
+ is det.
det_infer_par_conj(Goals0, Goals, GoalInfo, InstMap0, SolnContext,
- RightFailingContexts, DetInfo, Detism, GoalFailingContexts, !:Msgs) :-
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo,
+ Detism, GoalFailingContexts, !:Msgs) :-
det_infer_par_conj_goals(Goals0, Goals, InstMap0, SolnContext,
- RightFailingContexts, DetInfo, Detism, [], GoalFailingContexts,
- !:Msgs),
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo,
+ Detism, [], GoalFailingContexts, !:Msgs),
(
determinism_components(Detism, CanFail, Solns),
CanFail = cannot_fail,
@@ -642,22 +661,25 @@
).
:- pred det_infer_par_conj_goals(list(hlds_goal)::in, list(hlds_goal)::out,
- instmap::in, soln_context::in, list(failing_context)::in, det_info::in,
- determinism::out, list(failing_context)::in, list(failing_context)::out,
+ instmap::in, soln_context::in, list(failing_context)::in,
+ maybe(pess_info)::in, det_info::in, determinism::out,
+ list(failing_context)::in, list(failing_context)::out,
list(context_det_msg)::out) is det.
-det_infer_par_conj_goals([], [], _InstMap0, _SolnContext, _RightFailingContexts,
- _DetInfo, det, !ConjFailingContexts, []).
+det_infer_par_conj_goals([], [], _InstMap0, _SolnContext,
+ _RightFailingContexts, _MaybePromiseEqvSolutionSets, _DetInfo,
+ det, !ConjFailingContexts, []).
det_infer_par_conj_goals([Goal0 | Goals0], [Goal | Goals], InstMap0,
- SolnContext, RightFailingContexts, DetInfo, Detism,
- !ConjFailingContexts, Msgs) :-
+ SolnContext, RightFailingContexts, MaybePromiseEqvSolutionSets,
+ DetInfo, Detism, !ConjFailingContexts, Msgs) :-
det_infer_goal(Goal0, Goal, InstMap0, SolnContext, RightFailingContexts,
- DetInfo, HeadDetism, GoalFailingContexts, HeadMsgs),
+ MaybePromiseEqvSolutionSets, DetInfo, HeadDetism, GoalFailingContexts,
+ HeadMsgs),
determinism_components(HeadDetism, HeadCanFail, HeadMaxSolns),
det_infer_par_conj_goals(Goals0, Goals, InstMap0, SolnContext,
- RightFailingContexts, DetInfo, TailDetism, !ConjFailingContexts,
- TailMsgs),
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo,
+ TailDetism, !ConjFailingContexts, TailMsgs),
determinism_components(TailDetism, TailCanFail, TailMaxSolns),
det_conjunction_maxsoln(HeadMaxSolns, TailMaxSolns, MaxSolns),
@@ -668,14 +690,16 @@
:- pred det_infer_disj(list(hlds_goal)::in, list(hlds_goal)::out,
hlds_goal_info::in, instmap::in, soln_context::in,
- list(failing_context)::in, det_info::in, determinism::out,
- list(failing_context)::out, list(context_det_msg)::out) is det.
+ list(failing_context)::in, maybe(pess_info)::in, det_info::in,
+ determinism::out, list(failing_context)::out, list(context_det_msg)::out)
+ is det.
det_infer_disj(Goals0, Goals, GoalInfo, InstMap0, SolnContext,
- RightFailingContexts, DetInfo, Detism, GoalFailingContexts, !:Msgs) :-
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo,
+ Detism, GoalFailingContexts, !:Msgs) :-
det_infer_disj_goals(Goals0, Goals, InstMap0, SolnContext,
- RightFailingContexts, DetInfo, can_fail, at_most_zero, Detism,
- [], GoalFailingContexts0, !:Msgs),
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo,
+ can_fail, at_most_zero, Detism, [], GoalFailingContexts0, !:Msgs),
(
Goals = [],
goal_info_get_context(GoalInfo, Context),
@@ -686,19 +710,21 @@
).
:- pred det_infer_disj_goals(list(hlds_goal)::in, list(hlds_goal)::out,
- instmap::in, soln_context::in, list(failing_context)::in, det_info::in,
- can_fail::in, soln_count::in, determinism::out,
- list(failing_context)::in, list(failing_context)::out,
+ instmap::in, soln_context::in, list(failing_context)::in,
+ maybe(pess_info)::in, det_info::in, can_fail::in, soln_count::in,
+ determinism::out, list(failing_context)::in, list(failing_context)::out,
list(context_det_msg)::out) is det.
det_infer_disj_goals([], [], _InstMap0, _SolnContext, _RightFailingContexts,
- _DetInfo, CanFail, MaxSolns, Detism, !DisjFailingContexts, []) :-
+ _MaybePromiseEqvSolutionSets, _DetInfo, CanFail, MaxSolns, Detism,
+ !DisjFailingContexts, []) :-
determinism_components(Detism, CanFail, MaxSolns).
det_infer_disj_goals([Goal0 | Goals0], [Goal | Goals], InstMap0, SolnContext,
- RightFailingContexts, DetInfo, !.CanFail, !.MaxSolns, Detism,
- !DisjFailingContexts, Msgs) :-
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo,
+ !.CanFail, !.MaxSolns, Detism, !DisjFailingContexts, Msgs) :-
det_infer_goal(Goal0, Goal, InstMap0, SolnContext, RightFailingContexts,
- DetInfo, FirstDetism, GoalFailingContexts, FirstMsgs),
+ MaybePromiseEqvSolutionSets, DetInfo, FirstDetism, GoalFailingContexts,
+ FirstMsgs),
determinism_components(FirstDetism, FirstCanFail, FirstMaxSolns),
Goal = _ - GoalInfo,
% If a disjunct cannot succeed but is marked with the
@@ -733,8 +759,8 @@
true
),
det_infer_disj_goals(Goals0, Goals, InstMap0, SolnContext,
- RightFailingContexts, DetInfo, !.CanFail, !.MaxSolns, Detism,
- !DisjFailingContexts, LaterMsgs),
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo,
+ !.CanFail, !.MaxSolns, Detism, !DisjFailingContexts, LaterMsgs),
!:DisjFailingContexts = GoalFailingContexts ++ !.DisjFailingContexts,
Msgs = FirstMsgs ++ LaterMsgs.
@@ -743,20 +769,22 @@
:- pred det_infer_switch(prog_var::in, can_fail::in,
list(case)::in, list(case)::out,
hlds_goal_info::in, instmap::in, soln_context::in,
- list(failing_context)::in, det_info::in, determinism::out,
- list(failing_context)::out, list(context_det_msg)::out) is det.
+ list(failing_context)::in, maybe(pess_info)::in, det_info::in,
+ determinism::out, list(failing_context)::out, list(context_det_msg)::out)
+ is det.
det_infer_switch(Var, SwitchCanFail, Cases0, Cases, GoalInfo, InstMap0,
- SolnContext, RightFailingContexts, DetInfo, Detism,
- GoalFailingContexts, !:Msgs) :-
+ SolnContext, RightFailingContexts, MaybePromiseEqvSolutionSets,
+ DetInfo, Detism, GoalFailingContexts, !:Msgs) :-
% The determinism of a switch is the worst of the determinism of each
% of the cases. Also, if only a subset of the constructors are handled,
% then it is semideterministic or worse - this is determined
% in switch_detection.m and handled via the SwitchCanFail field.
det_infer_switch_cases(Cases0, Cases, InstMap0, SolnContext,
- RightFailingContexts, DetInfo, cannot_fail, at_most_zero,
- CasesDetism, [], GoalFailingContexts0, !:Msgs),
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo,
+ cannot_fail, at_most_zero, CasesDetism, [], GoalFailingContexts0,
+ !:Msgs),
determinism_components(CasesDetism, CasesCanFail, CasesSolns),
% The switch variable tests are in a first_soln context if and only
% if the switch goal as a whole was in a first_soln context and the
@@ -787,30 +815,32 @@
).
:- pred det_infer_switch_cases(list(case)::in, list(case)::out, instmap::in,
- soln_context::in, list(failing_context)::in, det_info::in, can_fail::in,
- soln_count::in, determinism::out,
+ soln_context::in, list(failing_context)::in, maybe(pess_info)::in,
+ det_info::in, can_fail::in, soln_count::in, determinism::out,
list(failing_context)::in, list(failing_context)::out,
list(context_det_msg)::out) is det.
det_infer_switch_cases([], [], _InstMap0, _SolnContext, _RightFailingContexts,
- _DetInfo, CanFail, MaxSolns, Detism, !SwitchFailingContexts, []) :-
+ _MaybePromiseEqvSolutionSets, _DetInfo, CanFail, MaxSolns,
+ Detism, !SwitchFailingContexts, []) :-
determinism_components(Detism, CanFail, MaxSolns).
det_infer_switch_cases([Case0 | Cases0], [Case | Cases], InstMap0, SolnContext,
- RightFailingContexts, DetInfo, !.CanFail, !.MaxSolns, Detism,
- !SwitchFailingContexts, Msgs) :-
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo,
+ !.CanFail, !.MaxSolns, Detism, !SwitchFailingContexts, Msgs) :-
% Technically, we should update the instmap to reflect the knowledge that
% the var is bound to this particular constructor, but we wouldn't use
% that information here anyway, so we don't bother.
Case0 = case(ConsId, Goal0),
det_infer_goal(Goal0, Goal, InstMap0, SolnContext, RightFailingContexts,
- DetInfo, FirstDetism, GoalFailingContexts, FirstMsgs),
+ MaybePromiseEqvSolutionSets, DetInfo, FirstDetism, GoalFailingContexts,
+ FirstMsgs),
Case = case(ConsId, Goal),
determinism_components(FirstDetism, FirstCanFail, FirstMaxSolns),
det_switch_canfail(!.CanFail, FirstCanFail, !:CanFail),
det_switch_maxsoln(!.MaxSolns, FirstMaxSolns, !:MaxSolns),
det_infer_switch_cases(Cases0, Cases, InstMap0, SolnContext,
- RightFailingContexts, DetInfo, !.CanFail, !.MaxSolns, Detism,
- !SwitchFailingContexts, LaterMsgs),
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo,
+ !.CanFail, !.MaxSolns, Detism, !SwitchFailingContexts, LaterMsgs),
!:SwitchFailingContexts = GoalFailingContexts ++ !.SwitchFailingContexts,
Msgs = FirstMsgs ++ LaterMsgs.
@@ -821,9 +851,8 @@
list(failing_context)::in, det_info::in, determinism::out,
list(failing_context)::out, list(context_det_msg)::out) is det.
-det_infer_call(PredId, ProcId0, ProcId, GoalInfo,
- SolnContext, RightFailingContexts, DetInfo, Detism,
- GoalFailingContexts, !:Msgs) :-
+det_infer_call(PredId, ProcId0, ProcId, GoalInfo, SolnContext,
+ RightFailingContexts, DetInfo, Detism, GoalFailingContexts, !:Msgs) :-
% For calls, just look up the determinism entry associated with
% the called predicate.
% This is the point at which annotations start changing
@@ -932,8 +961,7 @@
Detism0 = erroneous
->
proc_info_context(ProcInfo, ProcContext),
- WillNotThrowMsg =
- will_not_throw_with_erroneous(PredId, ProcId),
+ WillNotThrowMsg = will_not_throw_with_erroneous(PredId, ProcId),
WillNotThrowContextMsg =
context_det_msg(ProcContext, WillNotThrowMsg),
!:Msgs = [WillNotThrowContextMsg]
@@ -989,9 +1017,9 @@
list(failing_context)::in, det_info::in, determinism::out,
list(failing_context)::out, list(context_det_msg)::out) is det.
-det_infer_unify(LHS, RHS0, Unify, UnifyContext, RHS,
- GoalInfo, InstMap0, SolnContext, RightFailingContexts, DetInfo,
- Detism, GoalFailingContexts, !:Msgs) :-
+det_infer_unify(LHS, RHS0, Unify, UnifyContext, RHS, GoalInfo, InstMap0,
+ SolnContext, RightFailingContexts, DetInfo, Detism,
+ GoalFailingContexts, !:Msgs) :-
% Unifications are either deterministic or semideterministic.
(
RHS0 = lambda_goal(Purity, PredOrFunc, EvalMethod, NonLocalVars,
@@ -1006,7 +1034,7 @@
instmap__pre_lambda_update(ModuleInfo, Vars, Modes,
InstMap0, InstMap1),
det_infer_goal(Goal0, Goal, InstMap1, LambdaSolnContext, [],
- DetInfo, LambdaInferredDet, _LambdaFailingContexts, GoalMsgs),
+ no, DetInfo, LambdaInferredDet, _LambdaFailingContexts, GoalMsgs),
det_check_lambda(LambdaDeclaredDet, LambdaInferredDet,
Goal, GoalInfo, DetInfo, CheckLambdaMsgs),
list__append(GoalMsgs, CheckLambdaMsgs, !:Msgs),
@@ -1054,21 +1082,21 @@
:- pred det_infer_if_then_else(hlds_goal::in, hlds_goal::out,
hlds_goal::in, hlds_goal::out, hlds_goal::in, hlds_goal::out,
- instmap::in, soln_context::in,
- list(failing_context)::in, det_info::in, determinism::out,
+ instmap::in, soln_context::in, list(failing_context)::in,
+ maybe(pess_info)::in, det_info::in, determinism::out,
list(failing_context)::out, list(context_det_msg)::out) is det.
-det_infer_if_then_else(Cond0, Cond, Then0, Then, Else0, Else,
- InstMap0, SolnContext, RightFailingContexts, DetInfo, Detism,
- GoalFailingContexts, !:Msgs) :-
+det_infer_if_then_else(Cond0, Cond, Then0, Then, Else0, Else, InstMap0,
+ SolnContext, RightFailingContexts, MaybePromiseEqvSolutionSets,
+ DetInfo, Detism, GoalFailingContexts, !:Msgs) :-
% We process the goal right-to-left, doing the `then' before the
% condition of the if-then-else, so that we can propagate the
% SolnContext correctly.
% First process the `then' part
update_instmap(Cond0, InstMap0, InstMap1),
- det_infer_goal(Then0, Then, InstMap1, SolnContext,
- RightFailingContexts, DetInfo, ThenDetism, ThenFailingContexts,
+ det_infer_goal(Then0, Then, InstMap1, SolnContext, RightFailingContexts,
+ MaybePromiseEqvSolutionSets, DetInfo, ThenDetism, ThenFailingContexts,
ThenMsgs),
determinism_components(ThenDetism, ThenCanFail, ThenMaxSoln),
@@ -1085,13 +1113,14 @@
),
% Process the `condition' part
det_infer_goal(Cond0, Cond, InstMap0, CondSolnContext,
- ThenFailingContexts ++ RightFailingContexts, DetInfo,
+ ThenFailingContexts ++ RightFailingContexts,
+ MaybePromiseEqvSolutionSets, DetInfo,
CondDetism, _CondFailingContexts, CondMsgs),
determinism_components(CondDetism, CondCanFail, CondMaxSoln),
% Process the `else' part
- det_infer_goal(Else0, Else, InstMap0, SolnContext,
- RightFailingContexts, DetInfo, ElseDetism, ElseFailingContexts,
+ det_infer_goal(Else0, Else, InstMap0, SolnContext, RightFailingContexts,
+ MaybePromiseEqvSolutionSets, DetInfo, ElseDetism, ElseFailingContexts,
ElseMsgs),
determinism_components(ElseDetism, ElseCanFail, ElseMaxSoln),
@@ -1123,11 +1152,11 @@
!:Msgs = CondMsgs ++ ThenMsgs ++ ElseMsgs.
:- pred det_infer_not(hlds_goal::in, hlds_goal::out, hlds_goal_info::in,
- instmap::in, det_info::in, determinism::out,
+ instmap::in, maybe(pess_info)::in, det_info::in, determinism::out,
list(failing_context)::out, list(context_det_msg)::out) is det.
-det_infer_not(Goal0, Goal, GoalInfo, InstMap0, DetInfo, Detism,
- GoalFailingContexts, !:Msgs) :-
+det_infer_not(Goal0, Goal, GoalInfo, InstMap0, MaybePromiseEqvSolutionSets,
+ DetInfo, Detism, GoalFailingContexts, !:Msgs) :-
% Negations are almost always semideterministic. It is an error for
% a negation to further instantiate any non-local variable. Such errors
% will be reported by the mode analysis.
@@ -1135,8 +1164,9 @@
% Question: should we warn about the negation of goals that either
% cannot succeed or cannot fail?
% Answer: yes, probably, but it's not a high priority.
- det_infer_goal(Goal0, Goal, InstMap0, first_soln, [], DetInfo,
- NegDetism, _NegatedGoalCanFail, !:Msgs),
+ det_infer_goal(Goal0, Goal, InstMap0, first_soln, [],
+ MaybePromiseEqvSolutionSets, DetInfo, NegDetism, _NegatedGoalCanFail,
+ !:Msgs),
det_negation_det(NegDetism, MaybeDetism),
(
MaybeDetism = no,
@@ -1159,28 +1189,75 @@
:- pred det_infer_scope(scope_reason::in, hlds_goal::in, hlds_goal::out,
hlds_goal_info::in, instmap::in, soln_context::in,
- list(failing_context)::in, det_info::in, determinism::out,
- list(failing_context)::out, list(context_det_msg)::out) is det.
+ list(failing_context)::in, maybe(pess_info)::in, det_info::in,
+ determinism::out, list(failing_context)::out, list(context_det_msg)::out)
+ is det.
det_infer_scope(Reason, Goal0, Goal, GoalInfo, InstMap0, SolnContext,
- RightFailingContexts, DetInfo, Detism, GoalFailingContexts, !:Msgs) :-
+ RightFailingContexts, MaybePromiseEqvSolutionSets0, DetInfo, Detism,
+ GoalFailingContexts, !:Msgs) :-
% Existential quantification may require a cut to throw away solutions,
% but we cannot rely on explicit quantification to detect this.
% Therefore cuts are handled in det_infer_goal.
( Reason = promise_solutions(Vars, Kind) ->
+ det_get_proc_info(DetInfo, ProcInfo),
+ proc_info_varset(ProcInfo, VarSet),
+
+ goal_info_get_context(GoalInfo, Context),
+ (
+ Kind = equivalent_solutions,
SolnContextToUse = first_soln,
+ MaybePromiseEqvSolutionSets = MaybePromiseEqvSolutionSets0,
+ PromiseMsgs = []
+ ;
+ Kind = equivalent_solution_sets,
+ SolnContextToUse = SolnContext,
+ (
+ MaybePromiseEqvSolutionSets0 = no,
+ MaybePromiseEqvSolutionSets = yes(pess_info(Vars, Context)),
+ PromiseMsgs = []
+ ;
+ MaybePromiseEqvSolutionSets0 = yes(pess_info(OldVars,
+ OldContext)),
+ PromiseMsg = nested_promise_eqv_solution_sets(OldContext),
+ PromiseScopeMsg = context_det_msg(Context, PromiseMsg),
+ PromiseMsgs = [PromiseScopeMsg],
+ AllVars = set.union(list_to_set(OldVars), list_to_set(Vars)),
+ MaybePromiseEqvSolutionSets =
+ yes(pess_info(to_sorted_list(AllVars), OldContext))
+ )
+ ;
+ Kind = equivalent_solution_sets_arbitrary,
+ (
+ MaybePromiseEqvSolutionSets0 = no,
+ PromiseMsg = arbitrary_without_promise,
+ PromiseScopeMsg = context_det_msg(Context, PromiseMsg),
+ PromiseMsgs = [PromiseScopeMsg]
+ ;
+ MaybePromiseEqvSolutionSets0 = yes(pess_info(OldVars,
+ OldContext)),
+ IntersectVars = set.intersect(list_to_set(OldVars),
+ list_to_set(Vars)),
+ ( set.empty(IntersectVars) ->
+ PromiseMsgs = []
+ ;
+ PromiseMsg = arbitrary_promise_overlap(OldContext,
+ VarSet, IntersectVars),
+ PromiseScopeMsg = context_det_msg(Context, PromiseMsg),
+ PromiseMsgs = [PromiseScopeMsg]
+ )
+ ),
+ MaybePromiseEqvSolutionSets = no,
+ SolnContextToUse = first_soln
+ ),
goal_info_get_instmap_delta(GoalInfo, InstmapDelta),
instmap_delta_changed_vars(InstmapDelta, ChangedVars),
det_info_get_module_info(DetInfo, ModuleInfo),
set__divide(var_is_ground_in_instmap(ModuleInfo, InstMap0),
ChangedVars, _GroundAtStartVars, BoundVars),
- goal_info_get_context(GoalInfo, Context),
- det_get_proc_info(DetInfo, ProcInfo),
- proc_info_varset(ProcInfo, VarSet),
-
% Which vars were bound inside the scope but not listed
- % in the promise_{equivalent,same}_solutions?
+ % in the promise_equivalent_solution{s,_sets} or arbitrary scope?
set__difference(BoundVars, set__list_to_set(Vars), BugVars),
( set__empty(BugVars) ->
ScopeMsgs1 = []
@@ -1202,11 +1279,14 @@
ScopeMsgs = ScopeMsgs1 ++ ScopeMsgs2
;
SolnContextToUse = SolnContext,
+ MaybePromiseEqvSolutionSets = MaybePromiseEqvSolutionSets0,
+ PromiseMsgs = [],
ScopeMsgs = []
),
det_infer_goal(Goal0, Goal, InstMap0, SolnContextToUse,
- RightFailingContexts, DetInfo, Detism, GoalFailingContexts, SubMsgs),
- !:Msgs = SubMsgs ++ ScopeMsgs.
+ RightFailingContexts, MaybePromiseEqvSolutionSets, DetInfo, Detism,
+ GoalFailingContexts, SubMsgs),
+ !:Msgs = PromiseMsgs ++ SubMsgs ++ ScopeMsgs.
%-----------------------------------------------------------------------------%
Index: compiler/det_report.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/det_report.m,v
retrieving revision 1.112
diff -u -b -r1.112 det_report.m
--- compiler/det_report.m 24 Feb 2006 05:49:28 -0000 1.112
+++ compiler/det_report.m 20 Mar 2006 11:29:36 -0000
@@ -82,6 +82,9 @@
; export_model_non_proc(pred_id, proc_id, determinism)
% Procedure with multi or nondet detism exported
% via :- pragma export ...
+ ; nested_promise_eqv_solution_sets(prog_context)
+ ; arbitrary_without_promise
+ ; arbitrary_promise_overlap(prog_context, prog_varset, set(prog_var))
; promise_solutions_missing_vars(promise_solutions_kind, prog_varset,
set(prog_var))
; promise_solutions_extra_vars(promise_solutions_kind, prog_varset,
@@ -1138,6 +1141,9 @@
det_msg_get_type(has_io_state_but_not_det(_, _), det_error).
det_msg_get_type(will_not_throw_with_erroneous(_, _), det_error).
det_msg_get_type(export_model_non_proc(_, _, _), det_error).
+det_msg_get_type(nested_promise_eqv_solution_sets(_), det_error).
+det_msg_get_type(arbitrary_without_promise, det_error).
+det_msg_get_type(arbitrary_promise_overlap(_, _, _), det_error).
det_msg_get_type(promise_solutions_missing_vars(_, _, _), det_error).
det_msg_get_type(promise_solutions_extra_vars(_, _, _), det_error).
@@ -1169,6 +1175,9 @@
det_msg_is_any_mode_msg(has_io_state_but_not_det(_, _), any_mode).
det_msg_is_any_mode_msg(will_not_throw_with_erroneous(_, _), any_mode).
det_msg_is_any_mode_msg(export_model_non_proc(_, _, _), any_mode).
+det_msg_is_any_mode_msg(nested_promise_eqv_solution_sets(_), any_mode).
+det_msg_is_any_mode_msg(arbitrary_without_promise, any_mode).
+det_msg_is_any_mode_msg(arbitrary_promise_overlap(_, _, _), any_mode).
det_msg_is_any_mode_msg(promise_solutions_missing_vars(_, _, _), any_mode).
det_msg_is_any_mode_msg(promise_solutions_extra_vars(_, _, _), any_mode).
@@ -1490,11 +1499,48 @@
det_report_msg(export_model_non_proc(_PredId, _ProcId, Detism), Context,
_ModuleInfo, !IO) :-
Pieces = [words("Error: "),
- fixed(":- pragma export' declaration"),
+ fixed("`:- pragma export' declaration"),
words("for a procedure that has a determinism of"),
- fixed(hlds_out.determinism_to_string(Detism) ++ ",")
- ],
+ fixed(hlds_out.determinism_to_string(Detism) ++ ".")],
write_error_pieces(Context, 0, Pieces, !IO).
+det_report_msg(nested_promise_eqv_solution_sets(OuterContext), Context,
+ _ModuleInfo, !IO) :-
+ Pieces = [words("Error: "),
+ words("`promise_equivalent_solution_sets' scope"),
+ words("is nested inside another.")],
+ write_error_pieces(Context, 0, Pieces, !IO),
+ Pieces2 = [words("This is the outer "),
+ words("`promise_equivalent_solution_sets' scope.")],
+ write_error_pieces_not_first_line(OuterContext, 0, Pieces2, !IO).
+det_report_msg(arbitrary_without_promise, Context, _ModuleInfo, !IO) :-
+ Pieces = [words("Error: "),
+ words("this `arbitrary' scope is not nested inside"),
+ words("a `promise_equivalent_solution_sets' scope.")],
+ write_error_pieces(Context, 0, Pieces, !IO).
+det_report_msg(arbitrary_promise_overlap(PromiseContext, VarSet, OverlapVars),
+ Context, _ModuleInfo, !IO) :-
+ VarNames = list.map(lookup_var_name_in_varset(VarSet),
+ set.to_sorted_list(OverlapVars)),
+ (
+ VarNames = [],
+ unexpected(this_file, "det_report_msg: " ++
+ "arbitrary_promise_overlap empty")
+ ;
+ VarNames = [_],
+ VarStr = "the variable"
+ ;
+ VarNames = [_, _ | _],
+ VarStr = "the following variables:"
+ ),
+ Pieces = [words("Error: "),
+ words("this `arbitrary' scope and the"),
+ words("`promise_equivalent_solution_sets' scope it is nested inside"),
+ words("overlap on"), words(VarStr)]
+ ++ list_to_pieces(VarNames) ++ [suffix(".")],
+ write_error_pieces(Context, 0, Pieces, !IO),
+ Pieces2 = [words("This is the outer "),
+ words("`promise_equivalent_solution_sets' scope.")],
+ write_error_pieces_not_first_line(PromiseContext, 0, Pieces2, !IO).
det_report_msg(promise_solutions_missing_vars(Kind, VarSet, Vars), Context, _,
!IO) :-
VarNames = list.map(lookup_var_name_in_varset(VarSet),
@@ -1511,8 +1557,9 @@
VarNames = [_, _ | _],
ListStr = "some variables that are not listed:"
),
- Pieces = [words("Error: the"), words(KindStr), words("goal binds"),
- words(ListStr)] ++ list_to_pieces(VarNames) ++ [suffix(".")],
+ Pieces = [words("Error: the"), words(add_quotes(KindStr)),
+ words("goal binds"), words(ListStr)]
+ ++ list_to_pieces(VarNames) ++ [suffix(".")],
error_util.write_error_pieces(Context, 0, Pieces, !IO).
det_report_msg(promise_solutions_extra_vars(Kind, VarSet, Vars), Context, _,
!IO) :-
@@ -1530,16 +1577,19 @@
VarNames = [_, _ | _],
ListStr = "some extra variables:"
),
- Pieces = [words("Error: the"), words(KindStr), words("goal lists"),
- words(ListStr)] ++ list_to_pieces(VarNames) ++ [suffix(".")],
+ Pieces = [words("Error: the"), words(add_quotes(KindStr)),
+ words("goal lists"), words(ListStr)]
+ ++ list_to_pieces(VarNames) ++ [suffix(".")],
error_util.write_error_pieces(Context, 0, Pieces, !IO).
:- func promise_solutions_kind_str(promise_solutions_kind) = string.
promise_solutions_kind_str(equivalent_solutions)
= "promise_equivalent_solutions".
-promise_solutions_kind_str(same_solutions)
- = "promise_same_solutions".
+promise_solutions_kind_str(equivalent_solution_sets)
+ = "promise_equivalent_solution_sets".
+promise_solutions_kind_str(equivalent_solution_sets_arbitrary)
+ = "arbitrary".
:- func lookup_var_name_in_varset(prog_varset, prog_var) = string.
Index: compiler/hlds_goal.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/hlds_goal.m,v
retrieving revision 1.152
diff -u -b -r1.152 hlds_goal.m
--- compiler/hlds_goal.m 9 Mar 2006 04:56:32 -0000 1.152
+++ compiler/hlds_goal.m 20 Mar 2006 14:39:33 -0000
@@ -300,7 +300,8 @@
:- type promise_solutions_kind
---> equivalent_solutions
- ; same_solutions.
+ ; equivalent_solution_sets
+ ; equivalent_solution_sets_arbitrary.
:- type removable
---> removable
@@ -1012,22 +1013,10 @@
% thousand). This feature may be attached to
% switches as well as disjunctions.
- ; will_not_modify_trail
+ ; will_not_modify_trail.
% This goal will not modify the trail, so it
% is safe for the compiler to omit trailing
% primitives when generating code for this goal.
-
- ; promise_same_deconstruct.
- % This goal is a deconstruction unification
- % occurring in a promise_same_conj conjunction,
- % which would naturally have detism cc_multi
- % due to the deconstructed variable's type having
- % user-defined equality. However, this annotation
- % means that the programmer has promised that
- % the results of the conjunction don't depend
- % on which of the possible concrete representations
- % of the abstract value the deconstructed variable
- % actually has.
% We can think of the goal that defines a procedure to be a tree,
% whose leaves are primitive goals and whose interior nodes are
Index: compiler/hlds_out.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/hlds_out.m,v
retrieving revision 1.385
diff -u -b -r1.385 hlds_out.m
--- compiler/hlds_out.m 9 Mar 2006 04:56:33 -0000 1.385
+++ compiler/hlds_out.m 12 Mar 2006 13:25:41 -0000
@@ -1481,8 +1481,11 @@
Kind = equivalent_solutions,
io.write_string("promise_equivalent_solutions", !IO)
;
- Kind = same_solutions,
- io.write_string("promise_same_solutions", !IO)
+ Kind = equivalent_solution_sets,
+ io.write_string("promise_equivalent_solution_sets", !IO)
+ ;
+ Kind = equivalent_solution_sets_arbitrary,
+ io.write_string("arbitrary", !IO)
),
io.write_string(" [", !IO),
mercury_output_vars(Vars, VarSet, AppendVarNums, !IO),
Index: compiler/make_hlds_passes.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/make_hlds_passes.m,v
retrieving revision 1.34
diff -u -b -r1.34 make_hlds_passes.m
--- compiler/make_hlds_passes.m 20 Mar 2006 22:24:26 -0000 1.34
+++ compiler/make_hlds_passes.m 21 Mar 2006 00:16:45 -0000
@@ -1207,9 +1207,9 @@
% See the comments for prog_io.parse_mutable_decl for the reason
% why we _must_ use MutVarset here.
%
- InitClause = clause(compiler(mutable_decl), MutVarset,
- predicate, mutable_init_pred_sym_name(ModuleName, Name), [],
- call(mutable_set_pred_sym_name(ModuleName, Name),
+ InitClause = clause(compiler(mutable_decl), MutVarset, predicate,
+ mutable_init_pred_sym_name(ModuleName, Name), [],
+ call_expr(mutable_set_pred_sym_name(ModuleName, Name),
[InitTerm], purity_impure) - Context),
add_item_clause(InitClause, !Status, Context, !ModuleInfo, !QualInfo,
!IO),
Index: compiler/make_hlds_warn.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/make_hlds_warn.m,v
retrieving revision 1.8
diff -u -b -r1.8 make_hlds_warn.m
--- compiler/make_hlds_warn.m 17 Mar 2006 01:40:26 -0000 1.8
+++ compiler/make_hlds_warn.m 20 Mar 2006 08:44:31 -0000
@@ -594,12 +594,13 @@
is det.
check_promise_ex_goal(PromiseType, GoalExpr - Context, !IO) :-
- ( GoalExpr = some(_, Goal) -> check_promise_ex_goal(PromiseType, Goal, !IO)
- ; GoalExpr = ( _ ; _ ) ->
+ ( GoalExpr = some_expr(_, Goal) ->
+ check_promise_ex_goal(PromiseType, Goal, !IO)
+ ; GoalExpr = disj_expr(_, _) ->
flatten_to_disj_list(GoalExpr - Context, DisjList),
list.map(flatten_to_conj_list, DisjList, DisjConjList),
check_disjunction(PromiseType, DisjConjList, !IO)
- ; GoalExpr = all(_UnivVars, Goal) ->
+ ; GoalExpr = all_expr(_UnivVars, Goal) ->
promise_ex_error(PromiseType, Context,
"universal quantification should come before " ++
"the declaration name", !IO),
@@ -615,7 +616,7 @@
:- pred flatten_to_disj_list(goal::in, goals::out) is det.
flatten_to_disj_list(GoalExpr - Context, GoalList) :-
- ( GoalExpr = ( GoalA ; GoalB ) ->
+ ( GoalExpr = disj_expr(GoalA, GoalB) ->
flatten_to_disj_list(GoalA, GoalListA),
flatten_to_disj_list(GoalB, GoalListB),
GoalList = GoalListA ++ GoalListB
@@ -629,7 +630,7 @@
:- pred flatten_to_conj_list(goal::in, goals::out) is det.
flatten_to_conj_list(GoalExpr - Context, GoalList) :-
- ( GoalExpr = ( GoalA , GoalB ) ->
+ ( GoalExpr = conj_expr(GoalA, GoalB) ->
flatten_to_conj_list(GoalA, GoalListA),
flatten_to_conj_list(GoalB, GoalListB),
GoalList = GoalListA ++ GoalListB
@@ -662,11 +663,11 @@
Goals = []
;
Goals = [GoalExpr - Context | Rest],
- ( GoalExpr = unify(_, _, _) ->
+ ( GoalExpr = unify_expr(_, _, _) ->
check_disj_arm(PromiseType, Rest, CallUsed, !IO)
- ; GoalExpr = some(_, Goal) ->
+ ; GoalExpr = some_expr(_, Goal) ->
check_disj_arm(PromiseType, [Goal | Rest], CallUsed, !IO)
- ; GoalExpr = call(_, _, _) ->
+ ; GoalExpr = call_expr(_, _, _) ->
(
CallUsed = no
;
Index: compiler/mercury_to_mercury.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/mercury_to_mercury.m,v
retrieving revision 1.286
diff -u -b -r1.286 mercury_to_mercury.m
--- compiler/mercury_to_mercury.m 20 Mar 2006 22:24:26 -0000 1.286
+++ compiler/mercury_to_mercury.m 20 Mar 2006 23:59:53 -0000
@@ -676,7 +676,7 @@
(
UnivVars = [_ | _],
Goal0 = _GoalExpr - Context,
- Goal = all(UnivVars, Goal0) - Context
+ Goal = all_expr(UnivVars, Goal0) - Context
;
UnivVars = [],
Goal = Goal0
@@ -2475,7 +2475,7 @@
;
Args = []
),
- ( Body = true - _Context0 ->
+ ( Body = true_expr - _Context0 ->
true
;
io.write_string(" :-\n\t", !IO),
@@ -2501,7 +2501,7 @@
Args = []
),
io.write_string(" = ", !IO),
- ( Body = true - _Context0 ->
+ ( Body = true_expr - _Context0 ->
mercury_format_term(Result, VarSet, no, next_to_graphic_token, !IO)
;
mercury_format_term(Result, VarSet, no, !IO),
@@ -2518,13 +2518,13 @@
:- pred mercury_output_goal_2(goal_expr::in, prog_varset::in, int::in,
io::di, io::uo) is det.
-mercury_output_goal_2(fail, _, _, !IO) :-
+mercury_output_goal_2(fail_expr, _, _, !IO) :-
io.write_string("fail", !IO).
-mercury_output_goal_2(true, _, _, !IO) :-
+mercury_output_goal_2(true_expr, _, _, !IO) :-
io.write_string("true", !IO).
-mercury_output_goal_2(implies(G1,G2), VarSet, Indent, !IO) :-
+mercury_output_goal_2(implies_expr(G1,G2), VarSet, Indent, !IO) :-
Indent1 = Indent + 1,
io.write_string("(", !IO),
mercury_output_newline(Indent1, !IO),
@@ -2536,7 +2536,7 @@
mercury_output_newline(Indent, !IO),
io.write_string(")", !IO).
-mercury_output_goal_2(equivalent(G1,G2), VarSet, Indent, !IO) :-
+mercury_output_goal_2(equivalent_expr(G1,G2), VarSet, Indent, !IO) :-
Indent1 = Indent + 1,
io.write_string("(", !IO),
mercury_output_newline(Indent1, !IO),
@@ -2548,7 +2548,7 @@
mercury_output_newline(Indent, !IO),
io.write_string(")", !IO).
-mercury_output_goal_2(some(Vars, Goal), VarSet, Indent, !IO) :-
+mercury_output_goal_2(some_expr(Vars, Goal), VarSet, Indent, !IO) :-
(
Vars = [],
mercury_output_goal(Goal, VarSet, Indent, !IO)
@@ -2564,7 +2564,7 @@
io.write_string(")", !IO)
).
-mercury_output_goal_2(some_state_vars(Vars, Goal), VarSet, Indent, !IO) :-
+mercury_output_goal_2(some_state_vars_expr(Vars, Goal), VarSet, Indent, !IO) :-
(
Vars = [],
mercury_output_goal(Goal, VarSet, Indent, !IO)
@@ -2580,7 +2580,7 @@
io.write_string(")", !IO)
).
-mercury_output_goal_2(all(Vars, Goal), VarSet, Indent, !IO) :-
+mercury_output_goal_2(all_expr(Vars, Goal), VarSet, Indent, !IO) :-
(
Vars = [],
mercury_output_goal(Goal, VarSet, Indent, !IO)
@@ -2596,7 +2596,7 @@
io.write_string(")", !IO)
).
-mercury_output_goal_2(all_state_vars(Vars, Goal), VarSet, Indent, !IO) :-
+mercury_output_goal_2(all_state_vars_expr(Vars, Goal), VarSet, Indent, !IO) :-
(
Vars = [],
mercury_output_goal(Goal, VarSet, Indent, !IO)
@@ -2613,48 +2613,26 @@
).
mercury_output_goal_2(
- promise_equivalent_solutions(Vars, DotSVars, ColonSVars, Goal), VarSet,
- Indent, !IO) :-
- (
- Vars = [],
- DotSVars = [],
- ColonSVars = []
- ->
- % This should have been caught be prog_io_goal when reading in
- % the term, but there is no point in aborting here.
- mercury_output_goal(Goal, VarSet, Indent, !IO)
- ;
- io.write_string("promise_equivalent_solutions [", !IO),
- mercury_output_vars(Vars, VarSet, no, !IO),
- (
- Vars \= [],
- DotSVars \= []
- ->
- io.write_string(", ", !IO)
- ;
- true
- ),
- mercury_output_state_vars_using_prefix(DotSVars, "!.", VarSet, no,
- !IO),
- (
- ( Vars \= [] ; DotSVars \= [] ),
- ColonSVars \= []
- ->
- io.write_string(", ", !IO)
- ;
- true
- ),
- mercury_output_state_vars_using_prefix(ColonSVars, "!:", VarSet, no,
- !IO),
- io.write_string("] (", !IO),
- Indent1 = Indent + 1,
- mercury_output_newline(Indent1, !IO),
- mercury_output_goal(Goal, VarSet, Indent1, !IO),
- mercury_output_newline(Indent, !IO),
- io.write_string(")", !IO)
- ).
+ promise_equivalent_solutions_expr(Vars, DotSVars, ColonSVars, Goal),
+ VarSet, Indent, !IO) :-
+ mercury_output_promise_eqv_solutions_goal(Vars, DotSVars, ColonSVars,
+ Goal, VarSet, Indent, "promise_equivalent_solutions", !IO).
+
+mercury_output_goal_2(
+ promise_equivalent_solution_sets_expr(Vars, DotSVars, ColonSVars,
+ Goal),
+ VarSet, Indent, !IO) :-
+ mercury_output_promise_eqv_solutions_goal(Vars, DotSVars, ColonSVars,
+ Goal, VarSet, Indent, "promise_equivalent_solution_sets", !IO).
-mercury_output_goal_2(promise_purity(_Implicit, Purity, Goal), VarSet,
+mercury_output_goal_2(
+ promise_equivalent_solution_arbitrary_expr(Vars, DotSVars, ColonSVars,
+ Goal),
+ VarSet, Indent, !IO) :-
+ mercury_output_promise_eqv_solutions_goal(Vars, DotSVars, ColonSVars,
+ Goal, VarSet, Indent, "arbitrary", !IO).
+
+mercury_output_goal_2(promise_purity_expr(_Implicit, Purity, Goal), VarSet,
Indent, !IO) :-
(
Purity = purity_pure,
@@ -2672,7 +2650,7 @@
mercury_output_newline(Indent, !IO),
io.write_string(")", !IO).
-mercury_output_goal_2(if_then_else(Vars, StateVars, A, B, C), VarSet,
+mercury_output_goal_2(if_then_else_expr(Vars, StateVars, A, B, C), VarSet,
Indent, !IO) :-
io.write_string("(if", !IO),
mercury_output_some(Vars, StateVars, VarSet, !IO),
@@ -2690,20 +2668,7 @@
mercury_output_newline(Indent, !IO),
io.write_string(")", !IO).
-mercury_output_goal_2(if_then(Vars, StateVars, A, B), VarSet, Indent, !IO) :-
- io.write_string("(if", !IO),
- mercury_output_some(Vars, StateVars, VarSet, !IO),
- Indent1 = Indent + 1,
- mercury_output_newline(Indent1, !IO),
- mercury_output_goal(A, VarSet, Indent1, !IO),
- mercury_output_newline(Indent, !IO),
- io.write_string("then", !IO),
- mercury_output_newline(Indent1, !IO),
- mercury_output_goal(B, VarSet, Indent1, !IO),
- mercury_output_newline(Indent, !IO),
- io.write_string(")", !IO).
-
-mercury_output_goal_2(not(Goal), VarSet, Indent, !IO) :-
+mercury_output_goal_2(not_expr(Goal), VarSet, Indent, !IO) :-
io.write_string("\\+ (", !IO),
Indent1 = Indent + 1,
mercury_output_newline(Indent1, !IO),
@@ -2711,13 +2676,13 @@
mercury_output_newline(Indent, !IO),
io.write_string(")", !IO).
-mercury_output_goal_2((A,B), VarSet, Indent, !IO) :-
+mercury_output_goal_2(conj_expr(A, B), VarSet, Indent, !IO) :-
mercury_output_goal(A, VarSet, Indent, !IO),
io.write_string(",", !IO),
mercury_output_newline(Indent, !IO),
mercury_output_goal(B, VarSet, Indent, !IO).
-mercury_output_goal_2((A & B), VarSet, Indent, !IO) :-
+mercury_output_goal_2(par_conj_expr(A, B), VarSet, Indent, !IO) :-
io.write_string("(", !IO),
Indent1 = Indent + 1,
mercury_output_newline(Indent1, !IO),
@@ -2726,7 +2691,7 @@
mercury_output_newline(Indent, !IO),
io.write_string(")", !IO).
-mercury_output_goal_2((A;B), VarSet, Indent, !IO) :-
+mercury_output_goal_2(disj_expr(A, B), VarSet, Indent, !IO) :-
io.write_string("(", !IO),
Indent1 = Indent + 1,
mercury_output_newline(Indent1, !IO),
@@ -2735,16 +2700,63 @@
mercury_output_newline(Indent, !IO),
io.write_string(")", !IO).
-mercury_output_goal_2(call(Name, Term, Purity), VarSet, Indent, !IO) :-
+mercury_output_goal_2(call_expr(Name, Term, Purity), VarSet, Indent, !IO) :-
write_purity_prefix(Purity, !IO),
mercury_output_call(Name, Term, VarSet, Indent, !IO).
-mercury_output_goal_2(unify(A, B, Purity), VarSet, _Indent, !IO) :-
+mercury_output_goal_2(unify_expr(A, B, Purity), VarSet, _Indent, !IO) :-
write_purity_prefix(Purity, !IO),
mercury_output_term(A, VarSet, no, !IO),
io.write_string(" = ", !IO),
mercury_output_term(B, VarSet, no, next_to_graphic_token, !IO).
+:- pred mercury_output_promise_eqv_solutions_goal(prog_vars::in,
+ prog_vars::in, prog_vars::in, goal::in, prog_varset::in, int::in,
+ string::in, io::di, io::uo) is det.
+
+mercury_output_promise_eqv_solutions_goal(Vars, DotSVars, ColonSVars,
+ Goal, VarSet, Indent, Keyword, !IO) :-
+ (
+ Vars = [],
+ DotSVars = [],
+ ColonSVars = []
+ ->
+ % This should have been caught be prog_io_goal when reading in
+ % the term, but there is no point in aborting here.
+ mercury_output_goal(Goal, VarSet, Indent, !IO)
+ ;
+ io.write_string(Keyword, !IO),
+ io.write_string(" [", !IO),
+ mercury_output_vars(Vars, VarSet, no, !IO),
+ (
+ Vars = [_ | _],
+ DotSVars = [_ | _]
+ ->
+ io.write_string(", ", !IO)
+ ;
+ true
+ ),
+ mercury_output_state_vars_using_prefix(DotSVars, "!.", VarSet, no,
+ !IO),
+ (
+ ( Vars = [_ | _]
+ ; DotSVars = [_ | _]
+ ),
+ ColonSVars \= []
+ ->
+ io.write_string(", ", !IO)
+ ;
+ true
+ ),
+ mercury_output_state_vars_using_prefix(ColonSVars, "!:", VarSet, no,
+ !IO),
+ io.write_string("] (", !IO),
+ Indent1 = Indent + 1,
+ mercury_output_newline(Indent1, !IO),
+ mercury_output_goal(Goal, VarSet, Indent1, !IO),
+ mercury_output_newline(Indent, !IO),
+ io.write_string(")", !IO)
+ ).
:- pred mercury_output_state_vars_using_prefix(prog_vars::in, string::in,
prog_varset::in, bool::in, io::di, io::uo) is det.
@@ -2765,7 +2777,6 @@
mercury_output_state_vars_using_prefix(SVars, BangPrefix, VarSet,
AppendVarnums, !IO).
-
:- pred mercury_output_call(sym_name::in, list(prog_term)::in, prog_varset::in,
int::in, io::di, io::uo) is det.
@@ -2793,7 +2804,7 @@
io.write_string(";", !IO),
Indent1 = Indent + 1,
mercury_output_newline(Indent1, !IO),
- ( Goal = (A;B) - _Context ->
+ ( Goal = disj_expr(A, B) - _Context ->
mercury_output_goal(A, VarSet, Indent1, !IO),
mercury_output_disj(B, VarSet, Indent, !IO)
;
@@ -2808,7 +2819,7 @@
io.write_string("&", !IO),
Indent1 = Indent + 1,
mercury_output_newline(Indent1, !IO),
- ( Goal = (A & B) - _Context ->
+ ( Goal = par_conj_expr(A, B) - _Context ->
mercury_output_goal(A, VarSet, Indent1, !IO),
mercury_output_par_conj(B, VarSet, Indent, !IO)
;
Index: compiler/module_qual.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/module_qual.m,v
retrieving revision 1.128
diff -u -b -r1.128 module_qual.m
--- compiler/module_qual.m 20 Mar 2006 22:24:26 -0000 1.128
+++ compiler/module_qual.m 20 Mar 2006 23:59:54 -0000
@@ -486,54 +486,55 @@
% the maybe_and predicate to be associative.
% NB. accumulator introduction doesn't work on this case yet.
%
-process_assert((GA , GB) - _, Symbols, Success) :-
+process_assert(conj_expr(GA, GB) - _, Symbols, Success) :-
process_assert(GA, SymbolsA, SuccessA),
process_assert(GB, SymbolsB, SuccessB),
list.append(SymbolsA, SymbolsB, Symbols),
bool.and(SuccessA, SuccessB, Success).
-process_assert(true - _, [], yes).
-process_assert((GA & GB) - _, Symbols, Success) :-
+process_assert(true_expr - _, [], yes).
+process_assert(par_conj_expr(GA, GB) - _, Symbols, Success) :-
process_assert(GA, SymbolsA, SuccessA),
process_assert(GB, SymbolsB, SuccessB),
list.append(SymbolsA, SymbolsB, Symbols),
bool.and(SuccessA, SuccessB, Success).
-process_assert((GA ; GB) - _, Symbols, Success) :-
+process_assert(disj_expr(GA, GB) - _, Symbols, Success) :-
process_assert(GA, SymbolsA, SuccessA),
process_assert(GB, SymbolsB, SuccessB),
list.append(SymbolsA, SymbolsB, Symbols),
bool.and(SuccessA, SuccessB, Success).
-process_assert(fail - _, [], yes).
-process_assert(some(_, G) - _, Symbols, Success) :-
+process_assert(fail_expr - _, [], yes).
+process_assert(some_expr(_, G) - _, Symbols, Success) :-
process_assert(G, Symbols, Success).
-process_assert(some_state_vars(_, G) - _, Symbols, Success) :-
+process_assert(some_state_vars_expr(_, G) - _, Symbols, Success) :-
process_assert(G, Symbols, Success).
-process_assert(all(_, G) - _, Symbols, Success) :-
+process_assert(all_expr(_, G) - _, Symbols, Success) :-
process_assert(G, Symbols, Success).
-process_assert(all_state_vars(_, G) - _, Symbols, Success) :-
+process_assert(all_state_vars_expr(_, G) - _, Symbols, Success) :-
process_assert(G, Symbols, Success).
-process_assert(promise_purity(_I, _P, G) - _, Symbols, Success) :-
+process_assert(promise_purity_expr(_I, _P, G) - _, Symbols, Success) :-
process_assert(G, Symbols, Success).
-process_assert(promise_equivalent_solutions(_V, _D, _C, G) - _,
+process_assert(promise_equivalent_solutions_expr(_V, _D, _C, G) - _,
Symbols, Success) :-
process_assert(G, Symbols, Success).
-process_assert(implies(GA, GB) - _, Symbols, Success) :-
+process_assert(promise_equivalent_solution_sets_expr(_V, _D, _C, G) - _,
+ Symbols, Success) :-
+ process_assert(G, Symbols, Success).
+process_assert(promise_equivalent_solution_arbitrary_expr(_V, _D, _C, G) - _,
+ Symbols, Success) :-
+ process_assert(G, Symbols, Success).
+process_assert(implies_expr(GA, GB) - _, Symbols, Success) :-
process_assert(GA, SymbolsA, SuccessA),
process_assert(GB, SymbolsB, SuccessB),
list.append(SymbolsA, SymbolsB, Symbols),
bool.and(SuccessA, SuccessB, Success).
-process_assert(equivalent(GA, GB) - _, Symbols, Success) :-
+process_assert(equivalent_expr(GA, GB) - _, Symbols, Success) :-
process_assert(GA, SymbolsA, SuccessA),
process_assert(GB, SymbolsB, SuccessB),
list.append(SymbolsA, SymbolsB, Symbols),
bool.and(SuccessA, SuccessB, Success).
-process_assert(not(G) - _, Symbols, Success) :-
+process_assert(not_expr(G) - _, Symbols, Success) :-
process_assert(G, Symbols, Success).
-process_assert(if_then(_, _, GA, GB) - _, Symbols, Success) :-
- process_assert(GA, SymbolsA, SuccessA),
- process_assert(GB, SymbolsB, SuccessB),
- list.append(SymbolsA, SymbolsB, Symbols),
- bool.and(SuccessA, SuccessB, Success).
-process_assert(if_then_else(_, _, GA, GB, GC) - _, Symbols, Success) :-
+process_assert(if_then_else_expr(_, _, GA, GB, GC) - _, Symbols, Success) :-
process_assert(GA, SymbolsA, SuccessA),
process_assert(GB, SymbolsB, SuccessB),
process_assert(GC, SymbolsC, SuccessC),
@@ -541,14 +542,10 @@
list.append(Symbols0, SymbolsC, Symbols),
bool.and(SuccessA, SuccessB, Success0),
bool.and(Success0, SuccessC, Success).
-process_assert(call(SymName, Args0, _Purity) - _, Symbols, Success) :-
- (
- SymName = qualified(_, _)
- ->
+process_assert(call_expr(SymName, Args0, _Purity) - _, Symbols, Success) :-
+ ( SymName = qualified(_, _) ->
list.map(term.coerce, Args0, Args),
- (
- term_qualified_symbols_list(Args, Symbols0)
- ->
+ ( term_qualified_symbols_list(Args, Symbols0) ->
Symbols = [SymName | Symbols0],
Success = yes
;
@@ -559,7 +556,7 @@
Symbols = [],
Success = no
).
-process_assert(unify(LHS0, RHS0, _Purity) - _, Symbols, Success) :-
+process_assert(unify_expr(LHS0, RHS0, _Purity) - _, Symbols, Success) :-
term.coerce(LHS0, LHS),
term.coerce(RHS0, RHS),
(
Index: compiler/pd_util.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/pd_util.m,v
retrieving revision 1.48
diff -u -b -r1.48 pd_util.m
--- compiler/pd_util.m 17 Mar 2006 01:40:34 -0000 1.48
+++ compiler/pd_util.m 20 Mar 2006 09:52:07 -0000
@@ -379,7 +379,8 @@
proc_info_vartypes(ProcInfo, VarTypes),
det_info_init(ModuleInfo, VarTypes, PredId, ProcId, Globals, DetInfo),
pd_info_get_instmap(!.PDInfo, InstMap),
- det_infer_goal(Goal0, Goal, InstMap, SolnContext, [], DetInfo, _, _, Msgs),
+ det_infer_goal(Goal0, Goal, InstMap, SolnContext, [], no, DetInfo, _, _,
+ Msgs),
% Make sure there were no errors.
disable_det_warnings(OptionsToRestore, !IO),
Index: compiler/prog_io.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/prog_io.m,v
retrieving revision 1.262
diff -u -b -r1.262 prog_io.m
--- compiler/prog_io.m 20 Mar 2006 22:24:28 -0000 1.262
+++ compiler/prog_io.m 20 Mar 2006 23:59:54 -0000
@@ -1413,7 +1413,7 @@
% Get universally quantified variables.
( PromiseType = true ->
- ( Goal0 = all(UnivVars0, AllGoal) - _Context ->
+ ( Goal0 = all_expr(UnivVars0, AllGoal) - _Context ->
UnivVars0 = UnivVars,
Goal = AllGoal
;
Index: compiler/prog_io_dcg.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/prog_io_dcg.m,v
retrieving revision 1.35
diff -u -b -r1.35 prog_io_dcg.m
--- compiler/prog_io_dcg.m 17 Mar 2006 01:40:36 -0000 1.35
+++ compiler/prog_io_dcg.m 20 Mar 2006 09:19:06 -0000
@@ -124,7 +124,7 @@
% pair to the non-terminal's argument list.
new_dcg_var(!VarSet, !Counter, Var),
Args = Args0 ++ [term.variable(!.Var), term.variable(Var)],
- Goal = call(SymName, Args, purity_pure) - Context,
+ Goal = call_expr(SymName, Args, purity_pure) - Context,
!:Var = Var
)
;
@@ -133,7 +133,7 @@
% will catch calls to numbers and strings.
new_dcg_var(!VarSet, !Counter, Var),
term.coerce(Term, ProgTerm),
- Goal = call(unqualified("call"),
+ Goal = call_expr(unqualified("call"),
[ProgTerm, term.variable(!.Var), term.variable(Var)],
purity_pure) - Context,
!:Var = Var
@@ -173,43 +173,43 @@
parse_dcg_goal_2("promise_pure", [G], Context, Goal,
!VarSet, !Counter, !Var) :-
parse_dcg_goal(G, Goal0, !VarSet, !Counter, !Var),
- Goal = promise_purity(dont_make_implicit_promises, purity_pure, Goal0)
+ Goal = promise_purity_expr(dont_make_implicit_promises, purity_pure, Goal0)
- Context.
parse_dcg_goal_2("promise_semipure", [G], Context, Goal,
!VarSet, !Counter, !Var) :-
parse_dcg_goal(G, Goal0, !VarSet, !Counter, !Var),
- Goal = promise_purity(dont_make_implicit_promises, purity_semipure, Goal0)
- - Context.
+ Goal = promise_purity_expr(dont_make_implicit_promises, purity_semipure,
+ Goal0) - Context.
parse_dcg_goal_2("promise_impure", [G], Context, Goal,
!VarSet, !Counter, !Var) :-
parse_dcg_goal(G, Goal0, !VarSet, !Counter, !Var),
- Goal = promise_purity(dont_make_implicit_promises, purity_impure, Goal0)
- - Context.
+ Goal = promise_purity_expr(dont_make_implicit_promises, purity_impure,
+ Goal0) - Context.
parse_dcg_goal_2("promise_pure_implicit", [G], Context, Goal,
!VarSet, !Counter, !Var) :-
parse_dcg_goal(G, Goal0, !VarSet, !Counter, !Var),
- Goal = promise_purity(make_implicit_promises, purity_pure, Goal0)
+ Goal = promise_purity_expr(make_implicit_promises, purity_pure, Goal0)
- Context.
parse_dcg_goal_2("promise_semipure_implicit", [G], Context, Goal,
!VarSet, !Counter, !Var) :-
parse_dcg_goal(G, Goal0, !VarSet, !Counter, !Var),
- Goal = promise_purity(make_implicit_promises, purity_semipure, Goal0)
+ Goal = promise_purity_expr(make_implicit_promises, purity_semipure, Goal0)
- Context.
parse_dcg_goal_2("promise_impure_implicit", [G], Context, Goal,
!VarSet, !Counter, !Var) :-
parse_dcg_goal(G, Goal0, !VarSet, !Counter, !Var),
- Goal = promise_purity(make_implicit_promises, purity_impure, Goal0)
+ Goal = promise_purity_expr(make_implicit_promises, purity_impure, Goal0)
- Context.
parse_dcg_goal_2("[]", [], Context, Goal, !VarSet, !Counter, Var0, Var) :-
% Empty list - just unify the input and output DCG args.
new_dcg_var(!VarSet, !Counter, Var),
- Goal = unify(term.variable(Var0), term.variable(Var), purity_pure)
+ Goal = unify_expr(term.variable(Var0), term.variable(Var), purity_pure)
- Context.
parse_dcg_goal_2("[|]", [X, Xs], Context, Goal, !VarSet, !Counter,
@@ -220,32 +220,18 @@
ConsTerm0 = term.functor(term.atom("[|]"), [X, Xs], Context),
term.coerce(ConsTerm0, ConsTerm),
term_list_append_term(ConsTerm, term.variable(Var), Term),
- Goal = unify(term.variable(Var0), Term, purity_pure) - Context.
+ Goal = unify_expr(term.variable(Var0), Term, purity_pure) - Context.
parse_dcg_goal_2("=", [A0], Context, Goal, !VarSet, !Counter, Var, Var) :-
% Call to '='/1 - unify argument with DCG input arg.
term.coerce(A0, A),
- Goal = unify(A, term.variable(Var), purity_pure) - Context.
+ Goal = unify_expr(A, term.variable(Var), purity_pure) - Context.
parse_dcg_goal_2(":=", [A0], Context, Goal, !VarSet, !Counter, _Var0, Var) :-
% Call to ':='/1 - unify argument with DCG output arg.
new_dcg_var(!VarSet, !Counter, Var),
term.coerce(A0, A),
- Goal = unify(A, term.variable(Var), purity_pure) - Context.
-
-% parse_dcg_goal_2("->", [Cond0, Then0], Context, VarSet0, Counter0, Var0,
-% Goal, VarSet, Counter, Var) :-
-% % If-then (Prolog syntax).
-% % We need to add an else part to unify the DCG args.
-% parse_dcg_if_then(Cond0, Then0, Context, VarSet0, Counter0, Var0,
-% SomeVars, StateVars, Cond, Then, VarSet, Counter, Var),
-% ( Var = Var0 ->
-% Goal = if_then(SomeVars, StateVars, Cond, Then) - Context
-% ;
-% Unify = unify(term.variable(Var), term.variable(Var0)),
-% Goal = if_then_else(SomeVars, StateVars, Cond, Then,
-% Unify - Context) - Context
-% ).
+ Goal = unify_expr(A, term.variable(Var), purity_pure) - Context.
parse_dcg_goal_2("if", [term.functor(term.atom("then"), [Cond0, Then0], _)],
Context, Goal, !VarSet, !Counter, Var0, Var) :-
@@ -253,20 +239,22 @@
parse_dcg_if_then(Cond0, Then0, Context, SomeVars, StateVars,
Cond, Then, !VarSet, !Counter, Var0, Var),
( Var = Var0 ->
- Goal = if_then(SomeVars, StateVars, Cond, Then) - Context
+ Goal = if_then_else_expr(SomeVars, StateVars, Cond, Then,
+ true_expr - Context) - Context
;
- Unify = unify(term.variable(Var), term.variable(Var0), purity_pure),
- Goal = if_then_else(SomeVars, StateVars, Cond, Then, Unify - Context)
- - Context
+ Unify = unify_expr(term.variable(Var), term.variable(Var0),
+ purity_pure),
+ Goal = if_then_else_expr(SomeVars, StateVars, Cond, Then,
+ Unify - Context) - Context
).
-parse_dcg_goal_2(",", [A0, B0], Context, (A, B) - Context, !VarSet, !Counter,
- !Var) :-
+parse_dcg_goal_2(",", [A0, B0], Context, conj_expr(A, B) - Context, !VarSet,
+ !Counter, !Var) :-
% Conjunction.
parse_dcg_goal(A0, A, !VarSet, !Counter, !Var),
parse_dcg_goal(B0, B, !VarSet, !Counter, !Var).
-parse_dcg_goal_2("&", [A0, B0], Context, (A & B) - Context,
+parse_dcg_goal_2("&", [A0, B0], Context, par_conj_expr(A, B) - Context,
!VarSet, !Counter, !Var) :-
parse_dcg_goal(A0, A, !VarSet, !Counter, !Var),
parse_dcg_goal(B0, B, !VarSet, !Counter, !Var).
@@ -283,23 +271,23 @@
parse_dcg_goal(B0, B1, !VarSet, !Counter, Var0, VarB),
( VarA = Var0, VarB = Var0 ->
Var = Var0,
- Goal = (A1 ; B1) - Context
+ Goal = disj_expr(A1, B1) - Context
; VarA = Var0 ->
Var = VarB,
- Unify = unify(term.variable(Var), term.variable(VarA),
+ Unify = unify_expr(term.variable(Var), term.variable(VarA),
purity_pure),
append_to_disjunct(A1, Unify, Context, A2),
- Goal = (A2 ; B1) - Context
+ Goal = disj_expr(A2, B1) - Context
; VarB = Var0 ->
Var = VarA,
- Unify = unify(term.variable(Var), term.variable(VarB),
+ Unify = unify_expr(term.variable(Var), term.variable(VarB),
purity_pure),
append_to_disjunct(B1, Unify, Context, B2),
- Goal = (A1 ; B2) - Context
+ Goal = disj_expr(A1, B2) - Context
;
Var = VarB,
prog_util.rename_in_goal(VarA, VarB, A1, A2),
- Goal = (A2 ; B1) - Context
+ Goal = disj_expr(A2, B1) - Context
)
).
@@ -310,12 +298,12 @@
parse_dcg_if_then_else(Cond0, Then0, Else0, Context, Goal,
!VarSet, !Counter, !Var).
-parse_dcg_goal_2("not", [A0], Context, not(A) - Context,
+parse_dcg_goal_2("not", [A0], Context, not_expr(A) - Context,
!VarSet, !Counter, Var0, Var0) :-
% Negation (NU-Prolog syntax).
parse_dcg_goal(A0, A, !VarSet, !Counter, Var0, _).
-parse_dcg_goal_2("\\+", [A0], Context, not(A) - Context,
+parse_dcg_goal_2("\\+", [A0], Context, not_expr(A) - Context,
!VarSet, !Counter, Var0, Var0) :-
% Negation (Prolog syntax).
parse_dcg_goal(A0, A, !VarSet, !Counter, Var0, _).
@@ -336,15 +324,16 @@
;
Vars = [],
StateVars = [_ | _],
- GoalExpr = all_state_vars(StateVars, A)
+ GoalExpr = all_state_vars_expr(StateVars, A)
;
Vars = [_ | _],
StateVars = [],
- GoalExpr = all(Vars, A)
+ GoalExpr = all_expr(Vars, A)
;
Vars = [_ | _],
StateVars = [_ | _],
- GoalExpr = all(Vars, all_state_vars(StateVars, A) - ContextA)
+ GoalExpr = all_expr(Vars, all_state_vars_expr(StateVars, A)
+ - ContextA)
).
parse_dcg_goal_2("some", [QVars, A0], Context, GoalExpr - Context,
@@ -363,15 +352,16 @@
;
Vars = [],
StateVars = [_ | _],
- GoalExpr = some_state_vars(StateVars, A)
+ GoalExpr = some_state_vars_expr(StateVars, A)
;
Vars = [_ | _],
StateVars = [],
- GoalExpr = some(Vars, A)
+ GoalExpr = some_expr(Vars, A)
;
Vars = [_ | _],
StateVars = [_ | _],
- GoalExpr = some(Vars, some_state_vars(StateVars, A) - ContextA)
+ GoalExpr = some_expr(Vars, some_state_vars_expr(StateVars, A)
+ - ContextA)
).
:- pred parse_dcg_goal_with_purity(term::in, purity::in, goal::out,
@@ -380,10 +370,10 @@
parse_dcg_goal_with_purity(G, Purity, Goal, !VarSet, !Counter, !Var) :-
parse_dcg_goal(G, Goal1, !VarSet, !Counter, !Var),
- ( Goal1 = call(Pred, Args, purity_pure) - Context ->
- Goal = call(Pred, Args, Purity) - Context
- ; Goal1 = unify(ProgTerm1, ProgTerm2, purity_pure) - Context ->
- Goal = unify(ProgTerm1, ProgTerm2, Purity) - Context
+ ( Goal1 = call_expr(Pred, Args, purity_pure) - Context ->
+ Goal = call_expr(Pred, Args, Purity) - Context
+ ; Goal1 = unify_expr(ProgTerm1, ProgTerm2, purity_pure) - Context ->
+ Goal = unify_expr(ProgTerm1, ProgTerm2, Purity) - Context
;
% Inappropriate placement of an impurity marker, so we treat
% it like a predicate call. typecheck.m prints out something
@@ -391,19 +381,20 @@
Goal1 = _ - Context,
purity_name(Purity, PurityString),
term.coerce(G, G1),
- Goal = call(unqualified(PurityString), [G1], purity_pure) - Context
+ Goal = call_expr(unqualified(PurityString), [G1], purity_pure)
+ - Context
).
:- pred append_to_disjunct(goal::in, goal_expr::in, prog_context::in,
goal::out) is det.
append_to_disjunct(Disjunct0, Goal, Context, Disjunct) :-
- ( Disjunct0 = (A0 ; B0) - Context2 ->
+ ( Disjunct0 = disj_expr(A0, B0) - Context2 ->
append_to_disjunct(A0, Goal, Context, A),
append_to_disjunct(B0, Goal, Context, B),
- Disjunct = (A ; B) - Context2
+ Disjunct = disj_expr(A, B) - Context2
;
- Disjunct = (Disjunct0, Goal - Context) - Context
+ Disjunct = conj_expr(Disjunct0, Goal - Context) - Context
).
:- pred parse_some_vars_dcg_goal(term::in, list(prog_var)::out,
@@ -464,8 +455,9 @@
Var1 = Var2
->
new_dcg_var(!VarSet, !Counter, Var),
- Unify = unify(term.variable(Var), term.variable(Var2), purity_pure),
- Then = (Then1, Unify - Context) - Context
+ Unify = unify_expr(term.variable(Var), term.variable(Var2),
+ purity_pure),
+ Then = conj_expr(Then1, Unify - Context) - Context
;
Then = Then1,
Var = Var2
@@ -486,16 +478,16 @@
Else = Else1
; VarThen = Var0 ->
Var = VarElse,
- Unify = unify(term.variable(Var), term.variable(VarThen),
+ Unify = unify_expr(term.variable(Var), term.variable(VarThen),
purity_pure),
- Then = (Then1, Unify - Context) - Context,
+ Then = conj_expr(Then1, Unify - Context) - Context,
Else = Else1
; VarElse = Var0 ->
Var = VarThen,
Then = Then1,
- Unify = unify(term.variable(Var), term.variable(VarElse),
+ Unify = unify_expr(term.variable(Var), term.variable(VarElse),
purity_pure),
- Else = (Else1, Unify - Context) - Context
+ Else = conj_expr(Else1, Unify - Context) - Context
;
% We prefer to substitute the then part since it is likely to be
% smaller than the else part, since the else part may have a deeply
@@ -510,7 +502,7 @@
prog_util.rename_in_goal(VarThen, VarElse, Then1, Then),
Else = Else1
),
- Goal = if_then_else(SomeVars, StateVars, Cond, Then, Else) - Context.
+ Goal = if_then_else_expr(SomeVars, StateVars, Cond, Then, Else) - Context.
% term_list_append_term(ListTerm, Term, Result):
%
Index: compiler/prog_io_goal.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/prog_io_goal.m,v
retrieving revision 1.41
diff -u -b -r1.41 prog_io_goal.m
--- compiler/prog_io_goal.m 17 Mar 2006 01:40:36 -0000 1.41
+++ compiler/prog_io_goal.m 20 Mar 2006 09:13:12 -0000
@@ -119,12 +119,13 @@
% Check for predicate calls.
sym_name_and_args(ArgsTerm, SymName, Args)
->
- Goal = call(SymName, Args, purity_pure) - Context
+ Goal = call_expr(SymName, Args, purity_pure) - Context
;
% A call to a free variable, or to a number or string.
% Just translate it into a call to call/1 - the
% typechecker will catch calls to numbers and strings.
- Goal = call(unqualified("call"), [ArgsTerm], purity_pure) - Context
+ Goal = call_expr(unqualified("call"), [ArgsTerm], purity_pure)
+ - Context
)
).
@@ -138,15 +139,15 @@
% for the moment we'll just disallow it.
% For consistency we also disallow if-then without the else.
-parse_goal_2("true", [], true, !V).
-parse_goal_2("fail", [], fail, !V).
-parse_goal_2("=", [A0, B0], unify(A, B, purity_pure), !V) :-
+parse_goal_2("true", [], true_expr, !V).
+parse_goal_2("fail", [], fail_expr, !V).
+parse_goal_2("=", [A0, B0], unify_expr(A, B, purity_pure), !V) :-
term.coerce(A0, A),
term.coerce(B0, B).
-parse_goal_2(",", [A0, B0], (A, B), !V) :-
+parse_goal_2(",", [A0, B0], conj_expr(A, B), !V) :-
parse_goal(A0, A, !V),
parse_goal(B0, B, !V).
-parse_goal_2("&", [A0, B0], (A & B), !V) :-
+parse_goal_2("&", [A0, B0], par_conj_expr(A, B), !V) :-
parse_goal(A0, A, !V),
parse_goal(B0, B, !V).
parse_goal_2(";", [A0, B0], R, !V) :-
@@ -154,23 +155,24 @@
parse_some_vars_goal(X0, Vars, StateVars, X, !V),
parse_goal(Y0, Y, !V),
parse_goal(B0, B, !V),
- R = if_then_else(Vars, StateVars, X, Y, B)
+ R = if_then_else_expr(Vars, StateVars, X, Y, B)
;
parse_goal(A0, A, !V),
parse_goal(B0, B, !V),
- R = (A;B)
+ R = disj_expr(A, B)
).
-parse_goal_2("else", [IF, C0], if_then_else(Vars, StateVars, A, B, C), !V) :-
+parse_goal_2("else", [IF, C0], if_then_else_expr(Vars, StateVars, A, B, C),
+ !V) :-
IF = term.functor(term.atom("if"),
[term.functor(term.atom("then"), [A0, B0], _)], _),
parse_some_vars_goal(A0, Vars, StateVars, A, !V),
parse_goal(B0, B, !V),
parse_goal(C0, C, !V).
-parse_goal_2("not", [A0], not(A), !V) :-
+parse_goal_2("not", [A0], not_expr(A), !V) :-
parse_goal(A0, A, !V).
-parse_goal_2("\\+", [A0], not(A), !V) :-
+parse_goal_2("\\+", [A0], not_expr(A), !V) :-
parse_goal(A0, A, !V).
parse_goal_2("all", [QVars, A0], GoalExpr, !V):-
@@ -185,27 +187,27 @@
Vars = [], StateVars = [],
GoalExpr = GoalExprA
;
- Vars = [], StateVars = [_|_],
- GoalExpr = all_state_vars(StateVars, A)
+ Vars = [], StateVars = [_ | _],
+ GoalExpr = all_state_vars_expr(StateVars, A)
;
- Vars = [_|_], StateVars = [],
- GoalExpr = all(Vars, A)
+ Vars = [_ | _], StateVars = [],
+ GoalExpr = all_expr(Vars, A)
;
- Vars = [_|_], StateVars = [_|_],
- GoalExpr = all(Vars, all_state_vars(StateVars, A) - ContextA)
+ Vars = [_ | _], StateVars = [_ | _],
+ GoalExpr = all_expr(Vars, all_state_vars_expr(StateVars, A) - ContextA)
).
% Handle implication.
-parse_goal_2("<=", [A0, B0], implies(B, A), !V):-
+parse_goal_2("<=", [A0, B0], implies_expr(B, A), !V):-
parse_goal(A0, A, !V),
parse_goal(B0, B, !V).
-parse_goal_2("=>", [A0, B0], implies(A, B), !V):-
+parse_goal_2("=>", [A0, B0], implies_expr(A, B), !V):-
parse_goal(A0, A, !V),
parse_goal(B0, B, !V).
% handle equivalence
-parse_goal_2("<=>", [A0, B0], equivalent(A, B), !V):-
+parse_goal_2("<=>", [A0, B0], equivalent_expr(A, B), !V):-
parse_goal(A0, A, !V),
parse_goal(B0, B, !V).
@@ -217,17 +219,22 @@
parse_goal(A0, A @ (GoalExprA - ContextA), !V),
(
- Vars = [], StateVars = [],
+ Vars = [],
+ StateVars = [],
GoalExpr = GoalExprA
;
- Vars = [], StateVars = [_|_],
- GoalExpr = some_state_vars(StateVars, A)
+ Vars = [],
+ StateVars = [_ | _],
+ GoalExpr = some_state_vars_expr(StateVars, A)
;
- Vars = [_|_], StateVars = [],
- GoalExpr = some(Vars, A)
+ Vars = [_ | _],
+ StateVars = [],
+ GoalExpr = some_expr(Vars, A)
;
- Vars = [_|_], StateVars = [_|_],
- GoalExpr = some(Vars, some_state_vars(StateVars, A) - ContextA)
+ Vars = [_ | _],
+ StateVars = [_ | _],
+ GoalExpr = some_expr(Vars, some_state_vars_expr(StateVars, A)
+ - ContextA)
).
parse_goal_2("promise_equivalent_solutions", [OVars, A0], GoalExpr, !V):-
@@ -236,36 +243,58 @@
list.map(term.coerce_var, Vars0, Vars),
list.map(term.coerce_var, DotSVars0, DotSVars),
list.map(term.coerce_var, ColonSVars0, ColonSVars),
- GoalExpr = promise_equivalent_solutions(Vars, DotSVars, ColonSVars, A).
+ GoalExpr = promise_equivalent_solutions_expr(Vars,
+ DotSVars, ColonSVars, A).
+
+parse_goal_2("promise_equivalent_solution_sets", [OVars, A0], GoalExpr, !V):-
+ parse_goal(A0, A, !V),
+ parse_vars_and_state_vars(OVars, Vars0, DotSVars0, ColonSVars0),
+ list.map(term.coerce_var, Vars0, Vars),
+ list.map(term.coerce_var, DotSVars0, DotSVars),
+ list.map(term.coerce_var, ColonSVars0, ColonSVars),
+ GoalExpr = promise_equivalent_solution_sets_expr(Vars,
+ DotSVars, ColonSVars, A).
+
+parse_goal_2("arbitrary", [OVars, A0], GoalExpr, !V):-
+ parse_goal(A0, A, !V),
+ parse_vars_and_state_vars(OVars, Vars0, DotSVars0, ColonSVars0),
+ list.map(term.coerce_var, Vars0, Vars),
+ list.map(term.coerce_var, DotSVars0, DotSVars),
+ list.map(term.coerce_var, ColonSVars0, ColonSVars),
+ GoalExpr = promise_equivalent_solution_arbitrary_expr(Vars,
+ DotSVars, ColonSVars, A).
parse_goal_2("promise_pure", [A0], GoalExpr, !V):-
parse_goal(A0, A, !V),
- GoalExpr = promise_purity(dont_make_implicit_promises, purity_pure, A).
+ GoalExpr = promise_purity_expr(dont_make_implicit_promises,
+ purity_pure, A).
parse_goal_2("promise_semipure", [A0], GoalExpr, !V):-
parse_goal(A0, A, !V),
- GoalExpr = promise_purity(dont_make_implicit_promises, purity_semipure, A).
+ GoalExpr = promise_purity_expr(dont_make_implicit_promises,
+ purity_semipure, A).
parse_goal_2("promise_impure", [A0], GoalExpr, !V):-
parse_goal(A0, A, !V),
- GoalExpr = promise_purity(dont_make_implicit_promises, purity_impure, A).
+ GoalExpr = promise_purity_expr(dont_make_implicit_promises,
+ purity_impure, A).
parse_goal_2("promise_pure_implicit", [A0], GoalExpr, !V):-
parse_goal(A0, A, !V),
- GoalExpr = promise_purity(make_implicit_promises, purity_pure, A).
+ GoalExpr = promise_purity_expr(make_implicit_promises, purity_pure, A).
parse_goal_2("promise_semipure_implicit", [A0], GoalExpr, !V):-
parse_goal(A0, A, !V),
- GoalExpr = promise_purity(make_implicit_promises, purity_semipure, A).
+ GoalExpr = promise_purity_expr(make_implicit_promises, purity_semipure, A).
parse_goal_2("promise_impure_implicit", [A0], GoalExpr, !V):-
parse_goal(A0, A, !V),
- GoalExpr = promise_purity(make_implicit_promises, purity_impure, A).
+ GoalExpr = promise_purity_expr(make_implicit_promises, purity_impure, A).
% The following is a temporary hack to handle `is' in the parser -
% we ought to handle it in the code generation - but then `is/2' itself
% is a bit of a hack.
-parse_goal_2("is", [A0, B0], unify(A, B, purity_pure), !V) :-
+parse_goal_2("is", [A0, B0], unify_expr(A, B, purity_pure), !V) :-
term.coerce(A0, A),
term.coerce(B0, B).
parse_goal_2("impure", [A0], A, !V) :-
@@ -278,17 +307,17 @@
parse_goal_with_purity(A0, Purity, A, !V) :-
parse_goal(A0, A1, !V),
- ( A1 = call(Pred, Args, purity_pure) - _ ->
- A = call(Pred, Args, Purity)
- ; A1 = unify(ProgTerm1, ProgTerm2, purity_pure) - _ ->
- A = unify(ProgTerm1, ProgTerm2, Purity)
+ ( A1 = call_expr(Pred, Args, purity_pure) - _ ->
+ A = call_expr(Pred, Args, Purity)
+ ; A1 = unify_expr(ProgTerm1, ProgTerm2, purity_pure) - _ ->
+ A = unify_expr(ProgTerm1, ProgTerm2, Purity)
;
% Inappropriate placement of an impurity marker, so we treat
% it like a predicate call. typecheck.m prints out something
% descriptive for these errors.
purity_name(Purity, PurityString),
term.coerce(A0, A2),
- A = call(unqualified(PurityString), [A2], purity_pure)
+ A = call_expr(unqualified(PurityString), [A2], purity_pure)
).
%-----------------------------------------------------------------------------%
@@ -386,7 +415,7 @@
list(mer_mode)::out) is semidet.
parse_pred_expr_args([], [], []).
-parse_pred_expr_args([Term|Terms], [Arg|Args], [Mode|Modes]) :-
+parse_pred_expr_args([Term | Terms], [Arg | Args], [Mode | Modes]) :-
parse_lambda_arg(Term, Arg, Mode),
parse_pred_expr_args(Terms, Args, Modes).
@@ -403,7 +432,7 @@
convert_mode(allow_constrained_inst_var, DCGModeTermB, DCGModeB0),
constrain_inst_vars_in_mode(DCGModeA0, DCGModeA),
constrain_inst_vars_in_mode(DCGModeB0, DCGModeB).
-parse_dcg_pred_expr_args([Term|Terms], [Arg|Args], [Mode|Modes]) :-
+parse_dcg_pred_expr_args([Term | Terms], [Arg | Args], [Mode | Modes]) :-
Terms = [_, _ | _],
parse_lambda_arg(Term, Arg, Mode),
parse_dcg_pred_expr_args(Terms, Args, Modes).
Index: compiler/prog_item.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/prog_item.m,v
retrieving revision 1.8
diff -u -b -r1.8 prog_item.m
--- compiler/prog_item.m 20 Mar 2006 22:24:28 -0000 1.8
+++ compiler/prog_item.m 20 Mar 2006 23:59:55 -0000
@@ -622,49 +622,59 @@
:- type goal_expr
% conjunctions
- ---> (goal , goal) % (non-empty) conjunction
- ; true % empty conjunction
- ; {goal & goal} % parallel conjunction
- % (The curly braces just quote the '&'/2.)
+ ---> conj_expr(goal, goal)
+ % (non-empty) conjunction
+ ; true_expr % empty conjunction
+ ; par_conj_expr(goal, goal)
+ % parallel conjunction
% disjunctions
- ; {goal ; goal} % (non-empty) disjunction
- % (The curly braces just quote the ';'/2.)
- ; fail % empty disjunction
+ ; disj_expr(goal, goal)
+ % (non-empty) disjunction
+ ; fail_expr % empty disjunction
% quantifiers
- ; { some(prog_vars, goal) }
+ ; some_expr(prog_vars, goal)
% existential quantification
- % (The curly braces just quote the 'some'/2.)
- ; all(prog_vars, goal)
- % % universal quantification
- ; some_state_vars(prog_vars, goal)
- ; all_state_vars(prog_vars, goal)
+ ; all_expr(prog_vars, goal)
+ % universal quantification
+ ; some_state_vars_expr(prog_vars, goal)
+ ; all_state_vars_expr(prog_vars, goal)
% state variables extracted from
% some/2 and all/2 quantifiers.
% other scopes
- ; promise_purity(implicit_purity_promise, purity, goal)
- ; promise_equivalent_solutions(prog_vars, prog_vars, prog_vars, goal)
- % (OrdinaryVars, DotStateVars, ColonStateVars,
- % % Goal)
+ ; promise_purity_expr(implicit_purity_promise, purity, goal)
+ ; promise_equivalent_solutions_expr(
+ prog_vars, % OrdinaryVars
+ prog_vars, % DotStateVars
+ prog_vars, % ColonStateVars
+ goal)
+ ; promise_equivalent_solution_sets_expr(
+ prog_vars, % OrdinaryVars
+ prog_vars, % DotStateVars
+ prog_vars, % ColonStateVars
+ goal)
+ ; promise_equivalent_solution_arbitrary_expr(
+ prog_vars, % OrdinaryVars
+ prog_vars, % DotStateVars
+ prog_vars, % ColonStateVars
+ goal)
% implications
- ; implies(goal, goal)
+ ; implies_expr(goal, goal)
% A => B
- ; equivalent(goal, goal)
+ ; equivalent_expr(goal, goal)
% A <=> B
% negation and if-then-else
- ; not(goal)
- ; if_then(prog_vars, prog_vars, goal, goal)
- % if_then(SomeVars, StateVars, If, Then)
- ; if_then_else(prog_vars, prog_vars, goal, goal, goal)
+ ; not_expr(goal)
+ ; if_then_else_expr(prog_vars, prog_vars, goal, goal, goal)
% if_then_else(SomeVars, StateVars, If, Then, Else)
% atomic goals
- ; call(sym_name, list(prog_term), purity)
- ; unify(prog_term, prog_term, purity).
+ ; call_expr(sym_name, list(prog_term), purity)
+ ; unify_expr(prog_term, prog_term, purity).
%-----------------------------------------------------------------------------%
%
Index: compiler/prog_util.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/prog_util.m,v
retrieving revision 1.84
diff -u -b -r1.84 prog_util.m
--- compiler/prog_util.m 17 Mar 2006 01:40:38 -0000 1.84
+++ compiler/prog_util.m 20 Mar 2006 14:46:40 -0000
@@ -356,79 +356,90 @@
:- pred rename_in_goal_expr(prog_var::in, prog_var::in,
goal_expr::in, goal_expr::out) is det.
-rename_in_goal_expr(OldVar, NewVar, (GoalA0, GoalB0),
- (GoalA, GoalB)) :-
+rename_in_goal_expr(OldVar, NewVar, conj_expr(GoalA0, GoalB0),
+ conj_expr(GoalA, GoalB)) :-
rename_in_goal(OldVar, NewVar, GoalA0, GoalA),
rename_in_goal(OldVar, NewVar, GoalB0, GoalB).
-rename_in_goal_expr(OldVar, NewVar, (GoalA0 & GoalB0),
- (GoalA & GoalB)) :-
+rename_in_goal_expr(OldVar, NewVar, par_conj_expr(GoalA0, GoalB0),
+ par_conj_expr(GoalA, GoalB)) :-
rename_in_goal(OldVar, NewVar, GoalA0, GoalA),
rename_in_goal(OldVar, NewVar, GoalB0, GoalB).
-rename_in_goal_expr(_OldVar, _NewVar, true, true).
-rename_in_goal_expr(OldVar, NewVar, (GoalA0; GoalB0),
- (GoalA; GoalB)) :-
+rename_in_goal_expr(_OldVar, _NewVar, true_expr, true_expr).
+rename_in_goal_expr(OldVar, NewVar, disj_expr(GoalA0, GoalB0),
+ disj_expr(GoalA, GoalB)) :-
rename_in_goal(OldVar, NewVar, GoalA0, GoalA),
rename_in_goal(OldVar, NewVar, GoalB0, GoalB).
-rename_in_goal_expr(_Var, _NewVar, fail, fail).
-rename_in_goal_expr(OldVar, NewVar, not(Goal0), not(Goal)) :-
+rename_in_goal_expr(_Var, _NewVar, fail_expr, fail_expr).
+rename_in_goal_expr(OldVar, NewVar, not_expr(Goal0), not_expr(Goal)) :-
rename_in_goal(OldVar, NewVar, Goal0, Goal).
-rename_in_goal_expr(OldVar, NewVar, some(Vars0, Goal0),
- some(Vars, Goal)) :-
+rename_in_goal_expr(OldVar, NewVar, some_expr(Vars0, Goal0),
+ some_expr(Vars, Goal)) :-
rename_in_vars(OldVar, NewVar, Vars0, Vars),
rename_in_goal(OldVar, NewVar, Goal0, Goal).
-rename_in_goal_expr(OldVar, NewVar, some_state_vars(Vars0, Goal0),
- some_state_vars(Vars, Goal)) :-
+rename_in_goal_expr(OldVar, NewVar, some_state_vars_expr(Vars0, Goal0),
+ some_state_vars_expr(Vars, Goal)) :-
rename_in_vars(OldVar, NewVar, Vars0, Vars),
rename_in_goal(OldVar, NewVar, Goal0, Goal).
-rename_in_goal_expr(OldVar, NewVar, all(Vars0, Goal0),
- all(Vars, Goal)) :-
+rename_in_goal_expr(OldVar, NewVar, all_expr(Vars0, Goal0),
+ all_expr(Vars, Goal)) :-
rename_in_vars(OldVar, NewVar, Vars0, Vars),
rename_in_goal(OldVar, NewVar, Goal0, Goal).
-rename_in_goal_expr(OldVar, NewVar, all_state_vars(Vars0, Goal0),
- all_state_vars(Vars, Goal)) :-
+rename_in_goal_expr(OldVar, NewVar, all_state_vars_expr(Vars0, Goal0),
+ all_state_vars_expr(Vars, Goal)) :-
rename_in_vars(OldVar, NewVar, Vars0, Vars),
rename_in_goal(OldVar, NewVar, Goal0, Goal).
rename_in_goal_expr(OldVar, NewVar,
- promise_purity(Implicit, Purity, Goal0),
- promise_purity(Implicit, Purity, Goal)) :-
+ promise_purity_expr(Implicit, Purity, Goal0),
+ promise_purity_expr(Implicit, Purity, Goal)) :-
rename_in_goal(OldVar, NewVar, Goal0, Goal).
rename_in_goal_expr(OldVar, NewVar,
- promise_equivalent_solutions(Vars0, DotSVars0, ColonSVars0,
+ promise_equivalent_solutions_expr(Vars0, DotSVars0, ColonSVars0,
Goal0),
- promise_equivalent_solutions(Vars, DotSVars, ColonSVars,
+ promise_equivalent_solutions_expr(Vars, DotSVars, ColonSVars,
Goal)) :-
rename_in_vars(OldVar, NewVar, Vars0, Vars),
rename_in_vars(OldVar, NewVar, DotSVars0, DotSVars),
rename_in_vars(OldVar, NewVar, ColonSVars0, ColonSVars),
rename_in_goal(OldVar, NewVar, Goal0, Goal).
-rename_in_goal_expr(OldVar, NewVar, implies(GoalA0, GoalB0),
- implies(GoalA, GoalB)) :-
+rename_in_goal_expr(OldVar, NewVar,
+ promise_equivalent_solution_sets_expr(Vars0, DotSVars0, ColonSVars0,
+ Goal0),
+ promise_equivalent_solution_sets_expr(Vars, DotSVars, ColonSVars,
+ Goal)) :-
+ rename_in_vars(OldVar, NewVar, Vars0, Vars),
+ rename_in_vars(OldVar, NewVar, DotSVars0, DotSVars),
+ rename_in_vars(OldVar, NewVar, ColonSVars0, ColonSVars),
+ rename_in_goal(OldVar, NewVar, Goal0, Goal).
+rename_in_goal_expr(OldVar, NewVar,
+ promise_equivalent_solution_arbitrary_expr(Vars0,
+ DotSVars0, ColonSVars0, Goal0),
+ promise_equivalent_solution_arbitrary_expr(Vars,
+ DotSVars, ColonSVars, Goal)) :-
+ rename_in_vars(OldVar, NewVar, Vars0, Vars),
+ rename_in_vars(OldVar, NewVar, DotSVars0, DotSVars),
+ rename_in_vars(OldVar, NewVar, ColonSVars0, ColonSVars),
+ rename_in_goal(OldVar, NewVar, Goal0, Goal).
+rename_in_goal_expr(OldVar, NewVar, implies_expr(GoalA0, GoalB0),
+ implies_expr(GoalA, GoalB)) :-
rename_in_goal(OldVar, NewVar, GoalA0, GoalA),
rename_in_goal(OldVar, NewVar, GoalB0, GoalB).
-rename_in_goal_expr(OldVar, NewVar, equivalent(GoalA0, GoalB0),
- equivalent(GoalA, GoalB)) :-
+rename_in_goal_expr(OldVar, NewVar, equivalent_expr(GoalA0, GoalB0),
+ equivalent_expr(GoalA, GoalB)) :-
rename_in_goal(OldVar, NewVar, GoalA0, GoalA),
rename_in_goal(OldVar, NewVar, GoalB0, GoalB).
rename_in_goal_expr(OldVar, NewVar,
- if_then(Vars0, StateVars0, Cond0, Then0),
- if_then(Vars, StateVars, Cond, Then)) :-
- rename_in_vars(OldVar, NewVar, Vars0, Vars),
- rename_in_vars(OldVar, NewVar, StateVars0, StateVars),
- rename_in_goal(OldVar, NewVar, Cond0, Cond),
- rename_in_goal(OldVar, NewVar, Then0, Then).
-rename_in_goal_expr(OldVar, NewVar,
- if_then_else(Vars0, StateVars0, Cond0, Then0, Else0),
- if_then_else(Vars, StateVars, Cond, Then, Else)) :-
+ if_then_else_expr(Vars0, StateVars0, Cond0, Then0, Else0),
+ if_then_else_expr(Vars, StateVars, Cond, Then, Else)) :-
rename_in_vars(OldVar, NewVar, Vars0, Vars),
rename_in_vars(OldVar, NewVar, StateVars0, StateVars),
rename_in_goal(OldVar, NewVar, Cond0, Cond),
rename_in_goal(OldVar, NewVar, Then0, Then),
rename_in_goal(OldVar, NewVar, Else0, Else).
-rename_in_goal_expr(OldVar, NewVar, call(SymName, Terms0, Purity),
- call(SymName, Terms, Purity)) :-
+rename_in_goal_expr(OldVar, NewVar, call_expr(SymName, Terms0, Purity),
+ call_expr(SymName, Terms, Purity)) :-
term.substitute_list(Terms0, OldVar, term.variable(NewVar), Terms).
-rename_in_goal_expr(OldVar, NewVar, unify(TermA0, TermB0, Purity),
- unify(TermA, TermB, Purity)) :-
+rename_in_goal_expr(OldVar, NewVar, unify_expr(TermA0, TermB0, Purity),
+ unify_expr(TermA, TermB, Purity)) :-
term.substitute(TermA0, OldVar, term.variable(NewVar), TermA),
term.substitute(TermB0, OldVar, term.variable(NewVar), TermB).
Index: compiler/saved_vars.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/saved_vars.m,v
retrieving revision 1.59
diff -u -b -r1.59 saved_vars.m
--- compiler/saved_vars.m 17 Mar 2006 01:40:39 -0000 1.59
+++ compiler/saved_vars.m 20 Mar 2006 14:53:03 -0000
@@ -227,7 +227,6 @@
ok_to_duplicate(dont_warn_singleton) = yes.
ok_to_duplicate(mode_check_clauses_goal) = yes.
ok_to_duplicate(will_not_modify_trail) = yes.
-ok_to_duplicate(promise_same_deconstruct) = yes.
% Divide a list of goals into an initial subsequence of goals
% that construct constants, and all other goals.
Index: compiler/simplify.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/simplify.m,v
retrieving revision 1.169
diff -u -b -r1.169 simplify.m
--- compiler/simplify.m 17 Mar 2006 01:40:40 -0000 1.169
+++ compiler/simplify.m 20 Mar 2006 09:51:51 -0000
@@ -347,7 +347,7 @@
simplify_info_set_module_info(ModuleInfo3, !Info),
simplify_info_get_det_info(!.Info, DetInfo),
- det_infer_goal(Goal3, Goal, InstMap0, SolnContext, [], DetInfo,
+ det_infer_goal(Goal3, Goal, InstMap0, SolnContext, [], no, DetInfo,
_, _, _)
;
Goal = Goal3
cvs diff: Diffing compiler/notes
cvs diff: Diffing debian
cvs diff: Diffing debian/patches
cvs diff: Diffing deep_profiler
cvs diff: Diffing deep_profiler/notes
cvs diff: Diffing doc
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.347
diff -u -b -r1.347 reference_manual.texi
--- doc/reference_manual.texi 19 Mar 2006 23:50:34 -0000 1.347
+++ doc/reference_manual.texi 21 Mar 2006 00:18:57 -0000
@@ -475,7 +475,9 @@
<=> xfy 920
=> xfy 920
all fxy 950
+arbitrary fxy 950
promise_equivalent_solutions fxy 950
+promise_equivalent_solution_sets fxy 950
promise_exclusive fy 950
promise_exclusive_exhaustive fy 950
promise_exhaustive fy 950
@@ -776,6 +778,50 @@
If @var{Goal} has determinism @samp{nondet} or @samp{cc_nondet} then
@code{promise_equivalent_solutions @var{Vars} @var{Goal}}
has determinism @samp{semidet}.
+
+ at item @code{promise_equivalent_solution_sets @var{Vars} @var{Goal}}
+A determinism cast,
+of the kind performed by @code{promise_equivalent_solutions},
+on any goals of the form
+ at code{arbitrary @var{ArbVars} @var{ArbGoal}} inside @var{Goal},
+of which there should be at least one.
+ at var{Vars} and @var{ArbVars} must be lists of variables,
+and @var{Goal} and @var{ArbGoal} must be valid goals.
+ at var{Vars} must be the set of variables bound by @var{Goal},
+and @var{ArbVars} must be the set of variables bound by @var{ArbGoal},
+It is an error for @var{Vars} to include a variable not bound by @var{Goal}
+or for @var{Goal} to bind a non-local variable
+that is not listed in @var{Vars},
+and similarly for @var{ArbVars} and @var{ArbGoal}.
+The intersection of @var{Vars} and the @var{ArbVars} list
+of any @code{arbitrary @var{ArbVars} @var{ArbGoal}} goal
+included inside @var{Goal} must be empty.
+
+The overall @var{promise_equivalent_solution_sets} goal promises that
+the set of solutions computed for @var{Vars} by @var{Goal}
+is not influenced by which of the possible solutions
+for @var{ArbVars} is computed by each @var{ArbGoal};
+while different choices of solutions for some of the @var{ArbGoal}s
+may lead to syntactically different solutions for @var{Vars} for @var{Goal},
+all of these solutions are equivalent
+with respect to the equality theories of the variables in @var{Vars}.
+If an @var{ArbGoal} has determinism @samp{multi} or @samp{cc_multi} then
+ at code{arbitrary @var{ArbVars} @var{ArbGoal}} has determinism @samp{det}.
+If @var{ArbGoal} has determinism @samp{nondet} or @samp{cc_nondet} then
+ at code{arbitrary @var{ArbVars} @var{ArbGoal}} has determinism @samp{semidet}.
+ at var{Goal} itself may have any determinism.
+
+There is no requirement that given one of the @var{ArbGoal}s,
+all its solutions must be equivalent with respect to the equality theories
+of the corresponding @var{ArbVars};
+in fact, in typical usage, this won't be the case.
+The different solutions of the nested @var{arbitrary} goals
+are not required to be equivalent in any context
+except the @var{promise_equivalent_solution_sets} goal they are nested inside.
+
+Goals of the form @code{arbitrary @var{ArbVars} @var{ArbGoal}}
+are not allowed to occur outside
+ at code{promise_equivalent_solution_sets @var{Vars} @var{Goal}} goals.
@item @code{@var{Call}}
Any goal which does not match any of the above forms
cvs diff: Diffing extras
cvs diff: Diffing extras/aditi
cvs diff: Diffing extras/cgi
cvs diff: Diffing extras/complex_numbers
cvs diff: Diffing extras/complex_numbers/samples
cvs diff: Diffing extras/complex_numbers/tests
cvs diff: Diffing extras/concurrency
cvs diff: Diffing extras/curs
cvs diff: Diffing extras/curs/samples
cvs diff: Diffing extras/curses
cvs diff: Diffing extras/curses/sample
cvs diff: Diffing extras/dynamic_linking
cvs diff: Diffing extras/error
cvs diff: Diffing extras/gator
cvs diff: Diffing extras/gator/generations
cvs diff: Diffing extras/gator/generations/1
cvs diff: Diffing extras/graphics
cvs diff: Diffing extras/graphics/easyx
cvs diff: Diffing extras/graphics/easyx/samples
cvs diff: Diffing extras/graphics/mercury_glut
cvs diff: Diffing extras/graphics/mercury_opengl
cvs diff: Diffing extras/graphics/mercury_tcltk
cvs diff: Diffing extras/graphics/samples
cvs diff: Diffing extras/graphics/samples/calc
cvs diff: Diffing extras/graphics/samples/gears
cvs diff: Diffing extras/graphics/samples/maze
cvs diff: Diffing extras/graphics/samples/pent
cvs diff: Diffing extras/lazy_evaluation
cvs diff: Diffing extras/lex
cvs diff: Diffing extras/lex/samples
cvs diff: Diffing extras/lex/tests
cvs diff: Diffing extras/logged_output
cvs diff: Diffing extras/moose
cvs diff: Diffing extras/moose/samples
cvs diff: Diffing extras/moose/tests
cvs diff: Diffing extras/morphine
cvs diff: Diffing extras/morphine/non-regression-tests
cvs diff: Diffing extras/morphine/scripts
cvs diff: Diffing extras/morphine/source
cvs diff: Diffing extras/odbc
cvs diff: Diffing extras/posix
cvs diff: Diffing extras/quickcheck
cvs diff: Diffing extras/quickcheck/tutes
cvs diff: Diffing extras/references
cvs diff: Diffing extras/references/samples
cvs diff: Diffing extras/references/tests
cvs diff: Diffing extras/solver_types
cvs diff: Diffing extras/solver_types/library
cvs diff: Diffing extras/stream
cvs diff: Diffing extras/trailed_update
cvs diff: Diffing extras/trailed_update/samples
cvs diff: Diffing extras/trailed_update/tests
cvs diff: Diffing extras/windows_installer_generator
cvs diff: Diffing extras/windows_installer_generator/sample
cvs diff: Diffing extras/windows_installer_generator/sample/images
cvs diff: Diffing extras/xml
cvs diff: Diffing extras/xml/samples
cvs diff: Diffing extras/xml_stylesheets
cvs diff: Diffing java
cvs diff: Diffing java/runtime
cvs diff: Diffing library
Index: library/ops.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/library/ops.m,v
retrieving revision 1.60
diff -u -b -r1.60 ops.m
--- library/ops.m 7 Mar 2006 22:23:46 -0000 1.60
+++ library/ops.m 8 Mar 2006 02:37:43 -0000
@@ -349,6 +349,10 @@
ops.op_table("promise_semipure_implicit", before, fx, 950).% Mercury extension
ops.op_table("promise_equivalent_solutions", before, fxy, 950).
% Mercury extension
+ops.op_table("promise_equivalent_solution_sets", before, fxy, 950).
+ % Mercury extension
+ops.op_table("arbitrary", before, fxy, 950).
+ % Mercury extension
ops.op_table("some", before, fxy, 950). % Mercury/NU-Prolog extension
ops.op_table("then", after, xfx, 1150). % Mercury/NU-Prolog extension
ops.op_table("type", before, fx, 1180). % Mercury extension
cvs diff: Diffing mdbcomp
cvs diff: Diffing profiler
cvs diff: Diffing robdd
cvs diff: Diffing runtime
cvs diff: Diffing runtime/GETOPT
cvs diff: Diffing runtime/machdeps
cvs diff: Diffing samples
cvs diff: Diffing samples/c_interface
cvs diff: Diffing samples/c_interface/c_calls_mercury
cvs diff: Diffing samples/c_interface/cplusplus_calls_mercury
cvs diff: Diffing samples/c_interface/mercury_calls_c
cvs diff: Diffing samples/c_interface/mercury_calls_cplusplus
cvs diff: Diffing samples/c_interface/mercury_calls_fortran
cvs diff: Diffing samples/c_interface/simpler_c_calls_mercury
cvs diff: Diffing samples/c_interface/simpler_cplusplus_calls_mercury
cvs diff: Diffing samples/diff
cvs diff: Diffing samples/muz
cvs diff: Diffing samples/rot13
cvs diff: Diffing samples/solutions
cvs diff: Diffing samples/tests
cvs diff: Diffing samples/tests/c_interface
cvs diff: Diffing samples/tests/c_interface/c_calls_mercury
cvs diff: Diffing samples/tests/c_interface/cplusplus_calls_mercury
cvs diff: Diffing samples/tests/c_interface/mercury_calls_c
cvs diff: Diffing samples/tests/c_interface/mercury_calls_cplusplus
cvs diff: Diffing samples/tests/c_interface/mercury_calls_fortran
cvs diff: Diffing samples/tests/c_interface/simpler_c_calls_mercury
cvs diff: Diffing samples/tests/c_interface/simpler_cplusplus_calls_mercury
cvs diff: Diffing samples/tests/diff
cvs diff: Diffing samples/tests/muz
cvs diff: Diffing samples/tests/rot13
cvs diff: Diffing samples/tests/solutions
cvs diff: Diffing samples/tests/toplevel
cvs diff: Diffing scripts
cvs diff: Diffing slice
cvs diff: Diffing tests
cvs diff: Diffing tests/benchmarks
cvs diff: Diffing tests/debugger
cvs diff: Diffing tests/debugger/declarative
cvs diff: Diffing tests/dppd
cvs diff: Diffing tests/general
cvs diff: Diffing tests/general/accumulator
cvs diff: Diffing tests/general/string_format
cvs diff: Diffing tests/general/structure_reuse
cvs diff: Diffing tests/grade_subdirs
cvs diff: Diffing tests/hard_coded
Index: tests/hard_coded/Mmakefile
===================================================================
RCS file: /home/mercury/mercury1/repository/tests/hard_coded/Mmakefile,v
retrieving revision 1.280
diff -u -b -r1.280 Mmakefile
--- tests/hard_coded/Mmakefile 8 Mar 2006 02:25:40 -0000 1.280
+++ tests/hard_coded/Mmakefile 20 Mar 2006 11:21:53 -0000
@@ -134,6 +134,7 @@
no_warn_singleton \
nullary_ho_func \
null_char \
+ one_member \
ppc_bug \
pprint_test \
pprint_test2 \
Index: tests/hard_coded/one_member.exp
===================================================================
RCS file: tests/hard_coded/one_member.exp
diff -N tests/hard_coded/one_member.exp
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/one_member.exp 20 Mar 2006 11:21:28 -0000
@@ -0,0 +1 @@
+["four", "one", "three", "two"]
Index: tests/hard_coded/one_member.m
===================================================================
RCS file: tests/hard_coded/one_member.m
diff -N tests/hard_coded/one_member.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/one_member.m 20 Mar 2006 11:13:58 -0000
@@ -0,0 +1,126 @@
+% vim:ts=4 sw=4 expandtab
+
+:- module one_member.
+
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+:- implementation.
+
+:- import_module list.
+:- import_module std_util.
+
+:- type set_ctree234(T)
+ ---> ct(int, set_tree234(T))
+ where equality is one_member.equal,
+ comparison is one_member.compare_total_order.
+
+:- type set_tree234(T)
+ ---> empty
+ ; two(T, set_tree234(T), set_tree234(T))
+ ; three(T, T, set_tree234(T), set_tree234(T), set_tree234(T))
+ ; four(T, T, T, set_tree234(T), set_tree234(T),
+ set_tree234(T), set_tree234(T)).
+
+main(!IO) :-
+ Set = ct(4, two("two", two("one", empty, empty),
+ three("three", "four", empty, empty, empty))),
+ solutions(one_member(Set), Solns),
+ io.write(Solns, !IO),
+ io.nl(!IO).
+
+:- pred one_member(set_ctree234(T)::in, T::out) is nondet.
+
+one_member(Set, Item) :-
+ promise_equivalent_solution_sets [Item] (
+ arbitrary [Tree] Set = ct(_, Tree),
+ do_one_member(Tree, Item)
+ ).
+
+:- pred do_one_member(set_tree234(T)::in, T::out) is nondet.
+
+do_one_member(empty, _) :- fail.
+do_one_member(two(E0, T0, T1), E) :-
+ (
+ E = E0
+ ;
+ do_one_member(T0, E)
+ ;
+ do_one_member(T1, E)
+ ).
+do_one_member(three(E0, E1, T0, T1, T2), E) :-
+ (
+ E = E0
+ ;
+ E = E1
+ ;
+ do_one_member(T0, E)
+ ;
+ do_one_member(T1, E)
+ ;
+ do_one_member(T2, E)
+ ).
+do_one_member(four(E0, E1, E2, T0, T1, T2, T3), E) :-
+ (
+ E = E0
+ ;
+ E = E1
+ ;
+ E = E2
+ ;
+ do_one_member(T0, E)
+ ;
+ do_one_member(T1, E)
+ ;
+ do_one_member(T2, E)
+ ;
+ do_one_member(T3, E)
+ ).
+
+:- pred equal(set_ctree234(T)::in, set_ctree234(T)::in) is semidet.
+
+equal(SetA, SetB) :-
+ promise_equivalent_solution_sets [] (
+ arbitrary [SizeA, TreeA] SetA = ct(SizeA, TreeA),
+ arbitrary [SizeB, TreeB] SetB = ct(SizeB, TreeB),
+ SizeA = SizeB,
+ do_to_sorted_list(TreeA, [], ListA),
+ do_to_sorted_list(TreeB, [], ListB),
+ ListA = ListB
+ ).
+
+:- pred compare_total_order(comparison_result::uo,
+ set_ctree234(T)::in, set_ctree234(T)::in) is det.
+
+compare_total_order(Result, SetA, SetB) :-
+ promise_equivalent_solution_sets [Result] (
+ arbitrary [SizeA, TreeA] SetA = ct(SizeA, TreeA),
+ arbitrary [SizeB, TreeB] SetB = ct(SizeB, TreeB),
+ ( SizeA = SizeB ->
+ do_to_sorted_list(TreeA, [], ListA),
+ do_to_sorted_list(TreeB, [], ListB),
+ compare(Result, ListA, ListB)
+ ;
+ compare(Result, SizeA, SizeB)
+ )
+ ).
+
+:- pred do_to_sorted_list(set_tree234(T)::in, list(T)::in, list(T)::out)
+ is det.
+
+do_to_sorted_list(empty, L, L).
+do_to_sorted_list(two(E0, T0, T1), L0, L) :-
+ do_to_sorted_list(T1, L0, L1),
+ do_to_sorted_list(T0, [E0 | L1], L).
+do_to_sorted_list(three(E0, E1, T0, T1, T2), L0, L) :-
+ do_to_sorted_list(T2, L0, L1),
+ do_to_sorted_list(T1, [E1 | L1], L2),
+ do_to_sorted_list(T0, [E0 | L2], L).
+do_to_sorted_list(four(E0, E1, E2, T0, T1, T2, T3), L0, L) :-
+ do_to_sorted_list(T3, L0, L1),
+ do_to_sorted_list(T2, [E2 | L1], L2),
+ do_to_sorted_list(T1, [E1 | L2], L3),
+ do_to_sorted_list(T0, [E0 | L3], L).
cvs diff: Diffing tests/hard_coded/exceptions
cvs diff: Diffing tests/hard_coded/purity
cvs diff: Diffing tests/hard_coded/sub-modules
cvs diff: Diffing tests/hard_coded/typeclasses
cvs diff: Diffing tests/invalid
Index: tests/invalid/Mmakefile
===================================================================
RCS file: /home/mercury/mercury1/repository/tests/invalid/Mmakefile,v
retrieving revision 1.190
diff -u -b -r1.190 Mmakefile
--- tests/invalid/Mmakefile 8 Mar 2006 02:25:43 -0000 1.190
+++ tests/invalid/Mmakefile 20 Mar 2006 14:04:31 -0000
@@ -130,6 +130,7 @@
not_in_interface \
nullary_ho_func_error \
occurs \
+ one_member \
overloading \
polymorphic_unification \
pragma_c_code_dup_var \
Index: tests/invalid/one_member.err_exp
===================================================================
RCS file: tests/invalid/one_member.err_exp
diff -N tests/invalid/one_member.err_exp
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/invalid/one_member.err_exp 20 Mar 2006 11:30:29 -0000
@@ -0,0 +1,17 @@
+one_member.m:044: Error: this `arbitrary' scope is not nested inside a
+one_member.m:044: `promise_equivalent_solution_sets' scope.
+one_member.m:051: Error: this `arbitrary' scope and the
+one_member.m:051: `promise_equivalent_solution_sets' scope it is nested
+one_member.m:051: inside overlap on the variable Item.
+one_member.m:050: This is the outer `promise_equivalent_solution_sets' scope.
+one_member.m:051: Error: the `arbitrary' goal lists an extra variable: Tree.
+one_member.m:052: Error: unification for non-canonical type
+one_member.m:052: `one_member.set_ctree234/1' occurs in a context which
+one_member.m:052: requires all solutions.
+one_member.m:053: Call to do_one_member can fail.
+one_member.m:061: Error: `promise_equivalent_solution_sets' scope is nested
+one_member.m:061: inside another.
+one_member.m:060: This is the outer `promise_equivalent_solution_sets' scope.
+one_member.m:047: In `one_member2(in, out)':
+one_member.m:047: warning: determinism declaration could be tighter.
+one_member.m:047: Declared `nondet', inferred `semidet'.
Index: tests/invalid/one_member.m
===================================================================
RCS file: tests/invalid/one_member.m
diff -N tests/invalid/one_member.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/invalid/one_member.m 20 Mar 2006 11:26:20 -0000
@@ -0,0 +1,150 @@
+% vim:ts=4 sw=4 expandtab
+
+:- module one_member.
+
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+:- implementation.
+
+:- import_module list.
+:- import_module std_util.
+
+:- type set_ctree234(T)
+ ---> ct(int, set_tree234(T))
+ where equality is one_member.equal,
+ comparison is one_member.compare_total_order.
+
+:- type set_tree234(T)
+ ---> empty
+ ; two(T, set_tree234(T), set_tree234(T))
+ ; three(T, T, set_tree234(T), set_tree234(T), set_tree234(T))
+ ; four(T, T, T, set_tree234(T), set_tree234(T),
+ set_tree234(T), set_tree234(T)).
+
+main(!IO) :-
+ Set = ct(4, two("two", two("one", empty, empty),
+ three("three", "four", empty, empty, empty))),
+ solutions(one_member1(Set), Solns1),
+ io.write(Solns1, !IO),
+ io.nl(!IO),
+ solutions(one_member2(Set), Solns2),
+ io.write(Solns2, !IO),
+ io.nl(!IO),
+ solutions(one_member3(Set), Solns3),
+ io.write(Solns3, !IO),
+ io.nl(!IO).
+
+:- pred one_member1(set_ctree234(T)::in, T::out) is nondet.
+
+one_member1(Set, Item) :-
+ arbitrary [Tree] Set = ct(_, Tree),
+ do_one_member(Tree, Item).
+
+:- pred one_member2(set_ctree234(T)::in, T::out) is nondet.
+
+one_member2(Set, Item) :-
+ promise_equivalent_solution_sets [Item] (
+ arbitrary [Tree, Item] (
+ Set = ct(_, Tree),
+ do_one_member(Tree, Item)
+ )
+ ).
+
+:- pred one_member3(set_ctree234(T)::in, T::out) is nondet.
+
+one_member3(Set, Item) :-
+ promise_equivalent_solution_sets [Item] (
+ promise_equivalent_solution_sets [Item] (
+ arbitrary [Tree] Set = ct(_, Tree),
+ do_one_member(Tree, Item)
+ )
+ ).
+
+:- pred do_one_member(set_tree234(T)::in, T::out) is nondet.
+
+do_one_member(empty, _) :- fail.
+do_one_member(two(E0, T0, T1), E) :-
+ (
+ E = E0
+ ;
+ do_one_member(T0, E)
+ ;
+ do_one_member(T1, E)
+ ).
+do_one_member(three(E0, E1, T0, T1, T2), E) :-
+ (
+ E = E0
+ ;
+ E = E1
+ ;
+ do_one_member(T0, E)
+ ;
+ do_one_member(T1, E)
+ ;
+ do_one_member(T2, E)
+ ).
+do_one_member(four(E0, E1, E2, T0, T1, T2, T3), E) :-
+ (
+ E = E0
+ ;
+ E = E1
+ ;
+ E = E2
+ ;
+ do_one_member(T0, E)
+ ;
+ do_one_member(T1, E)
+ ;
+ do_one_member(T2, E)
+ ;
+ do_one_member(T3, E)
+ ).
+
+:- pred equal(set_ctree234(T)::in, set_ctree234(T)::in) is semidet.
+
+equal(SetA, SetB) :-
+ promise_equivalent_solution_sets [] (
+ arbitrary [SizeA, TreeA] SetA = ct(SizeA, TreeA),
+ arbitrary [SizeB, TreeB] SetB = ct(SizeB, TreeB),
+ SizeA = SizeB,
+ do_to_sorted_list(TreeA, [], ListA),
+ do_to_sorted_list(TreeB, [], ListB),
+ ListA = ListB
+ ).
+
+:- pred compare_total_order(comparison_result::uo,
+ set_ctree234(T)::in, set_ctree234(T)::in) is det.
+
+compare_total_order(Result, SetA, SetB) :-
+ promise_equivalent_solution_sets [Result] (
+ arbitrary [SizeA, TreeA] SetA = ct(SizeA, TreeA),
+ arbitrary [SizeB, TreeB] SetB = ct(SizeB, TreeB),
+ ( SizeA = SizeB ->
+ do_to_sorted_list(TreeA, [], ListA),
+ do_to_sorted_list(TreeB, [], ListB),
+ compare(Result, ListA, ListB)
+ ;
+ compare(Result, SizeA, SizeB)
+ )
+ ).
+
+:- pred do_to_sorted_list(set_tree234(T)::in, list(T)::in, list(T)::out)
+ is det.
+
+do_to_sorted_list(empty, L, L).
+do_to_sorted_list(two(E0, T0, T1), L0, L) :-
+ do_to_sorted_list(T1, L0, L1),
+ do_to_sorted_list(T0, [E0 | L1], L).
+do_to_sorted_list(three(E0, E1, T0, T1, T2), L0, L) :-
+ do_to_sorted_list(T2, L0, L1),
+ do_to_sorted_list(T1, [E1 | L1], L2),
+ do_to_sorted_list(T0, [E0 | L2], L).
+do_to_sorted_list(four(E0, E1, E2, T0, T1, T2, T3), L0, L) :-
+ do_to_sorted_list(T3, L0, L1),
+ do_to_sorted_list(T2, [E2 | L1], L2),
+ do_to_sorted_list(T1, [E1 | L2], L3),
+ do_to_sorted_list(T0, [E0 | L3], L).
Index: tests/invalid/promise_equivalent_solutions_test.err_exp
===================================================================
RCS file: /home/mercury/mercury1/repository/tests/invalid/promise_equivalent_solutions_test.err_exp,v
retrieving revision 1.2
diff -u -b -r1.2 promise_equivalent_solutions_test.err_exp
--- tests/invalid/promise_equivalent_solutions_test.err_exp 14 Sep 2005 05:26:50 -0000 1.2
+++ tests/invalid/promise_equivalent_solutions_test.err_exp 20 Mar 2006 13:06:19 -0000
@@ -1,7 +1,7 @@
promise_equivalent_solutions_test.m:018: Error: the
-promise_equivalent_solutions_test.m:018: promise_equivalent_solutions goal
+promise_equivalent_solutions_test.m:018: `promise_equivalent_solutions' goal
promise_equivalent_solutions_test.m:018: binds a variable that is not listed:
promise_equivalent_solutions_test.m:018: A.
promise_equivalent_solutions_test.m:033: Error: the
-promise_equivalent_solutions_test.m:033: promise_equivalent_solutions goal
+promise_equivalent_solutions_test.m:033: `promise_equivalent_solutions' goal
promise_equivalent_solutions_test.m:033: lists an extra variable: ASorted.
cvs diff: Diffing tests/invalid/purity
cvs diff: Diffing tests/misc_tests
cvs diff: Diffing tests/mmc_make
cvs diff: Diffing tests/mmc_make/lib
cvs diff: Diffing tests/recompilation
cvs diff: Diffing tests/tabling
cvs diff: Diffing tests/term
cvs diff: Diffing tests/trailing
cvs diff: Diffing tests/valid
cvs diff: Diffing tests/warnings
cvs diff: Diffing tools
cvs diff: Diffing trace
cvs diff: Diffing util
cvs diff: Diffing vim
cvs diff: Diffing vim/after
cvs diff: Diffing vim/ftplugin
cvs diff: Diffing vim/syntax
--------------------------------------------------------------------------
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