;;; unification to within alpha-congruence.

;;; This is krivine-machine file-- needs to be ripped up and revised.

;;; Grammar:

;;; external syntax
;;; M ::= string | int | var | (lambda (var...) M) | (M1 ... Mn)

;;; internal syntax
;;; term ::= (var id) | (const c) | (app term term) | (abs sym term) 

;;; subst ::= ((var term) ...)

(define-record const (c))
(define-record var (id)
(define-record app (rator rand))
(define-record abs (bv body))

(define-record unit-subst (id term))

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

(define parse
  (lambda (external)
    (let loop
      ((exp external) (symtab '()))
      (cond
        ((or (string? exp) (number? exp))
         (make-const exp))
        ((symbol? exp) 
         (let loop
           ((tab symtab)(acc 0))
           (cond
             ((null? tab) 
              ;; not in symtab.  Must be a constant
              (make-const exp))
             ((eq? exp (car tab)) 
              (make-var acc))
             (else (loop (cdr tab) (+ acc 1))))))
        ((and
           (eq? (car exp) 'lambda)
           (= (length exp) 3))
         (let inner
           ((vars (if (symbol? (cadr exp)) 
                    (list (cadr exp))
                    (cadr exp)))
            (symtab symtab))
           (if (null? vars)
             (loop (caddr exp) symtab)
             (make-abs
               (inner (cdr vars) (cons (car vars) symtab))))))
        ((pair? exp)
         (case (length exp)
           ((0)
            (error 'external-internal "ran off end processing ~s"
              external))
           ((1)
            (loop (car exp) symtab))
           ((2)
            (make-app
              (loop (car exp) symtab)
              (loop (cadr exp) symtab)))
           (else
             (loop
               (cons 
                 (list (car exp) (cadr exp))
                 (cddr exp))
               symtab))))
        (else
          (error 'external->internal
            "unknown external form ~s" exp))))))

(define unparse
  (lambda (internal)
    (record-case internal
      (const (c) c)
      (var (id) id)
      (app (rator rand)
           (let app-loop
             ((spine rator)
              (acc   (list (unparse rand))))
             (record-case spine
               (app (rator rand)
                    (app-loop rator
                      (cons (unparse rand) acc)))
               (else (cons (unparse rator) (reverse acc))))))
      (abs (bv body)
           (let abs-loop
             ((vars (list bv))
              (term body))
             (record-case term
               (abs (bv body)
                    (abs-loop (cons bv vars) body))
               (else `(lambda ,(reverse vars) (unparse term))))))
      (else (error 'unparse "unknown internal form ~s" internal)))))

(define S '(lambda (x y z) ((x z) (y z))))         

(define I '(lambda x x))

(define K '(lambda (x y) x))
           
(define Theta '((lambda (d) (d d))
                (lambda (x f) (f (x x f)))))

(define term1 `((lambda y (y y y))
                (lambda (a b) a)
                ,I
                (,S ,S)))

(define term2 `((,S ,K) (,S ,K ,K) (,S ,I)))

(define term3 `(,S ,S ,S ,S ,S ,S))

(define term4 `(,S (,S ,S) (,S ,S) (,S ,S) ,S ,S))