;========================UNIFICATION=====================

#| This does the substitutions sequentially rather than in parallel, and in
the reverse order from their occurrence in m. |#
(defunction sequential-sublis (m X)
    (cond ((eq (length m) 1)
                 (subst (cdr (mem1 m)) (mem1 (mem1 m)) X))
                (t (subst (cdr (mem1 m)) (mem1 (mem1 m)) (sequential-sublis (cdr m) X)))))

#| This substitutes in accordance with a match m. |#
(defunction match-sequential-sublis (m x)
    (cond ((eq m t) x)
                (t (sequential-sublis m x))))

#| This turns a sequential-match into a parallel match (to be applied by match-sublis). |#
(defunction parallelize-match (sm vars)
    (cond ((eq sm t) t)
                (t (let ((m nil))
                      (dolist (x vars)
                          (let ((x* (sequential-sublis sm x)))
                             (if (not (equal x x*)) (push (cons x x*) m))))
                      (if m m t)))))

(defun merge-sequential-matches (m m*)
    (cond ((equal m t) m*)
                ((equal m* t) m)
                (t (append m m*))))

(defunction reverse-match (m)
    (if (eq m t) t
         (mapcar #'(lambda (x) (cons (cdr x) (mem1 x))) m)))

#| If p and q have free variables in common, they must be rewritten before we can
apply the unification algorithm.  The following produces a pair of substitutions
(m1 m2) such that applying m1 to p and m2 to q unifies them.  m1 and m2 are
parallel matches to be applied by match-sublis.  The p-vars and q-vars are the 
node-variables. |#
(defunction unifier (p q p-vars q-vars)
    (cond ((and (null p-vars) (null q-vars))
               ;  (if (equal p q) (list t t)))
                 (if (or (equal p q) (notational-variant p q)) (list t t)))
                (t (catch 'unifier
                       (let ((terms (variable-correspondence p q p-vars q-vars (list nil nil nil))))
                          (unifier* (mem1 terms) (mem2 terms) p-vars q-vars))))))

(defunction ni-unifier (n m)
    (unifier (node-formula (node n)) (interest-formula (interest m))
                 (node-variables (node n)) (interest-variables (interest m))))

(defunction node-unifier (n m)
    (unifier (node-formula (node n)) (node-formula (node m))
                 (node-variables (node n)) (node-variables (node m))))

(defunction reductio-unifier (n m)
    (unifier (neg (node-formula (node n))) (node-formula (node m))
                 (node-variables (node n)) (node-variables (node m))))

#| This returns the list (terms1 terms quantifier-variables) where terms1 and terms are the lists 
of corresponding terms to be unified and quantifier-variables is the list of pairs (x . y) of
corresponding quantifier-variables used for testing for notational variants. |#
(defunction variable-correspondence (P Q P-vars Q-vars terms)
    (cond
      ((member P P-vars)
        (let ((quantifier-variables (mem3 terms)))
          (cond ((rassoc Q quantifier-variables) (throw 'unifier nil))
                    (t (list (cons P (mem1 terms)) (cons Q (mem2 terms)) quantifier-variables)))))
      ((member Q Q-vars)
        (cond ((assoc P (mem3 terms)) (throw 'unifier nil))
                  (t (list (cons P (mem1 terms)) (cons Q (mem2 terms)) (mem3 terms)))))
      ((null P)
        (cond ((null Q) terms)
                    (t (throw 'unifier nil))))
      ((null Q) (throw 'unifier nil))
      ((not (listp P))
        (cond ((not (listp Q))
                      (cond ((member Q Q-vars)
                                   (list (cons P (mem1 terms)) (cons Q (mem2 terms)) (mem3 terms)))
                                  ((eql P Q) terms)
                                  ((eql (cdr (assoc P (mem3 terms))) Q) terms)
                                  (t (throw 'unifier nil))))
                    (t (throw 'unifier nil))))
      ((not (listp Q)) (throw 'unifier nil))
      ((or (eq (car P) 'all) (eq (car P) 'some))
        (cond ((eql (car P) (car Q))
                     (variable-correspondence
                       (mem3 P) (mem3 Q) P-vars Q-vars
                       (list (mem1 terms) (mem2 terms)
                               (cons (cons (mem2 P) (mem2 Q)) (mem3 terms)))))
                    (t (throw 'unifier nil))))
      (t
        (variable-correspondence
          (cdr P) (cdr Q) P-vars Q-vars
          (variable-correspondence (car P) (car Q) P-vars Q-vars terms)))))

(defunction unifier* (p q p-vars q-vars)
   ; (let ((intersection (intersection p-vars q-vars :test 'equal)))
    (let ((intersection (intersection p-vars q-vars)))
       (cond (intersection
                    (let ((mr nil)
                            (p*-vars (setdifference p-vars intersection)))
                       (setf mr
                                (mapcar
                                  #'(lambda (x)
                                        (if (interest-variable x)
                                           (let ((x* (make-interest-variable)))
                                              (push x* p*-vars)
                                              (cons x x*))
                                           (let ((x* (make-conclusion-variable)))
                                              (push x* p*-vars)
                                              (cons x x*))))
                                  intersection))
                       (let* ((mgu (mgu (sublis mr p) q (append p*-vars q-vars)))
                               (rm (reverse-match mr)))
                          (list
                            (parallelize-match
                              (append rm (merge-sequential-matches mgu mr)) p-vars)
                            (parallelize-match (merge-sequential-matches rm mgu) q-vars)))))
                   (t (let ((mgu (mgu p q (append p-vars q-vars))))
                         (list
                           (parallelize-match mgu p-vars)
                           (parallelize-match mgu q-vars)))))))

#| (mgu p q) is a most general unifier for p and q for purposes of forwards
reasoning..  This assumes that they have no free variables in common.  vars are 
the free variables (possibly) occurring in x y.  They are assumed to be
interest-variables and node-variables.  This produces a serial match that
must be applied by match-sequential-sublis rather than match-sublis. |#
(defunction mgu (x y vars)
    (cond ((atom x)
                (cond ((eql x y) t)
                          ((member x vars)
                            (cond ((and (listp y) (eq (car y) 'q-var)) (throw 'unifier nil))
                                      ((occur x y) (throw 'unifier nil))
                                      (t (list (cons x y)))))
                          ((member y vars)
                            (cond ((and (listp x) (eq (car x) 'q-var)) (throw 'unifier nil))
                                      ((occur y x) (throw 'unifier nil))
                                      ((not (eq x '=))
                                        (list (cons y x)))
                                      (t (throw 'unifier nil))))
                          (t (throw 'unifier nil))))
              ((atom y)
                (cond ((member y vars)
                            (cond ((and (listp x) (eq (car x) 'q-var)) (throw 'unifier nil))
                                      ((occur y x) (throw 'unifier nil))
                                      (t (list (cons y x)))))
                          (t (throw 'unifier nil))))
              ((listp x)
                (cond ((not (listp y)) (throw 'unifier nil))
                          ((and (listp (cdr x)) (listp (cdr y)) (not (eql (length x) (length y)))) (throw 'unifier nil))
                          (t (mgu-list x y vars))))))

(defunction mgu-list (x y vars)
   (let ((m (mgu (mem1 x) (mem1 y) vars)))
     (cond ((null m) (throw 'unifier nil)))
     (cond ((null (cdr x)) m)
               ((eq m t)
                 (mgu-list (cdr x) (cdr y) vars))
               (t (let ((m* (mgu-list
                                   (sequential-sublis m (cdr x))
                                   (sequential-sublis m (cdr y))
                                   vars)))
                    (cond ((eq m* t) m)
                              (t (append m* m))))))))

(defunction permutations (X)
    (cond ((null X) (list nil))
                ((null (cdr X)) (list X))
                (t (let ((X1 nil) (X2 X) (permutations nil) (done nil))
                      (loop
                         (let ((y (car X2)))
                            (setf X2 (cdr X2))
                            (when (not (mem y done))
                                 (push y done)
                                 (dolist (Z (mapcar #'(lambda (p) (cons y p)) (permutations (append X1 X2))))
                                     (push Z permutations)))
                            (when (null X2) (return permutations))
                            (setf X1 (cons y X1))))))))

#| (Set-unifier X Y c-vars i-vars) returns the list of unifiers unifying X into Y. |#
;(defunction set-unifier (X Y x-vars y-vars)
;    (let ((length-x (length X))
;            (length-y (length Y)))
;       (when (<= length-x length-y)
;            (let ((unifiers nil)
;                    (n (- length-y length-x)))
;               (dolist (Y* (permutations Y))
;                   (let ((unifier (unifier X (nthcdr n Y*) x-vars y-vars)))
;                      (when unifier (pushnew unifier unifiers :test 'equal))))
;               unifiers))))

(defunction set-mgu (X Y vars)
    (cond (X
                 (let ((p (mem1 X))
                         (unifiers nil))
                    (dolist (q Y)
                        (let ((mgu (catch 'unifier (mgu p q vars))))
                           (when mgu (pushnew mgu unifiers :test 'equal))))
                    (when unifiers
                         (cond ((cdr X)
                                      (let ((new-unifiers nil))
                                         (dolist (unifier unifiers) 
                                             (let ((unifiers*
                                                       (set-mgu (match-sublis unifier (cdr X))
                                                                            (match-sublis unifier Y)
                                                                            vars)))
                                                (dolist (U unifiers*)
                                                    (push (merge-matches* unifier U) new-unifiers))))
                                         new-unifiers))
                                     (t unifiers)))))
                (t (list t))))

(defunction set-unifier (X Y X-vars Y-vars)
   ; (setf x0 x y0 y xv x-vars yv y-vars)
    (let ((intersection (intersection X-vars Y-vars)))
       (cond (intersection
                    (let ((mr nil)
                            (X*-vars (setdifference X-vars intersection)))
                       (setf mr
                                (mapcar
                                  #'(lambda (x)
                                        (if (interest-variable x)
                                           (let ((x* (make-interest-variable)))
                                              (push x* X*-vars)
                                              (cons x x*))
                                           (let ((x* (make-conclusion-variable)))
                                              (push x* X*-vars)
                                              (cons x x*))))
                                  intersection))
                       (let* ((mgus (set-mgu (sublis mr X) Y (append X*-vars Y-vars)))
                                 (rm (reverse-match mr)))
                          (mapcar
                            #'(lambda (mgu)
                                  (list
                                    (parallelize-match
                                      (append rm (merge-sequential-matches mgu mr)) X-vars)
                                    (parallelize-match (merge-sequential-matches rm mgu) Y-vars)))
                            mgus))))
                   (t (let ((mgus (set-mgu X Y (append X-vars Y-vars))))
                         (mapcar
                           #'(lambda (mgu)
                                 (list
                                   (parallelize-match mgu X-vars)
                                   (parallelize-match mgu Y-vars)))
                           mgus))))))

#|
(set-unifier '((F c) (G y)) '((G a) (H c) (G b) (F z)) '(x y) '(z))
yields ((((y . a)) ((z . c))) (((y . b)) ((z . c))))
|#

#| This checks that interest-variables in vars1 and vars2 do not instantiate
each other.
(defunction constrained-assignment (unifier vars1 vars2)
    (let ((u1 (mem1 unifier)))
       (or (eq u1 t)
             (not (some
                       #'(lambda (v)
                             (some #'(lambda (w) (occur w (e-assoc v u1))) vars2))
                       vars1))))
    (let ((u2 (mem2 unifier)))
       (or (eq u2 t)
             (not (some
                       #'(lambda (v)
                             (some #'(lambda (w) (occur w (e-assoc v u2))) vars1))
                       vars2)))))
 |#

#| This checks that interest-variables in vars1 and vars2 are not instantiated
by terms containing those same variables. |#
(defunction constrained-assignment (unifier vars1 vars2)
    (let ((u1 (mem1 unifier)))
       (or (eq u1 t)
             (not (some #'(lambda (v) (occur v (e-assoc v u1))) vars1))))
    (let ((u2 (mem2 unifier)))
       (or (eq u2 t)
             (not (some #'(lambda (v) (occur v (e-assoc v u2))) vars2)))))

;=====================================================================