[m-rev.] For review: State Variables

Ralph Becket rafe at cs.mu.OZ.AU
Fri Jun 7 17:40:23 AEST 2002


Pretty sure I've fixed things...


Index: make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.412
diff -u -r1.412 make_hlds.m
--- make_hlds.m	1 Jun 2002 13:34:34 -0000	1.412
+++ make_hlds.m	7 Jun 2002 07:39:12 -0000
@@ -16,6 +16,9 @@
 % super-homogenous form, and introduce implicit quantification.
 % 
 % XXX we should record each error using module_info_incr_errors.
+%
+% XXX For state variables, we should allow quantifiers around if-then-else
+% expressions.
 
 % WISHLIST - we should handle explicit module quantification
 
@@ -2773,11 +2776,12 @@
 		di, uo) is det.
 
 module_add_instance_defn(Module0, InstanceModuleName, Constraints, ClassName,
-		Types, Body, VarSet, Status, Context, Module) -->
+		Types, Body0, VarSet, Status, Context, Module) -->
 	{ module_info_classes(Module0, Classes) },
 	{ module_info_instances(Module0, Instances0) },
 	{ list__length(Types, ClassArity) },
 	{ ClassId = class_id(ClassName, ClassArity) },
+	{ Body = expand_bang_state_var_args_in_instance_method_heads(Body0) },
 	(
 		{ map__search(Classes, ClassId, _) }
 	->
@@ -3710,15 +3714,26 @@
 :- 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) -->
+
+	{ IllegalSVarResult =
+		( if   illegal_state_var_func_result(PredOrFunc, Args0, SVar)
+		  then yes(SVar)
+		  else no
+		) },
+	{ ArityAdjustment = ( if IllegalSVarResult = yes(_) then -1 else 0 ) },
+
+	{ Args = expand_bang_state_var_args(Args0) },
+
 	globals__io_lookup_bool_option(very_verbose, VeryVerbose),
 	( { VeryVerbose = yes } ->
 		io__write_string("% Processing clause for "),
 		hlds_out__write_pred_or_func(PredOrFunc),
 		io__write_string(" `"),
-		{ list__length(Args, PredArity) },
+		{ list__length(Args, PredArity0) },
+		{ PredArity = PredArity0 + ArityAdjustment },
 		{ adjust_func_arity(PredOrFunc, OrigArity, PredArity) },
 		prog_out__write_sym_name_and_arity(PredName/OrigArity),
 		io__write_string("'...\n")
@@ -3730,7 +3745,8 @@
 		% (If it's not there, call maybe_undefined_pred_error
 		% and insert an implicit declaration for the predicate.)
 	{ module_info_name(ModuleInfo0, ModuleName) },
-	{ list__length(Args, Arity) },
+	{ list__length(Args, Arity0) },
+	{ Arity = Arity0 + ArityAdjustment },
 	{ module_info_get_predicate_table(ModuleInfo0, PredicateTable0) },
 	(
 		{ predicate_table_search_pf_sym_arity(PredicateTable0,
@@ -3787,6 +3803,13 @@
 		PredInfo1 = PredInfo0
 	},
 	(
+		{ IllegalSVarResult = yes(StateVar) }
+	->
+		report_illegal_func_svar_result(Context, ClauseVarSet,
+			StateVar),
+		{ ModuleInfo = ModuleInfo1 },
+		{ Info       = Info0 }
+	;
 		%
 		% User-supplied clauses for field access functions are
 		% not allowed -- the clauses are always generated by the
@@ -4116,31 +4139,43 @@
 		ModuleInfo - QualInfo - ClausesInfo) -->
 	(
 		{ InstanceClause = clause(CVarSet, PredOrFunc, PredName,
-				HeadTerms, Body) }
+				HeadTerms0, Body) }
 	->
-		{ PredArity = list__length(HeadTerms) },
-		{ adjust_func_arity(PredOrFunc, Arity, PredArity) },
-		% The tvarset argument is only used for explicit type
-		% qualifications, of which there are none in this clause,
-		% so it is set to a dummy value.
-		{ varset__init(TVarSet0) },
-
-		{ ProcIds = [] }, % means this clause applies to _every_
-				  % mode of the procedure
-		{ GoalType = none },	% goal is not a promise
-		clauses_info_add_clause(ClausesInfo0, ProcIds,
-			CVarSet, TVarSet0, HeadTerms, Body, Context, Status,
-			PredOrFunc, Arity, GoalType, Goal,
-			VarSet, _TVarSet, ClausesInfo, Warnings,
-			ModuleInfo0, ModuleInfo, QualInfo0, QualInfo),
-
-		% warn about singleton variables 
-		maybe_warn_singletons(VarSet,
-			PredOrFunc - PredName/Arity, ModuleInfo, Goal),
-
-		% warn about variables with overlapping scopes
-		maybe_warn_overlap(Warnings, VarSet,
-			PredOrFunc - PredName/Arity)
+		(
+			{ illegal_state_var_func_result(PredOrFunc, HeadTerms0,
+				StateVar) }
+		->
+			report_illegal_func_svar_result(Context, CVarSet,
+				StateVar),
+			{ ModuleInfo  = ModuleInfo0 },
+			{ QualInfo    = QualInfo0 },
+			{ ClausesInfo = ClausesInfo0 }
+		;
+			{ HeadTerms = expand_bang_state_var_args(HeadTerms0) },
+			{ PredArity = list__length(HeadTerms) },
+			{ adjust_func_arity(PredOrFunc, Arity, PredArity) },
+			% The tvarset argument is only used for explicit type
+			% qualifications, of which there are none in this clause,
+			% so it is set to a dummy value.
+			{ varset__init(TVarSet0) },
+
+			{ ProcIds = [] }, % means this clause applies to _every_
+					  % mode of the procedure
+			{ GoalType = none },	% goal is not a promise
+			clauses_info_add_clause(ClausesInfo0, ProcIds,
+				CVarSet, TVarSet0, HeadTerms, Body, Context,
+				Status, PredOrFunc, Arity, GoalType, Goal,
+				VarSet, _TVarSet, ClausesInfo, Warnings,
+				ModuleInfo0, ModuleInfo, QualInfo0, QualInfo),
+
+			% warn about singleton variables 
+			maybe_warn_singletons(VarSet,
+				PredOrFunc - PredName/Arity, ModuleInfo, Goal),
+
+			% warn about variables with overlapping scopes
+			maybe_warn_overlap(Warnings, VarSet,
+				PredOrFunc - PredName/Arity)
+		)
 	;
 		{ error("produce_clause: invalid instance item") }
 	).
@@ -5500,7 +5535,7 @@
 clauses_info_add_pragma_foreign_proc(ClausesInfo0, Purity, Attributes0, PredId,
 		ProcId, PVarSet, PVars, OrigArgTypes, PragmaImpl0, Context,
 		PredOrFunc, PredName, Arity, ClausesInfo, ModuleInfo0,
-		ModuleInfo, Info, Info) -->
+		ModuleInfo, Info0, Info) -->
 
 	{ ClausesInfo0 = clauses_info(VarSet0, VarTypes, TVarNameMap,
 		VarTypes1, HeadVars, ClauseList, TI_VarMap, TCI_VarMap,
@@ -5618,6 +5653,7 @@
 	( { MultipleArgs = [_ | _] } ->
 		{ ClausesInfo = ClausesInfo0 },
 		{ ModuleInfo = ModuleInfo1 },
+		{ Info = Info0 },
 		prog_out__write_context(Context),
 		io__write_string(
 			"In `:- pragma foreign_proc' declaration for "),
@@ -5651,12 +5687,12 @@
 		% this foreign code is inlined
 		add_goal_info_purity_feature(GoalInfo1, Purity, GoalInfo),
 		HldsGoal0 = foreign_proc(Attributes, PredId, 
-			ProcId, HeadVars, ArgInfo, OrigArgTypes, PragmaImpl)
+			ProcId, Args, ArgInfo, OrigArgTypes, PragmaImpl)
 			- GoalInfo,
 		ModuleInfo = ModuleInfo1,
 		map__init(EmptyVarTypes),
 		implicitly_quantify_clause_body(HeadVars,
-			HldsGoal0, VarSet0, EmptyVarTypes,
+			HldsGoal1, VarSet2, EmptyVarTypes,
 			HldsGoal, VarSet, _, _Warnings),
 		NewClause = clause([ProcId], HldsGoal,
 			foreign_language(NewLang), Context),
@@ -5689,33 +5725,49 @@
 :- 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,
-		io__state, io__state).
+		transform_info, transform_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.
 
-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,
+		IO0, IO) :-
+
+	prepare_for_head(SInfo0),
+
+	term__apply_substitution_to_list(Args0, Subst, Args1),
+
+	substitute_state_var_mappings(Args1, Args, VarSet0, VarSet1,
+		SInfo0, SInfo1, IO0, IO1),
+
+	hlds_goal__true_goal(Head0),
+
+	( if GoalType = promise(_) then
+		VarSet2 = VarSet1,
+		Head    = Head0,
+		Info1   = Info0,
+		SInfo2  = SInfo1,
+		IO2     = IO1
+	  else
+		ArgContext = head(PredOrFunc, Arity),
 		insert_arg_unifications(HeadVars, Args, Context, ArgContext,
-			Goal1, VarSet1, Goal2, VarSet2, Info1, Info2)
+			no, Head0, VarSet1, Head, VarSet2, Info0, Info1,
+			SInfo1, SInfo2, IO1, IO2)
 	),
-	{ 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, VarSet2, VarSet3, SInfo2, SInfo3),
+
+	transform_goal(Body0, VarSet3, Subst, Body, VarSet4, Info1, Info2,
+		SInfo3, SInfo, IO2, IO),
+
+	finish_head_and_body(Context, FinalSVarMap, Head, Body, Goal0,
+		SInfo),
+
+	VarTypes2 = Info2 ^ qual_info ^ vartypes,
+	implicitly_quantify_clause_body(HeadVars, Goal0, VarSet4, VarTypes2,
+		Goal, VarSet, VarTypes, Warnings),
+
+	Info = Info2 ^ qual_info ^ vartypes := VarTypes.
 
 %-----------------------------------------------------------------------------%
 
@@ -5729,89 +5781,132 @@
 
 :- 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) -->
-	{ goal_info_init(GoalInfo) }.
+transform_goal_2(fail, _, VarSet0, _, disj([]) - GoalInfo, VarSet,
+		Info, Info, SInfo0, SInfo) -->
+	{ goal_info_init(GoalInfo) },
+	{ prepare_for_next_conjunct(set__init, VarSet0, VarSet,
+		SInfo0, SInfo) }.
 
-transform_goal_2(true, _, VarSet, _, conj([]) - GoalInfo, VarSet,
-		Info, Info) -->
-	{ goal_info_init(GoalInfo) }.
+transform_goal_2(true, _, VarSet0, _, conj([]) - GoalInfo, VarSet,
+		Info, Info, SInfo0, SInfo) -->
+	{ goal_info_init(GoalInfo) },
+	{ prepare_for_next_conjunct(set__init, VarSet0, VarSet,
+		SInfo0, SInfo) }.
 
 	% 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, SInfoA),
+	transform_goal(B0, VarSet1, Subst, B1, VarSet2, Info1, Info2,
+		SInfoA, SInfoB),
+	transform_goal(C0, VarSet2, Subst, C1, VarSet3, Info2, Info,
+		SInfo0, SInfoC),
+	{ goal_info_init(GoalInfo) },
+	{ finish_if_then_else(Context, GoalInfo, B1, B, C1, C,
+		SInfo0, SInfoA, SInfoB, SInfoC, SInfo, VarSet3, VarSet) }.
 
 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), _, VarSet0, Subst, Goal, VarSet, Info0, Info,
+		SInfo0, SInfo) -->
+	transform_goal(A0, VarSet0, Subst, A, VarSet, Info0, Info,
+		SInfo0, SInfo1),
 	{ goal_info_init(GoalInfo) },
-	{ Goal = not(A) - GoalInfo }.
+	{ Goal = not(A) - GoalInfo },
+	{ finish_negation(SInfo0, SInfo1, SInfo) }.
 
-transform_goal_2((A0,B0), _, VarSet0, Subst, Goal, VarSet, Info0, Info) -->
-	get_conj(B0, Subst, [], VarSet0, L0, VarSet1, Info0, Info1),
-	get_conj(A0, Subst, L0, VarSet1, L, VarSet, Info1, Info),
+transform_goal_2((A0, B0), _, VarSet0, Subst, Goal, VarSet, Info0, Info,
+		SInfo0, SInfo) -->
+	get_rev_conj(A0, Subst, [], VarSet0, R0, VarSet1, Info0, Info1,
+		SInfo0, SInfo1),
+	get_rev_conj(B0, Subst, R0, VarSet1, R,  VarSet, Info1, Info,
+		SInfo1, SInfo),
+	{ L = list__reverse(R) },
 	{ 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_rev_par_conj(B0, Subst, [], VarSet0, R0, VarSet1, Info0, Info1,
+		SInfo0, SInfo1),
+	get_rev_par_conj(A0, Subst, R0, VarSet1, R,  VarSet, Info1, Info,
+		SInfo1, SInfo),
+	{ L = list__reverse(R) },
 	{ 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),
-	{ goal_info_init(GoalInfo) },
+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, VarSet,  Info1, Info, SInfo0),
+	{ finish_disjunction(Context, VarSet, L1, L, SInfo) },
+	{ goal_info_init(Context, GoalInfo) },
 	{ disj_list_to_goal(L, GoalInfo, Goal) }.
 
 transform_goal_2(implies(P, Q), Context, 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), _, 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
@@ -5820,19 +5915,25 @@
 	% 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, VarSet,  Info1, Info,
+		SInfo1, SInfo2),
+	{ Goal = shorthand(bi_implication(P, Q)) - GoalInfo },
+	{ finish_equivalence(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_bang_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
@@ -5842,9 +5943,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 },
@@ -5860,11 +5961,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) },
 		(
@@ -5921,28 +6022,63 @@
 		{ record_called_pred_or_func(predicate, Name, Arity,
 			Info0, Info1) },
 		insert_arg_unifications(HeadVars, Args,
-			Context, call(CallId),
-			Goal0, VarSet1, Goal, VarSet, Info1, Info)
-	).
+			Context, call(CallId), no,
+			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) -->
-	{ term__apply_substitution(A0, Subst, A) },
-	{ term__apply_substitution(B0, Subst, B) },
-	unravel_unification(A, B, Context, explicit, [],
-			VarSet0, Purity, Goal, VarSet, Info0, Info).
-	
+		Info0, Info, SInfo0, SInfo) -->
+	% It is an error for the left or right hand side of a
+	% unification to be !X (it may be !.X or !:X, however).
+	%
+	( if { A0 = functor(atom("!"), [variable(StateVarA)], _) } then
+		report_svar_unify_error(Context, VarSet0, StateVarA),
+		{ true_goal(Goal) },
+		{ VarSet = VarSet0 },
+		{ Info   = Info0   },
+		{ SInfo  = SInfo0  }
+	  else if { B0 = functor(atom("!"), [variable(StateVarB)], _) } then
+		report_svar_unify_error(Context, VarSet0, StateVarB),
+		{ true_goal(Goal) },
+		{ VarSet = VarSet0 },
+		{ Info   = Info0   },
+		{ SInfo  = SInfo0  }
+	  else
+		{ 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, VarSet1, Info0, Info,
+			SInfo1, SInfo2),
+		{ finish_call(VarSet1, VarSet, SInfo2, SInfo) }
+	).
+
+
+:- pred report_svar_unify_error(prog_context, prog_varset, svar, io, io).
+:- mode report_svar_unify_error(in, in, in, di, uo) is det.
+
+report_svar_unify_error(Context, VarSet, StateVar) -->
+		{ Name = varset__lookup_name(VarSet, StateVar) },
+		prog_out__write_context(Context),
+		report_warning(string__format("\
+Error: !%s cannot appear as a unification argument.\n", [s(Name)])),
+		prog_out__write_context(Context),
+		report_warning(string__format("\
+       You probably meant !.%s or !:%s.\n", [s(Name), s(Name)])).
+
 
 :- 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,
@@ -5968,8 +6104,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,
@@ -5993,7 +6129,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,
@@ -6008,18 +6145,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] ->
 		(
@@ -6028,7 +6167,7 @@
 				FieldNames, FieldValueVar, TermInputVar,
 				TermOutputVar, VarSet1, VarSet2, Functor,
 				InnermostFunctor - InnermostSubContext, Goal0,
-				Info0, Info1, IO0, IO1),
+				Info0, Info1, SInfo0, SInfo1, IO0, IO1),
 
 
 			FieldArgNumber = 2,
@@ -6054,15 +6193,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, []),
 
@@ -6086,8 +6226,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")
@@ -6108,18 +6249,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) }.
 
@@ -6128,17 +6270,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) },
@@ -6163,7 +6307,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) }
@@ -6175,14 +6319,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
@@ -6201,14 +6346,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,
@@ -6218,7 +6364,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) }.
@@ -6237,16 +6383,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) }.
 
@@ -6254,17 +6401,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 = [_|_] } ->
@@ -6280,7 +6429,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 },
@@ -6288,13 +6437,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,
@@ -6371,12 +6521,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
@@ -6384,7 +6535,7 @@
 	->
 		transform_aditi_tuple_insert_delete(UpdateStr, InsertDelete,
 			Args0, Context, VarSet0, Goal,
-			VarSet, Info0, Info)
+			VarSet, Info0, Info, SInfo0, SInfo)
 	;
 		{
 			UpdateStr = "aditi_insert",
@@ -6414,19 +6565,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) },
 
@@ -6477,8 +6629,9 @@
 			{ record_called_pred_or_func(PredOrFunc, SymName, 
 				InsertArity, Info0, Info1) },
 			insert_arg_unifications(AllArgs, AllArgTerms,
-				Context, call(CallId),
-				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) },
@@ -6491,7 +6644,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,
@@ -6500,19 +6654,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) },
@@ -6524,7 +6679,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 -
@@ -6577,12 +6733,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, PredGoal0, VarSet3, PredGoal1, VarSet4,
-			Info1, Info2),
-
+			ArgContext, no, PredGoal0, VarSet3, PredGoal1, VarSet4,
+			Info1, Info2, SInfo1, SInfo2), 
 		% Quantification will reduce this down to
 		% the proper set of nonlocal arguments.
 		{ goal_util__goal_vars(PredGoal, LambdaGoalVars0) }, 
@@ -6652,8 +6807,8 @@
 		insert_arg_unifications(AllArgs,
 			[term__variable(LambdaVar), AditiState0Term,
 				AditiStateTerm],
-			Context, CallId, UpdateConj, VarSet7, UpdateGoal,
-			VarSet, Info4, Info)
+			Context, CallId, no, UpdateConj,
+			VarSet7, UpdateGoal, VarSet, Info4, Info, SInfo2, SInfo)
 	;
 		%
 		% Second syntax -
@@ -6693,7 +6848,8 @@
 		{ record_called_pred_or_func(PredOrFunc, SymName, Arity,
 			Info0, Info1) },
 		insert_arg_unifications(OtherArgs, OtherArgs0, Context, CallId,
-			Call, VarSet1, UpdateGoal, VarSet, Info1, Info)
+			no, Call, VarSet1, UpdateGoal,
+			VarSet, Info1, Info, SInfo0, SInfo)
 	;
 		{ invalid_goal(Descr, Args0, GoalInfo,
 			UpdateGoal, VarSet0, VarSet) },
@@ -6701,7 +6857,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,
@@ -6901,7 +7058,17 @@
 	% that each unification gets reduced to superhomogeneous form.
 	% It also gets passed a `arg_context', which indicates
 	% where the terms came from.
+
 	% We never insert unifications of the form X = X.
+	% If ForPragmaC is yes, we process unifications of the form
+	% X = Y by substituting the var expected by the outside environment
+	% (the head variable) for the variable inside the goal (which was
+	% created just for the pragma_c_code goal), while giving the headvar
+	% the name of the just eliminated variable. The result will be
+	% a proc_info in which the head variables have meaningful names
+	% and the body goal is just a pragma C code. Without this special
+	% treatment, the body goal will be a conjunction, which would
+	% complicate the handling of code generation for nondet pragma C codes.
 
 :- type arg_context
 	--->	
@@ -6919,80 +7086,89 @@
 		).
 
 :- pred insert_arg_unifications(list(prog_var), list(prog_term),
-		prog_context, arg_context, hlds_goal, prog_varset,
+		prog_context, arg_context, bool, hlds_goal, prog_varset,
 		hlds_goal, prog_varset, transform_info, transform_info,
-		io__state, io__state).
-:- mode insert_arg_unifications(in, in, in, in, in, in, out,
-		out, in, out, di, uo) is det.
+		svar_info, svar_info, io__state, io__state).
+:- mode insert_arg_unifications(in, in, in, in, in, in, in, out,
+		out, in, out, in, out, di, uo) is det.
 
-insert_arg_unifications(HeadVars, Args, Context, ArgContext,
-		Goal0, VarSet0, Goal, VarSet, Info0, Info) -->
+insert_arg_unifications(HeadVars, Args0, Context, ArgContext, ForPragmaC,
+		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) },
+		substitute_state_var_mappings(Args0, Args, VarSet0, VarSet1,
+			SInfo0, SInfo1),
 		insert_arg_unifications_2(HeadVars, Args, Context, ArgContext,
-			0, List0, VarSet0, List, VarSet,
-			Info0, Info),
+			ForPragmaC, 0, List0, VarSet1, List, VarSet,
+			Info0, Info, SInfo1, SInfo),
 		{ goal_info_set_context(GoalInfo0, Context, GoalInfo) },
 		{ conj_list_to_goal(List, GoalInfo, Goal) }
 	).
 
 :- pred insert_arg_unifications_2(list(prog_var), list(prog_term),
-		prog_context, arg_context, int, list(hlds_goal),
+		prog_context, arg_context, bool, int, list(hlds_goal),
 		prog_varset, list(hlds_goal), prog_varset,
-		transform_info, transform_info, io__state, io__state).
-:- mode insert_arg_unifications_2(in, 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_2(in, in, in, in, in, in, in, in,
+		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) --> [].
+insert_arg_unifications_2([], [], _, _, _, _, List, VarSet, List, VarSet,
+		Info, Info, SInfo, SInfo) --> [].
 insert_arg_unifications_2([Var|Vars], [Arg|Args], Context, ArgContext,
-		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,
-		N1, List0, VarSet0, List1, VarSet1, ArgUnifyConj,
-		Info0, Info1),
+		ForPragmaC, N1, List0, VarSet0, List1, VarSet1, ArgUnifyConj,
+		Info0, Info1, SInfo0, SInfo1),
 	(
 		{ ArgUnifyConj = [] }
 	->
 		insert_arg_unifications_2(Vars, Args, Context, ArgContext,
-			N1, List1, VarSet1, List, VarSet,
-			Info1, Info)
+			ForPragmaC, N1, List1, VarSet1, List, VarSet,
+			Info1, Info, SInfo1, SInfo)
 	;
 		insert_arg_unifications_2(Vars, Args, Context, ArgContext,
-			N1, List1, VarSet1, List2, VarSet,
-			Info1, Info),
+			ForPragmaC, N1, List1, VarSet1, List2, VarSet,
+			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) -->
+		ArgTerms0, ArgContexts, Context, Goal0, VarSet0,
+		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) },
+		substitute_state_var_mappings(ArgTerms0, ArgTerms,
+			VarSet0, VarSet1, SInfo0, SInfo1),
 		insert_arg_unifications_with_supplied_contexts_2(ArgVars,
 			ArgTerms, ArgContexts, Context, GoalList0,
-			VarSet0, GoalList, VarSet, Info0, Info),
+			VarSet1, GoalList, VarSet, Info0, Info, SInfo1, SInfo),
 		{ goal_info_set_context(GoalInfo0, Context, GoalInfo) },
 		{ conj_list_to_goal(GoalList, GoalInfo, Goal) }
 	).
@@ -7000,44 +7176,48 @@
 :- 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] },
 		{ ArgContexts = [ArgNumber - ArgContext | ArgContexts1] }
 	->
-		insert_arg_unification(Var, Term, Context, ArgContext,
+		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") }
 	).
 
 :- pred insert_arg_unification(prog_var, prog_term,
-		prog_context, arg_context, int,
+		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).
-:- mode insert_arg_unification(in, in, in, in, in,
-		in, in, out, out, out, in, out, di, uo) is det.
-
-insert_arg_unification(Var, Arg, Context, ArgContext, N1,
-		List0, VarSet0, List1, VarSet1, ArgUnifyConj, Info0, Info) -->
+		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, in, out, di, uo) is det.
+
+insert_arg_unification(Var, Arg, Context, ArgContext, ForPragmaC, N1,
+		List0, VarSet0, List1, VarSet1, ArgUnifyConj,
+		Info0, Info, SInfo0, SInfo) -->
 	(
 		{ Arg = term__variable(Var) }
 	->
@@ -7045,13 +7225,32 @@
 		{ VarSet1 = VarSet0 },
 		{ Info = Info0 },
 		{ ArgUnifyConj = [] },
-		{ List1 = List0 }
+		{ List1 = List0 },
+		{ SInfo = SInfo0 }
+	;
+		{ Arg = term__variable(ArgVar) },
+		{ ForPragmaC = yes }
+	->
+		% Handle unifications of the form `X = Y' by substitution
+		% if this is safe.
+		{ Info = Info0 },
+		{ ArgUnifyConj = [] },
+		{ map__init(Subst0) },
+		{ map__det_insert(Subst0, ArgVar, Var, Subst) },
+		{ goal_util__rename_vars_in_goals(List0, no, Subst, List1) },
+		{ varset__search_name(VarSet0, ArgVar, ArgVarName) ->
+			varset__name_var(VarSet0, Var, ArgVarName, VarSet1)
+		;
+			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 }
 	).
@@ -7063,65 +7262,75 @@
 :- 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, Args0, 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) },
+		substitute_state_var_mappings(Args0, Args, VarSet0, VarSet1,
+			SInfo0, SInfo1),
 		append_arg_unifications_2(HeadVars, Args, Context, ArgContext,
-			0, List0, VarSet0, List, VarSet, Info0, Info),
+			0, List0, VarSet1, List, VarSet, Info0, Info,
+			SInfo1, 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) }
 	).
 
@@ -7194,15 +7403,32 @@
 :- 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.
+
+unravel_unification(LHS0, RHS0, Context, MainContext, SubContext,
+		VarSet0, Purity, Goal, VarSet, Info0, Info, SInfo0, SInfo) -->
+	substitute_state_var_mapping(LHS0, LHS,
+		VarSet0, VarSet1, SInfo0, SInfo1),
+	substitute_state_var_mapping(RHS0, RHS,
+		VarSet1, VarSet2, SInfo1, SInfo2),
+	unravel_unification_2(LHS, RHS, Context, MainContext, SubContext,
+		VarSet2, Purity, Goal, VarSet, Info0, Info, SInfo2, SInfo).
+
+
+:- pred unravel_unification_2(prog_term, prog_term, prog_context,
+		unify_main_context, unify_sub_contexts, prog_varset, 
+		purity, hlds_goal, prog_varset, transform_info, transform_info,
+		svar_info, svar_info, io__state, io__state).
+:- mode unravel_unification_2(in, in, in, in, in, in, in, out, out,
+		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)
-		-->
+unravel_unification_2(term__variable(X), term__variable(Y), Context,
+		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),
@@ -7217,22 +7443,25 @@
 	%	NewVar3 = A3.
 	% In the trivial case `X = c', no unravelling occurs.
 
-unravel_unification(term__variable(X), RHS,
-			Context, MainContext, SubContext, VarSet0, Purity,
-			Goal, VarSet, Info0, Info) -->
-	{ RHS = term__functor(F, Args, FunctorContext) },
+unravel_unification_2(term__variable(X), RHS,
+		Context, MainContext, SubContext, VarSet0, Purity,
+		Goal, VarSet, Info0, Info, SInfo0, SInfo) -->
+	{ RHS = term__functor(F, Args0, FunctorContext) },
+	{ Args1 = expand_bang_state_var_args(Args0) },
+	substitute_state_var_mappings(Args1, Args, VarSet0, VarSet1,
+		SInfo0, SInfo1),
 	(
 		% Handle explicit type qualification.
 		{ F = term__atom("with_type") },
 		{ Args = [RVal, DeclType0] }
 	->
 		{ convert_type(DeclType0, DeclType) },
-		{ varset__coerce(VarSet0, DeclVarSet) },
+		{ varset__coerce(VarSet1, DeclVarSet) },
 		process_type_qualification(X, DeclType, DeclVarSet,
 			Context, Info0, Info1),
 		unravel_unification(term__variable(X), RVal,
-			Context, MainContext, SubContext, VarSet0,
-			Purity, Goal, VarSet, Info1, Info)
+			Context, MainContext, SubContext, VarSet1,
+			Purity, Goal, VarSet, Info1, Info, SInfo1, SInfo)
 	;
 		% Handle unification expressions.
 		{ F = term__atom("@") },
@@ -7240,10 +7469,12 @@
 	->
 		unravel_unification(term__variable(X), LVal,
 			Context, MainContext, SubContext,
-			VarSet0, Purity, Goal1, VarSet1, Info0, Info1),
+			VarSet1, Purity, Goal1, VarSet2, Info0, Info1,
+			SInfo1, SInfo2),
 		unravel_unification(term__variable(X), RVal,
 			Context, MainContext, SubContext,
-			VarSet1, Purity, Goal2, VarSet, Info1, Info),
+			VarSet2, Purity, Goal2, VarSet, Info1, Info,
+			SInfo2, SInfo),
 		{ goal_info_init(GoalInfo) },
 		{ goal_to_conj_list(Goal1, ConjList1) },
 		{ goal_to_conj_list(Goal2, ConjList2) },
@@ -7287,11 +7518,12 @@
 			Context, Info1, Info2),
 		{ Det = Det1 },
 		{ term__coerce(GoalTerm1, GoalTerm) },
-		{ parse_goal(GoalTerm, VarSet0, ParsedGoal, VarSet1) },
+		{ parse_goal(GoalTerm, VarSet1, ParsedGoal, VarSet2) },
 		build_lambda_expression(X, PredOrFunc, EvalMethod, Vars1,
-			Modes, Det, ParsedGoal, VarSet1,
+			Modes, Det, ParsedGoal, VarSet2,
 			Context, MainContext, SubContext, Goal, VarSet,
-			Info2, Info)
+			Info2, Info, SInfo1),
+		{ SInfo = SInfo1 }
 	;
 	    {
 		% handle higher-order dcg pred expressions -
@@ -7308,14 +7540,15 @@
 		make_hlds__qualify_lambda_mode_list(Modes0, Modes,
 			Context, Info0, Info1),
 		{ term__coerce(GoalTerm0, GoalTerm) },
-		{ parse_dcg_pred_goal(GoalTerm, VarSet0,
-			ParsedGoal, DCG0, DCGn, VarSet1) },
+		{ parse_dcg_pred_goal(GoalTerm, VarSet1,
+			ParsedGoal, DCG0, DCGn, VarSet2) },
 		{ list__append(Vars0, [term__variable(DCG0),
 				term__variable(DCGn)], Vars1) },
 		build_lambda_expression(X, predicate, EvalMethod, Vars1,
-			Modes, Det, ParsedGoal, VarSet1,
+			Modes, Det, ParsedGoal, VarSet2,
 			Context, MainContext, SubContext, Goal0, VarSet,
-			Info1, Info),
+			Info1, Info, SInfo1),
+		{ SInfo = SInfo1 },
 		{ Goal0 = GoalExpr - GoalInfo0 },
 		{ add_goal_info_purity_feature(GoalInfo0, Purity, GoalInfo) },
 		{ Goal = GoalExpr - GoalInfo }
@@ -7333,19 +7566,21 @@
 			    ElseTerm]
 		},
 		{ term__coerce(IfTerm0, IfTerm) },
-		{ parse_some_vars_goal(IfTerm, VarSet0, Vars,
+		{ parse_some_vars_goal(IfTerm, VarSet1, Vars,
 			IfParseTree, VarSet11) }
 	->
+		{ prepare_for_if_then_else_expr_condition(SInfo1, SInfo2) },
 		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, SInfo2, SInfo3),
+		{ finish_if_then_else_expr_condition(SInfo1, SInfo3, SInfo4) },
 		unravel_unification(term__variable(X), ThenTerm,
 			Context, MainContext, SubContext, VarSet22, 
-			pure, ThenGoal, VarSet33, Info2, Info3),
+			pure, ThenGoal, VarSet33, Info2, Info3, SInfo4, SInfo5),
 		unravel_unification(term__variable(X), ElseTerm,
 			Context, MainContext, SubContext, VarSet33, pure,
-			ElseGoal, VarSet, Info3, Info),
+			ElseGoal, VarSet, Info3, Info, SInfo5, SInfo),
 		{ IfThenElse = if_then_else(Vars, IfGoal,
 			ThenGoal, ElseGoal) },
 		{ goal_info_init(Context, GoalInfo) },
@@ -7359,15 +7594,16 @@
 	->
 		check_expr_purity(Purity, Context, Info0, Info1),
 		{ make_fresh_arg_var(InputTerm, InputTermVar, [],
-			VarSet0, VarSet1) },
+			VarSet1, VarSet2) },
 		expand_get_field_function_call(Context, MainContext,
 			SubContext, FieldNames, X, InputTermVar,
-			VarSet1, VarSet2, Functor, _, Goal0, Info1, Info2),
+			VarSet2, VarSet3, Functor, _, Goal0, Info1, Info2,
+			SInfo1, SInfo2),
 
 		{ ArgContext = functor(Functor, MainContext, SubContext) },
 		append_arg_unifications([InputTermVar], [InputTerm],
 			FunctorContext, ArgContext, Goal0,
-			VarSet2, Goal, VarSet, Info2, Info)
+			VarSet3, Goal, VarSet, Info2, Info, SInfo2, SInfo)
 	;
 		% handle field update expressions
 		{ F = term__atom(":=") },
@@ -7379,27 +7615,30 @@
 	->
 		check_expr_purity(Purity, Context, Info0, Info1),
 		{ make_fresh_arg_var(InputTerm, InputTermVar, [],
-			VarSet0, VarSet1) },
+			VarSet1, VarSet2) },
 		{ make_fresh_arg_var(FieldValueTerm, FieldValueVar,
-			[InputTermVar], VarSet1, VarSet2) },
+			[InputTermVar], VarSet2, VarSet3) },
 
 		expand_set_field_function_call(Context, MainContext,
 			SubContext, FieldNames, FieldValueVar, InputTermVar, X,
-			VarSet2, VarSet3, Functor,
-			InnerFunctor - FieldSubContext, Goal0, Info1, Info2),
+			VarSet3, VarSet4, Functor,
+			InnerFunctor - FieldSubContext, Goal0, Info1, Info2,
+			SInfo1, SInfo2),
 
 		{ TermArgContext = functor(Functor, MainContext, SubContext) },
 		{ TermArgNumber = 1 },
 		append_arg_unification(InputTermVar, InputTerm,
 			FunctorContext, TermArgContext, TermArgNumber,
-			TermUnifyConj, VarSet3, VarSet4, Info2, Info3),
+			TermUnifyConj, VarSet4, VarSet5, Info2, Info3,
+			SInfo2, SInfo3),
 
 		{ FieldArgContext = functor(InnerFunctor,
 			MainContext, FieldSubContext) },
 		{ FieldArgNumber = 2 },
 		append_arg_unification(FieldValueVar, FieldValueTerm,
 			FunctorContext, FieldArgContext, FieldArgNumber,
-			FieldUnifyConj, VarSet4, VarSet, Info3, Info),
+			FieldUnifyConj, VarSet5, VarSet, Info3, Info,
+			SInfo3, SInfo),
 
 		{ Goal0 = _ - GoalInfo0 },
 		{ goal_to_conj_list(Goal0, GoalList0) },
@@ -7428,10 +7667,11 @@
 			{ add_goal_info_purity_feature(GoalInfo0, Purity,
 				GoalInfo) },
 			{ Goal = GoalExpr - GoalInfo },
-			{ VarSet = VarSet0 }
+			{ VarSet = VarSet1 },
+			{ SInfo = SInfo1 }
 		;
-			{ make_fresh_arg_vars(FunctorArgs, VarSet0,
-				HeadVars, VarSet1) },
+			{ make_fresh_arg_vars(FunctorArgs, VarSet1,
+				HeadVars, VarSet2) },
 			{ make_atomic_unification(X,
 				functor(ConsId, HeadVars), Context,
 				MainContext, SubContext, Goal0,
@@ -7447,15 +7687,17 @@
 			( { Purity = pure } ->
 				append_arg_unifications(HeadVars, FunctorArgs,
 					FunctorContext, ArgContext, Goal0,
-					VarSet1, Goal, VarSet, Info1, Info)
+					VarSet2, Goal, VarSet,
+					Info1, Info, SInfo1, SInfo)
 			;
 				{ Goal0 = GoalExpr - GoalInfo0 },
 				{ add_goal_info_purity_feature(GoalInfo0,
 					Purity, GoalInfo) },
 				{ Goal1 = GoalExpr - GoalInfo },
 				insert_arg_unifications(HeadVars, FunctorArgs,
-					FunctorContext, ArgContext, Goal1,
-					VarSet1, Goal, VarSet, Info1, Info)
+					FunctorContext, ArgContext, no, Goal1,
+					VarSet2, Goal, VarSet,
+					Info1, Info, SInfo1, SInfo)
 			)
 		)
 	).
@@ -7463,11 +7705,13 @@
 
 	% 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) -->
+unravel_unification_2(term__functor(F, As, FC), term__variable(Y),
+		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(...)',
@@ -7475,21 +7719,21 @@
 	% Note that we can't simplify it yet, because we might simplify
 	% away type errors.
 
-unravel_unification(term__functor(LeftF, LeftAs, LeftC),
-			term__functor(RightF, RightAs, RightC),
-			Context, MainContext, SubContext, VarSet0,
-			Purity, Goal, VarSet, Info0, Info) -->
+unravel_unification_2(term__functor(LeftF, LeftAs, LeftC),
+		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) },
@@ -7555,13 +7799,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,
+build_lambda_expression(X, PredOrFunc, EvalMethod, Args0, 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
@@ -7597,47 +7841,82 @@
 	% corresponding to the function result term is a new variable,
 	% to avoid the function result term becoming lambda-quantified.
 	%
-	{ list__length(Args, NumArgs) },
-	{ varset__new_vars(VarSet0, NumArgs, LambdaVars, VarSet1) },
-	{ map__init(Substitution) },
-	transform_goal(ParsedGoal, VarSet1, Substitution,
-			HLDS_Goal0, VarSet2, Info1, Info2),
-	{ ArgContext = head(PredOrFunc, NumArgs) },
-	insert_arg_unifications(LambdaVars, Args, Context, ArgContext,
-		HLDS_Goal0, VarSet2, HLDS_Goal1, VarSet, Info2, Info3),
-
-	%
-	% Now figure out which variables we need to explicitly existentially
-	% quantify.
-	%
-	{
-		PredOrFunc = predicate,
-		QuantifiedArgs = Args
+	(
+		{ illegal_state_var_func_result(PredOrFunc, Args0, StateVar) }
+	->
+		report_illegal_func_svar_result(Context, VarSet0, StateVar),
+		{ true_goal(Goal) },
+		{ VarSet = VarSet0 },
+		{ Info   = Info1 }
 	;
-		PredOrFunc = function,
-		pred_args_to_func_args(Args, QuantifiedArgs, _ReturnValTerm)
-	},
-	{ term__vars_list(QuantifiedArgs, QuantifiedVars0) },
-	{ list__sort_and_remove_dups(QuantifiedVars0, QuantifiedVars) },
+		{ lambda_args_contain_bang_state_var(Args0, StateVar) }
+	->
+		report_illegal_bang_svar_lambda_arg(Context, VarSet0, StateVar),
+		{ true_goal(Goal) },
+		{ VarSet = VarSet0 },
+		{ Info   = Info1 }
+	;
+		{ prepare_for_lambda(SInfo0, SInfo1) },
+		{ Args1  = expand_bang_state_var_args(Args0) },
+		substitute_state_var_mappings(Args1, Args, VarSet0, VarSet1,
+			SInfo1, SInfo2),
 
-	{ goal_info_init(Context, GoalInfo) },
-	{ HLDS_Goal = some(QuantifiedVars, can_remove, HLDS_Goal1)
-			- GoalInfo },
+		{ list__length(Args, NumArgs) },
+		{ varset__new_vars(VarSet1, NumArgs, LambdaVars, VarSet2) },
+		{ map__init(Substitution) },
+		{ hlds_goal__true_goal(Head0) },
+		{ ArgContext = head(PredOrFunc, NumArgs) },
 
-	%
-	% We set the lambda nonlocals here to anything that could possibly
-	% be nonlocal.  Quantification will reduce this down to
-	% the proper set of nonlocal arguments.
-	%
-	{ goal_util__goal_vars(HLDS_Goal, LambdaGoalVars0) }, 
-	{ set__delete_list(LambdaGoalVars0, LambdaVars, LambdaGoalVars1) },
-	{ set__delete_list(LambdaGoalVars1, QuantifiedVars, LambdaGoalVars2) },
-	{ set__to_sorted_list(LambdaGoalVars2, LambdaNonLocals) },
-
-	{ make_atomic_unification(X,
-		lambda_goal(PredOrFunc, EvalMethod, modes_are_ok,
-			LambdaNonLocals, LambdaVars, Modes, Det, HLDS_Goal),
-		Context, MainContext, SubContext, Goal, Info3, Info) }.
+		insert_arg_unifications(LambdaVars, Args, Context, ArgContext,
+			no, Head0, VarSet2, Head, VarSet3, Info1, Info2,
+			SInfo2, SInfo3),
+
+		{ prepare_for_body(FinalSVarMap, VarSet3, VarSet4,
+			SInfo3, SInfo4) },
+
+		transform_goal(ParsedGoal, VarSet4, Substitution,
+			Body, VarSet, Info2, Info3, SInfo4, SInfo5),
+
+		{ finish_head_and_body(Context, FinalSVarMap,
+			Head, Body, HLDS_Goal0, SInfo5) },
+
+		%
+		% Now figure out which variables we need to
+		% explicitly existentially quantify.
+		%
+		{
+			PredOrFunc = predicate,
+			QuantifiedArgs = Args
+		;
+			PredOrFunc = function,
+			pred_args_to_func_args(Args, QuantifiedArgs,
+				_ReturnValTerm)
+		},
+		{ term__vars_list(QuantifiedArgs, QuantifiedVars0) },
+		{ list__sort_and_remove_dups(QuantifiedVars0, QuantifiedVars) },
+
+		{ goal_info_init(Context, GoalInfo) },
+		{ HLDS_Goal = some(QuantifiedVars, can_remove, HLDS_Goal0) -
+					GoalInfo },
+
+		%
+		% We set the lambda nonlocals here to anything that
+		% could possibly be nonlocal.  Quantification will
+		% reduce this down to the proper set of nonlocal arguments.
+		%
+		{ goal_util__goal_vars(HLDS_Goal, LambdaGoalVars0) }, 
+		{ set__delete_list(LambdaGoalVars0, LambdaVars,
+			LambdaGoalVars1) },
+		{ set__delete_list(LambdaGoalVars1, QuantifiedVars,
+			LambdaGoalVars2) },
+		{ set__to_sorted_list(LambdaGoalVars2, LambdaNonLocals) },
+
+		{ make_atomic_unification(X,
+			lambda_goal(PredOrFunc, EvalMethod, modes_are_ok,
+				LambdaNonLocals, LambdaVars, Modes, Det,
+				HLDS_Goal),
+			Context, MainContext, SubContext, Goal, Info3, Info) }
+	).
 
 %-----------------------------------------------------------------------------%
 
@@ -7804,85 +8083,95 @@
 :- 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")
+	).
 
 %-----------------------------------------------------------------------------%
 
-% get_conj(Goal, Conj0, Subst, Conj) :
+% get_rev_conj(Goal, Conj0, Subst, Conj) :
 % 	Goal is a tree of conjuncts.  Flatten it into a list (applying Subst),
-%	append Conj0, and return the result in Conj.
+%	append Conj0, and return the result in reverse order in Conj.
 
-:- pred get_conj(goal, prog_substitution, list(hlds_goal), prog_varset,
+:- pred get_rev_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_rev_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_rev_conj(Goal, Subst, RevConj0, VarSet0, RevConj,
+		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_rev_conj(A, Subst, RevConj0, VarSet0, RevConj1,
+			VarSet1, Info0, Info1, SInfo0, SInfo1),
+		get_rev_conj(B, Subst, RevConj1, VarSet1, RevConj,
+			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) }
+		{ RevConj = list__reverse(ConjList) ++ RevConj0 }
 	).
 
-% get_par_conj(Goal, ParConj0, Subst, ParConj) :
+% get_rev_par_conj(Goal, ParConj0, Subst, ParConj) :
 % 	Goal is a tree of conjuncts.  Flatten it into a list (applying Subst),
-%	append ParConj0, and return the result in ParConj.
+%	append ParConj0, and return the result in reverse order in ParConj.
 
-:- pred get_par_conj(goal, prog_substitution, list(hlds_goal), prog_varset,
+:- pred get_rev_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_rev_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_rev_par_conj(Goal, Subst, RevParConj0, VarSet0, RevParConj,
+		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_rev_par_conj(A, Subst, RevParConj0, VarSet0, RevParConj1,
+			VarSet1, Info0, Info1, SInfo0, SInfo1),
+		get_rev_par_conj(B, Subst, RevParConj1, VarSet1, RevParConj,
+			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) }
+		{ RevParConj = list__reverse(ParConjList) ++ RevParConj0 }
 	).
 
 % get_disj(Goal, Subst, Disj0, Disj) :
 % 	Goal is a tree of disjuncts.  Flatten it into a list (applying Subst)
 %	append Disj0, and return the result in Disj.
 
-:- 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] }
 	).
 
 %-----------------------------------------------------------------------------%
@@ -8633,4 +8922,1028 @@
 :- 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).
+
+%------------------------------------------------------------------------------%
+
+	% Obtain the mapping for a !.X state variable reference and
+	% update the svar_info.
+	%
+	% If we are processing the head of a clause or lambda, we
+	% incrementally accumulate the mappings.
+	%
+	% Otherwise, the mapping must already be present for a local
+	% or `external' state variable (i.e. one that may be visible,
+	% but not updatable, in the current context.)
+	%
+	% Note that if !.X does not appear in the head then !:X must
+	% appear before !.X can be referenced.
+	%
+:- 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),
+			report_unitialized_state_var(Context, VarSet, StateVar,
+				IO0, IO)
+		  else
+		  	Var    = StateVar,
+			VarSet = VarSet0,
+			SInfo  = SInfo0,
+			report_non_visible_state_var(Context, VarSet, StateVar,
+				IO0, IO)
+		)
+	).
+
+%------------------------------------------------------------------------------%
+
+	% Obtain the mapping for a !:X state variable reference.
+	%
+	% If we are processing the head of a clause or lambda, we
+	% incrementally accumulate the mappings.
+	%
+	% Otherwise, the mapping must already be present for a local
+	% state variable (`externally' visible state variables cannot
+	% be updated.)
+	%
+	% We also keep track of which state variables have been updated
+	% in an atomic context.
+	%
+:- 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,
+			PError = ( if SInfo0 ^ external_dot `contains` StateVar
+				   then report_illegal_state_var_update
+				   else report_non_visible_state_var
+				 ),
+			PError(Context, VarSet, StateVar, IO0, IO)
+		)
+	).
+
+
+:- 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_colon_state_var(svar, prog_var,
+		prog_varset, prog_varset, svar_info, svar_info).
+:- mode new_colon_state_var(in, out, in, out, in, out) is det.
+
+new_colon_state_var(StateVar, VarC, VarSet0, VarSet, SInfo0, SInfo) :-
+	N     = SInfo0 ^ num,
+	Name  = varset__lookup_name(VarSet0, StateVar),
+	NameC = string__format("STATE_VARIABLE_%s_%d", [s(Name), i(N)]),
+	varset__new_named_var(VarSet0, NameC, VarC, VarSet),
+	SInfo = ( SInfo0 ^ colon ^ elem(StateVar) := VarC ).
+
+
+:- 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 ).
+
+%------------------------------------------------------------------------------%
+
+	% Prepare for the head of a new clause.
+	%
+:- pred prepare_for_head(svar_info).
+:- mode prepare_for_head(out) is det.
+
+prepare_for_head(new_svar_info).
+
+%------------------------------------------------------------------------------%
+
+	% 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_lambda(svar_info, svar_info).
+:- mode prepare_for_lambda(in, out) is det.
+
+prepare_for_lambda(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_colon_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 arms of an
+	% if-then-else to make sure all the state variables match up.
+	%
+	% More to the point, we have to add unifiers to the Then arm
+	% for any new state variable mappings produced in the condition.
+	%
+	% We construct new mappings for the state variables and then
+	% add unifiers.
+	%
+:- pred finish_if_then_else(prog_context, hlds_goal_info,
+		hlds_goal, hlds_goal, hlds_goal, hlds_goal,
+		svar_info, svar_info, svar_info, svar_info, svar_info,
+		prog_varset, prog_varset).
+:- mode finish_if_then_else(in, in, in, out, in, out, in, in, in, in, out,
+		in, out) is det.
+
+finish_if_then_else(Context, GoalInfo, Then0, Then, Else0, Else,
+		SInfo0, SInfoC, SInfoT0, SInfoE, SInfo,
+		VarSet0, VarSet) :-
+
+		% Add unifiers to the Then arm for state variables that
+		% acquired new mappings in the condition, but not in the
+		% Them arm itself.  This is because the new mappings
+		% appear only in a negated context.
+		%
+	StateVars  = list__merge_and_remove_dups(map__keys(SInfoT0 ^ dot),
+						 map__keys(SInfoE  ^ dot)),
+	goal_to_conj_list(Then0, Thens0),
+	add_then_arm_specific_unifiers(Context, StateVars,
+		SInfo0, SInfoC, SInfoT0, SInfoT,
+		Thens0, Thens, VarSet0, VarSet),
+	conj_list_to_goal(Thens, GoalInfo, Then1),
+
+		% Calculate the svar_info with the highest numbered
+		% mappings from each arm.
+		%
+	DisjSInfos = [{Then1, SInfoT}, {Else0, SInfoE}],
+	SInfo      = reconciled_disj_svar_info(VarSet, DisjSInfos),
+
+		% Add unifiers to each arm to ensure they both construct
+		% the same final state variable mappings. 
+		%
+	Then       = add_disj_unifiers(Context, GoalInfo, SInfo, StateVars,
+				{Then1, SInfoT}),
+	Else       = add_disj_unifiers(Context, GoalInfo, SInfo, StateVars,
+				{Else0, SInfoE}).
+
+
+	% If a new mapping was produced for state variable X in the
+	% condition-goal (i.e. the condition refers to !:X), but not
+	% in the then-goal, then we have to add a new unifier !:X = !.X
+	% to the then-goal because the new mapping was created in a
+	% negated context.
+	%
+:- pred add_then_arm_specific_unifiers(prog_context, svars,
+		svar_info, svar_info, svar_info, svar_info,
+		hlds_goals, hlds_goals, prog_varset, prog_varset).
+:- mode add_then_arm_specific_unifiers(in, in, in, in, in, out,
+		in, out, in, out) is det.
+
+add_then_arm_specific_unifiers(_, [],
+		_, _, SInfoT, SInfoT,
+		Thens, Thens, VarSet, VarSet).
+
+add_then_arm_specific_unifiers(Context, [StateVar | StateVars],
+		SInfo0, SInfoC, SInfoT0, SInfoT,
+		Thens0, Thens, VarSet0, VarSet) :-
+	( if /* the condition refers to !:X, but the then-goal doesn't */
+	     SInfoC  ^ dot ^ elem(StateVar) \= SInfo0 ^ dot ^ elem(StateVar),
+	     SInfoT0 ^ dot ^ elem(StateVar)  = SInfoC ^ dot ^ elem(StateVar)
+	  then
+	  	Dot0    = SInfoT0 ^ dot ^ det_elem(StateVar),
+		new_dot_state_var(StateVar, Dot, VarSet0, VarSet1,
+			SInfoT0, SInfoT1),
+		Thens1  = [svar_unification(Context, Dot, Dot0) | Thens0]
+	  else
+	  	SInfoT1 = SInfoT0,
+		Thens1  = Thens0,
+		VarSet1 = VarSet0
+	),
+	add_then_arm_specific_unifiers(Context, StateVars,
+		SInfo0, SInfoC, SInfoT1, SInfoT,
+		Thens1, Thens, VarSet1, VarSet).
+
+%------------------------------------------------------------------------------%
+
+:- 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(svar_info, svar_info, svar_info).
+:- mode finish_negation(in, in, out) is det.
+
+finish_negation(SInfoBefore, SInfoNeg, SInfo) :-
+	SInfo = (( SInfoBefore ^ num   := SInfoNeg ^ num   )
+	                       ^ colon := SInfoNeg ^ colon ).
+
+%------------------------------------------------------------------------------%
+
+	% We have to make sure that all arms of a disjunction produce the
+	% same state variable bindings by adding unifiers as necessary.
+	%
+:- pred finish_disjunction(prog_context, prog_varset, hlds_goal_svar_infos,
+		hlds_goals, svar_info).
+:- mode finish_disjunction(in, in, in, out, out) is det.
+
+finish_disjunction(Context, VarSet, DisjSInfos, Disjs, SInfo) :-
+	SInfo      = reconciled_disj_svar_info(VarSet, DisjSInfos),
+	StateVars  = map__keys(SInfo ^ dot),
+	goal_info_init(Context, GoalInfo),
+	Disjs      = list__map(
+			add_disj_unifiers(Context, GoalInfo, SInfo, StateVars),
+			DisjSInfos).
+
+
+	% Each arm of a disjunction may have a different mapping for
+	% !.X and/or !:X.  The reconciled svar_info for the disjunction
+	% takes the highest numbered mapping for each disjunct (each
+	% state variable mapping for !.X or !:X will have a name of
+	% the form `STATE_VARIABLE_X_n' for some number `n'.)
+	%
+:- func reconciled_disj_svar_info(prog_varset, hlds_goal_svar_infos) =
+		svar_info.
+
+reconciled_disj_svar_info(_, []) = _ :-
+	error("make_hlds__reconciled_disj_svar_info: empty disjunct list").
+
+reconciled_disj_svar_info(VarSet, [{_, SInfo0} | DisjSInfos]) = SInfo :-
+
+		% We compute the set of final !. and !: state variables
+		% over the whole disjunction (not all arms will necessarily
+		% include !. and !: mappings for all state variables).
+		%
+	Dots0   = set__sorted_list_to_set(map__keys(SInfo0 ^ dot)),
+	Colons0 = set__sorted_list_to_set(map__keys(SInfo0 ^ colon)),
+	Dots    = union_dot_svars(Dots0, DisjSInfos),
+	Colons  = union_colon_svars(Colons0, DisjSInfos),
+
+		% Then we update SInfo0 to take the highest numbered
+		% !. and !: mapping for each state variable.
+		%
+	SInfo   = list__foldl(
+			reconciled_svar_infos(VarSet, Dots, Colons),
+			DisjSInfos,
+			SInfo0
+		  ).
+
+
+:- func union_dot_svars(svar_set, hlds_goal_svar_infos) = svar_set.
+
+union_dot_svars(Dots, []                       ) = Dots.
+
+union_dot_svars(Dots, [{_, SInfo} | DisjSInfos]) =
+	union_dot_svars(
+		Dots `union`
+			set__sorted_list_to_set(map__keys(SInfo ^ dot)),
+		DisjSInfos
+	).
+
+
+:- func union_colon_svars(svar_set, hlds_goal_svar_infos) = svar_set.
+
+union_colon_svars(Colons, []                       ) = Colons.
+
+union_colon_svars(Colons, [{_, SInfo} | DisjSInfos]) =
+	union_colon_svars(
+		Colons `union`
+			set__sorted_list_to_set(map__keys(SInfo ^ colon)),
+		DisjSInfos
+	).
+
+
+:- func reconciled_svar_infos(prog_varset, svar_set, svar_set,
+		hlds_goal_svar_info, svar_info) = svar_info.
+
+reconciled_svar_infos(VarSet, Dots, Colons,
+		{_, SInfoX}, SInfo0) = SInfo :-
+	SInfo1 = set__fold(
+			reconciled_svar_infos_dots(VarSet, SInfoX),
+			Dots,
+			SInfo0
+		 ),
+	SInfo  = set__fold(
+			reconciled_svar_infos_colons(VarSet, SInfoX),
+			Colons,
+			SInfo1
+		 ).
+
+
+:- func reconciled_svar_infos_dots(prog_varset, svar_info, svar, svar_info) =
+		svar_info.
+
+reconciled_svar_infos_dots(VarSet, SInfoX, StateVar, SInfo0) = SInfo :-
+	( if
+		DotX = SInfoX ^ dot ^ elem(StateVar),
+		Dot0 = SInfo0 ^ dot ^ elem(StateVar)
+	  then
+	  	NameX = varset__lookup_name(VarSet, DotX) `with_type` string,
+	  	Name0 = varset__lookup_name(VarSet, Dot0) `with_type` string,
+		compare(RDot, NameX, Name0),
+		(
+			RDot  = (<),
+			SInfo = ( SInfo0 ^ dot ^ elem(StateVar) := Dot0 )
+		;
+			RDot  = (=),
+			SInfo = SInfo0
+		;
+			RDot  = (>),
+			SInfo = ( SInfo0 ^ dot ^ elem(StateVar) := DotX )
+		)
+	  else
+	  	SInfo = SInfo0
+	).
+
+
+:- func reconciled_svar_infos_colons(prog_varset, svar_info, svar, svar_info) =
+		svar_info.
+
+reconciled_svar_infos_colons(VarSet, SInfoX, StateVar, SInfo0) = SInfo :-
+	( if
+		ColonX = SInfoX ^ colon ^ elem(StateVar),
+		Colon0 = SInfo0 ^ colon ^ elem(StateVar)
+	  then
+	  	NameX = varset__lookup_name(VarSet, ColonX) `with_type` string,
+	  	Name0 = varset__lookup_name(VarSet, Colon0) `with_type` string,
+		compare(RColon, NameX, Name0),
+		(
+			RColon = (<),
+			SInfo  = ( SInfo0 ^ colon ^ elem(StateVar) := Colon0 )
+		;
+			RColon = (=),
+			SInfo  = SInfo0
+		;
+			RColon = (>),
+			SInfo  = ( SInfo0 ^ colon ^ elem(StateVar) := ColonX )
+		)
+	  else
+	  	SInfo = SInfo0
+	).
+ 
+
+:- func add_disj_unifiers(prog_context, hlds_goal_info, svar_info, svars,
+		hlds_goal_svar_info) = hlds_goal.
+
+add_disj_unifiers(Context, GoalInfo, SInfo, StateVars, {GoalX, SInfoX}) =
+		Goal :-
+	Unifiers = list__foldl(add_disj_unifier(Context, SInfo, SInfoX),
+			StateVars, []),
+	goal_to_conj_list(GoalX, GoalsX),
+	conj_list_to_goal(GoalsX ++ Unifiers, GoalInfo, Goal).
+
+
+:- func add_disj_unifier(prog_context, svar_info, svar_info, svar,
+		hlds_goals) = hlds_goals.
+
+add_disj_unifier(Context, SInfo, SInfoX, StateVar, Unifiers) =
+	( if
+		Dot  = SInfo  ^ dot ^ elem(StateVar),
+		DotX = SInfoX ^ dot ^ elem(StateVar),
+		Dot \= DotX
+	  then
+	  	[svar_unification(Context, Dot, DotX) | Unifiers]
+	  else
+	  	Unifiers
+	).
+
+%------------------------------------------------------------------------------%
+
+	% We treat equivalence goals as if they were negations (they are
+	% in a negated context after all.)
+	%
+:- pred finish_equivalence(svar_info, svar_info, svar_info).
+:- mode finish_equivalence(in, in, out) is det.
+
+finish_equivalence(SInfoBefore, SInfoEqv, SInfo) :-
+	finish_negation(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.
+	%
+	% (We can still be in an atomic context if, for example, we've
+	% been processing a function call which must appear as an
+	% expression and hence occur inside an atomic context.)
+	%
+:- 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, ParentSInfo0) then
+		ParentSInfo = ( ParentSInfo0 ^ dot := SInfo0 ^ dot ),
+		( 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      )
+			    ^ external_dot := SInfo0 ^ dot )
+			    ^ 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 ).
+
+%------------------------------------------------------------------------------%
+
+	% Replace !X args with two args !.X, !:X in that order.
+	%
+:- func expand_bang_state_var_args(list(prog_term)) = list(prog_term).
+
+expand_bang_state_var_args(Args) =
+	list__foldr(expand_bang_state_var, Args, []).
+
+
+:- func expand_bang_state_var(prog_term, list(prog_term)) =
+		list(prog_term).
+
+expand_bang_state_var(T @ variable(_), Ts) = [T | Ts].
+
+expand_bang_state_var(T @ functor(Const, Args, Ctxt), Ts) =
+	( if Const = atom("!"), Args = [variable(_StateVar)] then
+		[ functor(atom("!."), Args, Ctxt),
+		  functor(atom("!:"), Args, Ctxt)
+		    | Ts ]
+	  else
+	  	[ T | Ts ]
+	).
+
+%------------------------------------------------------------------------------%
+
+:- func expand_bang_state_var_args_in_instance_method_heads(instance_body) =
+		instance_body.
+
+expand_bang_state_var_args_in_instance_method_heads(abstract) = abstract.
+
+expand_bang_state_var_args_in_instance_method_heads(concrete(Methods)) =
+	concrete(list__map(expand_method_bsvs, Methods)).
+
+
+:- func expand_method_bsvs(instance_method) = instance_method.
+
+expand_method_bsvs(IM) = IM :-
+	IM = instance_method(_, _, name(_), _, _).
+
+expand_method_bsvs(IM0) = IM :-
+	IM0 = instance_method(PredOrFunc, Method, clauses(Cs0), Arity0, Ctxt),
+	Cs  = list__map(expand_item_bsvs, Cs0),
+		% Note that the condition should always succeed...
+		%
+	( if   Cs = [clause(_, _, _, Args, _) | _]
+	  then adjust_func_arity(PredOrFunc, Arity, list__length(Args))
+	  else Arity = Arity0
+	),
+	IM  = instance_method(PredOrFunc, Method, clauses(Cs), Arity, Ctxt).
+
+
+	% The instance method clause items will all be clause items.
+	%
+:- func expand_item_bsvs(item) = item.
+
+expand_item_bsvs(Item) =
+	( if   Item = clause(VarSet, PredOrFunc, SymName, Args, Body)
+	  then clause(VarSet, PredOrFunc, SymName,
+			expand_bang_state_var_args(Args), Body)
+	  else Item
+	).
+
+%------------------------------------------------------------------------------%
+
+	% Given a list of argument terms, substitute !.X and !:X with
+	% the corresponding state variable mappings.  Any !X should
+	% already have been expanded into !.X, !:X via a call to
+	% expand_bang_state_var_args/1.
+	%
+:- pred substitute_state_var_mappings(list(prog_term), list(prog_term),
+		prog_varset, prog_varset, svar_info, svar_info, io, io).
+:- mode substitute_state_var_mappings(in, out, in, out, in, out, di, uo) is det.
+
+substitute_state_var_mappings([],    [],
+		VarSet,  VarSet, SInfo,  SInfo) --> [].
+
+substitute_state_var_mappings([Arg0 | Args0], [Arg | Args],
+		VarSet0, VarSet, SInfo0, SInfo) -->
+	substitute_state_var_mapping(Arg0, Arg,
+		VarSet0, VarSet1, SInfo0, SInfo1),
+	substitute_state_var_mappings(Args0, Args,
+		VarSet1, VarSet,  SInfo1, SInfo ).
+
+
+:- pred substitute_state_var_mapping(prog_term, prog_term,
+		prog_varset, prog_varset, svar_info, svar_info, io, io).
+:- mode substitute_state_var_mapping(in, out, in, out, in, out, di, uo) is det.
+
+substitute_state_var_mapping(Arg0, Arg, VarSet0, VarSet, SInfo0, SInfo) -->
+	( if
+		{ Arg0 = functor(atom("!."), [variable(StateVar)], Context) }
+	  then
+		dot(Context, StateVar, Var, VarSet0, VarSet, SInfo0, SInfo),
+		{ Arg  = variable(Var) }
+	  else if
+		{ Arg0 = functor(atom("!:"), [variable(StateVar)], Context) }
+	  then
+		colon(Context, StateVar, Var, VarSet0, VarSet, SInfo0, SInfo),
+		{ Arg  = variable(Var) }
+	  else
+	  	{ VarSet = VarSet0 },
+		{ SInfo  = SInfo0  },
+	  	{ Arg    = Arg0    }
+	).
+
+%------------------------------------------------------------------------------%
+
+:- pred illegal_state_var_func_result(pred_or_func, list(prog_term), svar).
+:- mode illegal_state_var_func_result(in, in, out) is semidet.
+
+illegal_state_var_func_result(function, Args, StateVar) :-
+	list__last(Args, functor(atom("!"), [variable(StateVar)], _Ctxt)).
+
+%------------------------------------------------------------------------------%
+
+	% We do not allow !X to appear as a lambda head argument.
+	% XXX We could extend the syntax still further to accommodate
+	% this as an option, e.g. !IO::(di, uo).
+	%
+:- pred lambda_args_contain_bang_state_var(list(prog_term), prog_var).
+:- mode lambda_args_contain_bang_state_var(in, out) is semidet.
+
+lambda_args_contain_bang_state_var([Arg | Args], StateVar) :-
+	( if   Arg      = functor(atom("!"), [variable(StateVar0)], _)
+	  then StateVar = StateVar0
+	  else lambda_args_contain_bang_state_var(Args, StateVar)
+	).
+
+%------------------------------------------------------------------------------%
+
+:- pred report_illegal_state_var_update(prog_context, prog_varset, svar,
+		io, io).
+:- mode report_illegal_state_var_update(in, in, in, di, uo) is det.
+
+report_illegal_state_var_update(Context, VarSet, StateVar) -->
+	{ Name = varset__lookup_name(VarSet, StateVar) },
+	prog_out__write_context(Context),
+	report_error(string__format("\
+cannot use !:%s in this context;\n", [s(Name)])),
+	prog_out__write_context(Context),
+	io__format("\
+  however !.%s may be used here.\n", [s(Name)]).
+
+%------------------------------------------------------------------------------%
+
+:- pred report_non_visible_state_var(prog_context, prog_varset, svar, io, io).
+:- mode report_non_visible_state_var(in, in, in, di, uo) is det.
+
+report_non_visible_state_var(Context, VarSet, StateVar) -->
+	{ Name = varset__lookup_name(VarSet, StateVar) },
+	prog_out__write_context(Context),
+	report_error(string__format("\
+state variable !:%s is not visible in this context.\n", [s(Name)])).
+
+%------------------------------------------------------------------------------%
+
+:- pred report_unitialized_state_var(prog_context, prog_varset, svar, io, io).
+:- mode report_unitialized_state_var(in, in, in, di, uo) is det.
+
+report_unitialized_state_var(Context, VarSet, StateVar) -->
+	{ Name = varset__lookup_name(VarSet, StateVar) },
+	prog_out__write_context(Context),
+	report_warning(string__format("\
+Warning: reference to unitialized state variable !.%s.\n", [s(Name)])).
+
+%------------------------------------------------------------------------------%
+
+:- pred report_illegal_func_svar_result(prog_context, prog_varset, svar,
+		io, io).
+:- mode report_illegal_func_svar_result(in, in, in, di, uo) is det.
+
+report_illegal_func_svar_result(Context, VarSet, StateVar) -->
+	{ Name = varset__lookup_name(VarSet, StateVar) },
+	prog_out__write_context(Context),
+	report_error(string__format("\
+!%s cannot be a function result.\n", [s(Name)])),
+	prog_out__write_context(Context),
+	io__format("\
+  You probably meant !.%s or !:%s.\n", [s(Name), s(Name)]).
+
+%------------------------------------------------------------------------------%
+
+:- pred report_illegal_bang_svar_lambda_arg(prog_context, prog_varset, svar,
+		io, io).
+:- mode report_illegal_bang_svar_lambda_arg(in, in, in, di, uo) is det.
+
+report_illegal_bang_svar_lambda_arg(Context, VarSet, StateVar) -->
+	{ Name = varset__lookup_name(VarSet, StateVar) },
+	prog_out__write_context(Context),
+	report_error(string__format("\
+!%s cannot be a lambda argument.\n", [s(Name)])),
+	prog_out__write_context(Context),
+	io__format("\
+  Perhaps you meant !.%s or !:%s.\n", [s(Name), s(Name)]).
+
+%------------------------------------------------------------------------------%
 %------------------------------------------------------------------------------%
--------------------------------------------------------------------------
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