;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; This unification procedure uses an algorithm described on p. 348
; of "Artificial Intelligence" by Charniak & McDermott.
; It returns an association list each of whose elements is a
; dotted pair consisting of a variable name and a formula which
; is to be substituted for it.  This returned value represents the
; MGU of the two formulas passed as arguments to it.  If the two
; formulas do not unify, the return value is the atom 'no.
; (Note that a return value of nil, the empty list, just means that
; the two formulas unify and no variable bindings are required for this.
; This occurs if and only if (equal pat1 pat2) ==> t.)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun unify (pat1 pat2) (subunify pat1 pat2 nil))

(defun subunify (pat1 pat2 theta)
  (cond
    ((equal pat1 pat2) theta)
    ((is-var? pat1) (setq theta (var-unify pat1 pat2 theta)))
    ((is-var? pat2) (setq theta (var-unify pat2 pat1 theta)))
    ((or (atom pat1) (atom pat2) (/= (length pat1) (length pat2))) 'no)
    (t
      (do ((rest1 pat1 (cdr rest1))       ;loop through lists together
	   (rest2 pat2 (cdr rest2)))
					  ; return if done or attempt failed
	  ((or (null rest1) (eql theta 'no)) theta)
         
	  (setq theta (subunify (car rest1) (car rest2) theta))))))

(defun var-unify (var pat theta)
   (let ((match (assoc var theta)))
	(cond
	  (match (subunify (cdr match) pat theta))
	  ((eql var pat) theta)
	  ((occurs-in var (varsubst pat theta)) 'no)
	  (t (cons (cons var pat) theta)))))

(defun occurs-in (a  l)
 ; returns t if the atom a occurs anywhere in l (won't work if a is a list)
  (cond ((atom l) nil)
	((eql a (car l)) t)
	(t (or (occurs-in a (car l)) (occurs-in a (cdr l))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; This function accepts a predicate calculus formula as input and returns
; the same formula with newly generated variable symbols substituted for
; the original variable symbols.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun standardize (formula)
  (varsubst formula (new-var-names formula nil)))

(defun new-var-names (formula subst-alist)
  (cond ((null formula) subst-alist)
	((listp formula)
	 (new-var-names (cdr formula)
			(new-var-names (car formula)
				       subst-alist)))
	((and (is-var? formula)
	      (null (assoc formula subst-alist)))
	 (cons (cons formula (gen-var))
	       subst-alist))
	(t subst-alist)
	))

(defun is-var? (formula)   ; test whether formula is symbol beginning with "?"
  (and (symbolp formula)
       (string= "?" (string formula) :end2 1)))

(defun gen-var ()		; generates a symbol beginning with "?x"
  (gensym "?x"))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; This function accepts as arguments a predicate calculus formula and an
; association list specifying a set of substitutions to perform and it
; returns the corresponding formula with the substitutions performed.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun varsubst (form subst-alist)
  (cond ((null subst-alist) form)
	(t (varsubst (subst (cdar subst-alist)
			    (caar subst-alist)
			    form)
		     (cdr subst-alist)))
	))