;;; UNIFY - A generalization of equality matching that allows variables in both 
;;; the pattern and the goal.  It returns a bindings list that makes the pattern
;;; equal? to the goal or #f if no set of bindings exist.
;;; (unify '(parent (? x) (? y)) '(parent foo (? z)) (empty-bindings))
;;; => (bindings (y (? z)) (x foo))
;;; This assumes that the variables are "standardized apart", that is, there are 
;;; no coincidental name conflicts.  Same name variables all get the same value:
;;; (unify '(parent (? x) foo) '(parent foo (? x)) (empty-bindings))
;;; => (bindings (x foo))
;;; (unify '(parent (? x) foo) '(parent bar (? x)) (empty-bindings))
;;; => #f

(define (unify pattern goal bindings)
  (cond ((simple-variable? pattern)
	 (unify-variable pattern goal bindings))
	((simple-variable? goal)
	 (unify-variable goal pattern bindings))
	((eq? pattern goal) bindings)
	((and (pair? pattern) (pair? goal))
	 (let* ((result 
		 (unify (first pattern) (first goal) bindings)))
	   (if result
	       (unify (rest pattern) (rest goal) result)
	       #f)))
	(else #f)))

(define (unify-variable variable stuff bindings)
  (let ((variable-value (lookup variable bindings)))
    (if (simple-variable? variable-value)
	(add-binding variable stuff bindings)
	(unify variable-value stuff bindings))))

(define (lookup variable environment)
  (define (loop last-var)
    (let ((binding (find-binding last-var environment)))
      ;; variable is unbound, return it
      (cond ((not binding)		
	     last-var)
	    ;; a value that is not a variable
	    ((not (simple-variable? (binding-value binding))) 
	     (binding-value binding))
	    ;; bound to a variable
	    (else			
	     (loop (binding-value binding))))))
  (loop variable))