[m-rev.] For review: State Variable Transformation
Ralph Becket
rafe at cs.mu.OZ.AU
Mon Apr 8 17:17:50 AEST 2002
Estimated hours taken: 300
Branches: main
Added a new syntax to the language ("state variables") to simplify the
manipulation of threaded state. State variables are a better mechanism
for threading state than DCGs.
NEWS:
Mention the new syntax, giving a pointer to the appropriate part
of the Reference Manual
doc/reference_manual.texi:
Documented the new syntax in the Syntax chapter, just before the
section on DCGs.
library/builtin.m:
Deleted the declarations and definitions for !/0 and !/2.
library/lexer.m:
Changed `!' from being a special token to being a graphical token.
library/ops.m:
Added three new prefix operators, `!', `!.' and `!:'.
library/prolog.m:
Deleted the already commented out implementations for !/0 and !/2.
library/term.m:
Added the function term__var_id/1 which is used by
varset__new_uniquely_named_var/4.
library/varset.m:
Added varset__new_uniquely_named_var/4 which is similar to
varset__new_named_var/4, except that the variable name has a unique
number appended to it (the number is unique w.r.t. the varset.)
compiler/hlds_goal.m:
Added an implicit/1 constructor to unify_main_context. This is
intended for contexts where intermediary variables have been
introduced, such as in the state variable transformation.
compiler/hlds_out.m:
Added a clause to write_unify_main_context//4 to handle the new
implicit/1 constructor.
compiler/make_hlds.m:
Extended to implement the state variable transformation.
compiler/mercury_compile.m:
Removed two calls to !/2 (remnants of the original Prolog version...)
compiler/prog_io.m:
Amended parse_item/4 to first replace all !X arguments with the
pair of arguments, !.X and !:X.
Added the function expand_dot_colon_state_vars/1.
doc/reference_manual.texi:
Added documentation to cover the new state variable syntax.
Index: NEWS
===================================================================
RCS file: /home/mercury1/repository/mercury/NEWS,v
retrieving revision 1.254
diff -u -r1.254 NEWS
--- NEWS 15 Mar 2002 07:31:39 -0000 1.254
+++ NEWS 8 Apr 2002 06:50:36 -0000
@@ -29,6 +29,10 @@
Changes to the Mercury language:
+* A more general alternative to DCG syntax has been added to the language
+ to simplify the manipulation of threaded state. See the section on State
+ Variables in the Syntax chapter in the reference manual.
+
* If a higher-order function term has inst 'ground' it is now assumed to have
the standard higher-order function inst 'func(in, .., in) = out is det'.
This makes higher-order functional programming much easier, particularly when
@@ -107,10 +111,16 @@
Changes to the Mercury standard library:
+<<<<<<< NEWS
+* The builtin predicates !/0 and !/2 from Mercury's Prolog heritage have been
+ removed (`!' is now a prefix operator used in the state variable syntax).
+
+=======
* Performance bugs in `pprint__to_doc' have now been fixed. Even
very large terms can now be converted to docs and pretty printed without
causing a machine to thrash or run out of memory.
+>>>>>>> 1.254
* `io__read_file' and `io__read_file_as_string' now have better error
handling. The result types have changed, so code using these predicates
will need minor modifications.
Index: compiler/hlds_goal.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_goal.m,v
retrieving revision 1.95
diff -u -r1.95 hlds_goal.m
--- compiler/hlds_goal.m 28 Mar 2002 03:43:00 -0000 1.95
+++ compiler/hlds_goal.m 4 Apr 2002 06:27:51 -0000
@@ -479,6 +479,13 @@
; call(
call_id, % the name and arity of the predicate
int % the argument number (first arg == 1)
+ )
+
+ % a unification added by some syntactic transformation
+ % (e.g. for handling state variables.)
+ ; implicit(
+ string % used to explain the source of the
+ % unification
).
% A unify_sub_context describes the location of sub-unification
Index: compiler/hlds_out.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_out.m,v
retrieving revision 1.282
diff -u -r1.282 hlds_out.m
--- compiler/hlds_out.m 28 Mar 2002 03:43:01 -0000 1.282
+++ compiler/hlds_out.m 8 Apr 2002 06:14:50 -0000
@@ -645,6 +645,10 @@
hlds_out__write_call_arg_id(CallId, ArgNum, Markers),
io__write_string(":\n").
+hlds_out__write_unify_main_context(First, implicit(Source), Context, First) -->
+ hlds_out__start_in_message(First, Context),
+ io__format("implicit %s unification:\n", [s(Source)]).
+
:- pred hlds_out__write_unify_sub_contexts(bool, unify_sub_contexts,
prog_context, bool, io__state, io__state).
:- mode hlds_out__write_unify_sub_contexts(in, in, in, out, di, uo) is det.
Index: compiler/make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.407
diff -u -r1.407 make_hlds.m
--- compiler/make_hlds.m 28 Mar 2002 03:43:12 -0000 1.407
+++ compiler/make_hlds.m 8 Apr 2002 05:22:13 -0000
@@ -5552,10 +5552,17 @@
% pragma foreign code are disjoint, the
% unifications can be implemented as
% substitutions, and they will be.
+
+ % There won't be any state vars, so it doesn't matter much
+ % what we put here.
+ { DotColonSubst0 = new_dot_colon_subst },
+ { InAtom = yes(new_svar_subst) },
insert_arg_unifications(HeadVars, TermArgs, Context,
head(PredOrFunc, Arity), yes, HldsGoal0, VarSet1,
- HldsGoal1, VarSet2, transform_info(ModuleInfo1, Info0),
- transform_info(ModuleInfo, Info)),
+ HldsGoal1, VarSet2,
+ transform_info(ModuleInfo1, Info0),
+ transform_info(ModuleInfo, Info),
+ DotColonSubst0, _DotColonSubst, InAtom),
{
map__init(EmptyVarTypes),
implicitly_quantify_clause_body(HeadVars,
@@ -5598,25 +5605,41 @@
in, out, di, uo) is det.
transform(Subst, HeadVars, Args0, Body, VarSet0, Context, PredOrFunc,
- Arity, GoalType, Goal, VarSet, Warnings, Info0, Info) -->
- transform_goal(Body, VarSet0, Subst, Goal1, VarSet1, Info0, Info1),
+ Arity, _GoalType, Goal, VarSet, Warnings, Info0, Info) -->
+
{ term__apply_substitution_to_list(Args0, Subst, Args) },
-
- % The head variables of an assertion will always be
- % variables, so it is unnecessary to insert unifications.
- (
- { GoalType = promise(_) }
- ->
- { VarSet2 = VarSet1 },
- { Goal2 = Goal1 },
- { Info2 = Info0 }
- ;
- { ArgContext = head(PredOrFunc, Arity) },
- insert_arg_unifications(HeadVars, Args, Context, ArgContext,
- no, Goal1, VarSet1, Goal2, VarSet2, Info1, Info2)
- ),
- { VarTypes2 = Info2 ^ qual_info ^ vartypes },
- { implicitly_quantify_clause_body(HeadVars, Goal2, VarSet2, VarTypes2,
+
+ { ArgContext = head(PredOrFunc, Arity) },
+ { hlds_goal__true_goal(EmptyConj) },
+ { DotColonSubst0 = new_dot_colon_subst },
+ { HeadInAtom = yes(new_svar_subst) },
+ insert_arg_unifications(HeadVars, Args, Context, ArgContext,
+ no, EmptyConj, VarSet0, HeadGoal, VarSet1, Info0, Info1,
+ DotColonSubst0, HeadDotColonSubst, HeadInAtom),
+ %
+ % At this point, DotColonSubst contains the state variable
+ % mappings to logical variables for each state var X that
+ % appears (as !.X or !:X) in the Args. This information is
+ % used to "tie the knot" in the transformation of the Body.
+
+ % The mappings for !: state variables from the head specify
+ % the mappings for the live state variables after the body.
+ % To start with we assume the body is not an atomic formula.
+ %
+ { BodyInAtom = no(HeadDotColonSubst ^ colon_subst) },
+ transform_goal(Body, VarSet1, Subst, BodyGoal0, VarSet2, Info1, Info2,
+ DotColonSubst0, BodyDotColonSubst0, BodyInAtom),
+ { insert_dot_svar_unifications(Context,
+ BodyDotColonSubst0, _BodyDotColonSubst,
+ no(HeadDotColonSubst ^ dot_subst), BodyGoal0, BodyGoal) },
+
+ { goal_info_init(Context, GoalInfo) },
+ { goal_to_conj_list(HeadGoal, HeadGoals) },
+ { goal_to_conj_list(BodyGoal, BodyGoals) },
+ { conj_list_to_goal(HeadGoals ++ BodyGoals, GoalInfo, Goal0) },
+
+ { VarTypes0 = Info2 ^ qual_info ^ vartypes },
+ { implicitly_quantify_clause_body(HeadVars, Goal0, VarSet2, VarTypes0,
Goal, VarSet, VarTypes, Warnings) },
{ Info = Info2 ^ qual_info ^ vartypes := VarTypes }.
@@ -5632,89 +5655,129 @@
:- pred transform_goal(goal, prog_varset, prog_substitution, hlds_goal,
prog_varset, transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
io__state, io__state).
-:- mode transform_goal(in, in, in, out, out, in, out, di, uo) is det.
+:- mode transform_goal(in, in, in, out, out, in, out, in, out, in, di, uo)
+ is det.
transform_goal(Goal0 - Context, VarSet0, Subst, Goal1 - GoalInfo1, VarSet,
- Info0, Info) -->
+ Info0, Info, DotColonSubst0, DotColonSubst, InAtom) -->
transform_goal_2(Goal0, Context, VarSet0, Subst, Goal1 - GoalInfo0,
- VarSet, Info0, Info),
+ VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom),
{ goal_info_set_context(GoalInfo0, Context, GoalInfo1) }.
:- pred transform_goal_2(goal_expr, prog_context, prog_varset,
prog_substitution, hlds_goal, prog_varset,
- transform_info, transform_info, io__state, io__state).
-:- mode transform_goal_2(in, in, in, in, out, out, in, out, di, uo) is det.
+ transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
+ io__state, io__state).
+:- mode transform_goal_2(in, in, in, in, out, out, in, out, in, out, in, di, uo)
+ is det.
-transform_goal_2(fail, _, VarSet, _, disj([]) - GoalInfo, VarSet,
- Info, Info) -->
- { goal_info_init(GoalInfo) }.
+transform_goal_2(fail, Context, VarSet, _, Goal, VarSet,
+ Info, Info, DotColonSubst0, DotColonSubst, InAtom) -->
+ { goal_info_init(GoalInfo) },
+ { insert_svar_tie_up_unifications(Context,
+ DotColonSubst0, DotColonSubst,
+ disj([]) - GoalInfo, Goal, InAtom) }.
-transform_goal_2(true, _, VarSet, _, conj([]) - GoalInfo, VarSet,
- Info, Info) -->
- { goal_info_init(GoalInfo) }.
+transform_goal_2(true, Context, VarSet, _, Goal, VarSet,
+ Info, Info, DotColonSubst0, DotColonSubst, InAtom) -->
+ { goal_info_init(GoalInfo) },
+ { insert_svar_tie_up_unifications(Context,
+ DotColonSubst0, DotColonSubst,
+ conj([]) - GoalInfo, Goal, InAtom) }.
% Convert `all [Vars] Goal' into `not some [Vars] not Goal'.
transform_goal_2(all(Vars0, Goal0), Context, VarSet0, Subst, Goal, VarSet,
- Info0, Info) -->
+ Info0, Info, DotColonSubst0, DotColonSubst, InAtom) -->
{ TransformedGoal = not(some(Vars0, not(Goal0) - Context) - Context) },
transform_goal_2(TransformedGoal, Context, VarSet0, Subst,
- Goal, VarSet, Info0, Info).
+ Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom).
transform_goal_2(some(Vars0, Goal0), _, VarSet0, Subst,
some(Vars, can_remove, Goal) - GoalInfo,
- VarSet, Info0, Info) -->
+ VarSet, Info0, Info, DotColonSubst0, DotColonSubst, InAtom) -->
{ substitute_vars(Vars0, Subst, Vars) },
- transform_goal(Goal0, VarSet0, Subst, Goal, VarSet, Info0, Info),
+ transform_goal(Goal0, VarSet0, Subst, Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom),
{ goal_info_init(GoalInfo) }.
-
-transform_goal_2(if_then_else(Vars0, A0, B0, C0), _, VarSet0, Subst,
- if_then_else(Vars, A, B, C) - GoalInfo, VarSet,
- Info0, Info) -->
+transform_goal_2(if_then_else(Vars0, I0, T0, E0), Context, VarSet0, Subst,
+ if_then_else(Vars, I, T, E) - GoalInfo, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
{ substitute_vars(Vars0, Subst, Vars) },
- transform_goal(A0, VarSet0, Subst, A, VarSet1, Info0, Info1),
- transform_goal(B0, VarSet1, Subst, B, VarSet2, Info1, Info2),
- transform_goal(C0, VarSet2, Subst, C, VarSet, Info2, Info),
+ transform_goal(T0, VarSet0, Subst, T, VarSet1, Info0, Info1,
+ DotColonSubst0, DotColonSubst1, InAtom),
+ { preceding_in_atom(InAtom, IInAtom, DotColonSubst1, DotColonSubst2) },
+ transform_goal(I0, VarSet1, Subst, I1, VarSet2, Info1, Info2,
+ DotColonSubst2, IfThenDotColonSubst, IInAtom),
+ transform_goal(E0, VarSet2, Subst, E1, VarSet3, Info2, Info,
+ DotColonSubst0, ElseDotColonSubst, InAtom),
+ { insert_binary_disj_dot_svar_unifications(Context,
+ IfThenDotColonSubst, ElseDotColonSubst, DotColonSubst,
+ I1, I, E1, E, VarSet3, VarSet) },
{ goal_info_init(GoalInfo) }.
transform_goal_2(if_then(Vars0, A0, B0), Context, Subst, VarSet0,
- Goal, VarSet, Info0, Info) -->
+ Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
transform_goal_2(if_then_else(Vars0, A0, B0, true - Context),
- Context, Subst, VarSet0, Goal, VarSet, Info0, Info).
+ Context, Subst, VarSet0, Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom).
-transform_goal_2(not(A0), _, VarSet0, Subst, Goal, VarSet, Info0, Info) -->
- transform_goal(A0, VarSet0, Subst, A, VarSet, Info0, Info),
- { goal_info_init(GoalInfo) },
- { Goal = not(A) - GoalInfo }.
-
-transform_goal_2((A0,B0), _, VarSet0, Subst, Goal, VarSet, Info0, Info) -->
- get_conj(B0, Subst, [], VarSet0, L0, VarSet1, Info0, Info1),
- get_conj(A0, Subst, L0, VarSet1, L, VarSet, Info1, Info),
+transform_goal_2(not(A0), Context, VarSet0, Subst, Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
+ transform_goal(A0, VarSet0, Subst, A, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst1, InAtom),
+ { goal_info_init(NotAInfo) },
+ { NotA = not(A) - NotAInfo },
+ { insert_dot_svar_unifications(Context,
+ DotColonSubst1, DotColonSubst, InAtom, NotA, Goal) }.
+
+transform_goal_2((A0,B0), _, VarSet0, Subst, Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom0) -->
+ get_conj(B0, Subst, [], VarSet0, L0, VarSet1, Info0, Info1,
+ DotColonSubst0, DotColonSubst1, InAtom0),
+ { preceding_in_atom(InAtom0, InAtom, DotColonSubst1, DotColonSubst2) },
+ get_conj(A0, Subst, L0, VarSet1, L, VarSet, Info1, Info,
+ DotColonSubst2, DotColonSubst, InAtom),
{ goal_info_init(GoalInfo) },
{ conj_list_to_goal(L, GoalInfo, Goal) }.
-transform_goal_2((A0 & B0), _, VarSet0, Subst, Goal, VarSet, Info0, Info) -->
- get_par_conj(B0, Subst, [], VarSet0, L0, VarSet1, Info0, Info1),
- get_par_conj(A0, Subst, L0, VarSet1, L, VarSet, Info1, Info),
+transform_goal_2((A0 & B0), _, VarSet0, Subst, Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom0) -->
+ get_par_conj(B0, Subst, [], VarSet0, L0, VarSet1, Info0, Info1,
+ DotColonSubst0, DotColonSubst1, InAtom0),
+ { preceding_in_atom(InAtom0, InAtom, DotColonSubst1, DotColonSubst2) },
+ get_par_conj(A0, Subst, L0, VarSet1, L, VarSet, Info1, Info,
+ DotColonSubst2, DotColonSubst, InAtom),
{ goal_info_init(GoalInfo) },
{ par_conj_list_to_goal(L, GoalInfo, Goal) }.
-transform_goal_2((A0;B0), _, VarSet0, Subst, Goal, VarSet, Info0, Info) -->
- get_disj(B0, Subst, [], VarSet0, L0, VarSet1, Info0, Info1),
- get_disj(A0, Subst, L0, VarSet1, L, VarSet, Info1, Info),
+transform_goal_2((A0;B0), Context, VarSet0, Subst, Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
+ get_dot_colon_subst_disj(B0, Subst, [], VarSet0, L0, VarSet1,
+ Info0, Info1, DotColonSubst0, _, InAtom),
+ get_dot_colon_subst_disj(A0, Subst, L0, VarSet1, L1, VarSet2,
+ Info1, Info, DotColonSubst0, _, InAtom),
+ { insert_disj_list_dot_svar_unifications(Context, L1, VarSet2,
+ DotColonSubst, L, VarSet) },
{ goal_info_init(GoalInfo) },
{ disj_list_to_goal(L, GoalInfo, Goal) }.
transform_goal_2(implies(P, Q), Context, VarSet0, Subst, Goal, VarSet,
- Info0, Info) -->
+ Info0, Info, DotColonSubst0, DotColonSubst, InAtom) -->
% `P => Q' is defined as `not (P, not Q)'
{ TransformedGoal = not( (P, not(Q) - Context) - Context ) },
transform_goal_2(TransformedGoal, Context, VarSet0, Subst,
- Goal, VarSet, Info0, Info).
+ Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom).
transform_goal_2(equivalent(P0, Q0), _Context, VarSet0, Subst, Goal, VarSet,
- Info0, Info) -->
+ Info0, Info, DotColonSubst0, DotColonSubst, InAtom0) -->
%
% `P <=> Q' is defined as `(P => Q), (Q => P)',
% but that transformation must not be done until
@@ -5722,20 +5785,32 @@
% the goals concerned affect the implicit quantification
% of the variables inside them.
%
+ % Note that since the lexical ordering in an equivalence goes
+ % both ways, it probably does not make sense to use !:X state
+ % variables in the context of an equivalence. However, we
+ % treat such goals as P lexically followed by Q.
+ %
{ goal_info_init(GoalInfo) },
- transform_goal(P0, VarSet0, Subst, P, VarSet1, Info0, Info1),
- transform_goal(Q0, VarSet1, Subst, Q, VarSet, Info1, Info),
+ transform_goal(Q0, VarSet0, Subst, Q, VarSet1, Info0, Info1,
+ DotColonSubst0, DotColonSubst1, InAtom0),
+ { preceding_in_atom(InAtom0, InAtom, DotColonSubst1, DotColonSubst2) },
+ transform_goal(P0, VarSet1, Subst, P, VarSet, Info1, Info,
+ DotColonSubst2, DotColonSubst, InAtom),
{ Goal = shorthand(bi_implication(P, Q)) - GoalInfo }.
transform_goal_2(call(Name, Args0, Purity), Context, VarSet0, Subst, Goal,
- VarSet, Info0, Info) -->
+ VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom0) -->
+ { InAtom = init_atomic_context(InAtom0) },
+ { DotColonSubst1 = DotColonSubst0 },
(
{ Name = unqualified("\\=") },
{ Args0 = [LHS, RHS] }
->
% `LHS \= RHS' is defined as `not (LHS = RHS)'
transform_goal_2(not(unify(LHS, RHS, Purity) - Context),
- Context, VarSet0, Subst, Goal, VarSet, Info0, Info)
+ Context, VarSet0, Subst, EndGoal, VarSet, Info0, Info,
+ DotColonSubst1, EndDotColonSubst, InAtom)
;
% check for a DCG field access goal:
% get: Field =^ field
@@ -5746,8 +5821,9 @@
)
->
{ term__apply_substitution_to_list(Args0, Subst, Args1) },
- transform_dcg_record_syntax(Operator, Args1, Context,
- VarSet0, Goal, VarSet, Info0, Info)
+ transform_dcg_record_syntax(Operator, Args1,
+ Context, VarSet0, EndGoal, VarSet, Info0, Info,
+ DotColonSubst1, EndDotColonSubst, InAtom)
;
% check for an Aditi builtin
{ Purity = pure },
@@ -5765,7 +5841,8 @@
->
{ term__apply_substitution_to_list(Args0, Subst, Args1) },
transform_aditi_builtin(Name1, Args1, Context, VarSet0,
- Goal, VarSet, Info0, Info)
+ EndGoal, VarSet, Info0, Info,
+ DotColonSubst1, EndDotColonSubst, InAtom)
;
{ term__apply_substitution_to_list(Args0, Subst, Args) },
{ make_fresh_arg_vars(Args, VarSet0, HeadVars, VarSet1) },
@@ -5825,27 +5902,37 @@
Info0, Info1) },
insert_arg_unifications(HeadVars, Args,
Context, call(CallId), no,
- Goal0, VarSet1, Goal, VarSet, Info1, Info)
- ).
+ Goal0, VarSet1, EndGoal, VarSet, Info1, Info,
+ DotColonSubst1, EndDotColonSubst, InAtom)
+ ),
+ { insert_svar_tie_up_unifications(Context,
+ EndDotColonSubst, DotColonSubst, EndGoal, Goal, InAtom0) }.
transform_goal_2(unify(A0, B0, Purity), Context, VarSet0, Subst, Goal, VarSet,
- Info0, Info) -->
+ Info0, Info, DotColonSubst0, DotColonSubst, InAtom0) -->
{ term__apply_substitution(A0, Subst, A) },
{ term__apply_substitution(B0, Subst, B) },
+ { InAtom = init_atomic_context(InAtom0) },
+ { DotColonSubst1 = DotColonSubst0 },
unravel_unification(A, B, Context, explicit, [],
- VarSet0, Purity, Goal, VarSet, Info0, Info).
-
+ VarSet0, Purity, EndGoal, VarSet, Info0, Info,
+ DotColonSubst1, EndDotColonSubst, InAtom),
+ { insert_svar_tie_up_unifications(Context,
+ EndDotColonSubst, DotColonSubst, EndGoal, Goal, InAtom0) }.
+
:- inst dcg_record_syntax_op = bound("=^"; ":=").
:- pred transform_dcg_record_syntax(string, list(prog_term), prog_context,
prog_varset, hlds_goal, prog_varset, transform_info,
- transform_info, io__state, io__state).
+ transform_info, dot_colon_subst, dot_colon_subst, in_atom,
+ io__state, io__state).
:- mode transform_dcg_record_syntax(in(dcg_record_syntax_op),
- in, in, in, out, out, in, out, di, uo) is det.
+ in, in, in, out, out, in, out, in, out, in, di, uo) is det.
transform_dcg_record_syntax(Operator, ArgTerms0, Context, VarSet0,
- Goal, VarSet, Info0, Info) -->
+ Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
{ goal_info_init(Context, GoalInfo) },
(
{ ArgTerms0 = [LHSTerm, RHSTerm,
@@ -5872,7 +5959,8 @@
transform_dcg_record_syntax_2(AccessType,
FieldNames, ArgTerms, Context, VarSet0, Goal,
- VarSet, Info0, Info)
+ VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom)
;
{ MaybeFieldNames = error(Msg, ErrorTerm) },
{ invalid_goal("^", ArgTerms0, GoalInfo,
@@ -5896,7 +5984,8 @@
io__write_string(Msg),
io__write_string(" at term `"),
term_io__write_term(VarSet, ErrorTerm),
- io__write_string("'.\n")
+ io__write_string("'.\n"),
+ { DotColonSubst = DotColonSubst0 }
)
;
{ invalid_goal("^", ArgTerms0, GoalInfo,
@@ -5911,18 +6000,22 @@
prog_out__write_context(Context),
io__write_string(" or `^ field1 ^ ... ^ fieldN := Field'.\n"),
prog_out__write_context(Context),
- io__write_string(" in DCG field access goal.\n")
+ io__write_string(" in DCG field access goal.\n"),
+ { DotColonSubst = DotColonSubst0 }
).
:- pred transform_dcg_record_syntax_2(field_access_type,
field_list, list(prog_term), prog_context,
prog_varset, hlds_goal, prog_varset,
- transform_info, transform_info, io__state, io__state).
+ transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
+ io__state, io__state).
:- mode transform_dcg_record_syntax_2(in, in, in, in, in, out, out,
- in, out, di, uo) is det.
+ in, out, in, out, in, di, uo) is det.
transform_dcg_record_syntax_2(AccessType, FieldNames, ArgTerms, Context,
- VarSet0, Goal, VarSet, Info0, Info, IO0, IO) :-
+ VarSet0, Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom, IO0, IO) :-
make_fresh_arg_vars(ArgTerms, VarSet0, ArgVars, VarSet1),
( ArgVars = [FieldValueVar, TermInputVar, TermOutputVar] ->
(
@@ -5931,7 +6024,9 @@
FieldNames, FieldValueVar, TermInputVar,
TermOutputVar, VarSet1, VarSet2, Functor,
InnermostFunctor - InnermostSubContext, Goal0,
- Info0, Info1, IO0, IO1),
+ Info0, Info1,
+ DotColonSubst0, DotColonSubst1, InAtom,
+ IO0, IO1),
FieldArgNumber = 2,
@@ -5958,14 +6053,17 @@
],
insert_arg_unifications_with_supplied_contexts(ArgVars,
ArgTerms, ArgContexts, Context, Goal0, VarSet2,
- Goal, VarSet, Info1, Info, IO1, IO)
+ Goal, VarSet, Info1, Info,
+ DotColonSubst1, DotColonSubst, InAtom, IO1, IO)
;
AccessType = get,
expand_dcg_field_extraction_goal(Context, explicit,
[], FieldNames, FieldValueVar, TermInputVar,
TermOutputVar, VarSet1, VarSet2, Functor,
InnermostFunctor - _InnerSubContext, Goal0,
- Info0, Info1, IO0, IO1),
+ Info0, Info1,
+ DotColonSubst0, DotColonSubst1, InAtom,
+ IO0, IO1),
InputTermArgNumber = 1,
InputTermArgContext = functor(Functor, explicit, []),
@@ -5990,7 +6088,8 @@
],
insert_arg_unifications_with_supplied_contexts(ArgVars,
ArgTerms, ArgContexts, Context, Goal0, VarSet2,
- Goal, VarSet, Info1, Info, IO1, IO)
+ Goal, VarSet, Info1, Info,
+ DotColonSubst1, DotColonSubst, InAtom, IO1, IO)
)
;
error("make_hlds__do_transform_dcg_record_syntax")
@@ -6011,18 +6110,23 @@
field_list, prog_var, prog_var,
prog_var, prog_varset, prog_varset, cons_id,
pair(cons_id, unify_sub_contexts), hlds_goal,
- transform_info, transform_info, io__state, io__state).
+ transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
+ io__state, io__state).
:- mode expand_set_field_function_call(in, in, in, in, in, in,
- in, in, out, out, out, out, in, out, di, uo) is det.
+ in, in, out, out, out, out, in, out, in, out, in,
+ di, uo) is det.
expand_set_field_function_call(Context, MainContext, SubContext0,
FieldNames, FieldValueVar, TermInputVar,
TermOutputVar, VarSet0, VarSet,
- Functor, FieldSubContext, Goal, Info0, Info) -->
+ Functor, FieldSubContext, Goal, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
expand_set_field_function_call_2(Context, MainContext,
SubContext0, FieldNames, FieldValueVar, TermInputVar,
TermOutputVar, VarSet0, VarSet,
- Functor, FieldSubContext, Goals, Info0, Info),
+ Functor, FieldSubContext, Goals, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom),
{ goal_info_init(Context, GoalInfo) },
{ conj_list_to_goal(Goals, GoalInfo, Goal) }.
@@ -6031,17 +6135,22 @@
field_list, prog_var, prog_var,
prog_var, prog_varset, prog_varset, cons_id,
pair(cons_id, unify_sub_contexts), list(hlds_goal),
- transform_info, transform_info, io__state, io__state).
+ transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
+ io__state, io__state).
:- mode expand_set_field_function_call_2(in, in, in, in, in, in,
- in, in, out, out, out, out, in, out, di, uo) is det.
+ in, in, out, out, out, out, in, out, in, out, in,
+ di, uo) is det.
-expand_set_field_function_call_2(_, _, _, [], _, _, _, _, _, _, _, _, _, _) -->
+expand_set_field_function_call_2(_, _, _, [], _, _, _, _, _, _, _, _, _, _,
+ _, _, _) -->
{ error(
"expand_set_field_function_call_2: empty list of field names") }.
expand_set_field_function_call_2(Context, MainContext, SubContext0,
[FieldName - FieldArgs | FieldNames], FieldValueVar,
TermInputVar, TermOutputVar, VarSet0, VarSet, Functor,
- FieldSubContext, Goals, Info0, Info) -->
+ FieldSubContext, Goals, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
{ make_fresh_arg_vars(FieldArgs, VarSet0, FieldArgVars, VarSet1) },
( { FieldNames = [_|_] } ->
{ varset__new_var(VarSet1, SubTermInputVar, VarSet2) },
@@ -6066,7 +6175,8 @@
expand_set_field_function_call_2(Context, MainContext,
SubContext, FieldNames, FieldValueVar, SubTermInputVar,
SubTermOutputVar, VarSet3, VarSet4, _,
- FieldSubContext, Goals0, Info2, Info3),
+ FieldSubContext, Goals0, Info2, Info3,
+ DotColonSubst0, DotColonSubst1, InAtom),
{ list__append([GetSubFieldGoal | Goals0],
[UpdateGoal], Goals1) }
@@ -6078,14 +6188,16 @@
MainContext, SubContext0, FieldName, TermOutputVar,
SetArgs, Functor, Goal, Info0, Info3) },
{ FieldSubContext = Functor - SubContext0 },
- { Goals1 = [Goal] }
+ { Goals1 = [Goal] },
+ { DotColonSubst1 = DotColonSubst0 }
),
{ ArgContext = functor(Functor, MainContext, SubContext0) },
{ goal_info_init(Context, GoalInfo) },
{ conj_list_to_goal(Goals1, GoalInfo, Conj0) },
append_arg_unifications(FieldArgVars, FieldArgs, Context, ArgContext,
- Conj0, VarSet4, Conj, VarSet, Info3, Info),
+ Conj0, VarSet4, Conj, VarSet, Info3, Info,
+ DotColonSubst1, DotColonSubst, InAtom),
{ goal_to_conj_list(Conj, Goals) }.
% Expand a field extraction goal into a list of goals which
@@ -6104,14 +6216,17 @@
unify_sub_contexts, field_list, prog_var, prog_var,
prog_var, prog_varset, prog_varset, cons_id,
pair(cons_id, unify_sub_contexts), hlds_goal,
- transform_info, transform_info, io__state, io__state).
+ transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
+ io__state, io__state).
:- mode expand_dcg_field_extraction_goal(in, in, in, in, in,
- in, in, in, out, out, out, out, in, out, di, uo) is det.
+ in, in, in, out, out, out, out, in, out, in, out, in,
+ di, uo) is det.
expand_dcg_field_extraction_goal(Context, MainContext, SubContext,
FieldNames, FieldValueVar, TermInputVar, TermOutputVar,
VarSet0, VarSet, Functor, FieldSubContext,
- Goal, Info0, Info) -->
+ Goal, Info0, Info, DotColonSubst0, DotColonSubst, InAtom) -->
% unify the DCG input and output variables
{ make_atomic_unification(TermOutputVar, var(TermInputVar),
Context, MainContext, SubContext, UnifyDCG,
@@ -6121,7 +6236,8 @@
% the output DCG variable
expand_get_field_function_call_2(Context, MainContext, SubContext,
FieldNames, FieldValueVar, TermOutputVar, VarSet0, VarSet,
- Functor, FieldSubContext, Goals1, Info1, Info),
+ Functor, FieldSubContext, Goals1, Info1, Info,
+ DotColonSubst0, DotColonSubst, InAtom),
{ Goals = [UnifyDCG | Goals1] },
{ goal_info_init(Context, GoalInfo) },
{ conj_list_to_goal(Goals, GoalInfo, Goal) }.
@@ -6140,16 +6256,21 @@
unify_sub_contexts, field_list, prog_var,
prog_var, prog_varset, prog_varset, cons_id,
pair(cons_id, unify_sub_contexts), hlds_goal,
- transform_info, transform_info, io__state, io__state).
+ transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
+ io__state, io__state).
:- mode expand_get_field_function_call(in, in, in, in, in,
- in, in, out, out, out, out, in, out, di, uo) is det.
+ in, in, out, out, out, out, in, out, in, out, in,
+ di, uo) is det.
expand_get_field_function_call(Context, MainContext, SubContext0,
FieldNames, FieldValueVar, TermInputVar, VarSet0, VarSet,
- Functor, FieldSubContext, Goal, Info0, Info) -->
+ Functor, FieldSubContext, Goal, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
expand_get_field_function_call_2(Context, MainContext, SubContext0,
FieldNames, FieldValueVar, TermInputVar,
- VarSet0, VarSet, Functor, FieldSubContext, Goals, Info0, Info),
+ VarSet0, VarSet, Functor, FieldSubContext, Goals, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom),
{ goal_info_init(Context, GoalInfo) },
{ conj_list_to_goal(Goals, GoalInfo, Goal) }.
@@ -6157,17 +6278,22 @@
unify_sub_contexts, field_list, prog_var,
prog_var, prog_varset, prog_varset, cons_id,
pair(cons_id, unify_sub_contexts), list(hlds_goal),
- transform_info, transform_info, io__state, io__state).
+ transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
+ io__state, io__state).
:- mode expand_get_field_function_call_2(in, in, in, in, in,
- in, in, out, out, out, out, in, out, di, uo) is det.
+ in, in, out, out, out, out, in, out, in, out, in,
+ di, uo) is det.
-expand_get_field_function_call_2(_, _, _, [], _, _, _, _, _, _, _, _, _) -->
+expand_get_field_function_call_2(_, _, _, [], _, _, _, _, _, _, _, _, _,
+ _, _, _) -->
{ error(
"expand_get_field_function_call_2: empty list of field names") }.
expand_get_field_function_call_2(Context, MainContext, SubContext0,
[FieldName - FieldArgs | FieldNames], FieldValueVar,
TermInputVar, VarSet0, VarSet, Functor,
- FieldSubContext, Goals, Info0, Info) -->
+ FieldSubContext, Goals, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
{ make_fresh_arg_vars(FieldArgs, VarSet0, FieldArgVars, VarSet1) },
{ GetArgVars = list__append(FieldArgVars, [TermInputVar]) },
( { FieldNames = [_|_] } ->
@@ -6183,7 +6309,8 @@
expand_get_field_function_call_2(Context, MainContext,
SubContext, FieldNames, FieldValueVar, SubTermInputVar,
VarSet2, VarSet3, _, FieldSubContext,
- Goals1, Info1, Info2),
+ Goals1, Info1, Info2,
+ DotColonSubst0, DotColonSubst1, InAtom),
{ Goals2 = [Goal | Goals1] }
;
{ VarSet3 = VarSet1 },
@@ -6191,13 +6318,15 @@
{ construct_field_access_function_call(get, Context,
MainContext, SubContext0, FieldName, FieldValueVar,
GetArgVars, Functor, Goal, Info0, Info2) },
- { Goals2 = [Goal] }
+ { Goals2 = [Goal] },
+ { DotColonSubst1 = DotColonSubst0 }
),
{ ArgContext = functor(Functor, MainContext, SubContext0) },
{ goal_info_init(Context, GoalInfo) },
{ conj_list_to_goal(Goals2, GoalInfo, Conj0) },
append_arg_unifications(FieldArgVars, FieldArgs, Context, ArgContext,
- Conj0, VarSet3, Conj, VarSet, Info2, Info),
+ Conj0, VarSet3, Conj, VarSet, Info2, Info,
+ DotColonSubst1, DotColonSubst, InAtom),
{ goal_to_conj_list(Conj, Goals) }.
:- pred construct_field_access_function_call(field_access_type, prog_context,
@@ -6274,12 +6403,15 @@
% Mercury Language Reference Manual.
:- pred transform_aditi_builtin(string, list(prog_term), prog_context,
prog_varset, hlds_goal, prog_varset,
- transform_info, transform_info, io__state, io__state).
+ transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
+ io__state, io__state).
:- mode transform_aditi_builtin(in(aditi_update_str), in,
- in, in, out, out, in, out, di, uo) is det.
+ in, in, out, out, in, out, in, out, in, di, uo) is det.
transform_aditi_builtin(UpdateStr, Args0, Context, VarSet0,
- Goal, VarSet, Info0, Info) -->
+ Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
(
{ UpdateStr = "aditi_insert", InsertDelete = insert
; UpdateStr = "aditi_delete", InsertDelete = delete
@@ -6287,7 +6419,8 @@
->
transform_aditi_tuple_insert_delete(UpdateStr, InsertDelete,
Args0, Context, VarSet0, Goal,
- VarSet, Info0, Info)
+ VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom)
;
{
UpdateStr = "aditi_insert",
@@ -6317,19 +6450,23 @@
},
transform_aditi_insert_delete_modify(UpdateStr,
Update, Args0, Context, VarSet0, Goal,
- VarSet, Info0, Info)
+ VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom)
).
:- pred transform_aditi_tuple_insert_delete(string, aditi_insert_delete,
list(prog_term), prog_context,
prog_varset, hlds_goal, prog_varset,
- transform_info, transform_info, io__state, io__state).
+ transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
+ io__state, io__state).
:- mode transform_aditi_tuple_insert_delete(in, in, in, in,
- in, out, out, in, out, di, uo) is det.
+ in, out, out, in, out, in, out, in, di, uo) is det.
transform_aditi_tuple_insert_delete(UpdateStr, InsertDelete, Args0, Context,
- VarSet0, Goal, VarSet, Info0, Info) -->
+ VarSet0, Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
% Build an empty goal_info.
{ goal_info_init(Context, GoalInfo) },
@@ -6381,7 +6518,8 @@
InsertArity, Info0, Info1) },
insert_arg_unifications(AllArgs, AllArgTerms,
Context, call(CallId), no,
- Goal0, VarSet3, Goal, VarSet, Info1, Info)
+ Goal0, VarSet3, Goal, VarSet, Info1, Info,
+ DotColonSubst0, DotColonSubst, InAtom)
;
{ invalid_goal(UpdateStr, Args0, GoalInfo,
Goal, VarSet0, VarSet) },
@@ -6394,7 +6532,8 @@
io__write(InsertDelete),
io__write_string(" in `"),
io__write_string(UpdateStr),
- io__write_string("'.\n")
+ io__write_string("'.\n"),
+ { DotColonSubst = DotColonSubst0 }
)
;
{ invalid_goal(UpdateStr, Args0, GoalInfo,
@@ -6403,19 +6542,23 @@
QualInfo) },
{ Info = Info0 ^ qual_info := QualInfo },
{ list__length(Args0, Arity) },
- aditi_update_arity_error(Context, UpdateStr, Arity, [3])
+ aditi_update_arity_error(Context, UpdateStr, Arity, [3]),
+ { DotColonSubst = DotColonSubst0 }
).
% Parse an `aditi_delete' or `aditi_modify' goal.
:- pred transform_aditi_insert_delete_modify(string,
aditi_insert_delete_modify, list(prog_term), prog_context,
prog_varset, hlds_goal, prog_varset, transform_info,
- transform_info, io__state, io__state).
+ transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
+ io__state, io__state).
:- mode transform_aditi_insert_delete_modify(in, in, in, in, in, out, out,
- in, out, di, uo) is det.
+ in, out, in, out, in, di, uo) is det.
transform_aditi_insert_delete_modify(Descr, InsertDelMod, Args0, Context,
- VarSet0, UpdateGoal, VarSet, Info0, Info) -->
+ VarSet0, UpdateGoal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
{ goal_info_init(Context, GoalInfo) },
(
{ list__length(Args0, Arity) },
@@ -6427,7 +6570,8 @@
{ qual_info_set_found_syntax_error(yes, Info0 ^ qual_info,
QualInfo) },
{ Info = Info0 ^ qual_info := QualInfo },
- aditi_update_arity_error(Context, Descr, Arity, [3, 4])
+ aditi_update_arity_error(Context, Descr, Arity, [3, 4]),
+ { DotColonSubst = DotColonSubst0 }
;
%
% First syntax -
@@ -6480,11 +6624,12 @@
{ parse_goal(GoalTerm, VarSet1, ParsedGoal, VarSet2) },
{ map__init(Substitution) },
transform_goal(ParsedGoal, VarSet2, Substitution,
- PredGoal0, VarSet3, Info0, Info1),
+ PredGoal0, VarSet3, Info0, Info1,
+ DotColonSubst0, DotColonSubst1, InAtom),
{ ArgContext = head(PredOrFunc, PredArity) },
insert_arg_unifications(HeadArgs, HeadArgs1, Context,
ArgContext, no, PredGoal0, VarSet3, PredGoal1, VarSet4,
- Info1, Info2),
+ Info1, Info2, DotColonSubst1, DotColonSubst2, InAtom),
% Quantification will reduce this down to
% the proper set of nonlocal arguments.
@@ -6556,7 +6701,8 @@
[term__variable(LambdaVar), AditiState0Term,
AditiStateTerm],
Context, CallId, no, UpdateConj, VarSet7, UpdateGoal,
- VarSet, Info4, Info)
+ VarSet, Info4, Info,
+ DotColonSubst2, DotColonSubst, InAtom)
;
%
% Second syntax -
@@ -6596,7 +6742,8 @@
{ record_called_pred_or_func(PredOrFunc, SymName, Arity,
Info0, Info1) },
insert_arg_unifications(OtherArgs, OtherArgs0, Context, CallId,
- no, Call, VarSet1, UpdateGoal, VarSet, Info1, Info)
+ no, Call, VarSet1, UpdateGoal, VarSet, Info1, Info,
+ DotColonSubst0, DotColonSubst, InAtom)
;
{ invalid_goal(Descr, Args0, GoalInfo,
UpdateGoal, VarSet0, VarSet) },
@@ -6604,7 +6751,8 @@
QualInfo) },
{ Info = Info0 ^ qual_info := QualInfo },
io__set_exit_status(1),
- output_expected_aditi_update_syntax(Context, InsertDelMod)
+ output_expected_aditi_update_syntax(Context, InsertDelMod),
+ { DotColonSubst = DotColonSubst0 }
).
:- pred aditi_delete_insert_delete_modify_goal_info(aditi_insert_delete_modify,
@@ -6816,6 +6964,37 @@
% treatment, the body goal will be a conjunction, which would
% complicate the handling of code generation for nondet pragma C codes.
+ % STATE VARIABLES
+ % ---------------
+ % State variables are identified as unifications with terms !.X or !:X
+ % where X is the name of a state variable. The translation of state
+ % variable syntax is described in the reference manual.
+ %
+ % State variables in head arguments dictate the initial and final
+ % bindings for the body.
+ %
+ % Each atomic goal A (including the subgoals for any expression
+ % arguments) is expanded as follows, constructing the dot_colon_subst
+ % S for the goal:
+ % 1. if !.X appears in A then substitute with some fresh variable D
+ % and S(!.X) = D;
+ % 2. if !:X appears in A then substitute with some fresh variable C
+ % and S(!:X) = C;
+ % 3. unifiers are added to the transformed A so that for each
+ % state variable X in A that also has a mapping in Post
+ % (where Post is the mapping from "live" state variables
+ % after A to logical variables),
+ % (i) if S(!:X) is defined we add the unifier S(!:X) = Post(X)
+ % (iii) otherwise if S(!.X) is defined then we add the unifier
+ % S(!.X) = Post(X).
+ %
+ % Pre is the mapping from "live" state variables before A to logical
+ % variables and is derived as follows:
+ % - if S(!.X) is defined
+ % then Pre(X) = S(!.X);
+ % - else if Post(X) is defined, but S(!:X) is not,
+ % then Pre(X) = Post(X).
+
:- type arg_context
--->
% the arguments in the head of the clause
@@ -6834,78 +7013,91 @@
:- pred insert_arg_unifications(list(prog_var), list(prog_term),
prog_context, arg_context, bool, hlds_goal, prog_varset,
hlds_goal, prog_varset, transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
io__state, io__state).
:- mode insert_arg_unifications(in, in, in, in, in, in, in, out,
- out, in, out, di, uo) is det.
+ out, in, out, in, out, in, di, uo) is det.
insert_arg_unifications(HeadVars, Args, Context, ArgContext, ForPragmaC,
- Goal0, VarSet0, Goal, VarSet, Info0, Info) -->
+ Goal0, VarSet0, Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
( { HeadVars = [] } ->
{ Goal = Goal0 },
{ VarSet = VarSet0 },
- { Info = Info0 }
+ { Info = Info0 },
+ { DotColonSubst = DotColonSubst0 }
;
{ Goal0 = _ - GoalInfo0 },
{ goal_to_conj_list(Goal0, List0) },
insert_arg_unifications_2(HeadVars, Args, Context, ArgContext,
- ForPragmaC, 0, List0, VarSet0, List, VarSet,
- Info0, Info),
- { goal_info_set_context(GoalInfo0, Context, GoalInfo) },
- { conj_list_to_goal(List, GoalInfo, Goal) }
+ ForPragmaC, 0, List0, VarSet0, List1, VarSet,
+ Info0, Info, DotColonSubst0, DotColonSubst1, InAtom),
+ { conj_list_to_goal(List1, GoalInfo, Goal1) },
+ { insert_svar_tie_up_unifications(Context,
+ DotColonSubst1, DotColonSubst, Goal1, Goal, InAtom) },
+ { goal_info_set_context(GoalInfo0, Context, GoalInfo) }
).
:- pred insert_arg_unifications_2(list(prog_var), list(prog_term),
prog_context, arg_context, bool, int, list(hlds_goal),
prog_varset, list(hlds_goal), prog_varset,
- transform_info, transform_info, io__state, io__state).
+ transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
+ io__state, io__state).
:- mode insert_arg_unifications_2(in, in, in, in, in, in, in, in,
- out, out, in, out, di, uo) is det.
+ out, out, in, out, in, out, in, di, uo) is det.
-insert_arg_unifications_2([], [_|_], _, _, _, _, _, _, _, _, _, _) -->
+insert_arg_unifications_2([], [_|_], _, _, _, _, _, _, _, _, _, _, _, _, _) -->
{ error("insert_arg_unifications_2: length mismatch") }.
-insert_arg_unifications_2([_|_], [], _, _, _, _, _, _, _, _, _, _) -->
+insert_arg_unifications_2([_|_], [], _, _, _, _, _, _, _, _, _, _, _, _, _) -->
{ error("insert_arg_unifications_2: length mismatch") }.
insert_arg_unifications_2([], [], _, _, _, _, List, VarSet, List, VarSet,
- Info, Info) --> [].
+ Info, Info, DotColonSubst, DotColonSubst, _) --> [].
insert_arg_unifications_2([Var|Vars], [Arg|Args], Context, ArgContext,
- ForPragmaC, N0, List0, VarSet0, List, VarSet, Info0, Info) -->
+ ForPragmaC, N0, List0, VarSet0, List, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
{ N1 is N0 + 1 },
insert_arg_unification(Var, Arg, Context, ArgContext,
ForPragmaC, N1, List0, VarSet0, List1, VarSet1, ArgUnifyConj,
- Info0, Info1),
+ Info0, Info1, DotColonSubst0, DotColonSubst1, InAtom),
(
{ ArgUnifyConj = [] }
->
insert_arg_unifications_2(Vars, Args, Context, ArgContext,
ForPragmaC, N1, List1, VarSet1, List, VarSet,
- Info1, Info)
+ Info1, Info, DotColonSubst1, DotColonSubst, InAtom)
;
insert_arg_unifications_2(Vars, Args, Context, ArgContext,
ForPragmaC, N1, List1, VarSet1, List2, VarSet,
- Info1, Info),
+ Info1, Info, DotColonSubst1, DotColonSubst, InAtom),
{ list__append(ArgUnifyConj, List2, List) }
).
:- pred insert_arg_unifications_with_supplied_contexts(list(prog_var),
list(prog_term), assoc_list(int, arg_context), prog_context,
hlds_goal, prog_varset, hlds_goal, prog_varset,
- transform_info, transform_info, io__state, io__state).
+ transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
+ io__state, io__state).
:- mode insert_arg_unifications_with_supplied_contexts(in, in, in, in, in, in,
- out, out, in, out, di, uo) is det.
+ out, out, in, out, in, out, in, di, uo) is det.
insert_arg_unifications_with_supplied_contexts(ArgVars,
ArgTerms, ArgContexts, Context, Goal0, VarSet0,
- Goal, VarSet, Info0, Info) -->
+ Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
( { ArgVars = [] } ->
{ Goal = Goal0 },
{ VarSet = VarSet0 },
- { Info = Info0 }
+ { Info = Info0 },
+ { DotColonSubst = DotColonSubst0 }
;
{ Goal0 = _ - GoalInfo0 },
{ goal_to_conj_list(Goal0, GoalList0) },
insert_arg_unifications_with_supplied_contexts_2(ArgVars,
ArgTerms, ArgContexts, Context, GoalList0,
- VarSet0, GoalList, VarSet, Info0, Info),
+ VarSet0, GoalList, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom),
{ goal_info_set_context(GoalInfo0, Context, GoalInfo) },
{ conj_list_to_goal(GoalList, GoalInfo, Goal) }
).
@@ -6913,18 +7105,22 @@
:- pred insert_arg_unifications_with_supplied_contexts_2(list(prog_var),
list(prog_term), assoc_list(int, arg_context), prog_context,
list(hlds_goal), prog_varset, list(hlds_goal), prog_varset,
- transform_info, transform_info, io__state, io__state).
+ transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
+ io__state, io__state).
:- mode insert_arg_unifications_with_supplied_contexts_2(in, in, in, in, in,
- in, out, out, in, out, di, uo) is det.
+ in, out, out, in, out, in, out, in, di, uo) is det.
insert_arg_unifications_with_supplied_contexts_2(Vars, Terms, ArgContexts,
- Context, List0, VarSet0, List, VarSet, Info0, Info) -->
+ Context, List0, VarSet0, List, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
(
{ Vars = [], Terms = [], ArgContexts = [] }
->
{ List = List0 },
{ VarSet = VarSet0 },
- { Info = Info0 }
+ { Info = Info0 },
+ { DotColonSubst = DotColonSubst0 }
;
{ Vars = [Var | Vars1] },
{ Terms = [Term | Terms1] },
@@ -6932,10 +7128,12 @@
->
insert_arg_unification(Var, Term, Context, ArgContext, no,
ArgNumber, List0, VarSet0, List1, VarSet1,
- UnifyConj, Info0, Info1),
+ UnifyConj, Info0, Info1,
+ DotColonSubst0, DotColonSubst1, InAtom),
insert_arg_unifications_with_supplied_contexts_2(Vars1, Terms1,
ArgContexts1, Context, List1, VarSet1, List2, VarSet,
- Info1, Info),
+ Info1, Info,
+ DotColonSubst1, DotColonSubst, InAtom),
{ list__append(UnifyConj, List2, List) }
;
{ error("insert_arg_unifications_with_supplied_contexts") }
@@ -6945,23 +7143,28 @@
prog_context, arg_context, bool, int,
list(hlds_goal), prog_varset, list(hlds_goal), prog_varset,
list(hlds_goal), transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
io__state, io__state).
:- mode insert_arg_unification(in, in, in, in, in, in,
- in, in, out, out, out, in, out, di, uo) is det.
+ in, in, out, out, out, in, out, in, out, in, di, uo) is det.
insert_arg_unification(Var, Arg, Context, ArgContext, ForPragmaC, N1,
- List0, VarSet0, List1, VarSet1, ArgUnifyConj, Info0, Info) -->
+ List0, VarSet0, List1, VarSet, ArgUnifyConj, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
(
{ Arg = term__variable(Var) }
->
% Skip unifications of the form `X = X'
- { VarSet1 = VarSet0 },
+ { VarSet = VarSet0 },
{ Info = Info0 },
{ ArgUnifyConj = [] },
- { List1 = List0 }
+ { List1 = List0 },
+ { DotColonSubst = DotColonSubst0 }
;
{ Arg = term__variable(ArgVar) },
- { ForPragmaC = yes }
+ { ForPragmaC = yes },
+ { VarSet1 = VarSet0 },
+ { DotColonSubst1 = DotColonSubst0 }
->
% Handle unifications of the form `X = Y' by substitution
% if this is safe.
@@ -6969,19 +7172,43 @@
{ ArgUnifyConj = [] },
{ map__init(Subst0) },
{ map__det_insert(Subst0, ArgVar, Var, Subst) },
- { goal_util__rename_vars_in_goals(List0, no, Subst,
- List1) },
- { varset__search_name(VarSet0, ArgVar, ArgVarName) ->
- varset__name_var(VarSet0, Var, ArgVarName, VarSet1)
+ { goal_util__rename_vars_in_goals(List0, no, Subst, List1) },
+ { varset__search_name(VarSet1, ArgVar, ArgVarName) ->
+ varset__name_var(VarSet1, Var, ArgVarName, VarSet)
;
- VarSet1 = VarSet0
- }
+ VarSet = VarSet1
+ },
+ { DotColonSubst = DotColonSubst1 }
+ ;
+ % If this is a state variable we should apply the appropriate
+ % substitution here.
+ (
+ { Arg = term__functor(term__atom("!."),
+ [term__variable(SVar)], Context) },
+ { svar_dot(SVar, ArgVar, VarSet0, VarSet1,
+ DotColonSubst0, DotColonSubst1, InAtom) }
+ ;
+ { Arg = term__functor(term__atom("!:"),
+ [term__variable(SVar)], Context) },
+ { svar_colon(SVar, ArgVar, VarSet0, VarSet1,
+ DotColonSubst0, DotColonSubst1, InAtom) }
+ )
+ ->
+ { arg_context_to_unify_context(ArgContext, N1,
+ UnifyMainContext, UnifySubContext) },
+ unravel_unification(term__variable(Var), term__variable(ArgVar),
+ Context, UnifyMainContext, UnifySubContext,
+ VarSet1, pure, Goal, VarSet, Info0, Info,
+ DotColonSubst1, DotColonSubst, InAtom),
+ { goal_to_conj_list(Goal, ArgUnifyConj) },
+ { List1 = List0 }
;
{ arg_context_to_unify_context(ArgContext, N1,
UnifyMainContext, UnifySubContext) },
unravel_unification(term__variable(Var), Arg,
Context, UnifyMainContext, UnifySubContext,
- VarSet0, pure, Goal, VarSet1, Info0, Info),
+ VarSet0, pure, Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom),
{ goal_to_conj_list(Goal, ArgUnifyConj) },
{ List1 = List0 }
).
@@ -6993,65 +7220,78 @@
:- pred append_arg_unifications(list(prog_var), list(prog_term),
prog_context, arg_context, hlds_goal, prog_varset, hlds_goal,
prog_varset, transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
io__state, io__state).
:- mode append_arg_unifications(in, in, in, in, in, in,
- out, out, in, out, di, uo) is det.
+ out, out, in, out, in, out, in, di, uo) is det.
append_arg_unifications(HeadVars, Args, Context, ArgContext, Goal0, VarSet0,
- Goal, VarSet, Info0, Info) -->
+ Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
( { HeadVars = [] } ->
{ Goal = Goal0 },
{ VarSet = VarSet0 },
- { Info = Info0 }
+ { Info = Info0 },
+ { DotColonSubst = DotColonSubst0 }
;
{ Goal0 = _ - GoalInfo },
{ goal_to_conj_list(Goal0, List0) },
append_arg_unifications_2(HeadVars, Args, Context, ArgContext,
- 0, List0, VarSet0, List, VarSet, Info0, Info),
+ 0, List0, VarSet0, List, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom),
{ conj_list_to_goal(List, GoalInfo, Goal) }
).
:- pred append_arg_unifications_2(list(prog_var), list(prog_term),
prog_context, arg_context, int, list(hlds_goal), prog_varset,
list(hlds_goal), prog_varset, transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
io__state, io__state).
:- mode append_arg_unifications_2(in, in, in, in, in, in, in,
- out, out, in, out, di, uo) is det.
+ out, out, in, out, in, out, in, di, uo) is det.
-append_arg_unifications_2([], [_|_], _, _, _, _, _, _, _, _, _) -->
+append_arg_unifications_2([], [_|_], _, _, _, _, _, _, _, _, _, _, _, _) -->
{ error("append_arg_unifications_2: length mismatch") }.
-append_arg_unifications_2([_|_], [], _, _, _, _, _, _, _, _, _) -->
+append_arg_unifications_2([_|_], [], _, _, _, _, _, _, _, _, _, _, _, _) -->
{ error("append_arg_unifications_2: length mismatch") }.
append_arg_unifications_2([], [], _, _, _, List, VarSet, List, VarSet,
- Info, Info) --> [].
+ Info, Info, DotColonSubst, DotColonSubst, _) --> [].
append_arg_unifications_2([Var|Vars], [Arg|Args], Context, ArgContext, N0,
- List0, VarSet0, List, VarSet, Info0, Info) -->
+ List0, VarSet0, List, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
{ N1 is N0 + 1 },
append_arg_unification(Var, Arg, Context, ArgContext,
- N1, ConjList, VarSet0, VarSet1, Info0, Info1),
+ N1, ConjList, VarSet0, VarSet1, Info0, Info1,
+ DotColonSubst0, DotColonSubst1, InAtom),
{ list__append(List0, ConjList, List1) },
append_arg_unifications_2(Vars, Args, Context, ArgContext, N1,
- List1, VarSet1, List, VarSet, Info1, Info).
+ List1, VarSet1, List, VarSet, Info1, Info,
+ DotColonSubst1, DotColonSubst, InAtom).
:- pred append_arg_unification(prog_var, prog_term, prog_context, arg_context,
int, list(hlds_goal), prog_varset, prog_varset,
- transform_info, transform_info, io__state, io__state).
+ transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
+ io__state, io__state).
:- mode append_arg_unification(in, in, in, in, in, out, in,
- out, in, out, di, uo) is det.
+ out, in, out, in, out, in, di, uo) is det.
append_arg_unification(Var, Arg, Context, ArgContext,
- N1, ConjList, VarSet0, VarSet, Info0, Info) -->
+ N1, ConjList, VarSet0, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
( { Arg = term__variable(Var) } ->
% skip unifications of the form `X = X'
{ Info = Info0 },
{ VarSet = VarSet0 },
- { ConjList = [] }
+ { ConjList = [] },
+ { DotColonSubst = DotColonSubst0 }
;
{ arg_context_to_unify_context(ArgContext, N1,
UnifyMainContext, UnifySubContext) },
unravel_unification(term__variable(Var), Arg,
Context, UnifyMainContext, UnifySubContext,
- VarSet0, pure, Goal, VarSet, Info0, Info),
+ VarSet0, pure, Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom),
{ goal_to_conj_list(Goal, ConjList) }
).
@@ -7124,15 +7364,16 @@
:- pred unravel_unification(prog_term, prog_term, prog_context,
unify_main_context, unify_sub_contexts, prog_varset,
purity, hlds_goal, prog_varset, transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
io__state, io__state).
:- mode unravel_unification(in, in, in, in, in, in, in, out, out,
- in, out, di, uo) is det.
+ in, out, in, out, in, di, uo) is det.
% `X = Y' needs no unravelling.
unravel_unification(term__variable(X), term__variable(Y), Context,
- MainContext, SubContext, VarSet0, Purity, Goal, VarSet, Info0, Info)
- -->
+ MainContext, SubContext, VarSet0, Purity, Goal, VarSet,
+ Info0, Info, DotColonSubst, DotColonSubst, _InAtom) -->
{ make_atomic_unification(X, var(Y), Context, MainContext,
SubContext, Goal, Info0, Info1) },
check_expr_purity(Purity, Context, Info1, Info),
@@ -7147,9 +7388,9 @@
% NewVar3 = A3.
% In the trivial case `X = c', no unravelling occurs.
-unravel_unification(term__variable(X), RHS,
- Context, MainContext, SubContext, VarSet0, Purity,
- Goal, VarSet, Info0, Info) -->
+unravel_unification(term__variable(X), RHS, Context,
+ MainContext, SubContext, VarSet0, Purity, Goal, VarSet,
+ Info0, Info, DotColonSubst0, DotColonSubst, InAtom) -->
{ RHS = term__functor(F, Args, FunctorContext) },
(
% Handle explicit type qualification.
@@ -7162,7 +7403,8 @@
Context, Info0, Info1),
unravel_unification(term__variable(X), RVal,
Context, MainContext, SubContext, VarSet0,
- Purity, Goal, VarSet, Info1, Info)
+ Purity, Goal, VarSet, Info1, Info,
+ DotColonSubst0, DotColonSubst, InAtom)
;
% Handle unification expressions.
{ F = term__atom("@") },
@@ -7170,10 +7412,12 @@
->
unravel_unification(term__variable(X), LVal,
Context, MainContext, SubContext,
- VarSet0, Purity, Goal1, VarSet1, Info0, Info1),
+ VarSet0, Purity, Goal1, VarSet1, Info0, Info1,
+ DotColonSubst0, DotColonSubst1, InAtom),
unravel_unification(term__variable(X), RVal,
Context, MainContext, SubContext,
- VarSet1, Purity, Goal2, VarSet, Info1, Info),
+ VarSet1, Purity, Goal2, VarSet, Info1, Info,
+ DotColonSubst1, DotColonSubst, InAtom),
{ goal_info_init(GoalInfo) },
{ goal_to_conj_list(Goal1, ConjList1) },
{ goal_to_conj_list(Goal2, ConjList2) },
@@ -7218,10 +7462,14 @@
{ Det = Det1 },
{ term__coerce(GoalTerm1, GoalTerm) },
{ parse_goal(GoalTerm, VarSet0, ParsedGoal, VarSet1) },
+ % Note that all state variables appearing in a lambda
+ % are considered local to the lambda - this is a stricter
+ % rule than that applied to ordinary logical variables.
build_lambda_expression(X, PredOrFunc, EvalMethod, Vars1,
Modes, Det, ParsedGoal, VarSet1,
Context, MainContext, SubContext, Goal, VarSet,
- Info2, Info)
+ Info2, Info),
+ { DotColonSubst = DotColonSubst0 }
;
{
% handle higher-order dcg pred expressions -
@@ -7246,6 +7494,7 @@
Modes, Det, ParsedGoal, VarSet1,
Context, MainContext, SubContext, Goal0, VarSet,
Info1, Info),
+ { DotColonSubst = DotColonSubst0 },
{ Goal0 = GoalExpr - GoalInfo0 },
{ add_goal_info_purity_feature(GoalInfo0, Purity, GoalInfo) },
{ Goal = GoalExpr - GoalInfo }
@@ -7268,16 +7517,26 @@
->
check_expr_purity(Purity, Context, Info0, Info1),
{ map__init(Subst) },
- transform_goal(IfParseTree, VarSet11, Subst, IfGoal, VarSet22,
- Info1, Info2),
+
+ % Since if-then-else expressions can only appear in
+ % unification goals or as (expressions in) arguments
+ % to calls, they therefore can only appear in the
+ % context of an atomic formula.
+
unravel_unification(term__variable(X), ThenTerm,
- Context, MainContext, SubContext, VarSet22,
- pure, ThenGoal, VarSet33, Info2, Info3),
+ Context, MainContext, SubContext, VarSet11,
+ pure, ThenGoal, VarSet22, Info1, Info2,
+ DotColonSubst0, DotColonSubst1, InAtom),
+
+ transform_goal(IfParseTree, VarSet22, Subst, IfGoal, VarSet33,
+ Info2, Info3, DotColonSubst1, DotColonSubst2, InAtom),
+
unravel_unification(term__variable(X), ElseTerm,
Context, MainContext, SubContext, VarSet33, pure,
- ElseGoal, VarSet, Info3, Info),
- { IfThenElse = if_then_else(Vars, IfGoal,
- ThenGoal, ElseGoal) },
+ ElseGoal, VarSet, Info3, Info,
+ DotColonSubst2, DotColonSubst, InAtom),
+
+ { IfThenElse = if_then_else(Vars, IfGoal, ThenGoal, ElseGoal) },
{ goal_info_init(Context, GoalInfo) },
{ Goal = IfThenElse - GoalInfo }
;
@@ -7292,12 +7551,14 @@
VarSet0, VarSet1) },
expand_get_field_function_call(Context, MainContext,
SubContext, FieldNames, X, InputTermVar,
- VarSet1, VarSet2, Functor, _, Goal0, Info1, Info2),
+ VarSet1, VarSet2, Functor, _, Goal0, Info1, Info2,
+ DotColonSubst0, DotColonSubst1, InAtom),
{ ArgContext = functor(Functor, MainContext, SubContext) },
append_arg_unifications([InputTermVar], [InputTerm],
FunctorContext, ArgContext, Goal0,
- VarSet2, Goal, VarSet, Info2, Info)
+ VarSet2, Goal, VarSet, Info2, Info,
+ DotColonSubst1, DotColonSubst, InAtom)
;
% handle field update expressions
{ F = term__atom(":=") },
@@ -7316,20 +7577,23 @@
expand_set_field_function_call(Context, MainContext,
SubContext, FieldNames, FieldValueVar, InputTermVar, X,
VarSet2, VarSet3, Functor,
- InnerFunctor - FieldSubContext, Goal0, Info1, Info2),
+ InnerFunctor - FieldSubContext, Goal0, Info1, Info2,
+ DotColonSubst0, DotColonSubst1, InAtom),
{ TermArgContext = functor(Functor, MainContext, SubContext) },
{ TermArgNumber = 1 },
append_arg_unification(InputTermVar, InputTerm,
FunctorContext, TermArgContext, TermArgNumber,
- TermUnifyConj, VarSet3, VarSet4, Info2, Info3),
+ TermUnifyConj, VarSet3, VarSet4, Info2, Info3,
+ DotColonSubst1, DotColonSubst2, InAtom),
{ FieldArgContext = functor(InnerFunctor,
MainContext, FieldSubContext) },
{ FieldArgNumber = 2 },
append_arg_unification(FieldValueVar, FieldValueTerm,
FunctorContext, FieldArgContext, FieldArgNumber,
- FieldUnifyConj, VarSet4, VarSet, Info3, Info),
+ FieldUnifyConj, VarSet4, VarSet, Info3, Info,
+ DotColonSubst2, DotColonSubst, InAtom),
{ Goal0 = _ - GoalInfo0 },
{ goal_to_conj_list(Goal0, GoalList0) },
@@ -7337,6 +7601,22 @@
GoalList) },
{ conj_list_to_goal(GoalList, GoalInfo0, Goal) }
;
+ { F = term__atom("!.") },
+ { Args = [term__variable(SVar)] }
+ ->
+ { svar_dot(SVar, Var, VarSet0, VarSet,
+ DotColonSubst0, DotColonSubst, InAtom) },
+ { Goal = svar_unification(Context, X, Var) },
+ { Info = Info0 }
+ ;
+ { F = term__atom("!:") },
+ { Args = [term__variable(SVar)] }
+ ->
+ { svar_colon(SVar, Var, VarSet0, VarSet,
+ DotColonSubst0, DotColonSubst, InAtom) },
+ { Goal = svar_unification(Context, X, Var) },
+ { Info = Info0 }
+ ;
{ parse_qualified_term(RHS, RHS, "", MaybeFunctor) },
(
{ MaybeFunctor = ok(FunctorName, FunctorArgs) },
@@ -7358,7 +7638,8 @@
{ add_goal_info_purity_feature(GoalInfo0, Purity,
GoalInfo) },
{ Goal = GoalExpr - GoalInfo },
- { VarSet = VarSet0 }
+ { VarSet = VarSet0 },
+ { DotColonSubst = DotColonSubst0 }
;
{ make_fresh_arg_vars(FunctorArgs, VarSet0,
HeadVars, VarSet1) },
@@ -7377,7 +7658,8 @@
( { Purity = pure } ->
append_arg_unifications(HeadVars, FunctorArgs,
FunctorContext, ArgContext, Goal0,
- VarSet1, Goal, VarSet, Info1, Info)
+ VarSet1, Goal, VarSet, Info1, Info,
+ DotColonSubst0, DotColonSubst, InAtom)
;
{ Goal0 = GoalExpr - GoalInfo0 },
{ add_goal_info_purity_feature(GoalInfo0,
@@ -7385,7 +7667,8 @@
{ Goal1 = GoalExpr - GoalInfo },
insert_arg_unifications(HeadVars, FunctorArgs,
FunctorContext, ArgContext, no, Goal1,
- VarSet1, Goal, VarSet, Info1, Info)
+ VarSet1, Goal, VarSet, Info1, Info,
+ DotColonSubst0, DotColonSubst, InAtom)
)
)
).
@@ -7394,10 +7677,12 @@
% Handle `f(...) = X' in the same way as `X = f(...)'.
unravel_unification(term__functor(F, As, FC), term__variable(Y),
- C, MC, SC, VarSet0, Purity, Goal, VarSet, Info0, Info) -->
+ C, MC, SC, VarSet0, Purity, Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
unravel_unification(term__variable(Y),
term__functor(F, As, FC),
- C, MC, SC, VarSet0, Purity, Goal, VarSet, Info0, Info).
+ C, MC, SC, VarSet0, Purity, Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom).
% If we find a unification of the form `f1(...) = f2(...)',
% then we replace it with `Tmp = f1(...), Tmp = f2(...)',
@@ -7408,18 +7693,21 @@
unravel_unification(term__functor(LeftF, LeftAs, LeftC),
term__functor(RightF, RightAs, RightC),
Context, MainContext, SubContext, VarSet0,
- Purity, Goal, VarSet, Info0, Info) -->
+ Purity, Goal, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom) -->
{ varset__new_var(VarSet0, TmpVar, VarSet1) },
unravel_unification(
term__variable(TmpVar),
term__functor(LeftF, LeftAs, LeftC),
Context, MainContext, SubContext,
- VarSet1, Purity, Goal0, VarSet2, Info0, Info1),
+ VarSet1, Purity, Goal0, VarSet2, Info0, Info1,
+ DotColonSubst0, DotColonSubst1, InAtom),
unravel_unification(
term__variable(TmpVar),
term__functor(RightF, RightAs, RightC),
Context, MainContext, SubContext,
- VarSet2, Purity, Goal1, VarSet, Info1, Info),
+ VarSet2, Purity, Goal1, VarSet, Info1, Info,
+ DotColonSubst1, DotColonSubst, InAtom),
{ goal_info_init(GoalInfo) },
{ goal_to_conj_list(Goal0, ConjList0) },
{ goal_to_conj_list(Goal1, ConjList1) },
@@ -7491,7 +7779,7 @@
build_lambda_expression(X, PredOrFunc, EvalMethod, Args, Modes, Det,
ParsedGoal, VarSet0, Context, MainContext, SubContext,
- Goal, VarSet, Info1, Info) -->
+ Goal, VarSet, Info0, Info) -->
%
% In the parse tree, the lambda arguments can be any terms.
% But in the HLDS, they must be distinct variables. So we introduce
@@ -7530,11 +7818,26 @@
{ list__length(Args, NumArgs) },
{ varset__new_vars(VarSet0, NumArgs, LambdaVars, VarSet1) },
{ map__init(Substitution) },
- transform_goal(ParsedGoal, VarSet1, Substitution,
- HLDS_Goal0, VarSet2, Info1, Info2),
+ { hlds_goal__true_goal(EmptyConj) },
+ { DotColonSubst0 = new_dot_colon_subst },
+ { HeadInAtom = yes(new_svar_subst) },
{ ArgContext = head(PredOrFunc, NumArgs) },
insert_arg_unifications(LambdaVars, Args, Context, ArgContext,
- no, HLDS_Goal0, VarSet2, HLDS_Goal1, VarSet, Info2, Info3),
+ no, EmptyConj, VarSet1, HeadGoal, VarSet2, Info0, Info1,
+ DotColonSubst0, HeadDotColonSubst, HeadInAtom),
+
+ { BodyInAtom = no(HeadDotColonSubst ^ colon_subst) },
+ transform_goal(ParsedGoal, VarSet2, Substitution,
+ BodyGoal0, VarSet, Info1, Info2,
+ DotColonSubst0, BodyDotColonSubst0, BodyInAtom),
+ { insert_dot_svar_unifications(Context,
+ BodyDotColonSubst0, _BodyDotColonSubst,
+ no(HeadDotColonSubst ^ dot_subst), BodyGoal0, BodyGoal) },
+
+ { goal_info_init(Context, GoalInfo) },
+ { goal_to_conj_list(HeadGoal, HeadGoals) },
+ { goal_to_conj_list(BodyGoal, BodyGoals) },
+ { conj_list_to_goal(HeadGoals ++ BodyGoals, GoalInfo, HLDS_Goal0) },
%
% Now figure out which variables we need to explicitly existentially
@@ -7550,9 +7853,7 @@
{ term__vars_list(QuantifiedArgs, QuantifiedVars0) },
{ list__sort_and_remove_dups(QuantifiedVars0, QuantifiedVars) },
- { goal_info_init(Context, GoalInfo) },
- { HLDS_Goal = some(QuantifiedVars, can_remove, HLDS_Goal1)
- - GoalInfo },
+ { HLDS_Goal = some(QuantifiedVars, can_remove, HLDS_Goal0) - GoalInfo },
%
% We set the lambda nonlocals here to anything that could possibly
@@ -7567,7 +7868,7 @@
{ make_atomic_unification(X,
lambda_goal(PredOrFunc, EvalMethod, modes_are_ok,
LambdaNonLocals, LambdaVars, Modes, Det, HLDS_Goal),
- Context, MainContext, SubContext, Goal, Info3, Info) }.
+ Context, MainContext, SubContext, Goal, Info2, Info) }.
%-----------------------------------------------------------------------------%
@@ -7752,19 +8053,26 @@
:- pred get_conj(goal, prog_substitution, list(hlds_goal), prog_varset,
list(hlds_goal), prog_varset, transform_info, transform_info,
- io__state, io__state).
-:- mode get_conj(in, in, in, in, out, out, in, out, di, uo) is det.
+ dot_colon_subst, dot_colon_subst, in_atom, io__state, io__state).
+:- mode get_conj(in, in, in, in, out, out, in, out, in, out, in, di, uo) is det.
-get_conj(Goal, Subst, Conj0, VarSet0, Conj, VarSet, Info0, Info) -->
+get_conj(Goal, Subst, Conj0, VarSet0, Conj, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom0) -->
(
{ Goal = (A,B) - _Context }
->
get_conj(B, Subst, Conj0, VarSet0, Conj1, VarSet1,
- Info0, Info1),
- get_conj(A, Subst, Conj1, VarSet1, Conj, VarSet, Info1, Info)
+ Info0, Info1, DotColonSubst0, DotColonSubst1,
+ InAtom0),
+ { preceding_in_atom(InAtom0, InAtom,
+ DotColonSubst1, DotColonSubst2) },
+ get_conj(A, Subst, Conj1, VarSet1, Conj, VarSet,
+ Info1, Info, DotColonSubst2, DotColonSubst,
+ InAtom)
;
transform_goal(Goal, VarSet0, Subst, Goal1, VarSet,
- Info0, Info),
+ Info0, Info, DotColonSubst0, DotColonSubst,
+ InAtom0),
{ goal_to_conj_list(Goal1, ConjList) },
{ list__append(ConjList, Conj0, Conj) }
).
@@ -7775,44 +8083,62 @@
:- pred get_par_conj(goal, prog_substitution, list(hlds_goal), prog_varset,
list(hlds_goal), prog_varset, transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
io__state, io__state).
-:- mode get_par_conj(in, in, in, in, out, out, in, out, di, uo) is det.
+:- mode get_par_conj(in, in, in, in, out, out, in, out, in, out, in, di, uo)
+ is det.
-get_par_conj(Goal, Subst, ParConj0, VarSet0, ParConj, VarSet, Info0, Info) -->
+get_par_conj(Goal, Subst, ParConj0, VarSet0, ParConj, VarSet, Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom0) -->
(
{ Goal = (A & B) - _Context }
->
get_par_conj(B, Subst, ParConj0, VarSet0, ParConj1, VarSet1,
- Info0, Info1),
+ Info0, Info1,
+ DotColonSubst0, DotColonSubst1, InAtom0),
+ { preceding_in_atom(InAtom0, InAtom,
+ DotColonSubst1, DotColonSubst2) },
get_par_conj(A, Subst, ParConj1, VarSet1, ParConj, VarSet,
- Info1, Info)
+ Info1, Info,
+ DotColonSubst2, DotColonSubst, InAtom)
;
transform_goal(Goal, VarSet0, Subst, Goal1, VarSet,
- Info0, Info),
+ Info0, Info,
+ DotColonSubst0, DotColonSubst, InAtom0),
{ goal_to_par_conj_list(Goal1, ParConjList) },
{ list__append(ParConjList, ParConj0, ParConj) }
).
-% get_disj(Goal, Subst, Disj0, Disj) :
+% get_dot_colon_subst_disj(Goal, Subst, Disj0, Disj) :
% Goal is a tree of disjuncts. Flatten it into a list (applying Subst)
-% append Disj0, and return the result in Disj.
+% append Disj0, and return the result in Disj. Each disjunct is paired
+% with its resulting state variable mapping.
-:- pred get_disj(goal, prog_substitution, list(hlds_goal), prog_varset,
- list(hlds_goal), prog_varset, transform_info, transform_info,
+:- pred get_dot_colon_subst_disj(goal, prog_substitution,
+ dot_colon_subst_goals, prog_varset,
+ dot_colon_subst_goals, prog_varset,
+ transform_info, transform_info,
+ dot_colon_subst, dot_colon_subst, in_atom,
io__state, io__state).
-:- mode get_disj(in, in, in, in, out, out, in, out, di, uo) is det.
+:- mode get_dot_colon_subst_disj(in, in, in, in, out, out, in, out,
+ in, out, in, di, uo) is det.
-get_disj(Goal, Subst, Disj0, VarSet0, Disj, VarSet, Info0, Info) -->
+get_dot_colon_subst_disj(Goal0, Subst, Disj0, VarSet0, Disj, VarSet,
+ Info0, Info, DotColonSubst0, DotColonSubst, InAtom) -->
(
- { Goal = (A;B) - _Context }
+ { Goal0 = (A;B) - _Context }
->
- get_disj(B, Subst, Disj0, VarSet0, Disj1, VarSet1,
- Info0, Info1),
- get_disj(A, Subst, Disj1, VarSet1, Disj, VarSet, Info1, Info)
- ;
- transform_goal(Goal, VarSet0, Subst, Goal1, VarSet,
- Info0, Info),
- { Disj = [Goal1 | Disj0] }
+ get_dot_colon_subst_disj(B, Subst, Disj0,
+ VarSet0, Disj1, VarSet1, Info0, Info1,
+ DotColonSubst0, DotColonSubst1, InAtom),
+ get_dot_colon_subst_disj(A, Subst, Disj1,
+ VarSet1, Disj, VarSet, Info1, Info,
+ DotColonSubst1, DotColonSubst, InAtom)
+ ;
+ transform_goal(Goal0, VarSet0, Subst, Goal, VarSet,
+ Info0, Info, DotColonSubst0, DotColonSubst,
+ InAtom),
+ { Disj = [DotColonSubst - Goal | Disj0] }
).
%-----------------------------------------------------------------------------%
@@ -8553,4 +8879,515 @@
:- func this_file = string.
this_file = "make_hlds.m".
+%------------------------------------------------------------------------------%
+
+ % An dot_colon_subst maps the live current state variables
+ % at each point to the logic variables used to represent them.
+ %
+ % The transformation is applied right-to-left since we don't
+ % want to propagate "dead" state variables.
+ %
+:- type svar_subst == map(prog_var, prog_var).
+
+ % An dot_colon_subst incrementally records the mapping from
+ % !.X and/or !:X to the fresh variables used in each case for
+ % each state variable X used in an atomic goal.
+ %
+:- type dot_colon_subst == pair(svar_subst).
+
+ % InAtom = yes(PostLiveSVarSubst)
+ % When we are processing an atomic formula (such as a call), we
+ % have to ensure that for all state variables X therein, !.X and
+ % !:X have the same respective substitution throughout the atom
+ % and that no intermediate values for X are introduced (for
+ % instance, we don't want this to happen for conjunctions in
+ % the conditions of if-then-else expressions.)
+ %
+ % Example:
+ % p((if q(!.X, !:X), r(!.X, !:X) then a else b))
+ %
+ % should be transformed into
+ %
+ % p((if q(X0, X1), r(X0, X1) then a else b))
+ %
+ % rather than
+ %
+ % p((if q(X0, X1), r(X1, X2) then a else b))
+ %
+ % since the conditional expression occurs inside an
+ % atomic formula and hence cannot introduce
+ % intermediary values for state variables.
+ %
+ % In these cases, PostLiveSVarSubst is the substitution for
+ % each live !.X after the atomic formula in question.
+ %
+ % Processing such goals we essentially extend a DotColonSubst
+ % as state variables are identified in the atomic formula
+ % (taking substitutions for !:X from PostLiveSVarSubst.)
+ %
+ % InAtom = no(PostLiveSVarSubst)
+ % When we are processing compound formulae (such as
+ % conjunctions) we must introduce new substitutions for
+ % state variables.
+ %
+ % Example:
+ % p(!.X, !:X), q(!.X, !:X)
+ %
+ % should be transformed into
+ %
+ % p(X0, X1), q(X1, X2)
+ %
+ % Once an atomic formula has been converted we may need to
+ % * add unifications between the fresh substitution for !.X for
+ % the atomic formula and the substitution for X in
+ % PostLiveSVarSubst if the atomic formula does not set !:X
+ % * and extend the DotColonSubst for !.X with the mapping for
+ % X from PostLiveSVarSubst where neither !:X nor !.X appear in
+ % the atomic formula.
+ %
+ % Example (assumingPostLiveSVarSubst is [X -> X1]):
+ % After transforming
+ %
+ % p(!.X)
+ % to
+ % p(X0)
+ %
+ % will be [!.X -> X0], necessitating adding a unification to
+ % give
+ %
+ % p(X0), X0 = X1
+ %
+ % whereas after transforming
+ %
+ % p
+ % to
+ % p
+ %
+ % the DotColonSubst will be [!.X -> X1] (taking X1 from
+ % the PostLiveSVarSubst).
+ %
+ % The !. mappings from the final DotColonSubst form the
+ % PostLiveSVarSubst for the preceding goal.
+ %
+:- type in_atom
+ ---> yes(svar_subst)
+ ; no(svar_subst).
+
+%------------------------------------------------------------------------------%
+
+:- func new_svar_subst = svar_subst.
+
+new_svar_subst = map__init.
+
+
+:- func new_dot_colon_subst = dot_colon_subst.
+
+new_dot_colon_subst = new_svar_subst - new_svar_subst.
+
+%------------------------------------------------------------------------------%
+
+:- func dot_subst(dot_colon_subst) = svar_subst.
+
+dot_subst(DotSubst - _ColonSubst) = DotSubst.
+
+:- func 'dot_subst :='(svar_subst, dot_colon_subst) = dot_colon_subst.
+
+'dot_subst :='(DotSubst, _ - ColonSubst) = DotSubst - ColonSubst.
+
+
+:- func colon_subst(dot_colon_subst) = svar_subst.
+
+colon_subst(_DotSubst - ColonSubst) = ColonSubst.
+
+:- func 'colon_subst :='(svar_subst, dot_colon_subst) = dot_colon_subst.
+
+'colon_subst :='(ColonSubst, DotSubst - _) = DotSubst - ColonSubst.
+
+%------------------------------------------------------------------------------%
+
+:- func dot(prog_var, dot_colon_subst) = prog_var is semidet.
+
+dot(SVar, DotColonSubst) = DotColonSubst ^ dot_subst ^ elem(SVar).
+
+
+:- func 'dot :='(prog_var, dot_colon_subst, prog_var) = dot_colon_subst.
+
+'dot :='(SVar, DotSVarSubst - ColonSVarSubst, Var) =
+ ( DotSVarSubst ^ elem(SVar) := Var ) - ColonSVarSubst.
+
+
+:- func colon(prog_var, dot_colon_subst) = prog_var is semidet.
+
+colon(SVar, DotColonSubst) = DotColonSubst ^ colon_subst ^ elem(SVar).
+
+
+:- func 'colon :='(prog_var, dot_colon_subst, prog_var) = dot_colon_subst.
+
+'colon :='(SVar, DotSVarSubst - ColonSVarSubst, Var) =
+ DotSVarSubst - ( ColonSVarSubst ^ elem(SVar) := Var ).
+
+%------------------------------------------------------------------------------%
+
+ % Find the mapping for "!.X" or add one if none exists.
+ %
+:- pred svar_dot(prog_var, prog_var, prog_varset, prog_varset,
+ dot_colon_subst, dot_colon_subst, in_atom).
+:- mode svar_dot(in, out, in, out, in, out, in) is det.
+
+svar_dot(SVar, Var, VarSet0, VarSet, DotColonSubst0, DotColonSubst, _InAtom) :-
+ ( if DotColonSubst0 ^ dot(SVar) = Dot then
+ Var = Dot,
+ VarSet = VarSet0,
+ DotColonSubst = DotColonSubst0
+ else
+ new_svar(SVar, Var, VarSet0, VarSet),
+ DotColonSubst = ( DotColonSubst0 ^ dot(SVar) := Var )
+ ).
+
+%------------------------------------------------------------------------------%
+
+ % Find the mapping for !:X or add one if none exists.
+ %
+:- pred svar_colon(prog_var, prog_var, prog_varset, prog_varset,
+ dot_colon_subst, dot_colon_subst, in_atom).
+:- mode svar_colon(in, out, in, out, in, out, in) is det.
+
+svar_colon(SVar, Var, VarSet0, VarSet, DotColonSubst0, DotColonSubst, InAtom) :-
+ ( if DotColonSubst0 ^ colon(SVar) = Colon then
+ Var = Colon,
+ VarSet = VarSet0,
+ DotColonSubst = DotColonSubst0
+ else if in_atom_svar_subst(InAtom) ^ elem(SVar) = Var0 then
+ Var = Var0,
+ VarSet = VarSet0,
+ DotColonSubst = ( DotColonSubst0 ^ colon(SVar) := Var )
+ else
+ new_svar(SVar, Var, VarSet0, VarSet),
+ DotColonSubst = ( DotColonSubst0 ^ colon(SVar) := Var )
+ ).
+
+%------------------------------------------------------------------------------%
+
+ % XXX rafe: we may well have to number the "SVar_(Dot|Colon)_X"s
+ % apart. Since the HLDS is dumped and read in for transitive
+ % intermodule optimization, reusing the same var name won't do.
+
+:- pred new_svar(prog_var, prog_var, prog_varset, prog_varset).
+:- mode new_svar(in, out, in, out) is det.
+
+new_svar(SVar, Var, VarSet0, VarSet) :-
+ VarName = "SVAR_" ++ lookup_name(VarSet0, SVar),
+ varset__new_uniquely_named_var(VarSet0, VarName, Var, VarSet).
+
+%------------------------------------------------------------------------------%
+
+ % This predicate adds unifiers to a tranformed atomic formula
+ % to ensure continuity of state variables. (This does not need
+ % to be done *inside* an atomic formula.)
+ %
+ % Example:
+ % p(!.X)
+ % where InAtom = yes(PostLiveSVars)
+ % and PostLiveSVars ^ elem(X) = X0
+ % will first be transformed into
+ % p(X1)
+ % and extended by calling this predicate to
+ % p(X1), X0 = X1
+ % (!.X is given a new mapping in p(!.X) since
+ % the transformation won't know whether or not
+ % there is a !:X in there or not until it's
+ % finished with p(...), hence the need for
+ % this extra step.)
+ %
+ % Afterwards, the DotColonSubst for p(...) will have
+ % been extended to include any live state variable
+ % mappings in PostLiveSVars that are not clobbered or
+ % shadowed by p(...) (we say that the mapping for !.X
+ % in PostLiveSVars is clobbered if p(...) contains
+ % !:X and is shadowed if p(...) contains !.X).
+ %
+:- pred insert_svar_tie_up_unifications(prog_context, dot_colon_subst,
+ dot_colon_subst, hlds_goal, hlds_goal, in_atom).
+:- mode insert_svar_tie_up_unifications(in, in, out, in, out, in) is det.
+
+ % If we're in the context of an atomic formula then no new
+ % state variable bindings will have been added.
+ %
+insert_svar_tie_up_unifications(_Context, DotColonSubst, DotColonSubst,
+ Goal, Goal, yes(_)).
+
+ % If we aren't in the context of an atomic formula then we may
+ % have introduced new state variable bindings. We also update
+ % DotColonSubst to reflect the liveness of any PostLiveSVars
+ % that are not mentioned in the formula that has just been
+ % transformed.
+ %
+insert_svar_tie_up_unifications(Context, DotColonSubst0, DotColonSubst,
+ Goal0, Goal, no(PostLiveSVars)) :-
+ Goal0 = _ - GoalInfo,
+ goal_to_conj_list(Goal0, Goals0),
+ map__foldl2(
+ insert_svar_tie_up_unification(Context),
+ PostLiveSVars,
+ DotColonSubst0, DotColonSubst,
+ Goals0, Goals
+ ),
+ conj_list_to_goal(Goals, GoalInfo, Goal).
+
+
+:- pred insert_svar_tie_up_unification(prog_context, prog_var, prog_var,
+ dot_colon_subst, dot_colon_subst, hlds_goals, hlds_goals).
+:- mode insert_svar_tie_up_unification(in, in, in, in, out, in, out) is det.
+
+insert_svar_tie_up_unification(Context, SVar, PostLiveVar,
+ DotColonSubst0, DotColonSubst, Goals0, Goals) :-
+ ( if DotColonSubst0 ^ colon(SVar) = _Colon then
+ DotColonSubst = DotColonSubst0, % _Colon = PostLiveVar
+ Goals = Goals0
+ else if DotColonSubst0 ^ dot(SVar) = Dot then
+ DotColonSubst = DotColonSubst0, % Dot \= PostLiveVar
+ Goals = [ svar_unification(Context, PostLiveVar, Dot)
+ | Goals0 ]
+ else
+ DotColonSubst = ( DotColonSubst0 ^ dot(SVar) := PostLiveVar ),
+ Goals = Goals0
+ ).
+
+%------------------------------------------------------------------------------%
+
+:- func svar_unification(prog_context, prog_var, prog_var) = hlds_goal.
+
+svar_unification(Context, SVar, Var) = Unification :-
+ hlds_goal__create_atomic_unification(SVar, var(Var), Context,
+ implicit("state variable"), [], Unification).
+
+%------------------------------------------------------------------------------%
+
+:- type dot_colon_subst_goal == pair(dot_colon_subst, hlds_goal).
+
+:- type dot_colon_subst_goals == list(dot_colon_subst_goal).
+
+ % After transforming (A ; B ; ... ; Z) to [SA - A', SB - B', ...,
+ % SZ - Z'] we find the pre-live state variable mapping S for the
+ % whole disjunction. S is the union of SA, SB, ..., SZ with
+ % the exception that where state variable X has a mapping to two
+ % different logical variables under Si, Sj then S maps X to just
+ % one of them.
+ %
+ % Finally, we translate the original disjunction list into
+ % [A'', B'', ..., Z''] by prepending unifications Si(X) = S(X)
+ % where the former is defined and different to the latter.
+ %
+:- pred insert_disj_list_dot_svar_unifications(prog_context,
+ dot_colon_subst_goals, prog_varset, dot_colon_subst,
+ hlds_goals, prog_varset).
+:- mode insert_disj_list_dot_svar_unifications(in, in, in, out, out, out)
+ is det.
+
+insert_disj_list_dot_svar_unifications(Context,
+ DotColonSubstGoals, VarSet0, DotColonSubst, Goals, VarSet) :-
+ list__foldl2(
+ extend_disj_list_svar_mappings,
+ DotColonSubstGoals,
+ new_dot_colon_subst, DotColonSubst,
+ VarSet0, VarSet
+ ),
+ Goals = list__map(
+ insert_disj_dot_svar_unifications(Context, DotColonSubst),
+ DotColonSubstGoals
+ ).
+
+%------------------------------------------------------------------------------%
+
+ % Special case disjunction state-variable tie-ups for binary
+ % disjunctions and if-then-elses.
+ %
+:- pred insert_binary_disj_dot_svar_unifications(prog_context,
+ dot_colon_subst, dot_colon_subst, dot_colon_subst,
+ hlds_goal, hlds_goal, hlds_goal, hlds_goal,
+ prog_varset, prog_varset).
+:- mode insert_binary_disj_dot_svar_unifications(in, in, in, out,
+ in, out, in, out, in, out) is det.
+
+insert_binary_disj_dot_svar_unifications(Context,
+ DotColonSubstA, DotColonSubstB, DotColonSubst, A0, A, B0, B,
+ VarSet0, VarSet) :-
+ list__foldl2(
+ extend_disj_list_svar_mappings,
+ [DotColonSubstA - A0, DotColonSubstB - B0],
+ new_dot_colon_subst, DotColonSubst,
+ VarSet0, VarSet
+ ),
+ A = insert_disj_dot_svar_unifications(Context,
+ DotColonSubst, DotColonSubstA - A0),
+ B = insert_disj_dot_svar_unifications(Context,
+ DotColonSubst, DotColonSubstB - B0).
+
+%------------------------------------------------------------------------------%
+
+:- pred extend_disj_list_svar_mappings(dot_colon_subst_goal,
+ dot_colon_subst, dot_colon_subst, prog_varset, prog_varset).
+:- mode extend_disj_list_svar_mappings(in, in, out, in, out) is det.
+
+extend_disj_list_svar_mappings(GoalDotColonSubst - _Goal,
+ DotColonSubst0, DotColonSubst, VarSet0, VarSet) :-
+ map__foldl2(
+ extend_disj_svar_mapping,
+ GoalDotColonSubst ^ dot_subst,
+ DotColonSubst0, DotColonSubst,
+ VarSet0, VarSet
+ ).
+
+:- pred extend_disj_svar_mapping(prog_var, prog_var,
+ dot_colon_subst, dot_colon_subst, prog_varset, prog_varset).
+:- mode extend_disj_svar_mapping(in, in, in, out, in, out) is det.
+
+extend_disj_svar_mapping(SVar, _,
+ DotColonSubst0, DotColonSubst, VarSet0, VarSet) :-
+ ( if DotColonSubst0 ^ dot_subst `contains` SVar then
+ DotColonSubst = DotColonSubst0,
+ VarSet = VarSet0
+ else
+ new_svar(SVar, Var, VarSet0, VarSet),
+ DotColonSubst = ( DotColonSubst0 ^ dot(SVar) := Var )
+ ).
+
+%------------------------------------------------------------------------------%
+
+:- func insert_disj_dot_svar_unifications(prog_context,
+ dot_colon_subst, dot_colon_subst_goal) = hlds_goal.
+
+insert_disj_dot_svar_unifications(Context, DotColonSubst,
+ GoalDotColonSubst - Goal0) = Goal :-
+ Goal0 = _ - GoalInfo,
+ goal_to_conj_list(Goal0, Goals0),
+ Goals = map__foldl(
+ insert_disj_dot_svar_unification(Context,
+ DotColonSubst),
+ GoalDotColonSubst ^ dot_subst, Goals0),
+ conj_list_to_goal(Goals, GoalInfo, Goal).
+
+
+:- func insert_disj_dot_svar_unification(prog_context,
+ dot_colon_subst, prog_var, prog_var, hlds_goals) = hlds_goals.
+
+insert_disj_dot_svar_unification(Context, DotColonSubst, SVar, Var, Goals) =
+ ( if DotColonSubst ^ dot(SVar) = Dot, Dot \= Var
+ then [svar_unification(Context, Dot, Var) | Goals]
+ else Goals
+ ).
+
+%------------------------------------------------------------------------------%
+
+ % This predicate adds unifiers to a goal to ensure continuity of
+ % state variables. It is used in two situations:
+ %
+ % 1. To tie the knot in any state variables that are not already tied
+ % in the body of a clause - for example,
+ %
+ % p(A, !.X, !:X) :- q(A).
+ %
+ % will be translated into
+ %
+ % p(A, X1, X0) :- q(A).
+ %
+ % and this predicate will extend the body to tie up !.X and !:X giving
+ %
+ % p(A, X1, X0) :- X0 = X1, q(A).
+ %
+ % 2. A negated goal may not immediately end up with the same mapping
+ % for !.X as the code that follows it - that is we have to ensure
+ % that after partially translating
+ %
+ % not(p(!.X, !:X)), q(!.X)
+ %
+ % into
+ %
+ % not(p(X2, X1)), q(X0)
+ %
+ % we also add a unifier to tie up the !.X's to get
+ %
+ % X0 = X2, not(p(X2, X1)), q(X0)
+ %
+ % In this case we extend the DotColonSubst for the negated goal
+ % to include any live state variable mappings that it does not
+ % clobber or shadow.
+ %
+:- pred insert_dot_svar_unifications(prog_context,
+ dot_colon_subst, dot_colon_subst,
+ in_atom, hlds_goal, hlds_goal).
+:- mode insert_dot_svar_unifications(in, in, out, in, in, out) is det.
+
+insert_dot_svar_unifications(_Context, DotColonSubst, DotColonSubst,
+ yes(_), Goal, Goal).
+
+insert_dot_svar_unifications(Context, DotColonSubst0, DotColonSubst,
+ no(PostLiveSVars), Goal0, Goal) :-
+ Goal0 = _ - GoalInfo,
+ goal_to_conj_list(Goal0, Goals0),
+ map__foldl2(
+ insert_dot_svar_unification(Context),
+ PostLiveSVars,
+ DotColonSubst0, DotColonSubst,
+ Goals0, Goals
+ ),
+ conj_list_to_goal(Goals, GoalInfo, Goal).
+
+
+:- pred insert_dot_svar_unification(prog_context, prog_var, prog_var,
+ dot_colon_subst, dot_colon_subst, hlds_goals, hlds_goals).
+:- mode insert_dot_svar_unification(in, in, in, in, out, in, out) is det.
+
+insert_dot_svar_unification(Context, SVar, PostLiveVar,
+ DotColonSubst0, DotColonSubst, Goals0, Goals) :-
+ ( if DotColonSubst0 ^ dot(SVar) = Dot then
+ DotColonSubst = DotColonSubst0,
+ Goals = [ svar_unification(Context, PostLiveVar, Dot)
+ | Goals0 ]
+ else
+ DotColonSubst = ( DotColonSubst0 ^ dot(SVar) := PostLiveVar ),
+ Goals = Goals0
+ ).
+
+%------------------------------------------------------------------------------%
+
+ % We need to preserve the information as to whether or not
+ % we're in the context of an atomic formula, but propagate
+ % the live state variable mappings.
+ %
+:- pred preceding_in_atom(in_atom, in_atom, dot_colon_subst, dot_colon_subst).
+:- mode preceding_in_atom(in, out, in, out) is det.
+
+preceding_in_atom(yes(_), yes(DotColonSubst ^ dot_subst),
+ DotColonSubst, DotColonSubst).
+
+preceding_in_atom(no(_), no(DotColonSubst ^ dot_subst),
+ DotColonSubst, new_dot_colon_subst).
+
+% XXX rafe: why does the compiler complain about this?
+% :- pred preceding_in_atom(in_atom, in_atom, dot_colon_subst, dot_colon_subst).
+% :- mode preceding_in_atom(in, out, in, out) is det.
+%
+% preceding_in_atom(DotColonSubst, DotColonSubst,
+% yes(_), yes(DotColonSubst ^ dot_subst)).
+%
+% preceding_in_atom(DotColonSubst, new_dot_colon_subst,
+% no(_), no(DotColonSubst ^ dot_subst)).
+
+%------------------------------------------------------------------------------%
+
+:- func in_atom_svar_subst(in_atom) = svar_subst.
+
+in_atom_svar_subst(yes(SVarSubst)) = SVarSubst.
+
+in_atom_svar_subst(no(SVarSubst)) = SVarSubst.
+
+%------------------------------------------------------------------------------%
+
+:- func init_atomic_context(in_atom) = in_atom.
+
+init_atomic_context(no(PostLiveSVars)) = yes(PostLiveSVars).
+init_atomic_context(yes(PostLiveSVars)) = yes(PostLiveSVars).
+
+%------------------------------------------------------------------------------%
%------------------------------------------------------------------------------%
Index: compiler/mercury_compile.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_compile.m,v
retrieving revision 1.243
diff -u -r1.243 mercury_compile.m
--- compiler/mercury_compile.m 2 Apr 2002 16:46:55 -0000 1.243
+++ compiler/mercury_compile.m 4 Apr 2002 06:06:20 -0000
@@ -1826,8 +1826,8 @@
mercury_compile__maybe_unneeded_code(HLDS39, Verbose, Stats, HLDS40),
mercury_compile__maybe_dump_hlds(HLDS40, "40", "unneeded_code"),
- mercury_compile__maybe_lco(HLDS40, Verbose, Stats, HLDS42), !,
- mercury_compile__maybe_dump_hlds(HLDS42, "42", "lco"), !,
+ mercury_compile__maybe_lco(HLDS40, Verbose, Stats, HLDS42),
+ mercury_compile__maybe_dump_hlds(HLDS42, "42", "lco"),
% DNF transformations should be after inlining.
mercury_compile__maybe_transform_dnf(HLDS40, Verbose, Stats, HLDS44),
Index: compiler/prog_io.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io.m,v
retrieving revision 1.205
diff -u -r1.205 prog_io.m
--- compiler/prog_io.m 20 Mar 2002 12:37:11 -0000 1.205
+++ compiler/prog_io.m 8 Apr 2002 05:18:34 -0000
@@ -801,7 +801,8 @@
convert_item(ok(Item, Context), ok(Item, Context)).
convert_item(error(M, T), error(M, T)).
-parse_item(ModuleName, VarSet, Term, Result) :-
+parse_item(ModuleName, VarSet, Term0, Result) :-
+ Term = expand_dot_colon_state_vars(Term0),
( %%% some [Decl, DeclContext]
Term = term__functor(term__atom(":-"), [Decl], _DeclContext)
->
@@ -3415,5 +3416,32 @@
:- pred root_module_name(module_name::out) is det.
root_module_name(unqualified("")).
+
+%------------------------------------------------------------------------------%
+
+:- func expand_dot_colon_state_vars(term) = term.
+
+expand_dot_colon_state_vars(T @ variable(_)) = T.
+
+expand_dot_colon_state_vars(functor(Const, Args, Ctxt)) =
+ functor(
+ Const,
+ list__foldr(expand_dot_colon_state_var, Args, []),
+ Ctxt
+ ).
+
+
+:- func expand_dot_colon_state_var(term, list(term)) = list(term).
+
+expand_dot_colon_state_var(T @ variable(_), Ts) = [T | Ts].
+
+expand_dot_colon_state_var(T @ functor(Const, Args, Ctxt), Ts) =
+ ( if Const = atom("!"), Args = [variable(_SVar)] then
+ [ functor(atom("!."), Args, Ctxt),
+ functor(atom("!:"), Args, Ctxt)
+ | Ts ]
+ else
+ [ expand_dot_colon_state_vars(T) | Ts ]
+ ).
%-----------------------------------------------------------------------------%
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.246
diff -u -r1.246 reference_manual.texi
--- doc/reference_manual.texi 16 Mar 2002 05:37:03 -0000 1.246
+++ doc/reference_manual.texi 8 Apr 2002 06:37:03 -0000
@@ -51,6 +51,7 @@
@author Simon Taylor
@author Chris Speirs
@author Tyson Dowd
+ at author Ralph Becket
@page
@vskip 0pt plus 1filll
Copyright @copyright{} 1995-2001 The University of Melbourne.
@@ -162,6 +163,7 @@
* Facts::
* Rules::
* Goals::
+* State variables::
* DCG-rules::
* DCG-goals::
* Data-terms::
@@ -738,8 +740,192 @@
@end table
+ at node State variables
+ at section State variables
+
+Clauses may use @samp{state variables} as a shorthand for naming
+intermediate values in a sequence. That is, where in the plain syntax one
+might write
+ at example
+ main(IO0, IO) :-
+ io__write_string("The answer is ", IO0, IO1),
+ io__write_int(calculate_answer(@dots{}), IO1, IO2),
+ io__nl(IO3, IO).
+ at end example
+using state variable syntax one could write
+ at example
+ main(!IO) :-
+ io__write_string("The answer is ", !IO),
+ io__write_int(calculate_answer(@dots{}), !IO),
+ io__nl(!IO).
+ at end example
+
+A state variable is written @samp{!. at var{X}} or @samp{!:@var{X}},
+denoting the ``current'' or ``next'' value of the sequence labelled
+ at var{X}. An argument @samp{!@var{X}} is shorthand for two state
+variable arguments @samp{!. at var{X}, !:@var{X}}; that is,
+ at samp{p(@dots{}, !@var{X}, @dots{})} is parsed as
+ at samp{p(@dots{}, !. at var{X}, !:@var{X}, @dots{})}.
+
+Within each clause, a transformation converts state variables into
+sequences of ordinary logic variables. The syntactic conversion is
+described in terms of the notional @samp{transform} function defined
+next.
+
+The transformation is applied once for each state variable @var{X}
+with some fresh variables which we shall call @var{ThisX} and
+ at var{NextX}.
+
+The expression
+ at samp{substitute(@var{Term}, @var{X}, @var{ThisX}, @var{NextX})}
+stands for a copy of @var{Term} with occurrences of @samp{!. at var{X}}
+replaced with @var{ThisX} and occurrences of @samp{!:@var{X}}
+replaced with @var{NextX}.
+
+ at table @code
+
+ at item @var{Head} :- @var{Body}
+ at example
+transform((@var{Head} :- @var{Body}), @var{X}, @var{ThisX}, @var{NextX}) =
+substitute(@var{Head}, @var{X}, @var{ThisX}, @var{NextX}) :- transform(@var{Body}, @var{X}, @var{ThisX}, @var{NextX})
+ at end example
+
+ at item @var{Head} --> @var{Body}
+ at example
+transform((@var{Head} --> @var{Body}), @var{X}, @var{ThisX}, @var{NextX}) =
+substitute(@var{Head}, @var{X}, @var{ThisX}, @var{NextX}) :- transform(@var{Body}, @var{X}, @var{ThisX}, @var{NextX})
+ at end example
+
+ at item @var{Goal1}, @var{Goal2}
+ at example
+transform((@var{Goal1}, @var{Goal2}), @var{X}, @var{ThisX}, @var{NextX}) =
+transform(@var{Goal1}, @var{X}, @var{ThisX}, @var{TmpX}), transform(@var{Goal2}, @var{X}, @var{TmpX}, @var{NextX})
+ at end example
+for some fresh variable @var{TmpX}.
+
+ at item @var{Goal1} ; @var{Goal2}
+ at example
+transform((@var{Goal1} ; @var{Goal2}), @var{X}, @var{ThisX}, @var{NextX}) =
+transform(@var{Goal1}, @var{X}, @var{ThisX}, @var{NextX}) ; transform(@var{Goal2}, @var{X}, @var{ThisX}, @var{NextX})
+ at end example
+
+ at item not @var{Goal}
+ at item \+ @var{Goal}
+A negation. The two different syntaxes have identical semantics.
+ at example
+transform((not @var{Goal}), @var{X}, @var{ThisX}, @var{NextX}) =
+not transform(@var{Goal1}, @var{X}, @var{ThisX}, @var{DummyX}), @var{NextX} = @var{ThisX}
+ at end example
+for some fresh variable @var{DummyX}.
+
+ at item if @var{Goal1} then @var{Goal2} else @var{Goal3}
+ at item @var{Goal1} -> @var{Goal2} ; @var{Goal3}
+An if-then-else. The two different syntaxes have identical semantics.
+ at example
+transform((if @var{Goal1} then @var{Goal2} else @var{Goal3}), @var{X}, @var{ThisX}, @var{NextX}) =
+if transform(@var{Goal1}, @var{X}, @var{ThisX}, @var{TmpX}) then transform(@var{Goal2}, @var{X}, @var{TmpX}, @var{NextX})
+ else transform(@var{Goal3}, @var{X}, @var{ThisX}, @var{NextX})
+ at end example
+for some fresh variable @var{TmpX}.
+
+ at item @var{Goal1} => @var{Goal2}
+ at item @var{Goal2} <= @var{Goal1}
+An implication. The two different syntaxes have identical semantics.
+ at example
+transform((@var{Goal1} => @var{Goal2}), @var{X}, @var{ThisX}, @var{NextX}) =
+transform(@var{Goal1}, @var{X}, @var{ThisX}, @var{TmpX}) => transform(@var{Goal2}, @var{X}, @var{TmpX}, @var{NextX}),
+ at var{NextX} = @var{ThisX}
+ at end example
+for some fresh variable @var{TmpX}.
+
+ at item all @var{Vars} @var{Goal}
+ at example
+transform((all @var{Vars} @var{Goal}), @var{X}, @var{ThisX}, @var{NextX}) =
+all @var{Vars} transform(@var{Goal}, @var{X}, @var{ThisX}, @var{DummyX}), @var{NextX} = @var{ThisX}
+ at end example
+for some fresh variable @var{DummyX}.
+
+ at item some @var{Vars} @var{Goal}
+ at example
+transform((some @var{Vars} @var{Goal}), @var{X}, @var{ThisX}, @var{NextX}) =
+some @var{Vars} transform(@var{Goal}, @var{X}, @var{ThisX}, @var{NextX})
+ at end example
+
+ at item @var{Call_or_Unification}
+If @samp{!:@var{X}} does not appear in @var{Call_or_Unification} then
+ at example
+transform(@var{Call_or_Unification}, @var{X}, @var{ThisX}, @var{NextX}) =
+substitute(@var{Call_or_Unification}, @var{X}, @var{ThisX}, @var{NextX}), @var{NextX} = @var{ThisX}
+ at end example
+If @samp{!:@var{X}} does appear in @var{Call_or_Unification} then
+ at example
+transform(@var{Call_or_Unification}, @var{X}, @var{ThisX}, @var{NextX}) =
+substitute(@var{Call_or_Unification}, @var{X}, @var{ThisX}, @var{NextX})
+ at end example
+
+ at end table
+
+This transformation can lead to the introduction of chains of
+unifications for variables that do not otherwise play a role in the
+definition. Such chains are removed transparently.
+
+Note that subexpressions in goals are not treated independently by the
+tranformation. For instance, the following goal employing an if-then-else
+expression
+ at example
+ @dots{},
+ p((if q(!@var{X}), r(!@var{X}) then @var{A} else @var{B}), !@var{X}),
+ @dots{}
+ at end example
+is equivalent to
+ at example
+ @dots{},
+ @var{ThisX} = !. at var{X},
+ p((if q(@var{ThisX}, @var{NextX}), r(@var{ThisX}, @var{NextX}) then @var{A} else @var{B}), @var{ThisX}, @var{NextX}),
+ !:@var{X} = @var{NextX},
+ @dots{}
+ at end example
+
+The following code fragments illustrate appropriate use of state
+variable syntax.
+
+ at table @b
+
+ at item Threading the IO state
+ at example
+main(!IO) :-
+ io__write_string("The 100th prime is ", !IO),
+ X = prime(100),
+ io__write_int(X, !IO),
+ io__nl(!IO).
+ at end example
+
+ at item Handling accumulators (1)
+ at example
+foldl2(_, [], !A, !B).
+
+foldl2(P, [X | Xs], !A, !B) :-
+ P(X, !A, !B),
+ foldl2(P, Xs, !A, !B).
+ at end example
+
+ at item Handling accumulators (2)
+ at example
+iterate_while2(P, F, !A, !B) :-
+ ( if P(!.A, !.B) then
+ F(!A, !B),
+ iterate_while2(P, F, !A, !B)
+ else
+ true
+ ).
+ at end example
+ at end table
+
@node DCG-rules
@section DCG-rules
+
+(Use of DCG syntax to thread hidden variables is now deprecated; the
+preferred mechanism is to use state variables instead.)
DCG-rules in Mercury have identical syntax and semantics to
DCG-rules in Prolog.
Index: library/builtin.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/builtin.m,v
retrieving revision 1.69
diff -u -r1.69 builtin.m
--- library/builtin.m 13 Mar 2002 12:25:34 -0000 1.69
+++ library/builtin.m 27 Mar 2002 01:56:48 -0000
@@ -169,19 +169,6 @@
%-----------------------------------------------------------------------------%
-
-% We define !/0 (and !/2 for dcgs) to be equivalent to `true'. This is for
-% backwards compatibility with Prolog systems. But of course it only works
-% if all your cuts are green cuts.
-
-:- pred ! is det.
-
-:- pred !(T, T).
-:- mode !(di, uo) is det.
-:- mode !(in, out) is det.
-
-%-----------------------------------------------------------------------------%
-
% unify(X, Y) is true iff X = Y.
:- pred unify(T::in, T::in) is semidet.
@@ -297,11 +284,6 @@
(Y :: out(pred(out, di, uo) is det)),
[will_not_call_mercury, thread_safe],
"Y = X;").
-
-%-----------------------------------------------------------------------------%
-
-!.
-!(X, X).
%-----------------------------------------------------------------------------%
Index: library/lexer.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/lexer.m,v
retrieving revision 1.35
diff -u -r1.35 lexer.m
--- library/lexer.m 8 Mar 2002 06:10:09 -0000 1.35
+++ library/lexer.m 27 Mar 2002 01:56:50 -0000
@@ -511,8 +511,8 @@
lexer__special_token('|', ht_sep).
lexer__special_token(',', comma).
lexer__special_token(';', name(";")).
-lexer__special_token('!', name("!")).
+lexer__graphic_token_char('!').
lexer__graphic_token_char('#').
lexer__graphic_token_char('$').
lexer__graphic_token_char('&').
Index: library/ops.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/ops.m,v
retrieving revision 1.39
diff -u -r1.39 ops.m
--- library/ops.m 8 Feb 2002 02:27:15 -0000 1.39
+++ library/ops.m 27 Mar 2002 01:56:51 -0000
@@ -346,6 +346,9 @@
ops__op_table("where", after, xfx, 1175). % NU-Prolog extension (*)
ops__op_table("~", before, fy, 900). % Goedel (*)
ops__op_table("~=", after, xfx, 700). % NU-Prolog (*)
+ops__op_table("!", before, fx, 40). % Mercury extension
+ops__op_table("!.", before, fx, 40). % Mercury extension
+ops__op_table("!:", before, fx, 40). % Mercury extension
% (*) means that the operator is not useful in Mercury
% and is provided only for compatibility.
Index: library/prolog.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/prolog.m,v
retrieving revision 1.10
diff -u -r1.10 prolog.m
--- library/prolog.m 25 May 1998 21:47:42 -0000 1.10
+++ library/prolog.m 11 Feb 2002 06:01:40 -0000
@@ -16,20 +16,6 @@
:- interface.
:- import_module std_util, list.
-% We define !/0 (and !/2 for dcgs) to be equivalent to `true'. This is for
-% backwards compatibility with Prolog systems. But of course it only works
-% if all your cuts are green cuts.
-
-/********
-cut is currently defined in builtin.m, for historical reasons.
-
-:- pred ! is det.
-
-:- pred !(T, T).
-:- mode !(di, uo) is det.
-:- mode !(in, out) is det.
-********/
-
% Prolog arithmetic operators.
:- pred T =:= T. % In Mercury, just use =
@@ -95,12 +81,6 @@
:- implementation.
:- import_module require, int.
-
-/*********
-% !/0 and !/2 currently defined in builtin.m, for historical reasons.
-!.
-!(X, X).
-*********/
% we use module qualifiers here to avoid
% overriding the builtin Prolog versions
Index: library/term.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/term.m,v
retrieving revision 1.100
diff -u -r1.100 term.m
--- library/term.m 9 Jan 2001 23:30:19 -0000 1.100
+++ library/term.m 8 Apr 2002 05:42:25 -0000
@@ -279,6 +279,11 @@
% create a fresh variable (var) and return the
% updated var_supply.
+:- func term__var_id(var(T)) = int.
+% term__var_id(Variable) :
+% returns a unique number associated with this variable w.r.t.
+% its originating var_supply.
+
%-----------------------------------------------------------------------------%
% from_int/1 should only be applied to integers returned
@@ -1073,6 +1078,10 @@
term__create_var(var_supply(V0), var(V), var_supply(V)) :-
V is V0 + 1.
+
+%------------------------------------------------------------------------------%
+
+term__var_id(var(V)) = V.
%-----------------------------------------------------------------------------%
Index: library/varset.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/varset.m,v
retrieving revision 1.65
diff -u -r1.65 varset.m
--- library/varset.m 20 Feb 2002 03:14:36 -0000 1.65
+++ library/varset.m 8 Apr 2002 05:31:19 -0000
@@ -52,6 +52,11 @@
:- pred varset__new_named_var(varset(T), string, var(T), varset(T)).
:- mode varset__new_named_var(in, in, out, out) is det.
+ % create a new named variable with a unique (w.r.t. the
+ % varset) number appended to the name.
+:- pred varset__new_uniquely_named_var(varset(T), string, var(T), varset(T)).
+:- mode varset__new_uniquely_named_var(in, in, out, out) is det.
+
% create a new variable, and maybe give it a name
:- pred varset__new_maybe_named_var(varset(T), maybe(string),
var(T), varset(T)).
@@ -259,6 +264,12 @@
varset(MaxId, Names, Vals)) :-
term__create_var(MaxId0, Var, MaxId),
map__set(Names0, Var, Name, Names).
+
+varset__new_uniquely_named_var(varset(MaxId0, Names0, Vals), Name, Var,
+ varset(MaxId, Names, Vals)) :-
+ term__create_var(MaxId0, Var, MaxId),
+ N = term__var_id(Var),
+ map__set(Names0, Var, string__format("%s_%d", [s(Name), i(N)]), Names).
varset__new_maybe_named_var(varset(MaxId0, Names0, Vals), MaybeName, Var,
varset(MaxId, Names, Vals)) :-
--------------------------------------------------------------------------
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