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
