A CPS interpreter for a CBV language written in syntax-rules

syntax-rules-eval.rkt

#lang racket

;; A CPS interpreter for a CBV language written in syntax-rules

;; e ::= 'd          literal
;;    |  x           variable
;;    |  (e e)       application
;;    |  (λ (x) e)   abstraction

;; (eval e) interprets e in an environment
;; that binds call/cc to its usual denotation.

(define-syntax eval
  (syntax-rules ()
    [(eval e)
     (letrec-syntax         
         ((apply
           (...
            (syntax-rules (λ)
              ((apply (λ (x ...) e1) e0 ...)
               (let-syntax ((kf (syntax-rules () ((_ x ...) e1))))
                 (kf e0 ...))))))
          (eval
           (...
            (syntax-rules (quote λ)
              ((eval ρ 'x k)
               (apply k x))
              ((eval ((x0 v0) ...) (λ (x) e0) k)
               (apply k
                      (λ (v k0) (eval ((x v) (x0 v0) ...) e0 k0))))                      
              ((eval ρ (e0 e1) k)
               (eval ρ e0
                     (λ (v0)
                       (eval ρ e1
                             (λ (v1)
                               (apply v0 v1 k))))))
              ((eval ((x0 v0) ...) x k)
               (letrec-syntax
                   ((lookup
                     (...
                      (syntax-rules (x)
                        ((lookup (x v) _ ...)
                         (apply k v))
                        ((lookup _ (y v) ...)
                         (lookup (y v) ...))))))
                 (lookup (x0 v0) ...)))))))
       
       (eval ((call/cc (λ (v0 k0)
                         (apply v0 (λ (x k1) (apply k0 x)) k0))))
             e
             (λ (v) 'v)))]))

;; This one's for Ron:
(eval (((call/cc (λ (c) c)) (λ (x) x)) 'HEY!))