Thanks Robby. This will be very handy.
On Sat, Feb 11, 2012 at 11:01 AM, Matthias Felleisen <matth...@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 <stch...@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 > _________________________ Racket Developers list: http://lists.racket-lang.org/dev
