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

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