Side conditions have inconsistent ellipses depth expectations

[MichaelBurge]

The following program intends to match a list of expressions which individually have a purple? derivation.

#lang racket

(require redex/reduction-semantics)

(define-language L
  [ x ::= variable-not-otherwise-mentioned ]
  )

(define-judgment-form L
  #:mode (purple? I)
  #:contract (purple? x)
  [(purple? purple)]
  )

(define find-purples
  (term-match L [((side-condition x (judgment-holds (purple? x))) ...)
                 'HIT]))

(find-purples (term (purple purple purple)))
(find-purples (term (purple red purple)))

; Error
; a.rkt:17:61: datum: missing ellipsis with pattern variable in template
;   at: x
;   in: (datum (x))

Since x is eventually bound to a list, its use within (purple? x) must use ellipses. It would make more sense for x to be locally-scoped to a lesser ellipses depth.

The first example shows that redex expects x to have an ellipses(i.e. that it is a list). This next example shows that x is bound to a single term purple during evaluation, which conflicts with the expectation that it is a list of terms.

(define find-purples
  (term-match L [((side-condition x (andmap (λ (t) (judgment-holds (purple? ,t)))
                                            (term (x ...)))) ...)
                 'HIT]))

; ERROR: term-let: term purple does not match pattern (x ...)

A workaround is to apply the side-condition to the matched list rather than each element:

(define find-purples
  (term-match L [(side-condition (x ...) (andmap (λ (t) (judgment-holds (purple? ,t)))
                                                 (term (x ...))))
                 'HIT]))

However, this workaround should be less efficient: A side-condition applied to individual elements should cause pattern-matching to abort as soon as it finds a failing element, but a side condition applied to a list pattern first generates all possible list matches.

I haven't yet tested to confirm that this workaround is less efficient on any specific example.

[MichaelBurge]

My "ideal" syntax for this would be:

(define find-purples (term-match L [((purple? x) ...) 'HIT]))

But converting I-mode judgments into patterns - similarly to how they're already terms - would require a pattern-let analogue to term-let. I'm not sure how difficult that is - I suspect the pattern language is restricted to enable efficient search algorithms.

[rfindler]

I think a better approach would be to just stick with Redex has to offer already, without trying to write so much Racket code. In other words, here's what I write if I wanted a function that filtered lists for purpleness.

#lang racket
(require redex)

(define-language L
  [ x ::= variable-not-otherwise-mentioned ]
  )

(define-judgment-form L
  #:mode (purple? I)
  #:contract (purple? x)
  [(purple? purple)]
  )

(define-metafunction L
  find-purples : any ... -> (any ...)
  [(find-purples any_1 any_2 ...)
   (any_1 any_3 ...)
   (judgment-holds (purple? any_1))
   (where (any_3 ...) (find-purples any_2 ...))]
  [(find-purples any_1 any_2 ...) (find-purples any_2 ...)]
  [(find-purples) ()])

(test-equal (term (find-purples purple purple purple))
            (term (purple purple purple)))

(test-equal (term (find-purples purple red purple))
            (term (purple purple)))

[rfindler]

(my previous comment was meant to apply only to the later notes on this issue, not the main complaint, which I agree is a bug)

[rfindler]

This got fixed, probably here.