
?- op(700, xfx, ->).

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

% Dimensional Mapping
% -------------------

% Glossary of symbols...
%
% V    = variable
% F    = function
% X    = index
% T    = template
% I    = template dimension
% J    = variable dimension
%
% D, E           = (daughter) node---complicated syntax!
%
% G, H           = collapsed index list
% K, L, M, N     = index to template dimension mappings---[] | [X -> I | M]
% A, B           = full index map---map(T, G, M)
% P              = variable dim to template dim mapping---[] | [J -> I | P]
% LocStatus      = status of mapping at local node---inher | synth(G)
% ParStatus      = contribution of local node to status of parent map---ditto.
%
% Q    = ``quality'' of pass.  Currently integer.  The larger the value,
%        the weaker the heuristics are being applied in this pass.
 
% Phase I
% -------
%    Decorate tree with index maps.  Instantiate map domains at each node.
% Impose horizontal constraints on target templates and index mappings.
% This is a post-order traversal.

idxMapDomain(var(V, Ds), var(V, Es, map(_, _, M), _), _, N) :-
    idxMapDomainDaughters(Ds, Es, _, M),
    domain(M, Xs),
    domain(N, Xs).
idxMapDomain(fun(F, Xs, Ds),
             fun(F, Xs, Es, map(T, G, L), map(T, G, N), _), _, K) :-
    idxMapDomainDaughters(Ds, Es, T, L),
    domain(M, Xs),
    union(L, M, N),
    domain(N, Ys),
    domain(K, Ys).
idxMapDomain(arr(Xs, D), arr(Xs, E, map(T, _, N), _), T, K) :-
    idxMapDomain(D, E, _, L),
    domain(M, Xs),
    union(L, M, N),
    subtract(L, M, K).
idxMapDomain(idx(X), idx(X), _, M) :-
    domain(M, [X]).
    
idxMapDomainDaughters([], [], _, []).
idxMapDomainDaughters([D | Ds], [E | Es], T, N) :-
    idxMapDomain(D, E, T, L),
    idxMapDomainDaughters(Ds, Es, T, M),
    union(L, M, N).

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

% Phase II
% --------
%      Synthesis Phase.  This post-order, except at a `var' node with
% a local reference mapping (which acts like a leaf, so far as the
% synthesis procedure is concerned).

idxMapSynthesis(Q, var(V, Ds, A, Propagation), Output, B) :-
    localMap(Q, V, Ds, A, Propagation, Output, B),
    idxMapSynthesisDaughters(Q, Ds, _, A).
idxMapSynthesis(Q, var(_, Ds, A, Propagation), Output, B) :-
    idxMapSynthesisDaughters(Q, Ds, Input, A),
    synthMap(Q, Input, A, Propagation, Output, B).
idxMapSynthesis(Q, fun(_, _, Ds, A, B, Propagation), Output, C) :-
    idxMapSynthesisDaughters(Q, Ds, Input, A),
    synthMap(Q, Input, B, Propagation, Output, C).
idxMapSynthesis(Q, arr(Xs, D, A, Propagation), Output, B) :-
    idxMapSynthesis(Q, D, Input, A),
    arrSynthMap(Q, Xs, Input, A, Propagation, Output, B).
idxMapSynthesis(_, idx(_), undef, _).

idxMapSynthesisDaughters(_, [], undef, _).
idxMapSynthesisDaughters(Q, [D | Ds], Result, A) :-
    idxMapSynthesis(Q, D, Result1, A),
    idxMapSynthesisDaughters(Q, Ds, Result2, A),
    resultCombine(Result1, Result2, Result).

resultCombine(synth(G1), synth(G2), synth(G)) :- union(G1, G2, G).
resultCombine(synth(G) , undef    , synth(G)).
resultCombine(undef    , synth(G) , synth(G)).
resultCombine(undef    , undef    , undef   ).

% `localMap'
%
%      Local reference map at `var' node.

localMap(Q, V, Ds, map(T, G, M), prop(local, PropDir), Result, B) :-
    variable(V, Js, T, P),
    mapIdxSubscripts(Ds, Js, P, G, M),
    template(T, Is),
    mapAll(Q, Is, G, M),
    parentMap(map(T, G, M), PropDir, Result, B).

mapIdxSubscripts([], [], _, [], _).
mapIdxSubscripts([D | Ds], [J | Js], P, G, M) :-
    mapIdxSubscript(D, J, P, G1, M),
    mapIdxSubscripts(Ds, Js, P, G2, M),
    union(G1, G2, G).

mapIdxSubscript(idx(X), J, P, G, M) :-
    compose(X, J, P, G, M).
mapIdxSubscript(_, _, _, [], _).

compose(X, J, P, [X], M) :-
    member(J -> *, P), !,
    member(X -> *, M).
compose(X, J, P, [], M) :-
    member(J -> I, P),
    member(X -> I, M).

% `synthMap'
%
%      Attempt to synthesise map at `var' or `fun' node.  Otherwise inherit.

synthMap(Q, synth(G), map(T, G, M), prop(nonloc, PropDir),
            Result, B) :-
    template(T, Is),
    mapAll(Q, Is, G, M),
    parentMap(map(T, G, M), PropDir, Result, B).
synthMap(_, undef, _, prop(nonloc, in), undef, _).


% `arrSynthMap'
%
%      Attempt to synthesise map at `arr' node.  Otherwise inherit.

arrSynthMap(Q, Xs, synth(G), map(T, G, M), prop(nonloc, out),
           synth(H), map(_, H, N)) :-
    union(M, N, L),
    template(T, Is),
    mapAll(Q, Is, G, L),
    subtract(G, Xs, H).
arrSynthMap(_, _, undef, _, prop(nonloc, in), undef, _).

% Misc utilities...

parentMap(map(T, G, M), out, synth(G), map(T, G, N)) :- % Propagate mapping up.
    subset(M, N).
parentMap(_, undef, undef, _).                          % par/node un-unified.

mapAll(_, _, _, []).
mapAll(Q, Is, G, [_ -> I | M]) :-     % Align to template dimension
    removeMember(I, Is, Is1),
    mapAll(Q, Is1, G, M).
mapAll(Q, Is, G, [X -> * | M]) :-     % Collapsed index
    member(X, G),
    mapAll(Q, Is, G, M).
mapAll(Q, Is, G, [_ -> ? | M]) :-     % Fail to map Q or fewer indices
    Q > 0,
    Q1 is Q - 1, mapAll(Q1, Is, G, M).


% Phase III
% ---------
%      Inheritance phase.  This is a pre-order traversal.

idxMapInheritance(Q, var(_, Ds, A, Propagation), B) :-
    inheritMap(B, A, Propagation),
    idxMapInheritanceDaughters(Q, Ds, A).
idxMapInheritance(Q, fun(_, _, Ds, A, B, Propagation), C)   :-
    inheritMap(C, B, Propagation),
    idxMapInheritanceDaughters(Q, Ds, A).
idxMapInheritance(Q, arr(_, D, A, Propagation), B) :-
    arrInheritMap(Q, B, A, Propagation),
    idxMapInheritance(Q, D, A).
idxMapInheritance(_, idx(_), _).

idxMapInheritanceDaughters(_, [], _).
idxMapInheritanceDaughters(Q, [D | Ds], M) :-
    idxMapInheritance(Q, D, M),
    idxMapInheritanceDaughters(Q, Ds, M).


% Inherit map at `var' or `fun' node.

inheritMap(map(T, G, M), map(T, H, N), prop(_, in)) :-
    subset(N, M),
    domain(N, Xs),
    intersection(Xs, G, H).
inheritMap(_, _, prop(_, out)).
inheritMap(_, _, prop(_, undef)).


% Attempt to inherit map at `arr' node.

arrInheritMap(Q, map(T, G, M), map(T, H, N), prop(_, in)) :-
    union(N, M, L),
    template(T, Is),
    mapAll(Q, Is, G, L),
    domain(N, Xs),
    intersection(Xs, G, H).
arrInheritMap(_, _, _, prop(_, out)).
arrInheritMap(_, _, _, prop(_, undef)).


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

% 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).

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

% Allow successively more ``undefined'' (presumably collapsed)
% index-mappings, until success.

alignMap(P) :- alignMapping(0, P).

alignMapping(Q, P) :-
    idxMapSynthesis(Q, P, synth(_), _),
    idxMapInheritance(Q, P, _).
alignMapping(Q, P) :-
    Q1 is Q + 1,
    alignMapping(Q1, P).

% 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, Q) :-
    see(Tree),
    getNode(P),
    !,
    seen,
    nl,
    idxMapDomain(P, Q, _, _),
    alignMap(Q),
    nl,
    printAssocs(0, Q).
go(Tree, _) :- printString("Failed to parse file "), write(Tree), seen.

