[m-rev.] For review: State Variables

Ralph Becket rafe at cs.mu.OZ.AU
Thu May 2 16:03:05 AEST 2002


After four attempts...  This is an almost entirely new implementation
and employs Simon's suggestion that all state variables should be either
listed in the head of a clause or lambda or explicitly introduced in a
some or all quantifier.  An `external' state variable X in scope may
only be referred to via !.X inside the body of a lambda or the condition
of an if-then-else expression.


Estimated hours taken: 340
Branches: main

Added state variables to the language.  State variables provide a
lightweight syntax for giving names to sequences that bear some
resemblance to destructively updated variables found in imperative
languages.  Code using state variables is translated into code that
uses only ordinary logic variables.  State variables are intended
to simplify code that passes (multiple) in-out state threads, without
the limitations attached to abusing DCG syntax for this purpose.

NEWS:
	Mention the addition of state variables to the language and
	provide a pointer to the relevant documentation.

compiler/hlds_goal.m:
	Added the implicit/1 constructor to the unify_main_contxt
	type.  This constructor is there for unifications added
	by source-to-source transformations.

compiler/hlds_out.m:
	Add a clause to write_unify_main_context to handle the new
	implicit/1 constructor.

compiler/make_hlds.m:
	Added the machinery implementing the state variable transformation.

compiler/mercury_compile.m:
	Removed two spurious Prolog cuts left over from long ago.

compiler/mercury_to_mercury.m:
	Added clauses to mercury_output_goal_2 to handle the new
	constructors some_state_vars/2 and all_state_vars/2.

compiler/module_qual.m:
	Added clauses to process_assert to handle the new
	constructors some_state_vars/2 and all_state_vars/2.

compiler/prog_data.m:
	Added the constructors some_state_vars/2 and all_state_vars/2
	to the goal_expr type.  These constructors are used to separate
	out local state variables introduced by explicit quantification.

compiler/prog_io_goal.m:
	Added clauses to parse_goal_2 to extract state variables
	introduced via some/2 and all/2 constructs and record them
	in some_state_vars/2 and all_state_vars/2 respectively.
	Fixed a bug in the "all" case which previously did not handle
	malformed variable lists properly.

compiler/prog_util.m:
	Added clauses to rename_in_goal_expr to handle the new
	constructors some_state_vars/2 and all_state_vars/2.

doc/reference_manual.texi:
	Added documentation in a new section, "State variables".

library/builtin.m:
	Removed implementations for Prolog's cut.  The new state variable
	syntax makes use of `!'.

library/lexer.m:
	Changed `!' from being a special token to being an ordinary graphic
	token.

library/ops.m:
	Added the prefix operators `!', `!.' and `!:'.

library/prolog.m:
	Removed commented out implementations of Prolog cut.

tests/general/Mmakefile:
tests/general/state_vars_tests.exp:
tests/general/state_vars_tests.m:
	Added a suite of tests for code using state variables.


Index: NEWS
===================================================================
RCS file: /home/mercury1/repository/mercury/NEWS,v
retrieving revision 1.255
diff -u -r1.255 NEWS
--- NEWS	15 Apr 2002 05:03:58 -0000	1.255
+++ NEWS	18 Apr 2002 07:22:57 -0000
@@ -30,6 +30,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,6 +111,9 @@
   extensions which are unlikely to be implemented.
 
 Changes to the Mercury standard library:
+
+* 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
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.408
diff -u -r1.408 make_hlds.m
--- compiler/make_hlds.m	7 Apr 2002 10:22:34 -0000	1.408
+++ compiler/make_hlds.m	2 May 2002 05:30:12 -0000
@@ -3582,9 +3582,12 @@
 :- mode module_add_clause(in, in, in, in, in, in, in, in, in,
 		out, in, out, di, uo) is det.
 
-module_add_clause(ModuleInfo0, ClauseVarSet, PredOrFunc, PredName, Args, Body,
+module_add_clause(ModuleInfo0, ClauseVarSet, PredOrFunc, PredName, Args0, Body,
 			Status, Context, GoalType, ModuleInfo,
 			Info0, Info) -->
+
+	{ Args = expand_dot_colon_state_var_args(Args0) },
+
 	globals__io_lookup_bool_option(very_verbose, VeryVerbose),
 	( { VeryVerbose = yes } ->
 		io__write_string("% Processing clause for "),
@@ -5294,7 +5297,8 @@
 	transform(Subst, HeadVars, Args, Body, VarSet1, Context, PredOrFunc,
 			Arity, GoalType, Goal0, VarSet, Warnings,
 			transform_info(Module0, Info1),
-			transform_info(Module, Info2)),
+			transform_info(Module, Info2),
+			new_svar_info),
 	{ TVarSet = Info2 ^ tvarset },
 	{ qual_info_get_found_syntax_error(Info2, FoundError) },
 	{ qual_info_set_found_syntax_error(no, Info2, Info) },
@@ -5534,8 +5538,10 @@
 			% substitutions, and they will be.
 		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),
+				new_svar_info, _),
 		{
 		map__init(EmptyVarTypes),
 		implicitly_quantify_clause_body(HeadVars,
@@ -5572,33 +5578,47 @@
 :- pred transform(prog_substitution, list(prog_var), list(prog_term), goal,
 		prog_varset, prog_context, pred_or_func, arity, goal_type,
 		hlds_goal, prog_varset, list(quant_warning),
-		transform_info, transform_info,
+		transform_info, transform_info, svar_info,
 		io__state, io__state).
 :- mode transform(in, in, in, in, in, in, in, in, in, out, out, out,
-		in, out, di, uo) is det.
+		in, out, in, 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),
-	{ 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) },
+transform(Subst, HeadVars, Args0, Body0, VarSet0, Context, PredOrFunc,
+		Arity, GoalType, Goal, VarSet, Warnings, Info0, Info,
+		SInfo0, IO0, IO) :-
+
+	term__apply_substitution_to_list(Args0, Subst, Args),
+
+	hlds_goal__true_goal(Head0),
+
+	prepare_for_head(SInfo0, SInfo1),
+
+	( if GoalType = promise(_) then
+		VarSet1 = VarSet0,
+		Head    = Head0,
+		Info1   = Info0,
+		SInfo2  = SInfo1,
+		IO1     = IO0
+	  else
+		ArgContext = head(PredOrFunc, Arity),
 		insert_arg_unifications(HeadVars, Args, Context, ArgContext,
-			no, Goal1, VarSet1, Goal2, VarSet2, Info1, Info2)
+			no, Head0, VarSet0, Head, VarSet1, Info0, Info1,
+			SInfo1, SInfo2, IO0, IO1)
 	),
-	{ VarTypes2 = Info2 ^ qual_info ^ vartypes },
-	{ implicitly_quantify_clause_body(HeadVars, Goal2, VarSet2, VarTypes2,
-		Goal, VarSet, VarTypes, Warnings) },
-	{ Info = Info2 ^ qual_info ^ vartypes := VarTypes }.
+
+	prepare_for_body(FinalSVarMap, VarSet1, VarSet2, SInfo2, SInfo3),
+
+	transform_goal(Body0, VarSet2, Subst, Body, VarSet3, Info1, Info2,
+		SInfo3, SInfo, IO1, IO),
+
+	finish_head_and_body(Context, FinalSVarMap, Head, Body, Goal0,
+		SInfo),
+
+	VarTypes2 = Info2 ^ qual_info ^ vartypes,
+	implicitly_quantify_clause_body(HeadVars, Goal0, VarSet3, VarTypes2,
+		Goal, VarSet, VarTypes, Warnings),
+
+	Info = Info2 ^ qual_info ^ vartypes := VarTypes.
 
 %-----------------------------------------------------------------------------%
 
@@ -5612,89 +5632,129 @@
 
 :- pred transform_goal(goal, prog_varset, prog_substitution, hlds_goal,
 		prog_varset, transform_info, transform_info,
-		io__state, io__state).
-:- mode transform_goal(in, in, in, out, out, in, out, di, uo) is det.
+		svar_info, svar_info, io__state, io__state).
+:- mode transform_goal(in, in, in, out, out, in, out, in, out, di, uo) is det.
 
 transform_goal(Goal0 - Context, VarSet0, Subst, Goal1 - GoalInfo1, VarSet,
-		Info0, Info) -->
+		Info0, Info, SInfo0, SInfo) -->
 	transform_goal_2(Goal0, Context, VarSet0, Subst, Goal1 - GoalInfo0,
-					VarSet, Info0, Info),
+					VarSet, Info0, Info, SInfo0, SInfo),
 	{ 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, svar_info, svar_info,
+		io__state, io__state).
+:- mode transform_goal_2(in, in, in, in, out, out, in, out, in, out, di, uo)
+		is det.
 
 transform_goal_2(fail, _, VarSet, _, disj([]) - GoalInfo, VarSet,
-		Info, Info) -->
+		Info, Info, SInfo, SInfo) -->
 	{ goal_info_init(GoalInfo) }.
 
 transform_goal_2(true, _, VarSet, _, conj([]) - GoalInfo, VarSet,
-		Info, Info) -->
+		Info, Info, SInfo, SInfo) -->
 	{ goal_info_init(GoalInfo) }.
 
 	% 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, SInfo0, SInfo) -->
 	{ TransformedGoal = not(some(Vars0, not(Goal0) - Context) - Context) },
 	transform_goal_2(TransformedGoal, Context, VarSet0, Subst,
-						Goal, VarSet, Info0, Info).
+		Goal, VarSet, Info0, Info, SInfo0, SInfo).
+
+transform_goal_2(all_state_vars(StateVars, Goal0), Context, VarSet0, Subst,
+		Goal, VarSet, Info0, Info, SInfo0, SInfo) -->
+	transform_goal_2(
+		not(some_state_vars(StateVars, not(Goal0) - Context) - Context),
+		Context, VarSet0, Subst, Goal, VarSet,
+		Info0, Info, SInfo0, SInfo).
 
 transform_goal_2(some(Vars0, Goal0), _, VarSet0, Subst,
 		some(Vars, can_remove, Goal) - GoalInfo,
-		VarSet, Info0, Info) -->
+		VarSet, Info0, Info, SInfo0, SInfo) -->
 	{ substitute_vars(Vars0, Subst, Vars) },
-	transform_goal(Goal0, VarSet0, Subst, Goal, VarSet, Info0, Info),
+	transform_goal(Goal0, VarSet0, Subst, Goal, VarSet, Info0, Info,
+		SInfo0, SInfo),
 	{ goal_info_init(GoalInfo) }.
 
+transform_goal_2(some_state_vars(StateVars0, Goal0), _, VarSet0, Subst,
+		some(Vars, can_remove, Goal) - GoalInfo,
+		VarSet, Info0, Info, SInfo0, SInfo) -->
+	{ substitute_vars(StateVars0, Subst, StateVars) },
+	{ prepare_for_local_state_vars(StateVars, VarSet0, VarSet1,
+		SInfo0, SInfo1) },
+	transform_goal(Goal0, VarSet1, Subst, Goal, VarSet, Info0, Info,
+		SInfo1, SInfo2),
+	{ finish_local_state_vars(StateVars, Vars, SInfo0, SInfo2, SInfo) },
+	{ goal_info_init(GoalInfo) }.
 
-transform_goal_2(if_then_else(Vars0, A0, B0, C0), _, VarSet0, Subst,
+transform_goal_2(if_then_else(Vars0, A0, B0, C0), Context, VarSet0, Subst,
 		if_then_else(Vars, A, B, C) - GoalInfo, VarSet,
-		Info0, Info) -->
+		Info0, Info, SInfo0, SInfo) -->
 	{ 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),
-	{ goal_info_init(GoalInfo) }.
+	transform_goal(A0, VarSet0, Subst, A, VarSet1, Info0, Info1,
+		SInfo0, SInfo1),
+	transform_goal(B0, VarSet1, Subst, B1, VarSet2, Info1, Info2,
+		SInfo1, SInfoB),
+	transform_goal(C0, VarSet2, Subst, C1, VarSet3, Info2, Info,
+		SInfo0, SInfoC),
+	{ goal_info_init(GoalInfo) },
+	{ finish_if_then_else(Context, B1, B, C1, C, VarSet3, VarSet,
+		SInfoB, SInfoC, SInfo) }.
 
 transform_goal_2(if_then(Vars0, A0, B0), Context, Subst, VarSet0,
-		Goal, VarSet, Info0, Info) -->
+		Goal, VarSet, Info0, Info, SInfo0, SInfo) -->
 	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,
+		SInfo0, SInfo).
 
-transform_goal_2(not(A0), _, VarSet0, Subst, Goal, VarSet, Info0, Info) -->
-	transform_goal(A0, VarSet0, Subst, A, VarSet, Info0, Info),
+transform_goal_2(not(A0), Context, VarSet0, Subst, Goal, VarSet, Info0, Info,
+		SInfo0, SInfo) -->
+	transform_goal(A0, VarSet0, Subst, A, VarSet1, Info0, Info,
+		SInfo0, SInfo1),
 	{ 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),
+	{ Goal0 = not(A) - GoalInfo },
+	{ finish_negation(Context, Goal0, Goal, VarSet1, VarSet,
+		SInfo0, SInfo1, SInfo) }.
+
+transform_goal_2((A0, B0), _, VarSet0, Subst, Goal, VarSet, Info0, Info,
+		SInfo0, SInfo) -->
+	get_conj(A0, Subst, [], VarSet0, L0, VarSet1, Info0, Info1,
+		SInfo0, SInfo1),
+	get_conj(B0, Subst, L0, VarSet1, L1, VarSet, Info1, Info,
+		SInfo1, SInfo),
+	{ L = list__reverse(L1) },
 	{ 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,
+		SInfo0, SInfo) -->
+	get_par_conj(B0, Subst, [], VarSet0, L0, VarSet1, Info0, Info1,
+		SInfo0, SInfo1),
+	get_par_conj(A0, Subst, L0, VarSet1, L1, VarSet, Info1, Info,
+		SInfo1, SInfo),
+	{ L = list__reverse(L1) },
 	{ 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,
+		SInfo0, SInfo) -->
+	get_disj(B0, Subst, [], VarSet0, L0, VarSet1, Info0, Info1, SInfo0),
+	get_disj(A0, Subst, L0, VarSet1, L1, VarSet2, Info1, Info, SInfo0),
+	{ finish_disjunction(Context, L1, L, VarSet2, VarSet, SInfo) },
 	{ 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, SInfo0, SInfo) -->
 		% `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, SInfo0, SInfo).
 
-transform_goal_2(equivalent(P0, Q0), _Context, VarSet0, Subst, Goal, VarSet,
-		Info0, Info) -->
+transform_goal_2(equivalent(P0, Q0), Context, VarSet0, Subst, Goal, VarSet,
+		Info0, Info, SInfo0, SInfo) -->
 	%
 	% `P <=> Q' is defined as `(P => Q), (Q => P)',
 	% but that transformation must not be done until
@@ -5703,19 +5763,26 @@
 	% of the variables inside them.
 	%
 	{ goal_info_init(GoalInfo) },
-	transform_goal(P0, VarSet0, Subst, P, VarSet1, Info0, Info1),
-	transform_goal(Q0, VarSet1, Subst, Q, VarSet, Info1, Info),
-	{ Goal = shorthand(bi_implication(P, Q)) - GoalInfo }.
+	transform_goal(P0, VarSet0, Subst, P, VarSet1, Info0, Info1,
+		SInfo0, SInfo1),
+	transform_goal(Q0, VarSet1, Subst, Q, VarSet2, Info1, Info,
+		SInfo1, SInfo2),
+	{ Goal0 = shorthand(bi_implication(P, Q)) - GoalInfo },
+	{ finish_equivalence(Context, Goal0, Goal, VarSet2, VarSet,
+		SInfo0, SInfo2, SInfo) }.
 
 transform_goal_2(call(Name, Args0, Purity), Context, VarSet0, Subst, Goal,
-		VarSet, Info0, Info) -->
+		VarSet, Info0, Info, SInfo0, SInfo) -->
+	{ prepare_for_call(SInfo0, SInfo1) },
+	{ Args1  = expand_dot_colon_state_var_args(Args0) },
 	( 
 		{ Name = unqualified("\\=") },
-		{ Args0 = [LHS, RHS] }
+		{ Args1 = [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, Goal, VarSetX, Info0, Info,
+			SInfo1, SInfoX)
 	;
 		% check for a DCG field access goal:
 		% get:  Field =^ field
@@ -5725,9 +5792,9 @@
 		; { Operator = ":=" }
 		)
 	->
-		{ term__apply_substitution_to_list(Args0, Subst, Args1) },
-		transform_dcg_record_syntax(Operator, Args1, Context,
-			VarSet0, Goal, VarSet, Info0, Info)
+		{ term__apply_substitution_to_list(Args1, Subst, Args2) },
+		transform_dcg_record_syntax(Operator, Args2, Context,
+			VarSet0, Goal, VarSetX, Info0, Info, SInfo1, SInfoX)
 	;
 		% check for an Aditi builtin
 		{ Purity = pure },
@@ -5743,11 +5810,11 @@
 		%; Name1 = "aditi_modify"
 		}
 	->
-		{ term__apply_substitution_to_list(Args0, Subst, Args1) },
-		transform_aditi_builtin(Name1, Args1, Context, VarSet0,
-			Goal, VarSet, Info0, Info)
+		{ term__apply_substitution_to_list(Args1, Subst, Args2) },
+		transform_aditi_builtin(Name1, Args2, Context, VarSet0,
+			Goal, VarSetX, Info0, Info, SInfo1, SInfoX)
 	;
-		{ term__apply_substitution_to_list(Args0, Subst, Args) },
+		{ term__apply_substitution_to_list(Args1, Subst, Args) },
 		{ make_fresh_arg_vars(Args, VarSet0, HeadVars, VarSet1) },
 		{ list__length(Args, Arity) },
 		(
@@ -5805,27 +5872,32 @@
 			Info0, Info1) },
 		insert_arg_unifications(HeadVars, Args,
 			Context, call(CallId), no,
-			Goal0, VarSet1, Goal, VarSet, Info1, Info)
-	).
+			Goal0, VarSet1, Goal, VarSetX, Info1, Info,
+			SInfo1, SInfoX)
+	),
+	{ finish_call(VarSetX, VarSet, SInfoX, SInfo) }.
 
 transform_goal_2(unify(A0, B0, Purity), Context, VarSet0, Subst, Goal, VarSet,
-		Info0, Info) -->
+		Info0, Info, SInfo0, SInfo) -->
+	{ prepare_for_call(SInfo0, SInfo1) },
 	{ term__apply_substitution(A0, Subst, A) },
 	{ term__apply_substitution(B0, Subst, B) },
 	unravel_unification(A, B, Context, explicit, [],
-			VarSet0, Purity, Goal, VarSet, Info0, Info).
+		VarSet0, Purity, Goal, VarSet1, Info0, Info,
+		SInfo1, SInfo2),
+	{ finish_call(VarSet1, VarSet, SInfo2, SInfo) }.
 	
 
 :- 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, svar_info, svar_info, 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, di, uo) is det.
 
 transform_dcg_record_syntax(Operator, ArgTerms0, Context, VarSet0,
-		Goal, VarSet, Info0, Info) -->
+		Goal, VarSet, Info0, Info, SInfo0, SInfo) -->
 	{ goal_info_init(Context, GoalInfo) },
 	(
 		{ ArgTerms0 = [LHSTerm, RHSTerm,
@@ -5851,8 +5923,8 @@
 					TermOutputTerm] },
 
 			transform_dcg_record_syntax_2(AccessType,
-				FieldNames, ArgTerms, Context, VarSet0, Goal,
-				VarSet, Info0, Info)
+				FieldNames, ArgTerms, Context, VarSet0,
+				Goal, VarSet, Info0, Info, SInfo0, SInfo)
 		;
 			{ MaybeFieldNames = error(Msg, ErrorTerm) },
 			{ invalid_goal("^", ArgTerms0, GoalInfo,
@@ -5876,7 +5948,8 @@
 			io__write_string(Msg),
 			io__write_string(" at term `"),
 			term_io__write_term(VarSet, ErrorTerm),
-			io__write_string("'.\n")
+			io__write_string("'.\n"),
+			{ SInfo = SInfo0 }
 		)
 	;
 		{ invalid_goal("^", ArgTerms0, GoalInfo,
@@ -5891,18 +5964,20 @@
 		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"),
+		{ SInfo = SInfo0 }
 	).
 
 :- 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, svar_info, svar_info,
+		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, 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, SInfo0, SInfo, IO0, IO) :-
 	make_fresh_arg_vars(ArgTerms, VarSet0, ArgVars, VarSet1),
 	( ArgVars = [FieldValueVar, TermInputVar, TermOutputVar] ->
 		(
@@ -5911,7 +5986,7 @@
 				FieldNames, FieldValueVar, TermInputVar,
 				TermOutputVar, VarSet1, VarSet2, Functor,
 				InnermostFunctor - InnermostSubContext, Goal0,
-				Info0, Info1, IO0, IO1),
+				Info0, Info1, SInfo0, SInfo1, IO0, IO1),
 
 
 			FieldArgNumber = 2,
@@ -5937,15 +6012,16 @@
 				OutputTermArgNumber - OutputTermArgContext
 			],
 			insert_arg_unifications_with_supplied_contexts(ArgVars,
-				ArgTerms, ArgContexts, Context, Goal0, VarSet2,
-				Goal, VarSet, Info1, Info, IO1, IO)
+				ArgTerms, ArgContexts, Context, Goal0,
+				VarSet2, Goal, VarSet, Info1, Info,
+				SInfo1, SInfo, 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, SInfo0, SInfo1, IO0, IO1),
 			InputTermArgNumber = 1,
 			InputTermArgContext = functor(Functor, explicit, []),
 
@@ -5969,8 +6045,9 @@
 				OutputTermArgNumber - OutputTermArgContext
 			],
 			insert_arg_unifications_with_supplied_contexts(ArgVars,
-				ArgTerms, ArgContexts, Context, Goal0, VarSet2,
-				Goal, VarSet, Info1, Info, IO1, IO)
+				ArgTerms, ArgContexts, Context, Goal0,
+				VarSet2, Goal, VarSet, Info1, Info,
+				SInfo1, SInfo, IO1, IO)
 		)
 	;
 		error("make_hlds__do_transform_dcg_record_syntax")
@@ -5991,18 +6068,19 @@
 		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, svar_info, svar_info,
+		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, 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, SInfo0, SInfo) -->
 	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, SInfo0, SInfo),
 	{ goal_info_init(Context, GoalInfo) },
 	{ conj_list_to_goal(Goals, GoalInfo, Goal) }.
 
@@ -6011,17 +6089,19 @@
 		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, svar_info, svar_info,
+		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, 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, SInfo0, SInfo) -->
 	{ make_fresh_arg_vars(FieldArgs, VarSet0, FieldArgVars, VarSet1) },
 	( { FieldNames = [_|_] } ->
 		{ varset__new_var(VarSet1, SubTermInputVar, VarSet2) },
@@ -6046,7 +6126,7 @@
 		expand_set_field_function_call_2(Context, MainContext,
 			SubContext, FieldNames, FieldValueVar, SubTermInputVar,
 			SubTermOutputVar, VarSet3, VarSet4, _,
-			FieldSubContext, Goals0, Info2, Info3),
+			FieldSubContext, Goals0, Info2, Info3, SInfo0, SInfo1),
 
 		{ list__append([GetSubFieldGoal | Goals0],
 			[UpdateGoal], Goals1) }
@@ -6058,14 +6138,15 @@
 			MainContext, SubContext0, FieldName, TermOutputVar,
 			SetArgs, Functor, Goal, Info0, Info3) },
 		{ FieldSubContext = Functor - SubContext0 },
-		{ Goals1 = [Goal] }
+		{ Goals1 = [Goal] },
+		{ SInfo1 = SInfo0 }
 
 	),
 	{ 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, SInfo1, SInfo),
 	{ goal_to_conj_list(Conj, Goals) }.
 
 	% Expand a field extraction goal into a list of goals which
@@ -6084,14 +6165,15 @@
 		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).
-:- mode expand_dcg_field_extraction_goal(in, in, in, in, in,
-		in, in, in, out, out, out, out, in, out, di, uo) is det.
+		transform_info, transform_info, svar_info, svar_info,
+		io__state, io__state).
+:- mode expand_dcg_field_extraction_goal(in, in, in, in, in, in, in,
+		in, out, out, out, out, in, out, in, out, 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, SInfo0, SInfo) -->
 	% unify the DCG input and output variables
 	{ make_atomic_unification(TermOutputVar, var(TermInputVar),
 			Context, MainContext, SubContext, UnifyDCG,
@@ -6101,7 +6183,7 @@
 	% 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, SInfo0, SInfo),
 	{ Goals = [UnifyDCG | Goals1] },
 	{ goal_info_init(Context, GoalInfo) },
 	{ conj_list_to_goal(Goals, GoalInfo, Goal) }.
@@ -6120,16 +6202,17 @@
 		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, svar_info, svar_info,
+		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, 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, SInfo0, SInfo) -->
 	expand_get_field_function_call_2(Context, MainContext, SubContext0,
-		FieldNames, FieldValueVar, TermInputVar,
-		VarSet0, VarSet, Functor, FieldSubContext, Goals, Info0, Info),
+		FieldNames, FieldValueVar, TermInputVar, VarSet0, VarSet,
+		Functor, FieldSubContext, Goals, Info0, Info, SInfo0, SInfo),
 	{ goal_info_init(Context, GoalInfo) },
 	{ conj_list_to_goal(Goals, GoalInfo, Goal) }.
 
@@ -6137,17 +6220,19 @@
 		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, svar_info, svar_info,
+		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, 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, SInfo0, SInfo) -->
 	{ make_fresh_arg_vars(FieldArgs, VarSet0, FieldArgVars, VarSet1) },
 	{ GetArgVars = list__append(FieldArgVars, [TermInputVar]) },
 	( { FieldNames = [_|_] } ->
@@ -6163,7 +6248,7 @@
 		expand_get_field_function_call_2(Context, MainContext,
 			SubContext, FieldNames, FieldValueVar, SubTermInputVar,
 			VarSet2, VarSet3, _, FieldSubContext,
-			Goals1, Info1, Info2),
+			Goals1, Info1, Info2, SInfo0, SInfo1),
 		{ Goals2 = [Goal | Goals1] }
 	;
 		{ VarSet3 = VarSet1 },
@@ -6171,13 +6256,14 @@
 		{ construct_field_access_function_call(get, Context,
 			MainContext, SubContext0, FieldName, FieldValueVar,
 			GetArgVars, Functor, Goal, Info0, Info2) },
-		{ Goals2 = [Goal] }
+		{ Goals2 = [Goal] },
+		{ SInfo1 = SInfo0 }
 	),
 	{ 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, SInfo1, SInfo),
 	{ goal_to_conj_list(Conj, Goals) }.
 
 :- pred construct_field_access_function_call(field_access_type, prog_context,
@@ -6254,12 +6340,13 @@
 	% 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).
-:- mode transform_aditi_builtin(in(aditi_update_str), in,
-		in, in, out, out, in, out, di, uo) is det.
+		transform_info, transform_info, svar_info, svar_info,
+		io__state, io__state).
+:- mode transform_aditi_builtin(in(aditi_update_str), in, in,
+		in, out, out, in, out, in, out, di, uo) is det.
 
 transform_aditi_builtin(UpdateStr, Args0, Context, VarSet0,
-		Goal, VarSet, Info0, Info) -->
+		Goal, VarSet, Info0, Info, SInfo0, SInfo) -->
 	(
 		{ UpdateStr = "aditi_insert", InsertDelete = insert
 		; UpdateStr = "aditi_delete", InsertDelete = delete
@@ -6267,7 +6354,7 @@
 	->
 		transform_aditi_tuple_insert_delete(UpdateStr, InsertDelete,
 			Args0, Context, VarSet0, Goal,
-			VarSet, Info0, Info)
+			VarSet, Info0, Info, SInfo0, SInfo)
 	;
 		{
 			UpdateStr = "aditi_insert",
@@ -6297,19 +6384,20 @@
 		},
 		transform_aditi_insert_delete_modify(UpdateStr,
 			Update, Args0, Context, VarSet0, Goal,
-			VarSet, Info0, Info)
+			VarSet, Info0, Info, SInfo0, SInfo)
 		
 	).
 
 :- 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, svar_info, svar_info,
+		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, di, uo) is det.
 
 transform_aditi_tuple_insert_delete(UpdateStr, InsertDelete, Args0, Context,
-		VarSet0, Goal, VarSet, Info0, Info) -->
+		VarSet0, Goal, VarSet, Info0, Info, SInfo0, SInfo) -->
 	% Build an empty goal_info. 
 	{ goal_info_init(Context, GoalInfo) },
 
@@ -6360,8 +6448,9 @@
 			{ record_called_pred_or_func(PredOrFunc, SymName, 
 				InsertArity, Info0, Info1) },
 			insert_arg_unifications(AllArgs, AllArgTerms,
-				Context, call(CallId), no,
-				Goal0, VarSet3, Goal, VarSet, Info1, Info)
+				Context, call(CallId), no, Goal0,
+				VarSet3, Goal, VarSet, Info1, Info,
+				SInfo0, SInfo)
 		;
 			{ invalid_goal(UpdateStr, Args0, GoalInfo,
 				Goal, VarSet0, VarSet) },
@@ -6374,7 +6463,8 @@
 			io__write(InsertDelete),
 			io__write_string(" in `"),
 			io__write_string(UpdateStr),
-			io__write_string("'.\n")
+			io__write_string("'.\n"),
+			{ SInfo = SInfo0 }
 		)
 	;
 		{ invalid_goal(UpdateStr, Args0, GoalInfo,
@@ -6383,19 +6473,20 @@
 			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]),
+		{ SInfo = SInfo0 }
 	).
 
 	% 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, svar_info, svar_info, 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, di, uo) is det.
 
 transform_aditi_insert_delete_modify(Descr, InsertDelMod, Args0, Context,
-		VarSet0, UpdateGoal, VarSet, Info0, Info) -->
+		VarSet0, UpdateGoal, VarSet, Info0, Info, SInfo0, SInfo) -->
 	{ goal_info_init(Context, GoalInfo) },
 	(
 		{ list__length(Args0, Arity) },
@@ -6407,7 +6498,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]),
+		{ SInfo = SInfo0 }
 	;
 		%
 		% First syntax -
@@ -6460,12 +6552,11 @@
 		{ parse_goal(GoalTerm, VarSet1, ParsedGoal, VarSet2) },
 		{ map__init(Substitution) },
 		transform_goal(ParsedGoal, VarSet2, Substitution,
-			PredGoal0, VarSet3, Info0, Info1),
+			PredGoal0, VarSet3, Info0, Info1, SInfo0, SInfo1),
 		{ ArgContext = head(PredOrFunc, PredArity) },
 		insert_arg_unifications(HeadArgs, HeadArgs1, Context,
 			ArgContext, no, PredGoal0, VarSet3, PredGoal1, VarSet4,
-			Info1, Info2),
-
+			Info1, Info2, SInfo1, SInfo2), 
 		% Quantification will reduce this down to
 		% the proper set of nonlocal arguments.
 		{ goal_util__goal_vars(PredGoal, LambdaGoalVars0) }, 
@@ -6535,8 +6626,8 @@
 		insert_arg_unifications(AllArgs,
 			[term__variable(LambdaVar), AditiState0Term,
 				AditiStateTerm],
-			Context, CallId, no, UpdateConj, VarSet7, UpdateGoal,
-			VarSet, Info4, Info)
+			Context, CallId, no, UpdateConj,
+			VarSet7, UpdateGoal, VarSet, Info4, Info, SInfo2, SInfo)
 	;
 		%
 		% Second syntax -
@@ -6576,7 +6667,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, SInfo0, SInfo)
 	;
 		{ invalid_goal(Descr, Args0, GoalInfo,
 			UpdateGoal, VarSet0, VarSet) },
@@ -6584,7 +6676,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),
+		{ SInfo = SInfo0 }
 	).
 
 :- pred aditi_delete_insert_delete_modify_goal_info(aditi_insert_delete_modify,
@@ -6814,22 +6907,23 @@
 :- 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,
-		io__state, io__state).
+		svar_info, svar_info, 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, di, uo) is det.
 
 insert_arg_unifications(HeadVars, Args, Context, ArgContext, ForPragmaC,
-		Goal0, VarSet0, Goal, VarSet, Info0, Info) -->
+		Goal0, VarSet0, Goal, VarSet, Info0, Info, SInfo0, SInfo) -->
 	( { HeadVars = [] } ->
 		{ Goal = Goal0 },
 		{ VarSet = VarSet0 },
-		{ Info = Info0 }
+		{ Info = Info0 },
+		{ SInfo = SInfo0 }
 	;
 		{ Goal0 = _ - GoalInfo0 },
 		{ goal_to_conj_list(Goal0, List0) },
 		insert_arg_unifications_2(HeadVars, Args, Context, ArgContext,
 			ForPragmaC, 0, List0, VarSet0, List, VarSet,
-			Info0, Info),
+			Info0, Info, SInfo0, SInfo),
 		{ goal_info_set_context(GoalInfo0, Context, GoalInfo) },
 		{ conj_list_to_goal(List, GoalInfo, Goal) }
 	).
@@ -6837,55 +6931,59 @@
 :- 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, svar_info, svar_info,
+		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, 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, SInfo, SInfo) --> [].
 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, SInfo0, SInfo) -->
 	{ N1 is N0 + 1 },
 	insert_arg_unification(Var, Arg, Context, ArgContext,
 		ForPragmaC, N1, List0, VarSet0, List1, VarSet1, ArgUnifyConj,
-		Info0, Info1),
+		Info0, Info1, SInfo0, SInfo1),
 	(
 		{ ArgUnifyConj = [] }
 	->
 		insert_arg_unifications_2(Vars, Args, Context, ArgContext,
 			ForPragmaC, N1, List1, VarSet1, List, VarSet,
-			Info1, Info)
+			Info1, Info, SInfo1, SInfo)
 	;
 		insert_arg_unifications_2(Vars, Args, Context, ArgContext,
 			ForPragmaC, N1, List1, VarSet1, List2, VarSet,
-			Info1, Info),
+			Info1, Info, SInfo1, SInfo),
 		{ 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).
-:- mode insert_arg_unifications_with_supplied_contexts(in, in, in, in, in, in,
-		out, out, in, out, di, uo) is det.
+		transform_info, transform_info, svar_info, svar_info,
+		io__state, io__state).
+:- mode insert_arg_unifications_with_supplied_contexts(in, in, in, in, in,
+		in, out, out, in, out, in, out, di, uo) is det.
 
 insert_arg_unifications_with_supplied_contexts(ArgVars,
 		ArgTerms, ArgContexts, Context, Goal0, VarSet0,
-		Goal, VarSet, Info0, Info) -->
+		Goal, VarSet, Info0, Info, SInfo0, SInfo) -->
 	( { ArgVars = [] } ->
 		{ Goal = Goal0 },
 		{ VarSet = VarSet0 },
-		{ Info = Info0 }
+		{ Info = Info0 },
+		{ SInfo = SInfo0 }
 	;
 		{ 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, SInfo0, SInfo),
 		{ goal_info_set_context(GoalInfo0, Context, GoalInfo) },
 		{ conj_list_to_goal(GoalList, GoalInfo, Goal) }
 	).
@@ -6893,18 +6991,21 @@
 :- 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, svar_info, svar_info,
+		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, 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,
+		SInfo0, SInfo) -->
 	(
 		{ Vars = [], Terms = [], ArgContexts = [] }
 	->
 		{ List = List0 },
 		{ VarSet = VarSet0 },
-		{ Info = Info0 }
+		{ Info = Info0 },
+		{ SInfo = SInfo0 }
 	;
 		{ Vars = [Var | Vars1] },
 		{ Terms = [Term | Terms1] },
@@ -6912,10 +7013,10 @@
 	->
 		insert_arg_unification(Var, Term, Context, ArgContext, no,
 			ArgNumber, List0, VarSet0, List1, VarSet1,
-			UnifyConj, Info0, Info1),
+			UnifyConj, Info0, Info1, SInfo0, SInfo1),
 		insert_arg_unifications_with_supplied_contexts_2(Vars1, Terms1,
 			ArgContexts1, Context, List1, VarSet1, List2, VarSet,
-			Info1, Info),
+			Info1, Info, SInfo1, SInfo),
 		{ list__append(UnifyConj, List2, List) }
 	;
 		{ error("insert_arg_unifications_with_supplied_contexts") }
@@ -6925,12 +7026,13 @@
 		prog_context, arg_context, bool, int,
 		list(hlds_goal), prog_varset, list(hlds_goal), prog_varset,
 		list(hlds_goal), transform_info, transform_info,
-		io__state, io__state).
+		svar_info, svar_info, 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, di, uo) is det.
 
 insert_arg_unification(Var, Arg, Context, ArgContext, ForPragmaC, N1,
-		List0, VarSet0, List1, VarSet1, ArgUnifyConj, Info0, Info) -->
+		List0, VarSet0, List1, VarSet1, ArgUnifyConj,
+		Info0, Info, SInfo0, SInfo) -->
 	(
 		{ Arg = term__variable(Var) }
 	->
@@ -6938,7 +7040,8 @@
 		{ VarSet1 = VarSet0 },
 		{ Info = Info0 },
 		{ ArgUnifyConj = [] },
-		{ List1 = List0 }
+		{ List1 = List0 },
+		{ SInfo = SInfo0 }
 	;
 		{ Arg = term__variable(ArgVar) },
 		{ ForPragmaC = yes }
@@ -6949,19 +7052,20 @@
 		{ ArgUnifyConj = [] },
 		{ map__init(Subst0) },
 		{ map__det_insert(Subst0, ArgVar, Var, Subst) },
-		{ goal_util__rename_vars_in_goals(List0, no, Subst,
-			List1) },
+		{ goal_util__rename_vars_in_goals(List0, no, Subst, List1) },
 		{ varset__search_name(VarSet0, ArgVar, ArgVarName) ->
 			varset__name_var(VarSet0, Var, ArgVarName, VarSet1)
 		;
 			VarSet1 = VarSet0
-		}
+		},
+		{ SInfo = SInfo0 }
 	;
 		{ 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, VarSet1, Info0, Info,
+			SInfo0, SInfo),
 		{ goal_to_conj_list(Goal, ArgUnifyConj) },
 		{ List1 = List0 }
 	).
@@ -6973,65 +7077,73 @@
 :- 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,
-		io__state, io__state).
+		svar_info, svar_info, 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, di, uo) is det.
 
-append_arg_unifications(HeadVars, Args, Context, ArgContext, Goal0, VarSet0,
-			Goal, VarSet, Info0, Info) -->
+append_arg_unifications(HeadVars, Args, Context, ArgContext, Goal0,
+		VarSet0, Goal, VarSet, Info0, Info, SInfo0, SInfo) -->
 	( { HeadVars = [] } ->
 		{ Goal = Goal0 },
 		{ VarSet = VarSet0 },
-		{ Info = Info0 }
+		{ Info = Info0 },
+		{ SInfo = SInfo0 }
 	;
 		{ 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,
+			SInfo0, SInfo),
 		{ 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,
-	io__state, io__state).
+	svar_info, svar_info, 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, 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, SInfo, SInfo) --> [].
 append_arg_unifications_2([Var|Vars], [Arg|Args], Context, ArgContext, N0,
-			List0, VarSet0, List, VarSet, Info0, Info) -->
+		List0, VarSet0, List, VarSet,
+		Info0, Info, SInfo0, SInfo) -->
 	{ N1 is N0 + 1 },
 	append_arg_unification(Var, Arg, Context, ArgContext,
-		N1, ConjList, VarSet0, VarSet1, Info0, Info1),
+		N1, ConjList, VarSet0, VarSet1,
+		Info0, Info1, SInfo0, SInfo1),
 	{ 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, SInfo1, SInfo).
 
 :- 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, svar_info, svar_info,
+		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, di, uo) is det.
 
-append_arg_unification(Var, Arg, Context, ArgContext,
-		N1, ConjList, VarSet0, VarSet, Info0, Info) -->
+append_arg_unification(Var, Arg, Context, ArgContext, N1, ConjList,
+		VarSet0, VarSet, Info0, Info, SInfo0, SInfo) -->
 	( { Arg = term__variable(Var) } ->
 		% skip unifications of the form `X = X'
 		{ Info = Info0 },
 		{ VarSet = VarSet0 },
-		{ ConjList = [] }
+		{ ConjList = [] },
+		{ SInfo = SInfo0 }
 	;
 		{ 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,
+			SInfo0, SInfo),
 		{ goal_to_conj_list(Goal, ConjList) }
 	).
 
@@ -7104,15 +7216,15 @@
 :- 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,
-		io__state, io__state).
+		svar_info, svar_info, 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, 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, SInfo, SInfo) -->
 	{ make_atomic_unification(X, var(Y), Context, MainContext,
 		SubContext, Goal, Info0, Info1) },
 	check_expr_purity(Purity, Context, Info1, Info),
@@ -7128,10 +7240,28 @@
 	% In the trivial case `X = c', no unravelling occurs.
 
 unravel_unification(term__variable(X), RHS,
-			Context, MainContext, SubContext, VarSet0, Purity,
-			Goal, VarSet, Info0, Info) -->
+		Context, MainContext, SubContext, VarSet0, Purity,
+		Goal, VarSet, Info0, Info, SInfo0, SInfo) -->
 	{ RHS = term__functor(F, Args, FunctorContext) },
 	(
+		% Handle !.X state variable references.
+		{ F = term__atom("!.") },
+		{ Args = [term__variable(StateVar)] }
+	->
+		dot(Context, StateVar, Var, VarSet0, VarSet,
+			SInfo0, SInfo),
+		{ Goal = svar_unification(Context, X, Var) },
+		{ Info = Info0 }
+	;
+		% Handle !:X state variable references.
+		{ F = term__atom("!:") },
+		{ Args = [term__variable(StateVar)] }
+	->
+		colon(Context, StateVar, Var, VarSet0, VarSet,
+			SInfo0, SInfo),
+		{ Goal = svar_unification(Context, X, Var) },
+		{ Info = Info0 }
+	;
 		% Handle explicit type qualification.
 		{ F = term__atom("with_type") },
 		{ Args = [RVal, DeclType0] }
@@ -7142,7 +7272,7 @@
 			Context, Info0, Info1),
 		unravel_unification(term__variable(X), RVal,
 			Context, MainContext, SubContext, VarSet0,
-			Purity, Goal, VarSet, Info1, Info)
+			Purity, Goal, VarSet, Info1, Info, SInfo0, SInfo)
 	;
 		% Handle unification expressions.
 		{ F = term__atom("@") },
@@ -7150,10 +7280,12 @@
 	->
 		unravel_unification(term__variable(X), LVal,
 			Context, MainContext, SubContext,
-			VarSet0, Purity, Goal1, VarSet1, Info0, Info1),
+			VarSet0, Purity, Goal1, VarSet1, Info0, Info1,
+			SInfo0, SInfo1),
 		unravel_unification(term__variable(X), RVal,
 			Context, MainContext, SubContext,
-			VarSet1, Purity, Goal2, VarSet, Info1, Info),
+			VarSet1, Purity, Goal2, VarSet, Info1, Info,
+			SInfo1, SInfo),
 		{ goal_info_init(GoalInfo) },
 		{ goal_to_conj_list(Goal1, ConjList1) },
 		{ goal_to_conj_list(Goal2, ConjList2) },
@@ -7201,7 +7333,8 @@
 		build_lambda_expression(X, PredOrFunc, EvalMethod, Vars1,
 			Modes, Det, ParsedGoal, VarSet1,
 			Context, MainContext, SubContext, Goal, VarSet,
-			Info2, Info)
+			Info2, Info, SInfo0),
+		{ SInfo = SInfo0 }
 	;
 	    {
 		% handle higher-order dcg pred expressions -
@@ -7225,7 +7358,8 @@
 		build_lambda_expression(X, predicate, EvalMethod, Vars1,
 			Modes, Det, ParsedGoal, VarSet1,
 			Context, MainContext, SubContext, Goal0, VarSet,
-			Info1, Info),
+			Info1, Info, SInfo0),
+		{ SInfo = SInfo0 },
 		{ Goal0 = GoalExpr - GoalInfo0 },
 		{ add_goal_info_purity_feature(GoalInfo0, Purity, GoalInfo) },
 		{ Goal = GoalExpr - GoalInfo }
@@ -7246,16 +7380,18 @@
 		{ parse_some_vars_goal(IfTerm, VarSet0, Vars,
 			IfParseTree, VarSet11) }
 	->
+		{ prepare_for_if_then_else_expr_condition(SInfo0, SInfo1) },
 		check_expr_purity(Purity, Context, Info0, Info1),
-		{ map__init(Subst) },
-		transform_goal(IfParseTree, VarSet11, Subst, IfGoal, VarSet22,
-			Info1, Info2),
+		{ map__init(EmptySubst) },
+		transform_goal(IfParseTree, VarSet11, EmptySubst,
+			IfGoal, VarSet22, Info1, Info2, SInfo1, SInfo2),
+		{ finish_if_then_else_expr_condition(SInfo0, SInfo2, SInfo3) },
 		unravel_unification(term__variable(X), ThenTerm,
 			Context, MainContext, SubContext, VarSet22, 
-			pure, ThenGoal, VarSet33, Info2, Info3),
+			pure, ThenGoal, VarSet33, Info2, Info3, SInfo3, SInfo4),
 		unravel_unification(term__variable(X), ElseTerm,
 			Context, MainContext, SubContext, VarSet33, pure,
-			ElseGoal, VarSet, Info3, Info),
+			ElseGoal, VarSet, Info3, Info, SInfo4, SInfo),
 		{ IfThenElse = if_then_else(Vars, IfGoal,
 			ThenGoal, ElseGoal) },
 		{ goal_info_init(Context, GoalInfo) },
@@ -7272,12 +7408,13 @@
 			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,
+			SInfo0, SInfo1),
 
 		{ ArgContext = functor(Functor, MainContext, SubContext) },
 		append_arg_unifications([InputTermVar], [InputTerm],
 			FunctorContext, ArgContext, Goal0,
-			VarSet2, Goal, VarSet, Info2, Info)
+			VarSet2, Goal, VarSet, Info2, Info, SInfo1, SInfo)
 	;
 		% handle field update expressions
 		{ F = term__atom(":=") },
@@ -7296,20 +7433,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,
+			SInfo0, SInfo1),
 
 		{ 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,
+			SInfo1, SInfo2),
 
 		{ 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,
+			SInfo2, SInfo),
 
 		{ Goal0 = _ - GoalInfo0 },
 		{ goal_to_conj_list(Goal0, GoalList0) },
@@ -7338,7 +7478,8 @@
 			{ add_goal_info_purity_feature(GoalInfo0, Purity,
 				GoalInfo) },
 			{ Goal = GoalExpr - GoalInfo },
-			{ VarSet = VarSet0 }
+			{ VarSet = VarSet0 },
+			{ SInfo = SInfo0 }
 		;
 			{ make_fresh_arg_vars(FunctorArgs, VarSet0,
 				HeadVars, VarSet1) },
@@ -7357,7 +7498,8 @@
 			( { Purity = pure } ->
 				append_arg_unifications(HeadVars, FunctorArgs,
 					FunctorContext, ArgContext, Goal0,
-					VarSet1, Goal, VarSet, Info1, Info)
+					VarSet1, Goal, VarSet,
+					Info1, Info, SInfo0, SInfo)
 			;
 				{ Goal0 = GoalExpr - GoalInfo0 },
 				{ add_goal_info_purity_feature(GoalInfo0,
@@ -7365,7 +7507,8 @@
 				{ Goal1 = GoalExpr - GoalInfo },
 				insert_arg_unifications(HeadVars, FunctorArgs,
 					FunctorContext, ArgContext, no, Goal1,
-					VarSet1, Goal, VarSet, Info1, Info)
+					VarSet1, Goal, VarSet,
+					Info1, Info, SInfo0, SInfo)
 			)
 		)
 	).
@@ -7374,10 +7517,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,
+		SInfo0, SInfo) -->
 	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,
+		SInfo0, SInfo).
 
 	% If we find a unification of the form `f1(...) = f2(...)',
 	% then we replace it with `Tmp = f1(...), Tmp = f2(...)',
@@ -7386,20 +7531,20 @@
 	% away type errors.
 
 unravel_unification(term__functor(LeftF, LeftAs, LeftC),
-			term__functor(RightF, RightAs, RightC),
-			Context, MainContext, SubContext, VarSet0,
-			Purity, Goal, VarSet, Info0, Info) -->
+		term__functor(RightF, RightAs, RightC),
+		Context, MainContext, SubContext, VarSet0,
+		Purity, Goal, VarSet, Info0, Info, SInfo0, SInfo) -->
 	{ 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, SInfo0, SInfo1),
 	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, SInfo1, SInfo),
 	{ goal_info_init(GoalInfo) },
 	{ goal_to_conj_list(Goal0, ConjList0) },
 	{ goal_to_conj_list(Goal1, ConjList1) },
@@ -7465,13 +7610,13 @@
 		list(prog_term), list(mode), determinism, goal, prog_varset,
 		prog_context, unify_main_context, unify_sub_contexts,
 		hlds_goal, prog_varset, transform_info, transform_info,
-		io__state, io__state).
+		svar_info, io__state, io__state).
 :- mode build_lambda_expression(in, in, in, in, in, in, in, in,
-		in, in, in, out, out, in, out, di, uo) is det.
+		in, in, in, out, out, in, out, in, di, uo) is det.
 
 build_lambda_expression(X, PredOrFunc, EvalMethod, Args, Modes, Det,
 		ParsedGoal, VarSet0, Context, MainContext, SubContext,
-		Goal, VarSet, Info1, Info) -->
+		Goal, VarSet, Info1, Info, SInfo0) -->
 	%
 	% In the parse tree, the lambda arguments can be any terms.
 	% But in the HLDS, they must be distinct variables.  So we introduce
@@ -7510,11 +7655,21 @@
 	{ list__length(Args, NumArgs) },
 	{ varset__new_vars(VarSet0, NumArgs, LambdaVars, VarSet1) },
 	{ map__init(Substitution) },
-	transform_goal(ParsedGoal, VarSet1, Substitution,
-			HLDS_Goal0, VarSet2, Info1, Info2),
+	{ prepare_for_head(SInfo0, SInfo1) },
+	{ hlds_goal__true_goal(Head0) },
 	{ ArgContext = head(PredOrFunc, NumArgs) },
+
 	insert_arg_unifications(LambdaVars, Args, Context, ArgContext,
-		no, HLDS_Goal0, VarSet2, HLDS_Goal1, VarSet, Info2, Info3),
+		no, Head0, VarSet1, Head, VarSet2, Info1, Info2,
+		SInfo1, SInfo2),
+
+	{ prepare_for_body(FinalSVarMap, VarSet2, VarSet3, SInfo2, SInfo3) },
+
+	transform_goal(ParsedGoal, VarSet3, Substitution,
+		Body, VarSet, Info2, Info3, SInfo3, SInfo4),
+
+	{ finish_head_and_body(Context, FinalSVarMap, Head, Body, HLDS_Goal0,
+		SInfo4) },
 
 	%
 	% Now figure out which variables we need to explicitly existentially
@@ -7531,8 +7686,7 @@
 	{ 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
@@ -7714,15 +7868,19 @@
 :- pred substitute_vars(list(var(T)), substitution(T), list(var(T))).
 :- mode substitute_vars(in, in, out) is det.
 
-substitute_vars([], _, []).
-substitute_vars([Var0 | Vars0], Subst, [Var | Vars]) :-
+substitute_vars(Vars0, Subst, Vars) :-
+	Vars = list__map(substitute_var(Subst), Vars0).
+
+
+:- func substitute_var(substitution(T), var(T)) = var(T).
+
+substitute_var(Subst, Var0) = Var :-
 	term__apply_substitution(term__variable(Var0), Subst, Term),
 	( Term = term__variable(Var1) ->
 		Var = Var1
 	;
-		error("substitute_vars: invalid substitution")
-	),
-	substitute_vars(Vars0, Subst, Vars).
+		error("substitute_var: invalid substitution")
+	).
 
 %-----------------------------------------------------------------------------%
 
@@ -7732,19 +7890,21 @@
 
 :- 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.
+	svar_info, svar_info, io__state, io__state).
+:- mode get_conj(in, in, in, in, out, out, in, out, in, out, di, uo) is det.
 
-get_conj(Goal, Subst, Conj0, VarSet0, Conj, VarSet, Info0, Info) -->
+get_conj(Goal, Subst, Conj0, VarSet0, Conj, VarSet, Info0, Info,
+		SInfo0, SInfo) -->
 	(
 		{ Goal = (A,B) - _Context }
 	->
-		get_conj(B, Subst, Conj0, VarSet0, Conj1, VarSet1,
-						Info0, Info1),
-		get_conj(A, Subst, Conj1, VarSet1, Conj, VarSet, Info1, Info)
+		get_conj(A, Subst, Conj0, VarSet0, Conj1, VarSet1,
+			Info0, Info1, SInfo0, SInfo1),
+		get_conj(B, Subst, Conj1, VarSet1, Conj, VarSet,
+			Info1, Info,  SInfo1, SInfo)
 	;
 		transform_goal(Goal, VarSet0, Subst, Goal1, VarSet,
-						Info0, Info),
+			Info0, Info,  SInfo0, SInfo),
 		{ goal_to_conj_list(Goal1, ConjList) },
 		{ list__append(ConjList, Conj0, Conj) }
 	).
@@ -7755,20 +7915,21 @@
 
 :- pred get_par_conj(goal, prog_substitution, list(hlds_goal), prog_varset,
 		list(hlds_goal), prog_varset, transform_info, transform_info,
-		io__state, io__state).
-:- mode get_par_conj(in, in, in, in, out, out, in, out, di, uo) is det.
+		svar_info, svar_info, io__state, io__state).
+:- mode get_par_conj(in, in, in, in, out, out, in, out, in, out, 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,
+		SInfo0, SInfo) -->
 	(
 		{ Goal = (A & B) - _Context }
 	->
-		get_par_conj(B, Subst, ParConj0, VarSet0, ParConj1, VarSet1,
-						Info0, Info1),
-		get_par_conj(A, Subst, ParConj1, VarSet1, ParConj, VarSet,
-						Info1, Info)
+		get_par_conj(A, Subst, ParConj0, VarSet0, ParConj1, VarSet1,
+			Info0, Info1, SInfo0, SInfo1),
+		get_par_conj(B, Subst, ParConj1, VarSet1, ParConj, VarSet,
+			Info1, Info,  SInfo1, SInfo)
 	;
 		transform_goal(Goal, VarSet0, Subst, Goal1, VarSet,
-						Info0, Info),
+			Info0, Info,  SInfo0, SInfo),
 		{ goal_to_par_conj_list(Goal1, ParConjList) },
 		{ list__append(ParConjList, ParConj0, ParConj) }
 	).
@@ -7777,22 +7938,24 @@
 % 	Goal is a tree of disjuncts.  Flatten it into a list (applying Subst)
 %	append Disj0, and return the result in Disj.
 
-:- pred get_disj(goal, prog_substitution, list(hlds_goal), prog_varset,
-		list(hlds_goal), prog_varset, transform_info, transform_info,
-		io__state, io__state).
-:- mode get_disj(in, in, in, in, out, out, in, out, di, uo) is det.
+:- pred get_disj(goal, prog_substitution, hlds_goal_svar_infos, prog_varset,
+		hlds_goal_svar_infos, prog_varset,
+		transform_info, transform_info,
+		svar_info, io__state, io__state).
+:- mode get_disj(in, in, in, in, out, out, in, out, in, di, uo) is det.
 
-get_disj(Goal, Subst, Disj0, VarSet0, Disj, VarSet, Info0, Info) -->
+get_disj(Goal, Subst, Disj0, VarSet0, Disj, VarSet, Info0, Info, SInfo) -->
 	(
 		{ Goal = (A;B) - _Context }
 	->
 		get_disj(B, Subst, Disj0, VarSet0, Disj1, VarSet1,
-							Info0, Info1),
-		get_disj(A, Subst, Disj1, VarSet1, Disj, VarSet, Info1, Info)
+			Info0, Info1, SInfo),
+		get_disj(A, Subst, Disj1, VarSet1, Disj, VarSet,
+			Info1, Info, SInfo)
 	;
 		transform_goal(Goal, VarSet0, Subst, Goal1, VarSet,
-							Info0, Info),
-		{ Disj = [Goal1 | Disj0] }
+			Info0, Info, SInfo, SInfo1),
+		{ Disj = [{Goal1, SInfo1} | Disj0] }
 	).
 
 %-----------------------------------------------------------------------------%
@@ -8543,4 +8706,647 @@
 :- func this_file = string.
 this_file = "make_hlds.m".
 
+%------------------------------------------------------------------------------%
+
+	% This synonym improves code legibility.
+	%
+:- type svar == prog_var.
+
+:- type svars == list(svar).
+
+	% A set of state variables.
+	%
+:- type svar_set == set(svar).
+
+	% A mapping from state variables to logical variables.
+	%
+:- type svar_map == map(svar, prog_var).
+
+	% This controls how state variables are dealt with.
+	%
+:- type svar_ctxt
+	--->	in_head		% In the head of a clause or lambda.
+	;	in_body		% In the body of a clause or lambda.
+	;	in_atom(svar_set, svar_info).
+				% In the context of an atomic goal at the
+				% level of the source code (the 1st argument
+				% is the set of state variables X that have
+				% been referenced as !:X in the arguments of
+				% the atomic goal; the 2nd argument is the
+				% "parent" svar_info, used to keep track of
+				% nesting in subterms of an atomic formula.)
+
+:- type svar_info
+	--->	svar_info(
+			ctxt		::	svar_ctxt,
+			num		::	int,
+				%
+				% This is used to number state variables and
+				% is incremented for each source-level
+				% conjunct.
+			external_dot	::	svar_map,
+				%
+				% The "read only" state variables in
+				% scope (e.g. external state variables
+				% visible from within a lambda body or
+				% condition of an if-then-else expression.)
+			dot		::	svar_map,
+			colon		::	svar_map
+				%
+				% The "read/write" state variables in scope.
+		).
+
+	% When collecting the arms of a disjunction we also need to
+	% collect the resulting svar_infos.
+	%
+:- type hlds_goal_svar_info == {hlds_goal, svar_info}.
+
+:- type hlds_goal_svar_infos == list(hlds_goal_svar_info).
+
+
+	% Create a new svar_info set up to start processing a clause head.
+	%
+:- func new_svar_info = svar_info.
+
+new_svar_info = svar_info(in_head, 0, map__init, map__init, map__init).
+
+%------------------------------------------------------------------------------%
+
+:- pred dot(prog_context, svar, prog_var,
+		prog_varset, prog_varset, svar_info, svar_info, io, io).
+:- mode dot(in, in, out, in, out, in, out, di, uo) is det.
+
+dot(Context, StateVar, Var, VarSet0, VarSet, SInfo0, SInfo, IO0, IO) :-
+
+	( if SInfo0 ^ ctxt = in_head then
+
+		( if SInfo0 ^ dot ^ elem(StateVar) = Var0 then
+			Var    = Var0,
+			VarSet = VarSet0,
+			SInfo  = SInfo0,
+			IO     = IO0
+		  else
+		  	new_dot_state_var(StateVar, Var,
+				VarSet0, VarSet, SInfo0, SInfo),
+			IO     = IO0
+		)
+
+	  else
+
+		( if SInfo0 ^ dot ^ elem(StateVar) = Var0 then
+			Var    = Var0,
+			VarSet = VarSet0,
+			SInfo  = SInfo0,
+			IO     = IO0
+		  else if SInfo0 ^ external_dot ^ elem(StateVar) = Var0 then
+			Var    = Var0,
+			VarSet = VarSet0,
+			SInfo  = SInfo0,
+			IO     = IO0
+		  else if SInfo0 ^ colon `contains` StateVar then
+		  	new_dot_state_var(StateVar, Var,
+				VarSet0, VarSet, SInfo0, SInfo),
+			prog_out__write_context(Context, IO0, IO1),
+		  	report_warning(string__format("\
+Warning: reference to unitialized state variable !.%s.\n",
+				[s(varset__lookup_name(VarSet, StateVar))]),
+				IO1, IO)
+		  else
+		  	Var    = StateVar,
+			VarSet = VarSet0,
+			SInfo  = SInfo0,
+			prog_out__write_context(Context, IO0, IO1),
+		  	report_warning(string__format("\
+Error: reference to !.%s, no such state variable in scope.\n",
+				[s(varset__lookup_name(VarSet, StateVar))]),
+				IO1, IO)
+		)
+	).
+
+%------------------------------------------------------------------------------%
+
+:- pred colon(prog_context, svar, prog_var,
+		prog_varset, prog_varset, svar_info, svar_info, io, io).
+:- mode colon(in, in, out, in, out, in, out, di, uo) is det.
+
+colon(Context, StateVar, Var, VarSet0, VarSet, SInfo0, SInfo, IO0, IO) :-
+
+	( if SInfo0 ^ ctxt = in_head then
+
+		( if SInfo0 ^ colon ^ elem(StateVar) = Var0 then
+			Var    = Var0,
+			VarSet = VarSet0,
+			SInfo  = SInfo0,
+			IO     = IO0
+		  else
+		  	new_final_state_var(StateVar, Var,
+				VarSet0, VarSet, SInfo0, SInfo),
+			IO     = IO0
+		)
+
+	  else
+
+		( if SInfo0 ^ colon ^ elem(StateVar) = Var0 then
+			Var    = Var0,
+			VarSet = VarSet0,
+			SInfo  = SInfo0 `with_updated_svar` StateVar,
+			IO     = IO0
+		  else
+		  	Var    = StateVar,
+			VarSet = VarSet0,
+			SInfo  = SInfo0,
+			Name   = varset__lookup_name(VarSet0, StateVar),
+			prog_out__write_context(Context, IO0, IO1),
+		  	report_warning(string__format("\
+Error: reference to !:%s, no such state variable in scope.\n", [s(Name)]),
+				IO1, IO2),
+			( if SInfo0 ^ external_dot `contains` StateVar then
+				prog_out__write_context(Context, IO2, IO3),
+				report_warning(string__format("\
+       (although state variable !.%s is in scope.)\n", [s(Name)]),
+       					IO3, IO)
+			  else
+			  	IO = IO2
+			)
+		)
+	).
+
+
+:- func svar_info `with_updated_svar` svar = svar_info.
+
+SInfo `with_updated_svar` StateVar =
+	( if   SInfo ^ ctxt =  in_atom(UpdatedStateVars, ParentSInfo)
+	  then SInfo ^ ctxt := in_atom(set__insert(UpdatedStateVars, StateVar),
+	                               ParentSInfo)
+	  else SInfo
+	).
+
+%------------------------------------------------------------------------------%
+
+	% Construct the initial and final mappings for a state variable.
+	%
+:- pred new_local_state_var(svar, prog_var, prog_var,
+		prog_varset, prog_varset, svar_info, svar_info).
+:- mode new_local_state_var(in, out, out, in, out, in, out) is det.
+
+new_local_state_var(StateVar, VarD, VarC, VarSet0, VarSet, SInfo0, SInfo) :-
+	new_dot_state_var(StateVar, VarD, VarSet0, VarSet1, SInfo0, SInfo1),
+	new_final_state_var(StateVar, VarC, VarSet1, VarSet, SInfo1, SInfo).
+
+	% Construct the initial and final mappings for a state variable.
+	%
+:- pred new_dot_state_var(svar, prog_var,
+		prog_varset, prog_varset, svar_info, svar_info).
+:- mode new_dot_state_var(in, out, in, out, in, out) is det.
+
+new_dot_state_var(StateVar, VarD, VarSet0, VarSet, SInfo0, SInfo) :-
+	N     = SInfo0 ^ num,
+	Name  = varset__lookup_name(VarSet0, StateVar),
+	NameD = string__format("STATE_VARIABLE_%s_%d", [s(Name), i(N)]),
+	varset__new_named_var(VarSet0, NameD, VarD, VarSet),
+	SInfo = ( SInfo0 ^ dot   ^ elem(StateVar) := VarD ).
+
+:- pred new_final_state_var(svar, prog_var,
+		prog_varset, prog_varset, svar_info, svar_info).
+:- mode new_final_state_var(in, out, in, out, in, out) is det.
+
+new_final_state_var(StateVar, VarC, VarSet0, VarSet, SInfo0, SInfo) :-
+	Name  = varset__lookup_name(VarSet0, StateVar),
+	NameC = string__format("STATE_VARIABLE_%s",    [s(Name)]),
+	varset__new_named_var(VarSet0, NameC, VarC, VarSet),
+	SInfo = ( SInfo0 ^ colon ^ elem(StateVar) := VarC ).
+
+%------------------------------------------------------------------------------%
+
+	% This is called either for a top-level clause or for a lambda.
+	% In the latter case, we need to make the current !.Xs external
+	% ("read-only") and clear the !.Xs and !:Xs.
+	%
+	% While processing the head, any state variables therein are
+	% implicitly scoped over the body and have !. and !: mappings
+	% set up.
+	%
+:- pred prepare_for_head(svar_info, svar_info).
+:- mode prepare_for_head(in, out) is det.
+
+prepare_for_head(SInfo0, SInfo) :-
+	SInfo = ( new_svar_info ^ external_dot := SInfo0 ^ dot ).
+
+%------------------------------------------------------------------------------%
+
+	% Having processed the head of a clause, prepare for the first
+	% (source-level) atomic conjunct.  We return the final !:
+	% mappings identified while processing the head.
+	%
+:- pred prepare_for_body(svar_map, prog_varset, prog_varset,
+		svar_info, svar_info).
+:- mode prepare_for_body(out, in, out, in, out) is det.
+
+prepare_for_body(FinalMap, VarSet0, VarSet, SInfo0, SInfo) :-
+	FinalMap  = SInfo0 ^ colon,
+	N         = SInfo0 ^ num + 1,
+	StateVars = list__merge_and_remove_dups(map__keys(SInfo0 ^ colon),
+						map__keys(SInfo0 ^ dot)),
+	next_svar_mappings(N, StateVars, VarSet0, VarSet, Colon),
+	SInfo     = ((( SInfo0 ^ ctxt  := in_body )
+			       ^ num   := N       )
+			       ^ colon := Colon   ).
+
+%------------------------------------------------------------------------------%
+
+	% We have to conjoin the head and body and add unifiers to tie up all
+	% the final values of the state variables to the head variables.
+	%
+:- pred finish_head_and_body(prog_context, svar_map,
+		hlds_goal, hlds_goal, hlds_goal, svar_info).
+:- mode finish_head_and_body(in, in, in, in, out, in) is det.
+
+finish_head_and_body(Context, FinalSVarMap, Head, Body, Goal, SInfo) :-
+	goal_info_init(Context, GoalInfo),
+	goal_to_conj_list(Head, HeadGoals),
+	goal_to_conj_list(Body, BodyGoals),
+	Unifiers = svar_unifiers(Context, FinalSVarMap, SInfo ^ dot),
+	conj_list_to_goal(HeadGoals ++ BodyGoals ++ Unifiers, GoalInfo, Goal).
+
+
+:- func svar_unifiers(prog_context, svar_map, svar_map) = hlds_goals.
+
+svar_unifiers(Context, LHSMap, RHSMap) =
+	map__foldl(
+		func(StateVar, Var, Unifiers) =
+			  [ svar_unification(Context,
+			  	Var, RHSMap ^ det_elem(StateVar))
+			  | Unifiers ],
+		LHSMap,
+		[]
+	).
+
+%------------------------------------------------------------------------------%
+
+:- 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).
+
+%------------------------------------------------------------------------------%
+
+	% Add some local state variables.
+	%
+:- pred prepare_for_local_state_vars(svars, prog_varset, prog_varset,
+		svar_info, svar_info).
+:- mode prepare_for_local_state_vars(in, in, out, in, out) is det.
+
+prepare_for_local_state_vars(StateVars, VarSet0, VarSet, SInfo0, SInfo) :-
+	list__foldl2(add_new_local_state_var, StateVars,
+		VarSet0, VarSet, SInfo0, SInfo).
+
+
+:- pred add_new_local_state_var(svar, prog_varset, prog_varset,
+		svar_info, svar_info).
+:- mode add_new_local_state_var(in, in, out, in, out) is det.
+
+add_new_local_state_var(StateVar, VarSet0, VarSet, SInfo0, SInfo) :-
+	new_local_state_var(StateVar, _, _, VarSet0, VarSet, SInfo0, SInfo).
+
+%------------------------------------------------------------------------------%
+
+	% Remove some local state variables.
+	%
+:- pred finish_local_state_vars(svars, prog_vars, 
+		svar_info, svar_info, svar_info).
+:- mode finish_local_state_vars(in, out, in, in, out) is det.
+
+finish_local_state_vars(StateVars, Vars, SInfoBefore, SInfo0, SInfo) :-
+	Dots   = list__map(map__lookup(SInfo0 ^ dot),   StateVars),
+	Colons = list__map(map__lookup(SInfo0 ^ colon), StateVars),
+	Vars   = list__sort_and_remove_dups(Dots ++ Colons),
+	SInfo  = (( SInfo0 ^ dot   := del_locals(StateVars,
+							SInfoBefore ^ dot,
+							SInfo0 ^ dot) )
+	                   ^ colon := del_locals(StateVars,
+							SInfoBefore ^ colon,
+							SInfo0 ^ colon) ).
+
+
+:- func del_locals(svars, svar_map, svar_map) = svar_map.
+
+del_locals(StateVars, MapBefore, Map) =
+	list__foldl(
+		func(K, M) =
+			( if   MapBefore ^ elem(K) = V
+			  then M ^ elem(K) := V
+			  else map__delete(M, K)
+			),
+		StateVars,
+		Map
+	).
+
+%------------------------------------------------------------------------------%
+
+	% We have to add unifiers to the Then and Else clauses of an
+	% if-then-else to make sure all the state variables match up.
+	%
+	% We construct new mappings for the state variables and then
+	% add unifiers.
+	%
+:- pred finish_if_then_else(prog_context,
+		hlds_goal, hlds_goal, hlds_goal, hlds_goal,
+		prog_varset, prog_varset, svar_info, svar_info, svar_info).
+:- mode finish_if_then_else(in, in, out, in, out, in, out, in, in, out) is det.
+
+finish_if_then_else(Context, Then0, Then, Else0, Else, VarSet0, VarSet,
+		SInfoT, SInfoE, SInfo) :-
+	SInfo0       = SInfoT,
+	N            = int__max(SInfoT ^ num, SInfoE ^ num),
+	next_svar_info(N, VarSet0, VarSet, SInfo0, SInfo),
+
+	goal_info_init(Context, GoalInfo),
+
+	goal_to_conj_list(Then0, ThenGoals0),
+	ThenUnifiers = svar_unifiers(Context, SInfo ^ dot, SInfoT ^ dot),
+	conj_list_to_goal(ThenGoals0 ++ ThenUnifiers, GoalInfo, Then),
+
+	goal_to_conj_list(Else0, ElseGoals0),
+	ElseUnifiers = svar_unifiers(Context, SInfo ^ dot, SInfoE ^ dot),
+	conj_list_to_goal(ElseGoals0 ++ ElseUnifiers, GoalInfo, Else).
+
+%------------------------------------------------------------------------------%
+
+:- pred next_svar_info(int, prog_varset, prog_varset, svar_info, svar_info).
+:- mode next_svar_info(in, in, out, in, out) is det.
+
+next_svar_info(N, VarSet0, VarSet, SInfo0, SInfo) :-
+	StateVars = map__keys(SInfo0 ^ dot),
+	next_svar_mappings(N + 1, StateVars, VarSet0, VarSet1, Dot),
+	next_svar_mappings(N + 2, StateVars, VarSet1, VarSet,  Colon),
+	SInfo     = ((( SInfo0 ^ num   := N + 2 )
+			       ^ dot   := Dot   )
+			       ^ colon := Colon ).
+
+
+:- pred next_svar_mappings(int, svars, prog_varset, prog_varset, svar_map).
+:- mode next_svar_mappings(in, in, in, out, out) is det.
+
+next_svar_mappings(N, StateVars, VarSet0, VarSet, Map) :-
+	next_svar_mappings_2(N, StateVars, VarSet0, VarSet, map__init, Map).
+
+
+:- pred next_svar_mappings_2(int, svars, prog_varset, prog_varset,
+		svar_map, svar_map).
+:- mode next_svar_mappings_2(in, in, in, out, in, out) is det.
+
+next_svar_mappings_2(_, [], VarSet, VarSet, Map, Map).
+
+next_svar_mappings_2(N, [StateVar | StateVars], VarSet0, VarSet, Map0, Map) :-
+	next_svar_mapping(N, StateVar, _, VarSet0, VarSet1, Map0, Map1),
+	next_svar_mappings_2(N, StateVars, VarSet1, VarSet, Map1, Map).
+
+%------------------------------------------------------------------------------%
+
+	% We assume that a negation updates all state variables in scope,
+	% so we construct new mappings for the state variables and then
+	% add unifiers from their pre-negated goal mappings.
+	%
+:- pred finish_negation(prog_context, hlds_goal, hlds_goal,
+		prog_varset, prog_varset, svar_info, svar_info, svar_info).
+:- mode finish_negation(in, in, out, in, out, in, in, out) is det.
+
+finish_negation(Context, Goal0, Goal, VarSet0, VarSet,
+		SInfoBefore, SInfoNeg, SInfo) :-
+	SInfo0    = SInfoBefore,
+	N         = SInfoNeg ^ num,
+	next_svar_info(N, VarSet0, VarSet, SInfo0, SInfo),
+
+	goal_info_init(Context, GoalInfo),
+
+	goal_to_conj_list(Goal0, Goals0),
+	Unifiers  = svar_unifiers(Context, SInfo ^ dot, SInfo0 ^ dot),
+	conj_list_to_goal(Goals0 ++ Unifiers, GoalInfo, Goal).
+
+%------------------------------------------------------------------------------%
+
+	% We have to make sure that all arms of a disjunction produce the
+	% same state variable bindings.
+	%
+:- pred finish_disjunction(prog_context, hlds_goal_svar_infos, hlds_goals,
+		prog_varset, prog_varset, svar_info).
+:- mode finish_disjunction(in, in, out, in, out, out) is det.
+
+finish_disjunction(_, [], _, _, _, _) :-
+	error("make_hlds__finish_disjunction: empty disjunct list").
+
+finish_disjunction(Context, DisjSInfos, Disjs, VarSet0, VarSet, SInfo) :-
+	DisjSInfos = [{_, SInfo0} | _],
+	N = list__foldl(
+		func({_, SI}, N0) = int__max(SI ^ num, N0),
+		DisjSInfos,
+		SInfo0 ^ num
+	    ),
+	next_svar_info(N, VarSet0, VarSet, SInfo0, SInfo),
+
+	goal_info_init(Context, GoalInfo),
+
+	Disjs = list__map(
+			( func({G0, SI}) = G :-
+				goal_to_conj_list(G0, Gs0),
+				Us = svar_unifiers(Context,
+						SInfo ^ dot, SI ^ dot),
+				conj_list_to_goal(Gs0 ++ Us, GoalInfo, G)
+			),
+			DisjSInfos
+		).
+
+%------------------------------------------------------------------------------%
+
+	% We treat equivalence goals as if they were negations (they are
+	% in a negated context after all.)
+	%
+:- pred finish_equivalence(prog_context, hlds_goal, hlds_goal,
+		prog_varset, prog_varset, svar_info, svar_info, svar_info).
+:- mode finish_equivalence(in, in, out, in, out, in, in, out) is det.
+
+finish_equivalence(Context, Goal0, Goal, VarSet0, VarSet,
+		SInfoBefore, SInfoEqv, SInfo) :-
+	finish_negation(Context, Goal0, Goal, VarSet0, VarSet,
+		SInfoBefore, SInfoEqv, SInfo).
+
+%------------------------------------------------------------------------------%
+
+	% We prepare for a call by setting the ctxt to in_atom.  If we're
+	% already in an atom then we inherit the parent's set of "updated"
+	% state variables.
+	%
+:- pred prepare_for_call(svar_info, svar_info).
+:- mode prepare_for_call(in, out) is det.
+
+prepare_for_call(ParentSInfo, SInfo) :-
+	UpdatedStateVars =
+		( if   ParentSInfo ^ ctxt = in_atom(UpdatedStateVars0, _)
+		  then UpdatedStateVars0
+		  else set__init
+		),
+	SInfo = ( ParentSInfo ^ ctxt := in_atom(UpdatedStateVars,ParentSInfo) ).
+
+%------------------------------------------------------------------------------%
+
+	% When we finish a call, we're either still inside the
+	% atomic formula, in which case we simply propagate the set of
+	% "updated" state variables, or we've just emerged, in which case
+	% we need to set up the svar_info for the next conjunct.
+	%
+:- pred finish_call(prog_varset, prog_varset, svar_info, svar_info).
+:- mode finish_call(in, out, in, out) is det.
+
+finish_call(VarSet0, VarSet, SInfo0, SInfo) :-
+	( if SInfo0 ^ ctxt = in_atom(UpdatedStateVars, ParentSInfo) then
+		( if ParentSInfo ^ ctxt = in_atom(_, GrandParentSInfo) then
+			VarSet = VarSet0,
+			SInfo  = ( ParentSInfo ^ ctxt :=
+					in_atom(UpdatedStateVars,
+					        GrandParentSInfo) )
+		  else
+			prepare_for_next_conjunct(UpdatedStateVars,
+				VarSet0, VarSet, ParentSInfo, SInfo)
+		)
+	  else
+	  	error("make_hlds__finish_call: ctxt is not in_atom")
+	).
+
+%------------------------------------------------------------------------------%
+
+	% The condition of an if-then-else expression is a goal in which
+	% only !.X state variables are visible (although the goal may
+	% use local state variables introduced via an explicit quantifier.)
+	%
+:- pred prepare_for_if_then_else_expr_condition(svar_info, svar_info).
+:- mode prepare_for_if_then_else_expr_condition(in, out) is det.
+
+prepare_for_if_then_else_expr_condition(SInfo0, SInfo) :-
+	SInfo = ((( SInfo0 ^ ctxt  := in_body   )
+			   ^ dot   := map__init )
+			   ^ colon := map__init ).
+
+%------------------------------------------------------------------------------%
+
+:- pred finish_if_then_else_expr_condition(svar_info, svar_info, svar_info).
+:- mode finish_if_then_else_expr_condition(in, in, out) is det.
+
+finish_if_then_else_expr_condition(SInfoBefore, SInfo0, SInfo) :-
+	SInfo = ( SInfoBefore ^ num := SInfo0 ^ num ).
+
+%------------------------------------------------------------------------------%
+
+	% Having finished processing one source-level atomic conjunct, prepare
+	% for the next.  Note that if !:X was not seen in the conjunct we've
+	% just processed, then we can reuse the !.X and !:X mappings.
+	%
+	% 	p(!.X) where [!.X -> X0, !:X -> X1]
+	%
+	% can yield
+	%
+	% 	p(X0) and [!.X -> X0, !:X -> X2]
+	%
+	% but
+	%
+	% 	p(!.X, !:X) where [!.X -> X0, !:X -> X1]
+	%
+	% will yield
+	%
+	% 	p(X0, X1) and [!.X -> X1, !:X -> X2]
+	%
+:- pred prepare_for_next_conjunct(svar_set, prog_varset, prog_varset,
+		svar_info, svar_info).
+:- mode prepare_for_next_conjunct(in, in, out, in, out) is det.
+
+prepare_for_next_conjunct(UpdatedStateVars, VarSet0, VarSet, SInfo0, SInfo) :-
+	Dot0   = SInfo0 ^ dot,
+	Colon0 = SInfo0 ^ colon,
+	N      = SInfo0 ^ num + 1,
+	map__init(Nil),
+	map__foldl(next_dot_mapping(UpdatedStateVars, Dot0, Colon0), Colon0,
+			Nil, Dot),
+	map__foldl2(next_colon_mapping(UpdatedStateVars, Colon0, N), Colon0,
+			VarSet0, VarSet, Nil, Colon),
+	SInfo  = (((( SInfo0 ^ ctxt  := in_body )
+		             ^ num   := N       )
+			     ^ dot   := Dot     )
+			     ^ colon := Colon   ).
+
+
+	% If the state variable has been updated (i.e. there was a !:X
+	% reference) then the next !.X mapping will be the current !:X
+	% mapping.
+	% Otherwise, preserve the current !.X mapping, if any (there
+	% may be none if, for example, the head only references !:X
+	% and there have been no prior references to !:X in the body.)
+	%
+:- pred next_dot_mapping(svar_set, svar_map, svar_map, svar, prog_var,
+		svar_map, svar_map).
+:- mode next_dot_mapping(in, in, in, in, in, in, out) is det.
+
+next_dot_mapping(UpdatedStateVars, OldDot, OldColon, StateVar, _, Dot0, Dot) :-
+	( if      UpdatedStateVars `contains` StateVar
+	  then    Var = OldColon ^ det_elem(StateVar),
+	  	  Dot = ( Dot0 ^ elem(StateVar) := Var )
+	  else if Var = OldDot ^ elem(StateVar)
+	  then    Dot = ( Dot0 ^ elem(StateVar) := Var )
+	  else    Dot = Dot0
+	).
+
+
+	% If the state variable has been updated (i.e. there was a !:X
+	% reference) then create a new mapping for the next !:X.
+	% Otherwise, the next !:X mapping is the same as the current
+	% !.X mapping.
+	%
+:- pred next_colon_mapping(svar_set, svar_map, int, svar, prog_var,
+		prog_varset, prog_varset, svar_map, svar_map).
+:- mode next_colon_mapping(in, in, in, in, in, in, out, in, out) is det.
+
+next_colon_mapping(UpdatedStateVars, OldColon, N, StateVar, _,
+		VarSet0, VarSet, Colon0, Colon) :-
+	( if UpdatedStateVars `contains` StateVar then
+		next_svar_mapping(N, StateVar, _Var, VarSet0, VarSet,
+			Colon0, Colon)
+	  else
+	  	VarSet = VarSet0,
+		Colon  = ( Colon0 ^ elem(StateVar) :=
+					OldColon ^ det_elem(StateVar) )
+	).
+
+
+:- pred next_svar_mapping(int, svar, prog_var, prog_varset, prog_varset,
+		svar_map, svar_map).
+:- mode next_svar_mapping(in, in, out, in, out, in, out) is det.
+
+next_svar_mapping(N, StateVar, Var, VarSet0, VarSet, Map0, Map) :-
+	Name = string__format("STATE_VARIABLE_%s_%d",
+			[s(varset__lookup_name(VarSet0, StateVar)), i(N)]),
+	varset__new_named_var(VarSet0, Name, Var, VarSet),
+	Map  = ( Map0 ^ elem(StateVar) := Var ).
+
+%------------------------------------------------------------------------------%
+
+:- func expand_dot_colon_state_var_args(list(prog_term)) = list(prog_term).
+
+expand_dot_colon_state_var_args(Args0) =
+	list__foldr(expand_dot_colon_state_var, Args0, []).
+
+
+:- func expand_dot_colon_state_var(prog_term, list(prog_term)) =
+		list(prog_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
+	  	[ T | Ts ]
+	).
+
+%------------------------------------------------------------------------------%
 %------------------------------------------------------------------------------%
Index: compiler/mercury_compile.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_compile.m,v
retrieving revision 1.247
diff -u -r1.247 mercury_compile.m
--- compiler/mercury_compile.m	19 Apr 2002 12:14:06 -0000	1.247
+++ compiler/mercury_compile.m	27 Apr 2002 00:52:50 -0000
@@ -1838,8 +1838,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/mercury_to_mercury.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_to_mercury.m,v
retrieving revision 1.212
diff -u -r1.212 mercury_to_mercury.m
--- compiler/mercury_to_mercury.m	9 Apr 2002 09:00:25 -0000	1.212
+++ compiler/mercury_to_mercury.m	29 Apr 2002 03:23:33 -0000
@@ -2379,6 +2379,20 @@
 		io__write_string(")")
 	).
 
+mercury_output_goal_2(some_state_vars(Vars, Goal), VarSet, Indent) -->
+	( { Vars = [] } ->
+		mercury_output_goal(Goal, VarSet, Indent)
+	;
+		io__write_string("some ["),
+		mercury_output_state_vars(Vars, VarSet, no),
+		io__write_string("] ("),
+		{ Indent1 = Indent + 1 },
+		mercury_output_newline(Indent1),
+		mercury_output_goal(Goal, VarSet, Indent1),
+		mercury_output_newline(Indent),
+		io__write_string(")")
+	).
+
 mercury_output_goal_2(all(Vars, Goal), VarSet, Indent) -->
 	( { Vars = [] } ->
 		mercury_output_goal(Goal, VarSet, Indent)
@@ -2393,6 +2407,20 @@
 		io__write_string(")")
 	).
 
+mercury_output_goal_2(all_state_vars(Vars, Goal), VarSet, Indent) -->
+	( { Vars = [] } ->
+		mercury_output_goal(Goal, VarSet, Indent)
+	;
+		io__write_string("all ["),
+		mercury_output_state_vars(Vars, VarSet, no),
+		io__write_string("] ("),
+		{ Indent1 = Indent + 1 },
+		mercury_output_newline(Indent1),
+		mercury_output_goal(Goal, VarSet, Indent1),
+		mercury_output_newline(Indent),
+		io__write_string(")")
+	).
+
 mercury_output_goal_2(if_then_else(Vars, A, B, C), VarSet, Indent) -->
 	io__write_string("(if"),
 	mercury_output_some(Vars, VarSet),
@@ -3267,6 +3295,23 @@
 	add_string(", "),
 	mercury_format_term(Term, VarSet, AppendVarnums),
 	mercury_format_remaining_terms(Terms, VarSet, AppendVarnums).
+
+	% Similar to mercury_output_vars//3, but prefixes each variable
+	% with `!' to indicate that it is a state variable.
+	%
+:- pred mercury_output_state_vars(list(var(T)), varset(T), bool, io, io).
+:- mode mercury_output_state_vars(in, in, in, di, uo) is det.
+
+mercury_output_state_vars(StateVars, VarSet, AppendVarnums) -->
+	io__write_list(StateVars, ", ",
+		mercury_output_state_var(VarSet, AppendVarnums)).
+
+:- pred mercury_output_state_var(varset(T), bool, var(T), io, io).
+:- mode mercury_output_state_var(in, in, in, di, uo) is det.
+
+mercury_output_state_var(VarSet, AppendVarnum, Var) -->
+	io__write_string("!"),
+	mercury_output_var(Var, VarSet, AppendVarnum).
 
 	% output a comma-separated list of variables
 
Index: compiler/module_qual.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/module_qual.m,v
retrieving revision 1.77
diff -u -r1.77 module_qual.m
--- compiler/module_qual.m	20 Mar 2002 12:36:58 -0000	1.77
+++ compiler/module_qual.m	29 Apr 2002 03:23:57 -0000
@@ -400,7 +400,11 @@
 process_assert(fail - _, [], yes).
 process_assert(some(_, G) - _, Symbols, Success) :-
 	process_assert(G, Symbols, Success).
+process_assert(some_state_vars(_, G) - _, Symbols, Success) :-
+	process_assert(G, Symbols, Success).
 process_assert(all(_, G) - _, Symbols, Success) :-
+	process_assert(G, Symbols, Success).
+process_assert(all_state_vars(_, G) - _, Symbols, Success) :-
 	process_assert(G, Symbols, Success).
 process_assert(implies(GA, GB) - _, Symbols, Success) :-
 	process_assert(GA, SymbolsA, SuccessA),
Index: compiler/prog_data.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_data.m,v
retrieving revision 1.82
diff -u -r1.82 prog_data.m
--- compiler/prog_data.m	20 Mar 2002 12:37:10 -0000	1.82
+++ compiler/prog_data.m	29 Apr 2002 03:45:42 -0000
@@ -685,6 +685,10 @@
 				% existential quantification
 				% (The curly braces just quote the 'some'/2.)
 	;	all(prog_vars, goal)	% universal quantification
+	;	some_state_vars(prog_vars, goal)
+	;	all_state_vars(prog_vars, goal)
+				% state variables extracted from
+				% some/2 and all/2 quantifiers.
 
 	% implications
 	;	implies(goal, goal)	% A => B
Index: compiler/prog_io_goal.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io_goal.m,v
retrieving revision 1.22
diff -u -r1.22 prog_io_goal.m
--- compiler/prog_io_goal.m	20 Mar 2002 12:37:13 -0000	1.22
+++ compiler/prog_io_goal.m	29 Apr 2002 04:15:40 -0000
@@ -197,14 +197,36 @@
 	parse_some_vars_goal(A0, V0, Vars, A, V1),
 	parse_goal(B0, V1, B, V2),
 	parse_goal(C0, V2, C, V).
+
 parse_goal_2("not", [A0], V0, not(A), V) :-
 	parse_goal(A0, V0, A, V).
+
 parse_goal_2("\\+", [A0], V0, not(A), V) :-
 	parse_goal(A0, V0, A, V).
-parse_goal_2("all", [Vars0, A0], V0, all(Vars, A), V):-
-	term__coerce(Vars0, Vars1),
-	term__vars(Vars1, Vars),
-	parse_goal(A0, V0, A, V).
+
+parse_goal_2("all", [QVars, A0], V0, GoalExpr, V):-
+
+		% Extract any state variables in the quantifier.
+		%
+	parse_quantifier_vars(QVars, StateVars0, Vars0),
+	list__map(term__coerce_var, StateVars0, StateVars),
+	list__map(term__coerce_var, Vars0, Vars),
+
+	parse_goal(A0, V0, A @ (GoalExprA - ContextA), V),
+
+	(
+		Vars = [],    StateVars = [],
+		GoalExpr = GoalExprA
+	;
+		Vars = [],    StateVars = [_|_],
+		GoalExpr = all_state_vars(StateVars, A)
+	;
+		Vars = [_|_], StateVars = [],
+		GoalExpr = all(Vars, A)
+	;
+		Vars = [_|_], StateVars = [_|_],
+		GoalExpr = all(Vars, all_state_vars(StateVars, A) - ContextA)
+	).
 
 	% handle implication
 parse_goal_2("<=", [A0, B0], V0, implies(B, A), V):-
@@ -220,10 +242,29 @@
 	parse_goal(A0, V0, A, V1),
 	parse_goal(B0, V1, B, V).
 
-parse_goal_2("some", [Vars0, A0], V0, some(Vars, A), V):-
-	parse_list_of_vars(Vars0, Vars1),
-	list__map(term__coerce_var, Vars1, Vars),
-	parse_goal(A0, V0, A, V).
+parse_goal_2("some", [QVars, A0], V0, GoalExpr, V):-
+
+		% Extract any state variables in the quantifier.
+		%
+	parse_quantifier_vars(QVars, StateVars0, Vars0),
+	list__map(term__coerce_var, StateVars0, StateVars),
+	list__map(term__coerce_var, Vars0, Vars),
+
+	parse_goal(A0, V0, A @ (GoalExprA - ContextA), V),
+
+	(
+		Vars = [],    StateVars = [],
+		GoalExpr = GoalExprA
+	;
+		Vars = [],    StateVars = [_|_],
+		GoalExpr = some_state_vars(StateVars, A)
+	;
+		Vars = [_|_], StateVars = [],
+		GoalExpr = some(Vars, A)
+	;
+		Vars = [_|_], StateVars = [_|_],
+		GoalExpr = some(Vars, some_state_vars(StateVars, A) - ContextA)
+	).
 
 	% The following is a temporary hack to handle `is' in
 	% the parser - we ought to handle it in the code generation -
@@ -257,6 +298,25 @@
 		A = call(unqualified(PurityString), [A2], pure)
 	).
 
+
+	% Parse a list of quantified variables, splitting it into
+	% state variables and ordinary logic variables.
+	%
+:- pred parse_quantifier_vars(term(T), list(var(T)), list(var(T))).
+:- mode parse_quantifier_vars(in, out, out) is semidet.
+
+parse_quantifier_vars(functor(atom("[]"),  [],     _), [],  []).
+
+parse_quantifier_vars(functor(atom("[|]"), [H, T], _), SVs, Vs) :-
+	(
+		H   = functor(atom("!"), [variable(SV)], _),
+		SVs = [SV | SVs0],
+		parse_quantifier_vars(T, SVs0, Vs)
+	;
+		H   = variable(V),
+		Vs = [V | Vs0],
+		parse_quantifier_vars(T, SVs, Vs0)
+	).
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/prog_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_util.m,v
retrieving revision 1.56
diff -u -r1.56 prog_util.m
--- compiler/prog_util.m	20 Mar 2002 12:37:15 -0000	1.56
+++ compiler/prog_util.m	29 Apr 2002 03:24:40 -0000
@@ -316,8 +316,16 @@
 		some(Vars, Goal)) :-
 	prog_util__rename_in_vars(Vars0, OldVar, NewVar, Vars),
 	prog_util__rename_in_goal(Goal0, OldVar, NewVar, Goal).
+prog_util__rename_in_goal_expr(some_state_vars(Vars0, Goal0), OldVar, NewVar,
+		some_state_vars(Vars, Goal)) :-
+	prog_util__rename_in_vars(Vars0, OldVar, NewVar, Vars),
+	prog_util__rename_in_goal(Goal0, OldVar, NewVar, Goal).
 prog_util__rename_in_goal_expr(all(Vars0, Goal0), OldVar, NewVar,
 		all(Vars, Goal)) :-
+	prog_util__rename_in_vars(Vars0, OldVar, NewVar, Vars),
+	prog_util__rename_in_goal(Goal0, OldVar, NewVar, Goal).
+prog_util__rename_in_goal_expr(all_state_vars(Vars0, Goal0), OldVar, NewVar,
+		all_state_vars(Vars, Goal)) :-
 	prog_util__rename_in_vars(Vars0, OldVar, NewVar, Vars),
 	prog_util__rename_in_goal(Goal0, OldVar, NewVar, Goal).
 prog_util__rename_in_goal_expr(implies(GoalA0, GoalB0), OldVar, NewVar,
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	29 Apr 2002 04:45:07 -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,198 @@
 
 @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 free occurrences of @samp{!. at var{X}}
+replaced with @var{ThisX} and occurrences of @samp{!:@var{X}}
+replaced with @var{NextX} (a free occurrence is one not bound by the
+head of a clause or lambda or by explicit quantification.)
+
+State variables obey the special scope rules.
+A state variable @var{X} must be explicitly introduced either in the head of
+the clause or lambda (in which case it may appear as either or both of
+ at samp{!. at var{X}} or @samp{!:@var{X}}) or in an explicit quantification (in
+which case it must appear as @samp{!@var{X}}.)  A state variable @var{X} in
+the enclosing scope of a lambda or if-then-else expression may only be 
+referred to as @samp{!. at var{X}} (unless the enclosing @var{X} is masked
+by a more local state variable of the same name.)
+
+For instance, the following goal employing an if-then-else expression
+ at example
+	p((if q(!@var{X}), r(!@var{X}) then @var{A} else @var{B}), !@var{X})
+ at end example
+is illegal because it implicitly refers to @samp{!:@var{X}} in the condition
+of the if-then-else expression.  However
+ at example
+	p((if some[!@var{X}] (q(!@var{X}), r(!@var{X})) then @var{A} else @var{B}), !@var{X})
+ at end example
+is acceptable because the state variable @var{X} is locally scoped to the
+condition of the if-then-else expression, hence @samp{!:@var{X}} may appear
+therein.
+
+ 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.
+
+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: tests/general/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/general/Mmakefile,v
retrieving revision 1.39
diff -u -r1.39 Mmakefile
--- tests/general/Mmakefile	26 Feb 2002 02:52:33 -0000	1.39
+++ tests/general/Mmakefile	9 Apr 2002 02:00:00 -0000
@@ -61,6 +61,7 @@
 		read_line_as_string \
 		semidet_map \
 		set_test \
+		state_vars_tests \
 		string_format_test \
 		string_format_test_2 \
 		string_format_test_3 \
Index: tests/general/state_vars_tests.exp
===================================================================
RCS file: tests/general/state_vars_tests.exp
diff -N tests/general/state_vars_tests.exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/general/state_vars_tests.exp	9 Apr 2002 01:54:57 -0000
@@ -0,0 +1 @@
+[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27]
Index: tests/general/state_vars_tests.m
===================================================================
RCS file: tests/general/state_vars_tests.m
diff -N tests/general/state_vars_tests.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/general/state_vars_tests.m	2 May 2002 05:33:28 -0000
@@ -0,0 +1,233 @@
+%------------------------------------------------------------------------------%
+% state_vars_tests.m
+% Ralph Becket <rafe at cs.mu.oz.au>
+% Wed Apr  3 14:19:02 EST 2002
+% vim: ft=mercury ff=unix ts=4 sw=4 et wm=0 tw=0
+%
+%------------------------------------------------------------------------------%
+
+:- module foo.
+
+:- interface.
+
+:- import_module io.
+
+
+
+:- pred main(io::di, io::uo) is cc_multi.
+
+%------------------------------------------------------------------------------%
+%------------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module std_util, string, int, list.
+
+%------------------------------------------------------------------------------%
+
+main(!IO) :-
+    unsorted_solutions(test, S),
+    io__print(list__reverse(S) `with_type` list(int), !IO),
+    io__nl(!IO).
+
+%------------------------------------------------------------------------------%
+
+:- pred test(int::out) is multi.
+
+test(X) :-
+    add(1, 0, X).
+
+test(X) :-
+    some [!A] (
+        add(2, 0, !:A), X = !.A
+    ).
+
+test(X) :-
+    some [!A] (
+        !:A = 0, add(3, !A), X = !.A
+    ).
+
+test(X) :-
+    some [!A] (
+        !:A = 4, not fail, X = !.A
+    ).
+
+test(X) :-
+    some [!A] (
+        !:A = 5, not (add(1, !A), !.A = 5), X = !.A
+    ).
+
+test(X) :-
+    some [!A, !B] (
+        !:A = 1, !:B = 1, add(1, !A), add(2, !B), X = !.A * !.B
+    ).
+
+test(X) :-
+    some [!A] (
+        ( if true then !:A = 7 else !:A = -1 ), X = !.A
+    ).
+
+test(X) :-
+    some [!A] (
+        ( if fail then !:A = -1 else !:A = 8 ), X = !.A
+    ).
+
+test(X) :-
+    some [!A] (
+        !:A = 0, ( if t(!.A, _) then !:A = 9 else !:A = -1 ), X = !.A
+    ).
+
+test(X) :-
+    some [!A] (
+        !:A = 0, ( if f(!.A, _) then !:A = -1 else !:A = 10 ), X = !.A
+    ).
+
+test(X) :-
+    some [!A] (
+        !:A = 0,
+        ( if ( f(!A) ; t(!A) ), !.A = 1 then !:A = 11 else !:A = -1 ),
+        X   = !.A
+    ).
+
+test(X) :-
+    some [!A] (
+        !:A = 0,
+        ( if ( t(!A) ; f(!A) ), !.A = 1 then !:A = 12 else !:A = -1 ),
+        X   = !.A
+    ).
+
+test(X) :-
+    some [!A] (
+        !:A = 0,
+        ( add(13, !A) ; add(14, !A) ),
+        X   = !.A
+    ).
+
+test(X) :-
+    some [!A, !B] (
+        !:A = 1,
+        !:B = 1,
+        ( add(14, !A) ; add(15, !B) ),
+        X   = !.A * !.B
+    ).
+
+test(X) :-
+    some [!A] (
+        !:A = 0,
+        !:A = fn_a(17, !.A),
+        X   = !.A
+    ).
+
+test(X) :-
+    some [!A] (
+        !:A = 0,
+        !:A = fn_b(18, !.A),
+        X   = !.A
+    ).
+
+test(X) :-
+    some [!A] (
+        !:A = 0,
+        F   = ( func(!.B) = !:B :-
+                    !:B = !.B + 19 ),
+        !:A = F(!.A),
+        X   = !.A
+    ).
+
+test(X) :-
+    some [!A] (
+        !:A = 0,
+        F   = ( func(!.B) = !.B + 20 ),
+        !:A = F(!.A),
+        X   = !.A
+    ).
+
+test(X) :-
+    some [!A] (
+        !:A = 0,
+        F   = ( func(!.A) = !:A :-
+                    !:A = !.A + 21 ),
+        !:A = F(!.A),
+        X   = !.A
+    ).
+
+test(X) :-
+    some [!A] (
+        !:A = 0,
+        F   = ( func(!.A) = !.A + 22 ),
+        !:A = F(!.A),
+        X   = !.A
+    ).
+
+test(X) :-
+    some [!A] (
+        !:A = 0,
+        P   = ( pred(!.B :: in, !:B :: out) is det :- !:B = !.B + 23 ),
+        P(!A),
+        X   = !.A
+    ).
+
+test(X) :-
+    some [!A] (
+        !:A = 0,
+        P   = ( pred(!.B :: in, (!.B + 24) :: out) is det ),
+        P(!A),
+        X   = !.A
+    ).
+
+test(X) :-
+    some [!A] (
+        !:A = 0,
+        P   = ( pred(!.A :: in, !:A :: out) is det :- !:A = !.A + 25 ),
+        P(!A),
+        X   = !.A
+    ).
+
+test(X) :-
+    some [!A] (
+        !:A = 0,
+        P   = ( pred(!.A :: in, (!.A + 26) :: out) is det ),
+        P(!A),
+        X   = !.A
+    ).
+
+test(!:A * !:B) :-
+    !:A = 2,
+    add(1, !A),
+    !:B = 8,
+    add(1, !B).
+
+%------------------------------------------------------------------------------%
+
+:- pred add(int::in, int::in, int::out) is det.
+
+add(N, X, X + N).
+
+
+:- pred t(int::in, int::out) is semidet.
+
+t(!X) :-
+    !:X = !.X + 1,
+    semidet_succeed.
+
+
+:- pred f(int::in, int::out) is semidet.
+
+f(!X) :-
+    X0  = !.X,
+    !:X = !.X + 1,
+    !.X = X0.
+
+
+:- func fn_a(int, int) = int.
+
+fn_a(N, !.X) = !:X :-
+    !:X = !.X + N.
+
+
+:- func fn_b(int, int) = int.
+
+fn_b(N, !.X) = !.X + N.
+
+%------------------------------------------------------------------------------%
+%------------------------------------------------------------------------------%
--------------------------------------------------------------------------
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