[m-rev.] for post-commit review: from_ground_term_initial improvements

Zoltan Somogyi zs at unimelb.edu.au
Mon Apr 16 18:15:33 AEST 2012


I am committing this now because I am working on other changes that
build on this diff. It passes bootcheck clean with several different
options.

Zoltan.

The post-typecheck phase (which is executed during the purity checking pass)
sometimes discovers that the code in a from_ground_term_initial scope
does not construct a ground term: that some part of what it constructs
is a higher order value. If the phase is repeated, this can also happen
for from_ground_term_construct scopes.

The polymorphism pass sometimes discovers that it needs to modify the contents
of a from_ground_term_initial scope.

In both cases, the transformed contents of the scope no longer obey the
invariants expected of it, and therefore the scope must either be turned
into a from_ground_term_other scope, or deleted. This loses all efficiency
advantages of the from_ground_term_{initial,construct} scope (fgt{i,c} scopes
for short) for ALL the old scope's conjuncts, even though some subsequences
of those conjuncts still obey the required invariants. This diff wraps such
subsequences in fgt{i,c} scopes; whichever is asked for. When it does this,
the original outer from_ground_term scope does not confer any benefit on
top of the the benefits conferred by the inner scopes. Instead of turning it
into a from_ground_term_other scope, as we used to do, we now simply delete it.

The code that does this rewrapping requires the old contents of the scope
to obey every detail of the required invariants. The scopes we used
to construct sometimes broke these invariants. Specifically, we used to assume
that the unraveling of every unification of the form "X = ground_term"
satisfied those invariants, but this is not true if ground_term contains
lambda definitions or field access operations. This diff therefore also
completely reworks the mechanism we use to build fgti scopes in the
first place.

We used to do this by testing on the way down a term whether a term was ground.
This is not only wrong (for the reason given above), it is also a potential
performance problem, since it requires the scan of each part of a potentially
large term to be repeated up to N times, where N is the number of function
symbols above it in the outermost term. For lists, where the Nth element
has N-1 cons function symbols on top of it, this testing requires O(N^2) time.

Superhomogeneous.m now makes decisions on when to insert fgti scopes
on the way up. When it unravels a unification, it does not directly return
the goal resulting from the expansion. Instead, it returns a data structure
(of the new type "expansion") that records not just information from which
that goal can be constructed if needed, but also the information needed
to decide whether (a) we CAN wrap a fgt{i,c} scope around that goal, and (b)
even if we can, whether we WANT to. Then, when we come to a point where
we cannot keep doing this, either because we have come back up to the top
of the term, or because we have come back up to a point in the original term
where the translation of the current function symbol does not obey the
fgt{i,c} invariants (which can happen e.g. because the current function symbol
represents a lambda expression or a field access or field update), we can
create scopes for the arguments for which this is both possible and desirable.
The data structure we use for this has some overhead, but the old code had
similar overhead, mostly in the form of repeated conversions of the results
of unification unraveling between two types: a single goal (probably a
conjunction), and a list of goals. It also used to do appends on lists;
the new code does appends on cords, which has much better worst case behavior.

This diff speeds up the compiler on x0.m, a particular cut-down version of
the rcpsp_cpx_bug test case by about a factor of two: from about 14 seconds
to less than 7 seconds. On tools/speedtest, there is a very small slowdown,
but it is in the noise.

compiler/from_ground_term_util.m:
	A new module containing utility types and predicates that are useful
	when compiler modules process from_ground_term scopes.

compiler/hlds.m:
	Add the new module to this package.

compiler/notes/compiler_design.html:
	Document the new module.

compiler/polymorphism.m:
compiler/purity.m:
	Make the change described above.

	In purity.m, change some predicate interfaces to make it clear
	that some predicates do not update the purity_info.

compiler/post_typecheck.m:
	Put the order of the parameters of a predicate in a more standard fix.

compiler/superhomogeneous.m:
	Make the change described above.
	
	Amongst other things, this means we stop threading !NumAdded
	through most of the predicates in this module.

	We also no longer need separate insert_arg_unifications and
	append_arg_unifications predicates: a single parameterized predicate
	can do the job of both.

	In the common case of unraveling a term, we used to create a list of
	variables to match a list of terms, and then iterate through both the
	list of terms and the list of variables, always looking for a mismatch
	in list lengths. We now create each variable in the list just as we
	process the corresponding term, which avoids some redundant tests.

	In the same common case of unraveling a term, we used to create terms
	containing variables just so we could give them to a general purpose
	predicate that could unify all four combinations of the LHS and RHS
	being var and functor. We now call a specialized predicate that
	KNOWS the LHS is a variable.

	Eliminate the double expansion of state variable references
	in some more situations.

	Adopt a significantly more consistent naming convention for variables.

	Give some predicates more accurate names.

	Remove some unneeded predicates, some of which were also unneeded
	before this diff.

compiler/add_clause.m:
compiler/field_access.m:
compiler/goal_expr_to_goal.m:
	Conform to the changes in superhomogeneous.m. Mostly this means
	not threading through !NumAdded, since the goals build by these modules
	do not obey the fgt{i,c} invariants.

	In goal_expr_to_goal.m, add a missing test for a semantic error.
	For unifications of the form !S = !T, we used to report an error
	only for the LHS; we now report an error for both sides.

compiler/format_call.m:
	Fix an old bug. We used to ignore from_ground_term_initial scopes,
	thinking them irrelevant, but since they can build part of the
	list of values being printed, we may need to process them.
	We now process such scopes if and only if we need to.

compiler/hlds_goal.m:
	Fix a comment.

compiler/qual_info.m:
	Fix white space.

cvs diff: Diffing .
Index: add_clause.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/add_clause.m,v
retrieving revision 1.69
diff -u -b -r1.69 add_clause.m
--- add_clause.m	26 Mar 2012 00:43:32 -0000	1.69
+++ add_clause.m	15 Apr 2012 14:25:37 -0000
@@ -584,7 +584,7 @@
             ArgContext = ac_head(PredOrFunc, Arity),
             HeadGoal0 = true_goal,
             insert_arg_unifications(HeadVarList, Args, Context, ArgContext,
-                HeadGoal0, HeadGoal1, 0, _, !SVarState, !SVarStore, !VarSet,
+                HeadGoal0, HeadGoal1, !SVarState, !SVarStore, !VarSet,
                 !ModuleInfo, !QualInfo, !Specs),
             % The only pass that pays attention to the from_head feature,
             % switch_detection, only does so on kinds of hlds_goal_exprs
@@ -602,7 +602,7 @@
                 do_not_attach_in_from_ground_term, HeadGoal1, HeadGoal)
         ),
         transform_goal_expr_context_to_goal(loc_whole_goal, ParseBody,
-            Renaming, BodyGoal, _, !SVarState, !SVarStore, !VarSet,
+            Renaming, BodyGoal, !SVarState, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs),
 
         trace [compiletime(flag("debug-statevar-lambda")), io(!IO)] (
Index: field_access.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/field_access.m,v
retrieving revision 1.22
diff -u -b -r1.22 field_access.m
--- field_access.m	26 Mar 2012 00:43:32 -0000	1.22
+++ field_access.m	16 Apr 2012 03:48:27 -0000
@@ -19,7 +19,6 @@
 :- import_module hlds.hlds_module.
 :- import_module hlds.make_hlds.qual_info.
 :- import_module hlds.make_hlds.state_var.
-:- import_module hlds.make_hlds.superhomogeneous.
 :- import_module parse_tree.error_util.
 :- import_module parse_tree.prog_data.
 :- import_module parse_tree.prog_io_util.
@@ -46,7 +45,6 @@
     unify_main_context::in, unify_sub_contexts::in, field_list::in,
     prog_var::in, prog_var::in, prog_var::in, cons_id::out,
     pair(cons_id, unify_sub_contexts)::out, hlds_goal::out,
-    num_added_goals::in, num_added_goals::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out,
     module_info::in, module_info::out, qual_info::in, qual_info::out,
@@ -68,7 +66,6 @@
     unify_main_context::in, unify_sub_contexts::in, field_list::in,
     prog_var::in, prog_var::in, prog_var::in, cons_id::out,
     pair(cons_id, unify_sub_contexts)::out, hlds_goal::out,
-    num_added_goals::in, num_added_goals::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out,
     module_info::in, module_info::out, qual_info::in, qual_info::out,
@@ -87,8 +84,7 @@
 :- pred expand_get_field_function_call(prog_context::in,
     unify_main_context::in, unify_sub_contexts::in, field_list::in,
     prog_var::in, prog_var::in, purity::in, cons_id::out,
-    pair(cons_id, unify_sub_contexts)::out,
-    hlds_goal::out, num_added_goals::in, num_added_goals::out,
+    pair(cons_id, unify_sub_contexts)::out, hlds_goal::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out,
     module_info::in, module_info::out, qual_info::in, qual_info::out,
@@ -121,11 +117,11 @@
 
 expand_set_field_function_call(Context, MainContext, SubContext0, FieldNames,
         FieldValueVar, TermInputVar, TermOutputVar, Functor, FieldSubContext,
-        Goal, !NumAdded, !SVarState, !SVarStore, !VarSet,
+        Goal, !SVarState, !SVarStore, !VarSet,
         !ModuleInfo, !QualInfo, !Specs) :-
     expand_set_field_function_call_2(Context, MainContext, SubContext0,
         FieldNames, FieldValueVar, TermInputVar, TermOutputVar, Functor,
-        FieldSubContext, Goals, !NumAdded,
+        FieldSubContext, Goals,
         !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
     goal_info_init(Context, GoalInfo),
     conj_list_to_goal(Goals, GoalInfo, Goal).
@@ -134,21 +130,20 @@
     unify_main_context::in, unify_sub_contexts::in, field_list::in,
     prog_var::in, prog_var::in, prog_var::in, cons_id::out,
     pair(cons_id, unify_sub_contexts)::out, list(hlds_goal)::out,
-    num_added_goals::in, num_added_goals::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out,
     module_info::in, module_info::out, qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-expand_set_field_function_call_2(_, _, _, [], _, _, _, _, _, _, !NumAdded,
+expand_set_field_function_call_2(_, _, _, [], _, _, _, _, _, _,
         !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
     unexpected($module, $pred, "empty list of field names").
 expand_set_field_function_call_2(Context, MainContext, SubContext0,
         [FieldName - FieldArgs | FieldNames], FieldValueVar,
         TermInputVar, TermOutputVar, Functor, FieldSubContext, Goals,
-        !NumAdded, !SVarState, !SVarStore, !VarSet,
-        !ModuleInfo, !QualInfo, !Specs) :-
-    make_fresh_arg_vars(FieldArgs, FieldArgVars, !VarSet, !SVarState, !Specs),
+        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
+    make_fresh_arg_vars_subst_svars(FieldArgs, FieldArgVars, !VarSet,
+        !SVarState, !Specs),
     (
         FieldNames = [_ | _],
         varset.new_var(SubTermInputVar, !VarSet),
@@ -157,14 +152,12 @@
         construct_field_access_function_call(set, Context,
             MainContext, SubContext0, FieldName, TermOutputVar,
             SetArgs, purity_pure, Functor, UpdateGoal, !QualInfo),
-        !:NumAdded = !.NumAdded + 1,
 
         % Extract the field containing the field to update.
         construct_field_access_function_call(get, Context,
             MainContext, SubContext0, FieldName, SubTermInputVar,
             FieldArgVars ++ [TermInputVar], purity_pure, _, GetSubFieldGoal,
             !QualInfo),
-        !:NumAdded = !.NumAdded + 1,
 
         % Recursively update the field.
         SubTermInputArgNumber = 2 + list.length(FieldArgs),
@@ -172,7 +165,7 @@
         SubContext = [TermInputContext | SubContext0],
         expand_set_field_function_call_2(Context, MainContext,
             SubContext, FieldNames, FieldValueVar, SubTermInputVar,
-            SubTermOutputVar, _, FieldSubContext, Goals0, !NumAdded,
+            SubTermOutputVar, _, FieldSubContext, Goals0,
             !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
 
         Goals1 = [GetSubFieldGoal | Goals0] ++ [UpdateGoal]
@@ -182,7 +175,6 @@
         construct_field_access_function_call(set, Context,
             MainContext, SubContext0, FieldName, TermOutputVar,
             SetArgs, purity_pure, Functor, Goal, !QualInfo),
-        !:NumAdded = !.NumAdded + 1,
         FieldSubContext = Functor - SubContext0,
         Goals1 = [Goal]
     ),
@@ -190,23 +182,22 @@
     goal_info_init(Context, GoalInfo),
     conj_list_to_goal(Goals1, GoalInfo, Conj0),
     insert_arg_unifications(FieldArgVars, FieldArgs, Context, ArgContext,
-        Conj0, Conj, !NumAdded, !SVarState, !SVarStore, !VarSet,
+        Conj0, Conj, !SVarState, !SVarStore, !VarSet,
         !ModuleInfo, !QualInfo, !Specs),
     svar_goal_to_conj_list(Conj, Goals, !SVarStore).
 
 expand_dcg_field_extraction_goal(Context, MainContext, SubContext, FieldNames,
         FieldValueVar, TermInputVar, TermOutputVar, Functor, FieldSubContext,
-        Goal, !NumAdded, !SVarState, !SVarStore, !VarSet,
+        Goal, !SVarState, !SVarStore, !VarSet,
         !ModuleInfo, !QualInfo, !Specs) :-
     % Unify the DCG input and output variables.
     make_atomic_unification(TermOutputVar, rhs_var(TermInputVar), Context,
         MainContext, SubContext, UnifyDCG, !QualInfo),
-    !:NumAdded = !.NumAdded + 1,
 
     % Process the access function as a get function on the output DCG variable.
     expand_get_field_function_call_2(Context, MainContext, SubContext,
         FieldNames, FieldValueVar, TermOutputVar, purity_pure,
-        Functor, FieldSubContext, Goals1, !NumAdded,
+        Functor, FieldSubContext, Goals1,
         !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
     Goals = [UnifyDCG | Goals1],
     goal_info_init(Context, GoalInfo),
@@ -214,11 +205,11 @@
 
 expand_get_field_function_call(Context, MainContext, SubContext0, FieldNames,
         FieldValueVar, TermInputVar, Purity, Functor, FieldSubContext,
-        Goal, !NumAdded, !SVarState, !SVarStore, !VarSet,
+        Goal, !SVarState, !SVarStore, !VarSet,
         !ModuleInfo, !QualInfo, !Specs) :-
     expand_get_field_function_call_2(Context, MainContext, SubContext0,
         FieldNames, FieldValueVar, TermInputVar, Purity, Functor,
-        FieldSubContext, Goals, !NumAdded, !SVarState, !SVarStore, !VarSet,
+        FieldSubContext, Goals, !SVarState, !SVarStore, !VarSet,
         !ModuleInfo, !QualInfo, !Specs),
     goal_info_init(Context, GoalInfo),
     conj_list_to_goal(Goals, GoalInfo, Goal).
@@ -227,20 +218,20 @@
     unify_main_context::in, unify_sub_contexts::in, field_list::in,
     prog_var::in, prog_var::in, purity::in, cons_id::out,
     pair(cons_id, unify_sub_contexts)::out, list(hlds_goal)::out,
-    num_added_goals::in, num_added_goals::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out,
     module_info::in, module_info::out, qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-expand_get_field_function_call_2(_, _, _, [], _, _, _, _, _, _, !NumAdded,
+expand_get_field_function_call_2(_, _, _, [], _, _, _, _, _, _,
         !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
     unexpected($module, $pred, "empty list of field names").
 expand_get_field_function_call_2(Context, MainContext, SubContext0,
         [FieldName - FieldArgs | FieldNames], FieldValueVar, TermInputVar,
-        Purity, Functor, FieldSubContext, Goals, !NumAdded,
+        Purity, Functor, FieldSubContext, Goals,
         !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
-    make_fresh_arg_vars(FieldArgs, FieldArgVars, !VarSet, !SVarState, !Specs),
+    make_fresh_arg_vars_subst_svars(FieldArgs, FieldArgVars, !VarSet,
+        !SVarState, !Specs),
     GetArgVars = FieldArgVars ++ [TermInputVar],
     (
         FieldNames = [_ | _],
@@ -248,7 +239,6 @@
         construct_field_access_function_call(get, Context, MainContext,
             SubContext0, FieldName, SubTermInputVar, GetArgVars, Purity,
             Functor, Goal, !QualInfo),
-        !:NumAdded = !.NumAdded + 1,
 
         % Recursively extract until we run out of field names.
         TermInputArgNumber = 1 + list.length(FieldArgVars),
@@ -256,7 +246,7 @@
         SubContext = [TermInputContext | SubContext0],
         expand_get_field_function_call_2(Context, MainContext,
             SubContext, FieldNames, FieldValueVar, SubTermInputVar, Purity,
-            _, FieldSubContext, Goals1, !NumAdded, !SVarState, !SVarStore,
+            _, FieldSubContext, Goals1, !SVarState, !SVarStore,
             !VarSet, !ModuleInfo, !QualInfo, !Specs),
         Goals2 = [Goal | Goals1]
     ;
@@ -265,14 +255,13 @@
         construct_field_access_function_call(get, Context,
             MainContext, SubContext0, FieldName, FieldValueVar,
             GetArgVars, Purity, Functor, Goal, !QualInfo),
-        Goals2 = [Goal],
-        !:NumAdded = !.NumAdded + 1
+        Goals2 = [Goal]
     ),
     ArgContext = ac_functor(Functor, MainContext, SubContext0),
     goal_info_init(Context, GoalInfo),
     conj_list_to_goal(Goals2, GoalInfo, Conj0),
     insert_arg_unifications(FieldArgVars, FieldArgs, Context, ArgContext,
-        Conj0, Conj, !NumAdded, !SVarState, !SVarStore, !VarSet,
+        Conj0, Conj, !SVarState, !SVarStore, !VarSet,
         !ModuleInfo, !QualInfo, !Specs),
     svar_goal_to_conj_list(Conj, Goals, !SVarStore).
 
Index: format_call.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/format_call.m,v
retrieving revision 1.29
diff -u -b -r1.29 format_call.m
--- format_call.m	13 Feb 2012 00:11:38 -0000	1.29
+++ format_call.m	15 Apr 2012 17:06:49 -0000
@@ -9,13 +9,18 @@
 % File: format_call.m.
 % Author: zs.
 %
-% This module has two related jobs. The first job is to generate warnings
-% about calls to string.format, io.format and stream.string_writer.format
-% in which the format string and the supplied lists of values do not agree.
+% This module has two related jobs.
+%
+% - The first job is to generate warnings about calls to string.format,
+%   io.format and stream.string_writer.format in which the format string
+%   and the supplied lists of values do not agree.
+%
 % The difficult part of this job is actually finding the values of the
-% variables representing the format string and the list of values to be printed.
-% The second job is to try to transform well formed calls into code that
-% interprets the format string at compile time, rather than runtime.
+%   variables representing the format string and the list of values to be
+%   printed.
+%
+% - The second job is to try to transform well formed calls into code
+%   that interprets the format string at compile time, rather than runtime.
 % 
 % Our general approach to the first job is a backwards traversal of the
 % procedure body. During this traversal, we assign an id to every conjunction
@@ -652,12 +657,19 @@
         map.det_insert(SubGoalId, CurId, !PredMap)
     ;
         GoalExpr = scope(Reason, SubGoal),
-        ( Reason = from_ground_term(_, from_ground_term_construct) ->
+        (
+            Reason = from_ground_term(TermVar, from_ground_term_construct),
             % These scopes cannot build the format string (since that is
-            % a single constant, from which we don't build such scopes),
-            % or the list of things to print (since that term won't be a ground
-            % term except in degenerate cases). These scopes also cannot call
-            % anything.
+            % either a single constant, or the result of an operation on
+            % strings, neither of which are things for which we build fgt
+            % scopes. It can build the term to print, but that will happen
+            % only in degenerate cases. However, we do have some degenerate 
+            % cases in the test suite.
+            not set_of_var.member(!.RelevantVars, TermVar)
+        ->
+            % It is ok not to traverse the subgoal. The scope cannot contain
+            % any calls, and the unifications it does contain are apparently
+            % not of interest to any later formal call.
             true
         ;
             format_call_traverse_conj(ModuleInfo, [SubGoal], CurId,
@@ -992,14 +1004,18 @@
         Goal = hlds_goal(GoalExpr, GoalInfo)
     ;
         GoalExpr0 = scope(Reason, SubGoal0),
-        ( Reason = from_ground_term(_, from_ground_term_construct) ->
-            % We did not traverse such scopes in format_call_traverse_conj,
-            % so there are no goals for us to transform in SubGoal0.
-            % There is not even any variable consumption for us to record,
-            % or any variable production for us to eliminate (since the things
-            % being printed out by format calls are all of atomic types,
-            % and these scopes can produce only values of non-atomic types).
-            Goal = Goal0
+        (
+            Reason = from_ground_term(TermVar, from_ground_term_construct),
+            not set_of_var.member(!.NeededVars, TermVar),
+            % If this succeeds, then the backward traversal cannot encounter
+            % any more producers of LHSVar.
+            set_of_var.remove(TermVar, !ToDeleteVars)
+        ->
+            % We cannot guarantee that the modified version of SubGoal0
+            % meets the invariants required of a goal in a
+            % from_ground_term_construct scope, so we remove the scope.
+            opt_format_call_sites_in_goal(SubGoal0, Goal,
+                !GoalIdMap, !NeededVars, !ToDeleteVars)
         ;
             opt_format_call_sites_in_goal(SubGoal0, SubGoal,
                 !GoalIdMap, !NeededVars, !ToDeleteVars),
Index: from_ground_term_util.m
===================================================================
RCS file: from_ground_term_util.m
diff -N from_ground_term_util.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ from_ground_term_util.m	16 Apr 2012 05:35:09 -0000
@@ -0,0 +1,365 @@
+%-----------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et
+%-----------------------------------------------------------------------------%
+% Copyright (C) 2012 The University of Melbourne.
+% This file may only be copied under the terms of the GNU General
+% Public License - see the file COPYING in the Mercury distribution.
+%-----------------------------------------------------------------------------%
+%
+% File: from_ground_term_util.m.
+% Author: zs.
+%
+% This module provides utility types and predicates that are useful
+% when compiler modules process from_ground_term scopes.
+%
+% Specifically, the contents of this module are designed
+% to help test whether after a program transformation,
+% a from_ground_term_{initial,construct} scope goal can still remain
+% a from_ground_term scope of the same kind, and if not, to wrap smaller
+% from_ground_term_{initial,construct} scopes around subsequences of the
+% original conjuncts whereever the status of the invariants permit it.
+%
+
+:- module hlds.from_ground_term_util.
+:- interface.
+
+:- import_module hlds.hlds_goal.
+:- import_module parse_tree.
+:- import_module parse_tree.prog_data.
+
+:- import_module list.
+:- import_module map.
+
+%-----------------------------------------------------------------------------%
+
+    % Describe whether a goal or sequence of goals inside a from_ground_term
+    % scope of the initial or construct kind still obeys the invariants
+    % required of such scopes after a program transformation.
+    %
+:- type fgt_invariants_status
+    --->    fgt_invariants_kept
+    ;       fgt_invariants_broken.
+
+    % A conjunct inside a from_ground_term_{initial,construct} scope must be
+    % a unification of the form X = f(Y1, ..., Yn). The X is constructed
+    % by this unification and by the goals that construct the Yi.
+    %
+    % Values of this type record both the relevant information about the input
+    % of a program transformation that operates on such conjuncts (the second
+    % and third fields of each functor), the result of the transformation
+    % (the first field of each functor) and whether the transformation
+    % breaks the scope's invariants (the functor itself).
+    %
+:- type fgt_marked_goal
+    --->    fgt_kept_goal(
+                % Either the original goal, or a version that is transformed
+                % in a way that keeps the from_ground_term_{initial,construct}
+                % invariants.
+                hlds_goal,
+
+                % The variable from the lhs of the original unification (X).
+                prog_var,
+
+                % The variables from the rhs of the original unification (Yi).
+                list(prog_var)
+            )
+    ;       fgt_broken_goal(
+                % A version of the original goal that is transformed
+                % in a way that breaks some of the
+                % from_ground_term_{initial,construct} invariants.
+                hlds_goal,
+
+                % The variable from the lhs of the original unification (X).
+                prog_var,
+
+                % The variables from the rhs of the original unification (Yi).
+                list(prog_var)
+            ).
+
+    % Return the goal from a goal marked as kept. Abort if the goal is marked
+    % as broken.
+    %
+:- pred project_kept_goal(fgt_marked_goal::in, hlds_goal::out) is det.
+
+    % A value of type fgt_build_info maps a variable to the code needed
+    % to build it, and to some other information that is of interest
+    % only to this module.
+    %
+:- type fgt_build_info.
+:- type fgt_build_info_map == map(prog_var, fgt_build_info).
+
+:- type goal_order
+    --->    construct_bottom_up
+    ;       deconstruct_top_down.
+
+    % introduce_partial_fgt_scopes(GoalInfo0, SubGoalInfo0, RevMarkedSubGoals,
+    %   Kind, SubGoal):
+    %
+    % Thes input to this predicate are:
+    %
+    % - The original goal infos for a fgt{i,c} goal and for its subgoal
+    %   (GoalInfo0 and SubGoalInfo0).
+    %
+    % - A list (MarkedSubGoals) of the transformed versions of the conjuncts
+    %   that were originally in that scope, in bottom up (construct) order,
+    %   marked up in the way required by the comment on the definition of the
+    %   fgt_marked_goal type). This predicate assumes that this list contains
+    %   some violations of the fgt{i,c} invariants (other than the order
+    %   invariant for initial scopes); if it doesn't, then the the WHOLE
+    %   conjunction can have a fgt{i,c} scope wrapped around it, using code
+    %   much simpler than what is in this predicate.
+    %
+    % - The order into which the goals should be put (Order).
+    %
+    % The SubGoal returned by this predicate will contain the code in the
+    % MarkedSubGoals in the desired order, but with any sequence of goals that
+    % does obey the fgt{i,c} invariants will be wrapped in a fgt scope;
+    % initial if Order = deconstruct_top_down, construct if Order =
+    % construct_bottom_up.
+    %
+    % This allows us to preserve the effect of the compiler optimizations of
+    % fgt{i,c} scopes for as large a portion of the original scope as possible.
+    %
+:- pred introduce_partial_fgt_scopes(hlds_goal_info::in, hlds_goal_info::in,
+    list(fgt_marked_goal)::in, goal_order::in, hlds_goal::out)
+    is det.
+
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module hlds.goal_util.
+:- import_module libs.globals.
+:- import_module parse_tree.set_of_var.
+
+:- import_module cord.
+:- import_module int.
+:- import_module maybe.
+:- import_module require.
+
+%-----------------------------------------------------------------------------%
+
+    % Has a goal or sequence of goals broken the fgt{i,c} invariants?
+    %
+:- type maybe_kept
+    --->    kept
+    ;       broken.
+
+    % Has a goal kept the fgt{i,c} invariants?
+    %
+:- type maybe_kept_goal_info
+    --->    kept_old_gi(
+                % Yes. But if its parent or one of its siblings has not,
+                % then we want to wrap it in an fgt scope if it is big
+                % enough (which is why we record the size of the goal,
+                % as a count of the unifications in it). The wrapping process
+                % needs the goal info of the unification that puts
+                % the top function symbol of the ground term in place.
+                mkgi_size           :: int,
+                mkgi_old_goal_info  :: hlds_goal_info
+            )
+    ;       broken_no_gi.
+            % No, the goal has not kept the fgt{i,c} invariants.
+
+    % The code needed to build a variable, and whether it breaks the fgt{i,c}
+    % invariants.
+    %
+:- type fgt_build_info
+    --->    fgt_build_info(
+                maybe_kept_goal_info,
+                cord(hlds_goal)
+            ).
+
+%-----------------------------------------------------------------------------%
+
+introduce_partial_fgt_scopes(GoalInfo0, SubGoalInfo0, RevMarkedSubGoals,
+        Order, SubGoal) :-
+    introduce_partial_fgt_scopes_loop(RevMarkedSubGoals, Order,
+        map.init, BuildInfoMap),
+    map.values(BuildInfoMap, BuildInfos),
+    list.map(project_build_info_goal_cord, BuildInfos, BuildGoalCords),
+    BuildGoalCord = cord_list_to_cord(BuildGoalCords),
+    BuildGoals = cord.list(BuildGoalCord),
+    (
+        BuildGoals = [],
+        unexpected($module, $pred, "BuildGoals = []")
+    ;
+        BuildGoals = [SubGoal1]
+    ;
+        BuildGoals = [_, _ | _],
+        SubGoalExpr1 = conj(plain_conj, BuildGoals),
+        SubGoal1 = hlds_goal(SubGoalExpr1, SubGoalInfo0)
+    ),
+    ( goal_info_has_feature(GoalInfo0, feature_from_head) ->
+        attach_features_to_all_goals([feature_from_head],
+            attach_in_from_ground_term, SubGoal1, SubGoal)
+    ;
+        SubGoal = SubGoal1
+    ).
+
+    % The main input to this predicate is a list of the goals in an fgt{i,c}
+    % scope, as transformed and marked up by a compiler pass.
+    % All the original goals were of the form X = f(Y1, ..., Yn), and
+    % the list is in reverse order, so that the code constructing the Yi
+    % precedes the code constructing X. Each of the Yi will have appeared
+    % exactly twice in the original goal sequence: once when constructed,
+    % and once when used.
+    %
+    % Process this sequence by creating an entry for a variable in
+    % !BuildInfoMap when it is constructed, and removing it when it is used.
+    % At the end, the final BuildInfoMap should contain exactly one entry,
+    % for the variable that the fgt scope is for.
+    %
+    % Each entry gives the code sequence required to build the variable
+    % and all its components, and says whether that code obeys the required
+    % fgt{i,c} invariants. In process of building the code for an X that
+    % breaks these invariants, we wrap fgt{i,c} scopes around the code
+    % subsequences that construct any of the Yi that keep those invariants.
+    %
+:- pred introduce_partial_fgt_scopes_loop(list(fgt_marked_goal)::in,
+    goal_order::in, fgt_build_info_map::in, fgt_build_info_map::out) is det.
+
+introduce_partial_fgt_scopes_loop([], _Order, !BuildInfoMap).
+introduce_partial_fgt_scopes_loop([RevMarkedGoal | RevMarkedGoals], Order,
+        !BuildInfoMap) :-
+    (
+        RevMarkedGoal = fgt_kept_goal(Goal, Var, ArgVars),
+        SavedBuildInfoMap = !.BuildInfoMap,
+        lookup_and_remove_arg_vars(ArgVars, cord.init, ArgsGoalCord0,
+            kept, Kept, 0, TotalArgSize, !BuildInfoMap),
+        (
+            Kept = kept,
+            ArgsGoalCord = ArgsGoalCord0,
+            Goal = hlds_goal(_, OldGoalInfo),
+            TotalSize = TotalArgSize + 1,
+            KeptGI = kept_old_gi(TotalSize, OldGoalInfo)
+        ;
+            Kept = broken,
+            !:BuildInfoMap = SavedBuildInfoMap,
+            lookup_and_remove_arg_vars_insert_fgt(ArgVars, Order,
+                cord.init, ArgsGoalCord, !BuildInfoMap),
+            KeptGI = broken_no_gi
+        )
+    ;
+        RevMarkedGoal = fgt_broken_goal(Goal, Var, ArgVars),
+        lookup_and_remove_arg_vars_insert_fgt(ArgVars, Order,
+            cord.init, ArgsGoalCord, !BuildInfoMap),
+        KeptGI = broken_no_gi
+    ),
+    (
+        Order = construct_bottom_up,
+        GoalCord = cord.snoc(ArgsGoalCord, Goal)
+    ;
+        Order = deconstruct_top_down,
+        GoalCord = cord.cons(Goal, ArgsGoalCord)
+    ),
+    VarBuildInfo = fgt_build_info(KeptGI, GoalCord),
+    map.det_insert(Var, VarBuildInfo, !BuildInfoMap),
+    introduce_partial_fgt_scopes_loop(RevMarkedGoals, Order, !BuildInfoMap).
+
+    % Loop over all the Yi in a unification of the form X = f(Y1, ..., Yn),
+    % and report the goal cord needed to build all the Yi (!:GoalCord),
+    % whether all parts of that code keep the fgt{i,c} invariants (!:Kept).
+    % In the process, remove all the Yi from !:BuildInfoMap, since they
+    % should never appear in the reverse goal sequence again.
+    %
+:- pred lookup_and_remove_arg_vars(list(prog_var)::in,
+    cord(hlds_goal)::in, cord(hlds_goal)::out,
+    maybe_kept::in, maybe_kept::out, int::in, int::out,
+    fgt_build_info_map::in, fgt_build_info_map::out) is det.
+
+lookup_and_remove_arg_vars([], !GoalCord, !Kept, !TotalSize, !BuildInfoMap).
+lookup_and_remove_arg_vars([Var | Vars], !GoalCord, !Kept, !TotalSize,
+        !BuildInfoMap) :-
+    map.det_remove(Var, BuildInfo, !BuildInfoMap),
+    BuildInfo = fgt_build_info(VarKept, VarGoalCord),
+    (
+        VarKept = kept_old_gi(Size, _),
+        !:TotalSize = !.TotalSize + Size
+    ;
+        VarKept = broken_no_gi,
+        % The final TotalSize won't be consulted, so it is OK not to
+        % update it here.
+        !:Kept = broken
+    ),
+    !:GoalCord = !.GoalCord ++ VarGoalCord,
+    lookup_and_remove_arg_vars(Vars, !GoalCord, !Kept, !TotalSize,
+        !BuildInfoMap).
+
+    % Loop over all the Yi in a unification of the form X = f(Y1, ..., Yn).
+    % We know that either the code that builds the top functor of X or
+    % the code that builds one or more of the Yi breaks the fgt{i,c}
+    % invariants, so wrap the codes that build the OTHER Yi in fgt{i,c}
+    % scopes. Return the code needed to build all Yi (in !:GoalCord).
+    % In the process, remove all the Yi from !:BuildInfoMap, since they
+    % should never appear in the reverse goal sequence again.
+    %
+:- pred lookup_and_remove_arg_vars_insert_fgt(list(prog_var)::in,
+    goal_order::in, cord(hlds_goal)::in, cord(hlds_goal)::out,
+    fgt_build_info_map::in, fgt_build_info_map::out) is det.
+
+lookup_and_remove_arg_vars_insert_fgt([], _Order, !GoalCord, !BuildInfoMap).
+lookup_and_remove_arg_vars_insert_fgt([Var | Vars], Order, !GoalCord,
+        !BuildInfoMap) :-
+    map.det_remove(Var, BuildInfo, !BuildInfoMap),
+    BuildInfo = fgt_build_info(VarKept, VarGoalCord0),
+    (
+        VarKept = kept_old_gi(Size0, GoalInfo0),
+        ( cord.is_empty(VarGoalCord0) ->
+            unexpected($module, $pred, "VarGoalCord0 is empty")
+        ;
+            MaybeThreshold = get_maybe_from_ground_term_threshold,
+            (
+                MaybeThreshold = yes(Threshold),
+                Size0 >= Threshold
+            ->
+                goal_info_set_nonlocals(set_of_var.make_singleton(Var),
+                    GoalInfo0, GoalInfo),
+                VarGoals0 = cord.list(VarGoalCord0),
+                ConjGoalExpr = conj(plain_conj, VarGoals0),
+                ConjGoal = hlds_goal(ConjGoalExpr, GoalInfo),
+                (
+                    Order = deconstruct_top_down,
+                    Kind = from_ground_term_initial
+                ;
+                    Order = construct_bottom_up,
+                    Kind = from_ground_term_construct
+                ),
+                Reason = from_ground_term(Var, Kind),
+                ScopeGoalExpr = scope(Reason, ConjGoal),
+                ScopeGoal = hlds_goal(ScopeGoalExpr, GoalInfo),
+                VarGoalCord = cord.singleton(ScopeGoal)
+            ;
+                VarGoalCord = VarGoalCord0
+            )
+        )
+    ;
+        VarKept = broken_no_gi,
+        VarGoalCord = VarGoalCord0
+    ),
+    !:GoalCord = !.GoalCord ++ VarGoalCord,
+    lookup_and_remove_arg_vars_insert_fgt(Vars, Order, !GoalCord,
+        !BuildInfoMap).
+
+%---------------------------------------------------------------------------%
+
+    % Return the hlds goal cord part of a fgt_build_info.
+    %
+:- pred project_build_info_goal_cord(fgt_build_info::in, cord(hlds_goal)::out)
+    is det.
+
+project_build_info_goal_cord(fgt_build_info(_, GoalCord), GoalCord).
+
+%---------------------------------------------------------------------------%
+
+project_kept_goal(MarkedGoal, Goal) :-
+    (
+        MarkedGoal = fgt_kept_goal(Goal, _, _)
+    ;
+        MarkedGoal = fgt_broken_goal(_, _, _),
+        unexpected($module, $pred, "broken goal")
+    ).
+
+%---------------------------------------------------------------------------%
+:- end_module hlds.from_ground_term_util.
+%---------------------------------------------------------------------------%
Index: goal_expr_to_goal.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/goal_expr_to_goal.m,v
retrieving revision 1.5
diff -u -b -r1.5 goal_expr_to_goal.m
--- goal_expr_to_goal.m	13 Apr 2012 09:10:22 -0000	1.5
+++ goal_expr_to_goal.m	16 Apr 2012 03:49:01 -0000
@@ -13,7 +13,6 @@
 :- import_module hlds.hlds_module.
 :- import_module hlds.make_hlds.qual_info.
 :- import_module hlds.make_hlds.state_var.
-:- import_module hlds.make_hlds.superhomogeneous.
 :- import_module parse_tree.error_util.
 :- import_module parse_tree.prog_data.
 
@@ -36,7 +35,7 @@
     % - expand references to state variables.
     %
 :- pred transform_goal_expr_context_to_goal(loc_kind::in, goal::in,
-    prog_var_renaming::in, hlds_goal::out, num_added_goals::out,
+    prog_var_renaming::in, hlds_goal::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out,
     module_info::in, module_info::out, qual_info::in, qual_info::out,
@@ -63,6 +62,7 @@
 :- import_module hlds.make_hlds.add_pred.
 :- import_module hlds.make_hlds.field_access.
 :- import_module hlds.make_hlds.make_hlds_warn.
+:- import_module hlds.make_hlds.superhomogeneous.
 :- import_module hlds.pred_table.
 :- import_module hlds.quantification.
 :- import_module libs.globals.
@@ -90,10 +90,9 @@
 %-----------------------------------------------------------------------------%
 
 transform_goal_expr_context_to_goal(LocKind, Goal0 - Context, Renaming, Goal,
-        NumAdded, !SVarState, !SVarStore, !VarSet,
-        !ModuleInfo, !QualInfo, !Specs) :-
+        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
     transform_goal_expr_to_goal(LocKind, Goal0, Context, Renaming, Goal1,
-        NumAdded, !SVarState, !SVarStore, !VarSet,
+        !SVarState, !SVarStore, !VarSet,
         !ModuleInfo, !QualInfo, !Specs),
     Goal1 = hlds_goal(GoalExpr, GoalInfo1),
     goal_info_set_context(Context, GoalInfo1, GoalInfo),
@@ -101,13 +100,12 @@
 
 :- pred transform_goal_expr_to_goal(loc_kind::in, goal_expr::in,
     prog_context::in, prog_var_renaming::in, hlds_goal::out,
-    num_added_goals::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out,
     module_info::in, module_info::out, qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-transform_goal_expr_to_goal(LocKind, Expr, Context, Renaming, Goal, !:NumAdded,
+transform_goal_expr_to_goal(LocKind, Expr, Context, Renaming, Goal,
         !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
     (
         (
@@ -117,7 +115,6 @@
             Expr = true_expr,
             GoalExpr = conj(plain_conj, [])
         ),
-        !:NumAdded = 0,
         goal_info_init(GoalInfo),
         Goal = hlds_goal(GoalExpr, GoalInfo)
     ;
@@ -132,13 +129,13 @@
                 not_expr(Goal0) - Context) - Context)
         ),
         transform_goal_expr_to_goal(LocKind, TransformedExpr, Context,
-            Renaming, Goal, !:NumAdded, !SVarState, !SVarStore, !VarSet,
+            Renaming, Goal, !SVarState, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs)
     ;
         Expr = some_expr(Vars0, SubExpr),
         rename_var_list(need_not_rename, Renaming, Vars0, Vars),
         transform_goal_expr_context_to_goal(LocKind, SubExpr, Renaming,
-            SubGoal, !:NumAdded, !SVarState, !SVarStore, !VarSet,
+            SubGoal, !SVarState, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs),
         Reason = exist_quant(Vars),
         GoalExpr = scope(Reason, SubGoal),
@@ -151,7 +148,7 @@
         svar_prepare_for_local_state_vars(Context, !.VarSet, StateVars,
             BeforeOutsideSVarState, BeforeInsideSVarState, !Specs),
         transform_goal_expr_context_to_goal(LocKind, SubExpr0, Renaming,
-            SubGoal, !:NumAdded, BeforeInsideSVarState, AfterInsideSVarState,
+            SubGoal, BeforeInsideSVarState, AfterInsideSVarState,
             !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
         svar_finish_local_state_vars(StateVars, BeforeOutsideSVarState,
             AfterInsideSVarState, AfterOutsideSVarState),
@@ -163,7 +160,7 @@
     ;
         Expr = promise_purity_expr(Purity, SubExpr0),
         transform_goal_expr_context_to_goal(LocKind, SubExpr0, Renaming,
-            SubGoal, !:NumAdded, !SVarState, !SVarStore, !VarSet,
+            SubGoal, !SVarState, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs),
         Reason = promise_purity(Purity),
         GoalExpr = scope(Reason, SubGoal),
@@ -174,7 +171,7 @@
             DotSVars0, ColonSVars0, SubExpr0),
         transform_promise_eqv_goal(LocKind, Vars0, StateVars0,
             DotSVars0, ColonSVars0, Context, Renaming, Vars, SubExpr0,
-            SubGoal, GoalInfo, !:NumAdded, !SVarState, !SVarStore, !VarSet,
+            SubGoal, GoalInfo, !SVarState, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs),
         Reason = promise_solutions(Vars, equivalent_solutions),
         GoalExpr = scope(Reason, SubGoal),
@@ -184,7 +181,7 @@
             DotSVars0, ColonSVars0, SubExpr0),
         transform_promise_eqv_goal(LocKind, Vars0, StateVars0,
             DotSVars0, ColonSVars0, Context, Renaming, Vars, SubExpr0,
-            SubGoal, GoalInfo, !:NumAdded, !SVarState, !SVarStore, !VarSet,
+            SubGoal, GoalInfo, !SVarState, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs),
         GoalExpr = scope(promise_solutions(Vars, equivalent_solution_sets),
             SubGoal),
@@ -194,7 +191,7 @@
             DotSVars0, ColonSVars0, SubExpr0),
         transform_promise_eqv_goal(LocKind, Vars0, StateVars0,
             DotSVars0, ColonSVars0, Context, Renaming, Vars, SubExpr0,
-            SubGoal, GoalInfo, !:NumAdded, !SVarState, !SVarStore, !VarSet,
+            SubGoal, GoalInfo, !SVarState, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs),
         GoalExpr = scope(promise_solutions(Vars,
             equivalent_solution_sets_arbitrary), SubGoal),
@@ -202,7 +199,7 @@
     ;
         Expr = require_detism_expr(Detism, SubExpr),
         transform_goal_expr_context_to_goal(LocKind, SubExpr, Renaming,
-            SubGoal, !:NumAdded, !SVarState, !SVarStore, !VarSet,
+            SubGoal, !SVarState, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs),
         GoalExpr = scope(require_detism(Detism), SubGoal),
         goal_info_init(GoalInfo),
@@ -211,7 +208,7 @@
         Expr = require_complete_switch_expr(Var0, SubExpr),
         rename_var(need_not_rename, Renaming, Var0, Var),
         transform_goal_expr_context_to_goal(LocKind, SubExpr, Renaming,
-            SubGoal, !:NumAdded, !SVarState, !SVarStore, !VarSet,
+            SubGoal, !SVarState, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs),
         GoalExpr = scope(require_complete_switch(Var), SubGoal),
         goal_info_init(GoalInfo),
@@ -256,12 +253,12 @@
         ),
         BeforeDisjSVarState = !.SVarState,
         transform_goal_expr_context_to_goal(LocKind, MainExpr, Renaming,
-            HLDSMainGoal0, !:NumAdded, BeforeDisjSVarState, AfterMainSVarState,
+            HLDSMainGoal0, BeforeDisjSVarState, AfterMainSVarState,
             !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
         MainDisjState =
             hlds_goal_svar_state(HLDSMainGoal0, AfterMainSVarState),
         transform_orelse_goals(LocKind, OrElseExprs, Renaming, OrElseDisjStates,
-            !NumAdded, BeforeDisjSVarState, !SVarStore, !VarSet,
+            BeforeDisjSVarState, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs),
         AllDisjStates = [MainDisjState | OrElseDisjStates],
         svar_finish_disjunction(Context, AllDisjStates, HLDSGoals, !VarSet,
@@ -295,7 +292,6 @@
         ;
             MaybeOuterScopeInfo = no
         ),
-        !:NumAdded = !.NumAdded + 1,
         ShortHand = atomic_goal(unknown_atomic_goal_type, Outer, Inner,
             MaybeOutputVars, HLDSMainGoal, HLDSOrElseGoals, []),
         GoalExpr = shorthand(ShortHand),
@@ -336,10 +332,8 @@
         svar_prepare_for_local_state_vars(Context, !.VarSet, StateVars,
             BeforeSVarState, BeforeInsideSVarState, !Specs),
         transform_goal_expr_context_to_goal(LocKind, SubExpr1, Renaming,
-            SubGoal, !:NumAdded, BeforeInsideSVarState, AfterInsideSVarState,
+            SubGoal, BeforeInsideSVarState, AfterInsideSVarState,
             !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
-        !:NumAdded =
-            list.length(GetExprs) + !.NumAdded + list.length(SetExprs),
         svar_finish_local_state_vars(StateVars, BeforeSVarState,
             AfterInsideSVarState, AfterSVarState),
         !:SVarState = AfterSVarState,
@@ -359,7 +353,7 @@
                 rename_var(need_not_rename, Renaming, IOStateVar0, IOStateVar),
                 transform_try_expr_with_io(LocKind, IOStateVar0, IOStateVar,
                     SubExpr0, Then0, Catches0, MaybeCatchAny0, Context,
-                    Renaming, Goal, !:NumAdded, !SVarState, !SVarStore,
+                    Renaming, Goal, !SVarState, !SVarStore,
                     !VarSet, !ModuleInfo, !QualInfo, !Specs)
             ;
                 MaybeElse0 = yes(_),
@@ -369,13 +363,12 @@
                 Spec = error_spec(severity_error,
                     phase_parse_tree_to_hlds, [Msg]),
                 !:Specs = [Spec | !.Specs],
-                Goal = true_goal,
-                !:NumAdded = 0
+                Goal = true_goal
             )
         ;
             MaybeIO0 = no,
             transform_try_expr_without_io(LocKind, SubExpr0, Then0, MaybeElse0,
-                Catches0, MaybeCatchAny0, Context, Renaming, Goal, !:NumAdded,
+                Catches0, MaybeCatchAny0, Context, Renaming, Goal,
                 !SVarState, !SVarStore, !VarSet,
                 !ModuleInfo, !QualInfo, !Specs)
         )
@@ -387,17 +380,16 @@
         svar_prepare_for_local_state_vars(Context, !.VarSet, StateVars,
             BeforeSVarState, BeforeCondSVarState, !Specs),
         transform_goal_expr_context_to_goal(LocKind, Cond0, Renaming, Cond,
-            CondAdded, BeforeCondSVarState, AfterCondSVarState, !SVarStore,
+            BeforeCondSVarState, AfterCondSVarState, !SVarStore,
             !VarSet, !ModuleInfo, !QualInfo, !Specs),
         transform_goal_expr_context_to_goal(LocKind, Then0, Renaming, Then1,
-            ThenAdded, AfterCondSVarState, AfterThenSVarState0, !SVarStore,
+            AfterCondSVarState, AfterThenSVarState0, !SVarStore,
             !VarSet, !ModuleInfo, !QualInfo, !Specs),
         svar_finish_local_state_vars(StateVars, BeforeSVarState,
             AfterThenSVarState0, AfterThenSVarState),
         transform_goal_expr_context_to_goal(LocKind, Else0, Renaming, Else1,
-            ElseAdded, BeforeSVarState, AfterElseSVarState, !SVarStore,
+            BeforeSVarState, AfterElseSVarState, !SVarStore,
             !VarSet, !ModuleInfo, !QualInfo, !Specs),
-        !:NumAdded = CondAdded + ThenAdded + ElseAdded,
         goal_info_init(Context, GoalInfo),
         svar_finish_if_then_else(LocKind, Context, StateVars,
             Then1, Then, Else1, Else,
@@ -409,7 +401,7 @@
         Expr = not_expr(SubExpr0),
         BeforeOutsideState = !.SVarState,
         transform_goal_expr_context_to_goal(LocKind, SubExpr0, Renaming,
-            SubGoal, !:NumAdded, !.SVarState, _, !SVarStore,
+            SubGoal, !.SVarState, _, !SVarStore,
             !VarSet, !ModuleInfo, !QualInfo, !Specs),
         !:SVarState = BeforeOutsideState,
         GoalExpr = negation(SubGoal),
@@ -417,18 +409,18 @@
         Goal = hlds_goal(GoalExpr, GoalInfo)
     ;
         Expr = conj_expr(A0, B0),
-        get_rev_conj(LocKind, A0, Renaming, [], R0, 0, !:NumAdded,
+        get_rev_conj(LocKind, A0, Renaming, [], R0,
             !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
-        get_rev_conj(LocKind, B0, Renaming, R0, R,  !NumAdded,
+        get_rev_conj(LocKind, B0, Renaming, R0, R,
             !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
         L = list.reverse(R),
         goal_info_init(GoalInfo),
         conj_list_to_goal(L, GoalInfo, Goal)
     ;
         Expr = par_conj_expr(A0, B0),
-        get_rev_par_conj(LocKind, A0, Renaming, [], R0, 0, !:NumAdded,
+        get_rev_par_conj(LocKind, A0, Renaming, [], R0,
             !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
-        get_rev_par_conj(LocKind, B0, Renaming, R0, R,  !NumAdded,
+        get_rev_par_conj(LocKind, B0, Renaming, R0, R,
             !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
         L = list.reverse(R),
         goal_info_init(GoalInfo),
@@ -437,11 +429,11 @@
         Expr = disj_expr(A0, B0),
         SVarStateBefore = !.SVarState,
         get_disj(LocKind, B0, Renaming, [], DisjunctsSVarStates1,
-            0, !:NumAdded, SVarStateBefore, !SVarStore, !VarSet,
+            SVarStateBefore, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs),
         get_disj(LocKind, A0, Renaming,
             DisjunctsSVarStates1, DisjunctsSVarStates,
-            !NumAdded, SVarStateBefore, !SVarStore, !VarSet,
+            SVarStateBefore, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs),
         svar_finish_disjunction(Context, DisjunctsSVarStates, Disjuncts,
             !VarSet, SVarStateBefore, SVarStateAfter, !SVarStore),
@@ -454,7 +446,7 @@
         TransformedExpr = not_expr(conj_expr(P, not_expr(Q) - Context)
             - Context),
         transform_goal_expr_to_goal(LocKind, TransformedExpr, Context,
-            Renaming, Goal, !:NumAdded, !SVarState, !SVarStore, !VarSet,
+            Renaming, Goal, !SVarState, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs)
     ;
         Expr = equivalent_expr(P0, Q0),
@@ -465,13 +457,12 @@
 
         SVarStateBefore = !.SVarState,
         transform_goal_expr_context_to_goal(LocKind, P0, Renaming, P,
-            NumAddedP, !SVarState, !SVarStore, !VarSet,
+            !SVarState, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs),
         transform_goal_expr_context_to_goal(LocKind, Q0, Renaming, Q,
-            NumAddedQ, !.SVarState, _, !SVarStore, !VarSet,
+            !.SVarState, _, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs),
         !:SVarState = SVarStateBefore,
-        !:NumAdded = NumAddedP + NumAddedQ,
         GoalExpr = shorthand(bi_implication(P, Q)),
         goal_info_init(GoalInfo),
         Goal = hlds_goal(GoalExpr, GoalInfo)
@@ -479,7 +470,8 @@
         Expr = event_expr(EventName, Args0),
         expand_bang_states(Args0, Args1),
         rename_vars_in_term_list(need_not_rename, Renaming, Args1, Args),
-        make_fresh_arg_vars(Args, HeadVars, !VarSet, !SVarState, !Specs),
+        make_fresh_arg_vars_subst_svars(Args, HeadVars, !VarSet,
+            !SVarState, !Specs),
         list.length(HeadVars, Arity),
         list.duplicate(Arity, in_mode, Modes),
         goal_info_init(Context, GoalInfo),
@@ -489,7 +481,7 @@
         Goal0 = hlds_goal(GoalExpr0, GoalInfo),
         CallId = generic_call_id(gcid_event_call(EventName)),
         insert_arg_unifications(HeadVars, Args, Context, ac_call(CallId),
-            Goal0, Goal, 0, !:NumAdded, !SVarState, !SVarStore, !VarSet,
+            Goal0, Goal, !SVarState, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs),
         svar_finish_atomic_goal(LocKind, !SVarState)
     ;
@@ -502,7 +494,7 @@
             % `LHS \= RHS' is defined as `not (LHS = RHS)'
             TransformedExpr = not_expr(unify_expr(LHS, RHS, Purity) - Context),
             transform_goal_expr_to_goal(LocKind, TransformedExpr, Context,
-                Renaming, Goal, !:NumAdded, !SVarState, !SVarStore, !VarSet,
+                Renaming, Goal, !SVarState, !SVarStore, !VarSet,
                 !ModuleInfo, !QualInfo, !Specs)
         ;
             % check for a state var record assignment:
@@ -523,7 +515,7 @@
             RHS = functor(atom(":="), [FieldList, RHS0], Context),
             TransformedExpr = unify_expr(LHS, RHS, Purity),
             transform_goal_expr_to_goal(LocKind, TransformedExpr, Context,
-                Renaming, Goal, !:NumAdded, !SVarState, !SVarStore, !VarSet,
+                Renaming, Goal, !SVarState, !SVarStore, !VarSet,
                 !ModuleInfo, !QualInfo, !Specs)
         ;
             % check for a DCG field access goal:
@@ -536,11 +528,12 @@
         ->
             rename_vars_in_term_list(need_not_rename, Renaming, Args1, Args2),
             transform_dcg_record_syntax(LocKind, Operator, Args2, Context,
-                Goal, !:NumAdded, !SVarState, !SVarStore, !VarSet,
+                Goal, !SVarState, !SVarStore, !VarSet,
                 !ModuleInfo, !QualInfo, !Specs)
         ;
             rename_vars_in_term_list(need_not_rename, Renaming, Args1, Args),
-            make_fresh_arg_vars(Args, HeadVars, !VarSet, !SVarState, !Specs),
+            make_fresh_arg_vars_subst_svars(Args, HeadVars, !VarSet,
+                !SVarState, !Specs),
             list.length(Args, Arity),
             (
                 % Check for a higher-order call,
@@ -578,7 +571,7 @@
 
             record_called_pred_or_func(pf_predicate, Name, Arity, !QualInfo),
             insert_arg_unifications(HeadVars, Args, Context, ac_call(CallId),
-                Goal0, Goal, 0, !:NumAdded, !SVarState, !SVarStore, !VarSet,
+                Goal0, Goal, !SVarState, !SVarStore, !VarSet,
                 !ModuleInfo, !QualInfo, !Specs)
         ),
         svar_finish_atomic_goal(LocKind, !SVarState)
@@ -586,19 +579,22 @@
         Expr = unify_expr(A0, B0, Purity),
         rename_vars_in_term(need_not_rename, Renaming, A0, A),
         rename_vars_in_term(need_not_rename, Renaming, B0, B),
-        % It is an error for the left or right hand side of a
-        % unification to be !X (it may be !.X or !:X, however).
+        % It is an error for the left or right hand side of a unification
+        % to be !X (it may be !.X or !:X, however).
         ( A = functor(atom("!"), [variable(StateVarA, _)], _) ->
             report_svar_unify_error(Context, !.VarSet, StateVarA, !Specs),
-            Goal = true_goal,
-            !:NumAdded = 0
+            ( B = functor(atom("!"), [variable(StateVarB, _)], _) ->
+                report_svar_unify_error(Context, !.VarSet, StateVarB, !Specs)
+            ;
+                true
+            ),
+            Goal = true_goal
         ; B = functor(atom("!"), [variable(StateVarB, _)], _) ->
             report_svar_unify_error(Context, !.VarSet, StateVarB, !Specs),
-            Goal = true_goal,
-            !:NumAdded = 0
+            Goal = true_goal
         ;
             unravel_unification(A, B, Context, umc_explicit, [], Purity, Goal,
-                0, !:NumAdded, !SVarState, !SVarStore, !VarSet,
+                !SVarState, !SVarStore, !VarSet,
                 !ModuleInfo, !QualInfo, !Specs),
             svar_finish_atomic_goal(LocKind, !SVarState)
         )
@@ -640,14 +636,14 @@
     list(prog_var)::in, list(prog_var)::in,
     list(prog_var)::in, list(prog_var)::in,
     prog_context::in, prog_var_renaming::in, list(prog_var)::out,
-    goal::in, hlds_goal::out, hlds_goal_info::out, int::out,
+    goal::in, hlds_goal::out, hlds_goal_info::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out, module_info::in, module_info::out,
     qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
 transform_promise_eqv_goal(LocKind, Vars0, StateVars0, DotSVars0, ColonSVars0,
-        Context, Renaming, QuantVars, Goal0, Goal, GoalInfo, NumAdded,
+        Context, Renaming, QuantVars, Goal0, Goal, GoalInfo,
         !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
     rename_var_list(need_not_rename, Renaming, Vars0, Vars),
     rename_var_list(need_not_rename, Renaming, StateVars0, StateVars1),
@@ -658,8 +654,7 @@
     list.map_foldl3(lookup_dot_state_var(Context), DotSVars1, DotSVars,
         !VarSet, !SVarState, !Specs),
     transform_goal_expr_context_to_goal(LocKind, Goal0, Renaming, Goal,
-        NumAdded, !SVarState, !SVarStore, !VarSet,
-        !ModuleInfo, !QualInfo, !Specs),
+        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
     goal_info_init(GoalInfo),
     list.map_foldl3(lookup_dot_state_var(Context), StateVars1, NewStateVars,
         !VarSet, !SVarState, !Specs),
@@ -684,14 +679,14 @@
 
 :- pred transform_dcg_record_syntax(loc_kind::in,
     string::in(dcg_record_syntax_op), list(prog_term)::in, prog_context::in,
-    hlds_goal::out, int::out,
+    hlds_goal::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out,
     module_info::in, module_info::out, qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
 transform_dcg_record_syntax(LocKind, Operator, ArgTerms0, Context, Goal,
-        NumAdded, !SVarState, !SVarStore, !VarSet,
+        !SVarState, !SVarStore, !VarSet,
         !ModuleInfo, !QualInfo, !Specs) :-
     goal_info_init(Context, GoalInfo),
     (
@@ -716,7 +711,7 @@
             MaybeFieldNames = ok1(FieldNames),
             ArgTerms = [FieldValueTerm, TermInputTerm, TermOutputTerm],
             transform_dcg_record_syntax_2(AccessType, FieldNames, ArgTerms,
-                Context, Goal, NumAdded, !SVarState, !SVarStore, !VarSet,
+                Context, Goal, !SVarState, !SVarStore, !VarSet,
                 !ModuleInfo, !QualInfo, !Specs),
             svar_finish_atomic_goal(LocKind, !SVarState)
         ;
@@ -724,13 +719,11 @@
             !:Specs = FieldNamesSpecs ++ !.Specs,
             invalid_goal("^", ArgTerms0, GoalInfo, Goal, !VarSet,
                 !SVarState, !Specs),
-            NumAdded = 0,
             qual_info_set_found_syntax_error(yes, !QualInfo)
         )
     ;
         invalid_goal("^", ArgTerms0, GoalInfo, Goal, !VarSet, !SVarState,
             !Specs),
-        NumAdded = 0,
         qual_info_set_found_syntax_error(yes, !QualInfo),
         Pieces = [words("Error: expected `Field =^ field1 ^ ... ^ fieldN'"),
             words("or `^ field1 ^ ... ^ fieldN := Field'"),
@@ -742,23 +735,23 @@
 
 :- pred transform_dcg_record_syntax_2(field_access_type::in, field_list::in,
     list(prog_term)::in, prog_context::in, hlds_goal::out,
-    num_added_goals::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out,
     module_info::in, module_info::out, qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
 transform_dcg_record_syntax_2(AccessType, FieldNames, ArgTerms, Context, Goal,
-        NumAdded, !SVarState, !SVarStore, !VarSet,
+        !SVarState, !SVarStore, !VarSet,
         !ModuleInfo, !QualInfo, !Specs) :-
-    make_fresh_arg_vars(ArgTerms, ArgVars, !VarSet, !SVarState, !Specs),
+    make_fresh_arg_vars_subst_svars(ArgTerms, ArgVars, !VarSet,
+        !SVarState, !Specs),
     ( ArgVars = [FieldValueVar, TermInputVar, TermOutputVar] ->
         (
             AccessType = set,
             expand_set_field_function_call(Context, umc_explicit, [],
                 FieldNames, FieldValueVar, TermInputVar, TermOutputVar,
                 Functor, InnermostFunctor - InnermostSubContext, Goal0,
-                0, NumAdded1, !SVarState, !SVarStore, !VarSet,
+                !SVarState, !SVarStore, !VarSet,
                 !ModuleInfo, !QualInfo, !Specs),
 
             FieldArgNumber = 2,
@@ -784,15 +777,14 @@
                 OutputTermArgNumber - OutputTermArgContext
             ],
             insert_arg_unifications_with_contexts(ArgVars, ArgTerms,
-                ArgContexts, Context, Goal0, Goal, NumAdded1, NumAdded,
-                !SVarState, !SVarStore, !VarSet,
-                !ModuleInfo, !QualInfo, !Specs)
+                ArgContexts, Context, Goal0, Goal, !SVarState, !SVarStore,
+                !VarSet, !ModuleInfo, !QualInfo, !Specs)
         ;
             AccessType = get,
             expand_dcg_field_extraction_goal(Context, umc_explicit, [],
                 FieldNames, FieldValueVar, TermInputVar, TermOutputVar,
                 Functor, InnermostFunctor - _InnerSubContext, Goal0,
-                0, NumAdded1, !SVarState, !SVarStore, !VarSet,
+                !SVarState, !SVarStore, !VarSet,
                 !ModuleInfo, !QualInfo, !Specs),
             InputTermArgNumber = 1,
             InputTermArgContext = ac_functor(Functor, umc_explicit, []),
@@ -817,9 +809,8 @@
                 OutputTermArgNumber - OutputTermArgContext
             ],
             insert_arg_unifications_with_contexts(ArgVars, ArgTerms,
-                ArgContexts, Context, Goal0, Goal, NumAdded1, NumAdded,
-                !SVarState, !SVarStore, !VarSet,
-                !ModuleInfo, !QualInfo, !Specs)
+                ArgContexts, Context, Goal0, Goal, !SVarState, !SVarStore,
+                !VarSet, !ModuleInfo, !QualInfo, !Specs)
         )
     ;
         unexpected($module, $pred, "arity != 3")
@@ -832,24 +823,21 @@
     %
 :- pred get_rev_conj(loc_kind::in, goal::in, prog_var_renaming::in,
     list(hlds_goal)::in, list(hlds_goal)::out,
-    num_added_goals::in, num_added_goals::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out, module_info::in, module_info::out,
     qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-get_rev_conj(LocKind, Goal, Renaming, RevConj0, RevConj, !NumAdded,
+get_rev_conj(LocKind, Goal, Renaming, RevConj0, RevConj,
         !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
     ( Goal = conj_expr(A, B) - _Context ->
-        get_rev_conj(LocKind, A, Renaming, RevConj0, RevConj1, !NumAdded,
+        get_rev_conj(LocKind, A, Renaming, RevConj0, RevConj1,
             !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
-        get_rev_conj(LocKind, B, Renaming, RevConj1, RevConj, !NumAdded,
+        get_rev_conj(LocKind, B, Renaming, RevConj1, RevConj,
             !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs)
     ;
         transform_goal_expr_context_to_goal(LocKind, Goal, Renaming, Goal1,
-            GoalAdded, !SVarState, !SVarStore, !VarSet,
-            !ModuleInfo, !QualInfo, !Specs),
-        !:NumAdded = !.NumAdded + GoalAdded,
+            !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
         goal_to_conj_list(Goal1, ConjList),
         RevConj = list.reverse(ConjList) ++ RevConj0
     ).
@@ -861,26 +849,24 @@
     %
 :- pred get_rev_par_conj(loc_kind::in, goal::in, prog_var_renaming::in,
     list(hlds_goal)::in, list(hlds_goal)::out,
-    num_added_goals::in, num_added_goals::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out, module_info::in, module_info::out,
     qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-get_rev_par_conj(LocKind, Goal, Renaming, RevParConj0, RevParConj, !NumAdded,
+get_rev_par_conj(LocKind, Goal, Renaming, RevParConj0, RevParConj,
         !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
     ( Goal = par_conj_expr(A, B) - _Context ->
         get_rev_par_conj(LocKind, A, Renaming, RevParConj0, RevParConj1,
-            !NumAdded, !SVarState, !SVarStore, !VarSet,
+            !SVarState, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs),
         get_rev_par_conj(LocKind, B, Renaming, RevParConj1, RevParConj,
-            !NumAdded, !SVarState, !SVarStore, !VarSet,
+            !SVarState, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs)
     ;
         transform_goal_expr_context_to_goal(LocKind, Goal, Renaming, Goal1,
-            GoalAdded, !SVarState, !SVarStore, !VarSet,
+            !SVarState, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs),
-        !:NumAdded = !.NumAdded + GoalAdded,
         goal_to_par_conj_list(Goal1, ParConjList),
         RevParConj = list.reverse(ParConjList) ++ RevParConj0
     ).
@@ -892,55 +878,50 @@
     %
 :- pred get_disj(loc_kind::in, goal::in, prog_var_renaming::in,
     list(hlds_goal_svar_state)::in, list(hlds_goal_svar_state)::out,
-    num_added_goals::in, num_added_goals::out,
     svar_state::in, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out,
     module_info::in, module_info::out, qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-get_disj(LocKind, Goal, Renaming, DisjStates0, DisjStates, !NumAdded,
-        SVarStateBefore, !SVarStore, !VarSet,
-        !ModuleInfo, !QualInfo, !Specs) :-
+get_disj(LocKind, Goal, Renaming, DisjStates0, DisjStates, SVarStateBefore,
+        !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
     ( Goal = disj_expr(A, B) - _Context ->
         % We recurse on the *second* arm first, so that we will put the
         % disjuncts from *that* arm at the front of DisjStates0, before
         % putting the disjuncts from the first arm at the front of the
         % resulting DisjStates1. This way, the overall result, DisjStates,
         % will have the disjuncts and their svar_infos in the correct order.
-        get_disj(LocKind, B, Renaming, DisjStates0, DisjStates1, !NumAdded,
+        get_disj(LocKind, B, Renaming, DisjStates0, DisjStates1,
             SVarStateBefore, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs),
-        get_disj(LocKind, A, Renaming, DisjStates1, DisjStates,  !NumAdded,
+        get_disj(LocKind, A, Renaming, DisjStates1, DisjStates,
             SVarStateBefore, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs)
     ;
         transform_goal_expr_context_to_goal(LocKind, Goal, Renaming,
-            HLDSGoal, GoalAdded, SVarStateBefore, SVarStateAfterDisjunct,
+            HLDSGoal, SVarStateBefore, SVarStateAfterDisjunct,
             !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
-        !:NumAdded = !.NumAdded + GoalAdded,
         DisjState = hlds_goal_svar_state(HLDSGoal, SVarStateAfterDisjunct),
         DisjStates = [DisjState | DisjStates0]
     ).
 
 :- pred transform_orelse_goals(loc_kind::in, list(goal)::in,
     prog_var_renaming::in, list(hlds_goal_svar_state)::out,
-    num_added_goals::in, num_added_goals::out,
     svar_state::in, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out, module_info::in, module_info::out,
     qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-transform_orelse_goals(_, [], _, [], !NumAdded, _SVarStateBefore, !SVarState,
+transform_orelse_goals(_, [], _, [], _SVarStateBefore, !SVarState,
         !VarSet, !ModuleInfo, !QualInfo, !Specs).
 transform_orelse_goals(LocKind, [Goal | Goals], Renaming,
-        [DisjState | DisjStates], !NumAdded, SVarStateBefore, !SVarStore,
+        [DisjState | DisjStates], SVarStateBefore, !SVarStore,
         !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
     transform_goal_expr_context_to_goal(LocKind, Goal, Renaming, HLDSGoal,
-        NumAddedGoal, SVarStateBefore, SVarStateAfterDisjunct, !SVarStore,
+        SVarStateBefore, SVarStateAfterDisjunct, !SVarStore,
         !VarSet, !ModuleInfo, !QualInfo, !Specs),
     DisjState = hlds_goal_svar_state(HLDSGoal, SVarStateAfterDisjunct),
-    !:NumAdded = !.NumAdded + NumAddedGoal,
-    transform_orelse_goals(LocKind, Goals, Renaming, DisjStates, !NumAdded,
+    transform_orelse_goals(LocKind, Goals, Renaming, DisjStates,
         SVarStateBefore, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs).
 
 %----------------------------------------------------------------------------%
@@ -973,14 +954,13 @@
 :- pred transform_try_expr_with_io(loc_kind::in, svar::in, svar::in,
     goal::in, goal::in, list(catch_expr)::in, maybe(catch_any_expr)::in,
     prog_context::in, prog_var_renaming::in, hlds_goal::out,
-    num_added_goals::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out, module_info::in, module_info::out,
     qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
 transform_try_expr_with_io(LocKind, IOStateVarUnrenamed, IOStateVar, Goal0,
-        Then0, Catches0, MaybeCatchAny0, Context, Renaming, TryGoal, NumAdded,
+        Then0, Catches0, MaybeCatchAny0, Context, Renaming, TryGoal,
         !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
     varset.new_named_var("TryResult", ResultVar, !VarSet),
     varset.new_var(ExcpVar, !VarSet),
@@ -995,7 +975,7 @@
     CallMagic0 = call_expr(magic_exception_result_sym_name, [ResultVarTerm],
         purity_pure) - Context,
     transform_goal_expr_context_to_goal(LocKind, CallMagic0, Renaming,
-        CallMagic, NumAddedA, !SVarState, !SVarStore, !VarSet,
+        CallMagic, !SVarState, !SVarStore, !VarSet,
         !ModuleInfo, !QualInfo, !Specs),
 
     % Get the variable for !.IO before the (eventual) try_io call.
@@ -1012,7 +992,7 @@
             purity_pure
         ) - Context,
     transform_goal_expr_context_to_goal(LocKind, ResultIsSucceededUnify0,
-        Renaming, ResultIsSucceededUnify, NumAddedB, !SVarState, !SVarStore,
+        Renaming, ResultIsSucceededUnify, !SVarState, !SVarStore,
         !VarSet, !ModuleInfo, !QualInfo, !Specs),
 
     % Build "some [] ( !:IO = !.IO, Goal )".
@@ -1027,7 +1007,7 @@
     ) - Context,
     ScopedGoal0 = some_expr([], conj_expr(IOUnify, Goal0) - Context) - Context,
     transform_goal_expr_context_to_goal(LocKind, ScopedGoal0, Renaming,
-        ScopedGoal, NumAddedC, !SVarState, !SVarStore, !VarSet,
+        ScopedGoal, !SVarState, !SVarStore, !VarSet,
         !ModuleInfo, !QualInfo, !Specs),
 
     % Remember the variable for !.IO after the (eventual) try_io Goal.
@@ -1037,7 +1017,7 @@
     % Build "some [] ( Then )".
     ScopedThen0 = some_expr([], Then0) - Context,
     transform_goal_expr_context_to_goal(LocKind, ScopedThen0, Renaming,
-        ScopedThen, NumAddedD, !SVarState, !SVarStore, !VarSet,
+        ScopedThen, !SVarState, !SVarStore, !VarSet,
         !ModuleInfo, !QualInfo, !Specs),
 
     % Build:
@@ -1056,7 +1036,7 @@
     make_exception_handling_disjunct(ResultVarTerm, ExcpVarTerm, Catches0,
         MaybeCatchAny0, Context, ResultIsExceptionDisjunct0),
     transform_goal_expr_context_to_goal(LocKind, ResultIsExceptionDisjunct0,
-        Renaming, ResultIsExceptionDisjunct, NumAddedE, !SVarState, !SVarStore,
+        Renaming, ResultIsExceptionDisjunct, !SVarState, !SVarStore,
         !VarSet, !ModuleInfo, !QualInfo, !Specs),
 
     SVarStateAfterResultIsExceptionDisjunct = !.SVarState,
@@ -1079,9 +1059,7 @@
     IOStateVars = try_io_state_vars(IOStateVarBefore, IOStateVarAfter),
     GoalExpr = shorthand(try_goal(yes(IOStateVars), ResultVar,
         CallMagicThenDisjunction)),
-    TryGoal = hlds_goal(GoalExpr, GoalInfo),
-
-    NumAdded = NumAddedA + NumAddedB + NumAddedC + NumAddedD + NumAddedE.
+    TryGoal = hlds_goal(GoalExpr, GoalInfo).
 
     % Transform a try_expr which does not need I/O.
     %
@@ -1115,14 +1093,13 @@
 :- pred transform_try_expr_without_io(loc_kind::in, goal::in, goal::in,
     maybe(goal)::in, list(catch_expr)::in, maybe(catch_any_expr)::in,
     prog_context::in, prog_var_renaming::in, hlds_goal::out,
-    num_added_goals::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out, module_info::in, module_info::out,
     qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
 transform_try_expr_without_io(LocKind, Goal0, Then0, MaybeElse0, Catches0,
-        MaybeCatchAny0, Context, Renaming, TryGoal, NumAdded,
+        MaybeCatchAny0, Context, Renaming, TryGoal,
         !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
     varset.new_named_var("TryResult", ResultVar, !VarSet),
     varset.new_var(ExcpVar, !VarSet),
@@ -1173,7 +1150,7 @@
             ) - Context
         ) - Context,
     transform_goal_expr_context_to_goal(LocKind, CallMagicThenDisjunction0,
-        Renaming, CallMagicThenDisjunction, NumAdded, !SVarState, !SVarStore,
+        Renaming, CallMagicThenDisjunction, !SVarState, !SVarStore,
         !VarSet, !ModuleInfo, !QualInfo, !Specs),
 
     GoalExpr = shorthand(try_goal(no, ResultVar, CallMagicThenDisjunction)),
@@ -1273,7 +1250,8 @@
     list(error_spec)::in, list(error_spec)::out) is det.
 
 invalid_goal(UpdateStr, Args0, GoalInfo, Goal, !VarSet, !SVarState, !Specs) :-
-    make_fresh_arg_vars(Args0, HeadVars, !VarSet, !SVarState, !Specs),
+    make_fresh_arg_vars_subst_svars(Args0, HeadVars, !VarSet,
+        !SVarState, !Specs),
     MaybeUnifyContext = no,
     GoalExpr = plain_call(invalid_pred_id, invalid_proc_id, HeadVars,
         not_builtin, MaybeUnifyContext, unqualified(UpdateStr)),
Index: hlds.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/hlds.m,v
retrieving revision 1.228
diff -u -b -r1.228 hlds.m
--- hlds.m	20 Dec 2010 07:47:31 -0000	1.228
+++ hlds.m	12 Apr 2012 10:36:56 -0000
@@ -46,6 +46,7 @@
 % Miscellaneous utilities.
 :- include_module arg_info.
 :- include_module code_model.
+:- include_module from_ground_term_util.
 :- include_module goal_form.
 :- include_module goal_path.
 :- include_module goal_util.
Index: hlds_goal.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/hlds_goal.m,v
retrieving revision 1.236
diff -u -b -r1.236 hlds_goal.m
--- hlds_goal.m	12 Apr 2012 11:32:31 -0000	1.236
+++ hlds_goal.m	14 Apr 2012 05:15:56 -0000
@@ -398,8 +398,8 @@
     % "unifications" may include things that look like function symbols
     % but are in fact function calls. When typecheck.m discovers that this
     % applies to a unification, it does not remove the scope or change its
-    % kind. The mode analysis pass will eventually change the kind to
-    % from_ground_term_other.
+    % kind. The post_typecheck phase, executed as part of the purity pass,
+    % will eventually change the kind to from_ground_term_other.
     %
     % Up to the first invocation of mode analysis, all from_ground_term scopes
     % will have kind from_ground_term_initial. After that, they will have
Index: polymorphism.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/polymorphism.m,v
retrieving revision 1.376
diff -u -b -r1.376 polymorphism.m
--- polymorphism.m	12 Apr 2012 07:15:01 -0000	1.376
+++ polymorphism.m	16 Apr 2012 05:52:05 -0000
@@ -392,6 +392,7 @@
 :- import_module check_hlds.clause_to_proc.
 :- import_module check_hlds.mode_util.
 :- import_module check_hlds.type_util.
+:- import_module hlds.from_ground_term_util.
 :- import_module hlds.goal_util.
 :- import_module hlds.hlds_args.
 :- import_module hlds.hlds_clauses.
@@ -1150,14 +1151,14 @@
                 (
                     Kind = from_ground_term_initial,
                     polymorphism_process_from_ground_term_initial(TermVar,
-                        Reason, GoalInfo0, SubGoal0, SubGoal, !Info)
+                        GoalInfo0, SubGoal0, GoalExpr, !Info)
                 ;
                     ( Kind = from_ground_term_construct
                     ; Kind = from_ground_term_deconstruct
                     ; Kind = from_ground_term_other
                     ),
                     polymorphism_process_goal(SubGoal0, SubGoal, !Info),
-                    Reason = Reason0
+                    GoalExpr = scope(Reason0, SubGoal)
                 )
             ;
                 Reason0 = promise_solutions(_, _),
@@ -1171,7 +1172,7 @@
                 get_maps_snapshot(!.Info, InitialSnapshot),
                 polymorphism_process_goal(SubGoal0, SubGoal, !Info),
                 set_maps_snapshot(InitialSnapshot, !Info),
-                Reason = Reason0
+                GoalExpr = scope(Reason0, SubGoal)
             ;
                 ( Reason0 = promise_purity(_)
                 ; Reason0 = require_detism(_)
@@ -1181,7 +1182,7 @@
                 ; Reason0 = loop_control(_, _, _)
                 ),
                 polymorphism_process_goal(SubGoal0, SubGoal, !Info),
-                Reason = Reason0
+                GoalExpr = scope(Reason0, SubGoal)
             ;
                 Reason0 = exist_quant(_),
                 % If we allowed a type_info created inside SubGoal to be reused
@@ -1195,7 +1196,7 @@
                 get_maps_snapshot(!.Info, InitialSnapshot),
                 polymorphism_process_goal(SubGoal0, SubGoal, !Info),
                 set_maps_snapshot(InitialSnapshot, !Info),
-                Reason = Reason0
+                GoalExpr = scope(Reason0, SubGoal)
             ;
                 Reason0 = trace_goal(_, _, _, _, _),
                 % Trace goal scopes will be deleted after semantic analysis
@@ -1211,9 +1212,8 @@
                 get_maps_snapshot(!.Info, InitialSnapshot),
                 polymorphism_process_goal(SubGoal0, SubGoal, !Info),
                 set_maps_snapshot(InitialSnapshot, !Info),
-                Reason = Reason0
-            ),
-            GoalExpr = scope(Reason, SubGoal)
+                GoalExpr = scope(Reason0, SubGoal)
+            )
         ),
         Goal = hlds_goal(GoalExpr, GoalInfo0)
     ;
@@ -1262,57 +1262,92 @@
         Goal = hlds_goal(GoalExpr, GoalInfo0)
     ).
 
+%-----------------------------------------------------------------------------%
+
 :- pred polymorphism_process_from_ground_term_initial(prog_var::in,
-    scope_reason::out, hlds_goal_info::in, hlds_goal::in, hlds_goal::out,
+    hlds_goal_info::in, hlds_goal::in, hlds_goal_expr::out,
     poly_info::in, poly_info::out) is det.
 
-polymorphism_process_from_ground_term_initial(TermVar, Reason, GoalInfo0,
-        SubGoal0, SubGoal, !Info) :-
-    poly_info_get_varset(!.Info, VarSetBefore),
+polymorphism_process_from_ground_term_initial(TermVar, GoalInfo0, SubGoal0,
+        GoalExpr, !Info) :-
+    SubGoal0 = hlds_goal(SubGoalExpr0, SubGoalInfo0),
+    ( SubGoalExpr0 = conj(plain_conj, SubGoals0Prime) ->
+        SubGoals0 = SubGoals0Prime
+    ;
+        unexpected($module, $pred,
+            "from_ground_term_initial goal is not plain conj")
+    ),
+    polymorphism_process_fgti_goals(SubGoals0, [], RevMarkedSubGoals,
+        fgt_invariants_kept, InvariantsStatus, !Info),
+    (
+        InvariantsStatus = fgt_invariants_kept,
+        Reason = from_ground_term(TermVar, from_ground_term_initial),
+        GoalExpr = scope(Reason, SubGoal0)
+    ;
+        InvariantsStatus = fgt_invariants_broken,
+        introduce_partial_fgt_scopes(GoalInfo0, SubGoalInfo0,
+            RevMarkedSubGoals, deconstruct_top_down, SubGoal),
+        % Delete the scope wrapper around SubGoal0.
+        SubGoal = hlds_goal(GoalExpr, _)
+    ).
+
+:- pred polymorphism_process_fgti_goals(list(hlds_goal)::in,
+    list(fgt_marked_goal)::in, list(fgt_marked_goal)::out,
+    fgt_invariants_status::in, fgt_invariants_status::out,
+    poly_info::in, poly_info::out) is det.
+
+polymorphism_process_fgti_goals([], !RevMarkedGoals, !InvariantsStatus, !Info).
+polymorphism_process_fgti_goals([Goal0 | Goals0], !RevMarkedGoals,
+        !InvariantsStatus, !Info) :-
+    % This is used only if polymorphism_fgt_sanity_tests is enabled.
+    OldInfo = !.Info,
+    Goal0 = hlds_goal(GoalExpr0, GoalInfo0),
+    (
+        GoalExpr0 = unify(XVarPrime, Y, ModePrime, UnificationPrime,
+            UnifyContextPrime),
+        Y = rhs_functor(ConsIdPrime, _, YVarsPrime)
+    ->
+        XVar = XVarPrime,
+        Mode = ModePrime,
+        Unification = UnificationPrime,
+        UnifyContext = UnifyContextPrime,
+        ConsId = ConsIdPrime,
+        YVars = YVarsPrime
+    ;
+        unexpected($module, $pred,
+            "from_ground_term_initial conjunct is not functor unify")
+    ),
+    polymorphism_process_unify_functor(XVar, ConsId, YVars, Mode,
+        Unification, UnifyContext, GoalInfo0, Goal, Changed, !Info),
+    (
+        Changed = no,
+        trace [compiletime(flag("polymorphism_fgt_sanity_tests"))] (
+            poly_info_get_varset(OldInfo, VarSetBefore),
     MaxVarBefore = varset.max_var(VarSetBefore),
-    poly_info_get_num_reuses(!.Info, NumReusesBefore),
-    polymorphism_process_goal(SubGoal0, SubGoal1, !Info),
+            poly_info_get_num_reuses(OldInfo, NumReusesBefore),
+
     poly_info_get_varset(!.Info, VarSetAfter),
     MaxVarAfter = varset.max_var(VarSetAfter),
     poly_info_get_num_reuses(!.Info, NumReusesAfter),
 
-    (
-        % If the first two goals fail, then we may have modified (and probably
-        % did modify) the code in the scope by adding a reference to typeinfo
-        % variables representing TermVarTypeVars.
-        MaxVarAfter = MaxVarBefore,
-        NumReusesAfter = NumReusesBefore,
-        require_det (
-            poly_info_get_var_types(!.Info, VarTypes),
-            map.lookup(VarTypes, TermVar, TermVarType),
-            type_vars(TermVarType, TermVarTypeVars)
-        ),
-        % If this fails, then we did introduce some variables into the scope,
-        % so we cannot guarantee that the scope still satisfies the invariants
-        % of from_ground_term_initial scopes.
-        TermVarTypeVars = []
-    ->
-        % TermVarTypeVars = [] says that there is no polymorphism imposed
-        % from the outside via TermVar, and MaxVarAfter = MaxVarBefore
-        % and NumReusesAfter = NumReusesBefore together say that there was
-        % no polymorphism added by the goals inside the scope (since those
-        % would have required the creation or reuse of typeinfo variables).
-        % XXX zs: I am only 90% sure of the statement in the parentheses.
-        % If it turns out to be wrong, we would have to add a flag to
-        % poly_infos that is set whenever this pass modifies a goal,
-        % at least in ways that would invalidate the
-        % from_ground_term_initial invariant.
-        Reason = from_ground_term(TermVar, from_ground_term_initial),
-        SubGoal = SubGoal1
-    ;
-        Reason = from_ground_term(TermVar, from_ground_term_other),
-        ( goal_info_has_feature(GoalInfo0, feature_from_head) ->
-            attach_features_to_all_goals([feature_from_head],
-                attach_in_from_ground_term, SubGoal1, SubGoal)
-        ;
-            SubGoal = SubGoal1
-        )
-    ).
+            expect(unify(MaxVarBefore, MaxVarAfter), $module, $pred,
+                "MaxVarBefore != MaxVarAfter"),
+            expect(unify(NumReusesBefore, NumReusesAfter), $module, $pred,
+                "NumReusesBefore != NumReusesAfter"),
+            expect(unify(Goal0, Goal), $module, $pred,
+                "Goal0 != Goal")
+        ),
+        MarkedGoal = fgt_kept_goal(Goal0, XVar, YVars)
+    ;
+        Changed = yes,
+        MarkedGoal = fgt_broken_goal(Goal, XVar, YVars),
+        !:InvariantsStatus = fgt_invariants_broken
+    ),
+    !:RevMarkedGoals = [MarkedGoal | !.RevMarkedGoals],
+    polymorphism_process_fgti_goals(Goals0, !RevMarkedGoals,
+        !InvariantsStatus, !Info).
+
+%-----------------------------------------------------------------------------%
 
 :- pred polymorphism_process_unify(prog_var::in, unify_rhs::in,
     unify_mode::in, unification::in, unify_context::in, hlds_goal_info::in,
@@ -1338,13 +1373,13 @@
         poly_info_get_var_types(!.Info, VarTypes),
         map.lookup(VarTypes, XVar, Type),
         unification_typeinfos(Type, Unification0, Unification,
-            GoalInfo0, GoalInfo, !Info),
+            GoalInfo0, GoalInfo, _Changed, !Info),
         Goal = hlds_goal(unify(XVar, Y, Mode, Unification, UnifyContext),
             GoalInfo)
     ;
         Y = rhs_functor(ConsId, _, Args),
         polymorphism_process_unify_functor(XVar, ConsId, Args, Mode,
-            Unification0, UnifyContext, GoalInfo0, Goal, !Info)
+            Unification0, UnifyContext, GoalInfo0, Goal, _Changed, !Info)
     ;
         Y = rhs_lambda_goal(Purity, Groundness, PredOrFunc, EvalMethod,
             ArgVars0, LambdaVars, Modes, Det, LambdaGoal0),
@@ -1382,14 +1417,21 @@
 
 :- pred unification_typeinfos(mer_type::in,
     unification::in, unification::out, hlds_goal_info::in, hlds_goal_info::out,
-    poly_info::in, poly_info::out) is det.
+    bool::out, poly_info::in, poly_info::out) is det.
 
-unification_typeinfos(Type, !Unification, !GoalInfo, !Info) :-
+unification_typeinfos(Type, !Unification, !GoalInfo, Changed, !Info) :-
     % Compute the type_info/type_class_info variables that would be used
     % if this unification ends up being a complicated_unify.
     type_vars(Type, TypeVars),
+    (
+        TypeVars = [],
+        Changed = no
+    ;
+        TypeVars = [_ | _],
     list.map_foldl(get_type_info_locn, TypeVars, TypeInfoLocns, !Info),
-    add_unification_typeinfos(TypeInfoLocns, !Unification, !GoalInfo).
+        add_unification_typeinfos(TypeInfoLocns, !Unification, !GoalInfo),
+        Changed = yes
+    ).
 
 unification_typeinfos_rtti_varmaps(Type, RttiVarMaps, !Unification,
         !GoalInfo) :-
@@ -1437,10 +1479,11 @@
 
 :- pred polymorphism_process_unify_functor(prog_var::in, cons_id::in,
     list(prog_var)::in, unify_mode::in, unification::in, unify_context::in,
-    hlds_goal_info::in, hlds_goal::out, poly_info::in, poly_info::out) is det.
+    hlds_goal_info::in, hlds_goal::out, bool::out,
+    poly_info::in, poly_info::out) is det.
 
 polymorphism_process_unify_functor(X0, ConsId0, ArgVars0, Mode0, Unification0,
-        UnifyContext, GoalInfo0, Goal, !Info) :-
+        UnifyContext, GoalInfo0, Goal, Changed, !Info) :-
     poly_info_get_module_info(!.Info, ModuleInfo0),
     poly_info_get_var_types(!.Info, VarTypes0),
     map.lookup(VarTypes0, X0, TypeOfX),
@@ -1503,7 +1546,8 @@
         poly_info_set_varset_and_types(VarSet, VarTypes, !Info),
         % Process the unification in its new form.
         polymorphism_process_unify(X0, Functor0, Mode0, Unification0,
-            UnifyContext, GoalInfo1, Goal, !Info)
+            UnifyContext, GoalInfo1, Goal, !Info),
+        Changed = yes
     ;
         % Is this a construction or deconstruction of an existentially
         % typed data type?
@@ -1539,21 +1583,23 @@
 
         % Some of the argument unifications may be complicated unifications,
         % which may need type_infos.
-        unification_typeinfos(TypeOfX,
-            Unification0, Unification, GoalInfo1, GoalInfo, !Info),
+        unification_typeinfos(TypeOfX, Unification0, Unification,
+            GoalInfo1, GoalInfo, _Changed, !Info),
 
         UnifyExpr = unify(X0, rhs_functor(ConsId, IsConstruction, ArgVars),
             Mode0, Unification, UnifyContext),
         Unify = hlds_goal(UnifyExpr, GoalInfo),
         GoalList = ExtraGoals ++ [Unify],
-        conj_list_to_goal(GoalList, GoalInfo0, Goal)
+        conj_list_to_goal(GoalList, GoalInfo0, Goal),
+        Changed = yes
     ;
         % We leave construction/deconstruction unifications alone.
         % Some of the argument unifications may be complicated unifications,
         % which may need type_infos.
 
-        unification_typeinfos(TypeOfX,
-            Unification0, Unification, GoalInfo0, GoalInfo, !Info),
+        % XXX Return original Goal0 if Changed = no.
+        unification_typeinfos(TypeOfX, Unification0, Unification,
+            GoalInfo0, GoalInfo, Changed, !Info),
         GoalExpr = unify(X0, rhs_functor(ConsId0, no, ArgVars0), Mode0,
             Unification, UnifyContext),
         Goal = hlds_goal(GoalExpr, GoalInfo)
@@ -2404,8 +2450,8 @@
         RenamedInstanceConstraints, ActualInstanceConstraints0),
     % XXX document diamond as guess
     % XXX does anyone know what the preceding line means?
-    ActualInstanceConstraints =
-        ActualInstanceConstraints0 `list.delete_elems` Seen,
+    list.delete_elems(ActualInstanceConstraints0, Seen,
+        ActualInstanceConstraints),
     apply_variable_renaming_to_constraint_proofs(Renaming,
         InstanceProofs, RenamedInstanceProofs),
     apply_rec_subst_to_constraint_proofs(InstanceSubst,
Index: post_typecheck.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/post_typecheck.m,v
retrieving revision 1.156
diff -u -b -r1.156 post_typecheck.m
--- post_typecheck.m	12 Apr 2012 04:56:17 -0000	1.156
+++ post_typecheck.m	12 Apr 2012 11:56:12 -0000
@@ -117,7 +117,7 @@
 :- pred resolve_unify_functor(prog_var::in, cons_id::in,
     list(prog_var)::in, unify_mode::in, unification::in, unify_context::in,
     hlds_goal_info::in, module_info::in, pred_info::in, pred_info::out,
-    vartypes::in, vartypes::out, prog_varset::in, prog_varset::out,
+    prog_varset::in, prog_varset::out, vartypes::in, vartypes::out,
     hlds_goal::out, is_plain_unify::out) is det.
 
 %-----------------------------------------------------------------------------%
@@ -1027,7 +1027,7 @@
 %-----------------------------------------------------------------------------%
 
 resolve_unify_functor(X0, ConsId0, ArgVars0, Mode0, Unification0, UnifyContext,
-        GoalInfo0, ModuleInfo, !PredInfo, !VarTypes, !VarSet,
+        GoalInfo0, ModuleInfo, !PredInfo, !VarSet, !VarTypes,
         Goal, IsPlainUnify) :-
     map.lookup(!.VarTypes, X0, TypeOfX),
     list.length(ArgVars0, Arity),
Index: purity.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/purity.m,v
retrieving revision 1.154
diff -u -b -r1.154 purity.m
--- purity.m	12 Apr 2012 11:32:48 -0000	1.154
+++ purity.m	16 Apr 2012 05:56:08 -0000
@@ -167,6 +167,7 @@
 :- implementation.
 
 :- import_module check_hlds.post_typecheck.
+:- import_module hlds.from_ground_term_util.
 :- import_module hlds.goal_util.
 :- import_module hlds.hlds_clauses.
 :- import_module hlds.hlds_error_util.
@@ -589,15 +590,21 @@
     Goal0 = hlds_goal(GoalExpr0, GoalInfo0),
     compute_expr_purity(GoalExpr0, GoalExpr, GoalInfo0, Purity, ContainsTrace,
         !Info),
-    goal_info_set_purity(Purity, GoalInfo0, GoalInfo1),
+    update_purity_ct_in_goal_info(Purity, ContainsTrace, GoalInfo0, GoalInfo),
+    Goal = hlds_goal(GoalExpr, GoalInfo).
+
+:- pred update_purity_ct_in_goal_info(purity::in, contains_trace_goal::in,
+    hlds_goal_info::in, hlds_goal_info::out) is det.
+
+update_purity_ct_in_goal_info(Purity, ContainsTrace, !GoalInfo) :-
+    goal_info_set_purity(Purity, !GoalInfo),
     (
         ContainsTrace = contains_trace_goal,
-        goal_info_add_feature(feature_contains_trace, GoalInfo1, GoalInfo)
+        goal_info_add_feature(feature_contains_trace, !GoalInfo)
     ;
         ContainsTrace = contains_no_trace_goal,
-        goal_info_remove_feature(feature_contains_trace, GoalInfo1, GoalInfo)
-    ),
-    Goal = hlds_goal(GoalExpr, GoalInfo).
+        goal_info_remove_feature(feature_contains_trace, !GoalInfo)
+    ).
 
     % Compute the purity of a list of hlds_goals. Since the purity of a
     % disjunction is computed the same way as the purity of a conjunction,
@@ -730,7 +737,7 @@
             contains_no_trace_goal, ContainsTrace, !Info),
         GoalExpr = switch(Var, Canfail, Cases)
     ;
-        GoalExpr0 = unify(LHS, RHS0, Mode, Unification, UnifyContext),
+        GoalExpr0 = unify(LHSVar, RHS0, Mode, Unification, UnifyContext),
         (
             RHS0 = rhs_lambda_goal(LambdaPurity, Groundness, PredOrFunc,
                 EvalMethod, LambdaNonLocals, LambdaQuantVars,
@@ -743,8 +750,10 @@
                 EvalMethod, LambdaNonLocals, LambdaQuantVars,
                 LambdaModes, LambdaDetism, LambdaGoal),
 
-            check_closure_purity(GoalInfo, LambdaPurity, GoalPurity, !Info),
-            GoalExpr = unify(LHS, RHS, Mode, Unification, UnifyContext),
+            check_closure_purity(GoalInfo, LambdaPurity, GoalPurity,
+                ClosureSpecs),
+            purity_info_add_messages(ClosureSpecs, !Info),
+            GoalExpr = unify(LHSVar, RHS, Mode, Unification, UnifyContext),
             % The unification itself is always pure,
             % even if the lambda expression body is impure.
             DeclaredPurity = goal_info_get_purity(GoalInfo),
@@ -769,9 +778,9 @@
                 PredInfo0 = !.Info ^ pi_pred_info,
                 VarTypes0 = !.Info ^ pi_vartypes,
                 VarSet0 = !.Info ^ pi_varset,
-                post_typecheck.resolve_unify_functor(LHS, ConsId, Args, Mode,
-                    Unification, UnifyContext, GoalInfo, ModuleInfo,
-                    PredInfo0, PredInfo, VarTypes0, VarTypes, VarSet0, VarSet,
+                post_typecheck.resolve_unify_functor(LHSVar, ConsId, Args,
+                    Mode, Unification, UnifyContext, GoalInfo, ModuleInfo,
+                    PredInfo0, PredInfo, VarSet0, VarSet, VarTypes0, VarTypes,
                     Goal1, IsPlainUnify),
                 !Info ^ pi_vartypes := VarTypes,
                 !Info ^ pi_varset := VarSet,
@@ -787,8 +796,10 @@
                 Goal1 = hlds_goal(GoalExpr0, GoalInfo)
             ),
             ( Goal1 = hlds_goal(unify(_, _, _, _, _), _) ->
-                check_higher_order_purity(GoalInfo, ConsId, LHS, Args,
-                    ActualPurity, !Info),
+                check_var_functor_unify_purity(!.Info, GoalInfo,
+                    LHSVar, ConsId, Args, UnifySpecs),
+                purity_info_add_messages(UnifySpecs, !Info),
+                ActualPurity = purity_pure,
                 ContainsTrace = contains_no_trace_goal,
                 Goal = Goal1
             ;
@@ -825,30 +836,85 @@
         (
             Reason0 = promise_purity(PromisedPurity),
             compute_goal_purity(SubGoal0, SubGoal, _, ContainsTrace, !Info),
-            Purity = PromisedPurity,
-            Reason = Reason0
+            GoalExpr = scope(Reason0, SubGoal),
+            Purity = PromisedPurity
         ;
             Reason0 = from_ground_term(TermVar, Kind0),
-            % We have not yet classified from_ground_term scopes into
-            % from_ground_term_construct and other kinds, which is a pity,
-            % since from_ground_term_construct scopes do not need purity
-            % checking.
-            % XXX However, from_ground_term scopes *are* guaranteed to be
-            % conjunctions of unifications, and we could take advantage of
-            % that, e.g. by avoiding repeatedly taking the varset and vartypes
-            % out of !Info and just as repeatedly putting it back again.
+            (
+                ( Kind0 = from_ground_term_initial
+                ; Kind0 = from_ground_term_construct
+                ),
+                SubGoal0 = hlds_goal(SubGoalExpr0, SubGoalInfo0),
+                ( SubGoalExpr0 = conj(plain_conj, SubGoals0Prime) ->
+                    SubGoals0 = SubGoals0Prime
+                ;
+                    unexpected($module, $pred,
+                        "from_ground_term_initial goal is not plain conj")
+                ),
+                PostTypeCheck = !.Info ^ pi_run_post_typecheck,
+                (
+                    PostTypeCheck = run_post_typecheck,
+                    compute_goal_purity_in_fgt_ptc(SubGoals0,
+                        [], RevMarkedSubGoals, purity_pure, Purity,
+                        contains_no_trace_goal, ContainsTrace, !Info,
+                        fgt_invariants_kept, Invariants),
+                    (
+                        Invariants = fgt_invariants_kept,
+                        list.map(project_kept_goal,
+                            RevMarkedSubGoals, RevSubGoals),
+                        list.reverse(RevSubGoals, SubGoals),
+                        SubGoalExpr = conj(plain_conj, SubGoals),
+                        update_purity_ct_in_goal_info(Purity, ContainsTrace,
+                            SubGoalInfo0, SubGoalInfo),
+                        SubGoal = hlds_goal(SubGoalExpr, SubGoalInfo),
+                        GoalExpr = scope(Reason0, SubGoal)
+                    ;
+                        Invariants = fgt_invariants_broken,
+                        (
+                            Kind0 = from_ground_term_initial,
+                            ConstructOrderMarkedSubGoals = RevMarkedSubGoals,
+                            Order = deconstruct_top_down
+                        ;
+                            Kind0 = from_ground_term_construct,
+                            list.reverse(RevMarkedSubGoals,
+                                ConstructOrderMarkedSubGoals),
+                            Order = construct_bottom_up
+                        ),
+                        introduce_partial_fgt_scopes(GoalInfo, SubGoalInfo0,
+                            ConstructOrderMarkedSubGoals, Order, SubGoal),
+                        % Delete the scope wrapper around SubGoal0.
+                        SubGoal = hlds_goal(GoalExpr, _)
+                    )
+                ;
+                    PostTypeCheck = do_not_run_post_typecheck,
+                    GoalExpr = GoalExpr0,
+                    compute_goal_purity_in_fgt_no_ptc(SubGoals0, !.Info,
+                        [], Specs),
+                    purity_info_add_messages(Specs, !Info),
+                    Purity = purity_pure,
+                    ContainsTrace = contains_no_trace_goal
+                )
+            ;
+                ( Kind0 = from_ground_term_deconstruct
+                ; Kind0 = from_ground_term_other
+                ),
             !Info ^ pi_converted_unify := have_not_converted_unify,
             compute_goal_purity(SubGoal0, SubGoal, Purity, ContainsTrace,
                 !Info),
             HaveConvertedUnify = !.Info ^ pi_converted_unify,
             (
                 HaveConvertedUnify = have_not_converted_unify,
-                Kind = Kind0
+                    GoalExpr = scope(Reason0, SubGoal)
             ;
                 HaveConvertedUnify = have_converted_unify,
-                Kind = from_ground_term_other
-            ),
-            Reason = from_ground_term(TermVar, Kind)
+                    % We could delete the scope. However, there may be
+                    % some compiler passes than could benefit from it,
+                    % and I expect we will get here rarely enough that
+                    % what we do here does not matter all that much.
+                    Reason = from_ground_term(TermVar, from_ground_term_other),
+                    GoalExpr = scope(Reason, SubGoal)
+                )
+            )
         ;
             ( Reason0 = promise_solutions(_, _)
             ; Reason0 = require_detism(_)
@@ -859,20 +925,19 @@
             ),
             compute_goal_purity(SubGoal0, SubGoal, Purity, ContainsTrace,
                 !Info),
-            Reason = Reason0
+            GoalExpr = scope(Reason0, SubGoal)
         ;
             Reason0 = trace_goal(_, _, _, _, _),
             compute_goal_purity(SubGoal0, SubGoal, _SubPurity, _, !Info),
+            GoalExpr = scope(Reason0, SubGoal),
             Purity = purity_pure,
-            ContainsTrace = contains_trace_goal,
-            Reason = Reason0
+            ContainsTrace = contains_trace_goal
         ;
             % Purity checking happens before the introduction of loop control
             % scopes.
             Reason0 = loop_control(_, _, _),
             unexpected($module, $pred, "loop_control")
-        ),
-        GoalExpr = scope(Reason, SubGoal)
+        )
     ;
         GoalExpr0 = if_then_else(Vars, Cond0, Then0, Else0),
         compute_goal_purity(Cond0, Cond, Purity1, ContainsTrace1, !Info),
@@ -971,6 +1036,123 @@
 
 %-----------------------------------------------------------------------------%
 %
+% Auxiliary procedures for handling from_ground_term scopes.
+%
+
+:- pred compute_goal_purity_in_fgt_ptc(list(hlds_goal)::in,
+    list(fgt_marked_goal)::in, list(fgt_marked_goal)::out,
+    purity::in, purity::out, contains_trace_goal::in, contains_trace_goal::out,
+    purity_info::in, purity_info::out,
+    fgt_invariants_status::in, fgt_invariants_status::out) is det.
+
+compute_goal_purity_in_fgt_ptc([], !RevMarkedSubGoals,
+        !Purity, !ContainsTrace, !Info, !Invariants).
+compute_goal_purity_in_fgt_ptc([Goal0 | Goals0], !RevMarkedSubGoals,
+        !Purity, !ContainsTrace, !Info, !Invariants) :-
+    Goal0 = hlds_goal(GoalExpr0, GoalInfo0),
+    (
+        GoalExpr0 = unify(XVarPrime, Y, ModePrime, UnificationPrime,
+            UnifyContextPrime),
+        Y = rhs_functor(ConsIdPrime, _, YVarsPrime)
+    ->
+        XVar = XVarPrime,
+        Mode = ModePrime,
+        Unification = UnificationPrime,
+        UnifyContext = UnifyContextPrime,
+        ConsId = ConsIdPrime,
+        YVars = YVarsPrime
+    ;
+        unexpected($module, $pred,
+            "from_ground_term_initial conjunct is not functor unify")
+    ),
+    ModuleInfo = !.Info ^ pi_module_info,
+    PredInfo0 = !.Info ^ pi_pred_info,
+    VarTypes0 = !.Info ^ pi_vartypes,
+    VarSet0 = !.Info ^ pi_varset,
+    post_typecheck.resolve_unify_functor(XVar, ConsId, YVars, Mode,
+        Unification, UnifyContext, GoalInfo0, ModuleInfo,
+        PredInfo0, PredInfo, VarSet0, VarSet, VarTypes0, VarTypes,
+        Goal1, IsPlainUnify),
+    Goal1 = hlds_goal(GoalExpr1, GoalInfo1),
+    (
+        IsPlainUnify = is_plain_unify,
+        trace [compiletime(flag("purity_fgt_sanity_tests"))] (
+            ( GoalExpr1 = unify(_, _, _, _, _) ->
+                true
+            ;
+                unexpected($module, $pred, "is_plain_unify goal is not unify")
+            ),
+            expect(unify(PredInfo0, PredInfo),
+                $module, $pred, "PredInfo != PredInfo"),
+            expect(unify(VarSet0, VarSet),
+                $module, $pred, "VarSet != VarSet"),
+            expect(unify(VarTypes0, VarTypes),
+                $module, $pred, "VarTypes != VarTypes")
+        ),
+        check_var_functor_unify_purity(!.Info, GoalInfo0, XVar, ConsId, YVars,
+            UnifySpecs),
+        purity_info_add_messages(UnifySpecs, !Info),
+        % !Purity and !ContainsTrace are unchanged.
+        update_purity_ct_in_goal_info(purity_pure, contains_no_trace_goal,
+            GoalInfo1, GoalInfo),
+        Goal = hlds_goal(GoalExpr1, GoalInfo),
+        % Goal may be different from Goal0 (e.g. it may have the cons_id
+        % module qualified), but if resolve_unify_functor returned
+        % is_plain_unify, then the change does not invalidate
+        % the invariants of from_ground_term_{initial,construct} scopes.
+        MarkedSubGoal = fgt_kept_goal(Goal, XVar, YVars)
+        % !Invariants is unchanged.
+    ;
+        IsPlainUnify = is_not_plain_unify,
+        !Info ^ pi_vartypes := VarTypes,
+        !Info ^ pi_varset := VarSet,
+        !Info ^ pi_pred_info := PredInfo,
+        ( GoalExpr1 = unify(_, _, _, _, _) ->
+            check_var_functor_unify_purity(!.Info, GoalInfo0,
+                XVar, ConsId, YVars, UnifySpecs),
+            purity_info_add_messages(UnifySpecs, !Info),
+            update_purity_ct_in_goal_info(purity_pure, contains_no_trace_goal,
+                GoalInfo1, GoalInfo),
+            Goal = hlds_goal(GoalExpr1, GoalInfo)
+            % !Purity and !ContainsTrace are unchanged.
+        ;
+            compute_goal_purity(Goal1, Goal, GoalPurity, GoalContainsTrace,
+                !Info),
+            !:Purity = worst_purity(GoalPurity, !.Purity),
+            !:ContainsTrace = worst_contains_trace(GoalContainsTrace,
+                !.ContainsTrace)
+        ),
+        MarkedSubGoal = fgt_broken_goal(Goal, XVar, YVars),
+        !:Invariants = fgt_invariants_broken
+    ),
+    !:RevMarkedSubGoals = [MarkedSubGoal | !.RevMarkedSubGoals],
+    compute_goal_purity_in_fgt_ptc(Goals0, !RevMarkedSubGoals,
+        !Purity, !ContainsTrace, !Info, !Invariants).
+
+:- pred compute_goal_purity_in_fgt_no_ptc(list(hlds_goal)::in,
+    purity_info::in, list(error_spec)::in, list(error_spec)::out) is det.
+
+compute_goal_purity_in_fgt_no_ptc([], _, !Specs).
+compute_goal_purity_in_fgt_no_ptc([Goal0 | Goals0], Info, !Specs) :-
+    Goal0 = hlds_goal(GoalExpr0, GoalInfo0),
+    (
+        GoalExpr0 = unify(XVarPrime, Y, _, _, _),
+        Y = rhs_functor(ConsIdPrime, _, YVarsPrime)
+    ->
+        XVar = XVarPrime,
+        ConsId = ConsIdPrime,
+        YVars = YVarsPrime
+    ;
+        unexpected($module, $pred,
+            "from_ground_term_initial conjunct is not functor unify")
+    ),
+    check_var_functor_unify_purity(Info, GoalInfo0, XVar, ConsId, YVars,
+        UnifySpecs),
+    !:Specs = UnifySpecs ++ !.Specs,
+    compute_goal_purity_in_fgt_no_ptc(Goals0, Info, !Specs).
+
+%-----------------------------------------------------------------------------%
+%
 % Auxiliary procedures for handling plain calls.
 %
 
@@ -1029,19 +1211,19 @@
 
 %-----------------------------------------------------------------------------%
 %
-% Auxiliary procedures for handling higher order calls.
+% Auxiliary procedures for handling unifications.
 %
 
-:- pred check_higher_order_purity(hlds_goal_info::in, cons_id::in,
-    prog_var::in, list(prog_var)::in, purity::out,
-    purity_info::in, purity_info::out) is det.
-
-check_higher_order_purity(GoalInfo, ConsId, Var, Args, ActualPurity, !Info) :-
-    % Check that the purity of the ConsId matches the purity of the
-    % variable's type.
-    VarTypes = !.Info ^ pi_vartypes,
+:- pred check_var_functor_unify_purity(purity_info::in, hlds_goal_info::in,
+    prog_var::in, cons_id::in, list(prog_var)::in, list(error_spec)::out)
+    is det.
+
+check_var_functor_unify_purity(Info, GoalInfo, Var, ConsId, Args, Specs) :-
+    % If the unification involves a higher order RHS, check that
+    % the purity of the ConsId matches the purity of the variable's type.
+    VarTypes = Info ^ pi_vartypes,
     map.lookup(VarTypes, Var, TypeOfVar),
-    PredInfo = !.Info ^ pi_pred_info,
+    PredInfo = Info ^ pi_pred_info,
     pred_info_get_markers(PredInfo, CallerMarkers),
     Context = goal_info_get_context(GoalInfo),
     (
@@ -1054,7 +1236,7 @@
         pred_info_get_head_type_params(PredInfo, HeadTypeParams),
         map.apply_to_list(Args, VarTypes, ArgTypes0),
         list.append(ArgTypes0, VarArgTypes, PredArgTypes),
-        ModuleInfo = !.Info ^ pi_module_info,
+        ModuleInfo = Info ^ pi_module_info,
         (
             get_pred_id_by_types(calls_are_fully_qualified(CallerMarkers),
                 PName, PredOrFunc, TVarSet, ExistQTVars, PredArgTypes,
@@ -1062,21 +1244,21 @@
         ->
             module_info_pred_info(ModuleInfo, CalleePredId, CalleePredInfo),
             pred_info_get_purity(CalleePredInfo, CalleePurity),
-            check_closure_purity(GoalInfo, TypePurity, CalleePurity, !Info)
+            check_closure_purity(GoalInfo, TypePurity, CalleePurity,
+                ClosureSpecs)
         ;
             % If we can't find the type of the function, it is because
             % typecheck couldn't give it one. Typechecking gives an error
             % in this case, we just keep silent.
-            true
+            ClosureSpecs = []
         )
     ;
-        true
+        % No closure; no specs.
+        ClosureSpecs = []
     ),
 
     % The unification itself is always pure,
     % even if it is a unification with an impure higher-order term.
-    ActualPurity = purity_pure,
-
     % Check for a bogus purity annotation on the unification.
     DeclaredPurity = goal_info_get_purity(GoalInfo),
     (
@@ -1086,28 +1268,29 @@
         % Don't warn about bogus purity annotations in compiler-generated
         % mutable predicates.
         ( check_marker(CallerMarkers, marker_mutable_access_pred) ->
-            true
+            Specs = ClosureSpecs
         ;
             Spec = impure_unification_expr_error(Context, DeclaredPurity),
-            purity_info_add_message(Spec, !Info)
+            Specs = [Spec | ClosureSpecs]
         )
     ;
-        DeclaredPurity = purity_pure
+        DeclaredPurity = purity_pure,
+        Specs = ClosureSpecs
     ).
 
 :- pred check_closure_purity(hlds_goal_info::in, purity::in, purity::in,
-    purity_info::in, purity_info::out) is det.
+    list(error_spec)::out) is det.
 
-check_closure_purity(GoalInfo, DeclaredPurity, ActualPurity, !Info) :-
+check_closure_purity(GoalInfo, DeclaredPurity, ActualPurity, Specs) :-
     ( less_pure(ActualPurity, DeclaredPurity) ->
         Context = goal_info_get_context(GoalInfo),
         Spec = report_error_closure_purity(Context,
             DeclaredPurity, ActualPurity),
-        purity_info_add_message(Spec, !Info)
+        Specs = [Spec]
     ;
         % We don't bother to warn if the DeclaredPurity is less pure than the
         % ActualPurity; that would lead to too many spurious warnings.
-        true
+        Specs = []
     ).
 
 %-----------------------------------------------------------------------------%
@@ -1412,8 +1595,23 @@
 :- pred purity_info_add_message(error_spec::in,
     purity_info::in, purity_info::out) is det.
 
-purity_info_add_message(Spec, Info0, Info) :-
-    Info = Info0 ^ pi_messages := [Spec | Info0 ^ pi_messages].
+purity_info_add_message(Spec, !Info) :-
+    Msgs0 = !.Info ^ pi_messages,
+    Msgs = [Spec | Msgs0],
+    !Info ^ pi_messages := Msgs.
+
+:- pred purity_info_add_messages(list(error_spec)::in,
+    purity_info::in, purity_info::out) is det.
+
+purity_info_add_messages(Specs, !Info) :-
+    (
+        Specs = []
+    ;
+        Specs = [_ | _],
+        Msgs0 = !.Info ^ pi_messages,
+        Msgs = Specs ++ Msgs0,
+        !Info ^ pi_messages := Msgs
+    ).
 
 %-----------------------------------------------------------------------------%
 :- end_module check_hlds.purity.
Index: qual_info.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/qual_info.m,v
retrieving revision 1.28
diff -u -b -r1.28 qual_info.m
--- qual_info.m	5 May 2011 07:11:51 -0000	1.28
+++ qual_info.m	15 Apr 2012 15:34:13 -0000
@@ -237,22 +237,22 @@
 
 %-----------------------------------------------------------------------------%
 
-make_atomic_unification(Var, Rhs, Context, MainContext, SubContext,
+make_atomic_unification(Var, RHS, Context, MainContext, SubContext,
         Goal, !QualInfo) :-
-    make_atomic_unification(Var, Rhs, Context, MainContext, SubContext,
+    make_atomic_unification(Var, RHS, Context, MainContext, SubContext,
             purity_pure, Goal, !QualInfo).
 
-make_atomic_unification(Var, Rhs, Context, MainContext, SubContext, Purity,
+make_atomic_unification(Var, RHS, Context, MainContext, SubContext, Purity,
         Goal, !QualInfo) :-
     (
-        Rhs = rhs_var(_)
+        RHS = rhs_var(_)
     ;
-        Rhs = rhs_lambda_goal(_, _, _, _, _, _, _, _, _)
+        RHS = rhs_lambda_goal(_, _, _, _, _, _, _, _, _)
     ;
-        Rhs = rhs_functor(ConsId, _, _),
+        RHS = rhs_functor(ConsId, _, _),
         record_used_functor(ConsId, !QualInfo)
     ),
-    create_atomic_complicated_unification(Var, Rhs, Context,
+    create_atomic_complicated_unification(Var, RHS, Context,
         MainContext, SubContext, Purity, Goal).
 
 record_called_pred_or_func(PredOrFunc, SymName, Arity, !QualInfo) :-
Index: superhomogeneous.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/superhomogeneous.m,v
retrieving revision 1.51
diff -u -b -r1.51 superhomogeneous.m
--- superhomogeneous.m	13 Apr 2012 09:10:22 -0000	1.51
+++ superhomogeneous.m	16 Apr 2012 06:38:48 -0000
@@ -7,7 +7,8 @@
 %-----------------------------------------------------------------------------%
 %
 % File: superhomogeneous.m.
-% Main author: fjh.
+% Main author of the original version of this module: fjh.
+% Main author of the current version of this module: zs.
 %
 % This module performs the conversion of clause bodies
 % to superhomogeneous form.
@@ -44,12 +45,6 @@
                 unify_sub_contexts
             ).
 
-    % We count how many goals we insert in the course of a call to one of the
-    % predicates below. We compute this count because we want to wrap a
-    % from_ground_term scope only around goals where it saves us nontrivial
-    % time (since the scope itself adds overhead).
-:- type num_added_goals == int.
-
     % `insert_arg_unifications' takes a list of variables, a list of terms
     % to unify them with, and a goal, and inserts the appropriate unifications
     % onto the front of the goal. It calls `unravel_unification' to ensure that
@@ -60,7 +55,6 @@
     %
 :- pred insert_arg_unifications(list(prog_var)::in, list(prog_term)::in,
     prog_context::in, arg_context::in, hlds_goal::in, hlds_goal::out,
-    num_added_goals::in, num_added_goals::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out,
     module_info::in, module_info::out, qual_info::in, qual_info::out,
@@ -69,43 +63,32 @@
 :- pred insert_arg_unifications_with_contexts(list(prog_var)::in,
     list(prog_term)::in, assoc_list(int, arg_context)::in, prog_context::in,
     hlds_goal::in, hlds_goal::out,
-    num_added_goals::in, num_added_goals::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out, module_info::in, module_info::out,
     qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-    % append_arg_unifications is the same as insert_arg_unifications,
-    % except that the unifications are added after the goal rather
-    % than before the goal.
-    %
-:- pred append_arg_unifications(list(prog_var)::in, list(prog_term)::in,
-    prog_context::in, arg_context::in, hlds_goal::in, hlds_goal::out,
-    num_added_goals::in, num_added_goals::out,
-    svar_state::in, svar_state::out, svar_store::in, svar_store::out,
-    prog_varset::in, prog_varset::out,
-    module_info::in, module_info::out, qual_info::in, qual_info::out,
-    list(error_spec)::in, list(error_spec)::out) is det.
-
 :- pred unravel_unification(prog_term::in, prog_term::in, prog_context::in,
     unify_main_context::in, unify_sub_contexts::in, purity::in,
-    hlds_goal::out, num_added_goals::in, num_added_goals::out,
+    hlds_goal::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out,
     module_info::in, module_info::out, qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-    % make_fresh_arg_vars(Args, Vars, !VarSet, !SVarState, !Specs):
+    % make_fresh_arg_vars_subst_svars(Args, Vars, !VarSet, !SVarState, !Specs):
     %
     % Vars is a list of distinct variables corresponding to the terms in Args.
     % For each term in Args, if the term is a variable V which is distinct
     % from the variables already produced, then the corresponding variable
     % in Vars is just V, otherwise we allocate a fresh variable from !VarSet.
     % !:VarSet is the varset resulting after all the necessary variables
-    % have been allocated. !SVarState and !Specs are required to handle
-    % state variables.
+    % have been allocated. If any of the Args is of the form !.S or !:S,
+    % we do state var substitution for them. We need !SVarState for correct
+    % state var references, and !Specs for incorrect state var references.
     %
-:- pred make_fresh_arg_vars(list(prog_term)::in, list(prog_var)::out,
+:- pred make_fresh_arg_vars_subst_svars(list(prog_term)::in,
+    list(prog_var)::out,
     prog_varset::in, prog_varset::out, svar_state::in, svar_state::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
@@ -115,6 +98,7 @@
 :- implementation.
 
 :- import_module check_hlds.mode_util.
+:- import_module hlds.from_ground_term_util.
 :- import_module hlds.goal_util.
 :- import_module hlds.hlds_out.
 :- import_module hlds.hlds_out.hlds_out_goal.
@@ -132,6 +116,7 @@
 :- import_module parse_tree.set_of_var.
 
 :- import_module bool.
+:- import_module cord.
 :- import_module int.
 :- import_module io.
 :- import_module map.
@@ -143,477 +128,449 @@
 
 %-----------------------------------------------------------------------------%
 
-insert_arg_unifications(HeadVars, Args0, Context, ArgContext, !Goal, !NumAdded,
+insert_arg_unifications(XVars, XArgTerms0, Context, ArgContext, Goal0, Goal,
         !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
-    substitute_state_var_mappings(Args0, Args, !VarSet, !SVarState, !Specs),
-    do_insert_arg_unifications(HeadVars, Args, Context, ArgContext, !Goal,
-        get_maybe_from_ground_term_threshold, !NumAdded,
-        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs).
-
-insert_arg_unifications_with_contexts(Vars, Args0, ArgContexts,
-        Context, !Goal, !NumAdded, !SVarState, !SVarStore,
-        !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
-    substitute_state_var_mappings(Args0, Args, !VarSet, !SVarState, !Specs),
-    do_insert_arg_unifications_with_contexts(Vars, Args, ArgContexts, Context,
-        !Goal, get_maybe_from_ground_term_threshold, !NumAdded,
-        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs).
+    substitute_state_var_mappings(XArgTerms0, XArgTerms,
+        !VarSet, !SVarState, !Specs),
+    do_arg_unifications(XVars, XArgTerms, Context, ArgContext,
+        construct_bottom_up, 1, Expansions,
+        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
+    Goal0 = hlds_goal(_, GoalInfo0),
+    insert_expansions_before_goal_top_not_fgti(GoalInfo0, Expansions,
+        Goal0, Goal).
 
-append_arg_unifications(HeadVars, Args0, Context, ArgContext, !Goal, !NumAdded,
-        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
-    substitute_state_var_mappings(Args0, Args, !VarSet, !SVarState, !Specs),
-    do_append_arg_unifications(HeadVars, Args, Context, ArgContext, !Goal,
-        get_maybe_from_ground_term_threshold, !NumAdded,
-        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs).
+insert_arg_unifications_with_contexts(XVars, XArgTerms0, ArgContexts, Context,
+        Goal0, Goal, !SVarState, !SVarStore, !VarSet,
+        !ModuleInfo, !QualInfo, !Specs) :-
+    substitute_state_var_mappings(XArgTerms0, XArgTerms,
+        !VarSet, !SVarState, !Specs),
+    do_arg_unifications_with_contexts(XVars, XArgTerms, ArgContexts, Context,
+        construct_bottom_up, Expansions,
+        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
+    Goal0 = hlds_goal(_, GoalInfo0),
+    insert_expansions_before_goal_top_not_fgti(GoalInfo0, Expansions,
+        Goal0, Goal).
 
 unravel_unification(LHS0, RHS0, Context, MainContext, SubContext, Purity,
-        Goal, !NumAdded, !SVarState, !SVarStore, !VarSet,
+        Goal, !SVarState, !SVarStore, !VarSet,
         !ModuleInfo, !QualInfo, !Specs) :-
+    (
+        Purity = purity_pure,
+        Order = deconstruct_top_down
+    ;
+        ( Purity = purity_semipure
+        ; Purity = purity_impure
+        ),
+        Order = construct_bottom_up
+    ),
     do_unravel_unification(LHS0, RHS0, Context, MainContext, SubContext,
-        Purity, Goal, get_maybe_from_ground_term_threshold, !NumAdded,
-        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs).
+        Purity, Order, Expansion,
+        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
+    goal_info_init(Context, GoalInfo),
+    expansion_to_goal_wrap_if_fgti(GoalInfo, Expansion, Goal).
 
 %-----------------------------------------------------------------------------%
 
-:- pred do_insert_arg_unifications(list(prog_var)::in, list(prog_term)::in,
-    prog_context::in, arg_context::in,
-    hlds_goal::in, hlds_goal::out, maybe(int)::in,
-    num_added_goals::in, num_added_goals::out,
-    svar_state::in, svar_state::out, svar_store::in, svar_store::out,
-    prog_varset::in, prog_varset::out, module_info::in, module_info::out,
-    qual_info::in, qual_info::out,
-    list(error_spec)::in, list(error_spec)::out) is det.
+:- type maybe_fgti_var_size
+    --->    not_fgti
+    ;       fgti_var_size(prog_var, int).
+
+:- type expansion
+    --->    expansion(
+                maybe_fgti_var_size,
+                cord(hlds_goal)
+            ).
 
-do_insert_arg_unifications(HeadVars, Args, Context, ArgContext,
-        !Goal, MaybeThreshold, !NumAdded, !SVarState, !SVarStore, !VarSet,
-        !ModuleInfo, !QualInfo, !Specs) :-
+%-----------------------------------------------------------------------------%
+
+:- pred expansion_to_goal_wrap_if_fgti(hlds_goal_info::in, expansion::in,
+    hlds_goal::out) is det.
+
+expansion_to_goal_wrap_if_fgti(GoalInfo, Expansion, Goal) :-
+    Expansion = expansion(MaybeFGTI, GoalCord),
+    Goals = cord.list(GoalCord),
     (
-        HeadVars = [],
-        expect(unify(Args, []), $module, $pred, "length mismatch 0")
+        Goals = [],
+        Goal = hlds_goal(true_goal_expr, GoalInfo)
     ;
-        HeadVars = [HeadVar1 | HeadVarsAfter1],
-        !.Goal = hlds_goal(_, GoalInfo0),
-        goal_info_set_context(Context, GoalInfo0, GoalInfo),
-        svar_goal_to_conj_list(!.Goal, Goals0, !SVarStore),
-
-        (
-            Args = [],
-            unexpected($module, $pred, "length mismatch 0")
-        ;
-            Args = [Arg1 | ArgsAfter1],
-            do_arg_unification(HeadVar1, Arg1, Context, ArgContext,
-                1, ArgUnifyConj1, MaybeThreshold,
-                !NumAdded, !SVarState, !SVarStore,
-                !VarSet, !ModuleInfo, !QualInfo, !Specs),
-
+        Goals = [Goal]
+    ;
+        Goals = [_, _ | _],
             (
-                HeadVarsAfter1 = [],
-                ArgsAfter1 = [],
-                Goals = ArgUnifyConj1 ++ Goals0,
-                conj_list_to_goal(Goals, GoalInfo, !:Goal)
-            ;
-                HeadVarsAfter1 = [],
-                ArgsAfter1 = [_ | _],
-                unexpected($module, $pred, "length mismatch 1")
-            ;
-                HeadVarsAfter1 = [_ | _],
-                ArgsAfter1 = [],
-                unexpected($module, $pred, "length mismatch 1")
-            ;
-                HeadVarsAfter1 = [HeadVar2 | HeadVarsAfter2],
-                ArgsAfter1 = [Arg2 | ArgsAfter2],
-                do_arg_unification(HeadVar2, Arg2, Context, ArgContext,
-                    2, ArgUnifyConj2, MaybeThreshold,
-                    !NumAdded, !SVarState, !SVarStore,
-                    !VarSet, !ModuleInfo, !QualInfo, !Specs),
+            MaybeFGTI = fgti_var_size(TermVar, Size),
+            get_maybe_from_ground_term_threshold = yes(Threshold),
+            Size >= Threshold
+        ->
+            goal_info_set_nonlocals(set_of_var.make_singleton(TermVar),
+                GoalInfo, MarkedGoalInfo),
+            mark_nonlocals_in_ground_term_construct(Goals, MarkedGoals),
+            ConjGoalExpr = conj(plain_conj, MarkedGoals),
+            ConjGoal = hlds_goal(ConjGoalExpr, MarkedGoalInfo),
+            Reason = from_ground_term(TermVar, from_ground_term_initial),
+            ScopeGoalExpr = scope(Reason, ConjGoal),
+            ScopeGoal = hlds_goal(ScopeGoalExpr, MarkedGoalInfo),
+            Goal = ScopeGoal
+        ;
+            ConjGoalExpr = conj(plain_conj, Goals),
+            ConjGoal = hlds_goal(ConjGoalExpr, GoalInfo),
+            Goal = ConjGoal
+        )
+    ).
+
+:- pred expansion_to_goal_cord_wrap_if_fgti(hlds_goal_info::in, expansion::in,
+    cord(hlds_goal)::out) is det.
+
+expansion_to_goal_cord_wrap_if_fgti(GoalInfo, Expansion,
+        MaybeWrappedGoalCord) :-
+    Expansion = expansion(MaybeFGTI, GoalCord),
+    (
+        MaybeFGTI = fgti_var_size(TermVar, Size),
+        get_maybe_from_ground_term_threshold = yes(Threshold),
+        Size >= Threshold
+    ->
+        Goals = cord.list(GoalCord),
+        goal_info_set_nonlocals(set_of_var.make_singleton(TermVar),
+            GoalInfo, MarkedGoalInfo),
+        mark_nonlocals_in_ground_term_construct(Goals, MarkedGoals),
+        ConjGoalExpr = conj(plain_conj, MarkedGoals),
+        ConjGoal = hlds_goal(ConjGoalExpr, MarkedGoalInfo),
+        Reason = from_ground_term(TermVar, from_ground_term_initial),
+        ScopeGoalExpr = scope(Reason, ConjGoal),
+        ScopeGoal = hlds_goal(ScopeGoalExpr, MarkedGoalInfo),
+        MaybeWrappedGoalCord = cord.singleton(ScopeGoal)
+    ;
+        MaybeWrappedGoalCord = GoalCord
+    ).
 
+:- pred mark_nonlocals_in_ground_term_construct(
+    list(hlds_goal)::in, list(hlds_goal)::out) is det.
+
+mark_nonlocals_in_ground_term_construct([], []).
+mark_nonlocals_in_ground_term_construct([Goal0 | Goals0], [Goal | Goals]) :-
+    Goal0 = hlds_goal(GoalExpr, GoalInfo0),
                 (
-                    HeadVarsAfter2 = [],
-                    ArgsAfter2 = [],
-                    Goals = ArgUnifyConj1 ++ ArgUnifyConj2 ++ Goals0,
-                    conj_list_to_goal(Goals, GoalInfo, !:Goal)
-                ;
-                    HeadVarsAfter2 = [],
-                    ArgsAfter2 = [_ | _],
-                    unexpected($module, $pred, "length mismatch 2")
-                ;
-                    HeadVarsAfter2 = [_ | _],
-                    ArgsAfter2 = [],
-                    unexpected($module, $pred, "length mismatch 2")
-                ;
-                    HeadVarsAfter2 = [HeadVar3 | HeadVarsAfter3],
-                    ArgsAfter2 = [Arg3 | ArgsAfter3],
-                    do_arg_unification(HeadVar3, Arg3, Context, ArgContext,
-                        3, ArgUnifyConj3, MaybeThreshold,
-                        !NumAdded, !SVarState, !SVarStore,
-                        !VarSet, !ModuleInfo, !QualInfo, !Specs),
+        GoalExpr = unify(LHSVar, RHS, _, _, _),
+        RHS = rhs_functor(_, _, RHSVars)
+    ->
+        set_of_var.list_to_set([LHSVar | RHSVars], NonLocals),
+        goal_info_set_nonlocals(NonLocals, GoalInfo0, GoalInfo),
+        Goal = hlds_goal(GoalExpr, GoalInfo)
+    ;
+        unexpected($module, $pred, "wrong shape goal")
+    ),
+    mark_nonlocals_in_ground_term_construct(Goals0, Goals).
 
-                    do_insert_arg_unifications_loop(HeadVarsAfter3, ArgsAfter3,
-                        Context, ArgContext, 4, Goals0, Goals4,
-                        MaybeThreshold, !NumAdded, !SVarState, !SVarStore,
-                        !VarSet, !ModuleInfo, !QualInfo, !Specs),
-                    Goals = ArgUnifyConj1 ++ ArgUnifyConj2 ++ ArgUnifyConj3
-                        ++ Goals4,
-                    conj_list_to_goal(Goals, GoalInfo, !:Goal)
-                )
-            )
-        )
+%-----------------------------------------------------------------------------%
+
+:- pred insert_expansion_before_goal_top_not_fgti(hlds_goal_info::in,
+    expansion::in, hlds_goal::in, hlds_goal::out) is det.
+
+insert_expansion_before_goal_top_not_fgti(GoalInfo, Expansion, BaseGoal,
+        Goal) :-
+    goal_to_conj_list(BaseGoal, BaseGoals),
+    expansion_to_goal_cord_wrap_if_fgti(GoalInfo, Expansion,
+        ExpansionGoalCord),
+    ExpansionGoals = cord.list(ExpansionGoalCord),
+    conj_list_to_goal(ExpansionGoals ++ BaseGoals, GoalInfo, Goal).
+
+:- pred insert_expansions_before_goal_top_not_fgti(hlds_goal_info::in,
+    list(expansion)::in, hlds_goal::in, hlds_goal::out) is det.
+
+insert_expansions_before_goal_top_not_fgti(GoalInfo, Expansions, BaseGoal,
+        Goal) :-
+    goal_to_conj_list(BaseGoal, BaseGoals),
+    list.map(expansion_to_goal_cord_wrap_if_fgti(GoalInfo), Expansions,
+        ExpansionGoalCords),
+    ExpansionGoals = cord.cord_list_to_list(ExpansionGoalCords),
+    conj_list_to_goal(ExpansionGoals ++ BaseGoals, GoalInfo, Goal).
+
+:- pred append_expansions_after_goal_top_ftgi(hlds_goal_info::in, prog_var::in,
+    hlds_goal::in, int::in, list(expansion)::in, expansion::out) is det.
+
+append_expansions_after_goal_top_ftgi(GoalInfo, TermVar,
+        BaseGoal, BaseGoalSize, ArgExpansions, Expansion) :-
+    append_expansions_after_goal_top_ftgi_loop(ArgExpansions, yes, AllFGTI,
+        BaseGoalSize, TotalSize),
+    (
+        AllFGTI = no,
+        list.map(expansion_to_goal_cord_wrap_if_fgti(GoalInfo),
+            ArgExpansions, ArgGoalCords),
+        ArgGoalsCord = cord.cord_list_to_cord(ArgGoalCords),
+        % XXX If BaseGoal can be a plain_conj, then we should expand it here.
+        GoalCord = cord.cons(BaseGoal, ArgGoalsCord),
+        Expansion = expansion(not_fgti, GoalCord)
+    ;
+        AllFGTI = yes,
+        list.map(project_expansion_goals, ArgExpansions, ArgGoalCords),
+        ArgGoalsCord = cord.cord_list_to_cord(ArgGoalCords),
+        % XXX If BaseGoal can be a plain_conj, then we should expand it here.
+        GoalCord = cord.cons(BaseGoal, ArgGoalsCord),
+        Expansion = expansion(fgti_var_size(TermVar, TotalSize), GoalCord)
     ).
 
-:- pred do_insert_arg_unifications_loop(list(prog_var)::in,
-    list(prog_term)::in, prog_context::in, arg_context::in, int::in,
-    list(hlds_goal)::in, list(hlds_goal)::out,
-    maybe(int)::in, num_added_goals::in, num_added_goals::out,
+:- pred append_expansions_after_goal_top_ftgi_loop(list(expansion)::in,
+    bool::in, bool::out, int::in, int::out) is det.
+
+append_expansions_after_goal_top_ftgi_loop([], !AllFGTI, !TotalSize).
+append_expansions_after_goal_top_ftgi_loop([Expansion | Expansions],
+        !AllFGTI, !TotalSize) :-
+    Expansion = expansion(MaybeFGTI, _),
+    (
+        MaybeFGTI = not_fgti,
+        !:AllFGTI = no
+    ;
+        MaybeFGTI = fgti_var_size(_, Size),
+        !:TotalSize = !.TotalSize + Size
+    ),
+    append_expansions_after_goal_top_ftgi_loop(Expansions,
+        !AllFGTI, !TotalSize).
+
+:- pred project_expansion_goals(expansion::in, cord(hlds_goal)::out)
+    is det.
+
+project_expansion_goals(expansion(_, GoalCord), GoalCord).
+
+%-----------------------------------------------------------------------------%
+
+:- pred do_arg_unifications(list(prog_var)::in, list(prog_term)::in,
+    prog_context::in, arg_context::in,
+    goal_order::in, int::in, list(expansion)::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out, module_info::in, module_info::out,
     qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-do_insert_arg_unifications_loop([], [_ | _], _, _, _, _, _, _,
-        !NumAdded, !SVarState, !SVarStore, !VarSet,
-        !ModuleInfo, !QualInfo, !Specs) :-
+do_arg_unifications([], [], _Context, _ArgContext,
+        _Order, _ArgNum, [], !SVarState, !SVarStore,
+        !VarSet, !ModuleInfo, !QualInfo, !Specs).
+do_arg_unifications([], [_ | _], _Context, _ArgContext,
+        _Order, _ArgNum, [], !SVarState, !SVarStore,
+        !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
     unexpected($module, $pred, "length mismatch").
-do_insert_arg_unifications_loop([_ | _], [], _, _, _, _, _, _,
-        !NumAdded, !SVarState, !SVarStore, !VarSet,
-        !ModuleInfo, !QualInfo, !Specs) :-
+do_arg_unifications([_ | _], [], _Context, _ArgContext,
+        _Order, _ArgNum, [], !SVarState, !SVarStore,
+        !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
     unexpected($module, $pred, "length mismatch").
-do_insert_arg_unifications_loop([], [], _, _, _, !Goals, _,
-        !NumAdded, !SVarState, !SVarStore, !VarSet,
-        !ModuleInfo, !QualInfo, !Specs).
-do_insert_arg_unifications_loop([HeadVar | HeadVars], [Arg | Args],
-        Context, ArgContext, ArgNum, !Goals, MaybeThreshold,
-        !NumAdded, !SVarState, !SVarStore, !VarSet,
-        !ModuleInfo, !QualInfo, !Specs) :-
-    do_arg_unification(HeadVar, Arg, Context, ArgContext, ArgNum, ArgUnifyConj,
-        MaybeThreshold, !NumAdded, !SVarState, !SVarStore, !VarSet,
-        !ModuleInfo, !QualInfo, !Specs),
-    (
-        ArgUnifyConj = [],
-        % Allow the recursive call to be tail recursive.
-        do_insert_arg_unifications_loop(HeadVars, Args, Context, ArgContext,
-            ArgNum + 1, !Goals, MaybeThreshold, !NumAdded,
-            !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs)
-    ;
-        ArgUnifyConj = [_ | _],
-        do_insert_arg_unifications_loop(HeadVars, Args, Context, ArgContext,
-            ArgNum + 1, !Goals, MaybeThreshold, !NumAdded,
-            !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
-        !:Goals = ArgUnifyConj ++ !.Goals
-    ).
-
-:- pred do_insert_arg_unifications_with_contexts(list(prog_var)::in,
-    list(prog_term)::in, assoc_list(int, arg_context)::in, prog_context::in,
-    hlds_goal::in, hlds_goal::out, maybe(int)::in,
-    num_added_goals::in, num_added_goals::out,
+do_arg_unifications([XVar | XVars], [YTerm | YTerms], Context, ArgContext,
+        Order, ArgNum, [Expansion | Expansions], !SVarState, !SVarStore,
+        !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
+    do_arg_unification(XVar, YTerm, Context, ArgContext, Order, ArgNum,
+        Expansion, !SVarState, !SVarStore,
+        !VarSet, !ModuleInfo, !QualInfo, !Specs),
+    do_arg_unifications(XVars, YTerms, Context, ArgContext, Order, ArgNum + 1,
+        Expansions, !SVarState, !SVarStore,
+        !VarSet, !ModuleInfo, !QualInfo, !Specs).
+
+:- pred do_arg_unifications_with_fresh_vars(list(prog_term)::in,
+    prog_context::in, arg_context::in, goal_order::in, int::in,
+    list(prog_var)::in, list(prog_var)::out, list(expansion)::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out, module_info::in, module_info::out,
     qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-do_insert_arg_unifications_with_contexts(ArgVars, ArgTerms, ArgContexts,
-        Context, !Goal, MaybeThreshold, !NumAdded, !SVarState, !SVarStore,
-        !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
-    (
-        ArgVars = []
-    ;
-        ArgVars = [_ | _],
-        !.Goal = hlds_goal(_, GoalInfo0),
-        svar_goal_to_conj_list(!.Goal, Goals0, !SVarStore),
-        do_insert_arg_unifications_with_contexts_loop(ArgVars, ArgTerms,
-            ArgContexts, Context, Goals0, Goals, MaybeThreshold, !NumAdded,
-            !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
-        goal_info_set_context(Context, GoalInfo0, GoalInfo),
-        conj_list_to_goal(Goals, GoalInfo, !:Goal)
-    ).
+do_arg_unifications_with_fresh_vars([], _Context, _ArgContext,
+        _Order, _ArgNum, _, [], [], !SVarState, !SVarStore,
+        !VarSet, !ModuleInfo, !QualInfo, !Specs).
+do_arg_unifications_with_fresh_vars([YTerm | YTerms], Context, ArgContext,
+        Order, ArgNum, !.SeenXVars, [XVar | XVars], [Expansion | Expansions],
+        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
+    make_fresh_arg_var_no_svar(YTerm, XVar, !.SeenXVars, !VarSet),
+    !:SeenXVars = [XVar | !.SeenXVars],
+    do_arg_unification(XVar, YTerm, Context, ArgContext, Order,
+        ArgNum, Expansion, !SVarState, !SVarStore,
+        !VarSet, !ModuleInfo, !QualInfo, !Specs),
+    do_arg_unifications_with_fresh_vars(YTerms, Context, ArgContext, Order,
+        ArgNum + 1, !.SeenXVars, XVars, Expansions, !SVarState, !SVarStore,
+        !VarSet, !ModuleInfo, !QualInfo, !Specs).
 
-:- pred do_insert_arg_unifications_with_contexts_loop(list(prog_var)::in,
+:- pred do_arg_unifications_with_contexts(list(prog_var)::in,
     list(prog_term)::in, assoc_list(int, arg_context)::in,
-    prog_context::in, list(hlds_goal)::in, list(hlds_goal)::out,
-    maybe(int)::in, num_added_goals::in, num_added_goals::out,
+    prog_context::in, goal_order::in, list(expansion)::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out, module_info::in, module_info::out,
     qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-do_insert_arg_unifications_with_contexts_loop(Vars, Terms, ArgContexts,
-        Context, !Goals, MaybeThreshold, !NumAdded, !SVarState, !SVarStore,
+do_arg_unifications_with_contexts(XVars, YTerms, ArgContexts,
+        Context, Order, Expansions, !SVarState, !SVarStore,
         !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
     (
-        Vars = [],
-        Terms = [],
+        XVars = [],
+        YTerms = [],
         ArgContexts = []
     ->
-        true
+        Expansions = []
     ;
-        Vars = [Var | VarsTail],
-        Terms = [Term | TermsTail],
-        ArgContexts = [ArgNumber - ArgContext | ArgContextsTail]
+        XVars = [HeadXVar | TailXVars],
+        YTerms = [HeadYTerm | TailYTerms],
+        ArgContexts = [HeadArgNumber - HeadArgContext | TailArgContexts]
     ->
-        do_arg_unification(Var, Term, Context, ArgContext, ArgNumber,
-            ArgUnifyConj, MaybeThreshold, !NumAdded, !SVarState, !SVarStore,
+        do_arg_unification(HeadXVar, HeadYTerm, Context, HeadArgContext, Order,
+            HeadArgNumber, HeadExpansion, !SVarState, !SVarStore,
             !VarSet, !ModuleInfo, !QualInfo, !Specs),
-        do_insert_arg_unifications_with_contexts_loop(VarsTail, TermsTail,
-            ArgContextsTail, Context, !Goals, MaybeThreshold, !NumAdded,
+        do_arg_unifications_with_contexts(TailXVars, TailYTerms,
+            TailArgContexts, Context, Order, TailExpansions,
             !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
-        !:Goals = ArgUnifyConj ++ !.Goals
+        Expansions = [HeadExpansion | TailExpansions]
     ;
         unexpected($module, $pred, "length mismatch")
     ).
 
-:- pred do_append_arg_unifications(list(prog_var)::in, list(prog_term)::in,
+:- pred do_arg_unification(prog_var::in, prog_term::in,
     prog_context::in, arg_context::in,
-    hlds_goal::in, hlds_goal::out, maybe(int)::in,
-    num_added_goals::in, num_added_goals::out,
+    goal_order::in, int::in, expansion::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out, module_info::in, module_info::out,
     qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-do_append_arg_unifications(HeadVars, Args, Context, ArgContext, !Goal,
-        MaybeThreshold, !NumAdded, !SVarState, !SVarStore, !VarSet,
-        !ModuleInfo, !QualInfo, !Specs) :-
+do_arg_unification(XVar, YTerm, Context, ArgContext, Order, ArgNum,
+        Expansion, !SVarState, !SVarStore,
+        !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
+    % It is the caller's job to make sure that if needed, then both
+    % XVar and the top level of YTerm have already been through
+    % state var mapping expansion.
     (
-        HeadVars = [],
-        expect(unify(Args, []), $module, $pred, "length mismatch 0")
+        YTerm = term.variable(YVar, _),
+        ( XVar = YVar ->
+            % Skip unifications of the form `XVar = XVar'.
+            GoalCord = cord.init
     ;
-        HeadVars = [HeadVar1 | HeadVarsAfter1],
-        !.Goal = hlds_goal(_, GoalInfo0),
-        goal_info_set_context(Context, GoalInfo0, GoalInfo),
-        svar_goal_to_conj_list(!.Goal, Goals0, !SVarStore),
-
-        (
-            Args = [],
-            unexpected($module, $pred, "length mismatch 0")
-        ;
-            Args = [Arg1 | ArgsAfter1],
-            do_arg_unification(HeadVar1, Arg1, Context, ArgContext,
-                1, ArgUnifyConj1, MaybeThreshold,
-                !NumAdded, !SVarState, !SVarStore,
-                !VarSet, !ModuleInfo, !QualInfo, !Specs),
-            Goals1 = Goals0 ++ ArgUnifyConj1,
-
-            (
-                HeadVarsAfter1 = [],
-                ArgsAfter1 = [],
-                conj_list_to_goal(Goals1, GoalInfo, !:Goal)
-            ;
-                HeadVarsAfter1 = [],
-                ArgsAfter1 = [_ | _],
-                unexpected($module, $pred, "length mismatch 1")
-            ;
-                HeadVarsAfter1 = [_ | _],
-                ArgsAfter1 = [],
-                unexpected($module, $pred, "length mismatch 1")
-            ;
-                HeadVarsAfter1 = [HeadVar2 | HeadVarsAfter2],
-                ArgsAfter1 = [Arg2 | ArgsAfter2],
-                do_arg_unification(HeadVar2, Arg2, Context, ArgContext,
-                    2, ArgUnifyConj2, MaybeThreshold,
-                    !NumAdded, !SVarState, !SVarStore,
-                    !VarSet, !ModuleInfo, !QualInfo, !Specs),
-                Goals2 = Goals1 ++ ArgUnifyConj2,
-
-                (
-                    HeadVarsAfter2 = [],
-                    ArgsAfter2 = [],
-                    conj_list_to_goal(Goals2, GoalInfo, !:Goal)
-                ;
-                    HeadVarsAfter2 = [],
-                    ArgsAfter2 = [_ | _],
-                    unexpected($module, $pred, "length mismatch 2")
-                ;
-                    HeadVarsAfter2 = [_ | _],
-                    ArgsAfter2 = [],
-                    unexpected($module, $pred, "length mismatch 2")
-                ;
-                    HeadVarsAfter2 = [HeadVar3 | HeadVarsAfter3],
-                    ArgsAfter2 = [Arg3 | ArgsAfter3],
-                    do_arg_unification(HeadVar3, Arg3, Context, ArgContext,
-                        3, ArgUnifyConj3, MaybeThreshold,
-                        !NumAdded, !SVarState, !SVarStore,
-                        !VarSet, !ModuleInfo, !QualInfo, !Specs),
-                    Goals3 = Goals2 ++ ArgUnifyConj3,
-
-                    do_append_arg_unifications_loop(HeadVarsAfter3, ArgsAfter3,
-                        Context, ArgContext, 4, Goals3, Goals,
-                        MaybeThreshold, !NumAdded, !SVarState, !SVarStore,
-                        !VarSet, !ModuleInfo, !QualInfo, !Specs),
-                    conj_list_to_goal(Goals, GoalInfo, !:Goal)
-                )
-            )
-        )
-    ).
-
-:- pred do_append_arg_unifications_loop(list(prog_var)::in,
-    list(prog_term)::in, prog_context::in, arg_context::in, int::in,
-    list(hlds_goal)::in, list(hlds_goal)::out,
-    maybe(int)::in, num_added_goals::in, num_added_goals::out,
-    svar_state::in, svar_state::out, svar_store::in, svar_store::out,
-    prog_varset::in, prog_varset::out, module_info::in, module_info::out,
-    qual_info::in, qual_info::out,
-    list(error_spec)::in, list(error_spec)::out) is det.
-
-do_append_arg_unifications_loop([], [_ | _], _, _, _, _, _, _, !NumAdded,
-        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
-    unexpected($module, $pred, "length mismatch").
-do_append_arg_unifications_loop([_ | _], [], _, _, _, _, _, _, !NumAdded,
-        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
-    unexpected($module, $pred, "length mismatch").
-do_append_arg_unifications_loop([], [], _, _, _, !GoalList, _, !NumAdded,
-        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs).
-do_append_arg_unifications_loop([HeadVar | HeadVars], [Arg | Args],
-        Context, ArgContext, ArgNum, !GoalList, MaybeThreshold, !NumAdded,
-        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
-    do_arg_unification(HeadVar, Arg, Context, ArgContext, ArgNum, ArgUnifyConj,
-        MaybeThreshold, !NumAdded, !SVarState, !SVarStore, !VarSet,
-        !ModuleInfo, !QualInfo, !Specs),
-    !:GoalList = !.GoalList ++ ArgUnifyConj,
-    do_append_arg_unifications_loop(HeadVars, Args, Context, ArgContext,
-        ArgNum + 1, !GoalList, MaybeThreshold, !NumAdded,
-        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs).
-
-:- pred do_arg_unification(prog_var::in, prog_term::in,
-    prog_context::in, arg_context::in, int::in, list(hlds_goal)::out,
-    maybe(int)::in, num_added_goals::in, num_added_goals::out,
-    svar_state::in, svar_state::out, svar_store::in, svar_store::out,
-    prog_varset::in, prog_varset::out, module_info::in, module_info::out,
-    qual_info::in, qual_info::out,
-    list(error_spec)::in, list(error_spec)::out) is det.
-
-do_arg_unification(Var, Arg, Context, ArgContext, ArgNum, ArgUnifyConj,
-        MaybeThreshold, !NumAdded, !SVarState, !SVarStore, !VarSet,
-        !ModuleInfo, !QualInfo, !Specs) :-
-    % It is the caller's job to make sure that if needed, then both
-    % Var and Arg have already been through state var mapping expansion.
-    ( Arg = term.variable(Var, _) ->
-        % Skip unifications of the form `X = X'.
-        ArgUnifyConj = []
+            arg_context_to_unify_context(ArgContext, ArgNum,
+                MainContext, SubContext),
+            make_atomic_unification(XVar, rhs_var(YVar), Context,
+                MainContext, SubContext, purity_pure, Goal, !QualInfo),
+            GoalCord = cord.singleton(Goal)
+        ),
+        Expansion = expansion(not_fgti, GoalCord)
     ;
+        YTerm = term.functor(YFunctor, YArgTerms, YFunctorContext),
         arg_context_to_unify_context(ArgContext, ArgNum,
             MainContext, SubContext),
-        do_unravel_unification(term.variable(Var, Context), Arg, Context,
-            MainContext, SubContext, purity_pure, Goal,
-            MaybeThreshold, !NumAdded, !SVarState, !SVarStore, !VarSet,
-            !ModuleInfo, !QualInfo, !Specs),
-        goal_to_conj_list(Goal, ArgUnifyConj)
+        unravel_var_functor_unification(XVar, YFunctor, YArgTerms,
+            YFunctorContext, Context, MainContext, SubContext, purity_pure,
+            Order, Expansion, !SVarState, !SVarStore, !VarSet,
+            !ModuleInfo, !QualInfo, !Specs)
     ).
 
 %-----------------------------------------------------------------------------%
 
-:- pred do_unravel_unification(prog_term::in, prog_term::in, prog_context::in,
-    unify_main_context::in, unify_sub_contexts::in, purity::in,
-    hlds_goal::out, maybe(int)::in, num_added_goals::in, num_added_goals::out,
+:- pred do_unravel_unification(prog_term::in, prog_term::in,
+    prog_context::in, unify_main_context::in, unify_sub_contexts::in,
+    purity::in, goal_order::in, expansion::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out, module_info::in, module_info::out,
     qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-do_unravel_unification(LHS0, RHS0, Context, MainContext, SubContext, Purity,
-        Goal, MaybeThreshold, !NumAdded, !SVarState, !SVarStore, !VarSet,
+do_unravel_unification(LHS0, RHS0, Context, MainContext, SubContext,
+        Purity, Order, Expansion, !SVarState, !SVarStore, !VarSet,
         !ModuleInfo, !QualInfo, !Specs) :-
     substitute_state_var_mapping(LHS0, LHS, !VarSet, !SVarState, !Specs),
     substitute_state_var_mapping(RHS0, RHS, !VarSet, !SVarState, !Specs),
-    classify_unravel_unification(LHS, RHS, Context, MainContext, SubContext,
-        Purity, Goal0, UnifyNumAdded, !SVarState, !SVarStore, !VarSet,
-        !ModuleInfo, !QualInfo, !Specs),
-    !:NumAdded = !.NumAdded + UnifyNumAdded,
-    (
-        MaybeThreshold = yes(Threshold),
-        UnifyNumAdded > Threshold,
-        LHS = term.variable(LHSVar, _),
-        term_is_ground(RHS)
-    ->
-        Goal0 = hlds_goal(GoalExpr0, GoalInfo0),
-        Kind = from_ground_term_initial,
-        goal_info_set_nonlocals(set_of_var.make_singleton(LHSVar),
-            GoalInfo0, GoalInfo),
-        ( GoalExpr0 = conj(plain_conj, Conjuncts0) ->
-            mark_nonlocals_in_ground_term_construct(Conjuncts0, Conjuncts),
-            SubGoalExpr = conj(plain_conj, Conjuncts),
-            SubGoal = hlds_goal(SubGoalExpr, GoalInfo),
-            GoalExpr = scope(from_ground_term(LHSVar, Kind), SubGoal),
-            Goal = hlds_goal(GoalExpr, GoalInfo)
-        ;
-            % This can happen if we unravel a large ground term that happens
-            % to be a lambda expression; the conjunction will then be *inside*
-            % the rhs_lambda_goal.
-            Goal = Goal0
-        )
-    ;
-        Goal = Goal0
-    ).
+    classify_unravel_unification(LHS, RHS,
+        Context, MainContext, SubContext, Purity, Order, Expansion,
+        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs).
 
-:- pred mark_nonlocals_in_ground_term_construct(
-    list(hlds_goal)::in, list(hlds_goal)::out) is det.
+:- pred do_unravel_var_unification(prog_var::in, prog_term::in,
+    prog_context::in, unify_main_context::in, unify_sub_contexts::in,
+    purity::in, goal_order::in, expansion::out,
+    svar_state::in, svar_state::out, svar_store::in, svar_store::out,
+    prog_varset::in, prog_varset::out, module_info::in, module_info::out,
+    qual_info::in, qual_info::out,
+    list(error_spec)::in, list(error_spec)::out) is det.
 
-mark_nonlocals_in_ground_term_construct([], []).
-mark_nonlocals_in_ground_term_construct([Goal0 | Goals0], [Goal | Goals]) :-
-    Goal0 = hlds_goal(GoalExpr, GoalInfo0),
-    (
-        GoalExpr = unify(LHSVar, RHS, _, _, _),
-        RHS = rhs_functor(_, _, RHSVars)
-    ->
-        set_of_var.list_to_set([LHSVar | RHSVars], NonLocals),
-        goal_info_set_nonlocals(NonLocals, GoalInfo0, GoalInfo),
-        Goal = hlds_goal(GoalExpr, GoalInfo)
-    ;
-        unexpected($module, $pred, "wrong shape goal")
-    ),
-    mark_nonlocals_in_ground_term_construct(Goals0, Goals).
+do_unravel_var_unification(LHSVar, RHS0, Context, MainContext, SubContext,
+        Purity, Order, Expansion, !SVarState, !SVarStore, !VarSet,
+        !ModuleInfo, !QualInfo, !Specs) :-
+    substitute_state_var_mapping(RHS0, RHS, !VarSet, !SVarState, !Specs),
+    classify_unravel_var_unification(LHSVar, RHS,
+        Context, MainContext, SubContext, Purity, Order, Expansion,
+        !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs).
 
 :- pred classify_unravel_unification(prog_term::in, prog_term::in,
     prog_context::in, unify_main_context::in, unify_sub_contexts::in,
-    purity::in, hlds_goal::out, num_added_goals::out,
+    purity::in, goal_order::in, expansion::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out, module_info::in, module_info::out,
     qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-classify_unravel_unification(TermX, TermY, Context, MainContext, SubContext,
-        Purity, Goal, NumAdded, !SVarState, !SVarStore, !VarSet,
+classify_unravel_unification(XTerm, YTerm, Context, MainContext, SubContext,
+        Purity, Order, Expansion, !SVarState, !SVarStore, !VarSet,
         !ModuleInfo, !QualInfo, !Specs) :-
     (
         % `X = Y' needs no unravelling.
-        TermX = term.variable(X, _),
-        TermY = term.variable(Y, _),
-        make_atomic_unification(X, rhs_var(Y), Context, MainContext,
+        XTerm = term.variable(XVar, _),
+        YTerm = term.variable(YVar, _),
+        make_atomic_unification(XVar, rhs_var(YVar), Context, MainContext,
             SubContext, Purity, Goal, !QualInfo),
-        NumAdded = 0
+        Expansion = expansion(not_fgti, cord.singleton(Goal))
+    ;
+        XTerm = term.variable(XVar, _),
+        YTerm = term.functor(YFunctor, YArgTerms, YFunctorContext),
+        unravel_var_functor_unification(XVar, YFunctor, YArgTerms,
+            YFunctorContext, Context, MainContext, SubContext,
+            Purity, Order, Expansion, !SVarState, !SVarStore,
+            !VarSet, !ModuleInfo, !QualInfo, !Specs)
     ;
-        TermX = term.variable(X, _),
-        TermY = term.functor(F, Args, FunctorContext),
-        unravel_var_functor_unification(X, F, Args, FunctorContext,
-            Context, MainContext, SubContext, Purity, Goal, NumAdded,
-            !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs)
-    ;
-        TermX = term.functor(F, Args, FunctorContext),
-        TermY = term.variable(Y, _),
-        unravel_var_functor_unification(Y, F, Args, FunctorContext,
-            Context, MainContext, SubContext, Purity, Goal, NumAdded,
-            !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs)
+        XTerm = term.functor(XFunctor, XArgTerms, XFunctorContext),
+        YTerm = term.variable(YVar, _),
+        unravel_var_functor_unification(YVar, XFunctor, XArgTerms,
+            XFunctorContext, Context, MainContext, SubContext,
+            Purity, Order, Expansion, !SVarState, !SVarStore,
+            !VarSet, !ModuleInfo, !QualInfo, !Specs)
     ;
         % If we find a unification of the form `f1(...) = f2(...)',
         % then we replace it with `Tmp = f1(...), Tmp = f2(...)',
         % and then process it according to the rules above.
         % Note that we can't simplify it yet, e.g. by pairwise unifying
-        % the args of TermX and TermY, because we might simplify away
+        % the args of XTerm and YTerm, because we might simplify away
         % type errors.
-        TermX = term.functor(_, _, _),
-        TermY = term.functor(_, _, _),
+        XTerm = term.functor(XFunctor, XArgTerms, XFunctorContext),
+        YTerm = term.functor(YFunctor, YArgTerms, YFunctorContext),
         varset.new_var(TmpVar, !VarSet),
-        NumAdded0 = 0,
-        do_unravel_unification(term.variable(TmpVar, Context), TermX,
-            Context, MainContext, SubContext, Purity, GoalX, no,
-            NumAdded0, NumAdded1,
+        unravel_var_functor_unification(TmpVar, XFunctor, XArgTerms,
+            XFunctorContext, Context, MainContext, SubContext,
+            Purity, Order, ExpansionX,
             !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
-        do_unravel_unification(term.variable(TmpVar, Context), TermY,
-            Context, MainContext, SubContext, Purity, GoalY, no,
-            NumAdded1, NumAdded,
+        unravel_var_functor_unification(TmpVar, YFunctor, YArgTerms,
+            YFunctorContext, Context, MainContext, SubContext,
+            Purity, Order, ExpansionY,
             !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
-        svar_goal_to_conj_list(GoalX, ConjListX, !SVarStore),
-        svar_goal_to_conj_list(GoalY, ConjListY, !SVarStore),
-        ConjList = ConjListX ++ ConjListY,
-        goal_info_init(GoalInfo),
-        conj_list_to_goal(ConjList, GoalInfo, Goal)
+        goal_info_init(Context, GoalInfo),
+        expansion_to_goal_cord_wrap_if_fgti(GoalInfo, ExpansionX,
+            MaybeWrappedGoalCordX),
+        expansion_to_goal_cord_wrap_if_fgti(GoalInfo, ExpansionY,
+            MaybeWrappedGoalCordY),
+        GoalCord = MaybeWrappedGoalCordX ++ MaybeWrappedGoalCordY,
+        Expansion = expansion(not_fgti, GoalCord)
+    ).
+
+:- pred classify_unravel_var_unification(prog_var::in, prog_term::in,
+    prog_context::in, unify_main_context::in, unify_sub_contexts::in,
+    purity::in, goal_order::in, expansion::out,
+    svar_state::in, svar_state::out, svar_store::in, svar_store::out,
+    prog_varset::in, prog_varset::out, module_info::in, module_info::out,
+    qual_info::in, qual_info::out,
+    list(error_spec)::in, list(error_spec)::out) is det.
+
+classify_unravel_var_unification(XVar, YTerm, Context, MainContext, SubContext,
+        Purity, Order, Expansion, !SVarState, !SVarStore, !VarSet,
+        !ModuleInfo, !QualInfo, !Specs) :-
+    (
+        % `X = Y' needs no unravelling.
+        YTerm = term.variable(YVar, _),
+        make_atomic_unification(XVar, rhs_var(YVar), Context, MainContext,
+            SubContext, Purity, Goal, !QualInfo),
+        Expansion = expansion(not_fgti, cord.singleton(Goal))
+    ;
+        YTerm = term.functor(YFunctor, YArgTerms, YFunctorContext),
+        unravel_var_functor_unification(XVar, YFunctor, YArgTerms,
+            YFunctorContext, Context, MainContext, SubContext,
+            Purity, Order, Expansion, !SVarState, !SVarStore,
+            !VarSet, !ModuleInfo, !QualInfo, !Specs)
     ).
 
     % Given an unification of the form
@@ -631,28 +588,28 @@
 :- pred unravel_var_functor_unification(prog_var::in, term.const::in,
     list(prog_term)::in, term.context::in,
     prog_context::in, unify_main_context::in, unify_sub_contexts::in,
-    purity::in, hlds_goal::out, num_added_goals::out,
+    purity::in, goal_order::in, expansion::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out, module_info::in, module_info::out,
     qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-unravel_var_functor_unification(X, F, Args0, FunctorContext,
-        Context, MainContext, SubContext, Purity, Goal, NumAdded,
+unravel_var_functor_unification(XVar, YFunctor, YArgTerms0, YFunctorContext,
+        Context, MainContext, SubContext, Purity, Order, Expansion,
         !SVarState, !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
-    substitute_state_var_mappings(Args0, Args, !VarSet, !SVarState, !Specs),
+    substitute_state_var_mappings(YArgTerms0, YArgTerms, !VarSet,
+        !SVarState, !Specs),
     (
-        F = term.atom(Atom),
-        maybe_unravel_special_var_functor_unification(X, Atom, Args,
-            FunctorContext, Context, MainContext, SubContext, Purity,
-            GoalPrime, NumAddedPrime, !SVarState, !SVarStore, !VarSet,
+        YFunctor = term.atom(YAtom),
+        maybe_unravel_special_var_functor_unification(XVar, YAtom, YArgTerms,
+            YFunctorContext, Context, MainContext, SubContext, Purity,
+            Order, ExpansionPrime, !SVarState, !SVarStore, !VarSet,
             !ModuleInfo, !QualInfo, !Specs)
     ->
-        Goal = GoalPrime,
-        NumAdded = NumAddedPrime
+        Expansion = ExpansionPrime
     ;
         % Handle higher-order pred and func expressions.
-        RHS = term.functor(F, Args, FunctorContext),
+        RHS = term.functor(YFunctor, YArgTerms, YFunctorContext),
         parse_rule_term(Context, RHS, HeadTerm0, GoalTerm1),
         term.coerce(HeadTerm0, HeadTerm1),
         parse_purity_annotation(HeadTerm1, LambdaPurity, HeadTerm),
@@ -680,16 +637,16 @@
         parse_goal(GoalTerm, ContextPieces, MaybeParsedGoal, !VarSet),
         (
             MaybeParsedGoal = ok1(ParsedGoal),
-            build_lambda_expression(X, Purity, LambdaPurity, Groundness,
+            build_lambda_expression(XVar, Purity, LambdaPurity, Groundness,
                 PredOrFunc, EvalMethod, Vars1, Modes, Det, ParsedGoal,
-                Context, MainContext, SubContext, Goal, 0, NumAdded,
+                Context, MainContext, SubContext, Goal,
                 !.SVarState, !SVarStore, !VarSet,
-                !ModuleInfo, !QualInfo, !Specs)
+                !ModuleInfo, !QualInfo, !Specs),
+            Expansion = expansion(not_fgti, cord.singleton(Goal))
         ;
             MaybeParsedGoal = error1(ParsedGoalSpecs),
             !:Specs = ParsedGoalSpecs ++ !.Specs,
-            NumAdded = 0,
-            Goal = true_goal
+            Expansion = expansion(not_fgti, cord.singleton(true_goal))
         )
     ;
         % Handle the usual case.
@@ -697,75 +654,81 @@
             % The condition of this if-then-else is based on the logic of
             % try_parse_sym_name_and_args, but specialized to this location,
             % so that we can do state var expansion only if we need to.
-            F = term.atom(FName),
+            YFunctor = term.atom(FName),
             (
                 FName = ".",
-                Args = [ModuleTerm, NameArgsTerm]
+                YArgTerms = [ModuleTerm, NameArgsTerm]
             ->
-                NameArgsTerm = term.functor(term.atom(Name), NArgs, _),
+                NameArgsTerm = term.functor(term.atom(Name), NameArgTerms, _),
                 try_parse_symbol_name(ModuleTerm, Module),
                 FunctorName = qualified(Module, Name),
                 % We have done state variable name expansion at the top
-                % level of Args, but not at the level of NArgs.
-                substitute_state_var_mappings(NArgs, FunctorArgsPrime,
-                    !VarSet, !SVarState, !Specs)
+                % level of Args, but not at the level of NameArgTerms.
+                substitute_state_var_mappings(NameArgTerms,
+                    MaybeQualifiedYArgTermsPrime, !VarSet, !SVarState, !Specs)
             ;
                 FunctorName = string_to_sym_name_sep(FName, "__"),
-                FunctorArgsPrime = Args
+                MaybeQualifiedYArgTermsPrime = YArgTerms
             )
         ->
-            FunctorArgs = FunctorArgsPrime,
-            list.length(FunctorArgs, Arity),
+            MaybeQualifiedYArgTerms = MaybeQualifiedYArgTermsPrime,
+            list.length(MaybeQualifiedYArgTerms, Arity),
             ConsId = cons(FunctorName, Arity, cons_id_dummy_type_ctor)
         ;
             % float, int or string constant
             %   - any errors will be caught by typechecking
-            list.length(Args, Arity),
-            ConsId = make_functor_cons_id(F, Arity),
-            FunctorArgs = Args
+            list.length(YArgTerms, Arity),
+            ConsId = make_functor_cons_id(YFunctor, Arity),
+            MaybeQualifiedYArgTerms = YArgTerms
         ),
         % At this point, we have done state variable name expansion
-        % at the top level of FunctorArgs.
+        % at the top level of MaybeQualifiedYArgTerms.
         (
-            FunctorArgs = [],
-            make_atomic_unification(X, rhs_functor(ConsId, no, []),
-                Context, MainContext, SubContext, Purity, Goal0, !QualInfo),
-            NumAdded = 1,
-            Goal0 = hlds_goal(GoalExpr, GoalInfo0),
-            goal_info_set_purity(Purity, GoalInfo0, GoalInfo),
-            % We could wrap a from_ground_term(X) scope around Goal,
-            % but there would be no gain from doing so, whereas the
-            % increase would lead to a slight increase in memory and time
-            % requirements.
-            Goal = hlds_goal(GoalExpr, GoalInfo)
+            MaybeQualifiedYArgTerms = [],
+            make_atomic_unification(XVar, rhs_functor(ConsId, no, []),
+                Context, MainContext, SubContext, Purity, FunctorGoal,
+                !QualInfo),
+            goal_set_purity(Purity, FunctorGoal, Goal),
+            Expansion = expansion(fgti_var_size(XVar, 1), cord.singleton(Goal))
         ;
-            FunctorArgs = [_ | _],
-            make_fresh_arg_vars_no_svar(FunctorArgs, HeadVars, !VarSet),
-            make_atomic_unification(X, rhs_functor(ConsId, no, HeadVars),
-                Context, MainContext, SubContext, Purity, Goal0, !QualInfo),
-            MainFunctorAdded = 1,
+            MaybeQualifiedYArgTerms = [_ | _],
             ArgContext = ac_functor(ConsId, MainContext, SubContext),
-            % Should this be insert_... rather than append_...?
-            % No, because that causes efficiency problems for type-checking :-(
-            % But for impure unifications, we need to do this, because
-            % mode reordering can't reorder around the functor unification.
             (
                 Purity = purity_pure,
-                do_append_arg_unifications(HeadVars, FunctorArgs,
-                    FunctorContext, ArgContext, Goal0, Goal, no,
-                    MainFunctorAdded, NumAdded, !SVarState, !SVarStore,
-                    !VarSet, !ModuleInfo, !QualInfo, !Specs)
+                % If we can, we want to add the unifications for the arguments
+                % AFTER the unification of the top level function symbol,
+                % because otherwise we get efficiency problems during
+                % type-checking :-(
+                do_arg_unifications_with_fresh_vars(MaybeQualifiedYArgTerms,
+                    YFunctorContext, ArgContext, deconstruct_top_down, 1,
+                    [], YVars, ArgExpansions, !SVarState, !SVarStore, !VarSet,
+                    !ModuleInfo, !QualInfo, !Specs),
+                make_atomic_unification(XVar, rhs_functor(ConsId, no, YVars),
+                    Context, MainContext, SubContext, Purity, FunctorGoal,
+                    !QualInfo),
+                goal_info_init(Context, GoalInfo),
+                append_expansions_after_goal_top_ftgi(GoalInfo, XVar,
+                    FunctorGoal, 1, ArgExpansions, Expansion)
             ;
                 ( Purity = purity_semipure
                 ; Purity = purity_impure
                 ),
-                Goal0 = hlds_goal(GoalExpr0, GoalInfo0),
-                goal_info_set_purity(Purity, GoalInfo0, GoalInfo1),
-                Goal1 = hlds_goal(GoalExpr0, GoalInfo1),
-                do_insert_arg_unifications(HeadVars, FunctorArgs,
-                    FunctorContext, ArgContext, Goal1, Goal, no,
-                    MainFunctorAdded, NumAdded, !SVarState, !SVarStore,
-                    !VarSet, !ModuleInfo, !QualInfo, !Specs)
+                % For impure unifications, we need to put the unifications
+                % for the arguments BEFORE the unification of the top level
+                % function symbol, because mode reordering can't reorder
+                % code around that unification.
+                do_arg_unifications_with_fresh_vars(MaybeQualifiedYArgTerms,
+                    YFunctorContext, ArgContext, construct_bottom_up, 1,
+                    [], YVars, ArgExpansions, !SVarState, !SVarStore, !VarSet,
+                    !ModuleInfo, !QualInfo, !Specs),
+                make_atomic_unification(XVar, rhs_functor(ConsId, no, YVars),
+                    Context, MainContext, SubContext, Purity, FunctorGoal,
+                    !QualInfo),
+                goal_info_init(Context, GoalInfo),
+                insert_expansions_before_goal_top_not_fgti(GoalInfo,
+                    ArgExpansions, FunctorGoal, Goal0),
+                goal_set_purity(Purity, Goal0, Goal),
+                Expansion = expansion(not_fgti, cord.singleton(Goal))
             )
         )
     ).
@@ -775,26 +738,26 @@
 :- pred maybe_unravel_special_var_functor_unification(prog_var::in,
     string::in, list(prog_term)::in, term.context::in,
     prog_context::in, unify_main_context::in, unify_sub_contexts::in,
-    purity::in, hlds_goal::out, num_added_goals::out,
+    purity::in, goal_order::in, expansion::out,
     svar_state::in, svar_state::out, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out, module_info::in, module_info::out,
     qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is semidet.
 
-maybe_unravel_special_var_functor_unification(X, Atom, Args,
-        FunctorContext, Context, MainContext, SubContext, Purity, Goal,
-        NumAdded, !SVarState, !SVarStore, !VarSet,
+maybe_unravel_special_var_functor_unification(XVar, YAtom, YArgs,
+        YFunctorContext, Context, MainContext, SubContext, Purity, Order,
+        Expansion, !SVarState, !SVarStore, !VarSet,
         !ModuleInfo, !QualInfo, !Specs)  :-
-    % Switch on Atom.
-    % XXX instead of failing if Atom has the wrong number of arguments or
+    % Switch on YAtom.
+    % XXX instead of failing if YAtom has the wrong number of arguments or
     % if the arguments have the wrong shape, we should generate an error
     % message.
     (
         % Handle explicit type qualification.
-        ( Atom = "with_type"
-        ; Atom = ":"
+        ( YAtom = "with_type"
+        ; YAtom = ":"
         ),
-        Args = [RVal0, DeclType0],
+        YArgs = [RVal, DeclType0],
 
         require_det (
             % DeclType0 is a prog_term, but it is really a type,
@@ -807,7 +770,7 @@
             (
                 DeclTypeResult = ok1(DeclType),
                 varset.coerce(!.VarSet, DeclVarSet),
-                process_type_qualification(X, DeclType, DeclVarSet,
+                process_type_qualification(XVar, DeclType, DeclVarSet,
                     Context, !ModuleInfo, !QualInfo, !Specs)
             ;
                 DeclTypeResult = error1(DeclTypeSpecs),
@@ -816,49 +779,41 @@
                 % a generic term.
                 !:Specs = DeclTypeSpecs ++ !.Specs
             ),
-            substitute_state_var_mapping(RVal0, RVal, !VarSet,
-                !SVarState, !Specs),
-            do_unravel_unification(term.variable(X, Context), RVal,
-                Context, MainContext, SubContext, Purity, Goal, no,
-                0, NumAdded, !SVarState, !SVarStore, !VarSet,
+            do_unravel_var_unification(XVar, RVal,
+                Context, MainContext, SubContext, Purity, Order, Expansion,
+                !SVarState, !SVarStore, !VarSet,
                 !ModuleInfo, !QualInfo, !Specs)
         )
     ;
         % Handle unification expressions.
-        Atom = "@",
-        Args = [LVal0, RVal0],
+        YAtom = "@",
+        YArgs = [LVal, RVal],
 
         require_det (
-            substitute_state_var_mapping(LVal0, LVal, !VarSet,
-                !SVarState, !Specs),
-            substitute_state_var_mapping(RVal0, RVal, !VarSet,
-                !SVarState, !Specs),
-            do_unravel_unification(term.variable(X, Context), LVal, Context,
-                MainContext, SubContext, Purity, GoalL, no,
-                0, NumAdded1, !SVarState, !SVarStore, !VarSet,
+            do_unravel_var_unification(XVar, LVal, Context,
+                MainContext, SubContext, Purity, Order, ExpansionL,
+                !SVarState, !SVarStore, !VarSet,
                 !ModuleInfo, !QualInfo, !Specs),
-            do_unravel_unification(term.variable(X, Context), RVal, Context,
-                MainContext, SubContext, Purity, GoalR, no,
-                NumAdded1, NumAdded, !SVarState, !SVarStore, !VarSet,
+            do_unravel_var_unification(XVar, RVal, Context,
+                MainContext, SubContext, Purity, Order, ExpansionR,
+                !SVarState, !SVarStore, !VarSet,
                 !ModuleInfo, !QualInfo, !Specs),
-            goal_info_init(GoalInfo),
-            svar_goal_to_conj_list(GoalL, ConjListL, !SVarStore),
-            svar_goal_to_conj_list(GoalR, ConjListR, !SVarStore),
-            ConjList = ConjListL ++ ConjListR,
-            conj_list_to_goal(ConjList, GoalInfo, Goal)
+            ExpansionL = expansion(_, GoalCordL),
+            ExpansionR = expansion(_, GoalCordR),
+            Expansion = expansion(not_fgti, GoalCordL ++ GoalCordR)
         )
     ;
         % Handle if-then-else expressions.
         (
-            Atom = "else",
-            Args = [CondThenTerm, ElseTerm0],
-            CondThenTerm = term.functor(term.atom("if"),
+            YAtom = "else",
+            YArgs = [CondThenTerm0, ElseTerm0],
+            CondThenTerm0 = term.functor(term.atom("if"),
                 [term.functor(term.atom("then"), [CondTerm0, ThenTerm0], _)],
                     _)
         ;
-            Atom = ";",
-            Args = [CondThenTerm, ElseTerm0],
-            CondThenTerm = term.functor(term.atom("->"),
+            YAtom = ";",
+            YArgs = [CondThenTerm0, ElseTerm0],
+            CondThenTerm0 = term.functor(term.atom("->"),
                 [CondTerm0, ThenTerm0], _)
         ),
 
@@ -873,30 +828,37 @@
                 svar_prepare_for_local_state_vars(Context, !.VarSet, StateVars,
                     BeforeSVarState, BeforeInsideSVarState, !Specs),
                 map.init(EmptySubst),
-                some [!NumAdded] (
+
                     transform_goal_expr_context_to_goal(loc_inside_atomic_goal,
-                        CondParseTree, EmptySubst, CondGoal, !:NumAdded,
+                    CondParseTree, EmptySubst, CondGoal,
                         BeforeInsideSVarState, AfterCondInsideSVarState,
                         !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
 
                     substitute_state_var_mapping(ThenTerm0, ThenTerm, !VarSet,
                         AfterCondInsideSVarState, AfterThenInsideSVarState0,
                         !Specs),
-                    do_unravel_unification(term.variable(X, Context), ThenTerm,
-                        Context, MainContext, SubContext, Purity, ThenGoal0,
-                        no, !NumAdded,
+                classify_unravel_var_unification(XVar, ThenTerm,
+                    Context, MainContext, SubContext,
+                    Purity, Order, ThenExpansion,
                         AfterThenInsideSVarState0, AfterThenInsideSVarState,
                         !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
+                goal_info_init(get_term_context(ThenTerm), ThenGoalInfo),
+                expansion_to_goal_wrap_if_fgti(ThenGoalInfo,
+                    ThenExpansion, ThenGoal0),
 
                     svar_finish_local_state_vars(StateVars, BeforeSVarState,
                         AfterThenInsideSVarState, AfterThenSVarState),
 
                     substitute_state_var_mapping(ElseTerm0, ElseTerm, !VarSet,
                         BeforeSVarState, AfterElseSVarState0, !Specs),
-                    do_unravel_unification(term.variable(X, Context), ElseTerm,
-                        Context, MainContext, SubContext, Purity, ElseGoal0,
-                        no, !NumAdded, AfterElseSVarState0, AfterElseSVarState,
+                classify_unravel_var_unification(XVar, ElseTerm,
+                    Context, MainContext, SubContext,
+                    Purity, Order, ElseExpansion,
+                    AfterElseSVarState0, AfterElseSVarState,
                         !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs),
+                goal_info_init(get_term_context(ElseTerm), ElseGoalInfo),
+                expansion_to_goal_wrap_if_fgti(ElseGoalInfo,
+                    ElseExpansion, ElseGoal0),
 
                     svar_finish_if_then_else(loc_inside_atomic_goal, Context,
                         StateVars, ThenGoal0, ThenGoal, ElseGoal0, ElseGoal,
@@ -909,19 +871,17 @@
                         CondGoal, ThenGoal, ElseGoal),
                     goal_info_init(Context, GoalInfo),
                     Goal = hlds_goal(GoalExpr, GoalInfo),
-                    NumAdded = !.NumAdded
-                )
+                Expansion = expansion(not_fgti, cord.singleton(Goal))
             ;
                 MaybeVarsCond = error3(VarsCondSpecs),
                 !:Specs = VarsCondSpecs ++ !.Specs,
-                Goal = true_goal,
-                NumAdded = 0
+                Expansion = expansion(not_fgti, cord.singleton(true_goal))
             )
         )
     ;
         % Handle field extraction expressions.
-        Atom = "^",
-        Args = [InputTerm0, FieldNameTerm],
+        YAtom = "^",
+        YArgs = [InputTerm0, FieldNameTerm],
         maybe_parse_field_list(FieldNameTerm, !.VarSet, FieldNames),
 
         require_det (
@@ -929,20 +889,24 @@
                 !SVarState, !Specs),
             make_fresh_arg_var_no_svar(InputTerm, InputTermVar, [], !VarSet),
             expand_get_field_function_call(Context, MainContext, SubContext,
-                FieldNames, X, InputTermVar, Purity, Functor, _, Goal0,
-                0, NumAdded1, !SVarState, !SVarStore, !VarSet,
+                FieldNames, XVar, InputTermVar, Purity, Functor, _, GetGoal,
+                !SVarState, !SVarStore, !VarSet,
                 !ModuleInfo, !QualInfo, !Specs),
 
             ArgContext = ac_functor(Functor, MainContext, SubContext),
-            do_insert_arg_unifications([InputTermVar], [InputTerm],
-                FunctorContext, ArgContext, Goal0, Goal, no,
-                NumAdded1, NumAdded, !SVarState, !SVarStore, !VarSet,
-                !ModuleInfo, !QualInfo, !Specs)
+            do_arg_unification(InputTermVar, InputTerm,
+                YFunctorContext, ArgContext, Order, 1, InputArgExpansion,
+                !SVarState, !SVarStore, !VarSet,
+                !ModuleInfo, !QualInfo, !Specs),
+            goal_info_init(Context, GoalInfo),
+            insert_expansion_before_goal_top_not_fgti(GoalInfo,
+                InputArgExpansion, GetGoal, Goal),
+            Expansion = expansion(not_fgti, cord.singleton(Goal))
         )
     ;
         % Handle field update expressions.
-        Atom = ":=",
-        Args = [FieldDescrTerm, FieldValueTerm0],
+        YAtom = ":=",
+        YArgs = [FieldDescrTerm, FieldValueTerm0],
         FieldDescrTerm = term.functor(term.atom("^"),
             [InputTerm0, FieldNameTerm], _),
         maybe_parse_field_list(FieldNameTerm, !.VarSet, FieldNames),
@@ -957,9 +921,9 @@
                 [InputTermVar], !VarSet),
 
             expand_set_field_function_call(Context, MainContext, SubContext,
-                FieldNames, FieldValueVar, InputTermVar, X,
-                Functor, InnerFunctor - FieldSubContext, Goal0,
-                0, NumAdded1, !SVarState, !SVarStore, !VarSet,
+                FieldNames, FieldValueVar, InputTermVar, XVar,
+                Functor, InnerFunctor - FieldSubContext, SetGoal,
+                !SVarState, !SVarStore, !VarSet,
                 !ModuleInfo, !QualInfo, !Specs),
 
             TermArgContext = ac_functor(Functor, MainContext, SubContext),
@@ -969,18 +933,22 @@
             FieldArgNumber = 2,
             ArgContexts = [TermArgNumber - TermArgContext,
                 FieldArgNumber - FieldArgContext],
-            do_insert_arg_unifications_with_contexts(
-                [InputTermVar, FieldValueVar], [InputTerm, FieldValueTerm],
-                ArgContexts, Context, Goal0, Goal, no,
-                NumAdded1, NumAdded, !SVarState, !SVarStore, !VarSet,
-                !ModuleInfo, !QualInfo, !Specs)
+            do_arg_unifications_with_contexts([InputTermVar, FieldValueVar],
+                [InputTerm, FieldValueTerm], ArgContexts, Context, Order,
+                InputFieldArgExpansions, !SVarState, !SVarStore, !VarSet,
+                !ModuleInfo, !QualInfo, !Specs),
+
+            goal_info_init(Context, GoalInfo),
+            insert_expansions_before_goal_top_not_fgti(GoalInfo,
+                InputFieldArgExpansions, SetGoal, Goal),
+            Expansion = expansion(not_fgti, cord.singleton(Goal))
         )
     ;
         % Handle higher-order dcg pred expressions. They have the same
         % semantics as higher-order pred expressions, but have two extra
         % arguments, and the goal is expanded as a DCG goal.
-        Atom = "-->",
-        Args = [PredTerm0, GoalTerm0],
+        YAtom = "-->",
+        YArgs = [PredTerm0, GoalTerm0],
         term.coerce(PredTerm0, PredTerm1),
         parse_purity_annotation(PredTerm1, DCGLambdaPurity, PredTerm),
         parse_dcg_pred_expression(PredTerm, Groundness, EvalMethod, Vars0,
@@ -998,19 +966,17 @@
                 Vars1 = Vars0 ++
                     [term.variable(DCG0, Context),
                     term.variable(DCGn, Context)],
-                build_lambda_expression(X, Purity, DCGLambdaPurity,
+                build_lambda_expression(XVar, Purity, DCGLambdaPurity,
                     Groundness, pf_predicate, EvalMethod, Vars1, Modes, Det,
                     ParsedGoal, Context, MainContext, SubContext,
-                    Goal0, 0, NumAdded, !.SVarState, !SVarStore, !VarSet,
+                    Goal0, !.SVarState, !SVarStore, !VarSet,
                     !ModuleInfo, !QualInfo, !Specs),
-                Goal0 = hlds_goal(GoalExpr, GoalInfo0),
-                goal_info_set_purity(Purity, GoalInfo0, GoalInfo),
-                Goal = hlds_goal(GoalExpr, GoalInfo)
+                goal_set_purity(Purity, Goal0, Goal),
+                Expansion = expansion(not_fgti, cord.singleton(Goal))
             ;
                 MaybeParsedGoal = error1(ParsedGoalSpecs),
                 !:Specs = ParsedGoalSpecs ++ !.Specs,
-                Goal = true_goal,
-                NumAdded = 0
+                Expansion = expansion(not_fgti, cord.singleton(true_goal))
             )
         )
     ).
@@ -1042,17 +1008,15 @@
     ho_groundness::in, pred_or_func::in, lambda_eval_method::in,
     list(prog_term)::in, list(mer_mode)::in, determinism::in, goal::in,
     prog_context::in, unify_main_context::in, unify_sub_contexts::in,
-    hlds_goal::out, num_added_goals::in, num_added_goals::out,
-    svar_state::in, svar_store::in, svar_store::out,
+    hlds_goal::out, svar_state::in, svar_store::in, svar_store::out,
     prog_varset::in, prog_varset::out,
     module_info::in, module_info::out, qual_info::in, qual_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
 build_lambda_expression(X, UnificationPurity, LambdaPurity, Groundness,
         PredOrFunc, EvalMethod, Args0, Modes, Det, ParsedGoal,
-        Context, MainContext, SubContext, Goal, !NumAdded,
-        OutsideSVarState, !SVarStore, !VarSet,
-        !ModuleInfo, !QualInfo, !Specs) :-
+        Context, MainContext, SubContext, Goal, OutsideSVarState,
+        !SVarStore, !VarSet, !ModuleInfo, !QualInfo, !Specs) :-
     % In the parse tree, the lambda arguments can be any terms, but in the HLDS
     % they must be distinct variables. So we introduce fresh variables
     % for the lambda arguments, and add appropriate unifications.
@@ -1107,9 +1071,9 @@
 
             % Create fresh variables, transform the goal to HLDS, and
             % add unifications with the fresh variables. We use varset.new_vars
-            % rather than make_fresh_arg_vars, since for functions we need
-            % to ensure that the variable corresponding to the function result
-            % term is a new variable, to avoid the function result term
+            % rather than make_fresh_arg_vars_subst_svars, since for functions
+            % we need to ensure that the variable corresponding to the function
+            % result term is a new variable, to avoid the function result term
             % becoming lambda-quantified.
 
             list.length(Args, NumArgs),
@@ -1140,13 +1104,12 @@
             HeadBefore0 = true_goal,
             insert_arg_unifications(NonOutputLambdaVars, NonOutputArgs,
                 Context, ArgContext, HeadBefore0, HeadBefore,
-                !NumAdded, !SVarState, !SVarStore, !VarSet,
+                !SVarState, !SVarStore, !VarSet,
                 !ModuleInfo, !QualInfo, !Specs),
 
             transform_goal_expr_context_to_goal(loc_whole_goal, ParsedGoal,
-                Substitution, Body, BodyAdded, !SVarState, !SVarStore,
+                Substitution, Body, !SVarState, !SVarStore,
                 !VarSet, !ModuleInfo, !QualInfo, !Specs),
-            !:NumAdded = !.NumAdded + BodyAdded,
 
             % Create the unifications that need to come after the body of the
             % lambda expression; those corresponding to args whose mode is
@@ -1154,7 +1117,7 @@
             HeadAfter0 = true_goal,
             insert_arg_unifications(OutputLambdaVars, OutputArgs,
                 Context, ArgContext, HeadAfter0, HeadAfter,
-                !NumAdded, !SVarState, !SVarStore, !VarSet,
+                !SVarState, !SVarStore, !VarSet,
                 !ModuleInfo, !QualInfo, !Specs),
 
             trace [compiletime(flag("debug-statevar-lambda")), io(!IO)] (
@@ -1218,7 +1181,8 @@
             ),
 
             LambdaRHS = rhs_lambda_goal(LambdaPurity, Groundness, PredOrFunc,
-                EvalMethod, LambdaNonLocals, LambdaVars, Modes, Det, HLDS_Goal),
+                EvalMethod, LambdaNonLocals, LambdaVars, Modes, Det,
+                HLDS_Goal),
             make_atomic_unification(X, LambdaRHS, Context, MainContext,
                 SubContext, UnificationPurity, Goal, !QualInfo)
         )
@@ -1264,18 +1228,6 @@
 
 %-----------------------------------------------------------------------------%
 
-:- pred term_is_ground(term(T)::in) is semidet.
-
-term_is_ground(term.functor(_, Terms, _)) :-
-    terms_are_ground(Terms).
-
-:- pred terms_are_ground(list(term(T))::in) is semidet.
-
-terms_are_ground([]).
-terms_are_ground([Term | Terms]) :-
-    term_is_ground(Term),
-    terms_are_ground(Terms).
-
 :- pred arg_context_to_unify_context(arg_context::in, int::in,
     unify_main_context::out, unify_sub_contexts::out) is det.
 
@@ -1302,29 +1254,35 @@
 
 %-----------------------------------------------------------------------------%
 
-make_fresh_arg_vars(Args, Vars, !VarSet, !SVarState, !Specs) :-
+make_fresh_arg_vars_subst_svars(Args, Vars, !VarSet, !SVarState, !Specs) :-
     % For efficiency, we construct `Vars' backwards and then reverse it
     % to get the correct order.
-    make_fresh_arg_vars_loop(Args, [], RevVars, !VarSet, !SVarState, !Specs),
+    make_fresh_arg_vars_subst_svars_loop(Args, [], RevVars,
+        !VarSet, !SVarState, !Specs),
     list.reverse(RevVars, Vars).
 
-:- pred make_fresh_arg_vars_loop(list(prog_term)::in, list(prog_var)::in,
-    list(prog_var)::out, prog_varset::in,prog_varset::out,
-    svar_state::in, svar_state::out,
+:- pred make_fresh_arg_vars_subst_svars_loop(list(prog_term)::in,
+    list(prog_var)::in, list(prog_var)::out,
+    prog_varset::in,prog_varset::out, svar_state::in, svar_state::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-make_fresh_arg_vars_loop([], !RevVars, !VarSet, !SVarState, !Specs).
-make_fresh_arg_vars_loop([Arg | Args], !RevVars, !VarSet, !SVarState,
-        !Specs) :-
-    make_fresh_arg_var(Arg, Var, !.RevVars, !VarSet, !SVarState, !Specs),
+make_fresh_arg_vars_subst_svars_loop([], !RevVars,
+        !VarSet, !SVarState, !Specs).
+make_fresh_arg_vars_subst_svars_loop([Arg | Args], !RevVars,
+        !VarSet, !SVarState, !Specs) :-
+    make_fresh_arg_var_subst_svars(Arg, Var, !.RevVars, !VarSet,
+        !SVarState, !Specs),
     !:RevVars = [Var | !.RevVars],
-    make_fresh_arg_vars_loop(Args, !RevVars, !VarSet, !SVarState, !Specs).
+    make_fresh_arg_vars_subst_svars_loop(Args, !RevVars, !VarSet,
+        !SVarState, !Specs).
 
-:- pred make_fresh_arg_var(prog_term::in, prog_var::out, list(prog_var)::in,
+:- pred make_fresh_arg_var_subst_svars(prog_term::in, prog_var::out,
+    list(prog_var)::in,
     prog_varset::in, prog_varset::out, svar_state::in, svar_state::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-make_fresh_arg_var(Arg0, Var, Vars0, !VarSet, !SVarState, !Specs) :-
+make_fresh_arg_var_subst_svars(Arg0, Var, Vars0, !VarSet, !SVarState,
+        !Specs) :-
     substitute_state_var_mapping(Arg0, Arg, !VarSet, !SVarState, !Specs),
     (
         Arg = term.variable(ArgVar, _),
cvs diff: Diffing notes
Index: notes/compiler_design.html
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/notes/compiler_design.html,v
retrieving revision 1.154
diff -u -b -r1.154 compiler_design.html
--- notes/compiler_design.html	13 Feb 2012 00:11:53 -0000	1.154
+++ notes/compiler_design.html	13 Apr 2012 05:37:50 -0000
@@ -607,6 +607,10 @@
 <dd> Defines the inst_graph data type,
 which describes the structures of insts for constraint based mode analysis,
 as well as predicates operating on that type.
+
+<dt> from_ground_term_util.m
+<dd> Contains types and predicates for operating on
+from_ground_term scopes and their contents.
 </dl>
 
 <h4> 2. Semantic analysis and error checking </h4>
--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to:       mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions:          mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------



More information about the reviews mailing list