search

racket / redex

Other
93 stars 36 forks source link

Feature request: Reinterpret metafunctions in new language when using `extend-reduction-relation` #221

Closed jsjolen closed 4 years ago

jsjolen commented 4 years ago

[...] In addition to adding the rules specified to the existing relation, this form also reinterprets the rules in the original reduction, using the new language.

This is great, but since reduction rules typically use metafunctions defined in the base language the new extended reduction relation isn't very useful.

If metafunctions' contracts were reinterpreted using the new language's grammar then the issue would be resolved.

This issue is already mentioned in David Van Horns' tutorial, the relevant section being:

https://dvanhorn.github.io/redex-aam-tutorial/#%28part._.A_brief_aside_on_the_caveats_of_language_extensions%29

camoy commented 4 years ago

I have a hacky redex-parameter package that you can use to get this behavior. But, I'd be very happy to see that package be deprecated in favor of a real implementation.

rfindler commented 4 years ago

This is kind of complex with the current design. I have long had in my mind a kind of redex module system where one would extend groups of metafunctions, judgment forms, reduction relations, etc simultaneously and then things would be behave exactly as you are asking for. Until then, I think we have to make do with hacks. (Of course, if someone sees how to adjust things to make this one work, I'm all ears!)

jsjolen commented 4 years ago

@rfindler That'd be amazing (and like a lot of hard work :)). I'm closing the issue since it won't be resolved for the time being.

Thank you @camoy! I ended up doing a copy/paste in the end.