;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;;  All the code  was taken from Russell and Norvig
;;;
;;;; Unification and Substitutions (aka Binding Lists)
;;; 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".  Note that it uses the term "bindings"
;;; rather than "substitution" or "theta".  The meaning is the same.

;;;; Constants

;;; Indicates unification failure"
(define *fail* #f)

;;; Indicates unification success, with no variables.
(define *no-bindings* '(( #f )))

;;;; 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*)))

;;; Replace all variables in x with new ones."

(define (rename-variables x . new-prefix)
  (let ((renaming
	 (map (lambda (var) 
		(make-binding var (apply new-variable var new-prefix)))
	      (variables-in x))))
    (if (null? renaming) x (subst-bindings renaming x))))

;;;; 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))))

;;; Replace any ? within exp with a variable of the form ?123.
(define (replace-?-vars exp)
  (cond ((eq? exp '?) (new-variable '?))
	((pair? exp)
	 (reuse-cons (replace-?-vars (first exp))
		     (replace-?-vars (rest exp))
		     exp))
	(else exp)))

;;; Is x a variable (a symbol beginning with `?')?"
(define (variable? x)
  (and (symbol? x) (equal? (string-ref (symbol->string x) 0) #\?)))

;;; Find a (variable . value) pair in a binding list."
(define (get-binding var bindings)
  (assoc var bindings))

;;; Get the variable part of a single binding."
(define (binding-var binding)
  (and binding (car binding)))

;;; Get the value part of a single binding."
(define (binding-val binding)
  (and binding (cdr binding)))

(define make-binding cons)

;;; Get the value part (for var) from a binding list."
(define (lookup var bindings)
  (binding-val (get-binding var bindings)))

;;; Add a (var . value) pair to a binding list."
(define (extend-bindings var val bindings)
  (cons (make-binding var val)
        ;; Once we add a "real" binding,
        ;; we can get rid of the dummy *no-bindings*
        (if (eq? bindings *no-bindings*)
            '()
            bindings)))

;;; Combine lists of bindings
(define (merge-bindings bindings1 bindings2)
  (cond ((or (eq? bindings1 *fail*) (eq? bindings2 *fail*))
	 *fail*)
	((eq? bindings1 *no-bindings*) bindings2)
	((eq? bindings2 *no-bindings*) bindings1)
	(else
	 (append bindings1 bindings2))))

;;; 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)))

;;; Substitute the value of variables in bindings into x,
;;;  taking recursively bound variables into account.
(define (subst-bindings bindings x)
  (cond ((eq? bindings *fail*) *fail*)
        ((eq? bindings *no-bindings*) x)
        ((and (variable? x) (get-binding x bindings))
         (subst-bindings bindings (lookup x bindings)))
        ((not (pair? x)) x)
        (else (reuse-cons (subst-bindings bindings (car x))
			  (subst-bindings bindings (cdr x))
			  x))))

;;; Return (cons x y), or reuse x-y if it is equal? to (cons x y)
(define (reuse-cons x y x-y)
  (if (and (eqv? x (car x-y)) (eqv? y (cdr x-y)))
      x-y
      (cons x y)))

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

;;; Return a list of all the variables in EXP.
(define (variables-in exp)
  (unique-find-anywhere-if variable? exp))

;;; Return a list of leaves of tree satisfying predicate,
;;;  with duplicates removed.

(define (unique-find-anywhere-if predicate tree)
  (define (loop tree found-so-far)
    (if (pair? tree)
	(loop
	 (first tree)
	 (loop (rest tree) found-so-far))
	(if (predicate tree)
	    (adjoin tree found-so-far)
	    found-so-far)))
  (loop tree '()))

(define (adjoin x l) (if (not (member x l)) (cons x l) l))

;;; Does predicate apply to any atom in the tree?
(define (find-anywhere-if predicate tree)
  (if (pair? tree)
      (or (find-anywhere-if predicate (first tree))
          (find-anywhere-if predicate (rest tree)))
      (predicate tree)
      ))

(define *new-variable-counter* 0)
(define *variable-prefix* "?@")
;;; "Create a new variable.  Assumes user never types variables of form ?X_9"
(define (new-variable var . new-prefix)
  (set! *new-variable-counter* (+ 1 *new-variable-counter*))
  (string->symbol
   (string-append (if (variable? var) "" "?")
                  (if (and (not (null? new-prefix)) (first new-prefix))
		      *variable-prefix* (symbol->string var))
		  "_"
		  (number->string *new-variable-counter*))))

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