:- op(500,xfy,&). 
:- op(510,xfy,=>). 
:- op(100,fx,`).

s(T) --> np(VP^S), vp(VP), {pull(S, T)}.

np(NP) --> 
   det(N2^NP), n(N1), optrel(N1^N2).
np((E^S)^S) --> pn(E).

vp(X^S) --> tv(X^IV), np(IV^S).
vp(IV) --> iv(IV).

optrel((X^S1)^(X^(S1 & S2))) --> [that], vp(X^S2).
optrel(N^N) --> [].

det(LF) --> [D], {det(D, LF)}.
det( every, (X^S1)^(X^S2)^
               q(P^Q^all(X,P=>Q),S1,S2) ).
det( a,     (X^S1)^(X^S2)^
               q(P^Q^exists(X,P&Q),S1,S2) ).

n(LF)   --> [N], {n(N, LF)}.
n( book,      X^(`book(X))      ).
n( professor, X^(`professor(X)) ).
n( program,   X^(`program(X))   ).
n( student,   X^(`student(X))   ).

pn(E) --> [PN], {pn(PN, E)}.
pn( terry,  terry  ).
pn( shrdlu, shrdlu ).

tv(LF) --> [TV], {tv(TV, LF)}.
tv( ran,   X^Y^(`ran(X,Y))   ).
tv( wrote, X^Y^(`wrote(X,Y)) ).

iv(LF) --> [IV], {iv(IV, LF)}.
iv( halts, X^(`halts(X)) ).



pull(QuantTree, Formula) :-
   pull(QuantTree, Matrix, Store),
   apply_quants(Store, Matrix, Formula).

pull(`Predication, Predication, []).
pull(QuantTree1 & QuantTree2, Formula1 & Formula2, Store) :-
   pull(QuantTree1, Matrix1, Store1),
   pull(QuantTree2, Matrix2, Store2),
   conc(Pass1, Apply1, Store1),
   conc(Pass2, Apply2, Store2),
   apply_quants(Apply1, Matrix1, Formula1),
   apply_quants(Apply2, Matrix2, Formula2),
   shuffle(Pass1, Pass2, Store).
pull(q(Quantifier, RangeTree, ScopeTree), Matrix, Store) :-
   pull(RangeTree, RangeMatrix, RangeStore),
   pull(ScopeTree, Matrix, ScopeStore),
   conc(RangePass, RangeApply, RangeStore),
   apply_quants(RangeApply, RangeMatrix, Range),
   reduce(Quantifier, Range, StoreElement),
   conc(RangePass, [StoreElement], Pass),
   shuffle(Pass, ScopeStore, Store).

apply_quants([], Formula, Formula).
apply_quants([StoreElement|Elements], Matrix, Formula) :-
   apply_quants(Elements, Matrix, SubFormula),
   reduce(StoreElement, SubFormula, Formula).


shuffle(L, [], L).
shuffle(L, [R1|Rrest], S) :-
    conc(L1, Lrest, L),
    shuffle(Lrest, Rrest, Srest),
    conc(L1, [R1|Srest], S).

conc([], List, List).
conc([Element|Rest], List, [Element|LongRest]) :-
    conc(Rest, List, LongRest).