;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Unification
;;; This code is borrowed from "Paradigms of AI Programming: Case Studies
;;; in Common Lisp", by Peter Norvig, published by Morgan Kaufmann, 1992.
;;; The complete code from that book is available for ftp at mkp.com in
;;; the directory "pub/Norvig".

;;;  Converted to Scheme by Tomas Lozano-Perez (MIT)

;;;; Top Level Functions

;;; See if x and y match with given bindings.  If they do,
;;; return a binding list that would make them equal? [p 303].

(define (unify x y)
  (unify-loop x y  *no-bindings*))

(define (unify-loop x y bindings)
  (cond ((eq? bindings *fail*) *fail*)
	((eqv? x y) bindings)
	((variable? x) (unify-var x y bindings))
	((variable? y) (unify-var y x bindings))
	((and (pair? x) (pair? y))
	 (unify-loop (rest x) (rest y) 
		     (unify-loop (first x) (first y) bindings)))
	(else *fail*)))

;;;; Auxiliary Functions

;;; Unify var with x, using (and maybe extending) bindings [p 303].
(define (unify-var var x bindings)
  (cond ((get-binding var bindings)
         (unify-loop (lookup var bindings) x bindings))
        ((and (variable? x) (get-binding x bindings))
         (unify-loop var (lookup x bindings) bindings))
        ((occurs-in? var x bindings)
         *fail*)
        (else (extend-bindings var x bindings))))

;;; Does var occur anywhere inside x?"
(define (occurs-in? var x bindings)
  (cond ((eq? var x) #t)
        ((and (variable? x) (get-binding x bindings))
         (occurs-in? var (lookup x bindings) bindings))
        ((pair? x) (or (occurs-in? var (first x) bindings)
                       (occurs-in? var (rest x) bindings)))
        (else #f)))

;;; Return something that unifies with both x and y (or fail).
(define (unifier x y)
 (subst-bindings (unify x y) x))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;