;;; unification to within alpha-congruence.

;;; parse.s: grammar and some help functions

;;; 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) 

(define-record const (datum))
(define-record var (sym))
(define-record app (rator rand))
(define-record abs (bv body))

(define parse
  (lambda (external)
    (let loop
      ((exp external))
      (cond
        ;; constants are strings, numbers, or quoted symbols
        ((or (string? exp) (number? exp)
           (and (pair? exp)
                (= (length exp) 2)
                (eq? (car exp) 'quote)
                (symbol? (cadr exp))))
         (make-const exp))
        ((symbol? exp) 
         (make-var exp))
        ((and
           (eq? (car exp) 'lambda)
           (= (length exp) 3))
         (let abs-loop
           ((vars (if (symbol? (cadr exp)) 
                    (list (cadr exp))
                    (cadr exp))))
           (if (null? vars)
             (loop (caddr exp))
             (make-abs (car vars) (abs-loop (cdr vars))))))
        ((pair? exp)
         (case (length exp)
           ((0)
            (error 'parse "ran off end processing ~s"
              external))
           ((1)
            (loop (car exp) symtab))
           ((2)
            (make-app
              (loop (car exp))
              (loop (cadr exp))))
           (else
             (loop
               (cons 
                 (list (car exp) (cadr exp))
                 (cddr exp))))))
        (else
          (error 'parse 
            "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 internal)
              (acc   '()))
             (record-case spine
               (app (rator rand)
                    (app-loop rator
                      (cons (unparse rand) acc)))
               (else (cons (unparse spine) 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 (report-bad-term 'unparse internal)))))

(define report-bad-term
  (lambda (site term)
    (error site "bad term ~s" term)))

(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))