From 79eb7c741e868a50d6a9e1402a88986a9e387bb7 Mon Sep 17 00:00:00 2001
From: portnov <portnov>
Date: Mon, 2 Jun 2008 04:55:30 +0000
Subject: [PATCH] Do eta-reduction only as last phase, after eval(). This fixes some bugs.

---
 data2.py    |   43 +++++++++++++++++++++++++++++++------------
 pylambda.py |    2 +-
 2 files changed, 32 insertions(+), 13 deletions(-)

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:
-- 
1.7.2.3