Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
A CPS interpreter for a CBV language w/ some fancy features written in syntax-rules
#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))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment