[racket] Redex question: parameterizing a language definition

From: Robby Findler (robby at eecs.northwestern.edu)
Date: Mon Jun 3 23:29:14 EDT 2013

I've written three little examples, extracted from the macro you pointed us
to. The first just reproduces the problem you're seeing, I expect. Note
that if you reverse the "a ..." and the "x" line, you don't get an error
anymore, but you do get strange output. This is because of the interaction
between Redex's typesetting and macro transformations. Macros preserve the
source locations of the input so, by the time Redex gets ahold of the
program, the "a ..." part is gone and in its place is the "+ - *" but with
the original source locations. That's why things seem to go "backwards"
from Redex's perspective in the example you got and in the example as
written below: it happens when it sees the "x" production and gets confused
about why the "+ - *" seems to actually be later in the source file.

Okay, onto the second example below: here I just punt entirely. If you put
the "+ - *" into its own non-terminal and then don't render that one, then
you can use some other technique to render these (like in the running text
or language extension or something). This idea doesn't generalize well, but
if you can get by with it, then it is easiest.

The third definition below shows how you can munge the source locations at
compile time so as to achieve something with sane looking source locations
by the time Redex gets it. Here it adjusts the "+ - *"'s source locations
so they all appear on one line (important because "HERE" takes only one
line but you can leave a blank line there if you plan to insert code that
takes two lines, etc) and they have reasonable looking space between them.

Hope this helps.


#lang racket
(require redex/reduction-semantics
  (mk-L L a ...)
  (define-language L
    (e (λ (x) e)
       (e e)
       a ...
    (x variable-not-otherwise-mentioned)))

(mk-L L + - *)
(with-handlers ((exn:fail? exn-message))
  (render-language L))

  (mk-L2 L a ...)
  (define-language L
    (e (λ (x) e)
       (e e)
    (prims a ...)
    (x variable-not-otherwise-mentioned)))

(mk-L2 L2 + - *)
(render-language L2 #:nts '(e x))

(define-syntax (mk-L3 stx)
  (syntax-case stx ()
    [(_ L a ...)
     (let ()
       (define template
         #'(define-language L
             (e (λ (x) e)
                (e e)
             (x variable-not-otherwise-mentioned)))
        (let loop ([stx template])
          (syntax-case stx (HERE)
             (let loop ([as (syntax->list #'(a ...))]
                        [pos (syntax-position stx)]
                        [col (syntax-column stx)])
                 [(null? as) '()]
                  (define a (car as))
                  (define span (string-length (symbol->string (syntax-e
                   (datum->syntax a
                                  (syntax-e a)
                                  (vector (syntax-source stx)
                                          (syntax-line stx)
                   (loop (cdr as)
                         (+ pos span 1)
                         (+ col span 1)))]))]
            [(a ...)
               (apply append (map loop (syntax->list #'(a ...))))
             (list stx)]))))]))

(mk-L3 L3 + - *)
(render-language L3)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20130603/b9da0845/attachment.html>

Posted on the users mailing list.