/********  LINEAR  SECOND-ORDER  UNIFICATION  **************

 The sintax of a well-typed normal term is defined by the following grammar:

Term ::=  constant                              for first-order constants
       |  par ( number )                        for bound variables
       |  number                                for first-order free variables
       |  app ( number , [ List ] )             for second-order free variables
       |  app ( constant , [ List ] )           for second-order constants

List ::=  Term
       |  List , Term

Therefore, terms are supposed to be normalized and well-typed.
They can not contain lambda-bindings (they are implicitly supposed
to be outermost). Try the following example.
*/


example :- unify(app(0,[app(apply,[app(lambda,[1]),2])]),
                 app(union,[app(3,[4]),app(3,[5])])).

example2 :- unify(app(f,[app(0,[app(f,[app(1,[a]),4])]), app(2,[app(f,[5,app(3,[a])])])]),
                             app(f,[app(f,[app(1,[app(0,[a])]), app(3,[app(2,[a])])]),
                                       app(f,[app(1,[app(0,[a])]), app(3,[app(2,[a])])])])).

example3 :- unify(app(g,[app(0,[app(1,[a])]),app(0,[app(1,[b])]),app(0,[a]),app(0,[b]),app(1,[a]),app(1,[b])]),
                  app(g,[app(r,[app(r,[f,a]),b]),app(r,[app(r,[f,b]),b]),app(3,[a,b]),app(3,[b,b]),app(3,[2,a]),app(3,[2,b])])).

example4 :- unify(app(g,[app(0,[app(1,[a])]),app(0,[app(1,[c])]),app(0,[2])]),
                  app(g,[app(r,[app(r,[f,a]),b]),app(r,[app(r,[f,c]),b]),app(1,[b])])).

example5 :- unify(app(f,[app(1,[app(0,[b])]),app(0,[a])]), app(0,[app(f,[b,a])])).

/*------------------------------------------------------------------
unify(T,U)
--------------------------------------------------------------------
This is the main predicate of the program. Given two terms T and U
finds the set of unifiers and writes them.
------------------------------------------------------------------*/

unify(X,Y) :-
    nl,write('PROBLEM: '),writeterm(X),write(' = '),writeterm(Y),nl,nl,
    maxvar([X,Y],N), M is N + 1,
    unif(X,Y,S,M,_,0),
    reduce(S,S1),
    nl,writesubst(S1,M),nl,
    fail.

unify(_,_).


/*------------------------------------------------------------------
writesubst(S,N)
writeterm(T)
--------------------------------------------------------------------
Auxiliar predicates to print substitutions and terms.
------------------------------------------------------------------*/

writesubst([],_).

writesubst([X/Y|L],N) :-
    (
         X < N, !, writebody(X),write(' -> '),writeterm(Y),nl
    ;
         true
    ), 
    writesubst(L,N).

writeterm(X):-
    writelambdas(X),
    writebody(X),
    !.

writebody(X) :-
    number(X),!,
    (
        position(X,['A','B','C','D','E','F','G','H','I','J','K','L','M','N','O','P','Q','R','S','T','U','V','W','X','Y','Z','A2','B2','C2','D2','E2','F2','G2','H2','I2','J2'],Y), !
    ;
        Y = X
    ),
    write(Y).

writebody(X) :-
    atomic(X),!,
    write(X).

writebody(app(X,P)) :-
    writebody(X),write('('),writeparam(P),write(')').

writebody(par(X)) :-
    position(X,[x,y,z,t,u,v,w],Y), write(Y).

writeparam([X]) :-
    writebody(X),!.

writeparam([X|Y]) :-
    writebody(X),write(', '),writeparam(Y).

writelambdas(X):-
    maxpar(X,N),
    writenlambdas(N,[x,y,z,t,u,v,w]).

writenlambdas(-1,_) :- !.

writenlambdas(N,[X|Y]) :-
    write('\\'),write(X),write('. '), M is N - 1, writenlambdas(M,Y).


/*------------------------------------------------------------------
maxpar(T,N)
--------------------------------------------------------------------
Given a term T returns the number of the maximum bound variable
(or -1 if there is none).
------------------------------------------------------------------*/

maxpar(par(N),N) :- !.

maxpar(app(_,P),N) :-
    maxpar(P,N), !.

maxpar([X|Y],N) :-
    maxpar(X,M1),
    maxpar(Y,M2),
    (M1 > M2, !, N = M1 ; N = M2), !.

maxpar(_,-1).


/*------------------------------------------------------------------
maxvar(T,N)
--------------------------------------------------------------------
Given a term T returns the number of the maximum free variable
(or -1 if there is none).
------------------------------------------------------------------*/

maxvar(N,N) :-
    number(N), !.

maxvar(app(P,Q),N) :-
    maxvar(P,M1),
    maxvar(Q,M2),
    (M1 > M2, !, N = M1 ; N = M2), !.

maxvar([X|Y],N) :-
    maxvar(X,M1),
    maxvar(Y,M2),
    (M1 > M2, !, N = M1 ; N = M2), !.

maxvar(_,-1).

/*------------------------------------------------------------------
unif(L1, L2, S, Vi, Vo, Lev)
--------------------------------------------------------------------
Given two lists of expressions L1 and L2 finds a substitution S which
unify them one-to-one. Vi is the number of the smallest fresh variable
before instantiate them and Vo is the number after the instantiation.
Lev is the indentation level.
------------------------------------------------------------------*/

unif(_ , _, _, _, _, N) :-
    N > 20,
    !,
    write('ABORT: too much work to do'), nl, fail.

unif([], [], [], Var, Var,_) :- !.

unif([X|L],[Y|M],S, VarIn, VarOut, Lev) :-
    !,
    unif(X, Y, S1, VarIn, V, Lev),
    subst(L, S1, L1),
    subst(M, S1, M1),
    unif(L1, M1, S2, V, VarOut, Lev),
    append(S1, S2, S).

/*------------------------------------------------------------------
unif(E1, E2, S, Vi, Vo, Lev)
--------------------------------------------------------------------
Like the previous predicate for two given terms.
------------------------------------------------------------------*/

/****** Equal term ******/

unif(X, X, [], V, V, _) :-
    !.

/****** Variable term ******/

nonumber(X) :- 
    number(X),!,fail.
nonumber(_).

unif(X, Y, [X/Y], V, V, Lev) :-
    number(X),
    (nonumber(Y);number(Y),Y < X),
    notfree(X,Y),
    indent(Lev),write('Instantiate:         '),writebody(X),write(' -> '),writeterm(Y),nl.

unif(Y, X, [X/Y], V, V, Lev) :-
    number(X),
    (nonumber(Y);number(Y),Y < X),
    notfree(X,Y),
    indent(Lev), write('Instantiate:         '),writebody(X),write(' -> '),writeterm(Y),nl.

/****** Non-equal variables or constants ******/

unif(X, Y,[], V, V, _) :-
    atomic(X),
    atomic(Y),
    !,
    fail.

/****** Simplification ******/

unif(app(X,P), app(X,Q), S, Vi, Vo, Lev) :-
    !,
    indent(Lev),write('Try simplification:  '),writeterm(app(X,P)),write(' = '),writeterm(app(X,Q)),nl,
    Lev2 is Lev + 1,
    unif(P, Q, S, Vi, Vo, Lev2).
   
/****** Projection ******/

unif(app(X,[P]), Y, [X/par(0)|S], Vi, Vo, Lev) :-
    number(X),
    indent(Lev),write('Try projection:      '),writeterm(app(X,[P])),write(' = '),writeterm(Y),nl,
    Lev2 is Lev + 1,
    subst(P, X/par(0), P2),
    subst(Y, X/par(0), Y2),
    unif(P2, Y2, S, Vi, Vo, Lev2).

unif(Y, app(X,[P]), [X/par(0)|S], Vi, Vo, Lev) :-
    number(X),
    indent(Lev),write('Try projection:      '),writeterm(app(X,[P])),write(' = '),writeterm(Y),nl,
    Lev2 is Lev + 1,
    subst(P, X/par(0), P2),
    subst(Y, X/par(0), Y2),
    unif(P2, Y2, S, Vi, Vo, Lev2).

/****** Forget ******/

unif(app(X,P), Y, [X/app(Vi,L)|S], Vi, Vo, Lev) :-
    number(X),
    length(P,R),
    R > 1,
    forgetsome(R,L),
    indent(Lev),write('Try forget some:      '),writeterm(app(X,P)),write(' = '),writeterm(Y),nl,
    subst(app(X,P), X/app(Vi,L), NT),
    subst(Y, X/app(Vi,L), Y2),
    V2 is Vi + 1,
    unif(NT, Y2, S, V2, Vo, Lev).
     
unif(Y, app(X,P), [X/app(Vi,L)|S], Vi, Vo, Lev) :-
    number(X),
    length(P,R),
    R > 1,
    forgetsome(R,L),
    indent(Lev),write('Try forget some:      '),writeterm(app(X,P)),write(' = '),writeterm(Y),nl,
    subst(app(X,P), X/app(Vi,L), NT),
    subst(Y, X/app(Vi,L), Y2),
    V2 is Vi + 1,
    unif(Y2, NT, S, V2, Vo, Lev).
 
unif(app(X,[P]), Y, [X/Y], V, V, Lev) :-
    number(X),
    notfree(X,Y),
    indent(Lev),write('Try forget all:      '),writeterm(app(X,[P])),write(' = '),writeterm(Y),nl.

unif(Y, app(X,[P]), [X/Y], V, V, Lev) :-
    number(X),
    notfree(X,Y),
    indent(Lev),write('Try forget all:      '),writeterm(app(X,[P])),write(' = '),writeterm(Y),nl.

/****** Flex-Flex with distinct heads ******/

unif(app(X,P), app(Y,Q), [X/F, Y/G| S], Vi, Vo, Lev) :-
    number(X),
    number(Y),
    !,                                             /* Do not try imitation */
    index(P, LP),
    index(Q, LQ),
    distribute(LP, 2, [Pprim,Prest]),
    distribute(LQ, 2, [Qprim,Qrest]),
    length(Pprim, LPprim),
    length(Qprim, LQprim),
    distribute(Prest, LQprim, Psub),
    distribute(Qrest, LPprim, Qsub),
    V1 is Vi + 1,
    addvariablehead(Psub, Fpar1, V1, V2),
    addvariablehead(Qsub, Gpar1, V2, V3),
    append(Pprim, Fpar1, Fpar2),
    append(Gpar1, Qprim, Gpar2),
    F = app(Vi,Fpar2),
    G = app(Vi,Gpar2),
    subst(app(X,P), [X/F,Y/G], E1),
    subst(app(Y,Q), [X/F,Y/G], E2),
    indent(Lev),write('Try flex-flex:       '),writeterm(app(X,P)),write(' = '),writeterm(app(Y,Q)),nl,
    Lev2 is Lev + 1,
    unif(E1, E2, S, V3, Vo, Lev2).

/****** Imitation ******/
    
unif(app(X,P), app(Y,Q), [X/F| S], Vi, Vo, Lev) :-
    number(X),
    index(P, LP),
    length(Q, LQ),
    distribute(LP, LQ, Psub),
    addvariablehead(Psub,Fparam, Vi, V),
    F = app(Y,Fparam),
    subst(app(X,P), X/F, E1),
    subst(app(Y,Q), X/F, E2),
    indent(Lev),write('Try imitation:       '),writeterm(app(X,P)),write(' = '),writeterm(app(Y,Q)),nl,
    Lev2 is Lev + 1,
    unif(E1, E2, S, V, Vo, Lev2).

unif(app(Y,Q), app(X,P), [X/F| S], Vi, Vo, Lev) :-
    number(X),
    index(P, LP),
    length(Q, LQ),
    distribute(LP, LQ, Psub),
    addvariablehead(Psub,Fparam, Vi, V),
    F = app(Y,Fparam),
    subst(app(X,P), X/F, E1),
    subst(app(Y,Q), X/F, E2),
    indent(Lev),write('Try imitation:       '),writeterm(app(X,P)),write(' = '),writeterm(app(Y,Q)),nl,
    Lev2 is Lev + 1,
    unif(E1, E2, S, V, Vo, Lev2).


/*------------------------------------------------------------------
distribute(L, N, S)
--------------------------------------------------------------------
Given a list L and a number N, distribute the elements of L among N 
disjoint subsets returned in S. 
------------------------------------------------------------------*/

distribute([], 0, []) :- !.

distribute(_, 0, _) :- 
    !, 
    fail.

distribute([], N, [[]|S]) :-
    !,
    M is N - 1,
    distribute([], M, S).

distribute([N|L], M, S) :-
    distribute(L, M, S2),
    includein(N, S2, S).


/*------------------------------------------------------------------
includein(E, S1, S2)
--------------------------------------------------------------------
Given an element E and a list of sets S1, gives a new list of sets S2
where E has been included in one of the sets.
------------------------------------------------------------------*/
    
includein(N,[S],[[N|S]]) :- !.

includein(N,[S1|S2],[[N|S1]|S2]).

includein(N,[S1|S2],[S1|S3]) :-
    includein(N,S2,S3).


/*------------------------------------------------------------------
index(L1, L2)
--------------------------------------------------------------------
Given a list L1 returns a list L2 with the same length and the form
[par(0),par(1),par(2),...,par(N)].
------------------------------------------------------------------*/

index([],[]).

index([_|Y], [par(N)|M]) :-
    index(Y,M),
    length(M,N).

/*------------------------------------------------------------------
addvariablehead(L1, L2, Vi, Vo)
--------------------------------------------------------------------
Given a list of (maybe empty) parameters, adds a fresh free variable
in the head and (if the list is non-empty) builds an application term.
Vi is the number of the smallest fresh variable before executing
the predicate, and Vo is the number after it.
------------------------------------------------------------------*/

addvariablehead([],[],V,V).

addvariablehead([[]|S2], [F|P], F, F2) :-
    !,
    F1 is F + 1,
    addvariablehead(S2,P,F1,F2).

addvariablehead([S1|S2], [app(F,S1)|P], F, F2) :-
    F1 is F + 1,
    addvariablehead(S2,P,F1,F2).
    
   
/*------------------------------------------------------------------
subst(E1, S, E2)
--------------------------------------------------------------------
Given an expression E1 and a substitution S, instantiates the 
expression and returns E2.
------------------------------------------------------------------*/

/* For lists */

subst([],_,[]) :- !.

subst([X|L], S, [X2|L2]) :-
    !,
    subst(X, S, X2),
    subst(L, S, L2).

/* For composed substitutions */

subst(X, [], X) :- !.

subst(X, [S1|S2], Y) :-
    !,
    subst(X, S1, X2),
    subst(X2, S2, Y).
    
/* Atomic case */

subst(X, X/Y, Y) :- !.                /* First-order variables */

subst(X, _, X) :-                     /* Constants and distinct FO variables */
    atomic(X),
    !.

subst(app(Y,P), Y/Y2, X2):-           /* Second-order variables */
    !,
    subst(P, Y/Y2, P2),
    betareduce(Y2, P2, X2).
    
subst(app(X,P1), Y/Y2, app(X,P2)) :-  /* Distinct SO variables */
    subst(P1, Y/Y2, P2),
    !.

subst(par(X),_,par(X)) :- !.          /* Bound variables */

subst(_,_,_) :-                       /* Panic */
    !,
    write('Fail subst'), nl,
    fail.

/*------------------------------------------------------------------
betareduce(E, P, NE)
--------------------------------------------------------------------
Given an expression E with bound variables, and a list of parameters P
substitute each bound variable by the corresponding parameter and
returns NE.
------------------------------------------------------------------*/

betareduce([], _, []) :- !.             /* For lists of expressions */

betareduce([X|L], P, [X2|L2]) :-
    !,
    betareduce(X,P,X2),
    betareduce(L,P,L2).
    
betareduce(par(N), P, X) :-             /* Bound variables */
    !,
    position(N, P, X).

betareduce(X, _, X) :-                  /* Free variables and constants */
    atomic(X),
    !.

betareduce(app(X,L1), P, app(X,L2)) :-  /* Applications */
    betareduce(L1, P, L2),
    !.

betareduce(_,_,_) :-                    /* Panic */
    !,
    write('Fail beta-reduce'), nl,
    fail.

/*------------------------------------------------------------------
notfree(N,E)
--------------------------------------------------------------------
Given a free variable number N and an expression E, finds if N
occurs free in E.
------------------------------------------------------------------*/

notfree(N, N) :-
    number(N),
    !,
    fail.

notfree(_, M) :-
    atomic(M),
    !.

notfree(_, par(_)) :- !.
 
notfree(N, app(M,L)) :-
    !,
    notfree(N, M),
    notfree(N, L).

notfree(_, []) :- !.

notfree(N, [M|L]) :-
    !,
    notfree(N, M),
    notfree(N, L).

notfree(_,_) :-
    write('Fail notfree'),nl,
    fail.

/*------------------------------------------------------------------
position(N, L, E)
--------------------------------------------------------------------
Given a number N and a list L returns in E the Nth element of the list.
It fails if L has less than N elements.
------------------------------------------------------------------*/

position(0, [X|_], X) :- !.

position(N, [_|L], Y) :-
    M is N - 1,
    position(M,L,Y).

   
/*------------------------------------------------------------------
reduce(S1, S2)
--------------------------------------------------------------------
Given a substitution S1 normalizes it.
------------------------------------------------------------------*/

reduce([],[]).

reduce([X/Y|S], [X/Y2|S2]) :-
    reduce(S, S2),
    subst(Y, S2, Y2).

indent(0) :- !.
indent(N) :-
    M is N - 1,
    indent(M),
    write(' ').

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

forgetsome(N, L) :-
    forget(N, L),
    length(L, M),
    M > 0,
    M < N.

forget(0, []) :- !.
forget(N, L) :-
    M is N - 1,
    forget(M, L).
forget(N, [par(M)|L]) :-
    M is N - 1,
    forget(M, L).


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