Binding forms parsing error

[dfeltey]

This language definition:

(define-language lc
    (e ::= (list e ...) x)
    (x ::= variable-not-otherwise-mentioned)
    #:binding-forms
    (list (list x ...) ...) #:exports nothing)

Produces the error: redex/redex-lib/redex/private/binding-forms-compiler.rkt:36:39: define-language: Same name used at two different ... depths: list (depth 1) vs. list (depth 0) in: (list (list p ...) ...)

[paulstansifer]

Hm, this one might be a little tricky. Should (e (e x ...) ...) also be accepted because it is transcribeable by duplicating the interior e for each x? I suppose so, and the case with a literal list is sort of the trivial case of that (just to check my understanding, you're looking for terms like (list (list a b c) (list x y z), right?). Maybe the solution is to only check names that get imported (eventually, this should be relaxed to allow (m1 x (e #:refers-to x) ...), once the system can handle that).

I'm worried that this error message is covering an implementation gap: the binding forms runtime has its own implementation of ...s, and it might be unable to deal with the case where a ...ed name "bottoms out" and needs to be duplicated. If that's so, it'll take a bit of work, but it shouldn't need a major overhaul.

[rfindler]

I'm not sure of that case, but certainly the current error message is incorrect because list is not a name. So for fixing this issue, maybe just taking the literals in the grammar into account?

[paulstansifer]

I think it might not be too much harder to be more generous (and might be easier, since it might require less plumbing). I think that (assuming the runtime handles ... correctly, which is reasonably likely), the rule can be: if x appears in a beta, it must be under exactly n ...s (it doesn't matter whether the ...s are part of the beta or not), where n is the smallest number of ...s that x appears under as a "normal" pattern part (because that's the "native" transcription depth).

[rfindler]

That rule is, I think, slightly more generous than the rule that term uses (term's implementation is inherited from syntax (which has been refactored into the datum library))