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

Fixes a bug in `where' clause binding.

Browse Source
This commit is contained in:
Casey Klein 2010-06-22 05:42:17 -05:00
parent 550a8b3fa4
commit c6ed9b9a12
2 changed files with 153 additions and 148 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

289
collects/redex/private/reduction-semantics.rkt
View File

@ -7,9 +7,11 @@
"loc-wrapper.ss" "loc-wrapper.ss"
"error.ss" "error.ss"
mzlib/trace mzlib/trace
racket/set
(lib "list.ss") (lib "list.ss")
(lib "etc.ss") (lib "etc.ss")
(for-syntax syntax/parse)) (for-syntax syntax/parse)
(for-syntax racket/set))
(require (for-syntax (lib "name.ss" "syntax") (require (for-syntax (lib "name.ss" "syntax")
"loc-wrapper-ct.ss" "loc-wrapper-ct.ss"
@ -223,78 +225,68 @@
(syntax/loc stx (do-reduction-relation orig-stx extend-reduction-relation orig-reduction-relation #t lang args ...)))])) (syntax/loc stx (do-reduction-relation orig-stx extend-reduction-relation orig-reduction-relation #t lang args ...)))]))
;; the withs, freshs, and side-conditions come in backwards order ;; the withs, freshs, and side-conditions come in backwards order
(define-for-syntax (bind-withs orig-name main lang lang-nts stx where-mode body) (define-for-syntax bind-withs
(let* ([bindings '()] (λ (orig-name main lang lang-nts stx where-mode body [lhs-bound #'()])
[body (let loop ([stx stx]
(let loop ([stx stx] [to-not-be-in main]
[to-not-be-in main]) [bound (apply set lhs-bound)])
(syntax-case stx (fresh) (syntax-case stx (fresh)
[() body] [() body]
[((-where x e) y ...) [((-where x e) y ...)
(or (free-identifier=? #'-where #'where) (or (free-identifier=? #'-where #'where)
(free-identifier=? #'-where #'where/hidden)) (free-identifier=? #'-where #'where/hidden))
(let-values ([(names names/ellipses) (extract-names lang-nts 'reduction-relation #t #'x)]) (let-values ([(names names/ellipses) (extract-names lang-nts 'reduction-relation #t #'x)])
(with-syntax ([(cpat) (generate-temporaries '(compiled-pattern))] (with-syntax ([side-conditions-rewritten (rewrite-side-conditions/check-errs
[side-conditions-rewritten (rewrite-side-conditions/check-errs lang-nts
lang-nts 'reduction-relation
'reduction-relation #f
#f #'x)]
#'x)] [(names ...) names]
[(names ...) names] [(names/ellipses ...) names/ellipses])
[(names/ellipses ...) names/ellipses]) (with-syntax ([(x ...) (generate-temporaries #'(names ...))])
(with-syntax ([(x ...) (generate-temporaries #'(names ...))]) (let ([rest-body (loop #'(y ...) #`(list x ... #,to-not-be-in) bound)])
(set! bindings (cons #`[cpat (compile-pattern #,lang `side-conditions-rewritten #t)] bindings)) #`(let* ([mtchs (match-pattern (compile-pattern #,lang `side-conditions-rewritten #t) (term e))]
(let ([rest-body (loop #'(y ...) #`(list x ... #,to-not-be-in))]) [result (λ (mtch)
#`(let ([mtchs (match-pattern cpat (term e))]) (let ([bindings (mtch-bindings mtch)])
(if mtchs (let ([x (lookup-binding bindings 'names)] ...)
#, (term-let ([names/ellipses x] ...)
(case where-mode #,rest-body))))])
[(flatten) (if mtchs
#`(apply #,
append (case where-mode
(map (λ (mtch) [(flatten)
(let ([bindings (mtch-bindings mtch)]) #`(apply append (map result mtchs))]
(let ([x (lookup-binding bindings 'names)] ...) [(predicate)
(term-let ([names/ellipses x] ...) #`(ormap result mtchs)]
#,rest-body)))) [else (error 'unknown-where-mode "~s" where-mode)])
mtchs))] #f))))))]
[(predicate) [((-side-condition s ...) y ...)
#`(ormap (λ (mtch) (or (free-identifier=? #'-side-condition #'side-condition)
(let ([bindings (mtch-bindings mtch)]) (free-identifier=? #'-side-condition #'side-condition/hidden))
(let ([x (lookup-binding bindings 'names)] ...) #`(and s ... #,(loop #'(y ...) to-not-be-in bound))]
(term-let ([names/ellipses x] ...) [((fresh x) y ...)
#,rest-body)))) (identifier? #'x)
mtchs)] #`(term-let ([x (variable-not-in #,to-not-be-in 'x)])
[else (error 'unknown-where-mode "~s" where-mode)]) #,(loop #'(y ...) #`(list (term x) #,to-not-be-in) bound))]
#f))))))] [((fresh x name) y ...)
[((-side-condition s ...) y ...) (identifier? #'x)
(or (free-identifier=? #'-side-condition #'side-condition) #`(term-let ([x (let ([the-name (term name)])
(free-identifier=? #'-side-condition #'side-condition/hidden)) (verify-name-ok '#,orig-name the-name)
#`(and s ... #,(loop #'(y ...) to-not-be-in))] (variable-not-in #,to-not-be-in the-name))])
[((fresh x) y ...) #,(loop #'(y ...) #`(list (term x) #,to-not-be-in) bound))]
(identifier? #'x) [((fresh (y) (x ...)) z ...)
#`(term-let ([x (variable-not-in #,to-not-be-in 'x)]) #`(term-let ([(y #,'...)
#,(loop #'(y ...) #`(list (term x) #,to-not-be-in)))] (variables-not-in #,to-not-be-in
[((fresh x name) y ...) (map (λ (_ignore_) 'y)
(identifier? #'x) (term (x ...))))])
#`(term-let ([x (let ([the-name (term name)]) #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in) bound))]
(verify-name-ok '#,orig-name the-name) [((fresh (y) (x ...) names) z ...)
(variable-not-in #,to-not-be-in the-name))]) #`(term-let ([(y #,'...)
#,(loop #'(y ...) #`(list (term x) #,to-not-be-in)))] (let ([the-names (term names)]
[((fresh (y) (x ...)) z ...) [len-counter (term (x ...))])
#`(term-let ([(y #,'...) (verify-names-ok '#,orig-name the-names len-counter)
(variables-not-in #,to-not-be-in (variables-not-in #,to-not-be-in the-names))])
(map (λ (_ignore_) 'y) #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in) bound))]))))
(term (x ...))))])
#,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in)))]
[((fresh (y) (x ...) names) z ...)
#`(term-let ([(y #,'...)
(let ([the-names (term names)]
[len-counter (term (x ...))])
(verify-names-ok '#,orig-name the-names len-counter)
(variables-not-in #,to-not-be-in the-names))])
#,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in)))]))])
(values body bindings)))
(define-syntax-set (do-reduction-relation) (define-syntax-set (do-reduction-relation)
(define (do-reduction-relation/proc stx) (define (do-reduction-relation/proc stx)
@ -701,25 +693,26 @@
(let* ([lang-nts (language-id-nts lang-id orig-name)] (let* ([lang-nts (language-id-nts lang-id orig-name)]
[rw-sc (λ (pat) (rewrite-side-conditions/check-errs lang-nts orig-name #t pat))]) [rw-sc (λ (pat) (rewrite-side-conditions/check-errs lang-nts orig-name #t pat))])
(let-values ([(name sides/withs/freshs) (process-extras stx orig-name name-table extras)]) (let-values ([(name sides/withs/freshs) (process-extras stx orig-name name-table extras)])
(let-values ([(names names/ellipses) (extract-names lang-nts orig-name #t from)] (let*-values ([(names names/ellipses) (extract-names lang-nts orig-name #t from)]
[(body-code compile-pattern-bindings) [(body-code)
(bind-withs orig-name (bind-withs orig-name
#'main-exp #'main-exp
lang lang
lang-nts lang-nts
sides/withs/freshs sides/withs/freshs
'flatten 'flatten
#`(list (term #,to)))] #`(list (term #,to))
[(test-case-body-code test-case-compile-pattern-bindings) names/ellipses)]
;; this contains some redundant code, eg. the test-case-compile-pattern-bindings [(test-case-body-code)
;; are (morally) the same as the compile-pattern-bindings ;; this contains some redundant code
(bind-withs orig-name (bind-withs orig-name
#'#t #'#t
#'lang-id2 #'lang-id2
lang-nts lang-nts
sides/withs/freshs sides/withs/freshs
'predicate 'predicate
#'#t)]) #'#t
names/ellipses)])
(with-syntax ([side-conditions-rewritten (rw-sc from)] (with-syntax ([side-conditions-rewritten (rw-sc from)]
[lhs-w/extras (rw-sc #`(side-condition #,from #,test-case-body-code))] [lhs-w/extras (rw-sc #`(side-condition #,from #,test-case-body-code))]
[lhs-source (format "~a:~a:~a" [lhs-source (format "~a:~a:~a"
@ -730,15 +723,12 @@
[lang lang] [lang lang]
[(names ...) names] [(names ...) names]
[(names/ellipses ...) names/ellipses] [(names/ellipses ...) names/ellipses]
[body-code body-code] [body-code body-code])
[(test-case-compile-pattern-bindings ...) test-case-compile-pattern-bindings]
[(compile-pattern-bindings ...) compile-pattern-bindings])
#` #`
(let ([case-id (gensym)]) (let ([case-id (gensym)])
(make-rewrite-proc (make-rewrite-proc
(λ (lang-id) (λ (lang-id)
(let ([cp (compile-pattern lang-id `side-conditions-rewritten #t)] (let ([cp (compile-pattern lang-id `side-conditions-rewritten #t)])
compile-pattern-bindings ...)
(λ (main-exp exp f other-matches) (λ (main-exp exp f other-matches)
(let ([mtchs (match-pattern cp exp)]) (let ([mtchs (match-pattern cp exp)])
(if mtchs (if mtchs
@ -768,7 +758,7 @@
(loop (cdr mtchs) acc)]))])) (loop (cdr mtchs) acc)]))]))
other-matches))))) other-matches)))))
name name
(λ (lang-id2) (let (test-case-compile-pattern-bindings ...) `lhs-w/extras)) (λ (lang-id2) `lhs-w/extras)
lhs-source lhs-source
case-id))))))) case-id)))))))
@ -1163,28 +1153,38 @@
(when (and prev-metafunction (eq? (syntax-e #'name) (syntax-e prev-metafunction))) (when (and prev-metafunction (eq? (syntax-e #'name) (syntax-e prev-metafunction)))
(raise-syntax-error syn-error-name "the extended and extending metafunctions cannot share a name" orig-stx prev-metafunction)) (raise-syntax-error syn-error-name "the extended and extending metafunctions cannot share a name" orig-stx prev-metafunction))
(parse-extras #'((stuff ...) ...)) (parse-extras #'((stuff ...) ...))
(with-syntax ([(((cp-let-bindings ...) rhs/wheres) ...) (let-values ([(lhs-namess lhs-namess/ellipsess)
(map (λ (sc/b rhs) (let loop ([lhss (syntax->list (syntax (lhs ...)))])
(let-values ([(body-code cp-let-bindings) (if (null? lhss)
(bind-withs (values null null)
syn-error-name '() (let-values ([(namess namess/ellipsess)
#'lang lang-nts (loop (cdr lhss))]
sc/b 'flatten [(names names/ellipses)
#`(list (term #,rhs)))]) (extract-names lang-nts syn-error-name #t (car lhss))])
(list cp-let-bindings body-code))) (values (cons names namess)
(cons names/ellipses namess/ellipsess)))))])
(with-syntax ([(rhs/wheres ...)
(map (λ (sc/b rhs names/ellipses)
(bind-withs
syn-error-name '()
#'lang lang-nts
sc/b 'flatten
#`(list (term #,rhs))
names/ellipses))
(syntax->list #'((stuff ...) ...)) (syntax->list #'((stuff ...) ...))
(syntax->list #'(rhs ...)))] (syntax->list #'(rhs ...))
[(((rg-cp-let-bindings ...) rg-rhs/wheres) ...) lhs-namess/ellipsess)]
(map (λ (sc/b rhs) [(rg-rhs/wheres ...)
(let-values ([(body-code cp-let-bindings) (map (λ (sc/b rhs names/ellipses)
(bind-withs (bind-withs
syn-error-name '() syn-error-name '()
#'lang lang-nts #'lang lang-nts
sc/b 'predicate sc/b 'predicate
#`#t)]) #`#t
(list cp-let-bindings body-code))) names/ellipses))
(syntax->list #'((stuff ...) ...)) (syntax->list #'((stuff ...) ...))
(syntax->list #'(rhs ...)))]) (syntax->list #'(rhs ...))
lhs-namess/ellipsess)])
(with-syntax ([(side-conditions-rewritten ...) (with-syntax ([(side-conditions-rewritten ...)
(map (λ (x) (rewrite-side-conditions/check-errs (map (λ (x) (rewrite-side-conditions/check-errs
lang-nts lang-nts
@ -1220,18 +1220,16 @@
#f #f
codom-contract)] codom-contract)]
[(rhs-fns ...) [(rhs-fns ...)
(map (λ (lhs rhs/where) (map (λ (names names/ellipses rhs/where)
(let-values ([(names names/ellipses) (with-syntax ([(names ...) names]
(extract-names lang-nts syn-error-name #t lhs)]) [(names/ellipses ...) names/ellipses]
(with-syntax ([(names ...) names] [rhs/where rhs/where])
[(names/ellipses ...) names/ellipses] (syntax
[rhs/where rhs/where]) (λ (name bindings)
(syntax (term-let-fn ((name name))
(λ (name bindings) (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
(term-let-fn ((name name)) rhs/where))))))
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...) lhs-namess lhs-namess/ellipsess
rhs/where)))))))
(syntax->list (syntax (lhs ...)))
(syntax->list (syntax (rhs/wheres ...))))] (syntax->list (syntax (rhs/wheres ...))))]
[(name2 name-predicate) (generate-temporaries (syntax (name name)))] [(name2 name-predicate) (generate-temporaries (syntax (name name)))]
@ -1243,9 +1241,7 @@
(with-syntax ([defs #`(begin (with-syntax ([defs #`(begin
(define-values (name2 name-predicate) (define-values (name2 name-predicate)
(let ([sc `(side-conditions-rewritten ...)] (let ([sc `(side-conditions-rewritten ...)]
[dsc `dom-side-conditions-rewritten] [dsc `dom-side-conditions-rewritten])
cp-let-bindings ... ...
rg-cp-let-bindings ... ...)
(let ([cases (map (λ (pat rhs-fn rg-lhs src) (let ([cases (map (λ (pat rhs-fn rg-lhs src)
(make-metafunc-case (make-metafunc-case
(compile-pattern lang pat #t) rhs-fn rg-lhs src (gensym))) (compile-pattern lang pat #t) rhs-fn rg-lhs src (gensym)))
@ -1354,7 +1350,7 @@
defs)) defs))
(syntax defs)) (syntax defs))
'disappeared-use 'disappeared-use
(map syntax-local-introduce (syntax->list #'(original-names ...)))))))))))))))] (map syntax-local-introduce (syntax->list #'(original-names ...))))))))))))))))]
[(_ prev-metafunction name lang clauses ...) [(_ prev-metafunction name lang clauses ...)
(begin (begin
(unless (identifier? #'name) (unless (identifier? #'name)
@ -2112,20 +2108,17 @@
(print-failed srcinfo) (print-failed srcinfo)
(fprintf (current-error-port) "found a cycle in the reduction graph\n")] (fprintf (current-error-port) "found a cycle in the reduction graph\n")]
[else [else
(unless (set-equal? expected got equiv?) (let* ([⊆ (λ (s1 s2) (andmap (λ (x1) (memf (λ (x) (equiv? x1 x)) s2)) s1))]
(inc-failures) [set-equal? (λ (s1 s2) (and (⊆ s1 s2) (⊆ s2 s1)))])
(print-failed srcinfo) (unless (set-equal? expected got)
(for-each (inc-failures)
(λ (v2) (fprintf (current-error-port) "expected: ~v\n" v2)) (print-failed srcinfo)
expected) (for-each
(for-each (λ (v2) (fprintf (current-error-port) "expected: ~v\n" v2))
(λ (v1) (fprintf (current-error-port) " actual: ~v\n" v1)) expected)
got))]))) (for-each
(λ (v1) (fprintf (current-error-port) " actual: ~v\n" v1))
(define (set-equal? s1 s2 equiv?) got)))])))
(define (⊆ s1 s2) (andmap (λ (x1) (memf (λ (x) (equiv? x1 x)) s2)) s1))
(and (⊆ s1 s2)
(⊆ s2 s1)))
(define-syntax (test-predicate stx) (define-syntax (test-predicate stx)
(syntax-case stx () (syntax-case stx ()

12
collects/redex/tests/tl-test.rkt
View File

@ -844,6 +844,18 @@
(list '((2 3) 20) (list '((2 3) 20)
'(6 (4 5)))) '(6 (4 5))))
; The scope of a `where' clause includes the left-hand sides
; of subsequent `where' clauses.
(test (apply-reduction-relation
(reduction-relation
grammar
(--> any
1
(where number_1 2)
(where (side-condition any (number? (term number_1))) dontcare)))
'dontcare)
'(1))
; shortcuts like this fail if compilation fails to preserve ; shortcuts like this fail if compilation fails to preserve
; lexical context for side-conditions expressions. ; lexical context for side-conditions expressions.
(test (let ([x #t]) (test (let ([x #t])