%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Copyright (C) 1989 Peter Van Roy and Regents of the University of California

% Code generation for unification.
% by Peter Van Roy

% Unification with a term is unraveled into a tree of explicit code.
% For clarity and ease of development this code is written using the
% Extended DCG notation.

% This code can be sped up somewhat by getting the type of an argument X
% first and then doing a simple case selection on it, instead of redoing
% the ctest selections everywhere.

% This module reuses code for write mode unification of the last argument.
% This reduces nested code size from O(N*N) to O(N) when there is deep
% recursion in the last argument of nested compound terms. This is especially
% useful for long immediate lists.

% Modes are taken into account to reduce the number of moves, trails, derefs,
% and multiway branches.  A mode is given as a logical formula F.

% Unitialized variables are taken into account.  They are given as modes
% uninit(reg,V,[]) and uninit(mem,V,[]) in F.

% Argument ISF contains the variables that have already
% been initialized upon entry of this code (except for the uninit variables).
% The others are initialized by this code when first encountered.  For example,
% in a head unification ISF contains the set of head arguments.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Extended DCG notation declarations:

% *** Description of accumulators:
% sf = set of variables that are currently initialized (i.e. NOT including um).
% vl = list of variables used in order of occurrence.  For register allocation.
% form = logical mode formula that currently holds.
% code = list of instructions generated.
% offset = offset into block of writemode code being generated.
% gnd = the set of all variables implied to be ground by the formula.
% *** Description of passed arguments:
% fail = the failure address.
% type = the type of the compound term being unified in read-mode unification.
% um = the set of uninitialized memory variables.
% top = the variable X during the writemode unification of X=Term.
% aun = allowed uninit, vars allowed to be created uninit (see clause_code.pl).

% *** Accumulators:
acc_info(    sf, V,  InSF,  OutSF, includev(V,InSF,OutSF)).
acc_info(   gnd, X, InGnd, OutGnd, includev(X,InGnd,OutGnd)).
acc_info(   drf, D, InDrf, OutDrf, includev(D,InDrf,OutDrf)).
acc_info(    vl, V,   Out,     In, Out=[V|In]).
acc_info(  form, F,   InF,   OutF, update_formula(F,InF,OutF)).
acc_info(  code, I,   Out,     In, Out=[I|In]).
acc_info(offset, S, InOff, OutOff, (OutOff is InOff+S)).

acc_info(newvar, V,   Out,     In, Out=[V|In]).
acc_info(  conj, C,   Out,     In, Out=(C,In)).

% *** Passed arguments:
pass_info(fail).
pass_info(type).
pass_info(aun, []).
pass_info(um, []).
pass_info(top, none).

% *** Predicates:
pred_info(       unify, 1,   [           aun,sf,vl,form,fail,code]).
pred_info(     unify_2, 2,   [drf,gnd,um,aun,sf,vl,form,fail,code]).
pred_info(     unify_3, 2,   [drf,gnd,um,aun,sf,vl,form,fail,code]).
pred_info(unify_3_conj, 1,   [drf,gnd,um,aun,sf,vl,form,fail,code]).
pred_info(unify_nonvar, 2,   [drf,gnd,um,aun,sf,vl,form,fail,code]).
pred_info(unify_nonvar, 4,   [drf,gnd,um,aun,sf,vl,form,fail,code]).
pred_info(   unify_var, 2,   [drf,gnd,um,aun,sf,vl,form,fail,code]).
pred_info(    unify_rm, 5,   [drf,gnd,um,aun,sf,vl,form,fail,code]).
pred_info(    unify_rm, 8,   [drf,gnd,um,aun,sf,vl,     fail     ]).
pred_info(    unify_wm, 4,   [drf,gnd,um,aun,sf,vl,form,fail,code]).
pred_info(    unify_wm, 8,   [drf,gnd,um,       vl,     fail     ]).
pred_info(  unify_args, 5,   [drf,gnd,um,aun,sf,vl,form,fail,code,type]).
pred_info(  unify_args, 6,   [drf,gnd,um,aun,sf,vl,form,fail,code,type]).
pred_info(   unify_arg, 7,   [drf,gnd,um,aun,sf,vl,form,fail,code,type]).
pred_info(  init_unify, 4,   [drf,gnd,um,aun,sf,vl,form,fail,code]).
pred_info( xinit_unify, 4,   [drf,gnd,um,aun,sf,vl,form,fail,code]).
pred_info(uninit_unify, 4,   [drf,gnd,um,aun,sf,vl,form,     code]).
pred_info( unify_var_i, 2,   [drf,gnd,um,aun,sf,vl,form,fail,code]).
pred_info( unify_var_i, 4,   [drf,gnd,um,aun,sf,vl,form,fail,code]).
pred_info( unify_var_u, 2,   [drf,gnd,um,    sf,vl,form,     code]).

% Writemode routines:
pred_info(    create_arg, 2, [           sf,vl,form,     code]).
pred_info(    new_var_nf, 1, [           sf,vl,          code]).
pred_info(    new_var_nf, 2, [           sf,vl,          code]).
pred_info(new_umemvar_nf, 1, [           sf,vl,          code]).
pred_info(       new_var, 1, [           sf,vl,form,     code]).
pred_info(       new_var, 2, [           sf,vl,form,     code]).
pred_info(      new_vars, 1, [           sf,vl,form,     code]).
pred_info(  new_var_list, 2, [           sf,vl,form,     code]).
pred_info(     writemode, 1, [    um,    sf,vl,          code]).
pred_info(     writemode, 5, [    um,aun,sf,vl,form,     code]).
pred_info(   b_writemode, 2, [    um,aun,sf,vl,form,     code,top,offset]).
pred_info(   b_writeargs, 4, [    um,aun,sf,vl,form,     code,top,offset]).
pred_info(    fill_slots, 2, [    um,aun,sf,vl,form,     code,top]).
pred_info(initialize_var, 2, [    um,aun,sf,vl,form,     code,top]).
pred_info(  push_if_init, 2, [    um,aun,sf,vl,form,     code,top]).
pred_info( is_uninit_mem, 1, [    um,    sf,   form          ]).

% Small utilities:
pred_info(          move_arg, 5, [drf,gnd,sf,vl,form,code,type]).
pred_info(          move_arg, 3, [drf,gnd,sf,vl,form,code,type]).
pred_info(    gnd_drf_update, 2, [drf,gnd,      form]).
pred_info(        drf_update, 2, [drf,          form]).
pred_info(      pragma_align, 2, [code]).
pred_info(        pragma_tag, 2, [code]).
pred_info(   cond_pragma_tag, 2, [code]).
pred_info(   pragma_tag_form, 1, [form,code]).
pred_info(         align_pad, 1, [code]).
pred_info(       uninit_dest, 3, [um]).
pred_info(         cond_pref, 1, [vl]).
pred_info(       uninit_bind, 2, [um,vl,form,code]).
pred_info(       uninit_move, 2, [um,   form,code]).
pred_info(      term_formula, 2, [form]).
pred_info(fence_if_nosurvive, 0, [vl]).
pred_info(     unify_depth_2, 3, [conj,newvar]).
pred_info(     unify_depth_2, 5, [conj,newvar]).

% These routines are defined externally:
pred_info( remove_uninit, 1, [form]).
pred_info( remove_uninit, 2, [form]).
pred_info(          ct_u, 1, [form,gnd]).
pred_info(         ctest, 1, [form]).
pred_info(         rtest, 2, [   form,fail,code]).
pred_info(      rtest_in, 2, [   form,fail,code]).
pred_info(   rtest_deref, 2, [vl,form,     code]).
pred_info(rtest_in_deref, 2, [vl,form,     code]).
pred_info(          rt_d, 2, [vl,form,     code,drf]).
pred_info(       rt_in_d, 2, [vl,form,     code,drf]).

% Versions of ctest, rtest_deref, rtest_in_deref that use local information:
% This one is better able to see if an argument is nonvar:
ct_u(nonvar(X)) -->> Gnd/gnd, {inv(X, Gnd)}, !.
ct_u(Test)      -->> ctest(Test).

% These are better able to see if an argument is deref:
rt_d(X, X) -->> Drf/drf, {inv(X, Drf)}, !.
rt_d(X, T) -->> rtest_deref(X, T).

rt_in_d(X, X) -->> Drf/drf, {inv(X, Drf)}, !.
rt_in_d(X, T) -->> rtest_in_deref(X, T).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% *** Main Entry Points ***
% Given:
%	ISF	set of variables that occurred before execution (In So Far).
%		This also contains the uninit variables.  However, the internal
%		SF contains only initialized variables, NO uninit variables.
%	IF	the mode formula true before execution (In Formula).
%	Fail	label to jump to on failure.
% Calculates:
%	UM	set of uninit mem variables in IF.
% Returns code for the unification X=Y, along with:
%	OSF	set of variables after execution that have occurred before
%		execution (Out So Far),	including uninits in the unification.
%	VList	list of all variables' usages, for register allocation.
%	OF	the updated IF, with uninit goals removed (Out Formula).
%		A variable is only uninit once, after that it becomes init.
unify(X=Y, ISF, OSF, IF) --> unify(X=Y, ISF, OSF, _, IF).
unify(X=Y, ISF, OSF, VList, IF) -->
	unify(X=Y, VList, ISF, OSF, IF, _).
unify(X=Y, VList, ISF, OSF, IF, OF) -->
	unify(X=Y, ISF, OSF, VList, [], IF, OF).
unify(X=Y, ISF, OSF, Vs, Vl, IF, OF) -->
	{varset(X=Y, Aun)},
	unify(X=Y, Aun, ISF, OSF, Vs, Vl, IF, OF, fail).

% Call from clause_code.pl:
% Aun = set of variables allowed to be created as uninit.
unify_goal(Unify, VList, Aun, ISF, OSF, IF, OF) -->
	unify(Unify, Aun, ISF, OSF, VList, [], IF, OF, fail).

% *** Interface between the unification compiler & rest of compiler ***
% This top level call interfaces between the form of SF needed in unification
% compilation (which contains only inits) and in the rest of the compiler
% (which contains all variables with a value, init and uninit).
% Also calculates Gnd & UM, and updates the mode formula.
unify(X=Y) -->>
	% Internal InSF contains only initialized variables:
	insert(ExtInSF, IntInSF):sf,
	IF/form,
	{uninit_set(IF, UnAll)},
	{diffv(ExtInSF, UnAll, IntInSF)},
		% Call to the internal unification compiler:
		{grounds_in_form(IF, Gnd)},
		{rderef_set(IF, Drf)},
		{intersectv(Drf, Gnd, StayDrf)},
		{uninit_set_type(mem, IF, UM)},
		unify_2(X, Y):[drf(StayDrf,_),gnd(Gnd,_),um(UM)],
	% External OutSF contains both init and uninit variables:
	insert(IntOutSF, ExtOutSF):sf,
	{varset(X=Y, Vars), unionv(IntOutSF, Vars, ExtOutSF)},
	% Update the mode formula:
	{intersectv(UnAll, IntOutSF, OutInit)},
	remove_uninit(OutInit),
	update_formula(X=Y, ExtInSF):form.
unify((U1,U2)) -->> unify(U1), unify(U2).

% *** Internal Routines ***

% This starts with two stub routines, followed by
% unify_var, uninit_unify and init_unify, which do the main work.
% Also includes unify_rm and unify_wm, which do the read and
% write mode compilation, and writemode, which creates the
% block of moves for write mode creation of compound terms.

% Take care of the order of terms X and Y and of unifying two nonvars:
unify_2(X, Y) -->> {   var(X),    var(Y)}, !, unify_var(X, Y).
unify_2(X, Y) -->> {   var(X), nonvar(Y)}, !, unify_3(X, Y).
unify_2(X, Y) -->> {nonvar(X),    var(Y)}, !, unify_3(Y, X).
unify_2(X, Y) -->> {nonvar(X), nonvar(Y)}, !, unify_nonvar(X, Y).

% Unifying two nonvariables together:
unify_nonvar(X, Y) -->> {functor(X, N, A), functor(Y, N, A)}, !,
	unify_nonvar(X, Y, 1, A).
unify_nonvar(X, Y) -->> [fail]:code, [fail]:form.

unify_nonvar(X, Y, I, A) -->> {I>A}, !.
unify_nonvar(X, Y, I, A) -->> {I=<A}, !,
	{arg(I, X, Xi)},
	{arg(I, Y, Yi)},
	unify_2(Xi, Yi),
	{I1 is I+1},
	unify_nonvar(X, Y, I1, A).

% Take care of distinction that X is initialized vs. uninitialized
% and do the depth limiting transformation for the unification
% of an initialized variable that is not known to be ground.
unify_3(X, Y) -->> SF/sf, {\+inv(X, SF)}, !,
	uninit_unify(X, Y, nonlast, _),
	[X]:sf.
unify_3(X, Y) -->> Gnd/gnd, {inv(X, Gnd)}, !,
	init_unify(X, Y, nonlast, _).
unify_3(X, Y) -->>
	{unify_depth(X, Y, NewY, _Vars, Conj)},
	init_unify(X, NewY, nonlast, _),
	unify_3_conj(Conj).

% The added unifications take advantage of a full unify_2
% (which is effectively unify_var or uninit_unify):
unify_3_conj(true) -->> [].
unify_3_conj((X=Y,Conj)) -->> unify_2(X, Y), unify_3_conj(Conj).

% *** Unifying two variables together:
unify_var(X, Y) -->> SoFar/sf, {inv(X, SoFar),   inv(Y, SoFar)}, !,
	unify_var_i(X, Y).
unify_var(X, Y) -->> SoFar/sf, {inv(X, SoFar), \+inv(Y, SoFar)}, !,
	uninit_dest(Y, YDest, Flag),
	cond_pref(Flag),
	[X,Y]:vl,
	map_formula(X, Y):form,
	cond_pragma_tag(Flag, Y),
	[move(X,YDest)]:code,
	[Y]:sf.
unify_var(X, Y) -->> SoFar/sf, {\+inv(X, SoFar),   inv(Y, SoFar)}, !,
	uninit_dest(X, XDest, Flag),
	cond_pref(Flag),
	[Y,X]:vl,
	map_formula(Y, X):form,
	cond_pragma_tag(Flag, X),
	[move(Y,XDest)]:code,
	[X]:sf.
unify_var(X, Y) -->> SoFar/sf, {\+inv(X, SoFar), \+inv(Y, SoFar)}, !,
	unify_var_u(X, Y).

% Conditional preference: if Flag is yes, then create a 'pref' flag
% in the varlist.  This is a suggestion to regalloc for improving
% register allocation.  It does not affect correctness.
cond_pref(yes) -->> !, [pref]:vl.
cond_pref( no) -->> !, [].

% Conditional tag pragma: insert a variable tag pragma if it's a store.
cond_pragma_tag(yes, _) -->> [].
cond_pragma_tag(no,  X) -->> pragma_tag(X, var).

% Location of an uninit X's value depends on whether it is in
% memory or not:
uninit_dest(X,  X, yes) -->> UM/um, \+inv(X, UM), !.
uninit_dest(X, [X], no) -->> UM/um,   inv(X, UM), !.

% Create a new formula containing terms for both X and Y by mapping
% the existing formula.  Relies on the fact that Y remains dereferenced
% if X is dereferenced, even if Y is uninit(mem).  This condition is
% enforced by clause_code.
map_formula(X, Y, InF, OutF) :-
	map_terms([X], [Y], InF, InFY),
	union_formula(InF, InFY, OutF).

% Both variables are initialized:
% There are many special cases handled here which result in better code.
% This routine is careful to make sure that the oldest variable is always
% bound to the youngest.
unify_var_i(X, Y) -->> Form/form, {atomic_value(Form, X, A)}, !,
	unify_2(Y, A).
unify_var_i(X, Y) -->> Form/form, {atomic_value(Form, Y, A)}, !,
	unify_2(X, A).
unify_var_i(X, Y) -->> ctest(atomic(X)), ctest(atomic(Y)), !,
	rtest_in_deref(X, T),
	rtest_in_deref(Y, U),
	[T,U]:vl,
	Fail/fail,
	[equal(T,U,Fail)]:code.
unify_var_i(X, Y) -->>
	Form/form,
	{unify_flag(Form, X, Xf)},
	{unify_flag(Form, Y, Yf)},
	unify_var_i(Xf, Yf, X, Y).

unify_var_i(var, nonvar, X, Y) -->> !,
	rtest_in_deref(X, T),
	rtest_in(trail(T), T),
	[Y,T]:vl,
	pragma_tag_form(T),
	[move(Y,[T])]:code.
unify_var_i(nonvar, var, X, Y) -->> !,
	rtest_in_deref(Y, T),
	rtest_in(trail(T), T),
	[X,T]:vl,
	pragma_tag_form(T),
	[move(X,[T])]:code.
unify_var_i(Xf, Yf, X, Y) -->>
	rtest_in_deref(X, T),
	rtest_in_deref(Y, U),
	[pref,T,U]:vl,
	fence_if_nosurvive,
	Fail/fail,
        [unify(T,U,Xf,Yf,Fail)]:code, % *** Call to general unify ***
	remove_vars:form.	% Because binding has many effects.

% Insert 'fence' if general unification kills all registers:
% This is needed for register allocation.  See regalloc.
fence_if_nosurvive -->> {  survive('$unify'(_,_))}, !.
fence_if_nosurvive -->> {\+survive('$unify'(_,_))}, !, [fence]:vl.

% Flag whether X is known to be variable, nonvariable or not:
% (This allows some optimization in the translator.)
unify_flag(Form, X, nonvar) :- implies(Form, nonvar(X)), !.
unify_flag(Form, X,    var) :- implies(Form, var(X)), !.
unify_flag(Form, X,    '?').

% Both variables are uninitialized:
unify_var_u(X, Y) -->> UM/um, {inv(X, UM), inv(Y, UM)}, !,
	[X,Y]:sf,
	[deref(X),deref(Y),var(X),var(Y)]:form,
	[X,pref,X,Y]:vl,
	pragma_tag(X, var),
	[move(X,[X])]:code,
	pragma_tag(Y, var),
	[move(X,[Y])]:code.
unify_var_u(X, Y) -->> UM/um, {inv(X, UM), \+inv(Y, UM)}, !,
	[X,Y]:sf,
	[deref(X),deref(Y),var(X),var(Y)]:form,
	[X,pref,X,Y]:vl,
	pragma_tag(X, var),
	[move(X,[X])]:code,
	[move(X,Y)]:code.
unify_var_u(X, Y) -->> UM/um, {\+inv(X, UM), inv(Y, UM)}, !,
	[X,Y]:sf,
	[deref(X),deref(Y),var(X),var(Y)]:form,
	[pref,Y,X,X]:vl,
	[move(Y,X)]:code,
	pragma_tag(X, var),
	[move(X,[X])]:code.
unify_var_u(X, Y) -->> UM/um, {\+inv(X, UM), \+inv(Y, UM)}, !,
	new_var_nf(X, Y).

% *** Uninit_unify assumes X has not yet been initialized:
uninit_unify(X, Term, Last, [Lbl|LLbls]) -->> {compound(Term)}, !,
	uninit_bind(X, Term),
	writemode(Last, X, Term, Lbl, LLbls).
uninit_unify(X, Term, Last, LLbls) -->> {atomic(Term)}, !,
	uninit_bind(X, Term).
uninit_unify(X, Var, Last, LLbls) -->> {var(Var)}, !,
	unify_var(X, Var).

% Bind X to a nonvariable and update the mode formula:
uninit_bind(X, Term) -->>
	[X]:vl,
	{make_word(Term, Word)},
	uninit_move(Word, X),
	term_formula(X, Term).

% Move to an uninit variable:
% Recognizes that the destination of an uninit_mem variable is in memory.
uninit_move(Word, X) -->> UM/um, {\+inv(X, UM)}, !,
	[deref(X)]:form,
	[move(Word,X)]:code.
uninit_move(Word, X) -->> UM/um,   {inv(X, UM)}, !,
	pragma_tag(X, var),
	[move(Word,[X])]:code.

% Update the formula for X assuming it is unified with Term:
term_formula(X, Term) -->> {nonvar(Term)}, !,
	{functor(Term, Na, Ar)},
	['$name_arity'(X,Na,Ar)]:form.
term_formula(X, Term) -->> {var(Term)}, !.

% *** Init_unify assumes X has already been initialized:

% Hook to trim mode formula for speed:
init_unify(X, T, L, LL) -->>
	insert(InF, InInitF):form,
	SoFar/sf,
	{split_formula(_, SoFar, X=T, InF, InInitF, RestF)},
	xinit_unify(X, T, L, LL),
	insert(OutInitF, OutF):form,
	{combine_formula(OutInitF, RestF, OutF)}.

xinit_unify(X, Term, Last, [Lbl|LLbls]) -->> {atomic(Term)}, ct_u(nonvar(X)),!,
	rtest_deref(X, T),
	unify_rm(T, Term, Last, LLbls, no).
xinit_unify(X, Term, Last, [Lbl|LLbls]) -->>{compound(Term)}, ct_u(nonvar(X)),!,
	rtest_deref(X, T),
	{term_test(Term, T, Test)},
	rtest(Test, T),
	unify_rm(T, Term, Last, LLbls, no).
xinit_unify(X, Term, Last, [Lbl|LLbls]) -->> {nonvar(Term)}, ctest(var(X)), !,
	rtest_deref(X, T),
	unify_wm(T, Term, Last, LLbls).
xinit_unify(X, Term, Last, [Lbl|LLbls])-->>{compile_option(uni),atomic(Term)},!,
	rtest_deref(X, T),
	rtest_in(trail_if_var(T), T),
	{term_tag(Term, Tag)},
	{make_word(Term, _, Word)},
	Fail/fail,
	[T]:vl,
	[unify_atomic(T,Word,Fail)]:code.
% This clause merges the output formulas from unify_rm and unify_wm:
xinit_unify(X, Term, Last, [Lbl|LLbls]) -->> {nonvar(Term)}, !,
	rtest_deref(X, T),
	{term_tag(Term, Tag)},
	{term_test(Term, T, Test)},
	Fail/fail,
	[T]:vl,
	[switch(unify,Tag,T,Write,Read,Fail)]:code,
	insert(Form, OutF):form,
	{update_formula(var(T), Form, WForm)},
	SoFar/sf,
	unify_wm(T, Term, Last, LLbls, SoFar, WForm, OutFW, Write),
	{update_formula(Test, Form, RForm)},
	unify_rm(T, Term, Last, LLbls, yes, RForm, OutFR, Read),
	{intersect_formula(OutFW, OutFR, OutF)}.
xinit_unify(X, Term, Last, [Lbl|LLbls]) -->> {var(Term)}, !,
	unify_var(X, Term).

% wm hook: Ignore output of sf.  Return vl, code list and output of form.
% It is assumed that using aun=[] guarantees that wm and rm initialize
% the same variables.
unify_wm(X, T, Last, LLbls, SF, IF, OF, Code) -->>
	unify_wm(X,T, Last, LLbls):[aun([]),form(IF,OF),sf(SF,_),code(Code,[])].

% rm hook: Return sf, vl, code list, and output of form.
unify_rm(X, T, Last, LLbls, Opt, IF, OF, Code) -->>
	unify_rm(X, T, Last, LLbls, Opt):[form(IF,OF),code(Code,[])].

% *** Unify_rm assumes X is a dereferenced nonvariable at run-time and Term is
%     a nonvariable at compile-time.
%     Matching between X and Term's tags is assumed to be done elsewhere.
unify_rm(X, Term, Last, LLbls, Opt) -->> {structure(Term)}, !,
	[X]:vl,
	{functor(Term, N, A), Term=..[N|Args]},
	rtest_in('$name_arity'(X,N,A), X),
	unify_args(Args, 1, X, LLbls, Opt):type(structure).
unify_rm(X, Term, Last, LLbls, Opt) -->> {cons(Term)}, !,
	[X]:vl,
	{Term=[Hd|Tl], Args=[Hd,Tl]},
	unify_args(Args, 0, X, LLbls, Opt):type(cons).
unify_rm(X, Term, Last, LLbls, Opt) -->> {atom(Term)}, !,
	[X]:vl,
	rtest_in('$name_arity'(X,Term,0), X).
unify_rm(X, Term, Last, LLbls, Opt) -->> {number(Term)}, !,
	[X]:vl,
	rtest_in('$name_arity'(X,Term,0), X).

% *** Unify_wm assumes X is initialized, unbound, and dereferenced at run-time
%     and Term is a nonvariable at compile-time.
unify_wm(X, Term, Last, [Lbl|LLbls]) -->>
	{compound(Term)}, !,
	[X]:vl,
	rtest_in(trail(X), X),
	{term_tag(Term, Tag)},
	pragma_tag(X, var),
	[move(Tag^r(h),[X])]:code,
	writemode(Last, X, Term, Lbl, LLbls).
unify_wm(X, Term, Last, LLbls) -->>
	{atom(Term)}, !,
	[X]:vl,
	{term_tag(Term, Tatm)},
	rtest_in(trail(X), X),
	pragma_tag(X, var),
	[move(Tatm^Term,[X])]:code.
unify_wm(X, Term, Last, LLbls) -->>
	{number(Term)}, !,
	[X]:vl,
	rtest_in(trail(X), X),
	pragma_tag(X, var),
	[move(Term,[X])]:code.

% Unification of the arguments of a structure.
% Two optimizations are done:
% 1. Use single move instruction when an argument is a first-occurrence
%    variable. (Why doesn't preferred allocation make this unnecessary?)
% 2. Group pairs of moves together to facilitate creating double word loads.
%    InV gives arguments whose moves have already been created.
unify_args(Args, I, X, LLbls, Opt) -->> unify_args([], Args, I, X, LLbls, Opt).

unify_args( [],  [], I, X, LLbls, Opt) -->> !.
unify_args(InV, [A], I, X, LLbls, no) -->> !,
	unify_arg(InV, _, A, I, X, nonlast, LLbls).
unify_args(InV, [A], I, X, LLbls, yes) -->> !,
	unify_arg(InV, _, A, I, X, last, LLbls).
unify_args( [], [A,B|Args], I, X, LLbls, Opt) -->>
	{align(2), 0 is I mod 2}, !,
	move_arg(X, I, Y1),
	{I1 is I+1},
	move_arg(X, I1, Y2),
	unify_args([Y1,Y2], [A,B|Args], I, X, LLbls, Opt).
unify_args(InV, [A,B|Args], I, X, LLbls, Opt) -->> !,
	unify_arg(InV, OutV, A, I, X, nonlast, _),
	{I1 is I+1},
	unify_args(OutV, [B|Args], I1, X, LLbls, Opt).

% Unification of one structure argument:
% Optimize the case when A is a first-occurrence variable.
% (Note that sf may become unsorted because of this, requiring a sort.)
unify_arg(InV, OutV, A, I, X, Last, LLbls) -->> {var(A)},
	SoFar/sf, {\+inv(A,SoFar)},
	UM/um, {\+inv(A,UM)}, !,
	move_arg(InV, OutV, X, I, A),
	sort:sf.
unify_arg(InV, OutV, A, I, X, Last, LLbls) -->>
	move_arg(InV, OutV, X, I, Y),
	init_unify(Y, A, Last, LLbls).

% Get argument only if it hasn't been done earlier:
move_arg([Y|Vs], Vs, X, I, Y) -->> [].
move_arg([],     [], X, I, Y) -->> move_arg(X, I, Y).

% Get argument I of a structure:
move_arg(X, I, Y) -->>
	Type/type,
	pragma_tag(X, Type),
	pragma_align(X, I),
	[move([X+I],Y)]:code,
	[X,Y]:vl,
	[Y]:sf,
	gnd_drf_update(Y, X).

pragma_tag(X, Type) -->>
	{tag(Type, Tag)},
	[pragma(tag(X,Tag))]:code.

% Insert tag pragma from mode formula if the tag is known:
pragma_tag_form(X) -->> F/form, {get_tag(F, X, Tag)}, !,
	[pragma(tag(X,Tag))]:code.
pragma_tag_form(_) -->> [].

pragma_align(X, I) -->>
	{align(K), 0 is I mod K}, !,
	[pragma(align(X,K))]:code.
pragma_align(X, I) -->> [].

% Update gnd and drf sets and the mode formula:
gnd_drf_update(Y, X) -->> Gnd/gnd, {inv(X, Gnd)}, !, [Y]:gnd,
	combine_formula(ground(Y)):form,
	drf_update(Y, X).
gnd_drf_update(_, _) -->> [].

% Only add Y to rderef set if X is ground:
drf_update(Y, X) -->> Drf/drf, {inv(X, Drf)}, !, [Y]:drf,
	combine_formula(rderef(Y)):form.
drf_update(_, _) -->> [].

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Generate a minimal sequence of moves to the global heap to
% create the structure Term (this is write mode unification),
% given that all initialized variables are in ISF.

% *** Create the term and return an argument for it:
create_arg(Var, Var) -->> {var(Var)}, SoFar/sf, {inv(Var, SoFar)}, !.
create_arg(Var, Var2) -->> {var(Var)}, SoFar/sf, {\+inv(Var, SoFar)}, !,
	new_var_nf(Var, Var2).
create_arg(Term, Word) -->> {atomic(Term)}, !, {make_word(Term, Word)}.
create_arg(Term, X) -->> {compound(Term)}, !,
	term_formula(X, Term),
	combine_formula(deref(X)):form,
	[X]:vl,
	[X]:sf, % Added Jan. 11
	{make_word(Term, Word)},
	[move(Word,X)]:code,
	% Interface between internal SF and external SF:
	insert(ExtInSF, IntInSF):sf,
	InF/form,
	{uninit_set(InF, Uninit)},
	{intersectv(ExtInSF, Uninit, UNSF)},
	{diffv(ExtInSF, UNSF, IntInSF)},
	{uninit_set_type(mem, InF, UM)},
		writemode(Term):um(UM),
	insert(IntOutSF, ExtOutSF):sf,
	{unionv(IntOutSF, UNSF, ExtOutSF)}.

% Create an unbound variable:
% (Does not update formula)
new_var_nf(X) -->>
	[X]:sf,
	[X,X]:vl,
	{tag(var, Tvar)},
	[move(Tvar^r(h),X)]:code,
	[pragma(push(variable))]:code,
	[push(X,r(h),1)]:code,
	{align_calc(1, _, Pad)},
	align_pad(Pad).

% Create two identical unbound variables:
% (Does not update formula)
new_var_nf(X, Y) -->>
	{X\==Y}, !,
	[X,Y]:sf,
	[X,pref,X,Y,Y]:vl,
	{tag(var, Tvar)},
	[move(Tvar^r(h),X)]:code,
	[move(Tvar^r(h),Y)]:code,
	[pragma(push(variable))]:code,
	[push(Y,r(h),1)]:code,
	{align_calc(1, _, Pad)},
	align_pad(Pad).
new_var_nf(X, Y) -->>
	{X==Y}, !,
	new_var_nf(X).

% Create an unbound variable:
% (Also updates formula)
new_var(X) -->>
	combine_formula((deref(X),var(X))):form,
	new_var_nf(X).

% Create two identical unbound variables:
% (Also updates formula)
new_var(X, Y) -->>
	{X\==Y}, !,
	combine_formula((deref(X),var(X),deref(Y),var(Y))):form,
	new_var_nf(X, Y).
new_var(X, Y) -->>
	{X==Y}, !,
	new_var(X).

% Create an uninit mem variable:
% (Does not update formula)
new_umemvar_nf(X) -->>
	[X]:sf,
	[X,X]:vl,
	{tag(var, Tvar)},
	[move(Tvar^r(h),X)]:code,
	[adda(r(h),1,r(h))]:code,
	{align_calc(1, _, Pad)},
	align_pad(Pad).

% Create unbound variables for those variables in VarBag that do not
% yet exist.  Both initialized and uninitialized variables are created
% depending on what is in the formula.  It is assumed that SF contains
% all variables that have a value, including both inits and uninits.
new_vars(VarBag) -->>
	{sort(VarBag, Vars)},
	SF/sf, {diffv(Vars, SF, NewVars)},
	F/form,
	{uninit_set_type(mem, F, UMemVars)},
	{uninit_set_type(reg, F, URegVars)},
	{diffv(NewVars, URegVars, IVars)},
	new_var_list(IVars, UMemVars).

new_var_list([], _) -->> [].
new_var_list([V|Vars], UMemVars) -->> {inv(V, UMemVars)}, !,
	new_umemvar_nf(V),
	new_var_list(Vars, UMemVars).
new_var_list([V|Vars], UMemVars) -->> {\+inv(V, UMemVars)}, !,
	new_var(V),
	new_var_list(Vars, UMemVars).

% *** Create a term on the heap:
writemode(Term) -->>
	writemode(nonlast, none, Term, _, _):[form(true,_)].

% *** Most general routine, used as part of unify above:
% Last flag:
%    Last = last: writemode is a jump to Lbl.
%    Last = nonlast: writemode is a full block; it creates LLbls, a list of
%                    labels for nested last arguments to jump to.
% Init flag:
%    Init = init: initialize all new variables in the code.
%    Init = uninit: the new variables are uninit(mem).
writemode(last, X, Term, Lbl, _) -->> !,
	[jump(Lbl)]:code.
writemode(nonlast, X, Term, _, LLbls) -->> !,
	[pragma(push(term(Size)))]:code,
	b_writemode(Term, LLbls):[offset(0,Size),top(X)].

% Create the Block of moves:
b_writemode(Str, LLbls) -->> {structure(Str)}, !,
	tag(atom, Tatm),
	{functor(Str, F, A)},
	[pragma(push(structure(A)))]:code,
	[push(Tatm^(F/A),r(h),1)]:code,
	{Str=..[F|Args]},
	{S is A+1},
	{align_calc(S, Size, Pad)},
	Offset/offset,
	{T is Offset+1},
	[Size]:offset,
	fill_slots(Args, Offsets),
	align_pad(Pad),
	b_writeargs(Args, T, Offsets, LLbls).
b_writemode(Cons, LLbls) -->> {cons(Cons)}, !,
	{Cons=[Hd|Tl], Args=[Hd,Tl]},
	{align_calc(2, Size, Pad)},
	Offset/offset,
	{T is Offset},
	[Size]:offset,
	[pragma(push(cons))]:code,
	fill_slots(Args, Offsets),
	align_pad(Pad),
	b_writeargs(Args, T, Offsets, LLbls).
b_writemode(Atom, []) -->> {atomic(Atom)}, !.
b_writemode(Var,  []) -->> {var(Var)}, !.

b_writeargs([], _, [], []) -->> !.
b_writeargs([A], S, [IO], [Lbl|LLbls]) -->> !,
	Offset/offset,
	{IO is Offset-S},
	[label(Lbl)]:code,
	b_writemode(A, LLbls).
b_writeargs([A,B|Args], S, [IO|Offsets], LLbls) -->> !,
	Offset/offset,
	{IO is Offset-S},
	{S1 is S+1},
	b_writemode(A, _),
	b_writeargs([B|Args], S1, Offsets, LLbls).

fill_slots([], []) -->> !.
fill_slots([A|Args], [Off|Offsets]) -->> !,
	{make_word(A, Off, Word)},
	initialize_var(A, Word),
	fill_slots(Args, Offsets).

make_word(C, Off, (Tcom^(r(h)+Off))) :- compound(C), term_tag(C, Tcom), !.
make_word(A, Off, (Tatm^A))          :- atom(A), term_tag(A, Tatm), !.
make_word(N, Off, N)                 :- number(N), !.
make_word(V, Off, (V))               :- var(V), !.

make_word(C, (Tcom^r(h))) :- compound(C), term_tag(C, Tcom), !.
make_word(A, (Tatm^A))    :- atom(A), term_tag(A, Tatm), !.
make_word(N, N)           :- number(N), !.
make_word(V, (V))         :- var(V), !.

% Initialize first-time variables in write mode:
initialize_var(V, Word) -->> is_uninit_mem(V), !,
	remove_uninit(mem, [V]),
	combine_formula(var(V)):form,
	[V,V]:vl,
	[V]:sf,
	pragma_tag(V, var),
	[move(V,[V])]:code,
	[push(Word,r(h),1)]:code.
initialize_var(V, Word) -->> {var(V)}, SoFar/sf, {\+inv(V, SoFar)}, !,
	{tag(var, Tvar)},
	[V,V]:vl,
	[move(Tvar^r(h),V)]:code,
	push_if_init(V,Word).
initialize_var(V, Word) -->> {var(V)}, SoFar/sf, {  inv(V, SoFar)}, !,
	[V]:vl,
	[push(Word,r(h),1)]:code.
initialize_var(V, Word) -->> {nonvar(V)}, !,
	[push(Word,r(h),1)]:code.

% is_uninit_mem(V) -->> {var(V)}, UM/um, SF/sf, {inv(V,UM), \+inv(V,SF)}, !.
is_uninit_mem(V) -->> {var(V)}, UM/um, SF/sf, {inv(V,UM), \+inv(V,SF)}, !.
is_uninit_mem(V) -->> {var(V)}, ctest(uninit(mem,V)), !.

% Create an uninit(mem) OR an init. var on the heap:
push_if_init(V, Word) -->> Us/aun, inv(V, Us), !,
	[adda(r(h),1,r(h))]:code,
	X/top,
	combine_formula(uninit(mem,V,[X])):form.
push_if_init(V, Word) -->> Us/aun, \+inv(V, Us), !,
	[push(Word,r(h),1)]:code,
	[V]:sf,
	combine_formula((var(V),deref(V))):form.

%*** Predicates used for compound term alignment:

% Calculate alignment value:
% Size is least integer >= S and multiple of alignment constant K:
% Pad is the difference between Size and S.
align_calc(S, Size, Pad) :-
	align(K),
	Size is (S+K-1)//K*K,
	Pad is Size-S.

% Generate pad instruction:
align_pad(0) -->> !.
align_pad(P) -->> {P=\=0}, !, [pad(P)]:code.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% *** Depth limiting in unification: (assumes X is always a variable)
% Ensures that unifications are only nested up to the global depth limit.
% This is done because compilation time and code size for deeply nested
% unifications goes as the square of the size of the term.
% A subterm Y at the depth limit is replaced by a variable Z and
% the goals V=Y, V=Z after the original unification goal.
% Then V=Y is done in writemode and V=Z is done with general unification.
% Also returns the set of the variables Z.
unify_depth(X, Y, NewY, VSet, Flat) :-
	unify_depth_2(0, Y, NewY, Conj, true, VBag, []),
	sort(VBag, VSet),
	flat_conj(Conj, Flat).

unify_depth_2(_, Y, Z) -->> {simple(Y)},            !, {Z=Y}.
unify_depth_2(D, Y, Z) -->> {depth_limit(L), D>=L}, !, [V=Y]:conj, [V=Z]:conj,
	[Z]:newvar,
	{comment(['Found structure ',Y,' at depth ',D])}.
unify_depth_2(D, Y, Z) -->>
	{functor(Y, Na, Ar)},
	{functor(Z, Na, Ar)},
	{D1 is D+1},
	unify_depth_2(1, Ar, D1, Y, Z).

unify_depth_2(I, Ar, D, Y, Z) -->> {I>Ar}, !.
unify_depth_2(I, Ar, D, Y, Z) -->> {I=<Ar}, !,
	{arg(I, Y, Yi)},
	{arg(I, Z, Zi)},
	unify_depth_2(D, Yi, Zi),
	{I1 is I+1},
	unify_depth_2(I1, Ar, D, Y, Z).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%