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

Thanks Robby. This will be very handy.


On Sat, Feb 11, 2012 at 11:01 AM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:
>
> Thanks, this looks just like what we have needed for a while. -- Matthias
>
>
>
> On Feb 11, 2012, at 4:26 AM, Robby Findler wrote:
>
>> Hi Stephen: I've added define-union-language to Redex now. For the
>> example below, you'd write this:
>>
>>
>> #lang racket
>> (require redex)
>>
>> (define-language L1
>> (e 1))
>> (define-language L2
>> (f 2))
>> (define-union-language L L1 L2)
>> (define-metafunction L
>> L1->L2 : e -> f
>> [(L1->L2 1) 2])
>>
>> or you could also write this:
>>
>> #lang racket
>> (require redex)
>>
>> (define-language L1
>> (e 1))
>> (define-language L2
>> (f 2))
>> (define-union-language L (l1: L1) (l2: L2))
>> (define-metafunction L
>> L1->L2 : l1:e -> l2:f
>> [(L1->L2 1) 2])
>>
>> Hope that works for your use case.
>>
>> Robby
>>
>> On Sun, Feb 5, 2012 at 4:11 PM, Stephen Chang <stchang at ccs.neu.edu> 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])
>>> _________________________
>>>  Racket Developers list:
>>>  http://lists.racket-lang.org/dev
>>
>> _________________________
>>  Racket Developers list:
>>  http://lists.racket-lang.org/dev
>