;;; unification 

;;; unify takes 4 arguments:  M1, M2, S1, and S2, and returns a tactic.
;;; M1 and M2 are terms in internal form
;;; S1 and S2 are equal-length lists of names.
;;; returns a substitution theta s.t. 
;;; (lambda ,S1 ,M1)theta =_alpha (lambda ,S2 ,M2)theta
;;; if such a theta exists, we succeed and return it
;;; else we fail.

(define unify
  (lambda (m1 m2 s1 s2)
    (cond
      ((and (const? m1) (const? m2))
       (if (equal?
             (const->datum m1)      
             (const->datum m2))
         (succeed (make-empty-subst))
         (fail)))
      ((and (var? m1) (var? m2))
       (unify-two-vars m1 m2 s1 s2))
      ((var? m1)
       (unify-one-var m1 m2 s1 s2))
      ((var? m2)
       (unify-one-var m2 m1 s2 s1))
      ((and (app? m1) (app? m2))
       (and-then
         (unify (app->rator m1) (app->rator m2)
           s1 s2)
         (lambda (theta)
           (and-then
             (unify (subst (app->rand m1) theta)
                    (subst (app->rand m2) theta)
                    s1 s2)
             (lambda (theta2)
               (succeed (comp-subst theta theta2)))))))
      ((and (abs? m1) (abs? m2))
       (unify (abs->body m1) (abs->body m2)
         (cons (abs->bv m1) s1)
         (cons (abs->bv m2) s2)))
      (else (fail)))))

(define unify-two-vars
  (lambda (v10 v20 s10 s20)
    (let ((v1 (var->sym v10))
          (v2 (var->sym v20)))
      (let loop ((s1 s10) (s2 s20))
        (cond
          ((and (null? s1) (null? s2))
           (succeed (make-unit-subst v1 (make-var v2))))
          ((or (null? s1) (null? s2))
           ;; don't fail here, raise an error immediately
           (error 'unify-two-vars
             "bound-variable lists had different lengths: ~s and ~s"
             s10 s20))
          ((and (eq? v1 (car s1)) (eq? v2 (car s2)))
           (succeed (make-empty-subst)))
          ((or (eq? v1 (car s1)) (eq? v2 (car s2)))
           (fail))
          (else
            (loop (cdr s1) (cdr s2))))))))

(define unify-one-var
  (lambda (vm1 m2 s1 s2)
    (let ((v1 (var->sym vm1)))
      (if
        (and
          (not (memq v1 s1))
          (not (non-empty-intersection?
                 (cons v1 s2)
                 (fv m2)))
          )
        (succeed (make-unit-subst v1 m2))
        (fail)))))

(define test-unify
  (lambda (t1 t2)
    (let ((t1 (parse t1))
          (t2 (parse t2)))
      (run-tac
        (unify t1 t2 '() '())
        (lambda (theta)
          (display* theta (subst t1 theta) (subst t2 theta)))
        (lambda () 'non-unifiable)))))