diff --git a/collects/redex/private/bmps/metafunction-Name-vertical.png b/collects/redex/private/bmps/metafunction-Name-vertical.png index cffd3e9f29..cde38b7b0f 100644 Binary files a/collects/redex/private/bmps/metafunction-Name-vertical.png and b/collects/redex/private/bmps/metafunction-Name-vertical.png differ diff --git a/collects/redex/private/bmps/metafunction-Name.png b/collects/redex/private/bmps/metafunction-Name.png index 68e075ab29..989837fdae 100644 Binary files a/collects/redex/private/bmps/metafunction-Name.png and b/collects/redex/private/bmps/metafunction-Name.png differ diff --git a/collects/redex/private/bmps/metafunction-TL.png b/collects/redex/private/bmps/metafunction-TL.png index ce08c4c321..81a744f06d 100644 Binary files a/collects/redex/private/bmps/metafunction-TL.png and b/collects/redex/private/bmps/metafunction-TL.png differ diff --git a/collects/redex/private/bmps/metafunctions-multiple.png b/collects/redex/private/bmps/metafunctions-multiple.png index f36bf7fc14..fc46812337 100644 Binary files a/collects/redex/private/bmps/metafunctions-multiple.png and b/collects/redex/private/bmps/metafunctions-multiple.png differ diff --git a/collects/redex/private/reduction-semantics.ss b/collects/redex/private/reduction-semantics.ss index a3a78bb33d..55a7978a09 100644 --- a/collects/redex/private/reduction-semantics.ss +++ b/collects/redex/private/reduction-semantics.ss @@ -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))]