[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