diff --git a/collects/redex/private/generate-term.rkt b/collects/redex/private/generate-term.rkt index 7e02fd9a77..ba4634422a 100644 --- a/collects/redex/private/generate-term.rkt +++ b/collects/redex/private/generate-term.rkt @@ -429,10 +429,20 @@ [(size) (let* ([j-f (lookup-judgment-form-id #'jf/mf-id)] [clauses (judgment-form-gen-clauses j-f)] - [nts (definition-nts #'lang-id stx 'redex-generator)]) + [nts (definition-nts #'lang-id stx 'redex-generator)] + [relation? (judgment-form-relation? j-f)] + [args-stx (if relation? + (syntax/loc #'args (args)) + #'args)]) (with-syntax ([(pat (names ...) (names/ellipses ...)) - (rewrite-side-conditions/check-errs nts 'redex-generator #t #'args)]) - #`(make-jf-gen/proc 'jf/mf-id #,clauses lang-id 'pat size)))] + (rewrite-side-conditions/check-errs nts 'redex-generator #t args-stx)]) + (if relation? + #`(let ([gen-proc (make-jf-gen/proc 'jf/mf-id #,clauses lang-id 'pat size)]) + (λ () + (match (gen-proc) + [`(,jf-name (,trms (... ...))) + `(,jf-name ,@trms)]))) + #`(make-jf-gen/proc 'jf/mf-id #,clauses lang-id 'pat size))))] [_ (raise-syntax-error 'redex-generator "expected an integer depth bound" diff --git a/collects/redex/private/judgment-form.rkt b/collects/redex/private/judgment-form.rkt index 40af3532af..5a9755dfe2 100644 --- a/collects/redex/private/judgment-form.rkt +++ b/collects/redex/private/judgment-form.rkt @@ -1097,32 +1097,7 @@ (λ () #,(check-pats #'(list comp-clauses ...))))))) - #`(values #,(do-compile-judgment-form-proc #'judgment-form-name - #'mode-arg - clauses - rule-names - contracts - nts - #'orig - #'full-def - syn-err-name) - #,(with-syntax* ([(comp-clauses ...) - (map (λ (c) (compile-gen-clause c mode nts syn-err-name - #'judgment-form-name #'lang)) - clauses)]) - (if (identifier? #'orig) - (with-syntax ([prev-mk (judgment-form-mk-gen-clauses (lookup-judgment-form-id #'orig))]) - #`(λ (effective-lang judgment-form-runtime-gen-clauses) - (define mk-prev-clauses (prev-mk effective-lang judgment-form-runtime-gen-clauses)) - (λ () - (append - (mk-prev-clauses) - #,(check-pats - #'(list comp-clauses ...)))))) - #`(λ (effective-lang judgment-form-runtime-gen-clauses) - (λ () - #,(check-pats - #'(list comp-clauses ...))))))))])) + #`(values #,proc-stx #,gen-stx))])) (define-for-syntax (rewrite-relation-prems clauses) (map (λ (c) diff --git a/collects/redex/tests/gen-test.rkt b/collects/redex/tests/gen-test.rkt index aa307e303e..79d4d285e4 100644 --- a/collects/redex/tests/gen-test.rkt +++ b/collects/redex/tests/gen-test.rkt @@ -56,6 +56,11 @@ [(sum (s n_1) n_2 (s n_3)) (sum n_1 n_2 n_3)]) + (define-relation nats + [(r-sum z n n)] + [(r-sum (s n_1) n_2 (s n_3)) + (r-sum n_1 n_2 n_3)]) + (test-equal (judgment-holds (sum z (s z) (s z))) #t) @@ -72,7 +77,11 @@ (match (generate-term nats #:satisfying (sum n_1 n_2 n_3) 5) [`(sum ,l ,r ,res) (test-equal (judgment-holds (sum ,l ,r n) n) - `(,res))]))) + `(,res))]) + (match (generate-term nats #:satisfying (r-sum n_1 n_2 n_3) 5) + [`(r-sum ,l ,r ,res) + (test-equal (term (r-sum ,l ,r ,res)) + #t)]))) (let () diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt index be4dc67a8a..4460150227 100644 --- a/collects/redex/tests/tl-test.rkt +++ b/collects/redex/tests/tl-test.rkt @@ -3014,6 +3014,9 @@ (parameterize ([relation-coverage (list c)]) (term (f 1)) (test (sorted-counts c) '(1 0 0)))) + + ;; coverage for define-relation not working since + ;; it was changed to compile to judgment-form #; (let ([c (make-coverage R)]) (parameterize ([relation-coverage (list c)])