[racket] [redex] Structured Semantics

How should I use Redex to encode a structured semantics... For example,

Suppose I have the L_thread language and the ->_thread reduction
relation with contract

(store_global store_local term) ->_thread (store_global store_local term)

and I want to have another language L_system with an ->_system rr with contract

(store_global (store_local term) ...) ->_system (store_global
(store_local term) ...)

where (among other rules) I have the rule:

(store_global store_local term) ->_thread (store_global' store_local' term')
---------------------
(store_global (store_local term) any_others ...) ->_system
(store_global' (store_local' term') any_others ...)

I could easily use reduction-relation for ->_thread and most of
->_system, but for this particular rule, it doesn't seem possible to
express in Redex. If the reduction-relation? structure were exposed
(or perhaps had a struct property associated with it), then I could
code this one rule in Racket and dispatch to the two other rrs when
necessary, but that seems wrong.

Another way I could do it is combine the two languages and rules into
one with a "mode" switching...

L_synthetic = (THREAD L_thread L_system/thread-hole) + (SYSTEM L_system)

->_synthetic =

(THREAD thread sys) -> (THREAD thread' sys)

...

(SYSTEM (in-hole sys thread)) -> (THREAD thread sys)

But that seems like the wrong thing too.

Any other ideas or examples?

Jay

-- 
Jay McCarthy <jay at cs.byu.edu>
Assistant Professor / Brigham Young University
http://teammccarthy.org/jay

"The glory of God is Intelligence" - D&C 93