[racket-dev] redex metafunction contract for two separate languages?

You're raising an issue that already exists, right? 

Say we have only this: 

>  (define-language L1
>    (a ... somestuff ...))
> 
>  (define-metafunction L1
>     f : a -> a
>     [(f a) ...somestuff...])
> 
>  (define-language L2
>    (a ... somedifferentstuff ...))
> 
>  (define-metafunction L2
>     g : a -> a
>     [(g a) ...somedifferentstuff...])


What do we do when we type-set f and g currently? We don't bother 
with any distinctions. When you run 

 (render-metafunction f)

you don't get to see that it maps a to a or that the function is 
defined in context L1. 

Perhaps we need to introduce optional arguments that make render 
show (1) the contract for f if it exists and (2) superscript the 
metavariables from their language. So rendering f may look like this: 

 f : a -> a 
 f[a^L1] = 1


On Feb 6, 2012, at 9:18 PM, Robby Findler wrote:

>  (define-union-language L ((L1 l1) (L2 l2))) ;; l1 & l2 are prefixes
> 
>  (define-metafunction L
>    h : l1.a -> l2.a
>    [(h l1.a) ...])
> 
> Also, how can we typeset L? Should it look like some combination of
> the typesetting of L1 and L2? (This part actually doable, altho not
> trivial.)

Yes, this is the only thing I can think of. The author of the model
and therefore the author of the paper intend to express 'combination' 
here. So 

 L:
   a^L = a^L1 | aa^L2 
   ...

might me most appropriate. 


> But if the union language actually extends some of the
> non-terminals (using the part I added that you didn't request), then
> the typesetting won't work out well, for the same reason that when
> using the four-period ellipsis in a define-extended-language you still
> see that ellipsis in the typeset version. So at a minimum, I would
> like to kill that extension.

I agree. 

But Redexers can express this idea already with 

(define-extended-language L3 L ...)

Is it clear how to typeset this language? If so, I think we're in the clear. 

Does this answer the question? -- Matthias