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 _________________________ Racket Developers list: http://lists.racket-lang.org/dev
