[racket] Redex question: parameterizing a language definition

Robby wrote:

> Yes, David's right. The (a bit more long-term than I hoped) plan is to
> essentially improve and automate parts of what you call the rabbit hole in
> your stackoverflow question (as also discussed in the link David posted).

I ran into this problem in a much simpler context while teaching a grad 
course using the Redex textbook last fall. What I wanted to do was to 
use define-extended-language to add an "ifzero" construct to the basic 
ISWIM language. But then I needed to define a new substitution 
metafunction, with a new name, because I couldn't extend or override the 
old one. And then, because the substitution metafunction is used in the 
beta_v reduction relation, I had to create a new version of that as 
well, rather defeating the point of extension. Robby's answer to my 
email question was much the same, namely that some sort of module system 
for Redex would help. The solution that the book uses is to write a very 
general substitution function right from the start, but this is a bit of 
a kludge. My conclusion was that define-extended-language is a feature 
in progress. But Redex has already moved on from what the textbook 
describes (with define-judgment), and I'm guessing that the next time I 
use this material in lecture, this issue will have been addressed. --PR