% NLIDB Programs
% nlidb.pl

% Grammar and lexicon in BHGRN

s(dec, Smx, Store0-Store) --->
  [np(NPmx, Store0-Store1), vp(VPmx, Store1-Store)],
  {beta_reduce(NPmx*X^exists(E, ((VPmx*X)*E)), Smx)}.

s(ynq, Smx, Store0-Store) --->
  [aux(Auxmx, Store0-Store1), np(NPmx, Store1-Store2), vp(VPmx, Store2-Store)],
  {beta_reduce(Auxmx*(NPmx*X^exists(E, ((VPmx*X)*E))), Smx)}.

s(whq, Smx, Store0-Store) --->
  [npwh(NPmx, Store0-Store1), vp(VPmx, Store1-Store)],
  {beta_reduce(NPmx*X^exists(E, ((VPmx*X)*E)), Smx)}.

vp(Vimx, Store) --->
  [vi(Vimx, Store)].

vp(VPmx, Store0-Store) --->
  [vt(Vtmx, Store0-Store1), np(NPmx, Store1-Store)],
  {beta_reduce(Vtmx*NPmx, VPmx)}.

vp(VPmmx, Store0-Store) --->
  [vp(VPmx, Store0-Store1), pp(PPmx, Store1-Store)],
  {beta_reduce(X^(PPmx*(VPmx*X)), VPmmx)}.

np(P^P(Z), [stored(NPmx, Z)| Store0]-Store) --->
  [det(Detmx, Store0-Store1), nbar(Nbarmx, Store1-Store)],
  {beta_reduce(Detmx*Nbarmx, NPmx)}.

npwh(P^P(Z), [stored(NPmx, Z)| Store0]-Store) --->
  [detwh(Detmx, Store0-Store1), nbar(Nbarmx, Store1-Store)],
  {beta_reduce(Detmx*Nbarmx, NPmx)}.

np(PNamemx, Store) ---> 
  [pname(PNamemx, Store)].

nbar(Nmx, Store) --->
  [n(Nmx, Store)].

nbar(Nbmmx, Store0-Store) --->
  [nbar(Nbmx, Store0-Store1), pp(PPmx, Store1-Store)],
  {beta_reduce(PPmx*Nbmx, Nbmmx)}.

pp(PPmx, Store0-Store) --->
  [p(Pmx, Store0-Store1), np(NPmx, Store1-Store)],
  {beta_reduce(Pmx*NPmx, PPmx)}.

vi(X^E^lectures1(E, X), S-S) ===> [lectures].
vi(X^E^lectures1(E, X), S-S) ===> [lecture].


vt(P^Y^E^(P*X^teach1(E, Y, X)), S-S) ===> [teaches].
vt(P^Y^E^(P*X^teach1(E, Y, X)), S-S) ===> [teach].
vt(P^Y^E^(P*X^study1(E, Y, X)), S-S) ===> [studies].
vt(P^Y^E^(P*X^study1(E, Y, X)), S-S) ===> [study].
vt(P^Y^E^(P*X^tutor1(E, Y, X)), S-S) ===> [tutors].
vt(P^Y^E^(P*X^tutor1(E, Y, X)), S-S) ===> [tutor].
vt(P^Y^E^(P*X^pass1(E, Y, X)), S-S)  ===> [passed].
vt(P^Y^E^(P*X^pass1(E, Y, X)), S-S)  ===> [pass].

aux(P^P, S-S) ===> [does].

det(Q^P^for_all(X, Q*X => P*X), S-S)     ===> [every].
det(Q^P^exists(X, Q*X &  P*X), S-S)       ===> [some].
det(Q^P^for_all(X, Q*X => (~P*X)), S-S) ===> [no].

detwh(Q^P^wh(X, Q*X & P*X), S-S)        ===> [which].

n(X^lecturer1(X), S-S) ===> [lecturer].
n(X^course1(X), S-S)   ===> [course].
n(X^student1(X), S-S)  ===> [student].

pname(P^(P*holofernes), S-S) ===> [holofernes].
pname(P^(P*pinch), S-S)      ===> [pinch].
pname(P^(P*nathaniel), S-S)  ===> [nathaniel].
pname(P^(P*balthazar), S-S)  ===> [balthazar].
pname(P^(P*litCrit), S-S)    ===> [literary, criticism].
pname(P^(P*shakeComs), S-S)  ===> [shakespearean, comedies].

p(P^P1^X^(P*Y^(P1*X & with1(X, Y)))) ===> [with].

% Logical definitions

~ P :- \+ P.

% (P & Q) :-          ---This is in-built in our Prolog, so we have commented out
%   call(P), call(Q). ---this definition.


for_all(X, P => Q) :-
  \+ (call(P),
      \+ call(Q)).

exists(X, P) :-
  call(P).

wh(X, P) :- 
   findall(X, P, Xs), write(Xs).

% The front end

nlidb :-
  write('Welcome to BH-NLIDB'), nl, nl,
  repeat,
    nl,
    write('> '),
    read_string(String), nl,
    linguistic_analyser(String), fail, !.


linguistic_analyser(String) :-
  setof(parse(Type, Smx, Store),
         parse(String, s(Type, Smx, Store-[])),
        Parses), !,
  findall(reading(Ty, ScopedTrans),
         (member(parse(Ty, Mx, St), Parses),
          scope(Mx, St, ScopedTrans),
          \+ fvs(ScopedTrans, 0)),
        Readings), !,
  converter(Readings).

linguistic_analyser(String) :-
  write('Linguistic analyser: Could not process'), nl.


converter(Readings) :-
  setof(reading(Type, ScopedTrans),
        (member(reading(Type, ScopedTrans), Readings),
         disambiguator(ScopedTrans),
         write('Paraphrase: '), write(ScopedTrans), nl,
         write('Response  : '), dbms(Type, ScopedTrans), nl),
        TestedReadings), !.

converter(Readings) :-
  write('Converter: Could not process'), nl.


dbms(dec, Query) :-
  (call(Query) -> write('That''s true')
   ;              write('That''s probably not true')).

dbms(ynq, Query) :-
  (call(Query) -> write('Yes')
   ;              write('I don''t think so')).

dbms(whq, Query) :-
  call(Query).

% Database

students(nathaniel).
students(balthazar).

lecturers(holofernes).
lecturers(pinch).

courses(litCrit). 
courses(shakeComs).

enrolments(nathaniel, litCrit,   c).
enrolments(balthazar, litCrit,   e).
enrolments(balthazar, shakeComs, a). 

offerings(holofernes, litCrit).
offerings(pinch,      shakeComs).

% Term conversion definitions

teach1(_, L, C) :- offerings(L, C).
study1(_, S, C) :- enrolments(S, C, _).
tutor1(_, L, S) :- offerings(L, C), enrolments(S, C, _).
pass1(_, S, C)  :- enrolments(S, C, G), member(G, [a, b, c]).
lectures1(_, _, L) :- lecturers(L).
lecturer1(L) : - lecturers(L).
course1(C) :- courses(C).
student1(S) :- students(S).

%Sortal restriction checker

disambiguator(Reading) :- 
   \+ \+ sortchk(Reading).

sortchk(~ Expr) :- !,
   sortchk(Expr).

sortchk(QuantExpr) :-
   QuantExpr =.. [Qfier, Var, Body],
   quantifier(Qfier), !,
   sortchk(Body).

sortchk(CompExpr) :-
   CompExpr =.. [Connective, Expr1, Expr2],
   connective(Connective), !,
   sortchk(Expr1),
   sortchk(Expr2).

sortchk(Atom) :-
   Atom =.. [Pred | Args],
   of_sort(Pred, PSort), !,
   of_sorts(Args, ArgSorts),
   PSort = ArgSorts.

of_sorts([], []).

of_sorts([Arg | Args], [ArgSort | ArgSorts]) :-
   \+ var(Arg), atomic(Arg),
   of_sort(Arg, ArgSort), !,
   of_sorts(Args, ArgSorts). 

of_sorts([Arg | Args], [Arg | ArgSorts]) :-
   (var(Arg) ; \+ atomic(Arg)), !,
   of_sorts(Args, ArgSorts).

%Sort definitions

of_sort(pinch, object(human(lecturer))).
of_sort(holofernes, object(human(lecturer))).
of_sort(nathaniel, object(human(student))).
of_sort(balthazar, object(human(student))).

of_sort(teach1, [object(absobj(event)),
                  object(human(lecturer)),
                  object(absobj(course))]).

of_sort(study1, [object(absobj(event)),
                  object(human(student)),
                  object(absobj(course))]).

of_sort(tutor1, [object(absobj(event)),
                  object(human(lecturer)),
                  object(human(student))]).

of_sort(pass1, [object(absobj(event)),
                  object(human(student)),
                  object(absobj(course))]).

of_sort(X, Y).