redex icon indicating copy to clipboard operation
redex copied to clipboard

judgment-form generation failure when variable-not-otherwise-mentioned combines with variable-not-in

Open rfindler opened this issue 9 years ago • 0 comments

The call to generate-program here always fails:

#lang racket
(require redex/reduction-semantics)
(define-language L
  (x ::= variable-not-otherwise-mentioned (list x)))

(define-judgment-form L
  #:mode (J I I O)
  [(where x ,(variable-not-in (term (x_a x_b)) 'q))
   ------------------
   (J x_a x_b x)])

(generate-term L #:satisfying (J any_1 any_2 any_3) 4)

The issue seems to be in the ground-or-ok function: https://github.com/racket/redex/blob/745e22c32359a469a2925156b902ba1550e9e378/redex-lib/redex/private/jdg-gen.rkt#L31 which doesn't seem to be treating variable-not-in properly.

rfindler avatar Oct 01 '16 03:10 rfindler