suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

fix compatible-closure to deal properly with language extension

Browse Source 
Thanks to David Van Horn for spotting the problem and providing
a nice simple test case

Please include in 6.1
(cherry picked from commit 3666842cd4)
This commit is contained in:
Robby Findler 2014-07-20 07:03:24 -05:00 committed by Ryan Culpepper
parent 3ba5639e04
commit d851817d66
2 changed files with 54 additions and 43 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt
View File

@ -193,11 +193,6 @@
"language argument does not contain a definition of the non-terminal ~a, needed by the reduction-relation" "language argument does not contain a definition of the non-terminal ~a, needed by the reduction-relation"
red-lang-nt)))) red-lang-nt))))
(let ([cp (compile-pattern
lang
`(in-hole (name ctxt ,pat)
(name exp any))
#f)])
(build-reduction-relation (build-reduction-relation
#f #f
lang lang
@ -205,7 +200,12 @@
(λ (make-proc) (λ (make-proc)
(make-rewrite-proc (make-rewrite-proc
(λ (lang) (λ (lang)
(let ([f (make-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) (λ (main-exp exp extend acc)
(let loop ([ms (or (match-pattern cp exp) '())] (let loop ([ms (or (match-pattern cp exp) '())]
[acc acc]) [acc acc])
@ -218,7 +218,7 @@
(f main-exp (f main-exp
(lookup-binding bindings 'exp) (lookup-binding bindings 'exp)
(λ (x) (extend (plug (lookup-binding bindings 'ctxt) x))) (λ (x) (extend (plug (lookup-binding bindings 'ctxt) x)))
acc)))]))))) acc)))]))))
(rewrite-proc-name make-proc) (rewrite-proc-name make-proc)
(rewrite-proc-lhs make-proc) (rewrite-proc-lhs make-proc)
(rewrite-proc-lhs-src make-proc) (rewrite-proc-lhs-src make-proc)
@ -235,7 +235,7 @@
;; not have a domain ;; not have a domain
`any] `any]
[else [else
`(in-hole ,pat ,orig-pat)]))))) `(in-hole ,pat ,orig-pat)]))))
(define (apply-reduction-relation/tagged p v) (define (apply-reduction-relation/tagged p v)
(let loop ([procs (reduction-relation-procs p)] (let loop ([procs (reduction-relation-procs p)]

11
pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt
View File

@ -3167,6 +3167,17 @@
(test #t (regexp-match? #rx"^compatible-closure:.*fred" err-msg))) (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 (let* ([R (reduction-relation
empty-language empty-language
(--> any any id))] (--> any any id))]