[racket-dev] redex metafunction contract for two separate languages?

I think in my case I actually do want the same nonterminal names. The 
higher-order language has lambdas while the first-order language 
doesn't. The first-order language has an outer `let' while the 
higher-order language has no `let'. Every other kind of expression is 
the same and has the same reduction rules in each language.

Neil ⊥

On 02/05/2012 03:58 PM, Robby Findler wrote:
> Yes, you guys are right-- this is not supported. You'd have to put
> everything into a single language to make it work.
>
> I've shied away from this because it seems overly complicated, but
> also because the language names ("L1" and "L2" in Stephen's example)
> don't show up anywhere in the typeset version of the model. So in
> order to really be clear, you want to have different non-terminals
> anyway, and then it seems like putting things into the same language
> is not problematic.
>
> But if you have some more context in the example that suggests my
> reasoning is flawed, I'd love to hear it.
>
> Robby
>
> On Sun, Feb 5, 2012 at 4:46 PM, Neil Toronto<neil.toronto at gmail.com>  wrote:
>> On 02/05/2012 03:11 PM, Stephen Chang wrote:
>>>
>>> I want to write a redex metafunction contract that goes between two
>>> languages. Is there currently a way to do this?
>>>
>>> For example,
>>>
>>> #lang racket
>>> (require redex)
>>>
>>> (define-language L1
>>>    (e 1))
>>> (define-language L2
>>>    (f 2))
>>> (define-metafunction L1
>>>    L1->L2 : e ->    f
>>>    [(L1->L2 1) 2])
>>>
>>>> (term (L1->L2 1))
>>>
>>> . . ..\..\plt\collects\redex\private\error.rkt:3:0: L1->L2: codomain
>>> test failed for 2, call was (L1->L2 1)
>>>
>>> Switching the metafunction language to L2 similarly produces an error
>>> about the domain. Currently it seems like I can't use a contract with
>>> these kinds of metafunctions. How difficult would it be to support
>>> this functionality? It seems like this use case should be pretty
>>> common.
>>>
>>> I'm imagining something like:
>>>
>>> (define-metafunction
>>>    L1->L2 : L1:e ->    L2:f
>>>    [(L1->L2 1) 2])
>>
>>
>> I'd like to know this myself. I'll be transforming terms from a higher-order
>> language to a first-order one via closure conversion. Neither language is an
>> extension of the other, so I can't use `defined-extended-language'. The only
>> way I've thought of so far is to make a third language that is a superset of
>> both.
>>
>> Neil ⊥
>>
>> _________________________
>>   Racket Developers list:
>>   http://lists.racket-lang.org/dev