diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt index bcd8563b29..e066e66db0 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt @@ -754,11 +754,12 @@ (define lang-nts (language-id-nts lang-id 'reduction-relation)) (define (rw-sc pat) (rewrite-side-conditions/check-errs lang-id orig-name #t pat)) (define-values (name computed-name sides/withs/freshs) (process-extras stx orig-name name-table extras)) + (define rt-lang-id (car (generate-temporaries (list lang)))) (with-syntax ([(from-syncheck-expr side-conditions-rewritten (names ...) (names/ellipses ...)) (rw-sc from)]) (define body-code (bind-withs orig-name #'main-exp - lang + rt-lang-id lang-nts lang-id sides/withs/freshs @@ -799,11 +800,12 @@ lhs-syncheck-expr (build-rewrite-proc/leaf `side-conditions-rewritten - (λ (main-exp bindings) - #,(bind-pattern-names 'reduction-relation - #'(names/ellipses ...) - #'((lookup-binding bindings 'names) ...) - #'body-code)) + (λ (#,rt-lang-id) + (λ (main-exp bindings) + #,(bind-pattern-names 'reduction-relation + #'(names/ellipses ...) + #'((lookup-binding bindings 'names) ...) + #'body-code))) lhs-source name (λ (lang-id2) `lhs-w/extras)))))) @@ -925,13 +927,14 @@ (do-reduction-relation/proc stx)) (define (build-rewrite-proc/leaf side-conditions-rewritten - build-really-matched + build-really-matched/lang-arg lhs-source name lhs-w/extras-proc) (let ([case-id (gensym)]) (make-rewrite-proc (λ (lang-id) + (define build-really-matched (build-really-matched/lang-arg lang-id)) (let ([cp (compile-pattern lang-id side-conditions-rewritten #t)]) (λ (main-exp exp f other-matches) (let ([mtchs (match-pattern cp exp)]) diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt index 16ac43a07c..3781027d29 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt @@ -2160,6 +2160,24 @@ (test (apply-reduction-relation red2 (term (X q))) (list (term (X z)) (term (X w))))) + (let () + (define-language L (M ::= number)) + (define r (reduction-relation L (--> M M (where M M)))) + (define-extended-language L1 L (M ::= string)) + (define r1 (extend-reduction-relation r L1)) + (test (apply-reduction-relation r1 "7") '("7"))) + + (let () + (define-language L (M ::= number)) + (define-extended-language L1 L (M ::= string)) + (define-judgment-form L + #:mode (id I O) + #:contract (id any any) + [(id any any)]) + (define t (reduction-relation L (--> M M (judgment-holds (id M M))))) + (define t1 (extend-reduction-relation t L1)) + (test (apply-reduction-relation t1 "7") '("7"))) + (test (reduction-relation->rule-names (reduction-relation empty-language