;;; checking for alpha-congruence.  Like unification or
;;; pattern-matching, but simpler.

;;; pattern-match 

;;; unify takes 4 arguments:  M1, Subj, S1, and S2, and returns a tactic.
;;; M1 and Subj are terms in internal form
;;; S1 and S2 are equal-length lists of names.
;;; returns a substitution theta on the fv's of M1 ONLY
;;; so this is like unification, except that M1 is the pattern and Subj
;;; is the subject

;;; (lambda ,S1 ,M1)theta =_alpha (lambda ,S2 ,Subj)theta
;;; if such a theta exists, we succeed and return it
;;; else we fail.

(define alpha-congruent?
  (lambda (pat subj s1 s2)
    (cond
      ((and (const? pat) (const? subj))
       (equal?
             (const->datum pat)      
             (const->datum subj)))
      ((and (var? pat) (var? subj))
       (cong-two-vars pat subj s1 s2))
      ((or (var? pat) (var? subj))
       ;; if one is a variable and the other isn't, then fail
       #f)
      ((and (app? pat) (app? subj))
       (and
         (alpha-congruent? (app->rator pat) (app->rator subj) s1 s2)
         (alpha-congruent? (app->rand pat) (app->rand subj) s1 s2)))
      ((and (abs? pat) (abs? subj))
       (alpha-congruent?
         (abs->body pat) (abs->body subj)
         (cons (abs->bv pat) s1)
         (cons (abs->bv subj) s2)))
      (else #f))))

(define cong-two-vars
  (lambda (v10 v20 s10 s20)             ; v1 is pattern variable
    (let ((v1 (var->sym v10))
          (v2 (var->sym v20)))
      (let loop ((s1 s10) (s2 s20))
        (cond
          ((and (null? s1) (null? s2))
           ;; both vars are free
           (eq? v1 v2))
          ((or (null? s1) (null? s2))
           ;; don't fail here, raise an error immediately
           (error 'match-two-vars
             "bound-variable lists had different lengths: ~s and ~s"
             s10 s20))
          ((and (eq? v1 (car s1)) (eq? v2 (car s2)))
           #t)
          ((or (eq? v1 (car s1)) (eq? v2 (car s2)))
           #f)
          (else
            (loop (cdr s1) (cdr s2))))))))

(define test-alpha-cong
  (lambda (t1 t2)
    (alpha-congruent? (parse t1) (parse t2) '() '())))