(load "cpsE.ss")

;===============================================================================
;;; Prior to binding 'k, we might discover that there is only one
;;; free occurrence of 'k in the body, so rather than binding the
;;; cont-exp, we inline it.  beta/k might do another beta step,
;;; since the one occurrence of 'k might be in rator position of an
;;; application.

(define possible-letk
  (lambda (cont-exp abs-body)
    (let ([k-var (if (symbol? cont-exp)
                   cont-exp
                   (generate-k))])
      (possible-letk-body k-var cont-exp (abs-body k-var)))))

(define possible-letk-body
  (lambda (k-var cont-exp body)
    (cond
      [(eqv? cont-exp k-var) body]
      [(symbol? cont-exp) (beta-subst cont-exp k-var body)]
      [(occurs-exactly-once? k-var (free-var-list body))
       (beta/k k-var cont-exp body)]  ; inlining here; +? beta step, too.
      [else `(let ((,k-var ,cont-exp)) ,body)])))

;;; Watch out for the rare practical use of memq's bizzare return value.

(define occurs-exactly-once?
  (lambda (id ls)
    (let ((x (memq id ls)))
      (if (not x) ;; if x is true, at least one.
          #f
          (not (memq id (cdr x)))))))

;;; The procedure poss-app is used once in beta/k and once in
;;; beta-substf.  It takes the result of the possible beta step
;;; referred to above and if it is an application, it turns it into a
;;; let, but since the last item bound is to k, it re-invokes
;;; possible-letk.  This is a very subtle piece of code, since a call
;;; to possible-letk can lead back to a call to poss-app, thus lots
;;; of safe in-lining can take place as a result of the first call to
;;; poss-app.  Why is this possible?  We know that all the operands to
;;; a non-continuation lambda in a function position of an application
;;; are values.  Furthermore, we know that the last one is a
;;; continuation, which must be either the k symbol or another
;;; CLAM expression.  So, all but the last operand can be bound by a
;;; let(*) and the last one passes its body to possible-letk.  We
;;; know that the formal for the last one must be k, which makes
;;; this call to poss-app safe.

(define poss-app
  (lambda (exp)
    (match exp
      [((lambda (,id) ,body) ,cont-exp)
       (possible-letk-body id cont-exp body)]
      [((lambda (,id1 ,id* ...) ,body) ,value-rand1 ,value-rand* ...)
       `(let ((,id1 ,value-rand1))
          ,(poss-app `((lambda ,id* ,body) ,@value-rand*)))]
      [,no exp])))

;;; Substitute lam-exp for the one free occurrence of the k symbol, being
;;; careful not to capture the free variables of its first argument,
;;; which must be a lambda expression.

(define beta/k
  (lambda (k-var clam-exp exp)
    (match exp
      [,var (guard (symbol? var))
        (if (eq? var k-var) clam-exp var)]
      [,constant
        (guard (or (number? constant) (boolean? constant)))
        constant]
      [(APk ,k ,value)
       (guard (eq? k k-var))
       (match clam-exp
         [(CLAM (,v-id) ,e) ;;; inlining here.
          (if (occurs-exactly-once? v-id (free-var-list e))
              (poss-app (beta-substf value v-id e))
              `(let ((,v-id ,value))
                 ,e))]
         [,other (error 'beta/k "APk-case: unmatched expression: ~a"
                        `(APk ,k ,value))])]
      [(APk ,cont ,rand)
       `(APk ,(beta/k k-var clam-exp cont)
             ,(beta/k k-var clam-exp rand))]
      [(CLAM (,id) ,body)
       `(CLAM (,id) ,(beta/k k-var clam-exp body))]
      [(lambda (,id* ...) ,body)
       `(lambda (,id* ...) ,body)]
      [(if ,test-exp ,true-exp ,false-exp)
       `(if ,(beta/k k-var clam-exp test-exp)
            ,(beta/k k-var clam-exp true-exp)
            ,(beta/k k-var clam-exp false-exp))]
      [(,prim ,rand* ...)
       (guard (primitive? prim))
       `(,prim ,@(map (lambda (rand) (beta/k k-var clam-exp rand)) rand*))]
      [(let ((,id ,rand)) ,body)
       (guard (free? id clam-exp))
       (beta/k
         k-var clam-exp
         (let ((g-id (fresh-var (fresh-var id))))
           `(let ((,g-id ,rand))
              ,(beta-subst g-id id body))))]
      [(let ((,id ,rand)) ,body)
       `(let ((,id ,(beta/k k-var clam-exp rand)))
          ,(beta/k k-var clam-exp body))]
      [(letrec ((,name* (lambda (,ids* ...) ,body*)) ...)
         ,body)
       (guard (disjoint? name* (free-vars clam-exp)))
       `(letrec ,(map list name*
                      (map (lambda (ids body)
                             `(lambda (,ids ...) ,body))
                           ids* body*))
          ,(beta/k k-var clam-exp body))]
      [(letrec ((,name* (lambda (,ids* ...) ,body*)) ...)
         ,body)
       (beta/k
         k-var clam-exp
         (let ((x (car (intersection name* (free-vars clam-exp)))))
           (let ((g-id (fresh-var (fresh-var x))))
             `(letrec ,(map list (subst g-id x name*)
                            (map (lambda (ids body)
                                   (if (memq x ids)
                                       `(lambda ,ids ,body)
                                       `(lambda ,(subst g-id x ids)
                                          ,(beta-subst g-id x body))))
                                 ids* body*))
                ,(beta-subst g-id x body)))))]
      [(,rator ,rand* ...)
       `(,(beta/k k-var clam-exp rator)
          ,@(map (lambda (x) (beta/k k-var clam-exp x)) rand*))]
      [,other (error 'beta/k "Invalid expression ~s" other)])))

;;; This is the same as beta-subst except for the fact that at this
;;; point the language is smaller and the existence of the first
;;; clause, which builds a let using poss-app.  The name of the
;;; procedure can not be the same as beta-subst, since its language is
;;; different (smaller) and since we are taking advantage of the fact
;;; that we know that the rands are all simple, otherwise it would be
;;; wrong to call poss-app.

(define beta-substf
  (lambda (e v-id exp)
    (match exp
      [(,rator ,rand* ...)
       (guard (eq? rator v-id))
       (poss-app `(,e ,@rand*))]
      [,constant
        (guard (or (number? constant) (boolean? constant)))
        constant]
      [,var (guard (symbol? var)) (if (eq? var v-id) e var)]
      [(APk ,cont ,rand)
       `(APk
          ,(beta-substf e v-id cont)
          ,(beta-substf e v-id rand))]
      [(CLAM (,id) ,body)
       `(CLAM (,id) ,(beta-substf e v-id body))]
      [(lambda (,id* ...) ,body)
       (guard (memq v-id id*))
       `(lambda (,id* ...) ,body)]
      
      [(lambda (,id* ...) ,body)
       (guard (disjoint? id* (free-vars e)))
       `(lambda (,id* ...) ,(beta-substf e v-id body))]
      
      [(lambda (,id* ...) ,body)
       (beta-substf
         (let ((x (car (intersection id* (free-vars e))))
               (g (fresh-var (fresh-var x))))
           `(lambda ,(subst g x id*)
              ,(beta-substf g x body))))]
      
      [(if ,test-exp ,true-exp ,false-exp)
       `(if ,(beta-substf e v-id test-exp)
            ,(beta-substf e v-id true-exp)
            ,(beta-substf e v-id false-exp))]
      [(,prim ,rand* ...)
       (guard (primitive? prim))
       `(,prim ,@(map (lambda (rand) (beta-substf e v-id rand)) rand*))]
      [(let ((,id* ,rand*) ...) ,body)
       (guard (memq v-id id*))
       `(let ,(map list id*
                   (map (lambda (rand)
                          (beta-substf e v-id rand))
                        rand*))
          ,body)]
      [(let ((,id* ,rand*) ...) ,body)
       (guard (disjoint? id* (free-vars e)))
       `(let ,(map list id*
                   (map (lambda (rand)
                          (beta-substf e v-id rand))
                        rand*))
          ,(beta-substf e v-id body))]
      [(let ((,id* ,rand*) ...) ,body)
       (beta-substf
         (let ((x (car (intersection id* (free-vars e)))))
           (let ((g (fresh-var (fresh-var x))))
             `(let ,(map list (subst g x id*)
                         (map (lambda (rand)
                                (beta-substf e v-id rand))
                              rand*))
                ,(beta-substf g x body)))))]
      [(letrec ((,name* (lambda (,ids* ...) ,body*)) ...)
         ,body)
       (guard (memq v-id name*))
       `(letrec ,(map list name*
                      (map (lambda (id* body)
                             `(lambda (,id* ...) ,body))
                           ids* body*))
          ,body)]
      [(letrec ((,name* (lambda (,ids* ...) ,body*)) ...)
         ,body)
       (guard (disjoint? name* (free-vars e)))
       (beta-substf e v-id
                    (let ((x (car (intersection name* (free-vars e)))))
                      (let ((g-id (fresh-var (fresh-var x))))
                        `(letrec (map list (subst g x name*)
                                      (map (lambda (ids body)
                                             (if (memq x ids)
                                                 `(lambda ,ids ,body)
                                                 `(lambda ,(subst g-id x ids)
                                                    ,(beta-substf g-id x body))))
                                           ids* body*))
                           ,(beta-substf g-id x body)))))]
      [(letrec ((,name* (lambda (,ids* ...) ,body*)) ...)
         ,body)
       `(letrec ,(map list name*
                      (map (lambda (ids body)
                             (beta-substf e v-id `(lambda (,ids ...) ,body)))
                           ids* body*))
          ,(beta-substf e v-id body))]
      [(,rator ,rand* ...)
       `(,(beta-substf e v-id rator)
          ,@(map (lambda (x) (beta-substf e v-id x)) rand*))]
      [,other (error 'beta-substf "Invalid expression ~s" other)])))

(load "cps-tester.ss")
(define header "******************************  F  *********************")
(newline)
(test-all header)

(define resultsF test-results)

;;; Some thoughts.  There may be a use for free-vars-list/operator-position and
;;; free-vars-list/operand-position.  Then, if a particular variable
;;; only appears once in function position, we can consider
;;; substituting for that one occurrence.  If the variable also
;;; appears no more than once in an operand position, then we can
;;; substitute for it as well.  If not, we must leave the let in place
;;; for the two or more operand position occurrences.  I have to think
;;; of test programs where this matters.  This would be a small change to
;;; this file only.