On 02/05/2012 03:11 PM, Stephen Chang 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])
I'd like to know this myself. I'll be transforming terms from a
higher-order language to a first-order one via closure conversion.
Neither language is an extension of the other, so I can't use
`defined-extended-language'. The only way I've thought of so far is to
make a third language that is a superset of both.
Neil ⊥
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
