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 racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
