From 62a53f3de78cc10ed385a4cb8015114eb55c2035 Mon Sep 17 00:00:00 2001 From: Matthew Flatt Date: Thu, 4 Mar 2010 23:20:52 +0000 Subject: [PATCH] add 'where/hidden' and 'side-condition/hidden' to redex; adjust typesetting to keep metafunction side conditions in original order svn: r18471 --- collects/redex/private/pict.ss | 28 +++++---- collects/redex/private/reduction-semantics.ss | 58 +++++++++++++++---- collects/redex/redex.scrbl | 36 ++++++++---- 3 files changed, 88 insertions(+), 34 deletions(-) diff --git a/collects/redex/private/pict.ss b/collects/redex/private/pict.ss index 2eeb5a549a..0d1f20e137 100644 --- a/collects/redex/private/pict.ss +++ b/collects/redex/private/pict.ss @@ -792,26 +792,32 @@ (* 2 sep))))) lhss rhss linebreak-list))] [scs (map (lambda (eqn) - (if (null? (list-ref eqn 1)) + (let ([scs (filter (lambda (v) + (not (or (metafunc-extra-side-cond/hidden? v) + (metafunc-extra-where/hidden? v)))) + (reverse (list-ref eqn 1)))]) + (if (null? scs) #f - (let-values ([(fresh where/sc) (partition metafunc-extra-fresh? (list-ref eqn 1))]) + (let-values ([(fresh where/sc) (partition metafunc-extra-fresh? scs)]) (side-condition-pict (foldl (λ (clause picts) - (foldr (λ (l ps) (cons (wrapper->pict l) ps)) - picts (metafunc-extra-fresh-vars clause))) + (foldr (λ (l ps) (cons (wrapper->pict l) ps)) + picts (metafunc-extra-fresh-vars clause))) '() fresh) (map (match-lambda - [(struct metafunc-extra-where (lhs rhs)) - (cons (wrapper->pict lhs) (wrapper->pict rhs))] - [(struct metafunc-extra-side-cond (expr)) - (wrapper->pict expr)]) + [(struct metafunc-extra-where (lhs rhs)) + (cons (wrapper->pict lhs) (wrapper->pict rhs))] + [(struct metafunc-extra-side-cond (expr)) + (wrapper->pict expr)]) where/sc) (if (memq style '(up-down/vertical-side-conditions - left-right/vertical-side-conditions)) + left-right/vertical-side-conditions + left-right*/vertical-side-conditions)) 0 (if (memq style '(up-down/compact-side-conditions - left-right/compact-side-conditions)) + left-right/compact-side-conditions + left-right*/compact-side-conditions)) max-line-w/pre-sc - +inf.0)))))) + +inf.0))))))) eqns)]) (case style [(left-right left-right/vertical-side-conditions left-right/compact-side-conditions left-right/beside-side-conditions) diff --git a/collects/redex/private/reduction-semantics.ss b/collects/redex/private/reduction-semantics.ss index 182ac20a02..38c6f72a5d 100644 --- a/collects/redex/private/reduction-semantics.ss +++ b/collects/redex/private/reduction-semantics.ss @@ -227,9 +227,11 @@ [body (let loop ([stx stx] [to-not-be-in main]) - (syntax-case stx (side-condition where fresh) + (syntax-case stx (fresh) [() body] - [((where x e) y ...) + [((-where x e) y ...) + (or (free-identifier=? #'-where #'where) + (free-identifier=? #'-where #'where/hidden)) (let-values ([(names names/ellipses) (extract-names lang-nts 'reduction-relation #t #'x)]) (with-syntax ([(cpat) (generate-temporaries '(compiled-pattern))] [side-conditions-rewritten (rewrite-side-conditions/check-errs @@ -264,7 +266,9 @@ mtchs)] [else (error 'unknown-where-mode "~s" where-mode)]) #f))))))] - [((side-condition s ...) y ...) + [((-side-condition s ...) y ...) + (or (free-identifier=? #'-side-condition #'side-condition) + (free-identifier=? #'-side-condition #'side-condition/hidden)) #`(and s ... #,(loop #'(y ...) to-not-be-in))] [((fresh x) y ...) (identifier? #'x) @@ -402,7 +406,7 @@ (cond [(null? stuffs) (values label (reverse scs/withs) (reverse fvars))] [else - (syntax-case (car stuffs) (where fresh variable-not-in) + (syntax-case (car stuffs) (fresh variable-not-in) [(fresh xs ...) (loop (cdr stuffs) label @@ -429,13 +433,17 @@ #'y)]))) (syntax->list #'(xs ...)))) fvars))] - [(where x e) + [(-where x e) + (or (free-identifier=? #'-where #'where) + (free-identifier=? #'-where #'where/hidden)) (loop (cdr stuffs) label (cons #`(cons #,(to-lw/proc #'x) #,(to-lw/proc #'e)) scs/withs) fvars)] - [(side-condition sc) + [(-side-condition sc) + (or (free-identifier=? #'-side-condition #'side-condition) + (free-identifier=? #'-side-condition #'side-condition/hidden)) (loop (cdr stuffs) label (cons (to-lw/uq/proc #'sc) scs/withs) @@ -769,7 +777,7 @@ (cond [(null? extras) '()] [else - (syntax-case (car extras) (side-condition fresh where) + (syntax-case (car extras) (fresh) [name (or (identifier? (car extras)) (string? (syntax-e (car extras)))) @@ -823,11 +831,17 @@ #'x)])) (syntax->list #'(var ...))) (loop (cdr extras)))] - [(side-condition exp ...) + [(-side-condition exp ...) + (or (free-identifier=? #'-side-condition #'side-condition) + (free-identifier=? #'-side-condition #'side-condition/hidden)) (cons (car extras) (loop (cdr extras)))] - [(where x e) + [(-where x e) + (or (free-identifier=? #'-where #'where) + (free-identifier=? #'-where #'where/hidden)) (cons (car extras) (loop (cdr extras)))] - [(where . x) + [(-where . x) + (or (free-identifier=? #'-where #'where) + (free-identifier=? #'-where #'where/hidden)) (raise-syntax-error orig-name "malformed where clause" stx (car extras))] [_ (raise-syntax-error orig-name "unknown extra" stx (car extras))])]))]) @@ -1037,7 +1051,9 @@ ;; Intermediate structures recording clause "extras" for typesetting. (define-struct metafunc-extra-side-cond (expr)) +(define-struct (metafunc-extra-side-cond/hidden metafunc-extra-side-cond) ()) (define-struct metafunc-extra-where (lhs rhs)) +(define-struct (metafunc-extra-where/hidden metafunc-extra-where) ()) (define-struct metafunc-extra-fresh (vars)) (define-syntax (in-domain? stx) @@ -1273,7 +1289,9 @@ (map (λ (hm) (map (λ (lst) - (syntax-case lst (side-condition where unquote) + (syntax-case lst (unquote + side-condition where + side-condition/hidden where/hidden) [(where pat (unquote (f _ _))) (and (or (identifier? #'pat) (andmap identifier? (syntax->list #'pat))) @@ -1289,8 +1307,14 @@ [(where pat exp) #`(make-metafunc-extra-where #,(to-lw/proc #'pat) #,(to-lw/proc #'exp))] + [(where/hidden pat exp) + #`(make-metafunc-extra-where/hidden + #,(to-lw/proc #'pat) #,(to-lw/proc #'exp))] [(side-condition x) #`(make-metafunc-extra-side-cond + #,(to-lw/uq/proc #'x))] + [(side-condition/hidden x) + #`(make-metafunc-extra-side-cond/hidden #,(to-lw/uq/proc #'x))])) (reverse (syntax->list hm)))) (syntax->list #'(... seq-of-tl-side-cond/binds)))] @@ -1417,15 +1441,23 @@ (λ (stuffs) (for-each (λ (stuff) - (syntax-case stuff (where side-condition) + (syntax-case stuff (where side-condition where/hidden side-condition/hidden) [(side-condition tl-side-conds ...) (void)] + [(side-condition/hidden tl-side-conds ...) + (void)] [(where x e) (void)] + [(where/hidden x e) + (void)] [(where . args) (raise-syntax-error 'define-metafunction "malformed where clause" stuff)] + [(where/hidden . args) + (raise-syntax-error 'define-metafunction + "malformed where/hidden clause" + stuff)] [_ (raise-syntax-error 'define-metafunction "expected a side-condition or where clause" @@ -2153,7 +2185,9 @@ (struct-out metafunc-case) (struct-out metafunc-extra-side-cond) + (struct-out metafunc-extra-side-cond/hidden) (struct-out metafunc-extra-where) + (struct-out metafunc-extra-where/hidden) (struct-out metafunc-extra-fresh) (struct-out binds)) diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl index 0df36e577a..5607b322df 100644 --- a/collects/redex/redex.scrbl +++ b/collects/redex/redex.scrbl @@ -721,10 +721,11 @@ The side-conditions are expected to all hold, and have the format of the second argument to the @pattech[side-condition] pattern, described above. -Each @scheme[where] clauses binds a variable and the side-conditions -(and @scheme[where] clauses) that follow the where declaration are in -scope of the where declaration. The bindings are the same as -bindings in a @scheme[term-let] expression. +Each @scheme[where] clause acts as a side condition requiring a +successful pattern match, and it can bind pattern variables in the +side-conditions (and @scheme[where] clauses) that follow and in the +reduction result. The bindings are the same as bindings in a +@scheme[term-let] expression. As an example, this @@ -884,7 +885,7 @@ All of the exports in this section are provided both by all non-GUI portions of Redex) and also exported by @schememodname[redex] (which includes all of Redex). -@defform/subs[#:literals (: ->) +@defform/subs[#:literals (: -> where side-condition side-condition/hidden where/hidden) (define-metafunction language contract [(name @#,ttpattern ...) @#,tttterm extras ...] @@ -892,7 +893,9 @@ all non-GUI portions of Redex) and also exported by ([contract (code:line) (code:line id : @#,ttpattern ... -> @#,ttpattern)] [extras (side-condition scheme-expression) - (where tl-pat @#,tttterm)] + (side-condition/hidden scheme-expression) + (where tl-pat @#,tttterm) + (where/hidden tl-pat @#,tttterm)] [tl-pat identifier (tl-pat-ele ...)] [tl-pat-ele tl-pat (code:line tl-pat ... (code:comment "a literal ellipsis"))])]{ @@ -902,11 +905,22 @@ expressions. The first argument indicates the language used to resolve non-terminals in the pattern expressions. Each of the rhs-expressions is implicitly wrapped in @|tttterm|. -If specified, the side-conditions are collected with -@scheme[and] and used as guards on the case being matched. The -argument to each side-condition should be a Scheme -expression, and the pattern variables in the @|ttpattern| are -bound in that expression. +All side-conditions provided with @scheme[side-condition] and +@scheme[hidden-side-condition] are collected with @scheme[and] and +used as guards on the case being matched. The argument to each +side-condition should be a Scheme expression, and the pattern +variables in the @|ttpattern| are bound in that expression. A +@scheme[side-condition/hidden] form is the same as +@scheme[side-condition], except that the side condition is not +rendered when typesetting via @schememodname[redex/pict]. + +Each @scheme[where] clause acts as a side condition requiring a +successful pattern match, and it can bind pattern variables in the +side-conditions (and @scheme[where] clauses) that follow and in the +metafunction result. The bindings are the same as bindings in a +@scheme[term-let] expression. A @scheme[where/hidden] clause is the +same as a @scheme[where] clause, but the clause is not +rendered when typesetting via @schememodname[redex/pict]. Raises an exception recognized by @scheme[exn:fail:redex?] if no clauses match, if one of the clauses matches multiple ways