/*************************************************************************

         name: lambda.pl
      version: April 27, 2001
  description: Semantic Construction with Beta Conversion
      authors: Patrick Blackburn & Johan Bos
    additions: Stephan Walter, Aljoscha Burchardt (2002) 
*************************************************************************/

:- module(lambda,[lambda/0,lambda/1,lambda/2]).

:- use_module(readLine,[readLine/1]).
:- use_module(comsemLib,[printRepresentations/1,compose/3]).
:- use_module(signature,[resetVars/0,vars2atoms/1]).
:- use_module(betaConversion,[betaConvert/2]).

:- ensure_loaded(englishGrammar).
:- ensure_loaded(comsemOperators).
:- [user:comsemOperators].

/*========================================================================
   Driver Predicates
========================================================================*/

lambda :-
	readLine(Sentence),
	parse(Sentence,Formula),
	betaConvert(Formula,Converted),
	resetVars,vars2atoms(Formula),
	printRepresentations([Converted]).

% This version returns the beta-converted semantic representation
% in the variable Converted. 
lambda(Converted) :-
	readLine(Sentence),
	lambda(Sentence,Converted).


% This version takes in a sentence (as a list of atoms) and
% gives back the beta converted semantic representation. It doesn't
% do any printout .
lambda(Sentence,Converted):-
	parse(Sentence,Formula),
	betaConvert(Formula,Converted),
	resetVars,vars2atoms(Formula).	

/*========================================================================
   Parsing 
========================================================================*/

parse(Sentence,Formula):-
	s2(Formula,Sentence,[]).
	

/*========================================================================
   Semantic Rules
========================================================================*/

combine(s2:X,[s1:X]).

combine(s2:(X>Y),[s1:X,cond,s1:Y]).

combine(s1:(NP@VP),[np2:NP,vp2:VP]).

combine(np2:X,[np1:X]).
combine(np2:((COORD@X)@Y),[np1:X,coord:COORD,np1:Y]).

combine(np1:(DET@N),[det:DET,n2:N]).
combine(np1:X,[pn:X]).
combine(np1:X,[np:X]).

combine(n2:X,[n1:X]).
combine(n2:((COORD@X)@Y),[n1:X,coord:COORD,n1:Y]).

combine(n1:(ADJ@N),[adj:ADJ,n1:N]).
combine(n1:X,[noun:X]).
combine(n1:(PP@NOUN),[noun:NOUN,pp:PP]).
combine(n1:(RC@NOUN),[noun:NOUN,rc:RC]).

combine(vp2:X,[vp1:X]).
combine(vp2:((COORD@X)@Y),[vp1:X,coord:COORD,vp1:Y]).

combine(vp1:X,[v2:X]).
combine(vp1:(MOD@V),[mod:MOD,v2:V]).

combine(v2:(COP@NP),[cop:COP,np2:NP]).
combine(v2:(NEG@(COP@NP)),[cop:COP,neg:NEG,np2:NP]).
combine(v2:X,[v1:X]).
combine(v2:((COORD@X)@Y),[v1:X,coord:COORD,v1:Y]).

combine(v1:X,[iv:X]).
combine(v1:(TV@NP),[tv:TV,np2:NP]).

combine(pp:(PREP@NP),[prep:PREP,np2:NP]).
combine(rc:(RELPRO@VP),[relpro:RELPRO,vp2:VP]).

/*========================================================================
   Semantic Macros
========================================================================*/

detSem(uni,lambda(P,lambda(Q,forall(X,(P@X)>(Q@X))))).

detSem(indef,lambda(P,lambda(Q,exists(X,(P@X)&(Q@X))))).

detSem(wh,lambda(P,lambda(Q,lambda(X,(P@X)&(Q@X))))).

nounSem(Sym,lambda(X,Formula)):- 
   compose(Formula,Sym,[X]).

pnSem(Sym,lambda(P,P@Sym)).

npSem(wh,Sym,lambda(Q,lambda(X,Formula&(Q@X)))):-
   compose(Formula,Sym,[X]).

ivSem(Sym,lambda(X,Formula)):- 
   compose(Formula,Sym,[X]).

tvSem(Sym,lambda(K,lambda(Y,K @ lambda(X,Formula)))):- 
   compose(Formula,Sym,[Y,X]).

relproSem(lambda(P,lambda(Q,lambda(X,(P@X)&(Q@X))))).

prepSem(Sym,lambda(K,lambda(P,lambda(Y,(K@lambda(X,F)) & (P@Y))))):-
   compose(F,Sym,[Y,X]).

adjSem(Sym,lambda(P,lambda(X,(F&(P@X))))):-
   compose(F,Sym,[X]).

modSem(neg,lambda(P,lambda(X,~(P@X)))).

coordSem(conj,lambda(X,lambda(Y,lambda(P,(X@P) & (Y@P))))).
coordSem(disj,lambda(X,lambda(Y,lambda(P,(X@P) v (Y@P))))).

%not implemented
proSem(_,_) :- fail.