;;; $Id: combinator-tools.scm,v 1.3 2006/01/05 22:24:09 leavens Exp $

;;; The algorithms toCombinators and toLambda are
;;  from Hindley, Lercher and Seldin's book
;;;     "Introduction to Combinatory Logic", Cambridge, 1972)

(module combinator-tools (lib "typedscm.ss" "typedscm")

(provide toCombinators interpret lambda-calculus-rep toLambda)

(require
 ;; For the input grammar, <expression>, see the following file:
 (lib "combinator-lambda-1-exp.scm" "lib342")
 ;; For the output grammar, <combinator-term>, see the following file:
 (lib "combinator-term-mod.scm" "lib342"))

;;; Examples:
;;; (unparse-combinator-term
;;;   (toCombinators (parse-expression '(lambda (x) (lambda (y) x)))))
;;;  ==> k
;;; (unparse-combinator-term
;;;   (toCombinators (parse-expression '(lambda (x) (lambda (y) y)))))
;;;  ==> (k i)

(deftype toCombinators (-> (expression) combinator-term))
(define toCombinators
  (lambda (exp)
    (cases expression exp
      (var-exp (id) (var id))
      (app-exp (rator rand)
               (capp (toCombinators rator) (toCombinators rand)))
      (lambda-exp (formal body)
        (if (not (occurs-free-in? formal body))
            (capp (K) (toCombinators body))
            (let ((outer-formal formal))
              (cases expression body
                (var-exp (id) (I))   ; because formal == id here
                (lambda-exp (inner-formal inner-body)
                  (toCombinators
                   (lambda-exp outer-formal
                               (toLambda (toCombinators body)))))
                (app-exp (rator rand)
                     (if (and (equal? rand (var-exp outer-formal))
                              (not (occurs-free-in? outer-formal rator)))
                         (toCombinators rator)  ; eta rule
                         (capp
                          (capp (S)
                                (toCombinators
                                 (lambda-exp outer-formal rator)))
                          (toCombinators (lambda-exp outer-formal rand)))))
                (else (toCombinators body))))))
      (LI () (I))
      (LS () (S))
      (LK () (K))
      (else (error "bad expression: " exp)))))

(deftype interpret (-> (combinator-term) combinator-term))
(define interpret
  (lambda (trm)
    ;; ENSURES LIBERALLY: result is the normal form of trm
    (displayln (unparse-combinator-term trm) " ==> ")
    (cond
     ((capp-of-I? trm) (interpret (capp->rand trm)))
     ((capp-of-K? trm) (interpret (capp->rand (capp->rator trm))))
     ((capp-of-S? trm)
      (interpret (capp
                  (capp (capp->rand (capp->rator (capp->rator trm)))
                        (capp->rand trm))
                  (capp (capp->rand (capp->rator trm))
                        (capp->rand trm)))))
     (else trm))))

(deftype capp-of-I? (-> (combinator-term) boolean))
(define capp-of-I?
  (lambda (trm)
    (and (capp? trm)
         (I? (capp->rator trm)))))

(deftype capp-of-K? (-> (combinator-term) boolean))
(define capp-of-K?
  (lambda (trm)
    (and (capp? trm)
         (capp? (capp->rator trm))
         (K? (capp->rator (capp->rator trm))))))

(deftype capp-of-S? (-> (combinator-term) boolean))
(define capp-of-S?
  (lambda (trm)
    (and (capp? trm)
         (capp? (capp->rator trm))
         (capp? (capp->rator (capp->rator trm)))
         (S? (capp->rator (capp->rator (capp->rator trm)))))))


(deftype lambda-calculus-rep (-> () poof))
(define lambda-calculus-rep
  (lambda ()
    ;; EFFECT: read, interpret, and print lambda calculus expressions.
    ;;         You can enter combinator terms directly by using LS, LK, and LI.
    ;;         You can quit by typing in something that doesn't parse, like
    ;;            (quit)
    (display "lambda-calculus> ")
    (force-output)   ; SCM specific
    (pretty-print
     (unparse-combinator-term
      (interpret
       (toCombinators
        (parse-expression
         (read))))))
    (newline)
    (lambda-calculus-rep)))

;;; The toLambda function is used internally above;
;;; it does not attempt to recover the initial forma of a lambda term,
;;; which would (in general) be impossible anyway.

(deftype toLambda (-> (combinator-term) expression))
(define toLambda
  (lambda (ctrm)
    (cases combinator-term ctrm
      (I () (LI))
      (K () (LK))
      (S () (LS))
      (var (symbol) (var-exp symbol))
      (capp (rator rand) (app-exp (toLambda rator) (toLambda rand)))
      )))

(deftype occurs-free-in? (-> (symbol expression) boolean))
(define occurs-free-in?
  (lambda (sym trm)
    ;; ENSURES: result is true just when sym occurs free in trm
    (cases expression trm
     (var-exp (id) (eq? sym id))
     (lambda-exp (formal body)
       (and (not (eq? sym formal)) (occurs-free-in? sym body)))
     (app-exp (rator rand)
       (or (occurs-free-in? sym rator)
           (occurs-free-in? sym rand)))
     (else #f))))

) ;; end module