
%-----------------------------------------------------------------

% Index Mapping
% -------------

% Glossary of symbols...
%
% V       = variable
% F       = function
% X, Y, Z = index
% T       = template
% I       = template dimension
% J       = variable dimension
%
% D, E           = (daughter) node---complicated syntax!
%
% K, L, M, N     = index to template dimension mappings---[] | [X -> I | M]
% P, Q, R, S     = template dimension to index mappings---[] | [I -> X | P]
% A, B           = full index map---map(T, M)
 

% Preprocessing
% -------------


%     Calculate index set for each node.


idxSet(var(V, Ds), var(V, Es, Xs), Xs)         :- idxSetDaughters(Ds, Es, Xs).
idxSet(fun(F, Xs, Ds), fun(F, Xs, Es, Ys, Zs), Zs) :-
    idxSetDaughters(Ds, Es, Ys),
    idxSetArgs(Es, Ys),
    union(Xs, Ys, Zs).
idxSet(arg(Xs, D), arg(Xs, E, _), Zs) :-
    idxSet(D, E, Ys),
    subtract(Ys, Xs, Zs).
idxSet(idx(X), idx(X), [X]).

idxSetDaughters([], [], []).
idxSetDaughters([D | Ds], [E | Es], Zs) :-
    idxSet(D, E, Xs),
    idxSetDaughters(Ds, Es, Ys),
    union(Xs, Ys, Zs).
    
idxSetArgs([], _).
idxSetArgs([arg(Xs, _, Zs) | Ds], Ys) :- union(Xs, Ys, Zs), idxSetArgs(Ds, Ys).


%      Preprocess expression tree prior to mapping.  Turn `var'
% nodes into leaves.  After processing, the only true non-leaf node is
% `nod'.  `arg' is regarded as a modification of a `nod' daughter.
% `arc' is regarded as a modifier on an arc.  (Bit bullshitty).
%
% Analyse subscript expressions for linearity.
% Set up alignment maps for arguments.

preprocess(var(V, Ds, Xs), arc(nod([arc(var(A), B) | Es], C), D)) :-
    varAttr(A), V  := A -> varNam, Xs := A -> idxSet, Subs := A -> subLis,
    arcAttr(B), Xs := B -> idxSet,
    nodAttr(C), Xs := C -> idxSet,
    arcAttr(D), Xs := D -> idxSet,
    preprocessSubs(Ds, Subs, Es).
preprocess(fun(F, Xs, Ds, Ys, Zs), arc(fun(nod(Es, A), B), C)) :-
    nodAttr(A), Ys := A -> idxSet,
    funAttr(B), F  := B -> funNam, Xs := B -> rnkSet,
                                   Zs := B -> idxSet, Resolve := B -> argAln,
    arcAttr(C), Zs := C -> idxSet,
    function(F, Aligns),
    resolveAligns(Aligns, [Resolve | Resolves]),
    preprocessArgs(Ds, Es, Resolves).
preprocess(idx(X), idx(X)).

preprocessSubs([], [], []).
preprocessSubs([D | Ds], [Sub | Subs], [E | Es]) :-
    analyseSub(D, Sub),
    preprocess(D, E),
    preprocessSubs(Ds, Subs, Es).

preprocessArgs([], [], []).
preprocessArgs([arg(Xs, D, Ys) | Ds], [arg(E, A) | Es], [Resolve | Resolves]) :-
    argAttr(A), Xs := A -> rnkSet, Ys := A -> idxSet, Resolve := A -> argAln, 
    preprocess(D, E),
    preprocessArgs(Ds, Es, Resolves).


% Analyse subscript expression for linearity or scalar expression.
% (Will eventually support more general definition of ``linearity''.)

analyseSub(idx(X),              lin(X))  :- !.
analyseSub(var(_, _, []),       exp)     :- !.
analyseSub(fun(_, _, _, _, []), exp)     :- !.
analyseSub(_,                   non).


% Resolve a list of (argument) alignments.  Eg
% 
%   [variable(a, b, [1],      [exp -> 2]),
%    variable(b, c, [3, 2],   [* -> 1]),
%    variable(c, T, [I, J, K], P)].
% 
% could yield
% 
%   [variable(a, T, [K],      [* -> I, exp -> J | P]),
%    variable(b, T, [K, J],   [* -> I | P]),
%    variable(c, T, [I, J, K], P)]
% 
% The alignment chain is terminated on targets which (are uninstantiated
% or) don't appear in the original list.

resolveAligns(Aligns, Resolves) :-
    sameKeys(Aligns, Resolves),
    composeAligns(Resolves, Aligns, Resolves).


sameKeys([], []).
sameKeys([variable(V, _, _, _) | As], [variable(V, _, _, _) | Bs]) :-
    sameKeys(As, Bs).


composeAligns(_, [], []).
composeAligns(Resolves, [Align | AlignsTail], [Resolve | ResolvesTail]) :-
    composeAlign(Resolves, Align, Resolve),
    composeAligns(Resolves, AlignsTail, ResolvesTail).

composeAlign(Resolves, variable(V, T, Is, P), variable(V, U, Ks, S)) :-
    ground(T),
    member(variable(T, U, Js, Q), Resolves), !,
    composeSeqSeq(Is, Js, Ks),
    composeRelSeq(P,  Js, R),
    append(R, Q, S).
composeAlign(_, variable(_, T, Is, P), variable(_, T, Is, P)).


% First argument of `composeSeqSeq' should be fully instantiated on entry.

composeSeqSeq([], _, []).
composeSeqSeq([I | Is], Js, [K | Ks]) :-
    isNth(I, Js, K),
    composeSeqSeq(Is, Js, Ks).

% Range of all mappings in first argument of `composeRelSeq' should be
% instantiated on entry.

composeRelSeq([], _, []).
composeRelSeq([X -> I | M], Js, [X -> K | N]) :-
    isNth(I, Js, K),
    composeRelSeq(M, Js, N).

isNth(*, _, *)        :- !.
isNth(1, [X | _ ], X) :- !.
isNth(N, [_ | Xs], X) :- N1 is N - 1, isNth(N1, Xs, X).

append([], Append, Append).
append([X | Old], Append, [X | New]) :- append(Old, Append, New).

%-----------------------------------------------------------------

% Index mapping
% -------------

% Phase I
% -------
%      Impose horizontal constraints on maps.  Pre-order traversal.


idxMapConstraint(nod(Ds, A), T, N) :-
    Xs := A -> idxSet, B := A -> nodMap,
    alnMap(B), T := B -> parTmp, M := B -> idxMap,
    domain(M, Xs),
    subset(M, N),
    idxMapConstraintDaughters(Ds, T, M).
idxMapConstraint(arc(D, A), U, L)  :-
    Xs := A -> idxSet, B := A -> srcMap, C := A -> dstMap,
    alnMap(B), T := B -> parTmp, M := B -> idxMap,
    alnMap(C), U := C -> parTmp, N := C -> idxMap,
    domain(N, Xs),
    subset(N, L),
    domain(M, Xs),
    idxMapConstraint(D, T, M).
idxMapConstraint(fun(D, A), T, N)  :-
    Xs := A -> rnkSet, Ys := A -> idxSet, Js := A -> argAln -> trgDms,
    B  := A -> nodMap, alnMap(B), T := B -> parTmp, M := B -> idxMap,
    domain(M, Ys),
    map(Xs, Js, L),
    subset(L, M),
    subset(M, N),
    idxMapConstraint(D, T, M).
idxMapConstraint(arg(D, A), T, N)  :-
    Xs := A -> rnkSet, Ys := A -> idxSet, Js := A -> argAln -> trgDms,
    B  := A -> nodMap, alnMap(B), T := B -> parTmp, M := B -> idxMap,
    domain(M, Ys),
    map(Xs, Js, L),
    subset(L, M),
    subset(N, M),
    idxMapConstraint(D, T, M).
idxMapConstraint(var(A), T, N)     :-
    Xs := A -> idxSet, B  := A -> nodMap,
    alnMap(B), T := B -> parTmp, M := B -> idxMap,
    domain(M, Xs),
    subset(M, N).
idxMapConstraint(idx(_), _, _).

    
idxMapConstraintDaughters([], _, _).
idxMapConstraintDaughters([D | Ds], T, M) :-
    idxMapConstraint(D, T, M),
    idxMapConstraintDaughters(Ds, T, M).


% Phase II
% --------
%      Index mapping proper.


% Phase IIIpre: Preamble.  Insert mapping ``quality'' in `nod' and `arg' nodes.
% Currently just the maximal template rank.  It's known that the associated
% strategy for IIIc doesn't work in general.  This phase may go away eventually.

idxMapQual(D) :-
    idxMapMaxDim(D, Max),
    idxMapQualNode(Max, D).


idxMapMaxDim(nod(Ds, _), Max) :- idxMapMaxDimDaughters(Ds, Max).
idxMapMaxDim(arc(D, _), Max)  :- idxMapMaxDim(D, Max).
idxMapMaxDim(fun(D, _), Max)  :- idxMapMaxDim(D, Max).
idxMapMaxDim(arg(D, _), Max)  :- idxMapMaxDim(D, Max).
idxMapMaxDim(var(A), Max)     :- V := A -> varNam, templateDim(V, Max).
idxMapMaxDim(idx(_), 0).

idxMapMaxDimDaughters([], 0).
idxMapMaxDimDaughters([D | Ds], Max) :-
    idxMapMaxDim(D, Max1),
    idxMapMaxDimDaughters(Ds, Max2),
    Max is max(Max1, Max2).


templateDim(V, Dim) :-
    alignment(V, T, _, _),
    variable(T, _, Is, _),
    size(Is, Dim).


idxMapQualNode(Max, nod(Ds, A)) :-
    Max := A -> mapQal,
    idxMapQualNodeDaughters(Max, Ds).
idxMapQualNode(Max, arc(D, _))  :- idxMapQualNode(Max, D).
idxMapQualNode(Max, fun(D, A))  :- Max := A -> mapQal, idxMapQualNode(Max, D).
idxMapQualNode(Max, arg(D, A))  :- Max := A -> mapQal, idxMapQualNode(Max, D).
idxMapQualNode(_, var(_)).
idxMapQualNode(_, idx(_)).

idxMapQualNodeDaughters(_, []).
idxMapQualNodeDaughters(Max, [D | Ds]) :-
    idxMapQualNode(Max, D),
    idxMapQualNodeDaughters(Max, Ds).


% Phase IIIa: Apply `var' heuristic.

idxMapVar(nod(Ds, _)) :- idxMapVarDaughters(Ds).
idxMapVar(arc(D, _))  :- idxMapVar(D).
idxMapVar(fun(D, _))  :- idxMapVar(D).
idxMapVar(arg(D, _))  :- idxMapVar(D).
idxMapVar(var(A))     :-
    V := A -> varNam, Subs := A -> subLis, B := A -> nodMap,
    varSynthMap(V, Subs, B).
idxMapVar(idx(_)).

idxMapVarDaughters([]).
idxMapVarDaughters([D | Ds]) :-
    idxMapVar(D),
    idxMapVarDaughters(Ds).


varSynthMap(V, Subs, A) :-
    T := A -> parTmp, M := A -> idxMap,
    alignment(V, T, Is, _),
    mapLinSubscripts(Subs, Is, M).

mapLinSubscripts([], [], _).
mapLinSubscripts([Sub | Subs], [I | Is], M) :-
    mapLinSubscript(Sub, I, M),
    mapLinSubscripts(Subs, Is, M).

mapLinSubscript(lin(X), I, M) :- linTarg(I, J), member(X -> J, M).
mapLinSubscript(_, _, _).

linTarg(*, *) :- !.
linTarg(I, lin(I)).

alignment(V, U, Ks, S) :-
    variable(V, T, Is, P),
    ground(T), !,
    alignment(T, U, Js, Q),
    composeSeqSeq(Is, Js, Ks),
    composeRelSeq(P,  Js, R),
    append(R, Q, S).
alignment(V, V, Is, _) :- variable(V, _, Is, _), enumFrom(1, Is).

enumFrom(_, []).
enumFrom(N, [N | Is]) :- N1 is N + 1, enumFrom(N1, Is).


% Phase IIIb: Apply `arc' heuristic.

idxMapArc(nod(Ds, _)) :- idxMapArcDaughters(Ds).
idxMapArc(arc(D, A))  :-
    B := A -> srcMap, C := A -> dstMap,
    idxMapArc(D),
    arcSynthMap(B, C).
idxMapArc(fun(D, _))  :- idxMapArc(D).
idxMapArc(arg(D, _))  :- idxMapArc(D).
idxMapArc(var(_)).
idxMapArc(idx(_)).

idxMapArcDaughters([]).
idxMapArcDaughters([D | Ds]) :-
    idxMapArc(D),
    idxMapArcDaughters(Ds).


arcSynthMap(A, B) :-
    T := A -> parTmp, M := A -> idxMap, T := B -> parTmp, M := B -> idxMap.
arcSynthMap(_, _).


% Phase IIIc: Instantiate remaining mappings.

% Note that with this strategy, it's known that some expressions
% can't be mapped at all!  This needs fixing eventually.

idxMapAll(nod(Ds, A)) :-
    Qual := A -> mapQal, B := A -> nodMap,
    nodSynthMap(Qual, B),
    idxMapAllDaughters(Ds).
idxMapAll(arc(D, _))  :- idxMapAll(D).
idxMapAll(fun(D, A))  :-
    Qual := A -> mapQal, B := A -> nodMap,
    nodSynthMap(Qual, B),
    idxMapAll(D).
idxMapAll(arg(D, A))  :-
    Qual := A -> mapQal, B := A -> nodMap,
    nodSynthMap(Qual, B),
    idxMapAll(D).
idxMapAll(var(_)).
idxMapAll(idx(_)).

idxMapAllDaughters([]).
idxMapAllDaughters([D | Ds]) :-
    idxMapAll(D),
    idxMapAllDaughters(Ds).


nodSynthMap(Qual, A) :-
    T := A -> parTmp, M := A -> idxMap,
    ground(T),
    alignment(T, T, Is, _),
    mapAll(Qual, Is, M).

mapAll(Max, Is, M) :-
    size(Is, TargDim),
    countUncollapsed(M, NumUncollapsed),
    NumFailures is max(0, NumUncollapsed - TargDim),
    (NumFailures =:= 0, ! | TargDim =:= Max),
    mapIndices(Is, NumFailures, M).


mapIndices(_, 0, []).
mapIndices(Is, N, [_ -> I | M]) :-
    mapIndex(Is, N, Is1, N1, I),
    mapIndices(Is1, N1, M).

mapIndex(Is, N, Is,  N,  I)      :- ground(I), I = *, !.
mapIndex(Is, N, Is1, N,  I)      :- ground(I), I = lin(J), !,
                                    removeMember(J, Is, Is1).
mapIndex(Is, N, Is1, N,  non(J)) :- removeMember(J, Is, Is1).
mapIndex(Is, N, Is,  N1, ?)      :- N > 0, N1 is N - 1.


countUncollapsed([], 0).
countUncollapsed([_ -> I | M], N)  :-
    ground(I), I = *, !,
    countUncollapsed(M, N).
countUncollapsed([_ -> _ | M], N1) :- countUncollapsed(M, N), N1 is N + 1.


%------

%      Reverse preprocessing transformations on the decorated syntax tree,
% ready for printing.

postprocess(arc(nod([arc(var(A), _) | Ds], B), _), var(V, Es, map(T, M))) :-
    V := A -> varNam, T := B -> nodMap -> parTmp, M := B -> nodMap -> idxMap,
    postprocessDaughters(Ds, Es).
postprocess(arc(fun(nod(Ds, _), A), _), fun(F, Xs, Es, map(T, M))) :-
    F := A -> funNam, Xs := A -> rnkSet,
    T := A -> nodMap -> parTmp, M := A -> nodMap -> idxMap,
    postprocessDaughters(Ds, Es).
postprocess(arg(D, A), arg(Xs, E, map(T, M))) :-
    Xs := A -> rnkSet, T := A -> nodMap -> parTmp, M := A -> nodMap -> idxMap,
    postprocess(D, E).
postprocess(idx(X), idx(X)).

postprocessDaughters([], []).
postprocessDaughters([D | Ds], [E | Es]) :-
    postprocess(D, E),
    postprocessDaughters(Ds, Es).

%-----------------------------------------------------------------

% Embedding
% ---------

% Phase I
% -------
%      Decorate tree with ``embedding'' records.

embedDecorate(nod(Ds, A)) :-
    B := A -> nodMap,
    invertIdxMap(B),
    embedDecorateDaughters(Ds).
embedDecorate(arc(D, A)) :-
    B := A -> srcMap, C := A -> dstMap,
    invertIdxMap(B),
    invertIdxMap(C),
    embedDecorate(D).
embedDecorate(fun(D, A)) :-
    B := A -> nodMap,
    invertIdxMap(B),
    embedDecorate(D).
embedDecorate(arg(D, A)) :-
    B := A -> nodMap,
    invertIdxMap(B),
    embedDecorate(D).
embedDecorate(var(A)) :-
    B := A -> nodMap,
    invertIdxMap(B).
embedDecorate(idx(_)).
 
embedDecorateDaughters([]).
embedDecorateDaughters([D | Ds]) :-
    embedDecorate(D),
    embedDecorateDaughters(Ds).


invertIdxMap(A) :-
    T := A -> parTmp, M := A -> idxMap, P := A -> embSeq,
    variable(T, _, P, _),
    invert(M, P).

invert([], _, _).
invert([X -> I | M], P) :-
    invertMapping(X, I, P),
    invert(M, P).

invertMapping(_, *, _, _) :- !.
invertMapping(_, ?, _, _) :- !.
invertMapping(X, lin(I), P) :- isNth(I, P, lin(X)),
invertMapping(X, non(I), P) :- isNth(I, P, non(X)),


% Phase II
% --------
%      Impose horizontal constraints on embeddings.  Post-order.

embedConstraint(nod(Ds, A), Q) :-
    P := A -> nodMap -> embSeq,
    embedConstraintDaughters(Ds, P),
    nodEmbedConstraint(Q, P).
embedConstraint(arc(D, A), R) :-
    P := A -> srcMap -> embSeq, Q := A -> dstMap -> embSeq,
    embedConstraint(D, P),
    nodEmbedConstraint(R, Q).
embedConstraint(fun(D, A), Q) :-
    ArgAlign := A -> argAln, P := A -> nodMap -> embSeq,
    embedConstraint(D, P),
    argEmbedConstraint(ArgAlign, 1, Q, P).
embedConstraint(arg(D, A), Q) :-
    ArgAlign := A -> argAln, P := A -> nodMap -> embSeq,
    embedConstraint(D, P),
    argEmbedConstraint(ArgAlign, 1, Q, P).
embedConstraint(var(A), Q) :-
    P := A -> nodMap -> embSeq,
    nodEmbedConstraint(Q, P).
embedConstraint(idx(_), _).
 
embedConstraintDaughters([], _).
embedConstraintDaughters([D | Ds], Q) :-
    embedConstraint(D, Q),
    embedConstraintDaughters(Ds, Q).


nodEmbedConstraint([], []).
nodEmbedConstraint([G | P], [H | Q]) :-
    embedBasicConstraint(G, H),
    nodEmbedConstraint(P, Q).

argEmbedConstraint(_, _, [], []).
argEmbedConstraint(ArgAlign, I, [G | P], [H | Q]) :-
    embedArgConstraint(ArgAlign, I, G, H),
    I1 is I + 1, argEmbedConstraint(ArgAlign, I1, P, Q).

% `ground' is used as a test for whether an index is mapped to a
% particular dimension.  This depends on the traversal being post-order
% (otherwise parent might already be instantiated to an embedded value).

% ***** This may need rethinking---it seems a bit obscure *****
% I think it's only an `arc' node where you might have to introduce
% replication.

embedBasicConstraint(_, Nod) :- ground(Nod), !.
embedBasicConstraint(Par, *) :- ground(Par), !.
embedBasicConstraint(Par, Par).

embedArgConstraint(A, I, Nod, Nod) :- P := A -> embMps, member(Nod -> I, P), !.
embedArgConstraint(A, I, *, *) :- P := A -> embMps, member(* -> I, P), !.
embedArgConstraint(A, I, Nod, Nod) :- P := A -> embMps, member(Nod -> I, P), !.
embedArgConstraint(_, _, Par, Nod) :- embedBasicConstraint(Par, Nod).


% Phase III
% ---------
%      Embedding proper.

% Phase IIIa: Apply `var' heuristic.

embedVar(nod(Ds, _)) :- embedVarDaughters(Ds).
embedVar(arc(D, _))  :- embedVar(D).
embedVar(fun(D, _))  :- embedVar(D).
embedVar(arg(D, _))  :- embedVar(D).
embedVar(var(A))     :-
    V := A -> varNam, Subs := A -> subLis, B := A -> nodMap,
    varEmbed(V, Subs, B).
embedVar(idx(_)).

embedVarDaughters([]).
embedVarDaughters([D | Ds]) :-
    embedVar(D),
    embedVarDaughters(Ds).


varEmbed(V, Subs, A) :-
    T := A -> parTmp, P := A -> embSeq,
    alignment(V, T, Is, E),
    embedThroughAlignment(1, P, E),
    embedScalarSubscripts(Subs, Is, P).

embedThroughAlignment(_, [], _).
embedThroughAlignment(I, [X | P], E) :-
    (member(X -> I, E), ! ; success),
    I1 is I + 1, embedThroughAlignment(I1, P, E).

embedScalarSubscripts([], [], _).
embedScalarSubscripts([Sub | Subs], [I | Is], P) :-
    isNth(I, P, X),
    embedScalarSubscript(Sub, X),
    embedScalarSubscripts(Subs, Is, P).

embedScalarSubscript(_, X)     :- ground(X), !.   % Need this clause?
embedScalarSubscript(exp, exp) :- !.
embedScalarSubscript(_, _).

% Phase IIIb: Apply `arc' heuristic.

embedArc(nod(Ds, _)) :- embedArcDaughters(Ds).
embedArc(arc(D, A))  :-
    B := A -> srcMap, C := A -> dstMap,
    embedArc(D),
    arcEmbed(B, C).
embedArc(fun(D, _))  :- embedArc(D).
embedArc(arg(D, _))  :- embedArc(D).
embedArc(var(_)).
embedArc(idx(_)).

embedArcDaughters([]).
embedArcDaughters([D | Ds]) :- embedArc(D), embedArcDaughters(Ds).

arcEmbed(B, C) :-
    % Check index maps are common
    T := B -> parTmp, T := C -> parTmp, M := B -> idxMap, M := C -> idxMap,
    % Attempt unification of embeddings, dimension by dimension.
    P := B -> embSeq, Q := C -> embSeq,
    touchLists(P, Q).
arcEmbed(_, _).

touchLists([], []).
touchLists([X | L], [Y | M]) :- touch(X, Y), touchLists(L, M).

touch(X, X) :- var(X).
touch(X, X) :- ground(X), (X = exp ; X = *).
touch(_, _).


% Phase IIIc: Instantiate remaining embeddings.

embedAll(nod(Ds, A)) :-
    P := A -> nodMap -> embSeq,
    nodEmbed(P),
    embedAllDaughters(Ds).
embedAll(arc(D, _))  :- embedAll(D).
embedAll(fun(D, A))  :-
    P := A -> nodMap -> embSeq,
    nodEmbed(P),
    embedAll(D).
embedAll(arg(D, A))  :-
    P := A -> nodMap -> embSeq,
    nodEmbed(P),
    embedAll(D).
embedAll(var(_)).
embedAll(idx(_)).

embedAllDaughters([]).
embedAllDaughters([D | Ds]) :-
    embedAll(D),
    embedAllDaughters(Ds).

nodEmbed([]).
nodEmbed([* | P]) :- !, nodEmbed(P).
nodEmbed([_ | P]) :- nodEmbed(P).

%------

embedPostprocess(arc(nod([arc(var(A), _) | Ds], B), C),
		 var(V, Es, Xs, T, P, U, Q)) :-
    V  := A -> varNam, Xs := B -> idxSet,
    T  := C -> srcMap -> parTmp, P := C -> srcMap -> embSeq,
    U  := C -> dstMap -> parTmp, Q := C -> dstMap -> embSeq,
    embedPostprocessDaughters(Ds, Es).
embedPostprocess(arc(fun(nod(Ds, _), A), B),
                 fun(F, Xs, Es, Ys, T, P, U, Q)) :-
    F  := A -> funNam, Xs := A -> rnkSet, Ys := A -> idxSet,
    T  := B -> srcMap -> parTmp, P := B -> srcMap -> embSeq,
    U  := B -> dstMap -> parTmp, Q := B -> dstMap -> embSeq,
    embedPostprocessDaughters(Ds, Es).
embedPostprocess(arg(D, A), arg(Xs, E)) :-
    Xs := A -> rnkSet,
    embedPostprocess(D, E).
embedPostprocess(idx(X), idx(X)).

embedPostprocessDaughters([], []).
embedPostprocessDaughters([D | Ds], [E | Es]) :-
    embedPostprocess(D, E),
    embedPostprocessDaughters(Ds, Es).

%-----------------------------------------------------------------

% Miscellaneous ``set'' operations.

union([], X, X).
union([X | R], Y, Z) :- member(X, Y), !, union(R, Y, Z). 
union([X | R], Y, [X | Z]) :- union(R, Y, Z).

intersection(X, Y, Z) :- subtract(X, Y, W), subtract(X, W, Z).

subtract(M, [], M).
subtract(M, [X | I], N) :- remove(X, M, P), subtract(P, I, N).

member(X, [X | _]).
member(X, [_ | Y]) :- member(X, Y).

removeMember(X, [X | L], L).
removeMember(X, [Y | L], [Y | M]) :- removeMember(X, L, M).

notMember(_, []).
notMember(X, [X | _]) :- !, fail.
notMember(X, [_ | L]) :- notMember(X, L).

remove(_, [], []).
remove(X, [X | L], L)       :- !.
remove(X, [Y | L], [Y | M]) :- remove(X, L, M).

subset([], _).
subset([X | M], N) :- member(X, N), !, subset(M, N).

size([], 0).
size([_ | R], N) :- ground(N), !, N > 0, N1 is N - 1, size(R, N1).
size([_ | R], N) :- size(R, N1), N is N1 + 1.

map([], [], []).
map([X | Xs], [Y | Ys], [X -> Y | M]) :- map(Xs, Ys, M).

domain([], []).
domain([X -> _ | M], [X | Xs]) :- domain(M, Xs).

%-----------------------------------------------------------------

% Run the whole mapping procedure, reading the program from a file.

run(Tree, Alignments, Q) :-
    [Alignments],
    !,
    go(Tree, Q).
run(_, Alignments, _) :- printString("Failed to load file "), write(Alignments).

go(Tree, R) :-
%go(Tree, R1) :-
%go(Tree, PP) :-
%go(Tree, Q1) :-
%go(Tree, P1) :-
%go(Tree, Q) :-
%go(Tree, P2) :-
    see(Tree),
    getNode(P),
    !,
    seen,
    nl,
    idxSet(P, PP, _),
    preprocess(PP, R),
    idxMapConstraint(R, _, _),
    idxMapQual(R),
    idxMapVar(R),
    idxMapArc(R),
    idxMapAll(R),
    embedDecorate(R),
    embedConstraint(R, _),
    embedVar(R),
    embedArc(R),
    embedAll(R),

%     nl,
%     printNodArc(0, P2).
% 
%     postprocess(P2, Q),
%     nl,
%     printIdxMap(0, Q).

    embedPostprocess(R, R1),
    nl,
    printEmbed(0, R1).
go(Tree, _) :- printString("Failed to parse file "), write(Tree), seen.

