private/unify.ss
#lang scheme
(require "../ast.ss"
         "env.ss")

(define (chase env t)
  (match t
    [(struct variable (_ var))
     (cond
       [(lookup env var)
        => (lambda (term) (chase env term))]
       [else t])]
    [_ t]))

(define (unify-term env t1 t2)
  (define t1-p (chase env t1))
  (define t2-p (chase env t2))
  (if (term-equal? t1-p t2-p)
      env
      (match t1-p
        [(struct variable (_ var))
         (extend env var t2-p)]
        [_
         (match t2-p
           [(struct variable (_ var))
            (extend env var t1-p)]
           [_
            #f])])))

(define (unify-terms env ts1 ts2)
  (if (empty? ts1)
      (if (empty? ts2)
          env
          #f)
      (if (empty? ts2)
          #f
          (match (unify-term env (first ts1) (first ts2))
            [#f #f]
            [env (unify-terms env (rest ts1) (rest ts2))]))))      

(define (unify l1 l2)
  (and (datum-equal? (literal-predicate l1)
                     (literal-predicate l2))
       (unify-terms (empty-env)
                    (literal-terms l1)
                    (literal-terms l2))))

(provide/contract
 [unify (literal? literal? . -> . (or/c false/c env/c))]
 [unify-term (env/c term/c term/c . -> . (or/c false/c env/c))])