A use case I'm running up against a lot in Redex is when I have some
pattern that's matching some number (let's say n) of elements, and I want
to replace all of them with n of the same element.
Take the following language:
(define-language L
(e number
(e ...)))
Suppose we now want to write a metafunction that replaces all lists with
lists of the same length, but where every element is 0.
The intuitive way to do this is
(define-metafunction L
replace-with-0 : e -> e
[(replace-with-0 (e ..._1)) (0 ..._1)])
This crashes and burns statically, however, because the ..._1 notation
isn't valid for a term - Redex wants to be able to figure out how long the
list should be from the term that's being repeated, not the user's
annotation.
There is a workaround. Instead of using a nice pretty pattern, we can
instead escape to Racket, which would give us
(define-metafunction L
replace-with-0 : e -> e
[(replace-with-0 (e ..._1)) ,(make-list (length (term (e ...))) 0)])
This accomplishes the same goal, but is not particularly pretty. It would
be very nice if Redex could be extended to allow the length of a
term-sequence to be determined by a named ... pattern.
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
For more options, visit https://groups.google.com/d/optout.
