Add difference_list type as required by issue #3.

src/Makefile

@@ -1,12 +1,13 @@
 
 PYTHON = python3.6
 
-mclock:
-	$(PYTHON) -m unittest -v mclock_test.py
 
 difference_structures:
 	$(PYTHON) -m unittest -v difference_structures_test.py
 
+mclock:
+	$(PYTHON) -m unittest -v mclock_test.py
+
 muk:
 	$(PYTHON) -m unittest -v microkanren_test.py
 

src/difference_structures_test.py

@@ -8,6 +8,7 @@ class difference_structures_test(unittest.TestCase):
 
     def test_extend_list(self):
         self.assertEqual(run(fresh(lambda α: unify([]+α, []))), [[]])
+        self.assertEqual(run(fresh(lambda β, α: unify([]+α, β))), [[]+rvar(0)])
         self.assertEqual(run(fresh(lambda α: unify([1, 2, 3]+α, [1,2]))), [])
         self.assertEqual(run(fresh(lambda α: unify([1, 2, 3]+α, [1,2,3]))), [[]])
         self.assertEqual(run(fresh(lambda α: unify([1, 2, 3]+α, [1,2,3,4,5,6,7]))), [[4,5,6,7]])
@@ -16,3 +17,56 @@ def test_extend_list(self):
         self.assertEqual(run(fresh(lambda out, α, β: unify([1, 2, 3]+α, [1,2,3,4,5]+β) & 
                                                      unify(β, [6,7,8]) &
                                                      unify([α, β], out))), [[[4,5,6,7,8], [6,7,8]]])
+        self.assertEqual(run(fresh(lambda X, Y, α, β, : 
+                                                    unify([1,2,3]+α, X) & 
+                                                    unify([4,5,6]+β, Y) & 
+                                                    unify(α, Y))), [[1,2,3,4,5,6]+rvar(0)])
+
+    def test_difference_list(self):
+        self.assertEqual(run(fresh(lambda out, α: unify(α - α, out))), [ [] ]) # the null difference list
+        self.assertEqual(run(fresh(lambda out, α: unify(([]+α) - α, out))), [ ([]+rvar(0))-rvar(0) ]) # the null difference list
+        self.assertEqual(run(fresh(lambda β, α: unify(([1,2,3]+α)-α, β))), [([1,2,3]+rvar(0))-rvar(0)])
+        self.assertEqual(run(fresh(lambda β, α: rectify(([1,2,3]+α)-α, β))), [ [1,2,3] ])
+        self.assertEqual(run(fresh(lambda α: unify(([1,2,3]+α)-α, [1,2,3]))), [rvar(0)])
+        self.assertEqual(run(fresh(lambda α: unify(([1,2,3]+α)-α, [1,2]))), [])
+        self.assertEqual(run(fresh(lambda α: unify(([1,2,3]+α)-α, [1,2,3,4]))), [])
+        self.assertEqual(run(fresh(lambda β, α: unify(([1,2,3]+α)-α, [1,2,3]+β))), [[]])
+        self.assertEqual(run(fresh(lambda α, β: unify(([1,2,3]+α)-α, [1,2,3]+β))), [rvar(0)]) 
+        self.assertEqual(run(fresh(lambda β, α: unify(([1,2,3]+α)-α, [1,2,3,4]+β))), [])
+        self.assertEqual(run(fresh(lambda β, α: unify(([1,2,3]+α)-α, [1,2]+β))), [[3]])
+        self.assertEqual(run(fresh(lambda α, β: unify(([1,2,3]+α)-α, [1,2]+β))), [rvar(0)])
+        self.assertEqual(run(fresh(lambda out, X, Y, x, y, α, β, : 
+                                                    unify([1,2,3]+α, x) & unify(x-α, X) &
+                                                    unify([4,5,6]+β, y) & unify(y-β, Y) &
+                                                    unify(x-β, out))), [([1,2,3]+rvar(0))-rvar(1)])
+        self.assertEqual(run(fresh(lambda out, X, Y, x, y, α, β, : 
+                                                    unify([1,2,3]+α, x) & unify(x-α, X) &
+                                                    unify([4,5,6]+β, y) & unify(y-β, Y) &
+                                                    unify(α, y) &
+                                                    unify(x-β, out))), [([1,2,3,4,5,6]+rvar(0))-rvar(0)])
+        self.assertEqual(run(fresh(lambda out, X, Y, x, y, α, β, : 
+                                                    unify([1,2,3]+α, x) & unify(x-α, X) &
+                                                    unify([4,5,6]+β, y) & unify(α-β, Y) &
+                                                    unify(x-β, out))), [([1,2,3]+rvar(0))-rvar(1)])
+        self.assertEqual(run(fresh(lambda out, X, Y, x, α, β, : 
+                                                    unify([1,2,3]+α, x) & unify(x-α, X) &
+                                                    unify([4,5,6]+β, α) & unify(α-β, Y) &
+                                                    unify(x-β, out))), [([1,2,3,4,5,6]+rvar(0))-rvar(0)])
+
+
+    def test_appendo(self):
+
+        def appendo(X, Y, XY):
+            return fresh(lambda α, β, γ: unify(X, α-β) & unify(Y, β-γ) & unify(XY, α-γ))
+
+        self.assertEqual(run(fresh(lambda αβ, α, β: appendo(([1,2,3]+α)-α, ([4,5,6]+β)-β, αβ))), 
+                         [([1,2,3,4,5,6]+rvar(0))-rvar(0)])
+        self.assertEqual(run(fresh(lambda out, X, Y, α, β:  appendo(([1,2,3]+α)-α, ([4,5,6]+β)-β, X-Y) & 
+                                                            unify([X, Y], out))), 
+                         [[[1, 2, 3, 4, 5, 6] + rvar(0), rvar(0)]])
+        self.assertEqual(run(fresh(lambda αβ, α, β: appendo(([i for i in range(1000)]+α)-α, ([-1]+β)-β, αβ))), 
+                        [])
+
+
+
+

src/muk/core.py

@@ -63,9 +63,15 @@ def as_cons(self, translate):
         return translate(tuple(self.prefix + [self.var]))
 
     def walk_star(self, W):
-        prefix = foldr(lambda c, acc: [W(c)]+acc, self.prefix, [])
-        walked_var = W(self.var)
-        return prefix + walked_var if isinstance(walked_var, list) else extend_list(prefix, walked_var)
+        prefix = W(self.prefix) # foldr(lambda c, acc: [W(c)]+acc, self.prefix, [])
+        walked = W(self.var)
+
+        if isinstance(walked, extend_list):
+            return extend_list(prefix + walked.prefix, walked.var)
+        if isinstance(walked, list):
+            return prefix + walked  
+        else:
+            return extend_list(prefix, walked)
 
     def unification(self, other, sub, ext_s, U, E):
         try: 
@@ -100,12 +106,24 @@ def _unification_extend_list(self, other, sub, ext_s, U):
             sub_prefix = U(other.prefix, self.prefix, sub, ext_s)
             return U(other.var, self.var, sub_prefix, ext_s)
 
+    def _unification_difference_list(self, other, sub, ext_s, U):
+        return other.whole._unification_prefix_extend_list(self, sub, ext_s, U)
+
+    def _unification_prefix_extend_list(self, other, sub, ext_s, U):
+        return U(self.prefix, other, sub, ext_s)
+
+    def _unification_exclude(self, other, exclude, sub, ext_s, U):
+        if exclude == self.var:
+            return U(self.prefix, other, sub, ext_s)
+
+        raise NotImplemented
+
     def reify_s(self, sub, R):
         sub_prefix = foldr(lambda c, sub: R(c, sub), self.prefix, sub)
         return R(self.var, sub_prefix) 
 
     def occur_check(self, u, O, E):
-        for c in self.prefix: 
+        for c in self.prefix:
             O(u, c)
         return O(u, self.var)
 
@@ -126,6 +144,65 @@ def __radd__(self, other):
 
         raise NotImplemented
 
+    def __sub__(self, other):
+        if isinstance(other, var):
+            return difference_list(whole=self, suffix=other)
+
+        raise NotImplemented
+
+
+
+class difference_list:
+
+    def __init__(self, whole, suffix):
+        self.whole = whole
+        self.suffix = suffix
+
+    def walk_star(self, W):
+        whole = W(self.whole)
+        suffix = W(self.suffix)
+        return [] if whole == suffix else difference_list(whole, suffix)
+
+    def unification(self, other, sub, ext_s, U, E):
+        try: 
+            UDL = other._unification_difference_list
+        except AttributeError:
+            if isinstance(other, list):
+                try: UP = self.whole._unification_exclude
+                except AttributeError: raise E
+                else: return UP(other, self.suffix, sub, ext_s, U)
+            else:
+                raise E
+        else: 
+            return UDL(self, sub, ext_s, U)
+
+    def _unification_difference_list(self, other, sub, ext_s, U):
+        sub_whole = U(other.whole, self.whole, sub, ext_s)
+        return U(other.suffix, self.suffix, sub_whole, ext_s)
+
+    def reify_s(self, sub, R):
+        sub_whole = R(self.whole, sub)
+        return R(self.suffix, sub_whole)
+
+    def occur_check(self, u, O, E):
+        raise NotImplemented
+
+        for c in self.prefix: 
+            O(u, c)
+        return O(u, self.var)
+
+    def __eq__(self, other):
+        try: eq = other.__eq__difference_list
+        except AttributeError: return False
+        else: return eq(self)
+
+    def __eq__difference_list(self, other):
+        return self.whole == other.whole and self.suffix == other.suffix
+
+    def __repr__(self):
+        return '({}) - {}'.format(repr(self.whole), repr(self.suffix))
+
+
 # }}}
 
 # VARS {{{
@@ -161,6 +238,13 @@ def __radd__(self, other):
 
         raise NotImplemented
 
+    def __sub__(self, other):
+
+        if isinstance(other, (list, var)): 
+            return difference_list(whole=self, suffix=other)
+
+        raise NotImplemented
+
     def walk_star(self, W):
         return self
 
@@ -251,8 +335,8 @@ def walk(u, sub):
 
 def walk_star(v, sub):
     v = walk(v, sub)
-    if isinstance(v, list): return [walk_star(u, sub) for u in v]  
-    elif hasattr(v, 'walk_star'): return v.walk_star(lambda u: walk_star(u, sub))
+    if hasattr(v, 'walk_star'): return v.walk_star(lambda u: walk_star(u, sub))
+    elif isinstance(v, (list, tuple)): return [walk_star(u, sub) for u in v]  
     else: return v
 
 class OccurCheck(ValueError):

src/muk/ext.py

@@ -185,3 +185,5 @@ def recv(*args):
 def lvars(vars_names, splitter=' '):
     return [var(b, n.strip()) for b, n in enumerate(vars_names.split(splitter))]
 
+def rectify(α_α, β):
+    return unify(α_α, β-[])

src/muk/sexp.py

@@ -43,7 +43,10 @@ class ImproperListError(ValueError):
 def list_to_cons(l, post=identity):
 
     if isinstance(l, (str, cons)): return l # we consider a `str` obj not an iterable obj but as an atom
-    elif hasattr(l, 'as_cons'): return l.as_cons(list_to_cons)
+
+    try: as_cons = l.as_cons
+    except AttributeError: pass
+    else: return as_cons(translate=list_to_cons)
 
     λ = type(l) 
     try: