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
____________________ Racket Users list: http://lists.racket-lang.org/users
