redex
redex copied to clipboard
judgment-form generation failure when variable-not-otherwise-mentioned combines with variable-not-in
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.