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

svn: r13814

Browse Source
This commit is contained in:
Robby Findler 2009-02-24 16:17:35 +00:00
parent 414e3b796e
commit 4c02e3736d
5 changed files with 63 additions and 62 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

BIN
collects/redex/private/bmps/metafunction-Name-vertical.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 4.7 KiB

After

Width:  |  Height:  |  Size: 4.7 KiB

BIN
collects/redex/private/bmps/metafunction-Name.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 4.3 KiB

After

Width:  |  Height:  |  Size: 4.4 KiB

BIN
collects/redex/private/bmps/metafunction-TL.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 4.5 KiB

After

Width:  |  Height:  |  Size: 4.5 KiB

BIN
collects/redex/private/bmps/metafunctions-multiple.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 7.8 KiB

After

Width:  |  Height:  |  Size: 7.9 KiB

125
collects/redex/private/reduction-semantics.ss
View File

@ -523,38 +523,15 @@
(define (do-leaf stx orig-name lang name-table from to extras lang-id)
(let* ([lang-nts (language-id-nts lang-id orig-name)]
[rw-sc (λ (pat) (rewrite-side-conditions/check-errs lang-nts orig-name #t pat))])
(let-values ([(name fresh-vars side-conditions/withs) (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)])
(with-syntax ([side-conditions-rewritten (rw-sc from)]
[lhs-w/extras (rw-sc #`(side-condition #,from #,(bind-withs side-conditions/withs #'#t)))]
[lhs-w/extras (rw-sc #`(side-condition #,from #,(bind-withs orig-name #'#t sides/withs/freshs #'#t)))]
[to to]
[name name]
[lang lang]
[(names ...) names]
[(names/ellipses ...) names/ellipses]
[(fresh-var-clauses ...)
(map (λ (fv-clause)
(syntax-case fv-clause ()
[x
(identifier? #'x)
#'[x (variable-not-in main 'x)]]
[(x name)
(identifier? #'x)
#'[x (let ([the-name (term name)])
(verify-name-ok '#,orig-name the-name)
(variable-not-in main the-name))]]
[((y) (x ...))
#`[(y #,'...)
(variables-not-in main
(map (λ (_ignore_) 'y)
(term (x ...))))]]
[((y) (x ...) names)
#`[(y #,'...)
(let ([the-names (term names)]
[len-counter (term (x ...))])
(verify-names-ok '#,orig-name the-names len-counter)
(variables-not-in main the-names))]]))
fresh-vars)])
[(names/ellipses ...) names/ellipses])
#`(do-leaf-match
name
`side-conditions-rewritten
@ -564,29 +541,52 @@
;; show up in the `fresh' side-conditions, the bindings for the variables
;; show up in the withs, and the withs show up in the 'fresh' side-conditions
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
(term-let (fresh-var-clauses ...)
#,(bind-withs side-conditions/withs
#'(make-successful (term to))))))))))))
#,(bind-withs orig-name #'main sides/withs/freshs
#'(make-successful (term to)))))))))))
;; the withs and side-conditions come in backwards order
(define (bind-withs stx body)
;; the withs, freshs, and side-conditions come in backwards order
(define (bind-withs orig-name main stx body)
(let loop ([stx stx]
[body body])
(syntax-case stx (side-condition where)
(syntax-case stx (side-condition where fresh)
[() body]
[((where x e) y ...)
(loop #'(y ...) #`(term-let ([x (term e)]) #,body))]
[((side-condition s ...) y ...)
(loop #'(y ...) #`(and s ... #,body))])))
(loop #'(y ...) #`(and s ... #,body))]
[((fresh x) y ...)
(identifier? #'x)
(loop #'(y ...) #`(term-let ([x (variable-not-in #,main 'x)]) #,body))]
[((fresh x name) y ...)
(identifier? #'x)
(loop #'(y ...)
#`(term-let ([x (let ([the-name (term name)])
(verify-name-ok '#,orig-name the-name)
(variable-not-in #,main the-name))])
#,body))]
[((fresh (y) (x ...)) z ...)
(loop #'(z ...)
#`(term-let ([(y #,'...)
(variables-not-in #,main
(map (λ (_ignore_) 'y)
(term (x ...))))])
#,body))]
[((fresh (y) (x ...) names) z ...)
(loop #'(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 #,main the-names))])
#,body))])))
(define (process-extras stx orig-name name-table extras)
(let ([the-name #f]
[the-name-stx #f]
[fresh-vars '()]
[side-conditions/withs '()])
[sides/withs/freshs '()])
(let loop ([extras extras])
(cond
[(null? extras) (values the-name fresh-vars side-conditions/withs)]
[(null? extras) (values the-name sides/withs/freshs)]
[else
(syntax-case (car extras) (side-condition fresh where)
[name
@ -618,39 +618,40 @@
(loop (cdr extras))))]
[(fresh var ...)
(begin
(set! fresh-vars
(set! sides/withs/freshs
(append
(map (λ (x)
(syntax-case x ()
[x
(identifier? #'x)
#'x]
[(x name)
(identifier? #'x)
#'(x name)]
[((ys dots2) (xs dots1))
(and (eq? (syntax-e #'dots1) (string->symbol "..."))
(eq? (syntax-e #'dots2) (string->symbol "...")))
#'((ys) (xs dots1))]
[((ys dots2) (xs dots1) names)
(and (eq? (syntax-e #'dots1) (string->symbol "..."))
(eq? (syntax-e #'dots2) (string->symbol "...")))
#'((ys) (xs dots1) names)]
[x
(raise-syntax-error orig-name
"malformed fresh variable clause"
stx
#'x)]))
(syntax->list #'(var ...)))
fresh-vars))
(reverse
(map (λ (x)
(syntax-case x ()
[x
(identifier? #'x)
#'(fresh x)]
[(x name)
(identifier? #'x)
#'(fresh x name)]
[((ys dots2) (xs dots1))
(and (eq? (syntax-e #'dots1) (string->symbol "..."))
(eq? (syntax-e #'dots2) (string->symbol "...")))
#'(fresh (ys) (xs dots1))]
[((ys dots2) (xs dots1) names)
(and (eq? (syntax-e #'dots1) (string->symbol "..."))
(eq? (syntax-e #'dots2) (string->symbol "...")))
#'(fresh (ys) (xs dots1) names)]
[x
(raise-syntax-error orig-name
"malformed fresh variable clause"
stx
#'x)]))
(syntax->list #'(var ...))))
sides/withs/freshs))
(loop (cdr extras)))]
[(side-condition exp ...)
(begin
(set! side-conditions/withs (cons (car extras) side-conditions/withs))
(set! sides/withs/freshs (cons (car extras) sides/withs/freshs))
(loop (cdr extras)))]
[(where x e)
(begin
(set! side-conditions/withs (cons (car extras) side-conditions/withs))
(set! sides/withs/freshs (cons (car extras) sides/withs/freshs))
(loop (cdr extras)))]
[(where . x)
(raise-syntax-error orig-name "malformed where clause" stx (car extras))]