#!/usr/bin/env python
import sys

sys.setrecursionlimit(50)

# Lambda calculus in Python
# as per M-J Dominus Perl example
# IF -> ^b.^x.^y.b x y
def IF(b):
	def _A(x):
		def __A(y):
			return b(x)(y)
		return __A
	return _A

# TRUE -> ^x.^y.x
def TRUE(x):
	def _TRUE(y):
		return x
	return _TRUE

# FALSE -> ^x.^y.y
def FALSE(x):
	def _FALSE(y):
		return y
	return _FALSE

print "IF test: IF(FALSE)(TRUE)(FALSE):",  IF(FALSE)(TRUE)(FALSE)
print "IF test: IF(TRUE)(TRUE)(FALSE):",  IF(TRUE)(TRUE)(FALSE)

# PAIR -> ^a.^b.^f.f a b
def PAIR(a):
	def _PAIR(b):
		def __PAIR(f):
			return f(a)(b)
		return __PAIR
	return _PAIR

# FIRST -> ^p.p TRUE
def FIRST(p):
	return p(TRUE)

# SECOND -> ^p.p FALSE
def SECOND(p):
	return p(FALSE)

# Not Church numerals, not exactly Henk Barendregt's system either.
# Essentially a tally system :
# Zero -> (T, T)
# One ->  (F, (T, T))
# Two ->  (F, (F, (T, T)))
# And so forth.  Makes it easy to do successor and
# predecessor, a bit harder to do addition and subtraction.
# ZERO -> PAIR TRUE TRUE
ZERO = PAIR(TRUE)(TRUE)

def ZEROP(n):
	return FIRST(n)

# SUCC -> ^n.(PAIR FALSE n)
# CONS a 2-element list with FALSE as first element, rest of list
# as 2nd element.
def SUCC(n):
	return PAIR(FALSE)(n)

ONE = SUCC(ZERO)
TWO = SUCC(ONE)
THREE = SUCC(TWO)

print "Test ZEROP: ZEROP(ZERO) ->", ZEROP(ZERO)
print "Test ZEROP: ZEROP(THREE) ->", ZEROP(THREE)

# PRED -> ^n.(SECOND n)
def PRED(n):
	return SECOND(n)

def convert_to_number(n):
	i = 0
	while IF(ZEROP(n))(False)(True):
		i += 1
		n = PRED(n)
	return i

try: print "PRED(ZERO) -> ", convert_to_number(PRED(ZERO))
except Exception, msg:
	print "PRED(ZERO) does not work:", msg
print "PRED(ONE) -> ", convert_to_number(PRED(ONE))
print "PRED(TWO) -> ", convert_to_number(PRED(TWO))
print "PRED(THREE) -> ", convert_to_number(PRED(THREE))

print "ZERO =", convert_to_number(ZERO)
print "ONE =", convert_to_number(ONE)
print "TWO =", convert_to_number(TWO)
print "THREE =", convert_to_number(THREE)


# YM = %f.(%x.(%y.f (x x)))(%x.(%y.f (x x)))
#$YM = sub { my $f = shift;
#	(sub { my $x = shift;
#		sub { my $y = shift;
#			$f->($x->($x));
#		};
#	})->
#	(sub { my $x = shift;
#		sub { my $y = shift;
#			$f->($x->($x));
#		};
#	})
#
#};

def Identity(x):
	return x

def T(a):
	return THREE

# YM -> ^f.(^x.(^y.f(x x)))(^x.(^y.f(x x)))
def YM0(f):
	def _B(x):
		def _dummy(y):
			return f(x(x))
		return _dummy(_dummy)
	return _B

# YM -> ^f.(^a.(^p.f(a a)))(^b.(^q.f(b b)))
def YM1(f):
	def _A(a):
		def _dummyA(*p):
			return f(a(a))
		return _dummyA
	def _B(b):
		def _dummyB(*q):
			return f(b(b))
		return _dummyB
	return _A(_B)

# YM -> ^f.(^x.(^y.f(x x)))(^x.(^y.f(x x)))
def YM(f):
	def _A(x):
		def _dummyA(*y):
			return f(x(x))
		return _dummyA
	return _A(_A)

print "YM test 1, Should print 3:", convert_to_number(YM(T)(ONE))

## R -> ^g.^m.^n.IF (ZEROP m)(^q.n)(^q.(g Identity (PRED m)(SUCC n)))
def R(g):
	def _A(m):
		def _B(n):
			def _force(*c): return Identity
			def _true_clause(a):  return n
			def _false_clause(b): return g(_force)(PRED(m))(SUCC(n))
			return IF(ZEROP(m))(_true_clause)(_false_clause)(_force)
		return _B
	return _A


print "Calling YM(R)(Identity)"
ADD = YM(R)(Identity)
#
print "Calling ADD(TWO)(THREE)"
FIVE = ADD(TWO)(THREE)
print FIVE
print "--> ANSWER 2 + 3 =", convert_to_number(FIVE)
#
print "Calling ADD(TWO)(ONE)"
ANSWER = ADD(TWO)(ONE)
print ANSWER
print "--> ANSWER 2 + 1 =", convert_to_number(ANSWER)

print "Calling ADD(FIVE)(ZERO)"
ANSWER = ADD(FIVE)(ZERO)
print "--> ANSWER 5 + 0 =", convert_to_number(ANSWER)

ADD2 = YM(R)(ONE)
TEN = ADD2(FIVE)(FIVE)
print "--> ANSWER 5 + 5 =", convert_to_number(TEN)

print "Calling ADD(TWO)(TWO)"
FOUR = ADD(TWO)(TWO)
print "--> ANSWER 2 + 2 =", convert_to_number(FOUR)

# Python multiply-the-hard-way
def multiply(m, n):
	if m == 0:
		return 0
	else:
		return n + multiply(m - 1, n)

def M(g):
	def _A(m):
		def _B(n):
			def _force(*c): return Identity  # Never gets executed
			def _true_clause(a): return ZERO 
			def _false_clause(b): return ADD(n)(g(_force)(PRED(m))(n))
			return IF(ZEROP(m))(_true_clause)(_false_clause)(_force)
		return _B
	return _A

MULT = YM(M)(ONE)

A = MULT(TWO)(THREE)
print "--> ANSWER  2 * 3 =", convert_to_number(A)

B = MULT(TWO)(FOUR)
print "--> ANSWER  2 * 4 =", convert_to_number(B)

def Rx(g):
	def _A(m):
		def _B(n):
			def _force(*c): return Identity
			def _true_clause(a): return n
			def _false_clause(b): return g(_force)(PRED(m))(SUCC(n))
			return IF(ZEROP(m))(_true_clause)(_false_clause)(_force)
		return _B
	return _A

ADD = YM(Rx)(Identity)

def P(g):
	def _A(m):
		def _B(n):
			def _force(*c): return Identity  # Never gets executed
			def _true_clause(a): return ONE 
			def _false_clause(b): return MULT(n)(g(_force)(PRED(m))(n))
			return IF(ZEROP(m))(_true_clause)(_false_clause)(_force)
		return _B
	return _A

POW = YM(P)(Identity)
C = POW(TWO)(THREE)
print "--> ANSWER 3^2 =", convert_to_number(C)
D = POW(FOUR)(TWO)
print "--> ANSWER 2^4 =", convert_to_number(D)

sys.exit(0)