Internal contract violation when using `generate-term` that should satisfy a target judgement

[ahmadsalim]

I am currently trying to implement Featerweight Java in PLT Redex, and I am getting the following error:

[...]/generate-term.rkt:825:9: error: contract violation
  expected: (or/c string? symbol?)
  given: #<procedure:resolve-no-nts/pat>
  argument position: 1st
  other arguments...:

when calling

(generate-term FJ #:satisfying
                    (well-formed () (L P))
                    10)

It seems to work well when using just

(generate-term FJ (L P) 10)

so I would guess the issue is intrinsic to the #:satisfying form.

The complete code is available here in this Gist: https://gist.github.com/ahmadsalim/e3b0359e8a81e89aa7089b9e82a52f09 .

Any idea on why this error occurs, and whether it is possible to fix it?

Thanks!

[rfindler]

I haven't fully grokked this error yet, but I believe you're running into a limitation of the #:satisfying generator. (I've pushed a fix so the error message is the intended one but it probably won't help you directly.)

[rfindler]

Here's a slightly simpler program that also illustrates the issue:

#lang racket/base
(require redex/reduction-semantics)

(define-language FJ
  (P ::= (L P) ())
  (L ::= (class C extends D K))
  (L? ::= L ⊤)
  (K ::= (C))
  (C D ::= variable-not-otherwise-mentioned Object))

(define-judgment-form FJ
  #:mode (well-formed I I)
  [--------------------
   (well-formed P ())]

  [(where #f (definition-of P_0 C))
   (well-formed ((class C extends D K) P_0) P_1)
   ----------------------------------------------
   (well-formed P_0 ((class C extends D K) P_1))])

(define-metafunction FJ
  definition-of : P D -> L? or #f
  [(definition-of ((class C extends D K) P) C)
   (class C extends D K)]
  [(definition-of P Object) ⊤]
  [(definition-of any_1 any_2) #f])

(generate-term FJ #:satisfying
               (well-formed () (L P))
               10)

[ahmadsalim]

@rfindler Thank you for the quick response.

Would you kindly explain me what the error is/limitation means when you have time? I am not sure I understand what a non-groundable pattern is.

[rfindler]

If I understand it correctly, it is a technical limitation in the solver that isn't easily explained in terms of the source programs. It may be that this amounts to an internal error in redex and we can fix it (at least for this model) but it may be a while before we can sort that out. In the meantime, I suggest you avoid #:satsifying for this model.

Sorry.

[ahmadsalim]

OK, thanks for the explanation, nonetheless!

[rfindler]

Rereading my comments, I think that I wasn't clear enough. I think that this is a legtimate bug in redex. I'm just not sure if the fix is to produce a better error message or if the fix is to make it actually work. @bfetscher may have an idea or at least some thoughts?

[ahmadsalim]

Ah, thanks for the clarification! I was closing some old issues, and thought this was resolved but wasn't closed.