<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
;;; Code from Paradigms of Artificial Intelligence Programming
;;; by Peter Norvig, adapted to Scheme by Gary Leavens
;;; File unify.ss: Unification functions


(define unify ; TYPE: s-expression, s-expression, env -> env
  (lambda (x y bindings)
    ; ENSURES: result is either *failure* or the env that unifies x and y
    (cond ((eq? bindings *failure*) *failure*)
	  ((equal? x y) bindings)
	  ((variable? x) (unify-variable x y bindings))
	  ((variable? y) (unify-variable y x bindings))
	  ((and (pair? x) (pair? y))
	   (unify (cdr x) (cdr y) 
	     (unify (car x) (car y) bindings)))
	  (else *failure*))))

(define unify-variable ; TYPE: variable, s-expression, env -> env
  (lambda (var x bindings)
    ; ENSURES: result is either *failure* or the unifing env for
    ;          var with x; the env may be extended
    (cond ((env-bound? var bindings)
	   (unify (env-value var bindings) x bindings))
	  ((and (variable? x) (env-bound? x bindings))
	   (unify var (env-value x bindings) bindings))
	  ((occurs-check var x bindings) *failure*)
	  (else (env-update var x bindings)))))

(define occurs-check  ; TYPE: variable, s-expression, env -> boolean
  (lambda (var x bindings)
    ; ENSURES: result is #t iff var occurs anywhere inside x
    (cond ((eq? var x) #t)
	  ((and (variable? x) (env-bound? x bindings))
	   (occurs-check var (env-value x bindings) bindings))
	  ((pair? x) (or (occurs-check var (car x) bindings)
			 (occurs-check var (cdr x) bindings)))
	  (else #f))))

;;; ==============================

(define subst-bindings ; TYPE: env, s-expression -> s-expression
  (lambda (bindings x)
    ; ENSURES: result is the substitution of the value of variables
    ;          in bindings into x, taking recursively bound variables
    ;           into account.
    (cond ((eq? bindings *failure*) *failure*)
	  ((eq? bindings (env-empty)) x)
	  ((and (variable? x) (env-bound? x bindings))
	   (subst-bindings bindings (env-value x bindings)))
	  ((not (pair? x)) x)
	  (else (cons (subst-bindings bindings (car x))
		      (subst-bindings bindings (cdr x)))))))

;;; ==============================

(define unifier ; TYPE: s-expression -> s-expression
  (lambda (x y)
    ; ENSURES: result is either *failure* or
    ;          an s-expression that unifies with both x and y
    (subst-bindings (unify x y (env-empty)) x)))