;;; VARIABLE BINDING FUNCTIONS

(define (unify p1 p2  bindings)
  ;;;
  ;;; Makes sure that two patterns, possibly both containing variables
  ;;; can be given consistent bindings of the variables
  ;;;
  (cond ((and (atom? p1) (atom? p2))	;Are both arguments atoms?
         (unify-atoms p1 p2 bindings))	;If yes, ok; if no, fail.
        ((simple-variable? p1)		;Is p1 a variable?
         (unify-variable p1 p2 bindings)) ;Unify variable using bindings.
        ((simple-variable? p2)		;Is p2 a variable?
         (unify-variable p2 p1 bindings)) ;Unify variable using bindings.
	((or (atom? p1) (atom? p2))	; atom can't match a list.
	 'fail)
        ((and (list? p1) (list? p2))	;Are both patterns lists?
         (unify-pieces p1 p2 bindings))	;Unify pieces.
        (else 'fail)))

(define (unify-atoms p1 p2 bindings)     ;Identical to MATCH-ATOMS.
  (if (eq? p1 p2) bindings 'fail))

(define (unify-pieces p1 p2 bindings)	;Identical to MATCH-PIECES.
  (let ((result (unify (first p1) (first p2) bindings)))
    (if (eq? 'fail result)
        'fail
        (unify (rest p1) (rest p2) result))))

(define (unify-variable p1 p2 bindings)
  (let ((binding (find-binding p1 bindings))) ;Find binding, if any.
    (if binding				;Is there a binding?
        (unify (extract-value binding) p2 bindings) ;If yes, use value.
        (if (insidep p1 p2 bindings)	;Is p1 inside p2?
            'fail			;If yes, fail.
            (add-binding p1 p2 bindings))))) ;If no, add binding.

(define (insidep variable expression bindings)
  (if (equal? variable expression)
      #f
      (inside-or-equal-p variable expression bindings)))

(define (inside-or-equal-p variable expression bindings)
  (cond ((equal? variable expression) #t)
        ((atom? expression) #f)
        ((simple-variable? expression)
         (let ((binding (find-binding expression bindings)))
           (if binding
	       (inside-or-equal-p variable (extract-value binding) bindings)
	       #f)))
        (else (or (inside-or-equal-p variable (first expression) bindings)
		  (inside-or-equal-p variable (rest expression) bindings)))))


(define (instantiate-variables pattern bindings)
  ;;; 
  ;;; Replace variables in pattern with their bindings from the bindings
  ;;; More complicated than forward chaining version because variables may
  ;;; be matched to variables.
  ;;;
  (cond ((atom? pattern) pattern)
        ((simple-variable? pattern)
         (let ((binding (find-binding pattern bindings)))
           (if binding
               (instantiate-variables (extract-value binding) bindings)
               pattern)))
        (else (cons (instantiate-variables (first pattern) bindings)
		    (instantiate-variables (rest pattern) bindings)))))