diff --git a/data.py b/data.py
index 41859d5..34477df 100644
--- a/data.py
+++ b/data.py
@@ -8,6 +8,64 @@ vars = dict()
varnames = "xyztspqfgabcdehijklmnoruvwABCDEFGHIJKLMNOPQRSTUVWXYZ"
DBFILE = os.path.expanduser("~/.config/pylambda.vars")
+DEBUG = 1
+
+if DEBUG:
+ def debug(s):
+ print s
+else:
+ def debug(s):
+ pass
+
+def multy_lambda(arglist,expr):
+ "Return Lambda(arglist[0],Lambda(arglist[1],...Lambda(arglist[n],expr))..)."
+ if len(arglist) == 1:
+ return Lambda(Var(arglist[0]),expr)
+ else:
+ return Lambda(Var(arglist[0]),multy_lambda(arglist[1:],expr))
+
+def first_var(num,excl_list=[]):
+ n = num
+ while varnames[n] in excl_list:
+ n = n+1
+ return varnames[n]
+
+def nextvar(old):
+ if old.count("'") < 3:
+ n = old + "'"
+ else:
+ o = old[0]
+ i = (varnames.index(o)+1)%len(varnames)
+ n = varnames[i]
+ return n
+
+def FV(obj):
+ return obj.FV()
+
+def V(obj):
+ return obj.V()
+
+def Clos(obj):
+ fv = FV(obj)
+ l = obj
+ for v in fv:
+ l = Lambda(v,l)
+ return l
+
+def CV(obj):
+ return V(obj).difference(FV(obj))
+
+def alpha(obj,app):
+ vs = V(obj)
+ fv = FV(app)
+ vs = vs.union(fv)
+ if type(obj) == Lambda:
+ for v in CV(obj):
+ nv = first_var(0,vs)
+ debug(">> Changing %s for %s in %s" % (v,nv,obj))
+ obj = obj.subst(v.show(), Var(nv))
+ vs.add(nv)
+ return obj
def lambda_pow(var,expr,const):
"Returns right part of (\var.expr^{n})"
@@ -28,6 +86,16 @@ class Expr(object):
self.a1 = a1
self.a2 = a2
+ def __repr__(self):
+ return "<Expr: %s %s %s>" % (self.a1,self.op,self.a2)
+
+ def FV(self):
+ "Set of free variables in this expression."
+ return self.a1.FV().union(self.a2.FV())
+
+ def V(self):
+ return self.a1.V().union(self.a2.V())
+
def show(self):
"String representation of an object."
if self.op == "@":
@@ -47,14 +115,14 @@ class Expr(object):
return self.a1.freeof(name) and self.a2.freeof(name)
def alpha(self,badlist,vlist=[]):
-# print ">> [%d]Expr.Renaming off %s" % (self.number,badlist)
+ debug(">> [%d]Expr.Renaming off %s" % (self.number,badlist))
a = self.a1.alpha(badlist,vlist)
b = self.a2.alpha(badlist,vlist)
return Expr(self.op,a,b)
def apply(self,expr,excl_list=[]):
"Try apply self (as a function) to given Expr."
-# print ">> [%d]Expr.Apply: <%s> to <%s>" % (self.number,self.show(),expr.show())
+ debug(">> [%d]Expr.Apply: <%s> to <%s>" % (self.number,self.show(),expr.show()))
t = self.eval(excl_list)
if isinstance(t,Lambda):
return t.apply(expr.alpha(excl_list),excl_list)
@@ -63,7 +131,7 @@ class Expr(object):
def eval_vars(self,excl_list=[]):
"Evaluate expression and substitute variables values where possible."
-# print ">> [%d]Expr.Eval_vars: <%s> excl_list = %s" % (self.number,self.show(),excl_list)
+ debug(">> [%d]Expr.Eval_vars: <%s> excl_list = %s" % (self.number,self.show(),excl_list))
tmp = self.eval(excl_list)
if isinstance(tmp,Lambda) or isinstance(tmp,Var) or isinstance(tmp,Const) or isinstance(tmp,Null):
return tmp
@@ -91,7 +159,7 @@ class Expr(object):
print "Cannot function-style exponent for constant."
return Null()
else:
- print "Should not reach: unknown operation."
+ debug("Should not reach: unknown operation.")
if self.op == "!":
t = self.a1.eval_vars(excl_list)
if isinstance(self.a2,Const) and isinstance(t,Lambda):
@@ -115,13 +183,13 @@ class Expr(object):
def eval(self,excl_list=[]):
"Evaluate Expr."
-# print ">> [%d]Expr.Eval: <%s> excl_list = %s" % (self.number,self.show(), excl_list)
+ debug(">> [%d]Expr.Eval: <%s> excl_list = %s" % (self.number,self.show(), excl_list))
lt = self.a1.eval(excl_list)
if self.op == "@":
if isinstance(lt,Lambda):
# if isinstance(self.a2,Var) and isinstance(lt,Lambda):
lt = lt.alpha([self.a2.show()])
-# print ">> [%d]Expr.Eval: LT = <%s>" % (self.number,lt.show())
+ debug(">> [%d]Expr.Eval: LT = <%s>" % (self.number,lt.show()))
l = lt.lambda_vars()
e = lt.apply(self.a2.alpha(excl_list,l),excl_list)
return e
@@ -149,6 +217,9 @@ class Assignment(Expr):
self.expr = expr
vars[var.show()] = expr
+ def __repr__(self):
+ return "<Assignment: %s = %s>" % (self.var,self.expr)
+
def show(self):
return "%s = %s" % (self.var.show(),self.expr.show())
@@ -176,7 +247,7 @@ class Comma(Expr):
return Comma(e,self.assign)
def eval_vars(self,excl_list=[]):
-# print ">> Eval_vars: <%s> excl_list = %s" % (self.show(),excl_list)
+ debug(">> Eval_vars: <%s> excl_list = %s" % (self.show(),excl_list))
t = self.expr.eval_vars(excl_list)
return t.subst(self.assign.var.show(),self.assign.expr).eval_vars(excl_list)
@@ -192,33 +263,11 @@ class Null(Expr):
def lambda_vars(self):
return []
def eval_vars(self,excl_list=[]):
-# print ">> Eval_vars: <%s> excl_list = %s" % (self.show(),excl_list)
+ debug(">> Eval_vars: <%s> excl_list = %s" % (self.show(),excl_list))
return self
def eval(self,excl_list=[]):
return self
-def multy_lambda(arglist,expr):
- "Return Lambda(arglist[0],Lambda(arglist[1],...Lambda(arglist[n],expr))..)."
- if len(arglist) == 1:
- return Lambda(Var(arglist[0]),expr)
- else:
- return Lambda(Var(arglist[0]),multy_lambda(arglist[1:],expr))
-
-def first_var(num,excl_list=[]):
- n = num
- while varnames[n] in excl_list:
- n = n+1
- return varnames[n]
-
-def nextvar(old):
- if old.count("'") < 3:
- n = old + "'"
- else:
- o = old[0]
- i = (varnames.index(o)+1)%len(varnames)
- n = varnames[i]
- return n
-
class Lambda(Expr):
"Lambda-expression."
@@ -232,6 +281,15 @@ class Lambda(Expr):
self.var = var
self.expr = expr
+ def __repr__(self):
+ return "<Lambda: %s. %s>" % (self.var,self.expr)
+
+ def FV(self):
+ return self.expr.FV().difference(set([self.var]))
+
+ def V(self):
+ return self.expr.V().union(set([self.var]))
+
def show(self):
return "(λ%s.%s)" % (self.var.show(), self.expr.show())
@@ -244,7 +302,7 @@ class Lambda(Expr):
return self.expr.freeof(name)
def alpha(self, badlist, vlist = []):
-# print ">> [%d]Lambda.Renaming <%s> off %s." % (self.number,self.show(),badlist)
+ debug(">> [%d]Lambda.Renaming <%s> off %s." % (self.number,self.show(),badlist))
o = self.var.show()
s = nextvar(o)
while s in badlist:
@@ -252,49 +310,49 @@ class Lambda(Expr):
b = copy(vlist)
if o in badlist:
v = Var(s)
-# print ">> [%d]Lambda.Rename: renamed <%s> to <%s>." % (self.number,o,s)
+ debug(">> [%d]Lambda.Rename: renamed <%s> to <%s>." % (self.number,o,s))
b.append(o)
e = self.expr.alpha(badlist,b)
r = Lambda(v,e,False)
else:
-# print ">> [%d]Lambda.Rename: will not rename var: my var is <%s>" % (self.number, o)
+ debug(">> [%d]Lambda.Rename: will not rename var: my var is <%s>" % (self.number, o))
e = self.expr.alpha(badlist,b)
# e = self.expr
r = Lambda(self.var,e,False)
-# print ">> [%d]Lambda.Rename result = <%s>" % (self.number,r.show())
+ debug(">> [%d]Lambda.Rename result = <%s>" % (self.number,r.show()))
return r
def subst(self,old,new):
- if self.var.show() != old:
+ if self.var.show() != old and not new in FV(self):
return Lambda(self.var,self.expr.subst(old,new))
else:
- return self
+ return Lambda(new,self.expr.subst(old,new))
def apply(self,expr,excl_list=[]):
-# print ">> [%d]Lambda.Apply Excl_list = %s." % (self.number,excl_list)
+ debug(">> [%d]Lambda.Apply Excl_list = %s." % (self.number,excl_list))
l = self.lambda_vars()
-# print ">> [%d]Lambda.Apply Lambda_vars = %s" % (self.number,l)
+ debug(">> [%d]Lambda.Apply Lambda_vars = %s" % (self.number,l))
q = expr.alpha(l)
e = self.expr.subst(self.var.show(),q)
-# print ">> [%d]Lambda.Apply <%s> to <%s> result: <%s>" % (self.number,self.show(),q.show(),e.show())
+ debug(">> [%d]Lambda.Apply <%s> to <%s> result: <%s>" % (self.number,self.show(),q.show(),e.show()))
return e
def eval_vars(self,excl_list=[]):
-# print ">> Lambda.Eval_vars: <%s> excl_list = %s" % (self.show(),excl_list)
+ debug(">> Lambda.Eval_vars: <%s> excl_list = %s" % (self.show(),excl_list))
l = copy(excl_list)
l.append(self.var.show())
e = self.expr.eval_vars(l).alpha(l)
return Lambda(self.var,e)
def eval(self,excl_list=[]):
-# print ">> [%d]Lambda.Eval: <%s> excl_list = %s" % (self.number,self.show(),excl_list)
+ debug(">> [%d]Lambda.Eval: <%s> excl_list = %s" % (self.number,self.show(),excl_list))
if self.var.show() in excl_list:
t = self.alpha(excl_list)
else:
t = copy(self)
l = copy(excl_list)
l.append(t.var.show())
-# print " > > [ % d]Lambda.Eval: L = % s" % (self.number, l)
+ debug(" > > [ % d]Lambda.Eval: L = % s" % (self.number, l))
# Perform η-reduction
try:
if t.expr.op == "@" and isinstance(t.expr.a2,Var) and not isinstance(t.expr.a2,Const):
@@ -335,6 +393,15 @@ class Var(Expr):
def __init__(self,name):
self.name = name
+ def __repr__(self):
+ return "<Var: %s>" % self.name
+
+ def FV(self):
+ return set([self])
+
+ def V(self):
+ return set([self])
+
def show(self):
return self.name
@@ -352,43 +419,43 @@ class Var(Expr):
def alpha(self,badlist,vlist=[]):
# return self
-# print ">> [%s]Var.Renaming off %s, %s" % (self.name,badlist,vlist)
+ debug(">> [%s]Var.Renaming off %s, %s" % (self.name,badlist,vlist))
if self.name in vlist and not self.name in vars:
o = nextvar(self.name)
while o in vlist+badlist:
o = nextvar(o)
v = Var(o)
-# print ">> [%s]Var.Rename: Lists: %s, %s. Renaming to <%s>" % (self.name,badlist,vlist,o)
+ debug(">> [%s]Var.Rename: Lists: %s, %s. Renaming to <%s>" % (self.name,badlist,vlist,o))
return v
else:
return self
def apply(self,expr,excl_list=[]):
-# print ">> Var.Apply called."
+ debug(">> Var.Apply called.")
return Expr('@',copy(self),expr)
def eval_vars(self,excl_list=[]):
-# print ">> [%s]Var.Eval_vars: excl_list = %s" % (self.show(),excl_list)
+ debug(">> [%s]Var.Eval_vars: excl_list = %s" % (self.show(),excl_list))
if self.name in excl_list:
return Var(self.name)
else:
e = self.eval(excl_list).alpha(excl_list)
-# print ">> Eval_vars: Var <%s> evaluated to <%s>." % (self.name,e.show())
+ debug(">> Eval_vars: Var <%s> evaluated to <%s>." % (self.name,e.show()))
return e
def eval(self,excl_list=[]):
-# print ">> [%s]Var.Eval: excl_list = %s" % (self.show(),excl_list)
+ debug(">> [%s]Var.Eval: excl_list = %s" % (self.show(),excl_list))
if (self.name in vars) and not (self.name in excl_list):
e = vars[self.name].alpha(excl_list)
-# print ">> [%s]Var.Eval: read <%s> from hash" % (self.show(),e.show())
+ debug(">> [%s]Var.Eval: read <%s> from hash" % (self.show(),e.show()))
if isinstance(e,Lambda):
if e.var.show() in excl_list:
-# print ">> [%s]Var.Eval: this is Lambda, creating new Lambda with new var." % self.show()
+ debug(">> [%s]Var.Eval: this is Lambda, creating new Lambda with new var." % self.show())
e = Lambda(e.var,e.expr.alpha(excl_list),True,excl_list)
-# print ">> -------"
+ debug(">> -------")
else:
e = copy(self)
-# print ">> Var.Eval: Var <%s> evaluated to <%s>." % (self.name,e.show())
+ debug(">> Var.Eval: Var <%s> evaluated to <%s>." % (self.name,e.show()))
return e
class Const(Var):
@@ -396,6 +463,15 @@ class Const(Var):
def __init__(self,num):
self.num = num
+ def __repr__(self):
+ return "<Const: %s>" % self.num
+
+ def FV(self):
+ return set()
+
+ def V(self):
+ return set()
+
def show(self):
return str(self.num)
@@ -409,7 +485,7 @@ class Const(Var):
return copy(self)
def eval_vars(self,excl_list=[]):
-# print ">> Eval_vars: <%s> excl_list = %s" % (self.show(),excl_list)
+ debug(">> Eval_vars: <%s> excl_list = %s" % (self.show(),excl_list))
return copy(self)
def apply(self,expr,excl_list=[]):
diff --git a/data.pyc b/data.pyc
index ccd78c2..48cdfc6 100644
Binary files a/data.pyc and b/data.pyc differ
diff --git a/lambdalex.pyc b/lambdalex.pyc
index fe31504..e10913b 100644
Binary files a/lambdalex.pyc and b/lambdalex.pyc differ
diff --git a/parsetab.pyc b/parsetab.pyc
index c8fcfa9..ecadf81 100644
Binary files a/parsetab.pyc and b/parsetab.pyc differ
diff --git a/pylambda.py b/pylambda.py
index f01adeb..941f1c1 100755
--- a/pylambda.py
+++ b/pylambda.py
@@ -7,7 +7,7 @@ from ply import yacc
from lambdalex import tokens
# from data import Assignment,Comma,Expr,Lambda,Var,Const,multy_lambda,typeof,load,save,show_vars
-from data import *
+from data2 import *
precedence = (
('left','EQ'),
@@ -32,7 +32,7 @@ def p_generic_assign(t):
def p_assignment(t):
'assignment : VAR EQ expr'
- if not t[3].freeof(t[1]):
+ if Var(t[1]) in FV(t[3]):
print "Warning: recursive assignment."
t[0]= Assignment(Var(t[1]),t[3])
@@ -160,8 +160,8 @@ if __name__ == "__main__":
break
if s == "" : continue
try:
- value = yacc.parse(s).eval().eval_vars()
- print ": %s :: %s" % (value.show(), typeof(value))
+ value = yacc.parse(s).eval().eval()
+ print ": %s :: %s" % (value, typeof(value))
set_old_value(value)
except TypeError,e:
print e