judgment-holds output positions with metafunction calls

[nicholasdiggi]

In the code block below, the first two calls to judgment-holds fail, but the third one succeeds. They should probably all succeed.

[define-language LC]

[define-judgment-form LC
  #:mode [J1 I O]
  [----
   [J1 any_1 any_1]]]

[define-metafunction LC
  M : any -> any
  [[M any] any]]

[define-judgment-form LC
  #:mode [J2 I]
  [[J1 any_1 [M any_1]]
   ----
   [J2 any_1]]]

[define-judgment-form LC
  #:mode [J3 I I]
  [[J1 any_1 any_2]
   ----
   [J3 any_1 any_2]]]

[judgment-holds [J1 1 [M 1]]]
[judgment-holds [J2 1]]
[judgment-holds [J3 1 [M 1]]]

[rfindler]

I think the issue here is that the metafunction calls are being used in pattern positions and redex is currently ignoring the fact that some identifiers are bound to metafunctions when compiling the pattern position into code that does matching.

This means that bizarro programs like this one "work":

#lang racket
(require redex/reduction-semantics)

(module m racket
  (require redex/reduction-semantics)
  (provide L J)

  (define-language L)

  (define-metafunction L
    identity : any -> any
    [(identity any) any])

  (define-judgment-form L
    #:mode (J I O)

    [--------------------------
     (J (identity any_1) any_1)]))

(require (submod "." m))
(judgment-holds (J (identity 1) any) any)

In this program, the judgment form J defines a private helper metafunction but also just happens to use its name in a pattern. Redex, in its current form, treats that like it is matching the literal identity in the pattern in the definition of J, meaning that the result of the judgment-holds at the bottom of the example returns '(1).

I also added some code on this branch to detect when there is a metafunction used in a pattern and it looks like this phenomenon is at least somewhat common so, probably we cannot change anything about this without breaking existing models. Alas.