A CPS interpreter for a CBV language w/ some fancy features 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
;;    |  (let ((x e) ...) e) let
;;    |  (if e e e)          conditional
;;    |  (cond [e e] ...)    cond
;;    |  (or e ...)          disjunction

;; All literals must be quoted.

;; Literal data only includes what is distinguishable by syntax-rules, so
;; d ::= ()
;;    |  (d . d)
;;    |  #t
;;    |  #f
;;    |  identifier

;; (You can get away with using strings and numbers, so long as you don't
;; use eq? on them.)

;; (eval e) interprets e in an environment
;; that contains: call/cc, car, cdr, cons, null?, pair?, procedure?, 
;; gensym, and eq?.

;; See test suite at bottom.

(define-syntax eval
  (syntax-rules ()
    [(eval e)
     ;; value tags, binding ensures they are unforgeable in syntax
     (let ((λ′ 'fresh)
           (cons′ 'fresh))
           
       (letrec-syntax         
           ((apply
             (...
              (syntax-rules (λ′)
                ((apply (λ′ (x ...) _ e1) e0 ...)
                 (let-syntax ((kf (syntax-rules () ((_ x ...) e1))))
                   (kf e0 ...))))))                                  
            (eval
             (...
              (syntax-rules (quote λ let if cond else or)
                ((eval ρ 'x k)
                 (letrec-syntax
                     ((quotation
                       (syntax-rules ()
                         ((_ (a . b) k0)
                          (quotation a
                                     (λ′ (qa) _
                                       (quotation b
                                                  (λ′ (qb) _
                                                    (let ((m 'alloc))                          
                                                      (apply k0 (cons′ m (qa . qb)))))))))
                         ((_ x0 k0) (apply k0 x0)))))
                   (quotation x k)))
                
                ((eval ρ (λ (x ...) e0) k)                 
                 (letrec-syntax
                     ((fresh
                       (...
                        (syntax-rules ()                            
                          ((fresh (x0 ... xn) r)
                           (fresh (x0 ...) ((xn yn) . r)))
                          ((fresh () ((x1 y1) ...))
                           (let ((m 'alloc))
                             (apply k
                                    (λ′ (y1 ... k0) m
                                      (eval ((x1 y1) ... . ρ) e0 k0)))))))))
                   (fresh (x ...) ())))
                
                ((eval ρ (if e0 e1 e2) k)
                 (let ((m 'alloc))
                   (eval ρ e0
                         (λ′ (v0) m
                           (let-syntax
                               ((case (syntax-rules ()
                                        ((_ #f) (eval ρ e2 k))
                                        ((_ _)  (eval ρ e1 k)))))
                             (case v0))))))
              
                ;; Derived forms
                ((eval ρ (let ((x1 e1) ...) e0) k)
                 (eval ρ ((λ (x1 ...) e0) e1 ...) k))              
                ((eval ρ (cond (else e0)) k)
                 (eval ρ e0 k))
                ((eval ρ (cond (e1 e2) c ...) k)
                 (eval ρ (if e1 e2 (cond c ...)) k))
                ((eval ρ (cond) k) ; not exactly faithful
                 (apply k #f))
                ((eval ρ (or) k)    (apply k #f))
                ((eval ρ (or e0) k) (eval ρ e0 k))
                ((eval ρ (or e0 e1 ...) k)            
                 ;; so fresh and so clean!
                 (let ((a 'fresh))
                   (eval ρ (let ((a e0))
                             (if a a (or e1 ...)))
                         k)))
              
                ;; Application (has to be next to last)
                ((eval ρ (e0 . es) k)
                 (letrec-syntax
                     ((eval-app
                       (...
                        (syntax-rules ()
                          ((eval-app v0 (v1 ...) ())
                           (apply v0 v1 ... k))
                          ((eval-app v0 (v1 ...) (ei . es*))
                           (let ((m 'alloc))
                             (eval ρ ei
                                   (λ′ (vi) m
                                     (eval-app v0 (v1 ... vi) es*)))))))))
                   (let ((m 'alloc))                   
                     (eval ρ e0
                           (λ′ (v0) m
                             (eval-app v0 () es))))))
              
                ;; Variables (has to be last)
                ((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) call/cc
                           (let ((m 'alloc))
                             (apply v0 (λ′ (x k1) m (apply k0 x)) k0))))
                (car (λ′ (v0 k0) car
                       (let-syntax ((car
                                     (syntax-rules ()
                                       [(car (cons′ m (a . b))) (apply k0 a)])))
                         (car v0))))
                (cdr (λ′ (v0 k0) cdr
                       (let-syntax ((cdr
                                     (syntax-rules ()
                                       [(cdr (cons′ m (a . b))) (apply k0 b)])))
                         (cdr v0))))
                (cons (λ′ (v0 v1 k0) cons
                        (let ((m 'alloc))
                          (apply k0 (cons′ m (v0 . v1))))))
                (null? (λ′ (v0 k0) null?
                         (let-syntax ((null?
                                       (syntax-rules ()
                                         [(null? ()) (apply k0 #t)]
                                         [(null? _)  (apply k0 #f)])))
                           (null? v0))))
                (pair? (λ′ (v0 k0) pair?
                         (let-syntax
                             ((pair?
                               (syntax-rules ()
                                 [(pair? (cons′ m (a . b))) (apply k0 #t)]
                                 [(pair? _)                 (apply k0 #f)])))
                           (pair? v0))))

                (procedure? (λ′ (v0 k0) procedure?
                                (let-syntax
                                    ((procedure?
                                      (syntax-rules (λ′)
                                        [(procedure? (λ′ . _)) (apply k0 #t)]
                                        [(procedure? _)        (apply k0 #f)])))
                                  (procedure? v0))))
                (gensym (λ′ (k0) gensym
                          (let ((x 'gen))
                            (apply k0 x))))
                (eq? (λ′ (v0 v1 k0) eq?
                       (let-syntax
                           ((same?
                             (syntax-rules ()
                               ((same? m1 m2)
                                (let-syntax
                                    ((same-m1?
                                      (syntax-rules (m1)
                                        ((same-m1? m1) (apply k0 #t))
                                        ((same-m1? _)  (apply k0 #f)))))
                                  (same-m1? m2))))))
                         (let-syntax
                             ((eq?
                               (syntax-rules (cons′ λ′)
                                 [(eq? () ()) (apply k0 #t)]
                                 [(eq? #t #t) (apply k0 #t)]
                                 [(eq? #f #f) (apply k0 #t)]
                                 [(eq? (cons′ m1 (a . b))
                                       (cons′ m2 (c . d)))
                                  (same? m1 m2)]
                                 [(eq? (λ′ _ m1 _)
                                       (λ′ _ m2 _))                                  
                                  (same? m1 m2)]
                                 [(eq? () _) (apply k0 #f)]
                                 [(eq? #t _) (apply k0 #f)]
                                 [(eq? #f _) (apply k0 #f)]
                                 [(eq? (cons′ . _) _) (apply k0 #f)]
                                 [(eq? (λ′ . _) _) (apply k0 #f)]
                                 [(eq? _ ()) (apply k0 #f)]
                                 [(eq? _ #t) (apply k0 #f)]
                                 [(eq? _ #f) (apply k0 #f)]
                                 [(eq? _ (cons′ . _) _) (apply k0 #f)]
                                 [(eq? _ (λ′ . _)) (apply k0 #f)]
                                 [(eq? x1 x2) (same? x1 x2)])))
                           (eq? v0 v1))))))
               e
               (λ′ (v) _ 'v))))]))

;; Check for consistency with interpretation in meta-language
(define-syntax-rule (check e0)
  (let ((v0 (eval e0))
        (v1 e0))
    (unless (equal? v0 v1)
      (eprintf "failed test: ~a; actual ~a, expected ~a" 'e0 v0 v1))))

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

;; recursively compute whether something is a proper list
(check (((λ (f) ;; Y        
           ((λ (x) (f (λ (v) ((x x) v))))
            (λ (x) (f (λ (v) ((x x) v))))))        
         (λ (list?)
           (λ (x)
             (if (null? x)
                 '#t
                 (if (pair? x)
                     (list? (cdr x))
                     '#f)))))
        '(x y . z)))

;; hygenic or produces #t
(check (let ((a '#t))
         (or '#f a)))

(check (pair? (λ (x) x)))
(check (eq? eq? eq?))

(check (let ((x (call/cc (λ (k) (if (k k) '1 '2)))))
         (eq? x (call/cc (λ (k) (if (k k) '1 '2))))))

(check (eq? '() '()))
(check (eq? 'x '()))
(check (eq? 'x 'x))
(check (eq? (gensym) (gensym)))
(check (eq? 'x (gensym)))
(check (let ((x (gensym)))
         (eq? x x)))
(check (let ((x (λ (y) y)))
         (eq? x x)))
(check (let ((x (λ (y) y)))
         (eq? x (λ (y) y))))
(check (null? '()))
(check (null? '#f))
(check (null? 'x))
(check (procedure? (λ (x) x)))
(check (procedure? '(λ (x) x)))
(check (procedure? '(λ′ (x) f x)))
(check (call/cc (λ (k) ('x (k 'y)))))
(check (procedure? procedure?))
(check (procedure? (call/cc (λ (k) k))))
(check (call/cc (λ (k) (eq? k k))))