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

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