[cl-unification-cvs] CVS cl-unification

[mantoniotti]

Update of /project/cl-unification/cvsroot/cl-unification
In directory cl-net:/tmp/cvs-serv18091

Modified Files:
	unifier.lisp 
Log Message:
After a careful reading of PAIP fixed a very subtle bug in VAR-UNIFY
that prevented the correct unification of:

    (?x ?y a)

with
	
    (?y ?x ?x)


--- /project/cl-unification/cvsroot/cl-unification/unifier.lisp	2009/12/17 16:44:46	1.7
+++ /project/cl-unification/cvsroot/cl-unification/unifier.lisp	2011/01/18 14:50:17	1.8
@@ -880,6 +880,8 @@
 
 (defgeneric occurs-in-p (var pat env))
 
+
+#+old-version-no-paip
 (defun var-unify (var pat env)
   (if (eq var pat)
       env
@@ -896,6 +898,33 @@
                (extend-environment var pat env))))))
 
 
+;;; Version with PAIP test.
+
+(defun var-unify (var pat env)
+  (if (eq var pat)
+      env
+      (multiple-value-bind (value foundp)
+          (find-variable-value var env)
+
+        (cond (foundp
+               (unify value pat env))
+              ((variablep pat)
+               (multiple-value-bind (pat-value foundp)
+                   (find-variable-value pat env)
+                 (if foundp
+                     (return-from var-unify
+                       (unify var pat-value env)))
+                 )))
+
+        (cond ((and *occurrence-check-p*
+                    (occurs-in-p var pat env))
+               (error 'unification-failure
+                      :format-control "Variable ~S occurs in ~S."
+                      :format-arguments (list var pat)))
+              (t
+               (extend-environment var pat env))))))
+
+
 
 #||
 (defmethod occurs-in-p ((var symbol) pat env)