;;; -*- Mode: LISP; Syntax: Common-lisp; Package: DTP; Base: 10 -*-

;;; This file was stolen from Matt Ginsberg's MVL 5/31/92

(in-package "DTP")

(defun first-binding-list (list-of-bl)
  (cond
   ((first list-of-bl)
    (first list-of-bl) )
   ((consp list-of-bl)
    '((t . t)) )
   (t nil) ))

(defvar unify-dummies)			; I comment out the original below

(defun dtp-instp (sexp1 sexp2 &optional (old-bl nil) &aux unify-dummies)
  (first-binding-list
   (remove 'fail
	   (mapcar #'subst-bdgs
		   (mapcar #'copy-alist
			   (inst-1 sexp1 sexp2 (list old-bl) nil) )))))

(defun dtp-unifyp (sexp1 sexp2)
  (first-binding-list (unifyp sexp1 sexp2)) )

(defun dtp-samep-binding-list (sexp1 sexp2)
  (let ((bls (samep sexp1 sexp2 t)))
    (cond
     ((first bls)
      (first bls) )		; Only one binding list matters
     ((consp bls)
      nil )			; Success, with no binding required
     (t
      :not-a-binding-list )	; Failure
     )))

#+mcl (defvar finished-bdgs)

;;;----------------------------------------------------------------------------

;; This file contains matching functions that handle sequence (*)
;; variables.
;;
;; Pre-unify --  determines whether two expressions unify ignoring
;;               possible variable binding conflicts.  Returns t or nil
;; Samep     --  determines whether two expressions are the same
;;    	         modulo variable renaming.  Returns t or nil.  (Returns
;;    	         a binding list if one is needed.)
;; Instp     --  determines whether one expression is an instance
;;     		 of another.  Returns a list of binding lists.
;; Unifyp    --  determines whether two expressions unify.
;;		 Returns a list of binding lists.
;;
;; The truth table for these functions is:
;; 
;;           Nil  List  Const  ?   *
;;         ---------------------------
;;    Nil  |  T    F      F    F   LR
;;    List |  F   Mtch    F    T   LR
;;    Const|  F    F      =    T   LR		LR= Lop and recur
;;    ?    |  F    T      T    T   LR
;;    *    |  LR   LR     LR   LR  LR     
;;

;; pre-unify is the simplest of the matching functions.  Note that this
;; function expects two lists as arguments.  Walk down each expression, doing:
;;  1.  If they are eq (presumably both NIL), succeed.
;;  2.  If the car's are equal, keep walking.
;;  3.  If the car's are both lists, make sure they pre-unify and then
;;  keep walking.
;;  4.  If the car of p is a sequence variable, call pre-unify*var, i.e.:
;;   4a. If the cdr of p is NIL, then you're done since p matches all of q
;;   4b. If the cdr of p matches any tail of q, you're also done
;;  5.  If the car of p is a variable, then:
;;   5a. If the car of q is a sequence variable, call pre-unify*var
;;   5b. Otherwise, keep walking
;;  6.  If the car of p is not a variable, then check out q and behave
;;  similarly, except if the car of q isn't a variable either, return
;;  failure.

(defun pre-unify (p q)
  (loop 
    (cond ((eq p q) (return t))
	  ((eql (car p) (car q)))
	  ((and (listp (car p)) (listp (car q)))
	   (unless (pre-unify (car p) (car q)) (return nil)))
	  (t (case (vartype (car p))
	       (?* (return (pre-unify*var p q)))
	       (? (if (varp* (car q)) (return (pre-unify*var q p))))
	       (t (case (vartype (car q))
		    (?* (return (pre-unify*var q p)))
		    (?)
		    (t (return nil)))))))
    (setq p (cdr p) q (cdr q))))

(defun pre-unify*var (p q)
  (or (null (setq p (cdr p)))
      (loop
	(if (pre-unify p q) (return t))
	(unless q (return))
	(setq q (cdr q)))))

;; Simple matcher that determines whether or not two expressions are the
;; same up to variable renaming.  Keeps variable equivalences in the
;; special binding list blist.  This function accepts an optional
;; argument that indicates that T or NIL is not good enough as an answer
;; -- you want the binding list created.

(defun samep (p q &optional return-answer? &aux blist)
  (declare (special blist))
  (when (samep1 p q)
    (or (null return-answer?)  	       ;knowing they're the same is good enough
	(samep-answer blist))))

;; Take the binding list produced by samep1, and make it suitable to be
;; returned.  There are two things that need to be done:
;;  1.  Any variable bound to itself should be pruned.
;;  2.  Any sequence variable is in fact bound not to a list, but to the
;;  value it represents (it can't be bound to a list of values -- this
;;  is samep, not unifyp).  So we have to bind it to the *list*
;;  containing this value.

(defun samep-answer (blist)
  (list (delete-if #'(lambda (x)
		       (cond ((eq (car x) (cdr x)))	;x bound to x
			     ((varp* (car x)) (rplacd x (list (cdr x))) nil)))
						;if x is * var, adjust
						;its binding and then
						;don't remove it
		   blist)))

;; The algorithm should be familiar -- walk down the two lists,
;; accumulating a binding list.  If p is an atom (this includes NIL),
;; then check to see if q has the same variable type as p (in which case
;; bind them to each other if possible); if neither is a variable, make
;; sure they are equal.  If only one is an atom, fail.  If neither is an
;; atom, recur.

(defun samep1 (p q)
  (cond ((atom p)				; catches nil also
	 (case (vartype p) 
	   (? (and (varp? q) (samep-var p q))) 
	   (?* (and (varp* q) (samep-var p q)))
	   (t (eql p q))))
	((atom q) nil)
	((samep1 (car p) (car q))
	 (samep1 (cdr p) (cdr q)))))

;; samep-var checks to see if p can be bound to q by seeing if either p
;; or q has already been bound.  If so, then the binding had better be
;; the same; if not, stick a new cons cell describing the binding onto
;; the binding list being accumulated.  It's ok to use eq instead of eql
;; because p and q are both symbols.

(defun samep-var (p q &aux bdg)
  (declare (special blist))
  (cond ((setq bdg (assoc p blist))
	 (eq (cdr bdg) q))
	((setq bdg (rassoc q blist))
	 (eq p (car bdg)))
	(t (push (cons p q) blist))))

;; One sided unifier that determines whether q is an instance of p.
;; Like UNIFY, passes around a set of binding lists to allow for the
;; possibility that multiple answers can result from the presence of *
;; variables.  The parameter rflg is used to indicate whether or not the
;; lists are reversed.  reversal is done for efficiency whenever a
;; non-terminal * variable is encountered.  Ignores atomic cdrs; i.e.
;; treats them as if they were nil.  A list of binding lists is returned.

(defun instp (p q)
  (inst-1 p q (list nil) nil))

;; the work is actually done here.  p and q can be assumed to be lists.
;; If q is NIL, then in order for it to be an instance of p, (car p)
;; must be a sequence variable, which is then bound to NIL and NIL must
;; be an instance of (cdr p) as well.

;; In general, if (car p) is a cons, we basically need to recur,
;; checking first that (car q) is also a cons and then doing the
;; recursion.  If (car p) is an atom, then:
;;  1.  If it is a sequence variable, call inst*var
;;  2.  If it is a normal variable, then provided that (car q) is not a
;;  sequence variable (in which case we fail), bind (car p) to (car q)
;;  and continue.
;;  3.  If it is not a variable, but is eql to (car q), simply recur.

(defun inst-1 (p q blists rflg)
  (cond ((null p) (unless q blists))	;to catch p and q both NIL
	((null q)
	 (and (varp* (car p))
	      (setq blists (inst?var (car p) nil blists))
	      (inst-1 (cdr p) nil blists rflg)))
	((consp (car p))
	 (and (listp (car q))		;to catch (car q) nil
	      (setq blists (inst-1 (car p) (car q) blists nil))
	      (inst-1 (cdr p) (cdr q) blists rflg)))
	(t (case (vartype (car p))
	     (?* (inst*var p q blists rflg))
	     (? (when (and (not (varp* (car q)))
			   (setq blists (inst?var (car p) (car q) blists)))
		  (inst-1 (cdr p) (cdr q) blists rflg)))
	     (t (and (eql (car p) (car q))
		     (inst-1 (cdr p) (cdr q) blists rflg)))))))

;; Handles the unification for star variables.  The first element of p
;; is guaranteed to be a * variable.  There are the following three
;; cases:
;;  1.  If (cdr p) is NIL, then the given * variable is all there is, so
;;  just call inst?var to do the actual unification.
;;  2.  If rflg is NIL, then this is the first * variable, and you can
;;  get away with simply reversing the two lists and trying again.
;;  3.  If rflg is T, then you have to walk down q, trying inst at each
;;  point.  This is done in a do loop, where qhead is the stuff being
;;  matched to (car p) and q contains what's left in q.  For each point
;;  in q, we call inst-1 to try to match the rest of p with the rest of
;;  q and if this succeeds, try to add the variable binding for (car p)
;;  to the result.

;; Note that qhead in the following routine is apparently reversed from its
;; true value.  In fact, this is as it should be, since the lists themselves
;; were presumably reversed when the first * variable was encountered.

(defmacro pushconc (c l) `(setf ,l (nconc ,c ,l)))

(defun inst*var (p q blists rflg)
  (cond ((null (cdr p)) 
	 (inst?var (car p) (if rflg (reverse q) q) blists))
	(rflg
	 (do (newblists qhead) (nil)
	   (pushconc (inst?var (car p) qhead (inst-1 (cdr p) q blists t))
		     newblists)
	   (unless q (return newblists))
	   (push (pop q) qhead)))	   
	(t (inst-1 (reverse p) (reverse q) blists t))))

;; inst?var actually adds a new variable binding to the binding lists
;; being accumulated.  The variable is in var, and the binding is q.
;; The binding lists that have been collected so far are in blists.
;; If the variable has already been bound, then the binding had better
;; be the same.  If it hasn't been bound, just push the binding onto the
;; accumulated list.

(defun inst?var (var q blists &aux newblists bdg)
  (dolist (blist blists newblists)
    (setq bdg (assoc var blist))
    (cond ((null bdg) (push (acons var q blist) newblists))
	  ((equal (cdr bdg) q) (push blist newblists)))))

;; General unification function and matcher.  Both call unify to do the
;; unification, then call subst-bdgs to fully instantiate the binding
;; lists and to check for any loops.  MATCHP is slightly different from
;; UNIFYP in that it must make sure new variables are created for any
;; database variables that end up free in the binding list.  It does
;; this by adding extra binding pairs for database variables to the
;; binding list before substitution.  After substitution MATCHP returns
;; a list of conses, the cars of which are the bindings for the
;; variables that appear in the query, and the cdrs of which are the
;; bindings generated for database variables.

;; In order that these functions be as efficient as possible, they
;; attempt to reuse as many conses as possible.  To make the code clear
;; while this is going on, these macros have been defined for pushing
;; and popping cells off of lists in ways that allow the conses to be
;; reused:

(defmacro popcell (l) `(rplacd (prog1 ,l (setq ,l (cdr ,l))) nil))

(defmacro pushcell (c l) `(setq ,l (rplacd ,c ,l)))

;; The unifier works by first calling unify, which does the basic
;; unification but may return binding lists with loops or incomplete
;; bindings (e.g., x is bound to y and y is then bound to z).  In order
;; to deal with these possibilities, we work through the list of binding
;; lists returned, calling subst-bdgs on each one to simplify it.  Since
;; subst-bdgs is destructive, we have to copy the binding list unless
;; it's the last one we need to do (in which case we don't mind
;; destroying it).

;; subst-bdgs returns FAIL if there is an internal conflict in the
;; binding list.  Thus we first check to see if the binding is empty (in
;; which case we just push it on to the list unchanged); if it isn't we
;; try subst-bdgs.  Then we just remove any FAILs from the result.

(defvar unify*flg)			;binding lists must be copied
;; (defvar unify-dummies)			;list of dummy variables
;; ^^^^^^^^^^^^^^^^^^^^^^ commented out 5/18/93 by Don Geddis (moved to top)
(defvar nasty-unify)			;variables may be in wrong order?

(defun unifyp (p q &aux unify-dummies (blists (unify p q)))
  (cond ((car blists)
	 (napcar #'copy-alist (cdr blists))
	 (napcar #'subst-bdgs blists)
	 (delete 'fail blists))
	(t blists)))

;; the matcher is much the same, but matches an expression to a database
;; sentence (which is referenced by its proposition symbol).  There are
;; a couple of additional subtleties, though:

;; 1.  We want to bind the database variables and not the variables in
;; the query wherever possible.  check-order is responsible for fiddling
;; with the binding lists to make this happen; nasty-unify is a flag
;; indicating that we couldn't get by without it being a possibility in
;; the unification phase.

;; 2.  We don't want to have things bound to the uninterned symbols in
;; the database sentence, so we next bind each database variable to a new
;; variable.  We simplify as for unify, and then split the bindings into 
;; those appearing in the query and those appearing in the database.

(defun matchp (exp datum &aux unify-dummies nasty-unify
			      (blists (unify (denotes datum) exp)))
  (cond ((car blists)
	 (when nasty-unify
	   (mapc #'(lambda (blist)
		     (napcar #'(lambda (b) (check-order b blist)) blist))
		 blists))
	 (let ((db (get datum 'vars-in)))
	   (napcar #'copy-alist (cdr blists))
	   (napcar #'(lambda (b) (match-db-vars b db)) blists)
	   (napcar #'divide-bdgs (delete 'fail blists))))
	(t blists)))

;; Here we check the order of the variables appearing in a particular
;; binding list.  If either the car is a database variable or the cdr
;; is bound, we don't have to worry.  (If the cdr is bound, the binding
;; will be simplified away.)  Now there are two cases:
;; 1.  If the car is a *var, and is bound to a list consisting of a
;;     *var alone, and the second *var is a database variable, we have
;;     to swap them.
;; 2.  If the car is a normal var, it's much the same.

(defun check-order (bdg blist)
  (cond ((or (database-variable (car bdg)) (assoc (cdr bdg) blist))
	 bdg)
	((varp? (car bdg))
	 (if (and (symbolp (cdr bdg)) (database-variable (cdr bdg)))
	     (cons (cdr bdg) (car bdg))
	   bdg))
	((and (symbolp (second bdg)) (database-variable (second bdg)))
	 (list (second bdg) (car bdg)))
	(t bdg)))

;; Here we replace the database variables with new variables.  Any unbound
;; database variable (there is a list in vars) gets bound to a new variable
;; before we call subst-bdgs to sort it all out.

(defun match-db-vars (bdgs vars)
  (dolist (var vars (subst-bdgs bdgs))
    (unless (assoc var bdgs)
      (push (if (varp* var) (list var (new-*var)) (cons var (new-?var)))
	    bdgs))))

;; And here we split the binding list into a database set and a query set.
;; We do it without consing up a whole bunch of new cells.

(defun divide-bdgs (bdgs)
  (do (bdg query database) 
      ((null bdgs) (cons query database))
    (setq bdg (popcell bdgs))
    (if (database-variable (caar bdg))
	(pushcell bdg database)
	(pushcell bdg query))))

;; Unifier that handles star variables.  Passes around a set of binding
;; lists to allow for the possibility that multiple answers can result
;; from the presence of * variables.  The parameter rflg is used to
;; indicate whether or not the lists are reversed.  reversal is done
;; for efficiency whenever a non-terminal * variable is encountered.
;; Note:  requires post pass to eliminate all variable loops and to
;; simplify variable bindings.  There is one other catch -- when possible,
;; we would like to bind the variables in p and not those in q.  This
;; functionality is needed by the matcher.  The special variable
;; nasty-unify is used to record the fact that we may have failed to
;; do this.

(defun unify (p q &aux unify*flg)
  (if (or (atom p) (atom q)) (setq p (list p) q (list q)))
  (unify-1 p q (list nil) nil))

;; Here we go.
;;  1.  If p and q are eq, you're done.
;;  2.  If p is NIL, then q needs to be a list starting with a *
;;  variable, in which case we try to unify (car q) with NIL and (cdr q)
;;  with NIL if that succeeds.
;;  3.  If q is NIL, it's much the same.
;;  4.  If the car's are eql, we unify the cdrs.
;;  5.  If the car's are both lists, we unify them and then the cdrs.
;;  6.  If the car of p is a variable, then:
;;   6a.  If the car of q is a sequence variable, we call unify*var
;;   6b.  Otherwise, we just try to set (car p) to (car q) and continue
;;  7.  If the car of p is a sequence variable, we call unify*var
;;  8.  If the car of p is not a variable, then if the car of q is a
;;   variable of any type, we treat it as in 6,7

(defun unify-1 (p q blists rflg)
  (cond ((eq p q) blists)
	((null p)
	 (and (varp* (car q))
	      (setq blists (unify?var (car q) nil blists))
	      (unify-1 (cdr q) nil blists rflg)))
	((null q)
	 (and (varp* (car p))
	      (setq blists (unify?var (car p) nil blists))
	      (unify-1 (cdr p) nil blists rflg)))
	((eql (car p) (car q)) 
	 (unify-1 (cdr p) (cdr q) blists rflg))
	((and (listp (car p)) (listp (car q)))
	 (and (setq blists (unify-1 (car p) (car q) blists nil))
	      (unify-1 (cdr p) (cdr q) blists rflg)))
	(t (case (vartype (car p))
	     (? (cond ((varp* (car q))
		       (setq nasty-unify t)
		       (unify*var q p blists rflg))
		      ((setq blists (unify?var (car p) (car q) blists))
		       (unify-1 (cdr p) (cdr q) blists rflg))))
	     (?* (unify*var p q blists rflg))
	     (t (case (vartype (car q))
		  (? (when (setq blists (unify?var (car q) (car p) blists))
		       (setq nasty-unify t)
		       (unify-1 (cdr p) (cdr q) blists rflg)))
		  (?* (setq nasty-unify t)
		      (unify*var q p blists rflg))))))))

;; Handles the unification for star variables.  The first element of p
;; is guaranteed to be a * variable.  The situation is complicated by
;; the fact that if the variable is already bound, we want to plug for
;; it here and not risk the looping that happens when two * variables
;; meet.  So we have to do the analysis for each binding list in blists.
;; There are the following four cases:
;;  1.  If (cdr p) is NIL, then the given * variable is all there is, so
;;  just call unify?var to do the actual unification.
;;  2.  If (car q) is a * var and (cdr q) is NIL, we treat it like (1).
;;  3.  If rflg is NIL, then this is the first * variable, and we can
;;  get away with simply reversing the two lists and trying again.
;;  4.  Otherwise we look through the blists to bind p if possible:
;;    4a.  If p is bound, then we stick its binding onto the cdr
;;  	   of p and repeat the call.
;;    4b.  If q does not begin with a * variable, things are somewhat 
;;         simpler; we have to walk down q, trying unify at each point.
;;         This is done by unify*loop.
;;    4c.  If q is bound, we plug in the binding as in case 1.
;;    4d.  The last case is nasty and unify-** is responsible for sorting
;;         it out.

(defun unify*var (p q blists rflg &aux qstar)
  (cond ((null (cdr p)) (unify?var (car p) (if rflg (reverse q) q) blists))
	((and (setq qstar (varp* (car q))) (null (cdr q)))
	 (setq nasty-unify t)
	 (unify?var (car q) (if rflg (reverse p) p) blists))
	(rflg
	 (setq unify*flg t)
	 (do (newblists)
	     ((null blists) newblists)
	   (let* ((blist (popcell blists))
		  (bdg (find*var (car p) blist)))
	     (pushconc
	      (cond (bdg (unify-1 (revappend (cdr bdg) (cdr p)) q blist t))
		    (qstar
		     (let ((qbdg (find*var (car q) blist)))
		       (if qbdg
			   (unify-1 p (revappend (cdr qbdg) (cdr q))
				    blist rflg)
			 (unify-** p q blist))))
		    (t (unify*loop p nil q blist)))
	      newblists))))
	(t (unify-1 (reverse p) (reverse q) blists t))))

;; Here we handle the loop where p begins with a * variable and q
;; doesn't.  qhead is the reverse of the stuff being matched to (car p)
;; and qtail is what's left in q.

;; It's pretty simple, except if q contains a * variable itself.  This
;; case is handled after the * variable is pushed onto qhead, so if it's
;; on qtail we don't have to do anything.  In the "simple" case where qtail
;; begins with something other than a * variable, we just call unify-1
;; to unify qtail with the cdr of p and bind the * variable beginning p
;; to all of qhead.  (If there is a * variable at the beginning of the
;; reversed qhead, this operation is a special case of the first clause
;; of the main cond below.)

;; To handle the case where there is a * variable in q, we have to 
;; allow for the possibility that (car p) only unifies with a *part* 
;; of this * variable (toegether with all of qhead, of course).  This 
;; is done by splitting the * variable into two new variables, and 
;; assuming that (car p) only includes the first.

;; There are two additional subtleties.  First, the new * variables created
;; are just dummies, and we want to be able to get rid of them at the end of
;; the unification process if possible.  So instead of invoking
;; (new-*var) to create them, we invoke (new-dummy-var), which records
;; their dummy status.

;; Second, we never "resplit" a * variable.  This is not complete, but
;; otherwise the unifier may loop in a variety of situations (which was
;; felt to be worse).

(defun unify*loop (p qhead qtail blists &aux newblists)
  (loop
    (cond ((member (car qhead) unify-dummies) nil)	;don't resplit *var
	  ((varp* (car qhead))
	   (pushconc
	    (let ((v1 (new-dummy-var)) (v2 (new-dummy-var)))
	      (unify-1 (cdr p) (cons v1 qtail)
		       (unify?var (car p) (cons v2 (cdr qhead))
				  (unify?var (car qhead) (list v1 v2)
					     (copy-list blists)))
		       t))
	    newblists))
	  ((not (varp* (car qtail)))
	   (pushconc (unify-1 (cdr p) qtail 
			      (unify?var (car p) qhead (copy-list blists)) t)
		     newblists)))
    (unless qtail (return newblists))
    (push (pop qtail) qhead)))

;; p and q both begin with * variables.  Now there are two
;; possibilities:
;;  1.  (car p) unifies with (car q) and perhaps a little more
;;  2.  (car q) unifies with (car p) and a little more
;; Of course, by "a little more", we mean some portion of the tail of
;; the list being considered -- which may mean a *part* of some
;; subsequent * variable.  Thus if ?*x is unifying with the car of
;; (?*y ?*z) and a little more, it might unify with ?*y and some *part*
;; of ?*z and not the whole thing.

;; To handle this (admittedly bizarre) case, when we decide to unify
;; with a "little more" and this little more ends in a * variable, we
;; split that * variable into two parts, including the first in the
;; little more and leaving the rest to unify with the remainder of the
;; expression.  But now note that since the first of these parts can
;; unify with nil (in which case it is just the same as if the *
;; variable wasn't included in the "little more" after all), there is no
;; point in ending the "little more" just before a sequence variable.

(defun unify-** (p q blists)
  (nconc
   (unify-1 (cdr p) (cdr q)
	    (unify?var (car p) (list (car q)) (copy-list blists)) t)
   (unify-**-1 p q (copy-list blists))
   (unify-**-1 q p (copy-list blists))))

;; here is the basic function; (car p) is assumed to unify with (car q)
;; and a little more.  But this is just what unify*loop does; we have to
;; be sure to move the first two elements of q to qhead and leave the
;; rest as qtail.

(defun unify-**-1 (p q blists)
  (when (cdr q)
    (unify*loop p (list (second q) (first q)) (cddr q) blists)))

(defun new-dummy-var (&aux (var (new-*var)))
  (push var unify-dummies)
  var)

;; modify a collection of binding lists to indicate that the variable
;; var is bound to the value q.  If unify*flg is T, then blists cannot
;; be destroyed in the process.

;; We proceed through blists one at a time.  For each blist, we check to
;; see if var is already bound; find?var returns q if it isn't and the
;; existing binding if it is.  There are therefore the following cases:
;;  1.  If the value returned is q (for whatever reason), then
;;  everything is fine and we just pass this blist off as done.
;;  2.  If the value returned is "badloopcheck", then we have
;;  essentially hit an occurcheck problem, in that the variable is
;;  already being investigated by a higher-level call to unify?var.  In
;;  this case, we give up.
;;  3.  If both the current and desired values are lists, then we have
;;  to try to unify them.  We mark the variable under consideration as
;;  "badloopcheck" (see 2 above), and invoke the unifier recursively.
;;  Then we reset the old value to which the variable is bound, and add
;;  the result of the unification call to the growing list of new
;;  answers.  (We do these two steps in the reverse order.)
;;  4.  If the desired value is a variable, then we basically do things
;;  in the reverse order, finding the value to which *q* is bound.  This
;;  leads to:
;;   4a.  If q is bound (for whatever reason) to the desired value,
;;   proceed with success.
;;   4b.  If q is bound to badloopcheck by a higher-level unification
;;   call, give up.  (This happens by default.)
;;   4c.  If both var's value and q's value are lists, try to unify
;;   them as in (3).

(defun unify?var (var q blists)
  (do (blist bdg val valq newblists) 
      ((null blists) newblists)
    (setq blist (popcell blists))		;strip off first blist
    (setq bdg (if unify*flg (find?var var q blist) (nfind?var var q blist))
	  val (cdr bdg))
    (cond ((eql val q) 
	   (pushcell blist newblists))
	  ((eq val '|BADLOOPCHECK|))
	  ((and (consp val) (consp q))
	   (rplacd bdg '|BADLOOPCHECK|)
	   (pushconc (unify-1 val q blist nil) newblists)
	   (rplacd bdg val))
	  ((varp q) 
	   (setq bdg (if unify*flg (find?var q val blist) 
		       (nfind?var q val blist))
		 valq (cdr bdg))
	   (cond ((eql val valq) (pushcell blist newblists))
		 ((and (consp val) (consp valq))
		  (rplacd bdg '|BADLOOPCHECK|)
		  (pushconc (unify-1 val valq blist nil) newblists)
		  (rplacd bdg valq)))))))

;; Find the value to which a variable is bound.  The binding list
;; examined is (car blist).

;; We first look for var's binding.  If it has none, we add a dotted
;; pair (var . q) giving the desired binding to the front of the
;; binding list, and return that.

;; If var is bound to a variable, then we basically just recur, trying
;; to find the binding for *that* variable.  The only catch is that if
;; we encounter the given variable again, we should just note that
;; we've hit a loop and bind either one of the two variables to the
;; desired value.  In practice, the variable var is bound to q.

;; If var is bound to something other than a variable, we just return
;; that.

;; There are two routines here, one for * variables (that returns nil if
;; the * variable is unbound, and the binding otherwise), and one for
;; normal variables, that successfully binds the variable to the given
;; value if there is no other binding.

(defun find*var (var blist &aux (bdg (assoc var (car blist))) (val (cdr bdg)))
  (cond ((null bdg) nil)		;failure -- no existing binding
	((and (consp val)
	      (null (cdr val)) 
	      (varp* (car val)))	;another * variable?
	 (prog2
	     (rplacd bdg '|VARLOOPCHECK|)
	     (or (find*var (car val) blist) bdg)
	   (rplacd bdg val)))
	((eq val '|VARLOOPCHECK|)	;variable loop -- hit loopcheck
	 (setf (car blist) (remove bdg (car blist)))
	 nil)
	(t bdg)))

(defun find?var (var q blist &aux (bdg (assoc var (car blist)))
				  (val (cdr bdg)))
  (cond ((null bdg)			;success -- no existing binding
	 (car (push (cons var q) (car blist))))
	((consp val) bdg)		;existing binding to a list
	((eql q val) bdg)		;existing binding to same value
	((eq val '|VARLOOPCHECK|)	;variable loop -- remove current
					;binding for var and set up a new one
	 (setf (car blist) (remove bdg (car blist)))
	 (car (push (cons (car bdg) q) (car blist))))
	((varp val)			;bound to a variable but no loop yet
	 (prog2
	     (rplacd bdg '|VARLOOPCHECK|)
	     (find?var val q blist)
	   (rplacd bdg val)))
	(t bdg)))			;bound to a constant -- return it

;; Destructive version of the above routine.  As it unwinds, nfind?var
;; destructively substitutes the final value into any intermediate
;; variables.

(defun nfind?var (var q blist &aux (bdg (assoc var (car blist)))
				   (val (cdr bdg)))
  (cond ((null bdg) 
	 (car (push (cons var q) (car blist))))
	((consp val) bdg)
	((eql q val) bdg)
	((eq val '|VARLOOPCHECK|)	;bind it destructively
	 (rplacd bdg q))
	((varp val)
	 (rplacd bdg '|VARLOOPCHECK|)
	 (setq val (nfind?var val q blist))
	 (cond ((eq bdg val) val)
	       ((atom (cdr val))
		(rplacd bdg (cdr val)))	;bind intermediates
	       (t (rplacd bdg (car val))
		  val)))
	(t bdg)))

;; Functions that check for loops in the binding list and do complete
;; binding list substitution.  Returns FAIL if the check fails.
;; Otherwise, returns the substituted binding list.

;; This routine works by working down the given binding list, one
;; binding at a time.  A list of equivalent variables is maintained in
;; equivalent-bdgs; a list of the variables that have been accumulated
;; so far is kept in finished-bdgs (so finished-bdgs is returned at the
;; end, after removing any bindings to dummy variables).

(defun subst-bdgs (working-bdgs &aux equivalent-bdgs finished-bdgs pending*)
  (declare (special working-bdgs equivalent-bdgs finished-bdgs pending*))
  (catch 'no-unify
    (do (temp) 
	((null working-bdgs) (remove-dummy-bindings finished-bdgs))
      (setq temp (popcell working-bdgs))	;chop a cell from working-bdgs
      (subst-bdg temp))))

;; Process a single binding.  There are five possibilities:

;;  1. If the variable is being bound to another variable (this will
;;  only happen with regular variables; * variables will always be bound
;;  to lists), add the variable to equivalent-bdgs and find the value
;;  for the variable using subst-var.

;;  2. If the variable is bound to an atom (including nil) move the
;;  binding to finished-bdgs.

;;  3. If the variable is a star variable and is bound to a list
;;  consisting of another star variable then treat it the same way as
;;  in case 1.

;;  4. If the variable is not a * variable and is being bound to a list,
;;  then process the given list to see (destructively) what *its*
;;  variables are bound to.  This is done by subst-term; when we
;;  call subst-term, we mark the given variable to make sure no binding
;;  loops occur.

;;  5. If the variable is a * variable and is bound to a list, it's a
;;  little harder.  We still want to do basically the same thing, but
;;  it is possible that the target list includes the given * variable
;;  without there being a conflict if the only other things on the target
;;  list are * variables that can be bound to NIL; consider unifying
;;  (?*1) with (?*1 ?*2).  To handle this, we invoke subst-term *without*
;;  pushing the given cell onto the list of finished bindings *or*
;;  marking the variable loop.  In the process, the original * variable
;;  will have been "forgotten" and therefore not rebound.  There are
;;  now three possibilities:

;;  5a. If the original * variable does not appear in the tree, it's ok
;;  to return it.
;;  5b. If it does appear in the tree, then it has to appear at the
;;  top level only, and everything else has to be a *var that can be
;;  bound to NIL.
;;  5c. Otherwise, fail.

;;  To make the check in (5a) faster, we do the whole process, keeping
;;  a list of *vars that are pending.  Whenever we try to find a binding
;;  for a *var and there isn't one (i.e., if it's pending, we just hit a
;;  loop), we delete the *var from the list.  Then we can just check to
;;  see if it's on the list to check (5a), avoiding the need to walk
;;  through the tree.

(defun subst-bdg (cell &aux (bdg (car cell)) (val (cdr bdg)))
  (declare (special equivalent-bdgs finished-bdgs pending*))
  (cond ((varp val)
	 (rplacd bdg '|BADLOOPCHECK|)
	 (rplacd bdg (subst-var val))
	 (unless (eq (car bdg) (cdr bdg)) (pushcell cell equivalent-bdgs))
	 (when equivalent-bdgs
	   (pushconc equivalent-bdgs finished-bdgs)
	   (setq equivalent-bdgs nil)))
	((atom val)
	 (pushcell cell finished-bdgs))
	((and (null (cdr val)) (varp* (car bdg)) (varp* (car val)))
	 (rplacd bdg '|BADLOOPCHECK|)
	 (let ((newval (subst-var (car val))))
	   (rplacd bdg (if (listp newval) newval val)))
	 (unless (eq (car bdg) (second bdg)) (pushcell cell equivalent-bdgs))
	 (when equivalent-bdgs
	   (pushconc equivalent-bdgs finished-bdgs)
	   (setq equivalent-bdgs nil)))	  
	((consp val)
	 (cond ((varp* (car bdg))
		(push (car bdg) pending*)
		(let ((term (subst-term val)))
		  (cond ((eq (car bdg) (car pending*))
			 (pop pending*)
			 (pushcell cell finished-bdgs)
			 (rplacd bdg term))
			(t (subst-bdg-special-case bdg term)))))
	       (t (pushcell cell finished-bdgs)
		  (rplacd bdg '|BADLOOPCHECK|)
		  (rplacd bdg (subst-term val))))))
  bdg)

;; Here is where we handle the cases (5b) and (5c) above.  Since the
;; term to which the binding has been reduced has all the variables
;; substituted in, any remaining variable is free for substitution.
;; So we have to check that every element of the term is a *var,
;; then it's easy.  We bind them all to nil and also bind the *given*
;; *var to nil if it appears multiple times, as in
;; (unifyp '(?*1 ?*2 ?*2) '(?*2)).

(defun subst-bdg-special-case (bdg term)
  (declare (special finished-bdgs))
  (cond ((notevery #'varp* term)
	 (throw 'no-unify 'fail))
	(t (let ((nil* bdg) (var (car bdg)) found1 found2)
	     (setf (cdr bdg) nil)
	     (dolist (v term (unless found2 (setf (cdr bdg) (list (car bdg)))))
	       (cond ((member v nil*)
		      (when (eql v var)
			(cond (found2)
			      (found1 (setq found2 t)
				      (push bdg finished-bdgs))
			      (t (setq found1 t)))))
		     (t (push v nil*)
			(push (list v) finished-bdgs))))))))

;; This routine finds the value for the variable var.  If a finished
;; binding is known for var, then either there is a variable loop (in
;; which case we give up), or we return that binding.  Otherwise, we:
;;  1. Find the value on the working binding-list
;;  2. Splice the binding out of the working binding list
;;  3. Call subst-bdg on the bdg to find out the value
;;  4. Return the fully substituted value
;; If there is no binding for the variable anywhere and it's a *var,
;; we remove it from the list of pending *vars as described in subst-bdg.

(defun subst-var (var &aux (bdg (assoc var finished-bdgs)) cell)
  (declare (special working-bdgs finished-bdgs pending*))
  (cond (bdg (if (eq (cdr bdg) '|BADLOOPCHECK|)
		 (throw 'no-unify 'fail)
	       (cdr bdg)))
	((setq cell (member var working-bdgs :key #'car))
	 (cond ((cdr cell)			;complex version of
		(setq bdg (car cell))		;(setq working
		(rplaca cell (cadr cell)) 	;  (delete bdg working))
		(setq bdg (rplaca (cdr cell) bdg))
		(rplacd cell (cddr cell))
		(setq cell bdg))
	       (t (setq working-bdgs (nbutlast working-bdgs))))
	 (cdr (subst-bdg cell)))
	(t (when (varp* var) (setq pending* (delete var pending* :count 1)))
	   var)))

(defun subst-term (term)
  (when term
    (case (vartype (car term))
      (? (reuse-cons (subst-var (car term)) (subst-term (cdr term)) term))
      (?* (let ((val (subst-var (car term))))
	    (cond ((null val) (subst-term (cdr term)))
		  ((atom val)		;no bdg for the var
		   (reuse-cons (car term) (subst-term (cdr term)) term))
		  (t (append val (subst-term (cdr term)))))))
      (t (reuse-cons (if (listp (car term)) (subst-term (car term)) (car term))
		     (subst-term (cdr term))
		     term)))))

(defun remove-dummy-bindings (bdgs)
  (if unify-dummies
      (delete-if #'(lambda (x) (member x unify-dummies)) bdgs :key #'car)
      bdgs))