;;;; Functions to Unify S-expressions
;;;;
;;;; File:         unify.lsp
;;;; Author:       CS 51 (Bob Walton)
;;;; Version:      1

;;      variable ::= 'variable-name
;;
;;      variable-name ::= atom except nil
;;
;;      substitution ::= ()
;;                   | ( (variable-name s-expression)
;;                       . substitution )
;;
;; Variable-names can be looked up in substitutions by
;; using ASSOC.
;;
;; Variable names may be numbers, so one can do things
;; like use '1, '2, '3, ... as generated variable names.
;;
;; Variables substituted for by a substitution may
;; appear in the s-expressions other variables are mapped
;; to by the substitution.  E.g., the substitution:
;;
;;      ((X (+ 'Y 4)) (Y 6))
;;
;; Substitutions may have cycles, but this will cause
;; many functions using them to loop indefinitely. 
;; An example of a substitution with a cycle is:
;;
;;      ((X (+ 'Y 4)) (Y (+ 'X 3)))

;; Helper functions to improve readability:
;;
(defun isvar (e) (and (consp e) (eql (car e) 'quote)))
(defun varname (e) (cadr e))


;; Integer used to generate new variables '1, '2, ... .
;;
(defvar *next-generated-name* 1)

;; Function to return the next generated name (from the
;; list 1, 2, 3, ...).  Just increments *next-generated-
;; name* returning its value before incrementing.
;;
(defun generate-variable-name ()
  (let ((j *next-generated-name*))
       (setf *next-generated-name* (+ j 1))
       j))

;; Find the most general unifier (mgu) of two
;; s-expressions (1st and 2nd arguments).  A
;; substitution (3rd argument) to be applied to the
;; s-expressions may also be input (defaults to ()).
;; Returns 'FAIL if the s-expressions do not unify,
;; or the most general unifier if the s-expressions
;; do unify.  The returned substitution is actually
;; the most general unifier prefixed to any input
;; substitution.  This function does no occurs check.
;;
;; The following must be applied in order:
;;
;;      (unify 'x 'y) ===> (unify 'x 'y '())
;;      (unify ''v 'y 's) ===> (unify 'e 'y 's)
;;              if (assoc 'v 's) ===> '(v e)
;;      (unify 'x ''v 's) ===> (unify 'x 'e 's)
;;              if (assoc 'v 's) ===> '(v e)
;;      (unify ''v 'v 's) ===> 's
;;      (unify ''v 'y 's) ===> '((v y) . s)
;;      (unify 'x ''v 's) ===> '((v x) . s)
;;      (unify 'a 'y 's)
;;          ===> 's if (eql 'a 'y)
;;          ===> 'fail  otherwise
;;      (unify 'x 'a 's)
;;          ===> 's if (eql 'x 'a)
;;          ===> 'fail  otherwise
;;      (unify '(x1 . y1) '(x2 . y2) 's)
;;          ===> 'fail if (unify 'x1 'x2 's) ===> 'fail
;;          ===> (unify 'y1 'y2 's2)
;;                   if (unify 'x1 'x2 's) ===> 's2
;;
;;      where x, x1, x2, y, y1, y2 are s-expressions;
;;            v is a variable name; a is an atom;
;;            s, s2 are substitutions

;; Since assoc is expensive, effort is made to avoid
;; calling it twice to do the same thing.
;;
(defun unify (x y &optional (s nil))
  (cond
   ((isvar x)
    (let* ((vx (varname x))
           (rx (assoc vx s)))
          (cond
           (rx (unify (cadr rx) y s))
           ((null rx)
            (cond
             ((isvar y)
              (let* ((vy (varname y))
                     (ry (assoc vy s)))
                    (cond
                     (ry (unify x (cadr ry) s))
                     ((eq vx vy) s)
                     (t `((,vx ,y) . ,s)))))
             (t `((,vx ,y) . ,s)))))))
   ((isvar y)
    (let* ((vy (varname y))
           (ry (assoc vy s)))
          (cond
           ((null ry) `((,vy ,x) . ,s))
           (t (unify x (cadr ry) s)))))
   ((or (atom x) (atom y))
    (cond
     ((eql x y) s)
     (t 'fail)))
   ((and (consp x) (consp y))
    (let ((s2maybe (unify (car x) (car y) s)))
         (cond
          ((eql s2maybe 'fail) 'fail)
          (t (unify (cdr x) (cdr y) s2maybe)))))))

;; Perform variable substitutions on an s-expression.
;; Takes an expression (1st argument) and a substitution
;; (2nd argument) and returns a copy of the expression
;; with substitutions made.  No substitutable variable
;; appears in the output.
;;
;;      (subin 'a 's) ===> 'a
;;      (subin ''v 's)
;;          ===> ''v    if (assoc 'v 's) ===> nil
;;          ===> (subin 'e 's)
;;                      if (assoc 'v 's) ===> '(v e)
;;      (subin '(x . y) 's) ===>
;;              (cons (subin 'x 's) (subin 'y 's))
;;
;;      where a is an atom; s is a substitution;
;;            v is a variable name;
;;            e, x, y are s-expressions
;;
(defun subin (e s)
  (cond
   ((atom e) e)
   ((isvar e)
    (let ((r (assoc (varname e) s)))
         (cond
          ((null r) e)
          (t (subin (cadr r) s)))))
   ((consp e)
    (cons (subin (car e) s) (subin (cdr e) s)))))

;; Returns a list of the names of all the variables in
;; an s-expression (1st and only argument).  Names are
;; not duplicated in the returned list. 
;;
;;      (variables 'x) ===> (variables 'x '())
;;      (variables 'a 'vl) ===> 'vl
;;      (variables ''v 'vl)
;;          ===> 'vl        if (member 'v 'vl)
;;          ===> '(v . vl)  otherwise
;;      (variables '(x . y) 'vl) ===>
;;          (variables 'x (variables 'y 'vl))
;;
;;      where x, y are s-expressions; a is an atom;
;;            v is a variable-name;
;;           vl is a list of variable-names;
;;
(defun variables (e &optional (vl nil))
  (cond
   ((atom e) vl)
   ((isvar e)
    (cond
     ((member (varname e) vl) vl)
     (t `(,(varname e) . ,vl))))
   ((consp e)
    (variables (car e) (variables (cdr e) vl)))))