/* Alpha and Beta conversion for lambda calculus
 *
 * Syntax:
 * - lam(Var, Expr). Eg. lam(X, foo(X)).
 * - app(LambdaExpr, Substitution). Eg. app(lam(X, foo(X)), 1) == foo(1).
 *
 * Example to clarify order of arguments:

?- betaconv(app(app(lam(X1,lam(X2, foo(X1,X2))),1),2),Res,[]).

X1 = _G183
X2 = _G184
Res = foo(1, 2) 

Yes

%*/

:- 
	nl,
	writeln('Run \'go\' to demonstrate all working sentences'),
	writeln('    (including quantification and conjunctive noun/verb phrases)'),
	writeln('Extra: ex12 (ditransitive verb)').

%Test all working sentences (sort of a "unit test").
go :- ex3, ex4, ex5, ex6, ex7, ex8, ex9, ex10, ex11.

%From assignment 1:
ex0 :-  ex([vincent, likes, mia]).
ex1 :-  ex([vincent, walks, and, vincent, likes, mia]).
ex2 :-  ex([vincent, walks, and, mia, walks]).

%From assignment 2:
ex3 :-  ex([some, woman, likes, vincent]).
ex4 :-  ex([vincent, likes, some, woman]).
ex5 :-  ex([some, woman, likes, every, foot, massage]).
ex6 :-  ex([mia, walks, and, likes, vincent]).
ex7 :-  ex([mia, and, vincent, walk]).
ex8 :-  ex([mia,likes, john, and, vincent]).
ex9 :-  ex([mia, talks, and, talks, and, talks, and, talks]).
ex10 :- ex([some, woman, and, mia, like, vincent, and, john, talks]).
ex11 :- ex([john, walks, and, mia, likes, john, and, vincent, likes, mia, and, vincent, likes, john, walker]).
%Ditransitive verbs, not yet working. Quantifier should end up outside of the give-predicate:
ex12 :- ex([vincent, gives, mia, a, foot, massage]).

ex(Sentence) :-
        write('Sentence: '), writeln(Sentence),
        s(Sem, Sentence, []), %!,
        %write('Parsed: '), writeln(Sem),	%this floods the terminal
        betaconv(Sem, Result, []),
        write('Reduced: '), writeln(Result), nl.

%Some syntatic sugar:
%Quantifiers
:- op(900, fx, @).
:- op(900, fx, 'E').
%Implication
:- op(800,xfx, ->).
%Conjunction
:- op(700,xfy, ^).
%Disjunction
:- op(600,xfy, v).

%Syntactic grammar
% 
% s --> np,vp.
% s --> s, con, s.
% np --> pn.
% np --> det, noun.
% np --> np con np.
% vp --> iv.
% vp --> tv, np.
% vp --> dtv, np.
% vp --> vp con vp.
% pn --> [mia].
% pn --> [vincent].
% pn --> [john].
% iv --> [walks].
% iv --> [talks].
% tv --> [likes].
% con --> [and].
% con --> [or].
% con --> [implies].
s(app(NP,app(app(DET, app(TV,N ))))) --> np(NP), tv(TV), det(DET),noun(N).
%semantic grammar (order matters, both that of the rules and of their conditions!)
s(app(NP, VP)) --> np(NP), vp(VP).
s(app(app(CON, S1), S2)) --> s1(S1), cons(CON), s(S2).
s1(app(NP, VP)) --> np(NP), vp(VP).


np(PN) --> pn(PN).
np(app(Det, Noun)) --> det(Det), noun(Noun).
np(app(app(CON, NP1), NP2)) --> np1(NP1), con(CON), np(NP2).

% np1 = np. Used to avoid left-recursion
np1(PN) --> pn(PN).
np1(app(Det, Noun)) --> det(Det), noun(Noun).

vp(IV) --> iv(IV).
vp(app(NP, TV)) --> tv(TV), np(NP).
vp(app(NP1, app(DTV, NP2))) --> dtv(DTV), np(NP1), np(NP2).
%this one works for "mia gives vincent mia":
%vp(app(NP1, app(NP2, DTV))) --> dtv(DTV), np1(NP1), np(NP2).

%hack for NP conjunction after a transitive verb:
%vp(app(app(DET,N),TV)) --> tv(TV),det(DET), noun(N).
vp(app(app(CON, app(NP1,TV )),app(NP2, TV)))  --> tv(TV),np1(NP1), con(CON), np(NP2).

vp(app(app(CON,VP1),VP2)) --> vp1(VP1), con(CON), vp(VP2).

% vp1 = vp. Used to avoid left-recursion
vp1(IV) --> iv(IV).
vp1(app(NP, TV)) --> tv(TV), np(NP).
vp1(app(NP1, app(DTV, NP2))) --> dtv(DTV), np(NP1), np(NP2).

%lexicon
noun(lam(X, footmassage(X))) --> [foot, massage].
noun(lam(X, woman(X))) --> [woman].
iv(lam(X, walk(X))) --> [walks];[walk].
iv(lam(X, talk(X))) --> [talks];[talk].
tv(lam(Y, lam(X, like(X,Y)))) --> [likes];[like].

dtv(lam(Z, lam(Y, lam(X, gives(X, Y, Z))))) --> [gives];[give].
pn(lam(X, app(X, vincent))) --> [vincent].
pn(lam(X, app(X, john))) --> [john].
pn(lam(X, app(X, johnnieWalker))) --> [john, walker].
pn(lam(X, app(X, mia))) --> [mia].

%Quantifiers:
det(lam(U, lam(V, @ (X, app(U, X) -> app(V, X))))) --> [every] ; [all].
det(lam(U, lam(V, 'E' (X, app(U, X) ^  app(V, X))))) --> [a] ; [some].
%Quantifiers for second NP:
det(lam(U, lam(V,lam(W, @ (X, app(U, X) -> app(app(V, X),W)))))) --> [every] ; [all].
det(lam(U, lam(V,lam(W,'E'(X, app(U, X) ^ app(app(V, X),W)))))) --> [a] ; [some].

%connectives for NP and VP
con(lam(U, lam(V, lam(X, (app(U, X) ^ app(V,X)))))) --> [and].
%con(lam(U, lam(V, lam(W, lam(X, (app(app(U, X),W) ^ app(app(V,X),W))))))) --> [and].
con(lam(U, lam(V, lam(X, (app(U, X) v app(V,X)))))) --> [or].
%connectives for sentences
cons(lam(U, lam(V, U -> V))) --> [imp].
cons(lam(U, lam(V, U ^ V))) --> [and].
cons(lam(U, lam(V, U v V))) --> [or].

%Beta conversion, ie. apply arguments to lambda expressions
%app(mia, lam(X, walk(X))) --> walk(mia)

betaconv(Expr, Result, []) :-
        var(Expr),
        Result = Expr.
%push variable on stack
betaconv(Expr, Result, Stack) :-
        nonvar(Expr), Expr = app(Functor, Arg),
        nonvar(Functor),
        alphaconv(Functor, [], []-_, Alpha),
        betaconv(Alpha, Result, [Arg|Stack]).
        %betaconv(Functor, Result, [Arg|Stack]).
%pop from stack
betaconv(Expr, Result, [Element|Stack]) :-
        nonvar(Expr), Expr = lam(Element, Formula),
        betaconv(Formula, Result, Stack).
%handle connectives and remaining lamda-expressions
betaconv(Expr, Result, []) :-
        nonvar(Expr),
        \+ (Expr = app(X, _), nonvar(X)),
        compose(Expr, Functor, SubExprs),
        betaconvlist(SubExprs, Results),
        compose(Result, Functor, Results).


%beta convert a list of expressions
betaconvlist([], []).
betaconvlist([Expr|Tail], [Result|Results]) :-
        betaconv(Expr, Result, []),
        betaconvlist(Tail, Results).

% foo(bar) -> [foo, bar]
compose(Term, Symbol, ArgList):-
    Term =.. [Symbol | ArgList].

%Alpha conversion, ie. rename variables so as not to conflict with variables
%outside their scope.
alphaconv(Expr, Sub, Free1-Free2, Result) :-
        var(Expr),
        (member(sub(Arg, Result), Sub),
        Expr==Arg, !,
        Free2=Free1
        ;
        Result=Expr,
        Free2=[Expr|Free1]).

%first test for lambda/quantifier
alphaconv(Expr, Subs, Free1-Free2, lam(Y, F2)) :-
        nonvar(Expr), Expr = lam(X, F1),
        alphaconv(F1, [sub(X, Y) | Subs], Free1-Free2, F2).
alphaconv(Expr, Subs, Free1-Free2, some(Y, F2)) :-
        nonvar(Expr), Expr = some(X, F1),
        alphaconv(F1, [sub(X, Y) | Subs], Free1-Free2, F2).
alphaconv(Expr, Subs, Free1-Free2, all(Y, F2)) :-
        nonvar(Expr), Expr = all(X, F1),
        alphaconv(F1, [sub(X, Y) | Subs], Free1-Free2, F2).

%then try to match binary connectives:
alphaconv(Expr1, Subs, Free1-Free2, Expr2) :-
        nonvar(Expr1),
        \+ Expr1 = lam(_,_), \+ Expr1 = some(_,_), \+ Expr1 = all(_,_),
        compose(Expr1, Symbol, Args1),
        alphaconvlist(Args1, Subs, Free1-Free2, Args2),
        compose(Expr2, Symbol, Args2).

alphaconv(Result, [], []-_, Result).

%process a list of expressions
alphaconvlist([], _, Free-Free, []).
alphaconvlist([Expr|Tail], Subs, Free1-Free3, [Result|Results]) :-
        alphaconv(Expr, Subs, Free1-Free2, Result),
        alphaconvlist(Tail, Subs, Free2-Free3, Results).