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

generalize rule-pict-style to allow more customization of reduction-relation layouts

Browse Source
This commit is contained in:
Robby Findler 2014-10-23 09:48:31 -05:00
parent 375abf3c2b
commit 58662d2208
6 changed files with 170 additions and 90 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

42
pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
View File

@ -3156,7 +3156,7 @@ are on the same lines as the rule, instead of on their own line below.
} }
@defthing[reduction-rule-style/c flat-contract?]{ @defthing[reduction-rule-style/c contract?]{
A contract equivalent to A contract equivalent to
@ -3165,8 +3165,44 @@ A contract equivalent to
'vertical-overlapping-side-conditions 'vertical-overlapping-side-conditions
'horizontal 'horizontal
'horizontal-left-align 'horizontal-left-align
'horizontal-side-conditions-same-line) 'horizontal-side-conditions-same-line
]} (-> (listof rule-pict-info?) pict?))]
The symbols indicate various pre-defined styles. The procedure
implements new styles; it is give the @racket[rule-pict-info?]
values, one for each clause in the reduction relation,
and is expected to combine them into a single @racket[pict?]
}
@defproc[(rule-pict-info? [x any/c]) boolean?]{
A predicate that recognizes information about a rule for use
in rendering the rule as a @racket[pict?].
}
@defproc[(rule-pict-info-arrow [rule-pict-info rule-pict-info?]) symbol?]{
Extracts the arrow used for this rule. See also @racket[arrow->pict].
}
@defproc[(rule-pict-info-lhs [rule-pict-info rule-pict-info?]) pict?]{
Extracts a pict for the left-hand side of this rule.
}
@defproc[(rule-pict-info-rhs [rule-pict-info rule-pict-info?]) pict?]{
Extracts a pict for the right-hand side of this rule.
}
@defproc[(rule-pict-info-label [rule-pict-info rule-pict-info?]) (or/c symbol? #f)]{
Returns the label used for this rule, unless there is no label
for the rule or @racket[_computed-label] was used,
in which case this returns @racket[#f].
}
@defproc[(rule-pict-info-computed-label [rule-pict-info rule-pict-info?]) (or/c pict? #f)]{
Returns a pict for the typeset version of the label of this rule, when
@racket[_computed-label] was used. Otherwise, returns @racket[#f].
}
@defproc[(rule-pict-info->side-condition-pict [rule-pict-info rule-pict-info?]
[max-width real? +inf.0])
pict?]{
Builds a pict for the @racket[_side-condition]s and @racket[_where] clauses
for @racket[rule-pict-info], attempting to keep the width under @racket[max-width].
}
@defparam[arrow-space space natural-number/c]{ @defparam[arrow-space space natural-number/c]{

36
pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt
View File

@ -513,24 +513,24 @@
(extract-pattern-binds #'lhs)] (extract-pattern-binds #'lhs)]
[((tl-id . tl-pat) ...) [((tl-id . tl-pat) ...)
(extract-term-let-binds #'rhs)]) (extract-term-let-binds #'rhs)])
#`(make-rule-pict 'arrow #`(make-rule-pict-info 'arrow
#,(to-lw/proc #'lhs) #,(to-lw/proc #'lhs)
#,(to-lw/proc #'rhs) #,(to-lw/proc #'rhs)
#,label #,label
#,(and computed-label #,(and computed-label
(to-lw/proc #`,#,computed-label)) (to-lw/proc #`,#,computed-label))
(list scs/withs ... (list scs/withs ...
#,@(map (λ (bind-id bind-pat) #,@(map (λ (bind-id bind-pat)
#`(cons #,(to-lw/proc bind-id) #`(cons #,(to-lw/proc bind-id)
#,(to-lw/proc bind-pat))) #,(to-lw/proc bind-pat)))
(syntax->list #'(bind-id ...)) (syntax->list #'(bind-id ...))
(syntax->list #'(bind-pat ...))) (syntax->list #'(bind-pat ...)))
#,@(map (λ (tl-id tl-pat) #,@(map (λ (tl-id tl-pat)
#`(cons #,(to-lw/proc tl-id) #`(cons #,(to-lw/proc tl-id)
#,(to-lw/uq/proc tl-pat))) #,(to-lw/uq/proc tl-pat)))
(syntax->list #'(tl-id ...)) (syntax->list #'(tl-id ...))
(syntax->list #'(tl-pat ...)))) (syntax->list #'(tl-pat ...))))
(list fvars ...))))] (list fvars ...))))]
;; just skip over junk here, since syntax error checks elsewhere will catch this ;; just skip over junk here, since syntax error checks elsewhere will catch this
[_ #f])) [_ #f]))

7
pkgs/redex-pkgs/redex-lib/redex/private/struct.rkt
View File

@ -14,9 +14,12 @@
empty-reduction-relation empty-reduction-relation
make-rewrite-proc rewrite-proc? rewrite-proc-name make-rewrite-proc rewrite-proc? rewrite-proc-name
rewrite-proc-lhs rewrite-proc-lhs-src rewrite-proc-id rewrite-proc-lhs rewrite-proc-lhs-src rewrite-proc-id
(struct-out rule-pict)) (struct-out rule-pict-info))
(define-struct rule-pict (arrow lhs rhs label computed-label side-conditions/pattern-binds fresh-vars)) (define-struct rule-pict-info (arrow
lhs rhs
label computed-label
side-conditions/pattern-binds fresh-vars))
;; type proc = (exp exp (any -> any) (listof any) -> (listof any))) ;; type proc = (exp exp (any -> any) (listof any) -> (listof any)))
;; a proc is a `cached' version of a make-proc, specialized to a particular language ;; a proc is a `cached' version of a make-proc, specialized to a particular language

17
pkgs/redex-pkgs/redex-pict-lib/redex/pict.rkt
View File

@ -3,6 +3,7 @@
(require racket/contract (require racket/contract
"private/pict.rkt" "private/pict.rkt"
"private/core-layout.rkt" "private/core-layout.rkt"
redex/private/struct
redex/private/loc-wrapper redex/private/loc-wrapper
redex/reduction-semantics redex/reduction-semantics
texpict/mrpict) texpict/mrpict)
@ -13,7 +14,8 @@
'vertical-overlapping-side-conditions 'vertical-overlapping-side-conditions
'horizontal 'horizontal
'horizontal-left-align 'horizontal-left-align
'horizontal-side-conditions-same-line)) 'horizontal-side-conditions-same-line
(-> (listof rule-pict-info?) pict?)))
(provide reduction-rule-style/c render-term term->pict (provide reduction-rule-style/c render-term term->pict
term->pict/pretty-write term->pict/pretty-write
@ -32,7 +34,8 @@
[reduction-relation->pict (->* (reduction-relation?) [reduction-relation->pict (->* (reduction-relation?)
(#:style reduction-rule-style/c) (#:style reduction-rule-style/c)
pict?)] pict?)]
[render-reduction-relation-rules (parameter/c (or/c false/c (listof (or/c symbol? string? exact-nonnegative-integer?))))] [render-reduction-relation-rules
(parameter/c (or/c #f (listof (or/c symbol? string? exact-nonnegative-integer?))))]
[language->pict (->* (compiled-lang?) [language->pict (->* (compiled-lang?)
(#:nts (or/c false/c (listof (or/c string? symbol?)))) (#:nts (or/c false/c (listof (or/c string? symbol?))))
@ -45,7 +48,15 @@
[result (file) [result (file)
(if (path-string? file) (if (path-string? file)
void? void?
pict?)])]) pict?)])]
[rule-pict-info-arrow (-> rule-pict-info? symbol?)]
[rule-pict-info-lhs (-> rule-pict-info? pict?)]
[rule-pict-info-rhs (-> rule-pict-info? pict?)]
[rule-pict-info-label (-> rule-pict-info? (or/c symbol? #f))]
[rule-pict-info-computed-label (-> rule-pict-info? (or/c pict? #f))]
[rule-pict-info->side-condition-pict (->* (rule-pict-info?) ((and/c positive? real?)) pict?)]
[rule-pict-info? (-> any/c boolean?)])
; syntax ; syntax
(provide relation->pict (provide relation->pict

135
pkgs/redex-pkgs/redex-pict-lib/redex/private/pict.rkt
View File

@ -84,7 +84,9 @@
set-arrow-pict! set-arrow-pict!
arrow->pict arrow->pict
horizontal-bar-spacing horizontal-bar-spacing
relation-clauses-combine) relation-clauses-combine
rule-pict-info->side-condition-pict)
(provide/contract (provide/contract
[linebreaks (parameter/c (or/c #f (listof boolean?)))]) [linebreaks (parameter/c (or/c #f (listof boolean?)))])
@ -130,7 +132,7 @@
(for ([rp (in-list (reduction-relation-lws rr))] (for ([rp (in-list (reduction-relation-lws rr))]
[i (in-naturals)]) [i (in-naturals)])
(hash-set! ht i rp) (hash-set! ht i rp)
(hash-set! ht (rule-pict-label rp) rp)) (hash-set! ht (rule-pict-info-label rp) rp))
(map (lambda (label) (map (lambda (label)
(hash-ref ht (if (string? label) (hash-ref ht (if (string? label)
(string->symbol label) (string->symbol label)
@ -159,25 +161,25 @@
(define ((rr-lws->trees nts) rp) (define ((rr-lws->trees nts) rp)
(let ([tp (λ (x) (lw->pict nts x))]) (let ([tp (λ (x) (lw->pict nts x))])
(make-rule-pict (rule-pict-arrow rp) (make-rule-pict-info (rule-pict-info-arrow rp)
(tp (rule-pict-lhs rp)) (tp (rule-pict-info-lhs rp))
(tp (rule-pict-rhs rp)) (tp (rule-pict-info-rhs rp))
(rule-pict-label rp) (rule-pict-info-label rp)
(and (rule-pict-computed-label rp) (and (rule-pict-info-computed-label rp)
(let ([rewritten (apply-rewrites (rule-pict-computed-label rp))]) (let ([rewritten (apply-rewrites (rule-pict-info-computed-label rp))])
(and (not (and (rule-pict-label rp) (and (not (and (rule-pict-info-label rp)
(let has-unq? ([x rewritten]) (let has-unq? ([x rewritten])
(and (lw? x) (and (lw? x)
(or (lw-unq? x) (or (lw-unq? x)
(and (list? (lw-e x)) (and (list? (lw-e x))
(ormap has-unq? (lw-e x)))))))) (ormap has-unq? (lw-e x))))))))
(tp rewritten)))) (tp rewritten))))
(map (lambda (v) (map (lambda (v)
(if (pair? v) (if (pair? v)
(where-pict (tp (car v)) (tp (cdr v))) (where-pict (tp (car v)) (tp (cdr v)))
(tp v))) (tp v)))
(rule-pict-side-conditions/pattern-binds rp)) (rule-pict-info-side-conditions/pattern-binds rp))
(map tp (rule-pict-fresh-vars rp))))) (map tp (rule-pict-info-fresh-vars rp)))))
(define current-label-extra-space (make-parameter 0)) (define current-label-extra-space (make-parameter 0))
(define reduction-relation-rule-separation (make-parameter 4)) (define reduction-relation-rule-separation (make-parameter 4))
@ -187,14 +189,14 @@
[max-rhs (apply max [max-rhs (apply max
0 0
(map pict-width (map pict-width
(map rule-pict-rhs rps)))] (map rule-pict-info-rhs rps)))]
[max-w (apply max [max-w (apply max
0 0
(map (lambda (rp) (map (lambda (rp)
(+ sep sep (+ sep sep
(pict-width (rule-pict-lhs rp)) (pict-width (rule-pict-info-lhs rp))
(pict-width (arrow->pict (rule-pict-arrow rp))) (pict-width (arrow->pict (rule-pict-info-arrow rp)))
(pict-width (rule-pict-rhs rp)))) (pict-width (rule-pict-info-rhs rp))))
rps))]) rps))])
(table 4 (table 4
(apply (apply
@ -203,23 +205,24 @@
(for/list ([rp (in-list rps)] (for/list ([rp (in-list rps)]
[i (in-naturals 1)]) [i (in-naturals 1)])
(let ([arrow (hbl-append (blank (arrow-space) 0) (let ([arrow (hbl-append (blank (arrow-space) 0)
(arrow->pict (rule-pict-arrow rp)) (arrow->pict (rule-pict-info-arrow rp))
(blank (arrow-space) 0))] (blank (arrow-space) 0))]
[lhs (rule-pict-lhs rp)] [lhs (rule-pict-info-lhs rp)]
[rhs (rule-pict-rhs rp)] [rhs (rule-pict-info-rhs rp)]
[spc (basic-text " " (default-style))] [spc (basic-text " " (default-style))]
[label (hbl-append (blank (label-space) 0) (rp->pict-label rp))] [label (hbl-append (blank (label-space) 0) (rp->pict-label rp))]
[sep (blank 4)]) [sep (blank 4)])
(append (append
(if side-conditions-same-line? (if side-conditions-same-line?
(list lhs arrow (list lhs arrow
(hbl-append rhs (hbl-append
(let ([sc (rp->side-condition-pict rp max-w)]) rhs
(inset sc (min 0 (- max-rhs (pict-width sc))) 0 0 0))) (let ([sc (rule-pict-info->side-condition-pict rp max-w)])
(inset sc (min 0 (- max-rhs (pict-width sc))) 0 0 0)))
label) label)
(list lhs arrow rhs label (list lhs arrow rhs label
(blank) (blank) (blank) (blank)
(let ([sc (rp->side-condition-pict rp max-w)]) (let ([sc (rule-pict-info->side-condition-pict rp max-w)])
(inset sc (min 0 (- max-rhs (pict-width sc))) 0 0 0)) (inset sc (min 0 (- max-rhs (pict-width sc))) 0 0 0))
(blank))) (blank)))
(if (= len i) (if (= len i)
@ -235,16 +238,16 @@
(define ((make-vertical-style side-condition-combiner) rps) (define ((make-vertical-style side-condition-combiner) rps)
(let* ([mk-top-line-spacer (let* ([mk-top-line-spacer
(λ (rp) (λ (rp)
(hbl-append (rule-pict-lhs rp) (hbl-append (rule-pict-info-lhs rp)
(basic-text " " (default-style)) (basic-text " " (default-style))
(arrow->pict (rule-pict-arrow rp)) (arrow->pict (rule-pict-info-arrow rp))
(basic-text " " (default-style)) (basic-text " " (default-style))
(rp->pict-label rp)))] (rp->pict-label rp)))]
[mk-bot-line-spacer [mk-bot-line-spacer
(λ (rp) (λ (rp)
(rt-superimpose (rt-superimpose
(rule-pict-rhs rp) (rule-pict-info-rhs rp)
(rp->side-condition-pict rp +inf.0)))] (rule-pict-info->side-condition-pict rp +inf.0)))]
[multi-line-spacer [multi-line-spacer
(if (null? rps) (if (null? rps)
(blank) (blank)
@ -267,14 +270,14 @@
(side-condition-combiner (side-condition-combiner
(vl-append (vl-append
(ltl-superimpose (ltl-superimpose
(htl-append (rule-pict-lhs rp) (htl-append (rule-pict-info-lhs rp)
(basic-text " " (default-style)) (basic-text " " (default-style))
(arrow->pict (rule-pict-arrow rp))) (arrow->pict (rule-pict-info-arrow rp)))
(rtl-superimpose (rtl-superimpose
spacer spacer
(rp->pict-label rp))) (rp->pict-label rp)))
(rule-pict-rhs rp)) (rule-pict-info-rhs rp))
(rp->side-condition-pict rp +inf.0))) (rule-pict-info->side-condition-pict rp +inf.0)))
rps) rps)
(blank 0 (reduction-relation-rule-separation))))))) (blank 0 (reduction-relation-rule-separation)))))))
@ -291,10 +294,10 @@
(compact-vertical-min-width) (compact-vertical-min-width)
(map pict-width (map pict-width
(append (append
(map rule-pict-lhs rps) (map rule-pict-info-lhs rps)
(map rule-pict-rhs rps))))] (map rule-pict-info-rhs rps))))]
[scs (map (lambda (rp) [scs (map (lambda (rp)
(rp->side-condition-pict rp max-w)) (rule-pict-info->side-condition-pict rp max-w))
rps)] rps)]
[labels (map (lambda (rp) [labels (map (lambda (rp)
(hbl-append (blank (label-space) 0) (rp->pict-label rp))) (hbl-append (blank (label-space) 0) (rp->pict-label rp)))
@ -308,9 +311,10 @@
[one-line [one-line
(lambda (sep?) (lambda (sep?)
(lambda (rp sc label) (lambda (rp sc label)
(let ([arrow (hbl-append (arrow->pict (rule-pict-arrow rp)) (blank (arrow-space) 0))] (let ([arrow (hbl-append (arrow->pict (rule-pict-info-arrow rp))
[lhs (rule-pict-lhs rp)] (blank (arrow-space) 0))]
[rhs (rule-pict-rhs rp)] [lhs (rule-pict-info-lhs rp)]
[rhs (rule-pict-info-rhs rp)]
[spc (basic-text " " (default-style))] [spc (basic-text " " (default-style))]
[sep (blank (compact-vertical-min-width) [sep (blank (compact-vertical-min-width)
(reduction-relation-rule-separation))] (reduction-relation-rule-separation))]
@ -392,16 +396,16 @@
(make-parameter (lambda (lhs rhs) (make-parameter (lambda (lhs rhs)
(htl-append lhs (make-=) rhs)))) (htl-append lhs (make-=) rhs))))
(define (rp->side-condition-pict rp max-w) (define (rule-pict-info->side-condition-pict rp [max-w +inf.0])
(side-condition-pict (rule-pict-fresh-vars rp) (side-condition-pict (rule-pict-info-fresh-vars rp)
(rule-pict-side-conditions/pattern-binds rp) (rule-pict-info-side-conditions/pattern-binds rp)
max-w)) max-w))
(define (rp->pict-label rp) (define (rp->pict-label rp)
(cond [(rule-pict-computed-label rp) => bracket] (cond [(rule-pict-info-computed-label rp) => bracket]
[(rule-pict-label rp) [(rule-pict-info-label rp)
(string->bracketed-label (string->bracketed-label
(format "~a" (rule-pict-label rp)))] (format "~a" (rule-pict-info-label rp)))]
[else (blank)])) [else (blank)]))
(define (string->bracketed-label str) (define (string->bracketed-label str)
@ -422,18 +426,23 @@
(define (make-horiz-space picts) (blank (pict-width (apply cc-superimpose picts)) 0)) (define (make-horiz-space picts) (blank (pict-width (apply cc-superimpose picts)) 0))
(define rule-pict-style (make-parameter 'vertical)) (define rule-pict-style (make-parameter 'vertical))
(define rule-pict-style-table
(make-hash
(list (cons 'vertical rule-picts->pict/vertical)
(cons 'compact-vertical rule-picts->pict/compact-vertical)
(cons 'vertical-overlapping-side-conditions
rule-picts->pict/vertical-overlapping-side-conditions)
(cons 'horizontal-left-align
(rule-picts->pict/horizontal ltl-superimpose #f))
(cons 'horizontal-side-conditions-same-line
(rule-picts->pict/horizontal rtl-superimpose #t))
(cons 'horizontal
(rule-picts->pict/horizontal rtl-superimpose #f)))))
(define (rule-pict-style->proc style) (define (rule-pict-style->proc style)
(case style (cond
[(vertical) rule-picts->pict/vertical] [(symbol? style) (hash-ref rule-pict-style-table style)]
[(compact-vertical) rule-picts->pict/compact-vertical] [else style]))
[(vertical-overlapping-side-conditions)
rule-picts->pict/vertical-overlapping-side-conditions]
[(horizontal-left-align)
(rule-picts->pict/horizontal ltl-superimpose #f)]
[(horizontal-side-conditions-same-line)
(rule-picts->pict/horizontal rtl-superimpose #t)]
[else ;; horizontal
(rule-picts->pict/horizontal rtl-superimpose #f)]))
(define (mk-arrow-pict sz style) (define (mk-arrow-pict sz style)
(let ([cache (make-hash)]) (let ([cache (make-hash)])

23
pkgs/redex-pkgs/redex-test/redex/tests/pict-test.rkt
View File

@ -97,4 +97,25 @@
(render-judgment-form deep-empty))) (render-judgment-form deep-empty)))
0) 0)
(printf "pict-test.rkt passed\n") ;; check the contracts for the various rule-pict functions
(void
(parameterize ([rule-pict-style
(λ (rule-pict-infos)
(for ([r (in-list rule-pict-infos)])
(rule-pict-info-arrow r)
(rule-pict-info-lhs r)
(rule-pict-info-rhs r)
(rule-pict-info-label r)
(rule-pict-info-computed-label r)
(rule-pict-info->side-condition-pict r))
(blank))])
(render-reduction-relation
(reduction-relation
empty-language
(--> (a any) 1 "a")
(--> (b any) 2 b)
(--> (c any) 3 (computed-name (format "c: ~a" (term any))))
(--> (d any) 4)
(--> (e any) 5 (where (1) any))))))
(printf "pict-test.rkt done\n")