;; v ::= <variable>

(define v
  (lambda (s)
    (symbol? s)))


;; t ::= <v>
;;     | (lambda <v> <t>)
;;     | (<t> <t>)

(define lambda?
  (lambda (s)
    (and (= (length s) 3)
         (equal? 'lambda (list-ref s 0)))))

(define lambda-var
  (lambda (s)
    (list-ref s 1)))

(define lambda-body
  (lambda (s)
    (list-ref s 2)))

(define application?
  (lambda (s)
    (equal? (length s) 2)))

(define t
  (lambda (s)
    (or (v s)
        (and (lambda? s)
             (v (lambda-var s))
             (t (lambda-body s)))
        (and (application? s)
             (t (list-ref s 0))
             (t (list-ref s 1))))))


;; c ::= s
;;     | k
;;     | (<c> <c>)

(define c
  (lambda (s)
    (or (equal? s 's)
        (equal? s 'k)
        (and (application? s)
             (c (list-ref s 0))
             (c (list-ref s 1))))))


;; L[I]       = &#955;x.x
;; L[K]       = &#955;x.&#955;y.x
;; L[C]       = &#955;x.&#955;y.&#955;z.(x z y)
;; L[B]       = &#955;x.&#955;y.&#955;z.(x (y z))
;; L[S]       = &#955;x.&#955;y.&#955;z.(x z (y z))
;; L[(E1 E2)] = (L[E1] L[E2])
;;
;; -- http://www.angelfire.com/tx4/cus/combinator/birds.html

(define i-combinator ;; Idiot
  '(lambda x
     x))

(define k-combinator ;; Kestrel
  '(lambda x
     (lambda y
       x)))

(define c-combinator ;; Cardinal
  '(lambda x
     (lambda y
       (lambda z
         ((x z) y)))))

(define d-combinator ;; Dove
  '(lambda x
     (lambda y
       (lambda z
         (lambda w
           ((x y) (z w)))))))

(define b-combinator ;; Bluebird
  '(lambda x
     (lambda y
       (lambda z
         (x (y z))))))

(define s-combinator ;; Starling
  '(lambda x
     (lambda y
       (lambda z
         ((x z) (y z))))))


(define l-convert
  (lambda (s)
    (cond ((equal? s 'i) i-combinator)
          ((equal? s 'k) k-combinator)
          ((equal? s 'c) c-combinator)
          ((equal? s 'd) d-combinator)
          ((equal? s 'b) b-combinator)
          ((equal? s 's) s-combinator)
          ((application? s)
           (list (l-convert (list-ref s 0))
                 (l-convert (list-ref s 1))))
          (else (error "l-convert: Invalid combinator term")))))


;; T[V] => V
;; T[(E1 E2)] => (T[E1] T[E2])
;; T[&#955;x.E] => (K T[E]) (if x is not free in E)
;; T[&#955;x.x] => I
;; T[&#955;x.&#955;y.E] => T[&#955;x.T[&#955;y.E]] (if x is free in E)
;; T[&#955;x.(E1 E2)] => (S T[&#955;x.E1] T[&#955;x.E2])

(define free?
  (lambda (v t)
    (cond ((symbol? t) (equal? v t))
          ((lambda? t) (and (not (equal? v (lambda-var t)))
                            (free? v (lambda-body t))))
          ((application? t) (or (free? v (list-ref t 0))
                                (free? v (list-ref t 1)))))))

(define t-convert
  (lambda (s)
    (cond ((v s) s)
          ((= (length s) 2)
           (list (t-convert (list-ref s 0))
                 (t-convert (list-ref s 1))))
          ((and (lambda? s)
                (not (free? (lambda-var s)
                            (lambda-body s))))
           `(k ,(t-convert (lambda-body s))))
          ((and (lambda? s)
                (equal? (lambda-var s)
                        (lambda-body s)))
           `i)
          ((and (lambda? s)
                (lambda? (lambda-body s))
                (free? (lambda-var s)
                       (lambda-body (lambda-body s))))
           (t-convert
            `(lambda ,(lambda-var s)
               ,(t-convert
                 (lambda-body s)))))
          ((and (lambda? s)
                (application? (lambda-body s)))
           `((s ,(t-convert
                   `(lambda ,(lambda-var s)
                      ,(list-ref (lambda-body s) 0))))
             ,(t-convert
               `(lambda ,(lambda-var s)
                  ,(list-ref (lambda-body s) 1))))))))