(define equal-term?
  (lambda (t u)
    (cond
      [(and (symbol? t) (symbol? u)) (if (eqv? t u) #t #f)]
      [(symbol? t) #f]
      [(symbol? u) #f]
      [(and (constant? t) (constant? u)) (if (equal? t u) #t #f)]
      [(constant? t) #f]
      [(constant? u) #f]
      [(and (list? t) (list? u)) (equal-terms? t u)]
      [(list? t) #f]
      [(list? u) #f])))

(define equal-terms?
  (lambda (t* u*)
    (cond
      [(and (null? t*) (null? u*)) #t]
      [(or (null? t*) (null? u*)) #f]
      [else
        (let ((car-okay? (equal-term? (car t*) (car u*))))
          (if (not car-okay?)
              #f
              (let ((cdr-okay? (equal-terms? (cdr t*) (cdr u*))))
                (if (not cdr-okay?)
                    #f
                    #t))))])))

(define var? symbol?)

(define unify
  (lambda (t u)
    (unify-term t u
                (lambda (subst) subst)
                (lambda () #f))))

(define unify-term
  (lambda (t u sk fk)
    (cond
      [(and (var? t) (var? u)) (sk (unit-subst t u))]
      [(var? t)
       (if (occurs? t u) (fk) (sk (unit-subst t u)))]
      [(var? u)
       (if (occurs? u t) (fk) (sk (unit-subst u t)))]
      [(and (constant? t) (constant? u))
       (if (equal? t u) (sk (empty-subst)) (fk))]
      [(or (constant? t) (constant? u)) (fk)]
      [(and (list? t) (list? u)) (unify-terms t u sk fk)]
      [else (fk)])))

(define unify-terms
  (lambda (t* u* sk fk)
    (cond
      [(and (null? t*) (null? u*)) (sk (empty-subst))]
      [(or (null? t*) (null? u*)) (fk)]
      [else (unify-term (car t*) (car u*)
                        (lambda (subst-car)
                          (unify-terms
                            (subst-in-terms (cdr t*) subst-car)
                            (subst-in-terms (cdr u*) subst-car)
                            (lambda (subst-cdr)
                              (sk (compose-substs subst-car subst-cdr)))
                            fk))
                        fk)])))

;;; ----------------------------------------------------
;;;
;;; These are the functions where it becomes obvious that
;;; substitutions are represented as functions: (lambda (id) id),
;;; (lambda (id2) (if (eqv? id2 id) term id2)), and (lambda (id)
;;; (subst-in-term (apply-subst s1 id) s2).  For your homework, these
;;; three lambda terms must be represented with three distinct data
;;; structures (a data type) that are dispatched over using either
;;; match or cases in the definition of apply-subst.

(define empty-subst
  (lambda ()
    (lambda (id) id)))

(define unit-subst
  (lambda (id term)
    (if (eqv? id term)
        (empty-subst)
        (lambda (id2)
          (if (eqv? id2 id) term id2)))))

(define compose-substs
  (lambda (s1 s2)
    (lambda (id)
      (subst-in-term (apply-subst s1 id) s2))))

;;; --------------------------------------------------
;;;
;;; By introducing apply-subst, like apply-env, we have
;;; hidden the knowledge that subst is represented as
;;; a function.  You might rewrite these programs without
;;; apply-subst. Then it will become even more obvious that
;;; substitutions are represented as functions.

(define apply-subst
  (lambda (subst id)
    (subst id)))

(define subst-in-term
  (lambda (term subst)
    (cond
      ((symbol? term) (apply-subst subst term))
      ((constant? term) term)
      ((list? term) (subst-in-terms term subst)))))

;;; -----------------------------------------------------

(define subst-in-terms
  (lambda (term* subst)
    (map (lambda (t) (subst-in-term t subst)) term*)))

(define occurs?
  (lambda (var term)
    (memq var (all-ids term))))

(define all-ids
  (lambda (term)
    (cond
      [(symbol? term) (list term)]
      [(constant? term) '()]
      [(list? term) (map-union all-ids term)])))

(define map-union
  (lambda (f ls)
    (cond
      [(null? ls) '()]
      [else (union (f (car ls)) (map-union f (cdr ls)))])))

(define union
  (lambda (set1 set2)
    (cond
      [(null? set1) set2]
      [(memq (car set1) set2) (union (cdr set1) set2)]
      [else (cons (car set1) (union (cdr set1) set2))])))

(define constant?
  (lambda (c)
    (or (string? c) (number? c) (boolean? c))))

(define b (equal-term? '(R (V (W X) 8)) '(R (V (W X) 8))))
(define s (unify '(R (V (W X) 8)) '(R (U ("abc" U) X))))