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

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