[m-rev.] For review: State Variables

Ralph Becket rafe at cs.mu.OZ.AU
Thu May 9 18:48:09 AEST 2002


Simon Taylor, Monday,  6 May 2002:
> On 02-May-2002, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> > -module_add_clause(ModuleInfo0, ClauseVarSet, PredOrFunc, PredName, Args, Body,
> > +module_add_clause(ModuleInfo0, ClauseVarSet, PredOrFunc, PredName, Args0, Body,
> >  			Status, Context, GoalType, ModuleInfo,
> >  			Info0, Info) -->
> > +
> > +	{ Args = expand_dot_colon_state_var_args(Args0) },
> > +
> 
> That doesn't do the right thing for function clauses.

Fixed throughout.

> > +		% Handle !.X state variable references.
> > +		{ F = term__atom("!.") },
> > +		{ Args = [term__variable(StateVar)] }
> > +	->
> > +		dot(Context, StateVar, Var, VarSet0, VarSet,
> > +			SInfo0, SInfo),
> > +		{ Goal = svar_unification(Context, X, Var) },
> > +		{ Info = Info0 }
> > +	;
> > +		% Handle !:X state variable references.
> > +		{ F = term__atom("!:") },
> > +		{ Args = [term__variable(StateVar)] }
> > +	->
> > +		colon(Context, StateVar, Var, VarSet0, VarSet,
> > +			SInfo0, SInfo),
> > +		{ Goal = svar_unification(Context, X, Var) },
> > +		{ Info = Info0 }
> 
> The way you've done this the type and mode error messages for
> state variable references will be really awful. 

Fixed.

> It would be better to expand state variable references before calling
> make_fresh_arg_vars.

Done.

> You should allow state variable quantifiers on if-then-elses.

On the To-Do list.

> > -get_conj(Goal, Subst, Conj0, VarSet0, Conj, VarSet, Info0, Info) -->
> > +get_conj(Goal, Subst, Conj0, VarSet0, Conj, VarSet, Info0, Info,
> > +		SInfo0, SInfo) -->
> >  	(
> >  		{ Goal = (A,B) - _Context }
> >  	->
> > -		get_conj(B, Subst, Conj0, VarSet0, Conj1, VarSet1,
> > -						Info0, Info1),
> > -		get_conj(A, Subst, Conj1, VarSet1, Conj, VarSet, Info1, Info)
> > +		get_conj(A, Subst, Conj0, VarSet0, Conj1, VarSet1,
> > +			Info0, Info1, SInfo0, SInfo1),
> > +		get_conj(B, Subst, Conj1, VarSet1, Conj, VarSet,
> > +			Info1, Info,  SInfo1, SInfo)
> >  	;
> >  		transform_goal(Goal, VarSet0, Subst, Goal1, VarSet,
> > -						Info0, Info),
> > +			Info0, Info,  SInfo0, SInfo),
> >  		{ goal_to_conj_list(Goal1, ConjList) },
> >  		{ list__append(ConjList, Conj0, Conj) }
> >  	).
> 
> You're now building Conj in reverse, so ConjList needs to be reversed
> before adding it to Conj0 (same for get_par_conj and get_disj).

The lists are reversed in the respective callers.

> > +	% This synonym improves code legibility.
> > +	%
> > +:- type svar == prog_var.
> 
> It would probably be better to do
> :- type svar == var(svar_type).
> :- type svar_type ---> svar_type.
> 
> This would help avoid confusing state variables with ordinary variables.

That means putting in coercions all over the shop.  Since it isn't a
problem at the moment, I'll defer that to a later change.

> > +:- 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.
> 
> This predicate needs documentation and a more descriptive name.
> 
> > +:- 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.
> 
> Ditto.

Done.

> > +	% 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).
> 
> It's probably better to substitute in the head rather than adding
> unifications (adding too many variables will cause slow compilation).

Done.

> +       % When we finish a call, we're either still inside the
> +       % atomic formula, in which case we simply propagate the set of
> +       % "updated" state variables, or we've just emerged, in which
> case
> +       % we need to set up the svar_info for the next conjunct.
> +       %
> +:- pred finish_call(prog_varset, prog_varset, svar_info, svar_info).
> +:- mode finish_call(in, out, in, out) is det.
> 
> How can you still be inside an atomic formula when you've finished a
> call?

I'm using call in a generic sense here, so an argument subexpression
is basically an atomic call inside an atomic call.  Perhaps `atomic'
is a poor choice of word, since it really means "goal and all its
subexpressions".  I've amended the comment to explain properly.

> > +finish_if_then_else(Context, Then0, Then, Else0, Else, VarSet0, VarSet,
> > +		SInfoT, SInfoE, SInfo) :-
> > +	SInfo0       = SInfoT,
> > +	N            = int__max(SInfoT ^ num, SInfoE ^ num),
> > +	next_svar_info(N, VarSet0, VarSet, SInfo0, SInfo),
> > +
> > +	goal_info_init(Context, GoalInfo),
> > +
> > +	goal_to_conj_list(Then0, ThenGoals0),
> > +	ThenUnifiers = svar_unifiers(Context, SInfo ^ dot, SInfoT ^ dot),
> > +	conj_list_to_goal(ThenGoals0 ++ ThenUnifiers, GoalInfo, Then),
> > +
> > +	goal_to_conj_list(Else0, ElseGoals0),
> > +	ElseUnifiers = svar_unifiers(Context, SInfo ^ dot, SInfoE ^ dot),
> > +	conj_list_to_goal(ElseGoals0 ++ ElseUnifiers, GoalInfo, Else).
> 
> This doesn't handle code like the following properly:
> 
> 	( p(!X) ->
> 		q
> 	;
> 		r(!X)
> 	).

Fixed.

> It would also be nice to avoid adding lots of extra variables at the
> end of each branch (you do this for disjunctions as well). See how
> prog_io_dcg.m does this.

Fixed.

> > +:- pred next_svar_info(int, prog_varset, prog_varset, svar_info, svar_info).
> > +:- mode next_svar_info(in, in, out, in, out) is det.
> 
> Documentation please.

Deleted.

> > +finish_negation(Context, Goal0, Goal, VarSet0, VarSet,
> > +		SInfoBefore, SInfoNeg, SInfo) :-
> > +	SInfo0    = SInfoBefore,
> > +	N         = SInfoNeg ^ num,
> > +	next_svar_info(N, VarSet0, VarSet, SInfo0, SInfo),
> > +
> > +	goal_info_init(Context, GoalInfo),
> > +
> > +	goal_to_conj_list(Goal0, Goals0),
> > +	Unifiers  = svar_unifiers(Context, SInfo ^ dot, SInfo0 ^ dot),
> > +	conj_list_to_goal(Goals0 ++ Unifiers, GoalInfo, Goal).
> 
> You should be able to do this without adding unifications.
> I think you're making life difficult for yourself by trying
> to maintain the `dot' and `colon' mappings all the time, rather
> than generating a `colon' mapping only when a reference to `!:X'
> is seen in an atom (as prog_io_dcg.m does).

Fixed.

> > @@ -220,10 +242,29 @@
> >  	parse_goal(A0, V0, A, V1),
> >  	parse_goal(B0, V1, B, V).
> >  
> > -parse_goal_2("some", [Vars0, A0], V0, some(Vars, A), V):-
> > -	parse_list_of_vars(Vars0, Vars1),
> > -	list__map(term__coerce_var, Vars1, Vars),
> > -	parse_goal(A0, V0, A, V).
> > +parse_goal_2("some", [QVars, A0], V0, GoalExpr, V):-
> 
> You also need to modify the similar code in prog_io_dcg.m.

Done.

> You should also handle state variables in the quantifiers
> on if-then-elses.

You mentioned this one above - it's on the TODO list.

Some diffs:

Index: prog_io_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io_util.m,v
retrieving revision 1.24
diff -u -r1.24 prog_io_util.m
--- prog_io_util.m	20 Mar 2002 12:37:14 -0000	1.24
+++ prog_io_util.m	9 May 2002 08:09:05 -0000
@@ -66,6 +66,12 @@
 :- pred parse_list_of_vars(term(T), list(var(T))).
 :- mode parse_list_of_vars(in, out) is semidet.
 
+	% Parse a list of quantified variables, splitting it into
+	% state variables and ordinary logic variables, respectively.
+	%
+:- pred parse_quantifier_vars(term(T), list(var(T)), list(var(T))).
+:- mode parse_quantifier_vars(in, out, out) is semidet.
+
 :- pred parse_name_and_arity(module_name, term(_T), sym_name, arity).
 :- mode parse_name_and_arity(in, in, out, out) is semidet.
 
@@ -591,4 +597,20 @@
 		[]
 	).
 
+%------------------------------------------------------------------------------%
+
+parse_quantifier_vars(functor(atom("[]"),  [],     _), [],  []).
+
+parse_quantifier_vars(functor(atom("[|]"), [H, T], _), SVs, Vs) :-
+	(
+		H   = functor(atom("!"), [variable(SV)], _),
+		SVs = [SV | SVs0],
+		parse_quantifier_vars(T, SVs0, Vs)
+	;
+		H   = variable(V),
+		Vs = [V | Vs0],
+		parse_quantifier_vars(T, SVs, Vs0)
+	).
+
+%-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%

Index: prog_io_dcg.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io_dcg.m,v
retrieving revision 1.19
diff -u -r1.19 prog_io_dcg.m
--- prog_io_dcg.m	20 Mar 2002 12:37:13 -0000	1.19
+++ prog_io_dcg.m	9 May 2002 08:13:27 -0000
@@ -288,20 +288,60 @@
 	Var = Var0.
 
 	% Universal quantification.
-parse_dcg_goal_2("all", [Vars0, A0], Context,
-		VarSet0, N0, Var0, all(Vars, A) - Context,
+parse_dcg_goal_2("all", [QVars, A0], Context,
+		VarSet0, N0, Var0, GoalExpr - Context,
 		VarSet, N, Var) :-
-	term__coerce(Vars0, Vars1),
-	term__vars(Vars1, Vars),
-	parse_dcg_goal(A0, VarSet0, N0, Var0, A, VarSet, N, Var).
+
+		% Extract any state variables in the quantifier.
+		%
+	parse_quantifier_vars(QVars, StateVars0, Vars0),
+	list__map(term__coerce_var, StateVars0, StateVars),
+	list__map(term__coerce_var, Vars0, Vars),
+
+	parse_dcg_goal(A0, VarSet0, N0, Var0, A @ (GoalExprA - ContextA),
+			VarSet, N, Var),
+
+	(
+		Vars = [],    StateVars = [],
+		GoalExpr = GoalExprA
+	;
+		Vars = [],    StateVars = [_|_],
+		GoalExpr = all_state_vars(StateVars, A)
+	;
+		Vars = [_|_], StateVars = [],
+		GoalExpr = all(Vars, A)
+	;
+		Vars = [_|_], StateVars = [_|_],
+		GoalExpr = all(Vars, all_state_vars(StateVars, A) - ContextA)
+	).
 
 	% Existential quantification.
-parse_dcg_goal_2("some", [Vars0, A0], Context,
-		VarSet0, N0, Var0, some(Vars, A) - Context,
+parse_dcg_goal_2("some", [QVars, A0], Context,
+		VarSet0, N0, Var0, GoalExpr - Context,
 		VarSet, N, Var) :-
-	term__coerce(Vars0, Vars1),
-	term__vars(Vars1, Vars),
-	parse_dcg_goal(A0, VarSet0, N0, Var0, A, VarSet, N, Var).
+
+		% Extract any state variables in the quantifier.
+		%
+	parse_quantifier_vars(QVars, StateVars0, Vars0),
+	list__map(term__coerce_var, StateVars0, StateVars),
+	list__map(term__coerce_var, Vars0, Vars),
+
+	parse_dcg_goal(A0, VarSet0, N0, Var0, A @ (GoalExprA - ContextA),
+			VarSet, N, Var),
+
+	(
+		Vars = [],    StateVars = [],
+		GoalExpr = GoalExprA
+	;
+		Vars = [],    StateVars = [_|_],
+		GoalExpr = some_state_vars(StateVars, A)
+	;
+		Vars = [_|_], StateVars = [],
+		GoalExpr = some(Vars, A)
+	;
+		Vars = [_|_], StateVars = [_|_],
+		GoalExpr = some(Vars, some_state_vars(StateVars, A) - ContextA)
+	).
 
 :- pred parse_dcg_goal_with_purity(term, prog_varset, int, prog_var,
 		purity, goal, prog_varset, int, prog_var).

Relative-diff:

diff -u make_hlds.m make_hlds.m
--- make_hlds.m	2 May 2002 03:54:54 -0000
+++ make_hlds.m	9 May 2002 08:26:46 -0000
@@ -117,7 +117,7 @@
 :- import_module libs__options, libs__globals.
 
 :- import_module string, char, int, set, bintree, map, multi_map, require.
-:- import_module bag, term, varset, getopt, assoc_list, term_io, counter.
+:- import_module bag, term, varset, getopt, assoc_list, term_io.
 
 parse_tree_to_hlds(module(Name, Items), MQInfo0, EqvMap, Module, QualInfo,
 		UndefTypes, UndefModes) -->
@@ -3586,14 +3586,22 @@
 			Status, Context, GoalType, ModuleInfo,
 			Info0, Info) -->
 
-	{ Args = expand_dot_colon_state_var_args(Args0) },
+	{ 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")
@@ -3605,7 +3613,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,
@@ -3662,6 +3671,13 @@
 		PredInfo1 = PredInfo0
 	},
 	(
+		{ IllegalSVarResult = yes(StateVar) }
+	->
+		report_illegal_func_svar_result(Context, ClauseVarSet,
+			StateVar),
+		{ ModuleInfo = ModuleInfo1 },
+		{ Info       = Info0 }
+	;
 		{ pred_info_pragma_goal_type(PredInfo1) },
 		{ get_mode_annotations(Args, _, empty, ModeAnnotations) },
 		{ ModeAnnotations = empty ; ModeAnnotations = none }
@@ -3991,31 +4007,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") }
 	).
@@ -5297,8 +5325,7 @@
 	transform(Subst, HeadVars, Args, Body, VarSet1, Context, PredOrFunc,
 			Arity, GoalType, Goal0, VarSet, Warnings,
 			transform_info(Module0, Info1),
-			transform_info(Module, Info2),
-			new_svar_info),
+			transform_info(Module, Info2)),
 	{ TVarSet = Info2 ^ tvarset },
 	{ qual_info_get_found_syntax_error(Info2, FoundError) },
 	{ qual_info_set_found_syntax_error(no, Info2, Info) },
@@ -5578,44 +5605,46 @@
 :- 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, svar_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, in, di, uo) is det.
+		in, out, di, uo) is det.
 
 transform(Subst, HeadVars, Args0, Body0, VarSet0, Context, PredOrFunc,
 		Arity, GoalType, Goal, VarSet, Warnings, Info0, Info,
-		SInfo0, IO0, IO) :-
+		IO0, IO) :-
 
-	term__apply_substitution_to_list(Args0, Subst, Args),
+	prepare_for_head(SInfo0),
 
-	hlds_goal__true_goal(Head0),
+	term__apply_substitution_to_list(Args0, Subst, Args1),
 
-	prepare_for_head(SInfo0, SInfo1),
+	substitute_state_var_mappings(Args1, Args, VarSet0, VarSet1,
+		SInfo0, SInfo1, IO0, IO1),
+
+	hlds_goal__true_goal(Head0),
 
 	( if GoalType = promise(_) then
-		VarSet1 = VarSet0,
+		VarSet2 = VarSet1,
 		Head    = Head0,
 		Info1   = Info0,
 		SInfo2  = SInfo1,
-		IO1     = IO0
+		IO2     = IO1
 	  else
 		ArgContext = head(PredOrFunc, Arity),
 		insert_arg_unifications(HeadVars, Args, Context, ArgContext,
-			no, Head0, VarSet0, Head, VarSet1, Info0, Info1,
-			SInfo1, SInfo2, IO0, IO1)
+			no, Head0, VarSet1, Head, VarSet2, Info0, Info1,
+			SInfo1, SInfo2, IO1, IO2)
 	),
 
-	prepare_for_body(FinalSVarMap, VarSet1, VarSet2, SInfo2, SInfo3),
+	prepare_for_body(FinalSVarMap, VarSet2, VarSet3, SInfo2, SInfo3),
 
-	transform_goal(Body0, VarSet2, Subst, Body, VarSet3, Info1, Info2,
-		SInfo3, SInfo, IO1, IO),
+	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, VarSet3, VarTypes2,
+	implicitly_quantify_clause_body(HeadVars, Goal0, VarSet4, VarTypes2,
 		Goal, VarSet, VarTypes, Warnings),
 
 	Info = Info2 ^ qual_info ^ vartypes := VarTypes.
@@ -5648,13 +5677,17 @@
 :- 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, SInfo, SInfo) -->
-	{ 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, SInfo, SInfo) -->
-	{ 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,
@@ -5693,14 +5726,14 @@
 		if_then_else(Vars, A, B, C) - GoalInfo, VarSet,
 		Info0, Info, SInfo0, SInfo) -->
 	{ substitute_vars(Vars0, Subst, Vars) },
-	transform_goal(A0, VarSet0, Subst, A, VarSet1, Info0, Info1,
+	transform_goal(A0, VarSet0, Subst, A,  VarSet1, Info0, Info1,
 		SInfo0, SInfo1),
 	transform_goal(B0, VarSet1, Subst, B1, VarSet2, Info1, Info2,
 		SInfo1, SInfoB),
-	transform_goal(C0, VarSet2, Subst, C1, VarSet3, Info2, Info,
+	transform_goal(C0, VarSet2, Subst, C1, VarSet,  Info2, Info,
 		SInfo0, SInfoC),
 	{ goal_info_init(GoalInfo) },
-	{ finish_if_then_else(Context, B1, B, C1, C, VarSet3, VarSet,
+	{ finish_if_then_else(Context, B1, B, C1, C, VarSet,
 		SInfoB, SInfoC, SInfo) }.
 
 transform_goal_2(if_then(Vars0, A0, B0), Context, Subst, VarSet0,
@@ -5709,14 +5742,13 @@
 		Context, Subst, VarSet0, Goal, VarSet, Info0, Info,
 		SInfo0, SInfo).
 
-transform_goal_2(not(A0), Context, VarSet0, Subst, Goal, VarSet, Info0, Info,
+transform_goal_2(not(A0), _, VarSet0, Subst, Goal, VarSet, Info0, Info,
 		SInfo0, SInfo) -->
-	transform_goal(A0, VarSet0, Subst, A, VarSet1, Info0, Info,
+	transform_goal(A0, VarSet0, Subst, A, VarSet, Info0, Info,
 		SInfo0, SInfo1),
 	{ goal_info_init(GoalInfo) },
-	{ Goal0 = not(A) - GoalInfo },
-	{ finish_negation(Context, Goal0, Goal, VarSet1, VarSet,
-		SInfo0, SInfo1, SInfo) }.
+	{ Goal = not(A) - GoalInfo },
+	{ finish_negation(SInfo0, SInfo1, SInfo) }.
 
 transform_goal_2((A0, B0), _, VarSet0, Subst, Goal, VarSet, Info0, Info,
 		SInfo0, SInfo) -->
@@ -5741,9 +5773,9 @@
 transform_goal_2((A0 ; B0), Context, VarSet0, Subst, Goal, VarSet, Info0, Info,
 		SInfo0, SInfo) -->
 	get_disj(B0, Subst, [], VarSet0, L0, VarSet1, Info0, Info1, SInfo0),
-	get_disj(A0, Subst, L0, VarSet1, L1, VarSet2, Info1, Info, SInfo0),
-	{ finish_disjunction(Context, L1, L, VarSet2, VarSet, SInfo) },
-	{ goal_info_init(GoalInfo) },
+	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,
@@ -5753,7 +5785,7 @@
 	transform_goal_2(TransformedGoal, Context, VarSet0, Subst,
 		Goal, VarSet, Info0, Info, SInfo0, SInfo).
 
-transform_goal_2(equivalent(P0, Q0), Context, VarSet0, Subst, Goal, VarSet,
+transform_goal_2(equivalent(P0, Q0), _, VarSet0, Subst, Goal, VarSet,
 		Info0, Info, SInfo0, SInfo) -->
 	%
 	% `P <=> Q' is defined as `(P => Q), (Q => P)',
@@ -5765,16 +5797,15 @@
 	{ goal_info_init(GoalInfo) },
 	transform_goal(P0, VarSet0, Subst, P, VarSet1, Info0, Info1,
 		SInfo0, SInfo1),
-	transform_goal(Q0, VarSet1, Subst, Q, VarSet2, Info1, Info,
+	transform_goal(Q0, VarSet1, Subst, Q, VarSet,  Info1, Info,
 		SInfo1, SInfo2),
-	{ Goal0 = shorthand(bi_implication(P, Q)) - GoalInfo },
-	{ finish_equivalence(Context, Goal0, Goal, VarSet2, VarSet,
-		SInfo0, SInfo2, SInfo) }.
+	{ 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, SInfo0, SInfo) -->
 	{ prepare_for_call(SInfo0, SInfo1) },
-	{ Args1  = expand_dot_colon_state_var_args(Args0) },
+	{ Args1 = expand_bang_state_var_args(Args0) },
 	( 
 		{ Name = unqualified("\\=") },
 		{ Args1 = [LHS, RHS] }
@@ -5879,14 +5910,50 @@
 
 transform_goal_2(unify(A0, B0, Purity), Context, VarSet0, Subst, Goal, VarSet,
 		Info0, Info, SInfo0, SInfo) -->
-	{ prepare_for_call(SInfo0, SInfo1) },
-	{ term__apply_substitution(A0, Subst, A) },
-	{ term__apply_substitution(B0, Subst, B) },
-	unravel_unification(A, B, Context, explicit, [],
-		VarSet0, Purity, Goal, VarSet1, Info0, Info,
-		SInfo1, SInfo2),
-	{ finish_call(VarSet1, VarSet, SInfo2, 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)])),
+		globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
+		(
+			{ VerboseErrors = yes },
+			prog_out__write_context(Context),
+			report_warning(string__format("\
+       You probably meant !.%s or !:%s.\n", [s(Name), s(Name)]))
+		;
+			{ VerboseErrors = no }
+		).
+
 
 :- inst dcg_record_syntax_op = bound("=^"; ":=").
 
@@ -6911,7 +6978,7 @@
 :- 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, ForPragmaC,
+insert_arg_unifications(HeadVars, Args0, Context, ArgContext, ForPragmaC,
 		Goal0, VarSet0, Goal, VarSet, Info0, Info, SInfo0, SInfo) -->
 	( { HeadVars = [] } ->
 		{ Goal = Goal0 },
@@ -6921,9 +6988,11 @@
 	;
 		{ 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,
-			ForPragmaC, 0, List0, VarSet0, List, VarSet,
-			Info0, Info, SInfo0, SInfo),
+			ForPragmaC, 0, List0, VarSet1, List, VarSet,
+			Info0, Info, SInfo1, SInfo),
 		{ goal_info_set_context(GoalInfo0, Context, GoalInfo) },
 		{ conj_list_to_goal(List, GoalInfo, Goal) }
 	).
@@ -6971,7 +7040,7 @@
 		in, out, out, in, out, in, out, di, uo) is det.
 
 insert_arg_unifications_with_supplied_contexts(ArgVars,
-		ArgTerms, ArgContexts, Context, Goal0, VarSet0,
+		ArgTerms0, ArgContexts, Context, Goal0, VarSet0,
 		Goal, VarSet, Info0, Info, SInfo0, SInfo) -->
 	( { ArgVars = [] } ->
 		{ Goal = Goal0 },
@@ -6981,9 +7050,11 @@
 	;
 		{ 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, SInfo0, SInfo),
+			VarSet1, GoalList, VarSet, Info0, Info, SInfo1, SInfo),
 		{ goal_info_set_context(GoalInfo0, Context, GoalInfo) },
 		{ conj_list_to_goal(GoalList, GoalInfo, Goal) }
 	).
@@ -7050,9 +7121,9 @@
 		% if this is safe.
 		{ Info = Info0 },
 		{ ArgUnifyConj = [] },
-		{ map__init(EmptySubst) },
-		{ goal_util__rename_vars_in_goals(List0, no, EmptySubst,
-			List1) },
+		{ 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)
 		;
@@ -7081,7 +7152,7 @@
 :- mode append_arg_unifications(in, in, in, in, in, in,
 		out, out, in, out, in, out, di, uo) is det.
 
-append_arg_unifications(HeadVars, Args, Context, ArgContext, Goal0,
+append_arg_unifications(HeadVars, Args0, Context, ArgContext, Goal0,
 		VarSet0, Goal, VarSet, Info0, Info, SInfo0, SInfo) -->
 	( { HeadVars = [] } ->
 		{ Goal = Goal0 },
@@ -7091,9 +7162,11 @@
 	;
 		{ 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,
-			SInfo0, SInfo),
+			0, List0, VarSet1, List, VarSet, Info0, Info,
+			SInfo1, SInfo),
 		{ conj_list_to_goal(List, GoalInfo, Goal) }
 	).
 
@@ -7220,9 +7293,26 @@
 :- mode unravel_unification(in, in, in, in, in, in, in, out, out,
 		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,
+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,
@@ -7239,40 +7329,25 @@
 	%	NewVar3 = A3.
 	% In the trivial case `X = c', no unravelling occurs.
 
-unravel_unification(term__variable(X), RHS,
+unravel_unification_2(term__variable(X), RHS,
 		Context, MainContext, SubContext, VarSet0, Purity,
 		Goal, VarSet, Info0, Info, SInfo0, SInfo) -->
-	{ RHS = term__functor(F, Args, FunctorContext) },
+	{ RHS = term__functor(F, Args0, FunctorContext) },
+	{ Args1 = expand_bang_state_var_args(Args0) },
+	substitute_state_var_mappings(Args1, Args, VarSet0, VarSet1,
+		SInfo0, SInfo1),
 	(
-		% Handle !.X state variable references.
-		{ F = term__atom("!.") },
-		{ Args = [term__variable(StateVar)] }
-	->
-		dot(Context, StateVar, Var, VarSet0, VarSet,
-			SInfo0, SInfo),
-		{ Goal = svar_unification(Context, X, Var) },
-		{ Info = Info0 }
-	;
-		% Handle !:X state variable references.
-		{ F = term__atom("!:") },
-		{ Args = [term__variable(StateVar)] }
-	->
-		colon(Context, StateVar, Var, VarSet0, VarSet,
-			SInfo0, SInfo),
-		{ Goal = svar_unification(Context, X, Var) },
-		{ Info = Info0 }
-	;
 		% Handle explicit type qualification.
 		{ F = term__atom("with_type") },
 		{ Args = [RVal, DeclType0] }
 	->
 		{ 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, SInfo0, SInfo)
+			Context, MainContext, SubContext, VarSet1,
+			Purity, Goal, VarSet, Info1, Info, SInfo1, SInfo)
 	;
 		% Handle unification expressions.
 		{ F = term__atom("@") },
@@ -7280,12 +7355,12 @@
 	->
 		unravel_unification(term__variable(X), LVal,
 			Context, MainContext, SubContext,
-			VarSet0, Purity, Goal1, VarSet1, Info0, Info1,
-			SInfo0, SInfo1),
+			VarSet1, Purity, Goal1, VarSet2, Info0, Info1,
+			SInfo1, SInfo2),
 		unravel_unification(term__variable(X), RVal,
 			Context, MainContext, SubContext,
-			VarSet1, Purity, Goal2, VarSet, Info1, Info,
-			SInfo1, SInfo),
+			VarSet2, Purity, Goal2, VarSet, Info1, Info,
+			SInfo2, SInfo),
 		{ goal_info_init(GoalInfo) },
 		{ goal_to_conj_list(Goal1, ConjList1) },
 		{ goal_to_conj_list(Goal2, ConjList2) },
@@ -7329,12 +7404,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, SInfo0),
-		{ SInfo = SInfo0 }
+			Info2, Info, SInfo1),
+		{ SInfo = SInfo1 }
 	;
 	    {
 		% handle higher-order dcg pred expressions -
@@ -7351,15 +7426,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, SInfo0),
-		{ SInfo = SInfo0 },
+			Info1, Info, SInfo1),
+		{ SInfo = SInfo1 },
 		{ Goal0 = GoalExpr - GoalInfo0 },
 		{ add_goal_info_purity_feature(GoalInfo0, Purity, GoalInfo) },
 		{ Goal = GoalExpr - GoalInfo }
@@ -7377,21 +7452,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(SInfo0, SInfo1) },
+		{ prepare_for_if_then_else_expr_condition(SInfo1, SInfo2) },
 		check_expr_purity(Purity, Context, Info0, Info1),
 		{ map__init(EmptySubst) },
 		transform_goal(IfParseTree, VarSet11, EmptySubst,
-			IfGoal, VarSet22, Info1, Info2, SInfo1, SInfo2),
-		{ finish_if_then_else_expr_condition(SInfo0, SInfo2, SInfo3) },
+			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, SInfo3, SInfo4),
+			pure, ThenGoal, VarSet33, Info2, Info3, SInfo4, SInfo5),
 		unravel_unification(term__variable(X), ElseTerm,
 			Context, MainContext, SubContext, VarSet33, pure,
-			ElseGoal, VarSet, Info3, Info, SInfo4, SInfo),
+			ElseGoal, VarSet, Info3, Info, SInfo5, SInfo),
 		{ IfThenElse = if_then_else(Vars, IfGoal,
 			ThenGoal, ElseGoal) },
 		{ goal_info_init(Context, GoalInfo) },
@@ -7405,16 +7480,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,
-			SInfo0, SInfo1),
+			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, SInfo1, SInfo)
+			VarSet3, Goal, VarSet, Info2, Info, SInfo2, SInfo)
 	;
 		% handle field update expressions
 		{ F = term__atom(":=") },
@@ -7426,30 +7501,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,
+			VarSet3, VarSet4, Functor,
 			InnerFunctor - FieldSubContext, Goal0, Info1, Info2,
-			SInfo0, SInfo1),
+			SInfo1, SInfo2),
 
 		{ TermArgContext = functor(Functor, MainContext, SubContext) },
 		{ TermArgNumber = 1 },
 		append_arg_unification(InputTermVar, InputTerm,
 			FunctorContext, TermArgContext, TermArgNumber,
-			TermUnifyConj, VarSet3, VarSet4, Info2, Info3,
-			SInfo1, SInfo2),
+			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,
-			SInfo2, SInfo),
+			FieldUnifyConj, VarSet5, VarSet, Info3, Info,
+			SInfo3, SInfo),
 
 		{ Goal0 = _ - GoalInfo0 },
 		{ goal_to_conj_list(Goal0, GoalList0) },
@@ -7478,11 +7553,11 @@
 			{ add_goal_info_purity_feature(GoalInfo0, Purity,
 				GoalInfo) },
 			{ Goal = GoalExpr - GoalInfo },
-			{ VarSet = VarSet0 },
-			{ SInfo = SInfo0 }
+			{ 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,
@@ -7498,8 +7573,8 @@
 			( { Purity = pure } ->
 				append_arg_unifications(HeadVars, FunctorArgs,
 					FunctorContext, ArgContext, Goal0,
-					VarSet1, Goal, VarSet,
-					Info1, Info, SInfo0, SInfo)
+					VarSet2, Goal, VarSet,
+					Info1, Info, SInfo1, SInfo)
 			;
 				{ Goal0 = GoalExpr - GoalInfo0 },
 				{ add_goal_info_purity_feature(GoalInfo0,
@@ -7507,8 +7582,8 @@
 				{ Goal1 = GoalExpr - GoalInfo },
 				insert_arg_unifications(HeadVars, FunctorArgs,
 					FunctorContext, ArgContext, no, Goal1,
-					VarSet1, Goal, VarSet,
-					Info1, Info, SInfo0, SInfo)
+					VarSet2, Goal, VarSet,
+					Info1, Info, SInfo1, SInfo)
 			)
 		)
 	).
@@ -7516,7 +7591,7 @@
 
 	% Handle `f(...) = X' in the same way as `X = f(...)'.
 
-unravel_unification(term__functor(F, As, FC), term__variable(Y),
+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),
@@ -7530,7 +7605,7 @@
 	% Note that we can't simplify it yet, because we might simplify
 	% away type errors.
 
-unravel_unification(term__functor(LeftF, LeftAs, LeftC),
+unravel_unification_2(term__functor(LeftF, LeftAs, LeftC),
 		term__functor(RightF, RightAs, RightC),
 		Context, MainContext, SubContext, VarSet0,
 		Purity, Goal, VarSet, Info0, Info, SInfo0, SInfo) -->
@@ -7614,7 +7689,7 @@
 :- mode build_lambda_expression(in, in, in, in, in, in, in, in,
 		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, SInfo0) -->
 	%
@@ -7652,56 +7727,75 @@
 	% 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) },
-	{ prepare_for_head(SInfo0, SInfo1) },
-	{ hlds_goal__true_goal(Head0) },
-	{ ArgContext = head(PredOrFunc, NumArgs) },
+	(
+		{ illegal_state_var_func_result(PredOrFunc, Args0, StateVar) }
+	->
+		report_illegal_func_svar_result(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),
 
-	insert_arg_unifications(LambdaVars, Args, Context, ArgContext,
-		no, Head0, VarSet1, Head, VarSet2, Info1, Info2,
-		SInfo1, SInfo2),
+		{ list__length(Args, NumArgs) },
+		{ varset__new_vars(VarSet1, NumArgs, LambdaVars, VarSet2) },
+		{ map__init(Substitution) },
+		{ hlds_goal__true_goal(Head0) },
+		{ ArgContext = head(PredOrFunc, NumArgs) },
 
-	{ prepare_for_body(FinalSVarMap, VarSet2, VarSet3, SInfo2, SInfo3) },
+		insert_arg_unifications(LambdaVars, Args, Context, ArgContext,
+			no, Head0, VarSet2, Head, VarSet3, Info1, Info2,
+			SInfo2, SInfo3),
 
-	transform_goal(ParsedGoal, VarSet3, Substitution,
-		Body, VarSet, Info2, Info3, SInfo3, SInfo4),
+		{ prepare_for_body(FinalSVarMap, VarSet3, VarSet4,
+			SInfo3, SInfo4) },
 
-	{ finish_head_and_body(Context, FinalSVarMap, Head, Body, HLDS_Goal0,
-		SInfo4) },
+		transform_goal(ParsedGoal, VarSet4, Substitution,
+			Body, VarSet, Info2, Info3, SInfo4, 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) },
+		{ finish_head_and_body(Context, FinalSVarMap,
+			Head, Body, HLDS_Goal0, SInfo5) },
 
-	{ goal_info_init(Context, GoalInfo) },
-	{ HLDS_Goal = some(QuantifiedVars, can_remove, HLDS_Goal0) - GoalInfo },
+		%
+		% 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) },
 
-	%
-	% 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) }.
+		{ 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) }
+	).
 
 %-----------------------------------------------------------------------------%
 
@@ -8708,21 +8802,6 @@
 
 %------------------------------------------------------------------------------%
 
-% 	% Compute the svar_info for the following atomic conjunct.  We update
-% 	% the set of updated state variables, reset the set of locally updated
-% 	% state variables, make the new `!.' mappings match the old `!:'
-% 	% mappings and construct new `!:' mappings for those state variables
-% 	% that were updated.
-% 	%
-% :- func next_conj(svar_info) = svar_info.
-% 
-% next_conj(SInfo0) = SInfo :-
-% 	LocalUSVs0 = SInfo0 ^ locally_updated_svars,
-% 	USVs       = (SInfo0 ^ updated_svars) `union` LocalUSVs,
-% 	Dot        = SInfo0 ^ colon,
-% 
-%------------------------------------------------------------------------------%
-
 	% This synonym improves code legibility.
 	%
 :- type svar == prog_var.
@@ -8787,6 +8866,19 @@
 
 %------------------------------------------------------------------------------%
 
+	% 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.
@@ -8840,6 +8932,18 @@
 
 %------------------------------------------------------------------------------%
 
+	% 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.
@@ -8871,17 +8975,18 @@
 			VarSet = VarSet0,
 			SInfo  = SInfo0,
 			Name   = varset__lookup_name(VarSet0, StateVar),
-			prog_out__write_context(Context, IO0, IO1),
-		  	report_warning(string__format("\
-Error: reference to !:%s, no such state variable in scope.\n", [s(Name)]),
-				IO1, IO2),
 			( if SInfo0 ^ external_dot `contains` StateVar then
+				prog_out__write_context(Context, IO0, IO1),
+				report_warning(string__format("\
+Error: cannot use !:%s in this context;\n", [s(Name)]), IO1, IO2),
 				prog_out__write_context(Context, IO2, IO3),
 				report_warning(string__format("\
-       (although state variable !.%s is in scope.)\n", [s(Name)]),
-       					IO3, IO)
+       however !.%s may be used here.\n", [s(Name)]), IO3, IO)
 			  else
-			  	IO = IO2
+				prog_out__write_context(Context, IO0, IO1),
+				report_warning(string__format("\
+Error: state variable !:%s is not visible in this context.\n",
+				[s(Name)]), IO1, IO)
 			)
 		)
 	).
@@ -8919,7 +9024,20 @@
 	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 ).
+	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).
@@ -8933,18 +9051,25 @@
 
 %------------------------------------------------------------------------------%
 
-	% This is called either for a top-level clause or for a lambda.
-	% In the latter case, we need to make the current !.Xs external
+	% Prepare for the head of a new clause.
+	%
+:- pred prepare_for_head(svar_info).
+
+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_head(svar_info, svar_info).
-:- mode prepare_for_head(in, out) is det.
+:- pred prepare_for_lambda(svar_info, svar_info).
+:- mode prepare_for_lambda(in, out) is det.
 
-prepare_for_head(SInfo0, SInfo) :-
+prepare_for_lambda(SInfo0, SInfo) :-
 	SInfo = ( new_svar_info ^ external_dot := SInfo0 ^ dot ).
 
 %------------------------------------------------------------------------------%
@@ -9022,7 +9147,7 @@
 :- mode add_new_local_state_var(in, in, out, in, out) is det.
 
 add_new_local_state_var(StateVar, VarSet0, VarSet, SInfo0, SInfo) :-
-	new_local_state_var(StateVar, _, _, VarSet0, VarSet, SInfo0, SInfo).
+	new_colon_state_var(StateVar, _, VarSet0, VarSet, SInfo0, SInfo).
 
 %------------------------------------------------------------------------------%
 
@@ -9067,39 +9192,22 @@
 	%
 :- pred finish_if_then_else(prog_context,
 		hlds_goal, hlds_goal, hlds_goal, hlds_goal,
-		prog_varset, prog_varset, svar_info, svar_info, svar_info).
-:- mode finish_if_then_else(in, in, out, in, out, in, out, in, in, out) is det.
+		prog_varset, svar_info, svar_info, svar_info).
+:- mode finish_if_then_else(in, in, out, in, out, in, in, in, out) is det.
 
-finish_if_then_else(Context, Then0, Then, Else0, Else, VarSet0, VarSet,
+finish_if_then_else(Context, Then0, Then, Else0, Else, VarSet,
 		SInfoT, SInfoE, SInfo) :-
-	SInfo0       = SInfoT,
-	N            = int__max(SInfoT ^ num, SInfoE ^ num),
-	next_svar_info(N, VarSet0, VarSet, SInfo0, SInfo),
-
+	DisjSInfos = [{Then0, SInfoT}, {Else0, SInfoE}],
+	SInfo      = reconciled_disj_svar_info(VarSet, DisjSInfos),
+	StateVars  = map__keys(SInfoT ^ dot),
 	goal_info_init(Context, GoalInfo),
-
-	goal_to_conj_list(Then0, ThenGoals0),
-	ThenUnifiers = svar_unifiers(Context, SInfo ^ dot, SInfoT ^ dot),
-	conj_list_to_goal(ThenGoals0 ++ ThenUnifiers, GoalInfo, Then),
-
-	goal_to_conj_list(Else0, ElseGoals0),
-	ElseUnifiers = svar_unifiers(Context, SInfo ^ dot, SInfoE ^ dot),
-	conj_list_to_goal(ElseGoals0 ++ ElseUnifiers, GoalInfo, Else).
+	Then       = add_disj_unifiers(Context, GoalInfo, SInfo, StateVars,
+				{Then0, SInfoT}),
+	Else       = add_disj_unifiers(Context, GoalInfo, SInfo, StateVars,
+				{Else0, SInfoE}).
 
 %------------------------------------------------------------------------------%
 
-:- pred next_svar_info(int, prog_varset, prog_varset, svar_info, svar_info).
-:- mode next_svar_info(in, in, out, in, out) is det.
-
-next_svar_info(N, VarSet0, VarSet, SInfo0, SInfo) :-
-	StateVars = map__keys(SInfo0 ^ dot),
-	next_svar_mappings(N + 1, StateVars, VarSet0, VarSet1, Dot),
-	next_svar_mappings(N + 2, StateVars, VarSet1, VarSet,  Colon),
-	SInfo     = ((( SInfo0 ^ num   := N + 2 )
-			       ^ dot   := Dot   )
-			       ^ colon := Colon ).
-
-
 :- pred next_svar_mappings(int, svars, prog_varset, prog_varset, svar_map).
 :- mode next_svar_mappings(in, in, in, out, out) is det.
 
@@ -9123,68 +9231,165 @@
 	% so we construct new mappings for the state variables and then
 	% add unifiers from their pre-negated goal mappings.
 	%
-:- pred finish_negation(prog_context, hlds_goal, hlds_goal,
-		prog_varset, prog_varset, svar_info, svar_info, svar_info).
-:- mode finish_negation(in, in, out, in, out, in, in, out) is det.
-
-finish_negation(Context, Goal0, Goal, VarSet0, VarSet,
-		SInfoBefore, SInfoNeg, SInfo) :-
-	SInfo0    = SInfoBefore,
-	N         = SInfoNeg ^ num,
-	next_svar_info(N, VarSet0, VarSet, SInfo0, SInfo),
+:- pred finish_negation(svar_info, svar_info, svar_info).
+:- mode finish_negation(in, in, out) is det.
 
-	goal_info_init(Context, GoalInfo),
-
-	goal_to_conj_list(Goal0, Goals0),
-	Unifiers  = svar_unifiers(Context, SInfo ^ dot, SInfo0 ^ dot),
-	conj_list_to_goal(Goals0 ++ Unifiers, GoalInfo, Goal).
+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.
 	%
-:- pred finish_disjunction(prog_context, hlds_goal_svar_infos, hlds_goals,
-		prog_varset, prog_varset, svar_info).
-:- mode finish_disjunction(in, in, out, in, out, out) is det.
-
-finish_disjunction(_, [], _, _, _, _) :-
-	error("make_hlds__finish_disjunction: empty disjunct list").
-
-finish_disjunction(Context, DisjSInfos, Disjs, VarSet0, VarSet, SInfo) :-
-	DisjSInfos = [{_, SInfo0} | _],
-	N = list__foldl(
-		func({_, SI}, N0) = int__max(SI ^ num, N0),
-		DisjSInfos,
-		SInfo0 ^ num
-	    ),
-	next_svar_info(N, VarSet0, VarSet, SInfo0, SInfo),
-
+:- 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).
+
+
+:- 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 :-
+	Dots0   = set__sorted_list_to_set(map__keys(SInfo0 ^ dot)),
+	Colons0 = set__sorted_list_to_set(map__keys(SInfo0 ^ colon)),
+	Dots    = intersect_dot_svars(Dots0, DisjSInfos),
+	Colons  = intersect_colon_svars(Colons0, DisjSInfos),
+	SInfo   = list__foldl(
+			reconciled_svar_infos(VarSet, Dots, Colons),
+			DisjSInfos,
+			SInfo0
+		  ).
+
+
+:- func intersect_dot_svars(svar_set, hlds_goal_svar_infos) = svar_set.
+
+intersect_dot_svars(Dots, []                       ) = Dots.
+
+intersect_dot_svars(Dots, [{_, SInfo} | DisjSInfos]) =
+	intersect_dot_svars(
+		Dots `intersect`
+			set__sorted_list_to_set(map__keys(SInfo ^ dot)),
+		DisjSInfos
+	).
+
+
+:- func intersect_colon_svars(svar_set, hlds_goal_svar_infos) = svar_set.
+
+intersect_colon_svars(Colons, []                       ) = Colons.
+
+intersect_colon_svars(Colons, [{_, SInfo} | DisjSInfos]) =
+	intersect_colon_svars(
+		Colons `intersect`
+			set__sorted_list_to_set(map__keys(SInfo ^ colon)),
+		DisjSInfos
+	).
 
-	Disjs = list__map(
-			( func({G0, SI}) = G :-
-				goal_to_conj_list(G0, Gs0),
-				Us = svar_unifiers(Context,
-						SInfo ^ dot, SI ^ dot),
-				conj_list_to_goal(Gs0 ++ Us, GoalInfo, G)
-			),
-			DisjSInfos
-		).
+
+:- 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 :-
+	DotX = SInfoX ^ dot ^ det_elem(StateVar),
+	Dot0 = SInfo0 ^ dot ^ det_elem(StateVar),
+	compare(RDot, varset__lookup_name(VarSet, DotX) `with_type` string,
+		      varset__lookup_name(VarSet, Dot0) `with_type` string),
+	(
+		RDot  = (<),
+		SInfo = ( SInfo0 ^ dot ^ elem(StateVar) := Dot0 )
+	;
+		RDot  = (=),
+		SInfo = SInfo0
+	;
+		RDot  = (>),
+		SInfo = ( SInfo0 ^ dot ^ elem(StateVar) := DotX )
+	).
+
+
+:- func reconciled_svar_infos_colons(prog_varset, svar_info, svar, svar_info) =
+		svar_info.
+
+reconciled_svar_infos_colons(VarSet, SInfoX, StateVar, SInfo0) = SInfo :-
+	ColonX = SInfoX ^ colon ^ det_elem(StateVar),
+	Colon0 = SInfo0 ^ colon ^ det_elem(StateVar),
+	compare(RColon, varset__lookup_name(VarSet, ColonX) `with_type` string,
+		        varset__lookup_name(VarSet, Colon0) `with_type` string),
+	(
+		RColon = (<),
+		SInfo  = ( SInfo0 ^ colon ^ elem(StateVar) := Colon0 )
+	;
+		RColon = (=),
+		SInfo  = SInfo0
+	;
+		RColon = (>),
+		SInfo  = ( SInfo0 ^ colon ^ elem(StateVar) := ColonX )
+	).
+
+
+:- 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(prog_context, hlds_goal, hlds_goal,
-		prog_varset, prog_varset, svar_info, svar_info, svar_info).
-:- mode finish_equivalence(in, in, out, in, out, in, in, out) is det.
-
-finish_equivalence(Context, Goal0, Goal, VarSet0, VarSet,
-		SInfoBefore, SInfoEqv, SInfo) :-
-	finish_negation(Context, Goal0, Goal, VarSet0, VarSet,
-		SInfoBefore, SInfoEqv, SInfo).
+:- 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).
 
 %------------------------------------------------------------------------------%
 
@@ -9210,6 +9415,10 @@
 	% "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.
 
@@ -9343,24 +9552,91 @@
 
 %------------------------------------------------------------------------------%
 
-:- func expand_dot_colon_state_var_args(list(prog_term)) = list(prog_term).
+:- func expand_bang_state_var_args(list(prog_term)) = list(prog_term).
 
-expand_dot_colon_state_var_args(Args0) =
-	list__foldr(expand_dot_colon_state_var, Args0, []).
+expand_bang_state_var_args(Args0) =
+	list__foldr(expand_bang_state_var, Args0, []).
 
 
-:- func expand_dot_colon_state_var(prog_term, list(prog_term)) =
+:- func expand_bang_state_var(prog_term, list(prog_term)) =
 		list(prog_term).
 
-expand_dot_colon_state_var(T @ variable(_), Ts) = [T | Ts].
+expand_bang_state_var(T @ variable(_), Ts) = [T | Ts].
 
-expand_dot_colon_state_var(T @ functor(Const, Args, Ctxt), Ts) =
-	( if Const = atom("!"), Args = [variable(_SVar)] then
+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 ]
+	).
+
+%------------------------------------------------------------------------------%
+
+:- 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), prog_var).
+:- 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)).
+
+%------------------------------------------------------------------------------%
+
+:- 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_warning(string__format("\
+Warning: !%s cannot be a function result.\n", [s(Name)])),
+	globals__io_lookup_bool_option(verbose_errors, Verbose),
+	(
+		{ Verbose = yes },
+		prog_out__write_context(Context),
+		report_warning(string__format("\
+         You probably meant !.%s or !:%s.\n", [s(Name), s(Name)]))
+	;
+		{ Verbose = no }
 	).
 
 %------------------------------------------------------------------------------%
--------------------------------------------------------------------------
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