(use srfi-1) ; lset-union

;; helpers

(define (variable? x)
  (and (symbol? x)
       (< 1 (string-length (symbol->string x)))
       (eqv? #\? (string-ref (symbol->string x) 0))))

(define (constant? x)
  (and (symbol? x)
       (not (variable? x))))

;; unification

(define (unify/binds binds s1 s2)
  (cond ((variable? s1) (unify-binding binds s1 s2))
	((variable? s2) (unify-binding binds s2 s1))
	((and (pair? s1) (pair? s2))
	 (let ((new-binds (unify/binds binds (car s1) (car s2))))
	   (and new-binds (unify/binds new-binds (cdr s1) (cdr s2)))))
	((equal? s1 s2) binds)
	(else #f)))

(define (unify-binding binds var defn)
  (cond ((assoc var binds)
	 => (lambda (old-bind)
	      (unify/binds binds defn (cadr old-bind))))
	(else (cons (list var defn) binds))))

(define (unify s1 s2)
  (let ((binds (unify/binds '() s1 s2)))
    (and binds (fill-template s1 (fill-binds binds)))))

;; generality (or subsumption) relation

(define (generalises/binds binds s1 s2)
  (cond ((variable? s1) (add-binding binds s1 s2))
	((and (pair? s1) (pair? s2))
	 (let ((new-binds (generalises/binds binds (car s1) (car s2))))
	   (and new-binds (generalises/binds new-binds (cdr s1) (cdr s2)))))
	((equal? s1 s2) binds)
	(else #f)))

(define (add-binding binds var defn)
  (let ((old-binding (assoc var binds)))
    (cond ((not old-binding) (cons (list var defn) binds))
	  ((equal? defn (cadr old-binding)) binds)
	  (else #f))))

(define (generalises s1 s2) (generalises/binds '() s1 s2))
(define at-least-as-generic? generalises)

;; unflattening of bindings

(define (fill-template template binds)
  (cond ((assoc template binds) => cadr)
	((pair? template) (cons (fill-template (car template) binds)
				(fill-template (cdr template) binds)))
	(else template)))

(define (fill-binds binds)
  (if (null? binds) binds
    (let* ((var (caar binds))
	   (rest-binds (fill-binds (cdr binds)))
	   (expansion (fill-template (cadar binds) rest-binds)))
      (cons (list var expansion)
	    (substitute var expansion rest-binds)))))

;; variable rewriting

;(define gensym
;  (let ((serial 0))
;    (lambda (str)
;      (set! serial (+ serial 1))
;      (string->symbol (string-append str (number->string serial))))))

(define (generate-variable) (gensym "?G"))
(define (generate-constant) (gensym "const"))

(define (generated-variable? x)
  (and (variable? x) ; XXX depends on |?| not being variable
       (eqv? #\G (string-ref (symbol->string x) 1))))

(define (variables form)
  (cond ((variable? form) (list form))
	((pair? form)
	 (lset-union equal? (variables (car form)) (variables (cdr form))))
	(else '())))

(define (rewrite-variables form)
  (fill-template form (map (lambda (var) (list var (generate-variable)))
			   (variables form))))

(define (variable->constant var)
  (string->symbol (string-append "co" (symbol->string var))))

(define (rewrite-variables-into-constants term)
  (cond ((variable? term) (variable->constant term))
	((pair? term)
	 (cons (rewrite-variables-into-constants (car term))
	       (rewrite-variables-into-constants (cdr term))))
	(else term)))