%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%                                                                %%
%% (Program 3.12 with semantics                                   %%
%% This is similar to but different from Program 4.5 in P&S.)     %%
%%                                                                %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%% Stuff to overcome Sictus' ever-so-helpful  abbreviation of list terms

portray(Term) :- is_list(Term), write(Term).

is_list([]).
is_list([_|_]).

%%%% End of stuff

:- op(500, xfy, &).		% A dummy logical conjunction operator
:- op(510, xfy, =>).    % Dummy implication, for whenwe want to do "every"

%% root S has no gap
s(S) --> s(S,nogap).

%% A predicate is a function NP->S; S is instantiated by `partial
%% execution'.   But the subject is now a function over predicates:
s(S1,Gap) --> np(VP^S1,nogap), vp(VP,Gap).

%%%%%%%%%%%%%%%%% write new sentence-level rules here:
%s_whq(answer(X)&S1) --> ...
%s_whq(answer(X)&S1) --> ...
%
%s_ynq(S1) --> ...
%%%%%%%%%%%%%%%%%

%% In fact, ALL NPs, even proper names, are functions over properties
%% (so betrand becomes np((bertrand^S)^S), while walks as always yields
%% vp(X^walks(X)).   MAKE SURE YOU UNDERSTAND HOW THIS MAKES THE ABOVE
%% S RULE YIELD S1 = walks(bertrand) BEFORE YOU READ BEYOND THE NEXT LINE):
np((E^S)^S,nogap) --> pn(E).

%% The real point of this is to make full NPs do the right thing with
%% quantifiers (look at the definition of determiners etc
%% below.  They turn it via partial execution into the equivalent of
%% the following: 
%%np((X^S2)^S3,nogap) -->
%%      det((X^S1)^(X^S2)^S3), n(X^S0),optrel((X^S0)^(X^S1)).
np(NP,nogap) -->
      det(N2^NP), n(N1),optrel(N1^N2).

%% ... And gaps 
np((X^S)^S,gap(np,X)) --> [].


%%%%%%%%%%%%%%%%%%%%%% define wh_nps like who and which frog
%%wh_nps
%wh_np(WH) --> whn(WH).
%
%wh_np(NP) --> ...
%wh_np(NP) --> ...
%%%%%%%%%%%%%%%%%%%%%%%%


vp(X^S1,Gap) -->                    % NB Here we depart from P&S
      tv(Y^X^S),                    % There is more to this than meets
      np((Y^S)^S1,Gap).             % the eye !

vp(VP,nogap) -->
      iv(VP).

%% The following bind S0, S1, S2, and S3 in the NP definition:
optrel(N^N) --> [].

optrel((X^S1)^(X^(S1&S2))) -->
      relpron(X), vp(X^S2,nogap).

optrel((X^S1)^(X^(S1&S2))) -->
      relpron(X), s(S2,gap(np,X)).

det(LF) --> [Det], {det(Det,LF)}.
det(a,(X^S1)^(X^S2)^exists(X,S1&S2)).
det(the,(X^S1)^(X^S2)^def(X,S1&S2)).
det(some,(X^S1)^(X^S2)^exists(X,S1&S2)).
det(every,(X^S1)^(X^S2)^all(X,S1=>S2)).

%%%%%%%%%%%%%%%%%%%define wh determiners whdet and whpronouns whn here



%%%%%%%%%%%%%%%%%%%

n(LF) --> [N], {n(N,LF)}.
n(author,X^author(X)).
n(book,X^book(X)).
n(man,X^man(X)).
n(program,X^program(X)).
n(programmer,X^programmer(X)).
n(professor,X^professor(X)).
n(student,X^student(X)).
n(subject,X^subject(X)).

pn(E) --> [PN], {pn(PN,E)}.
pn(begriffsschrift,begriffsschrift).
pn(principia,principia).
pn(lunar,lunar).
pn(shrdlu,shrdlu).
pn(bertrand,bertrand).
pn(gottlob,gottlob).
pn(gilbert,gilbert).
pn(george,george).
pn(terry,terry).
pn(bill,bill).
pn(mathematics,mathematics).

tv(LF) --> [TV], {tv(TV,LF)}.         % NB Here we depart from P&S
tv(concerns,Y^X^concerns(X,Y)).       % Note that this is a more
tv(met,Y^X^met(X,Y)).                 % traditional semantics for TV
tv(ran,Y^X^ran(X,Y)).                 % See the transitive vp defn above
tv(wrote,Y^X^wrote(X,Y)).
tv(write,Y^X^wrote(X,Y)).
tv(concern,Y^X^concerns(X,Y)).

iv(LF) --> [IV], {iv(IV,LF)}.
iv(halted,X^halted(X)).
iv(walks,X^walks(X)).

relpron(LF) --> [RelPron], {relpron(RelPron,LF)}.
relpron(that,LF).
relpron(who,LF).
relpron(whom,LF).

%%%%%%%%%%%%%%%%%%%%%%%%

answer(Term).
'&'(X,Y) :- X,Y.


%not using exists(X,TerminX) :- \+ \+ TerminX.
exists(X,TerminX) :- TerminX.

%%%%%%%%%%%%%%%%%%%%%%%% all etc defined here


%%%%%%%%%%%%%%%%%%%%%%%%