I think in my case I actually do want the same nonterminal names. The
higher-order language has lambdas while the first-order language
doesn't. The first-order language has an outer `let' while the
higher-order language has no `let'. Every other kind of expression is
the same and has the same reduction rules in each language.
Neil ⊥
On 02/05/2012 03:58 PM, Robby Findler wrote:
Yes, you guys are right-- this is not supported. You'd have to put
everything into a single language to make it work.
I've shied away from this because it seems overly complicated, but
also because the language names ("L1" and "L2" in Stephen's example)
don't show up anywhere in the typeset version of the model. So in
order to really be clear, you want to have different non-terminals
anyway, and then it seems like putting things into the same language
is not problematic.
But if you have some more context in the example that suggests my
reasoning is flawed, I'd love to hear it.
Robby
On Sun, Feb 5, 2012 at 4:46 PM, Neil Toronto<neil.toro...@gmail.com> wrote:
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
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
