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 67b754d656..fdcfdaf565 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt @@ -193,49 +193,49 @@ "language argument does not contain a definition of the non-terminal ~a, needed by the reduction-relation" red-lang-nt)))) - (let ([cp (compile-pattern - lang - `(in-hole (name ctxt ,pat) - (name exp any)) - #f)]) - (build-reduction-relation - #f - lang - (map - (λ (make-proc) - (make-rewrite-proc - (λ (lang) - (let ([f (make-proc lang)]) - (λ (main-exp exp extend acc) - (let loop ([ms (or (match-pattern cp exp) '())] - [acc acc]) - (cond - [(null? ms) acc] - [else - (let* ([mtch (car ms)] - [bindings (mtch-bindings mtch)]) - (loop (cdr ms) - (f main-exp - (lookup-binding bindings 'exp) - (λ (x) (extend (plug (lookup-binding bindings 'ctxt) x))) - acc)))]))))) - (rewrite-proc-name make-proc) - (rewrite-proc-lhs make-proc) - (rewrite-proc-lhs-src make-proc) - (rewrite-proc-id make-proc))) - (reduction-relation-make-procs red)) - (reduction-relation-rule-names red) - (reduction-relation-lws red) - (let ([orig-pat (reduction-relation-domain-pat red)]) - (cond - [(equal? orig-pat `any) - ;; special case for backwards compatibility: - ;; if there was no #:domain argument, then we - ;; probably should let the compatible closure also - ;; not have a domain - `any] - [else - `(in-hole ,pat ,orig-pat)]))))) + (build-reduction-relation + #f + lang + (map + (λ (make-proc) + (make-rewrite-proc + (λ (lang) + (define f (make-proc lang)) + (define cp (compile-pattern + lang + `(in-hole (name ctxt ,pat) + (name exp any)) + #f)) + (λ (main-exp exp extend acc) + (let loop ([ms (or (match-pattern cp exp) '())] + [acc acc]) + (cond + [(null? ms) acc] + [else + (let* ([mtch (car ms)] + [bindings (mtch-bindings mtch)]) + (loop (cdr ms) + (f main-exp + (lookup-binding bindings 'exp) + (λ (x) (extend (plug (lookup-binding bindings 'ctxt) x))) + acc)))])))) + (rewrite-proc-name make-proc) + (rewrite-proc-lhs make-proc) + (rewrite-proc-lhs-src make-proc) + (rewrite-proc-id make-proc))) + (reduction-relation-make-procs red)) + (reduction-relation-rule-names red) + (reduction-relation-lws red) + (let ([orig-pat (reduction-relation-domain-pat red)]) + (cond + [(equal? orig-pat `any) + ;; special case for backwards compatibility: + ;; if there was no #:domain argument, then we + ;; probably should let the compatible closure also + ;; not have a domain + `any] + [else + `(in-hole ,pat ,orig-pat)])))) (define (apply-reduction-relation/tagged p v) (let loop ([procs (reduction-relation-procs p)] 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 399e615b0d..b5aef188b5 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt @@ -3166,6 +3166,17 @@ "no error raised")) (test #t (regexp-match? #rx"^compatible-closure:.*fred" err-msg))) + +;; this tests that context-closure (and thus compatible-closure) +;; play along properly with way extend-reduction-relation handles +;; language extensions +(let () + (define-language L0 (K ::= number)) + (define r (reduction-relation L0 (--> 5 6))) + (define r0 (context-closure r L0 (hole K))) + (define-language L1 (K ::= string)) + (define r1 (extend-reduction-relation r0 L1)) + (test (apply-reduction-relation r1 (term (5 "14"))) (list '(6 "14")))) (let* ([R (reduction-relation empty-language