Binding forms parsing error about redex HOT 4 OPEN

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.

from redex.

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?

from redex.

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).

from redex.

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))

from redex.