Improve treatment of ellipsis in `define-judgment-form`

Original text by @rfindler.

In general, this aspect of the handling of ellipses is implemented by the racket/datum library (the same library that syntax-case uses). It can cope with writing things like this:

((a b) ...)

where a is bound in some pattern like this (a ...) but b is just b with no ellipsis around it. It handles this by duplicating b, once for each a. That's what we'd like to happen here too. But the ellipses that are "between" premises in a define-judgment-form are not handled by just giving them to the racket/datum library. Instead, Redex is doing some of its own work before it can hand them off. And that work is what is raising the syntax error in this case.

So: best case, we figure out a more relaxed well-formedness check to implement in define-judgment-form and this example just starts working. Worse case, we need to change how the "inter premise" ellipses handling is implemented. I'm not sure which case we are in.

Test case

#lang racket
(require redex/reduction-semantics)

(define-language L
  (τ ::= n b)
  (e ::= (amb τ e ...) natural #t #f))

(define-judgment-form L
  #:mode (type I O)
  [----------------
   (type natural n)]

  [-----------
   (type #t b)]

  [-----------
   (type #f b)]

  [(type e τ) ...
   ----------------------
   (type (amb τ e ...) τ)])

(test-judgment-holds (type (amb b #f #t) b))
(test-judgment-holds (type (amb n 0 1) n))
(test-equal (judgment-holds (type (amb n 0 #f) any)) #f)
(test-equal (judgment-holds (type (amb n #t #t 11 #f) any)) #f)

Error

unsaved editor:21:14: define-judgment-form: found the same binder, τ, at different depths, 1 and 0 at: τ

References

• Initial discussion.

Start by running the provided define-judgment-form test case and reading the inter-premise ellipsis handling in define-judgment-form, along with the referenced racket/datum behavior. The work is done when the example no longer raises the binder-depth syntax error, the judgment tests pass, and existing ellipsis cases remain correct.