;;;;             Traditional unifier, as in SICP
;;;  The unifier of two terms was introduced by J.A. Robinson in his
;;;  famous paper in JACM, January 1965.  It is the most general
;;;  common specialization of the two terms.  Unlike the original,
;;;  this unifier allows variables in the operator positions of terms,
;;;  but we require operators to be of the same arity.

(define (match:unify p1 p2 dictionary)
  (cond ((equal? p1 p2) dictionary)
	((match:unknown? p1)
	 (extend-if-possible p1 p2 dictionary))
	((match:unknown? p2)
	 (extend-if-possible p2 p1 dictionary))
	((and (pair? p1) (pair? p2))
	 (let ((dictionary
		(match:unify (car p1)
			     (car p2)
			     dictionary)))
	   (if dictionary
	       (match:unify (cdr p1)
			    (cdr p2)
			    dictionary)
	       #f)))
	(else #f)))

(define (extend-if-possible var val dictionary)
  (let ((binding1 (match:lookup var dictionary)))
    (cond (binding1
	   (match:unify (match:value binding1) val dictionary))
	  ((match:unknown? val)
	   (let ((binding2 (match:lookup val dictionary)))
	     (if binding2
		 (match:unify var (match:value binding2) dictionary)
		 (match:bind var val dictionary))))
	  ((unify:depends-on? val var dictionary) #f)
	  (else (match:bind var val dictionary)))))

(define (unify:depends-on? expr var dictionary)
  (define (tree-walk e)
    (cond ((match:unknown? e)
	   (if (match:same-var? var e)
	       #t
	       (let ((binding
		      (match:lookup e dictionary)))
		 (if binding
		     (tree-walk (match:value binding))
		     #f))))
	  ((pair? e)
	   (or (tree-walk (car e))
	       (tree-walk (cdr e))))
	  (else #f)))
  (tree-walk expr))

;;; Instantiator:

(define (match:expression-value expression dictionary)
  (cond ((match:unknown? expression)
	 (match:variable-value expression dictionary))
	((pair? expression)
	 (cons (match:expression-value (car expression) dictionary)
	       (match:expression-value (cdr expression) dictionary)))
	(else expression)))

(define (match:variable-value variable dictionary)
  (let ((binding (match:lookup variable dictionary)))
    (if binding
	(match:expression-value (match:value binding) dictionary)
	variable)))



(define (match:same-var? v1 v2)
  (eq? v1 v2))

(define (match:unknown? pattern)
  (and (pair? pattern)
       (eq? (car pattern) '$$$)))

(define (unknown)
  (list '$$$))