On 10/24/12 2:28 PM, Prabhakar Ragde wrote:
David Van Horn wrote:
Then I thought, PCF's binding structure is a lot like Racket's: wouldn't
it be nice to get syntax coloring, syntax arrows, renaming, etc. That
was about another 30 lines of code.
Can you say a few words about how you achieved this? Thanks to Matthew's
article and RacketCon tutorial, I now know how creating languages works,
but he didn't cover this last bit. I could start poring over the code,
but I suspect a minute or two of your time will save me a lot more.
Thanks. --PR
Sure! First, write a redex model.
If you want to create a language, you need a reader. Since I'm using an
S-Expression based syntax, this is trivial; here is my reader:
#lang s-exp syntax/module-reader
pcf/langs/pcf
The pcf/langs/pcf.rkt module provide the #%top-interaction and
#%module-begin forms that implement the language.
The module-begin form is basically the following rewrite:
(_ e ...)
#'(#%module-begin
(apply values (append (apply-reduction-relation* R (term e)) ...)))
So the program is expanded into a call to apply-reduction-relation* that
reduces each term using the reduction relation R. That gets you a
redex-based #lang language.
Now, if you want to enforce a static discipline, you just make a call to
your type judgment *at expansion time*:
(_ e ...)
(for-each (λ (e)
(unless (typable? (syntax->datum e))
(raise-syntax-error 'type-error "ill-typed" e)))
(syntax->list #'(e ...)))
#'(#%module-begin
(apply values (append (apply-reduction-relation* R (term e)) ...)))
Here I'm using the typable? function from my redex model, which is just
defined as
(define (typable? M)
(cons? (judgment-holds (typeof () ,M T) T)))
where `typeof' is just the run of the mill typing relation for this
language.
The top-interaction is similar:
(_ . e)
(unless (typable? (syntax->datum #'e))
(raise-syntax-error 'type-error "ill-typed" #'e))
#`(apply values (apply-reduction-relation* #,R (term e))
What's left is getting the syntax coloring, renaming, etc. The key here
is turn your S-Expression into some piece of Racket code that has the
same binding structure as the program at hand. You won't actually *do*
anything with this Racket expression; it's just there to tell DrRacket
about the binding structure. So you do the following:
(_ e ...)
(for-each (λ (e)
(unless (typable? (syntax->datum e))
(raise-syntax-error 'type-error "ill-typed" e)))
(syntax->list #'(e ...)))
#'(#%module-begin
(lexical e) ... ;; <<== expand into Racket with lexical structure
(apply values (append (apply-reduction-relation* R (term e)) ...)))
Where lexical is something like this (it varies based on the particulars
of the language you're implementing):
(define-syntax (lexical stx)
(syntax-case stx ()
;; throw away the result w/o evaluating
[(_ e) #'(void (λ () (lx e)))]))
(define-syntax (lx stx)
(syntax-case stx (λ • : err ⚖)
[(_ (λ ([x : _] ...) e))
#'(λ (x ...) (lx e))]
[(_ (if0 e0 e1 e2))
#'(if (lx e0)
(lx e1)
(lx e2))]
[(_ (err _ string)) #'string]
[(_ (• t)) #''(• t)]
[(_ (c ⚖ e)) #'(begin (lc c) (lx e))]
[(_ (e ...))
#'((lx e) ...)]
[(_ e) #'e]))
(define-syntax (lc stx)
(syntax-case stx (->)
[(_ (c0 ... -> c1))
#'(begin (lc c0) ... (lc c1))]
[(_ e) #'(lx e)]))
There's one last trick to get arrows from the language to the special
forms. That involves syntax-local-introduce, which I think puts that
feature beyond what should be in such a cute little demo.
But that's the basic idea.
David
____________________
Racket Users list:
http://lists.racket-lang.org/users
