;;; substitution

;;; subst ::= (unit-subst varsym term) | (comp-subst subst subst) 
;;;           | (empty-subst)

(define-record unit-subst (varsym term))
(define-record empty-subst ())
(define-record comp-subst (subst1 subst2)) ; subst1 followed by subst2

(define comp-subst
  (lambda (s1 s2)
    (cond
      ((empty-subst? s1) s2)
      ((empty-subst? s2) s1)
      (else (make-comp-subst s1 s2)))))

(define gensym
  (let ((counter 0))
    (lambda (sym)
      (set! counter (+ 1 counter))
      (string->symbol
        (string-append (symbol->string sym) (number->string
                                              counter))))))

(define rember
  (lambda (sym syms)
    (cond
      ((null? syms) '())
      ((eq? (car syms) sym)
       (rember sym (cdr syms)))
      (else (cons (car syms)
                  (rember sym (cdr syms)))))))

(define set-cons
  (lambda (sym set)
    (if (memq sym set) set
      (cons sym set))))

(define fv
  (lambda (term)
    (let loop ;; computes (union (fv term) set).  This avoids an N^2
              ;; union at applications.
      ((term term)
       (set '()))
      (record-case term
        (const (c) set)
        (var (id) (set-cons id set))
        (app (rator rand)
             (loop rand (loop rator set)))
        (abs (bv body)
             (rember bv (loop body set)))
        (else 
          (report-bad-term 'rember term))))))

(define non-empty-intersection?
  (lambda (set1 set2)
    (let loop ((set1 set1))
      (if (null? set1) #f
        (if (memq (car set1) set2) #t
          (loop (cdr set1)))))))

(define subst
  (lambda (term s)
    (record-case s
      (empty-subst () term)
      (unit-subst (varsym term1) (subst1 term term1 varsym))
      (comp-subst (s1 s2) (subst (subst term s1) s2))
      (else (error 'subst "bad substitution ~s" s)))))

(define subst1
  (lambda (term new old)
    (let ((fv-of-new (fv new)))
      (let subst-loop ((term term))
        (record-case term
          (const (c) term)
          (var (id)
               (if (eq? id old) new term))
          (app (rator rand)
               (make-app (subst-loop rator) (subst-loop rand)))
          (abs (bv body)
               (cond
                 ((eq? bv old) term)
                 ((and (memq bv fv-of-new)
                       (memq old (fv body)))
                  (let ((newvar (gensym bv)))
                    (make-abs newvar
                      ;; this subst could be replaced by something faster
                      (subst-loop (subst1 body (make-var newvar) bv)))))
                 (else
                   (make-abs bv (subst-loop body)))))
          (else (report-bad-term 'subst term)))))))

(define test-subst1
  (lambda (term new old)
    (unparse 
      (subst1 (parse term) (parse new) old))))