(define (metavar? x)
  (and (symbol? x)
       (eqv? #\? (string-ref (symbol->string x) 0))))

(define (unify-with binds s1 s2)
  (cond ((metavar? s1) (add-binding binds s1 s2))
	((metavar? s2) (add-binding binds s2 s1))
	((and (pair? s1) (pair? s2))
	 (let ((new-binds (unify-with binds (car s1) (car s2))))
	   (if new-binds (unify-with new-binds (cdr s1) (cdr s2)) #f)))
	((equal? s1 s2) binds)
	(else #f)))

(define (add-binding binds var defn)
  (cond ((assv var binds)
	 => (lambda (old-bind)
	      (unify-with binds defn (cadr old-bind))))
	(else (cons (list var defn) binds))))

(define (fill-template template binds)
  (let fill ((tl template))
    (cond ((and (metavar? tl) (assv tl binds))
	   => (lambda (binding) (fill (cadr binding))))
	  ((pair? tl) (cons (fill (car tl)) (fill (cdr tl))))
	  (else tl))))

(define (fill-binds binds)
  (define (fill-defn bind)
    (cons (car bind) (fill-template (cdr bind) binds)))
  (if binds (map fill-defn binds) #f))

(define (unify s1 s2)
  (fill-binds (unify-with '() s1 s2)))