[racket-dev] redex metafunction contract for two separate languages?
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])