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)