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
