add 'where/hidden' and 'side-condition/hidden' to redex; adjust typesetting to keep metafunction side conditions in original order
svn: r18471
This commit is contained in:
Matthew Flatt
parent
e703d52b94
commit
62a53f3de7
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user