diff --git a/data2.py b/data2.py
index 43085f5..b8a5767 100644
--- a/data2.py
+++ b/data2.py
@@ -148,7 +148,7 @@ def rename_off(obj,excl):
debug("%s: renaming %s to %s" % (d_show(obj),v,nv))
obj = obj.rename(v,Var(nv))
excl.add(Var(nv))
-# debug("%s: renaming off %s => %s" % (d_show(old),old_e,d_show(obj)))
+ debug("%s: renaming off %s => %s" % (d_show(old),old_e,d_show(obj)))
return obj
def alpha(obj,app,excl_vars=Set()):
@@ -160,6 +160,9 @@ class Term(object):
global N
N += 1
self.n = N
+
+ def eta(self):
+ return self
class Var(Term):
def __init__(self,name):
@@ -262,18 +265,24 @@ class Lambda(Term):
return l
def eval(self,excl_vars=Set()):
- self = self.eval_vars(excl_vars + Set(self.var))
- if type(self) != Lambda:
- return self
+# self = self.eval_vars(excl_vars + Set(self.var))
+# if type(self) != Lambda:
+# return self
return Lambda(self.var,self.expr.eval(excl_vars + Set(self.var)))
def eval_vars(self,excl_vars=Set()):
+ debug("Lambda.eval_vars called for %s" % d_show(self))
l = Lambda(self.var, self.expr.eval_vars(excl_vars + Set(self.var)))
- # eta-reduction
- if type(l.expr)==Expr and l.expr.op=='@' and str(l.expr.a2)==str(l.var):
- return l.expr.a1
+ return l
+
+ def eta(self):
+ "Eta-reduction"
+ if type(self.expr)==Expr and self.expr.op=='@' and str(self.expr.a2)==str(self.var):
+ debug("[%d] Lambda.eval_vars returning %s" % (self.n,d_show(self.expr.a1)))
+ return self.expr.a1
else:
- return l
+ debug("[%d] Lambda.eval_vars returning %s" % (self.n,d_show(self)))
+ return self
def apply(self,expr,excl_vars=Set()):
old = copy(self)
@@ -289,7 +298,7 @@ class Expr(Term):
self.a1 = a1
self.a2 = a2
self.setnumber()
-# debug("[%d] New Expr: %s" % d_show(self))
+ debug("[%d] New Expr: %s" % (self.n,self))
def __repr__(self):
return "<Expr: %s %s %s>" % (self.a1,self.op,self.a2)
@@ -317,14 +326,17 @@ class Expr(Term):
return Expr(self.op,a,b)
def eval(self,excl_vars=Set()):
+ debug("[%d] Eval called for (%s) <%s>, <%s>" % (self.n, self.op,self.a1,self.a2))
+ old_n = self.n
self = self.eval_vars()
+ debug("[%d] %s => %s" % (old_n,type(self),d_show(self)))
if type(self) != Expr:
return self
-# debug("[%d] A1 = %s" % (self.n,self.a1))
a = self.a1.eval(excl_vars)
b = rename_off(self.a2,V(a)+excl_vars)
-# debug("[%d] A = %s" % (self.n,a))
+ debug("[%d] Arg types: %s, %s" % (self.n, type(a), type(b)))
if self.op=='@' and type(a)==Lambda:
+ debug("[%d] Apply called" % self.n)
e = a.apply(b,excl_vars)
elif self.op=='!' and type(a)==Lambda and type(b)==Const:
e = Lambda(a.var, lambda_pow(a.var,a.expr,b.value))
@@ -337,6 +349,7 @@ class Expr(Term):
global vars
b = self.a2.eval_vars(excl_vars)
a = self.a1.eval_vars(excl_vars + V(b))
+ debug("[%d] (eval_vars) (%s) <%s>, <%s>" % (self.n,self.op,d_show(a),d_show(b)))
e = Expr(self.op,a,b)
if e.op == '@' and type(a)==Lambda:
return a.apply(b,excl_vars)
@@ -351,7 +364,7 @@ class Expr(Term):
return Const(e.a1.value / e.a2.value)
if e.op=='^':
return Const(e.a1.value ** e.a2.value)
-# debug("[%d] Eval_vars: %s" % (self.n,e))
+ debug("[%d] (eval_vars) returning: %s" % (self.n,e))
return e
class Assignment(Term):
@@ -371,6 +384,9 @@ class Assignment(Term):
def eval(self,excl_vars=Set()):
return self
+ def eval_vars(self,excl_vars=Set()):
+ return self
+
class Comma(Term):
"Variable substitution expression, as in: 'sqr z, z=5'."
def __init__(self,expr,assign):
@@ -387,6 +403,9 @@ class Comma(Term):
def eval(self,excl_vars=Set()):
return self.expr.subst(self.assign.var,self.assign.expr).eval()
+
+ def eval_vars(self,excl_vars=Set()):
+ return self.expr.subst(self.assign.var,self.assign.expr).eval()
def save():
global vars
diff --git a/pylambda.py b/pylambda.py
index 39743c7..a93120d 100755
--- a/pylambda.py
+++ b/pylambda.py
@@ -160,7 +160,7 @@ if __name__ == "__main__":
break
if s == "" : continue
try:
- value = yacc.parse(s).eval()
+ value = yacc.parse(s).eval().eval_vars().eta()
print ": %s :: %s" % (value, typeof(value))
set_old_value(value)
except TypeError,e: