[pypy-svn] r22419 - pypy/dist/pypy/lib/logic
nico at codespeak.net
nico at codespeak.net
Thu Jan 19 11:30:42 CET 2006
Author: nico
Date: Thu Jan 19 11:30:40 2006
New Revision: 22419
Added:
pypy/dist/pypy/lib/logic/
pypy/dist/pypy/lib/logic/test_unification.py
pypy/dist/pypy/lib/logic/unification.py
Log:
preliminary work on implementing a oz-like variable store
Added: pypy/dist/pypy/lib/logic/test_unification.py
==============================================================================
--- (empty file)
+++ pypy/dist/pypy/lib/logic/test_unification.py Thu Jan 19 11:30:40 2006
@@ -0,0 +1,85 @@
+import unification as u
+from py.test import raises, skip
+
+class TestUnification:
+
+ def setup_method(self, meth):
+ u._store = u.Store()
+
+ def test_bind_var_var(self):
+ x = u.var('x')
+ y = u.var('y')
+ z = u.var('z')
+ u.bind(x, z)
+ assert u._store.unbound == set([u.EqSet([y]),
+ u.EqSet([x,z])])
+ assert u.bound() == []
+
+ def test_bind_var_val(self):
+ y = u.var('y')
+ u.bind(y, 42)
+ assert u.unbound() == []
+ assert u._store.bound == {y:42}
+ x = u.var('x')
+ z = u.var('z')
+ u.bind(x, z)
+ u.bind(z, 3.14)
+ assert u.unbound() == []
+ assert u._store.bound == {x:3.14, y:42, z:3.14}
+
+ def test_already_in_store(self):
+ x = u.var('x')
+ raises(u.AlreadyInStore, u.var, 'x')
+
+ def test_already_bound(self):
+ x = u.var('x')
+ u.bind(x, 42)
+ raises(u.AlreadyBound, u.bind, x, 42)
+
+ def test_unify_lists_success(self):
+ x,y,z,w = (u.var('x'), u.var('y'),
+ u.var('z'), u.var('w'))
+ u.bind(x, [42, z])
+ u.bind(y, [w, 44])
+ u.unify(x, y)
+ assert u._store.bound == {y: [w, 44], x: [42, z],
+ z: 44, w: 42}
+
+ def test_unify_dicts_success(self):
+ x,y,z,w = (u.var('x'), u.var('y'),
+ u.var('z'), u.var('w'))
+ u.bind(x, {1:42, 2:z})
+ u.bind(y, {1:w, 2:44})
+ u.unify(x, y)
+ assert u._store.bound == {y: {1:w, 2:44},
+ x: {1:42, 2:z},
+ z: 44, w: 42}
+
+ def test_unify_failure(self):
+ x,y,z = u.var('x'), u.var('y'), u.var('z')
+ u.bind(x, [42, z])
+ u.bind(y, [z, 44])
+ raises(u.UnificationFailure, u.unify, x, y)
+
+ def test_unify_failure2(self):
+ x,y,z,w = (u.var('x'), u.var('y'),
+ u.var('z'), u.var('w'))
+ u.bind(x, [42, z])
+ u.bind(y, [w, 44])
+ u.bind(z, w)
+ raises(u.UnificationFailure, u.unify, x, y)
+
+ def test_unify_circular(self):
+ x, y, z, w, a, b = (u.var('x'), u.var('y'),
+ u.var('z'), u.var('w'),
+ u.var('a'), u.var('b'))
+ u.bind(x, [y])
+ u.bind(y, [x])
+ raises(u.Circularity, u.unify, x, y)
+ u.bind(z, [1, w])
+ u.bind(w, [z, 2])
+ raises(u.UnificationFailure, u.unify, z, w)
+ u.bind(a, {1:42, 2:b})
+ u.bind(b, {1:a, 2:42})
+ raises(u.UnificationFailure, u.unify, a, b)
+
Added: pypy/dist/pypy/lib/logic/unification.py
==============================================================================
--- (empty file)
+++ pypy/dist/pypy/lib/logic/unification.py Thu Jan 19 11:30:40 2006
@@ -0,0 +1,285 @@
+# Oz unification in Python 2.4
+# within a single assignment store
+# crude and buggy ...
+
+#TODO :
+# * ensure that the store is intact after a failure
+# (maybe with some anti-bind ops)
+# * provide a way to copy the store to a fresh one
+# (clone operator)
+# After reading more of the "book", I see some more ops
+# are needed for the store to be part of a computation
+# space ...
+
+#----------- Variables ----------------------------------
+class EqSet(frozenset):
+ """An equivalence set for variables"""
+ pass
+
+class Var(object):
+
+ def __init__(self, name, store):
+ self.name = name
+ self.store = store
+ store.add_unbound(self)
+
+ def __str__(self):
+ if self in self.store.bound.keys():
+ return "%s = %s" % (self.name,
+ self.store.bound[self])
+ return "%s" % self.name
+
+ def __repr__(self):
+ return self.__str__()
+
+ def __eq__(self, thing):
+ return type(thing) == Var and self.name == thing.name
+
+ def __hash__(self):
+ return self.name.__hash__()
+
+def var(name):
+ return Var(name, _store)
+
+#----------- Store Exceptions ----------------------------
+class VariableException(Exception):
+ def __init__(self, name):
+ self.name = name
+
+class UnboundVariable(VariableException):
+ def __str__(self):
+ return "%s has no value yet" % self.name
+
+class AlreadyBound(VariableException):
+ def __str__(self):
+ return "%s is already bound" % self.name
+
+class AlreadyInStore(VariableException):
+ def __str__(self):
+ return "%s already in store" % self.name
+
+class UnificationFailure(Exception):
+ def __init__(self, var1, var2):
+ self.var1, self.var2 = (var1, var2)
+ def __str__(self):
+ return "%s %s can't be unified" % (self.var1,
+ self.var2)
+
+class Circularity(UnificationFailure):
+ def __str__(self):
+ return "cycle : % %s not unifiable" % (self.var1,
+ self.var2)
+
+#----------- Variable Exceptions-------------------------
+class NotAVariable(VariableException):
+ def __str__(self):
+ return "%s is not a variable" % self.name
+
+#----------- Store ------------------------------------
+class Store(object):
+ """The Store consists of a set of k variables
+ x1,...,xk that are partitioned as follows:
+ * set of unbound variables that are equal
+ (also called equivalence sets of variables).
+ The variables in each set are equal to each
+ other but not to any other variables.
+ * variables bound to a number, record or procedure
+ (also called determined variables)."""
+
+ def __init__(self):
+ # set of all known vars
+ # var->equivalence set mapping for unbound vars
+ # set of equisets (clusters of unbound variables)
+ # var->objects bindings
+ self.vars = set()
+ self.equisets = {}
+ self.unbound = set()
+ self.bound = {}
+ # memoizer for unify (avoids infinite loops when
+ # one wants to unify vars with cycles)
+ self.unify_memo = set()
+
+ def add_unbound(self, var):
+ # register globally
+ if var in self.vars:
+ raise AlreadyInStore(var.name)
+ print "adding %s to the store" % var
+ self.vars.add(var)
+ # put into new singleton equiv. set
+ eqset = EqSet([var])
+ self.equisets[var] = eqset
+ self.unbound.add(eqset)
+
+ #-- BIND -------------------------------------------
+
+ def bind(self, var, val):
+ """1. (unbound)Variable/(unbound)Variable or
+ 2. (unbound)Variable/(bound)Variable or
+ 3. (unbound)Variable/Value binding
+ """
+ assert(isinstance(var, Var) and (var in self.vars))
+ if var == val:
+ return
+ if self._both_are_vars(var, val):
+ if self._both_are_bound(var, val):
+ raise AlreadyBound(var.name)
+ if self.bound.has_key(var): # 2.
+ self.bind(val, var)
+ elif self.bound.has_key(val): # 2.
+ self._bind(self.equisets[var],
+ self.bound[val])
+ else: # 1.
+ self._merge(self.equisets[var],
+ self.equisets[val])
+ else: # 3.
+ if self.bound.has_key(var):
+ raise AlreadyBound(var.name)
+ self._bind(self.equisets[var], val)
+
+ def _both_are_vars(self, v1, v2):
+ try:
+ return v1 in self.vars and v2 in self.vars
+ except:
+ return False
+
+ def _both_are_bound(self, v1, v2):
+ return self.bound.has_key(v1) and \
+ self.bound.has_key(v2)
+
+ def _bind(self, eqs, val):
+ print "variable - value binding : %s %s" % (eqs, val)
+ # bind all vars in the eqset to obj
+ for name in eqs:
+ del self.equisets[name]
+ self.bound[name] = val
+ self.unbound.remove(eqs)
+
+ def _merge(self, eqs1, eqs2):
+ print "unbound variables binding : %s %s" % (eqs1, eqs2)
+ if eqs1 == eqs2: return
+ # merge two equisets into one
+ neweqs = eqs1 | eqs2
+ # let's reassign everybody to eqs1
+ for name in neweqs:
+ self.equisets[name] = neweqs
+ self.unbound.remove(eqs1)
+ self.unbound.remove(eqs2)
+ self.unbound.add(neweqs)
+
+ #-- UNIFY ------------------------------------------
+
+ def unify(self, x, y):
+ #FIXME in case of failure, the store state is not
+ # properly restored ...
+ print "unify %s with %s" % (x,y)
+ # do the memoization work
+ if (x,y) in self.unify_memo: raise Circularity(x,y)
+ self.unify_memo.add((x, y))
+ # dispatch to the apropriate unifier
+ try:
+ if x not in self.bound and y not in self.bound:
+ if x != y:
+ if type(x) is Var:
+ self.bind(x,y)
+ else:
+ self.bind(y,x)
+ elif x in self.bound and y in self.bound:
+ self._unify_bound(x,y)
+ elif x in self.bound:
+ self.bind(x,y)
+ else:
+ self.bind(y,x)
+ except AlreadyBound:
+ raise UnificationFailure(x, y)
+
+ def _unify_bound(self, x, y):
+ print "unify bound %s %s" % (x, y)
+ vx, vy = (self.bound[x], self.bound[y])
+ if not _unifiable(vx, vy): raise UnificationFailure(x, y)
+ elif type(vx) in [list, set] and isinstance(vy, type(vx)):
+ self._unify_iterable(x, y)
+ elif type(vx) is dict and isinstance(vy, type(vx)):
+ self._unify_mapping(x, y)
+ else:
+ raise UnificationFailure(x, y)
+
+ def _unify_iterable(self, x, y):
+ print "unify sequences %s %s" % (x, y)
+ vx, vy = (self.bound[x], self.bound[y])
+ idx, top = (0, len(vx))
+ while (idx < top):
+ self.unify(vx[idx], vy[idx])
+ idx += 1
+
+ def _unify_mapping(self, x, y):
+ print "unify mappings %s %s" % (x, y)
+ vx, vy = (self.bound[x], self.bound[y])
+ for xk in vx.keys():
+ self.unify(vx[xk], vy[xk])
+
+#-- Unifiability checks---------------------------------------
+#--
+#-- quite costly & could be merged back in unify
+#-- FIXME : memoize _iterable
+
+def _iterable(thing):
+ return type(thing) in [list, set]
+
+def _mapping(thing):
+ return type(thing) is dict
+
+def _unifiable(term1, term2):
+ """Checks wether two terms can be unified"""
+ print "unifiable ? %s %s" % (term1, term2)
+ if _iterable(term1):
+ if _iterable(term2):
+ return _iter_unifiable(term1, term2)
+ return False
+ if _mapping(term1) and _mapping(term2):
+ return _mapping_unifiable(term1, term2)
+ if not(isinstance(term1, Var) or isinstance(term2, Var)):
+ return term1 == term2 # same 'atomic' object
+ return True
+
+def _iter_unifiable(c1, c2):
+ """Checks wether two iterables can be unified"""
+ print "unifiable sequences ? %s %s" % (c1, c2)
+ if len(c1) != len(c2): return False
+ idx, top = (0, len(c1))
+ while(idx < top):
+ if not _unifiable(c1[idx], c2[idx]):
+ return False
+ idx += 1
+ return True
+
+def _mapping_unifiable(m1, m2):
+ """Checks wether two mappings can be unified"""
+ print "unifiable mappings ? %s %s" % (m1, m2)
+ if len(m1) != len(m2): return False
+ if m1.keys() != m2.keys(): return False
+ v1, v2 = (m1.items(), m2.items())
+ v1.sort()
+ v2.sort()
+ return _iter_unifiable([e[1] for e in v1],
+ [e[1] for e in v2])
+
+#-- Some utilities -----------------------------------------------
+#--
+#-- the global store
+_store = Store()
+
+#-- global accessor functions
+def bind(var, val):
+ return _store.bind(var, val)
+
+def unify(var1, var2):
+ return _store.unify(var1, var2)
+
+def bound():
+ return _store.bound.keys()
+
+def unbound():
+ res = []
+ for cluster in _store.unbound:
+ res.append('='.join([str(var) for var in cluster]))
+ return res
More information about the Pypy-commit
mailing list