Running some ellipsis patterns in define-judgment-form causes syntax error.

[akuhlens]

There is a small issue with the parsing of ellipsis patterns in define-judgment-form. The following file gets the error in racket 6.2. There are some observations about the pattern in the use and test cases.

#lang racket

(require redex)

(define-language L
  (t ::= () (t ... -> t)))

(define-judgment-form L
  #:mode (≈ I I)
  #:contract (≈ t t)
  [-------------------- "≈Refl"
   (≈ () ())]
  [(≈ t_1 t_2)
   ;; I have the intuition that this should be the same as
   ;; (≈* (τ_1 ...) (γ_1 ...))
   (≈ t_n t_m) ... 
   ------------------------------------------ "≈->"
   (≈ (t_n ... -> t_1) (t_m ... -> t_2))
   ;; The following conclusion gets rid of this error.
   #;(≈ (t_n ..._n -> t_1) (t_m ..._n -> t_2))])

(define-judgment-form L
  #:mode (≈* I I)
  #:contract (≈* (t ...) (t ...))
  [--------- "≈*base"
   (≈* () ())]
  [(≈ t_1 t_2) (≈* (t_n ...) (t_m ...))
   ---------------------- "≈->"
   (≈* (t_1 t_n ...) (t_2 t_m ...))])

(module+ test
  (test-true  (judgment-holds (≈ () ())))
  (test-true  (judgment-holds (≈ (-> ()) (-> ()))))
  (test-true  (judgment-holds (≈ (() -> ()) (() -> ()))))
  (test-true  (judgment-holds (≈ (() () -> ()) (() () -> ()))))
  (test-false (judgment-holds (≈ () (-> ()))))
  ;; This test causes this pattern mentioned above to report
  ;; the following error.
  ;;syntax: incompatible ellipsis match counts for template in: ...
  (test-false (judgment-holds (≈ (-> ()) (() -> ()))))
  )

(module+ test (test-results))

;; Helpers to consider abstracting

(define-syntax-rule (test-true e)
  (test-equal e #t))

(define-syntax-rule (test-false e)
  (test-equal e #f))

[bfetscher]

Thanks for the report!

This is an issue with metafunctions and reduction relations as well, it turns out. After talking over a few approaches with @rfindler, we're thinking this should be a syntax error to the effect that appropriate length constraints should be added to the ellipses in the conclusion. (As opposed to automatically imposing the constraints on the match.)

Here's a minimized example:

(define-language L0)

(define-judgment-form L0
  #:mode (J I I)
  [(J number_1 number_2) ...
   ----------------------------------
   (J (number_1 ...) (number_2 ...))] 
  [----------------------
   (J number_1 number_2)])

(judgment-holds (J (1 2) (3)))

Implementation notes:

The error is coming from inside term, when it tries to assemble ellipses with different lengths. The relevant bindings are created with bind-pattern-names, using the names/ellipses results from rewrite-side-conditions/check-errs. It seems like the best way to cope with this is to check for ellipsis variables that are guaranteed to have the same length in rewrite-side-conditions, preserve that information, and pass it in as an extra argument to term-let/error-name, which can add some appropriate expansion-phase bindings. Term can then check that two variables under the same ellipsis have the appropriate constraints, and raise an error if they're not there.

[akuhlens]

That sounds like an excellent way of fixing this.