diff --git a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl index 03dbdc2db2..c082a48956 100644 --- a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl +++ b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl @@ -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 @@ -3165,8 +3165,44 @@ A contract equivalent to 'vertical-overlapping-side-conditions 'horizontal '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]{ diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt index c56c1e4d3c..8d2c93b281 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt @@ -513,24 +513,24 @@ (extract-pattern-binds #'lhs)] [((tl-id . tl-pat) ...) (extract-term-let-binds #'rhs)]) - #`(make-rule-pict 'arrow - #,(to-lw/proc #'lhs) - #,(to-lw/proc #'rhs) - #,label - #,(and computed-label - (to-lw/proc #`,#,computed-label)) - (list scs/withs ... - #,@(map (λ (bind-id bind-pat) - #`(cons #,(to-lw/proc bind-id) - #,(to-lw/proc bind-pat))) - (syntax->list #'(bind-id ...)) - (syntax->list #'(bind-pat ...))) - #,@(map (λ (tl-id tl-pat) - #`(cons #,(to-lw/proc tl-id) - #,(to-lw/uq/proc tl-pat))) - (syntax->list #'(tl-id ...)) - (syntax->list #'(tl-pat ...)))) - (list fvars ...))))] + #`(make-rule-pict-info 'arrow + #,(to-lw/proc #'lhs) + #,(to-lw/proc #'rhs) + #,label + #,(and computed-label + (to-lw/proc #`,#,computed-label)) + (list scs/withs ... + #,@(map (λ (bind-id bind-pat) + #`(cons #,(to-lw/proc bind-id) + #,(to-lw/proc bind-pat))) + (syntax->list #'(bind-id ...)) + (syntax->list #'(bind-pat ...))) + #,@(map (λ (tl-id tl-pat) + #`(cons #,(to-lw/proc tl-id) + #,(to-lw/uq/proc tl-pat))) + (syntax->list #'(tl-id ...)) + (syntax->list #'(tl-pat ...)))) + (list fvars ...))))] ;; just skip over junk here, since syntax error checks elsewhere will catch this [_ #f])) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/struct.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/struct.rkt index b449ab5acb..e7a89e575b 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/struct.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/struct.rkt @@ -14,9 +14,12 @@ empty-reduction-relation make-rewrite-proc rewrite-proc? rewrite-proc-name 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))) ;; a proc is a `cached' version of a make-proc, specialized to a particular language diff --git a/pkgs/redex-pkgs/redex-pict-lib/redex/pict.rkt b/pkgs/redex-pkgs/redex-pict-lib/redex/pict.rkt index be85b227be..7f9a6e21aa 100644 --- a/pkgs/redex-pkgs/redex-pict-lib/redex/pict.rkt +++ b/pkgs/redex-pkgs/redex-pict-lib/redex/pict.rkt @@ -3,6 +3,7 @@ (require racket/contract "private/pict.rkt" "private/core-layout.rkt" + redex/private/struct redex/private/loc-wrapper redex/reduction-semantics texpict/mrpict) @@ -13,7 +14,8 @@ 'vertical-overlapping-side-conditions 'horizontal '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 term->pict/pretty-write @@ -32,7 +34,8 @@ [reduction-relation->pict (->* (reduction-relation?) (#:style reduction-rule-style/c) 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?) (#:nts (or/c false/c (listof (or/c string? symbol?)))) @@ -45,7 +48,15 @@ [result (file) (if (path-string? file) 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 (provide relation->pict diff --git a/pkgs/redex-pkgs/redex-pict-lib/redex/private/pict.rkt b/pkgs/redex-pkgs/redex-pict-lib/redex/private/pict.rkt index 37db7e6bbf..77978c3d46 100644 --- a/pkgs/redex-pkgs/redex-pict-lib/redex/private/pict.rkt +++ b/pkgs/redex-pkgs/redex-pict-lib/redex/private/pict.rkt @@ -84,7 +84,9 @@ set-arrow-pict! arrow->pict horizontal-bar-spacing - relation-clauses-combine) + relation-clauses-combine + + rule-pict-info->side-condition-pict) (provide/contract [linebreaks (parameter/c (or/c #f (listof boolean?)))]) @@ -130,7 +132,7 @@ (for ([rp (in-list (reduction-relation-lws rr))] [i (in-naturals)]) (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) (hash-ref ht (if (string? label) (string->symbol label) @@ -159,25 +161,25 @@ (define ((rr-lws->trees nts) rp) (let ([tp (λ (x) (lw->pict nts x))]) - (make-rule-pict (rule-pict-arrow rp) - (tp (rule-pict-lhs rp)) - (tp (rule-pict-rhs rp)) - (rule-pict-label rp) - (and (rule-pict-computed-label rp) - (let ([rewritten (apply-rewrites (rule-pict-computed-label rp))]) - (and (not (and (rule-pict-label rp) - (let has-unq? ([x rewritten]) - (and (lw? x) - (or (lw-unq? x) - (and (list? (lw-e x)) - (ormap has-unq? (lw-e x)))))))) - (tp rewritten)))) - (map (lambda (v) - (if (pair? v) - (where-pict (tp (car v)) (tp (cdr v))) - (tp v))) - (rule-pict-side-conditions/pattern-binds rp)) - (map tp (rule-pict-fresh-vars rp))))) + (make-rule-pict-info (rule-pict-info-arrow rp) + (tp (rule-pict-info-lhs rp)) + (tp (rule-pict-info-rhs rp)) + (rule-pict-info-label rp) + (and (rule-pict-info-computed-label rp) + (let ([rewritten (apply-rewrites (rule-pict-info-computed-label rp))]) + (and (not (and (rule-pict-info-label rp) + (let has-unq? ([x rewritten]) + (and (lw? x) + (or (lw-unq? x) + (and (list? (lw-e x)) + (ormap has-unq? (lw-e x)))))))) + (tp rewritten)))) + (map (lambda (v) + (if (pair? v) + (where-pict (tp (car v)) (tp (cdr v))) + (tp v))) + (rule-pict-info-side-conditions/pattern-binds rp)) + (map tp (rule-pict-info-fresh-vars rp))))) (define current-label-extra-space (make-parameter 0)) (define reduction-relation-rule-separation (make-parameter 4)) @@ -187,14 +189,14 @@ [max-rhs (apply max 0 (map pict-width - (map rule-pict-rhs rps)))] + (map rule-pict-info-rhs rps)))] [max-w (apply max 0 (map (lambda (rp) (+ sep sep - (pict-width (rule-pict-lhs rp)) - (pict-width (arrow->pict (rule-pict-arrow rp))) - (pict-width (rule-pict-rhs rp)))) + (pict-width (rule-pict-info-lhs rp)) + (pict-width (arrow->pict (rule-pict-info-arrow rp))) + (pict-width (rule-pict-info-rhs rp)))) rps))]) (table 4 (apply @@ -203,23 +205,24 @@ (for/list ([rp (in-list rps)] [i (in-naturals 1)]) (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))] - [lhs (rule-pict-lhs rp)] - [rhs (rule-pict-rhs rp)] + [lhs (rule-pict-info-lhs rp)] + [rhs (rule-pict-info-rhs rp)] [spc (basic-text " " (default-style))] [label (hbl-append (blank (label-space) 0) (rp->pict-label rp))] [sep (blank 4)]) (append (if side-conditions-same-line? (list lhs arrow - (hbl-append rhs - (let ([sc (rp->side-condition-pict rp max-w)]) - (inset sc (min 0 (- max-rhs (pict-width sc))) 0 0 0))) + (hbl-append + rhs + (let ([sc (rule-pict-info->side-condition-pict rp max-w)]) + (inset sc (min 0 (- max-rhs (pict-width sc))) 0 0 0))) label) (list lhs arrow rhs label (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)) (blank))) (if (= len i) @@ -235,16 +238,16 @@ (define ((make-vertical-style side-condition-combiner) rps) (let* ([mk-top-line-spacer (λ (rp) - (hbl-append (rule-pict-lhs rp) + (hbl-append (rule-pict-info-lhs rp) (basic-text " " (default-style)) - (arrow->pict (rule-pict-arrow rp)) + (arrow->pict (rule-pict-info-arrow rp)) (basic-text " " (default-style)) (rp->pict-label rp)))] [mk-bot-line-spacer (λ (rp) (rt-superimpose - (rule-pict-rhs rp) - (rp->side-condition-pict rp +inf.0)))] + (rule-pict-info-rhs rp) + (rule-pict-info->side-condition-pict rp +inf.0)))] [multi-line-spacer (if (null? rps) (blank) @@ -267,14 +270,14 @@ (side-condition-combiner (vl-append (ltl-superimpose - (htl-append (rule-pict-lhs rp) + (htl-append (rule-pict-info-lhs rp) (basic-text " " (default-style)) - (arrow->pict (rule-pict-arrow rp))) + (arrow->pict (rule-pict-info-arrow rp))) (rtl-superimpose spacer (rp->pict-label rp))) - (rule-pict-rhs rp)) - (rp->side-condition-pict rp +inf.0))) + (rule-pict-info-rhs rp)) + (rule-pict-info->side-condition-pict rp +inf.0))) rps) (blank 0 (reduction-relation-rule-separation))))))) @@ -291,10 +294,10 @@ (compact-vertical-min-width) (map pict-width (append - (map rule-pict-lhs rps) - (map rule-pict-rhs rps))))] + (map rule-pict-info-lhs rps) + (map rule-pict-info-rhs rps))))] [scs (map (lambda (rp) - (rp->side-condition-pict rp max-w)) + (rule-pict-info->side-condition-pict rp max-w)) rps)] [labels (map (lambda (rp) (hbl-append (blank (label-space) 0) (rp->pict-label rp))) @@ -308,9 +311,10 @@ [one-line (lambda (sep?) (lambda (rp sc label) - (let ([arrow (hbl-append (arrow->pict (rule-pict-arrow rp)) (blank (arrow-space) 0))] - [lhs (rule-pict-lhs rp)] - [rhs (rule-pict-rhs rp)] + (let ([arrow (hbl-append (arrow->pict (rule-pict-info-arrow rp)) + (blank (arrow-space) 0))] + [lhs (rule-pict-info-lhs rp)] + [rhs (rule-pict-info-rhs rp)] [spc (basic-text " " (default-style))] [sep (blank (compact-vertical-min-width) (reduction-relation-rule-separation))] @@ -392,16 +396,16 @@ (make-parameter (lambda (lhs rhs) (htl-append lhs (make-=) rhs)))) -(define (rp->side-condition-pict rp max-w) - (side-condition-pict (rule-pict-fresh-vars rp) - (rule-pict-side-conditions/pattern-binds rp) +(define (rule-pict-info->side-condition-pict rp [max-w +inf.0]) + (side-condition-pict (rule-pict-info-fresh-vars rp) + (rule-pict-info-side-conditions/pattern-binds rp) max-w)) (define (rp->pict-label rp) - (cond [(rule-pict-computed-label rp) => bracket] - [(rule-pict-label rp) + (cond [(rule-pict-info-computed-label rp) => bracket] + [(rule-pict-info-label rp) (string->bracketed-label - (format "~a" (rule-pict-label rp)))] + (format "~a" (rule-pict-info-label rp)))] [else (blank)])) (define (string->bracketed-label str) @@ -422,18 +426,23 @@ (define (make-horiz-space picts) (blank (pict-width (apply cc-superimpose picts)) 0)) (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) - (case style - [(vertical) rule-picts->pict/vertical] - [(compact-vertical) rule-picts->pict/compact-vertical] - [(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)])) + (cond + [(symbol? style) (hash-ref rule-pict-style-table style)] + [else style])) (define (mk-arrow-pict sz style) (let ([cache (make-hash)]) diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/pict-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/pict-test.rkt index 11c2907945..0367f51e50 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/pict-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/pict-test.rkt @@ -97,4 +97,25 @@ (render-judgment-form deep-empty))) 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")