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 k e0 ...)
               (let-syntax ((kf k))
                 (kf e0 ...))))))
          (eval
           (...
            (syntax-rules (quote λ)
              ((eval ρ 'x k)
               (apply k x))
              ((eval ((x0 v0) ...) (λ (x) e0) k)
               (apply k
                      (syntax-rules ()
                        ((_ v k0)
                         (eval ((x v) (x0 v0) ...) e0 k0)))))              
              ((eval ρ (e0 e1) k)
               (eval ρ e0
                     (syntax-rules ()
                       [(_ v0)
                        (eval ρ e1
                              (syntax-rules ()
                                [(_ 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 (syntax-rules ()
                         [(_ v0 k0)
                          (apply v0 (syntax-rules ()
                                      [(_ x k1) (apply k0 x)])
                                 k0)])))
             e
             (syntax-rules () ((_ v) 'v))))]))

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