UNIFY-4: Fixed false unification on seqs of differing lengths

Author: fogus

pom.xml

@@ -18,7 +18,7 @@
   <parent>
     <groupId>org.clojure</groupId>
     <artifactId>pom.contrib</artifactId>
-    <version>0.0.25</version>
+    <version>0.0.26</version>
   </parent>
 
   <developers>

src/main/clojure/clojure/core/unify.clj

@@ -50,11 +50,13 @@
 
 (defn- bind-phase
   [binds variable expr]
-  (if (ignore-variable? variable)
+  (if (or (nil? expr)
+          (ignore-variable? variable))
     binds
     (assoc binds variable expr)))
 
-(defn- determine-occursness [want-occurs? variable? v expr binds]
+(defn- determine-occursness
+  [want-occurs? variable? v expr binds]
   (if want-occurs?
     `(if (occurs? ~variable? ~v ~expr ~binds)
        (throw (IllegalStateException. (str "Cycle found in the path " ~expr)))
@@ -63,11 +65,10 @@
 
 (defmacro create-var-unification-fn
   [want-occurs?]
-  (let [varp  'varp ;;(gensym)
-        v     'v ;;(gensym)
-        expr  'expr ;;(gensym)
-        binds 'binds ;;(gensym)
-        ]
+  (let [varp  (gensym)
+        v     (gensym)
+        expr  (gensym)
+        binds (gensym)]
     `(fn var-unify
        [~varp ~v ~expr ~binds]
        (if-let [vb# (~binds ~v)] 
@@ -128,6 +129,7 @@
 (defn- try-subst
   "Attempts to substitute the bindings in the appropriate locations in the given expression."
   [variable? x binds]
+  {:pre [(map? binds) (fn? variable?)]}
   (walk/prewalk (fn [expr] 
                   (if (variable? expr)
                     (or (binds expr) expr) 

src/test/clojure/clojure/core/unify/tests.clj

@@ -40,15 +40,6 @@
   (is (= '{Bar 2, Foo 1}                   (#'clojure.core.unify/garner-unifiers CAPS '(Foo Bar) '(1 2))))
   (is (= '{?y a, ?x ?y}                    (#'clojure.core.unify/garner-unifiers '(?x ?y a)        '(?y ?x ?x)))))
 
-(deftest test-norvig-bug-cases
-  (testing "that the unification of the problem cases in Norvig's paper
-            'Correcting A Widespread Error in Unification Algorithms'. An
-            incorrect unifier will return nil or loop forever."
-    (is (= '{?x ?y}                        (unify '(p ?x ?y) '(p ?y ?x))))
-    (is (= '{?y a, ?x ?y}                  (unify '(p ?x ?y a) '(p ?y ?x ?x))))
-    ;; higher-order predicates!
-    (is (= '{?x ?y, ?z (p ?x ?y)}          (unify '(q (p ?x ?y) (p ?y ?x)) '(q ?z ?z))))))
-
 (deftest test-range-variables
   (is (= '{?x 1 ?y (2 3)}                  (#'clojure.core.unify/garner-unifiers '(?x & ?y) [1 2 3])))
   (is (= '{?x 1 ?y 2 ?z (3)}               (#'clojure.core.unify/garner-unifiers '(?x ?y & ?z) [1 2 3])))
@@ -69,25 +60,37 @@
   (is (= '(a a a)                          (#'clojure.core.unify/unifier* CAPS '(X Y a) '(Y X X))))
   (is (= '((?a * 5 ** 2) + (4 * 5) + 3)    (#'clojure.core.unify/unifier* '((?a * ?x ** 2) + (?b * ?x) + ?c) '(?z + (4 * 5) + 3)))))
 
-
 (deftest test-unifier
   (is (= '((?a * 5 ** 2) + (4 * 5) + 3)    (#'clojure.core.unify/unifier '((?a * ?x ** 2) + (?b * ?x) + ?c) '(?z + (4 * 5) + 3))))
   (is (= 42                                (#'clojure.core.unify/unifier '?x 42)))
   (is (= '{a 2}                            (#'clojure.core.unify/unifier (hash-map 'a '?x) (hash-map 'a 2))))
   (is (= #{2 3 4}                          (#'clojure.core.unify/unifier #{'?a '?b '?c} #{2 3 4}))))
 
-
 (deftest test-unifier-no-occurs
   (is (= '((?a * 5 ** 2) + (4 * 5) + 3)    (#'clojure.core.unify/unifier- '((?a * ?x ** 2) + (?b * ?x) + ?c) '(?z + (4 * 5) + 3))))
   (is (= 42                                (#'clojure.core.unify/unifier- '?x 42)))
   (is (= '{a 2}                            (#'clojure.core.unify/unifier- (hash-map 'a '?x) (hash-map 'a 2))))
   (is (= #{2 3 4}                          (#'clojure.core.unify/unifier- #{'?a '?b '?c} #{2 3 4}))))
 
-
 (deftest test-mk-unifier
   (let [u (#'clojure.core.unify/make-occurs-unifier-fn #(and (symbol? %) 
                                                              (re-matches #"^\?.*" (name %))))]
     (is (= '((?a * 5 ** 2) + (4 * 5) + 3)  (u '((?a * ?x ** 2) + (?b * ?x) + ?c) '(?z + (4 * 5) + 3))))))
 
 (deftest test-aux
   (is (#'clojure.core.unify/composite? "foo")))
+
+(deftest test-norvig-bug-cases
+  (testing "that the unification of the problem cases in Norvig's paper
+            'Correcting A Widespread Error in Unification Algorithms'. An
+            incorrect unifier will return nil or loop forever."
+    (is (= '{?x ?y}                        (unify '(p ?x ?y) '(p ?y ?x))))
+    (is (= '{?y a, ?x ?y}                  (unify '(p ?x ?y a) '(p ?y ?x ?x))))
+    ;; higher-order predicates!
+    (is (= '{?x ?y, ?z (p ?x ?y)}          (unify '(q (p ?x ?y) (p ?y ?x)) '(q ?z ?z))))))
+
+(deftest regressions
+  (testing "That seqs of different lengths do not unify per UNIFY-4"
+    (is (= {} (unify '[1 ?x] '[1])))
+    (is (= {} (unify '[1 ?x ?y ?z] '[1])))))
+