class Term:
    """The supertype of all terms in the lambda calculus."""

    def __repr__(self):
        return str(self)

    def __str__(self):
        return self._str(True, True)

    def C(self):
        """Convert me into a combinator expression."""
        raise NotImplementedError

    def isFree(self, var):
        """True iff VAR appears free (not lambda bound) in SELF."""
        raise NotImplementedError

    def beta(self):
        """Attempt to find a beta reduction in SELF. If found, return
        (S', True), where S' is the result of applying the reduction.  Otherwise
        return (SELF, False)."""
        raise NotImplementedError

    def subst(self, var, val):
        """The result of substituting VAL for all free occurrences of VAR in SELF."""
        raise NotImplementedError

class Prim(Term):
    """A primitive combinator."""

    def __init__(self, id, arity, redux):
        """The combinator denoted by ID, and performing the reduction REDUX
        when applied to ARITY arguments."""
        self._id, self._arity, self._redux = id, arity, redux

    def _str(self, leftd, rightd):
        return self._id

    def C(self):
        return self

    def isFree(self, var):
        return False

    def beta(self):
        return self, False

    def subst(self, var, val):
        return self

    def arity(self):
        return self._arity

    def redux(self, args):
        return self._redux(*args)

# The standard combinators

I = Prim('I', 1, lambda x: x)
S = Prim('S', 3, lambda x, y, z: Apply(Apply(x, z), Apply(y, z)))
K = Prim('K', 2, lambda x, y: x)

class Sym(Term):
    """A symbol."""

    uid = 0

    def __init__(self, id):
        """The symbol whose printed form is ID."""
        self._id = id

    def _str(self, leftd, rightd):
        return self._id

    def C(self):
        return self

    def __eq__(self, other):
        if type(other) is Sym:
            return other._id == self._id
        else:
            return False

    def isFree(self, var):
        return self == var

    def beta(self):
        return self, False

    def subst(self, var, val):
        if var == self:
            return val
        else:
            return self

    @staticmethod
    def new_var():
        Sym.uid += 1
        return Sym('v' + str(uid))

class Apply(Term):
    """An application term."""

    def __init__(self, left, right):
        """The application (LEFT RIGHT)."""
        self._left, self._right = left, right

    def _str(self, leftd, rightd):
        if not leftd:
            return "({} {})".format(self._left._str(True, False),
                                    self._right._str(False, True))
        else:
            return "{} {}".format(self._left._str(True, False),
                                  self._right._str(False, rightd))

    def C(self):
        return Apply(self._left.C(), self._right.C())

    def isFree(self, var):
        return self._left.isFree(var) or self._right.isFree(var)

    @property
    def left(self):
        return self._left

    @property
    def right(self):
        return self._right

    def _getPrim(self, nesting):
        p = self
        if type(self._left) is Prim:
            if nesting + 1 == self._left.arity():
                return self._left, [self._right]
        elif type(self._left) is Apply:
            prim, args = self._left._getPrim(nesting + 1)
            if prim:
                return prim, args + [self._right]
        return None, None

    def beta(self):
        if type(self._left) is Lambda:
            return self._left.apply(self._right), True
        prim, args = self._getPrim(0)
        if prim:
            return prim.redux(args), True
        else:
            left, change = self._left.beta()
            if change:
                return Apply(left, self._right), True
            right, change = self._right.beta()
            if change:
                return Apply(left, right), True
            return self, False

    def subst(self, var, val):
        return Apply(self._left.subst(var, val), self._right.subst(var, val))

class Lambda(Term):
    """A lambda term."""

    def __init__(self, var, body):
        """The term \ VAR. BODY."""
        self._var, self._body = var, body

    def _str(self, leftd, rightd):
        if rightd:
            return "\\{}. {}".format(self._var, self._body._str(True, True))
        else:
            return "(\\{}. {})".format(self._var, self._body._str(True, True))        
    def isFree(self, var):
        return var != self._var and self._body.isFree(var)

    def C(self):
        if not self._body.isFree(self._var):
            return Apply(K, self._body.C())
        elif self._var == self._body:
            return I
        elif type(self._body) is Lambda and self._body._body.isFree(self._var):
            return Lambda(self._var, self._body.C()).C()
        else:
            t1 = Lambda(self._var, self._body.left).C()
            t2 = Lambda(self._var, self._body.right).C()
            return Apply(Apply(S, t1), t2)
    
    def beta(self):
        return self, False

    def apply(self, arg):
        return self._body.subst(self._var, arg)

    def subst(self, var, val):
        if var == self._var:
            return self
        elif val.isFree(self._var):
            newv = Sym.new_var()
            new_body = self._body.subst(self._var, newv).subst(var, val)
            return Lambda(newv, new_body)
        return Lambda(self._var, self._body.subst(var, val))

def reduce(term, lim=10):
    """Apply beta reductions to TERM up to LIM times, or until TERM contains no
    further reductions."""

    changed = True
    while lim > 0 and changed:
        term, changed = term.beta()
        lim -= 1
    return term

# Some symbols.

x = Sym('x')
y = Sym('y')
z = Sym('z')
a = Sym('a')
b = Sym('b')
f = Sym('f')
n = Sym('n')
p = Sym('p')

# \x. \y. y x

term = Lambda(x, Lambda(y, Apply(y, x)))

# The "paradoxical" combinator.

Y = Lambda(f, Apply(Lambda(x, Apply(f, Apply(x, x))),
                    Lambda(x, Apply(f, Apply(x, x)))))

# Church Numerals

ZERO       = Lambda(f, Lambda(x, x))
SUCCESSOR  = Lambda(n, Lambda(f, Lambda(x, Apply(f, Apply(Apply(n, f), x)))))
ADD        = Lambda(a, Lambda(b, Apply(Apply(a, SUCCESSOR), b)))
MULT       = Lambda(a, Lambda(b, Apply(Apply(a, Apply(ADD, b)), ZERO)))

# Logic and conditionals

TRUE       = Lambda(x, Lambda(y, x))
FALSE      = Lambda(x, Lambda(y, y))
IFTHENELSE = Lambda(p, Lambda(x, Lambda(y, Apply(Apply(p, x), y))))
AND        = Lambda(x, Lambda(y, Apply(Apply(x, y), x)))
OR         = Lambda(x, Lambda(y, Apply(Apply(x, x), y)))
NOT        = Lambda(x, Apply(Apply(x, FALSE), TRUE))
ISZERO     = Lambda(x, Apply(Apply(x, Lambda(y, FALSE)), TRUE))

# Church numerals in Python

zero        = lambda f: lambda x: x
successor   = lambda n: lambda f: lambda x: f(n(f)(x))
add_church  = lambda a: lambda b: a(successor)(b)
mult_church = lambda a: lambda b: a(add_church(b))(zero)

def to_int(church):
    """Convert a Python Church numeral into a Python int."""
    return church(lambda x: x+1)(0)