#!/usr/bin/python
#lexicalised type driven semantic grammar. Andreas van Cranenburgh 2010.
import nltk
types = {'A': '<<e,t>,t>', 'B': '<<e,t>,t>', 'C': '<<e,t>,t>',
	'D': '<<<e,t>,t>, <<e,t>, t>>',
	'P': '<e,t>', 'Q': '<e,t>',
	'girl': '<e,t>', 'book': '<e,t>', 'boy': '<e,t>', 'smokes': '<e,t>',
	'x': 'e', 'y': 'e', 'z': 'e'}

lexicon = {'every': r'\P Q.all x.(P(x) & Q(x))',
	'girl' : r'\x.girl(x)',
	'book' : r'\x.book(x)',
	'boy' : r'\x.boy(x)',
	'with' : [r'\A P B.(A(\y.(B(\x.(using(x)(y) & P(x))))))',
				r'\A B P.(A(\y.(B(\x.(has(x)(y) & P(y))))))'],
	'smokes' : r'\x.smokes(x)',
	'gives' : [r'\B C A.C(\x.A(\z.(B(\y.give(x)(y)(z)))))',
			r'\B C x.C(\z.(B(\y.give(x)(y)(z))))'],
	'mary' : r'\P.P(mary)',
	'john' : r'\P.P(john)',
	'bill' : r'\P.P(bill)',
	'a' : r'\P Q.exists x.(P(x) & Q(x))',
	'hits' : r'\A x.A(\y.(hits(x)(y)))',
	'too' : r'\D.D',
	'does' : r'\A.A',
	'and' : r'\P A y.A(\x.(P(x) & P(y)))' }

lp = nltk.sem.logic.LogicParser(True) #typed logic
lp = nltk.sem.logic.LogicParser()

def vr(n, phi):
	return lp.parse(r"\x.\V.(V(%s(x)))" % phi)
def ar(n, phi):
	return lp.parse(r"\x.\Y.\z.(Y(\y.%s(x)(y)(z)))" % phi)
def al(n, phi):
	return lp.parse(r"\x.\y.\z.(%s(x)(\V.V(y))(z))" % phi)

def vr1(phi):
	return lp.parse(r"\A V.(V(A))")(phi)
def ar1(phi):
	return lp.parse(r"\A Y y1.(Y(\z1.(A(z1)(y1))))")(phi)
def al1(phi):
	return lp.parse(r"\A y2 z2.(A(\V.V(y2))(z2))")(phi)

def vr2(phi):
	return lp.parse(r"\A x22 V.(V(A(x22)))")(phi)
def ar2(phi):
	return lp.parse(r"\A x11 Y.(Y(\y11.(A(x11)(y11))))")(phi)
def al2(phi):
	return lp.parse(r"\A x33 y33.(A(x33)(\V.V(y33)))")(phi)

#print ar1("find").simplify()
#print al1("seek").simplify()

#exit()

#lexicon = dict((w, (type(m) == list and m or [m])) for w, m in lexicon.items())
#lexicon = dict((w, [lp.parse(a, types) for a in m]) for w, m in lexicon.items())
#print "the lexicon:"
#for w,m in lexicon.items(): 
#	print w, 
#	for a in m: print a, a.type