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

How will you disambiguate them on the printed page for readers of your paper?

Robby

On Sun, Feb 5, 2012 at 9:36 PM, Neil Toronto <neil.toronto at gmail.com> wrote:
> 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
>
>