(in-package "USER")

(defparameter *bottom* (quote %fail%))

(defmacro bottomp (foo) `(eq ,foo *bottom*))

(defvar *bindings* nil)

(defvar *equalities* nil)

(defstruct fs
  structure
  bindings)

(defun unify (fs-1 fs-2 &key variables)
  (let* ((bindings-1 (or variables (fs-bindings fs-1)))
         (offset (if bindings-1
                   (apply #'max (remove-if-not #'integerp bindings-1))
                   0))
	 #||
         (bindings (append bindings-1 (add! offset (fs-bindings fs-2))))
         equalities
	 ||#
	 )
    ;;(declare (special bindings equalities))
    (setq *bindings* (append bindings-1 (add! offset (fs-bindings fs-2)))
	  *equalities* nil)
    (let ((unification (unify! (fs-structure fs-1)
			       (add! offset (fs-structure fs-2)))))
      (when (bottomp unification)
        (return-from unify *bottom*))
      (loop for (variable equality-list) on *equalities* by #'cddr
	    ;; for iterator = *equalities* then (rest (rest iterator))
	    ;; for variable = (first iterator)
	    do (loop for equality in equality-list ;; (second iterator)
		     do (nsubstitute! variable equality unification :test #'eql)))
      (make-fs :structure unification :bindings *bindings*))))

(defun unify (fs-1 fs-2 &key variables)
  (unify4 (fs-structure fs-1)
	  (or variables (fs-bindings fs-1))
	  (fs-structure fs-2)
	  (fs-bindings fs-2)))

(defun unify4 (fvps-1 bind-1 fvps-2 bind-2)
  (let* ((offset (if bind-1
                   (apply #'max (remove-if-not #'integerp bind-1))
                   0)))
    (setq *bindings* (append bind-1 (add! offset bind-2))
	  *equalities* nil)
    (let ((unification (unify! fvps-1
			       (add! offset fvps-2))))
      (when (bottomp unification)
        (return-from unify4 *bottom*))
      (loop for (variable equality-list) on *equalities* by #'cddr
	    do (loop for equality in equality-list
		     do (nsubstitute! variable equality unification :test #'eql)))
      (make-fs :structure unification :bindings *bindings*))))

(defun unify! (fvps-1 fvps-2)
  (cond ((null fvps-1) fvps-2)
        ((null fvps-2) fvps-1)
        ((or (integerp fvps-1) (integerp fvps-2))
         (let* ((value-1 (if (integerp fvps-1) (getf *bindings* fvps-1) fvps-1))
                (value-2 (if (integerp fvps-2) (getf *bindings* fvps-2) fvps-2))
                (unification (unify! value-1 value-2)))
           (cond ((bottomp unification) *bottom*)
                 ((integerp fvps-1) 
                  (setf (getf *bindings* fvps-1) unification)
		  (when (integerp fvps-2) 
                    (push fvps-2 (getf *equalities* fvps-1)))
                  fvps-1)
                 (t;; fvps-2 is integerp
                  (setf (getf *bindings* fvps-2) unification)
                  fvps-2))))
        ((eq fvps-1 fvps-2) fvps-1)
        ((or (atom fvps-1) (atom fvps-2)) *bottom*)
        (t
	 (loop for (key . value-1) in fvps-1
	       for value-2 = (rest (assoc key fvps-2))
	       for unification = (unify! value-1 value-2)
	       when (bottomp unification) do
	       (return-from unify! *bottom*)
	       when (integerp value-2)
	       collect (cons key value-2) into result
	       else
	       collect (cons key unification) into result
	       finally (return (append result
				       (set-difference fvps-2 result :key #'first)))))))