;;; -*- Mode:Lisp; Package:User; Syntax:Common-Lisp; Base:10;-*-
;;; ************************************************************************
;;; FLAIR PROJECT
;;; ************************************************************************
;;; Filename:   unify-alg.cl
;;; ========================================================================
;;; The UNIFICATION ALGORITHM. 
;;; It is derived from Chang+Lee: Symbolic Logic etc. pp77-78
;;; We assume that variables are symbols starting with '?', like
;;; ?X, ?X213, ?JOHN
;;; Substitutions [or assignments] are represented as association lists whose
;;; keys are variables. For example, ((?X (F A)) (?Z B))
;;; Unification is applied to literals in prefix form. For example,
;;; (F (G ?X A) (H ?Y) C) and (F ?Z ?X ?Y) are literals in prefix form.
;;; Their most general unifier is ((?Y  C) (?X (H C)) (?Z (G (H C) A))).
;;; NOTE: This code can be used as is (no additional code is required).
;;;-------------------------------------------------------------------------


(defun varp (x)
  ;; To check to see if something is a variable, just check to see if the
  ;; first character is a "?".
  ;; For example, (varp '?A) => T,  (varp "Ann") => nil.
  (and (symbolp x)
       (char= (char (symbol-name x) 0) '#\?)))

(defun occurs (f1 f2)
  ;; It determines if the variable F1 appears anywhere in F2.
  ;; For example (occurs '?X '(F A (G ?X B) C)) => T.
  (if (varp f2) 
      (string-equal f1 f2)
    (unless (atom f2) 
      (or (occurs f1 (first f2))
          (occurs f1 (rest f2))))))

(defun replace-variables (s a-list &aux x)
  ;; We replace in S all occurrences of variables
  ;; by the value they have in the variable assignment A-LIST
  ;; For example (replace-variables '(H (K ?X ?Y) D))  '((?X  A) (?Y (F B))).
  ;; => (H (K A (F B)) D) 
  (cond ((varp s)
         (setq x (assoc s a-list))
         (if x 
             (second x)
             s))
        ((atom s) s)
        (t (cons (replace-variables (first s) a-list)
                 (replace-variables (rest s) a-list)))))

(defun composition (assignement1 assignement2)
  ;; This is function composition as used in logic. For example
  ;;  (COMPOSITION '((?X (F ?Z A)) (?Y (G ?W))) '((?Z B) (?U C))) 
  ;; =>    ((?X (F B A)) (?Y (G ?W)) (?Z B) (?U C))
  (append
   (mapcar
    #'(lambda (var-pair)
        (list (first var-pair)
              (replace-variables (second var-pair) assignement2)))
    assignement1)
   (remove-if-not 
    #'(lambda (x) (member (first x) (set-difference (mapcar #'first assignement2)
                                            (mapcar #'first assignement1)
                                            :test #'string-equal)
                          :test #'string-equal))
    assignement2)))

(defun find-difference (form1 form2)
  ;; Given two forms, it scans them left-to-right until it finds
  ;; the first position where they differ. It returns 'FAIL, if unification 
  ;; is not possible, nil, if they don't differ, otherwise a pair
  ;; (variable value) of the first location in matching the forms where a
  ;;  variable must be instantiated.
  ;;  For example (FIND-DIFFERENCE '(P A (G ?A B) C) '(P A (G (F C) B) C))
  ;;  => (?A (F C))
  (cond ((varp form1)
         (cond ((eq form1 form2) nil)
               ((occurs form1 form2) 'fail)
               (t (list form1 form2))))
        ((varp form2)
         (if (occurs form2 form1) 
             'fail
           (list form2 form1)))
        ((or (atom form1) (atom form2))
         (if (eq form1 form2) 
             nil
           'fail))
        (t
         (or (find-difference (first form1) (first form2))
             (find-difference (rest form1) (rest form2))))))
;
(defun unify (form1 form2 &optional assignement
                        &aux (difference-set (find-difference form1 form2)))
  ;; Given two forms and a substitution ASSIGNEMENT, 
  ;; it returns, if they are unifiable with an extension of ASSIGNEMENT, 
  ;; the Most General Unifier (MGU) and the corresponding form, called
  ;; Most General Instance (MGI); otherwise it returns NIL.
  ;; For example, (unify '(F (G ?X A) (H ?Y) C) '(F ?Z ?X ?Y))
  ;; => ((?Z (G (H C) A)) (?X (H C)) (?Y  C)) ; This is the MGU
  ;; => (F (G (H C) (K C) C))  ; This is the MGI.

  (if (null difference-set) 
      (values assignement form1)
    (if (atom difference-set) 
        (values nil nil)
      (unify (subst (second difference-set)
                    (first  difference-set)
                    form1 :test 'equal)
             (subst (second difference-set)
                    (first difference-set)
                    form2 :test 'equal)
             (composition assignement (list difference-set))))))
;;;-------------------------------------------------------------------------