diff --git a/collects/redex/main.ss b/collects/redex/main.ss index 1bdf2e876c..228d1030ea 100644 --- a/collects/redex/main.ss +++ b/collects/redex/main.ss @@ -4,4 +4,5 @@ "pict.ss") (provide (all-from-out "reduction-semantics.ss" "gui.ss" - "pict.ss")) \ No newline at end of file + "pict.ss")) +(provide render-language) \ No newline at end of file diff --git a/collects/redex/pict.ss b/collects/redex/pict.ss index 169a02721d..f9dc0ac11b 100644 --- a/collects/redex/pict.ss +++ b/collects/redex/pict.ss @@ -9,31 +9,24 @@ (lib "mrpict.ss" "texpict")) (provide/contract - [reduction-relation->pict - (->* (reduction-relation?) - ((or/c false/c (listof (or/c string? symbol?)))) - pict?)] - [reduction-relation->ps - (->* (reduction-relation? - (or/c string? path?)) - ((or/c false/c (listof (or/c string? symbol?)))) - void?)] - [language->pict - (->* (compiled-lang?) - ((or/c false/c (cons/c symbol? (listof symbol?)))) - pict?)] - [language->ps - (->* (compiled-lang? - (or/c path? string?)) - ((or/c false/c (cons/c symbol? (listof symbol?)))) - void?)] - [extend-language-show-union (parameter/c boolean?)]) + [render-reduction-relation + (case-> (-> reduction-relation? pict?) + (-> reduction-relation? (or/c string? path?) void?))] + [reduction-relation->pict (-> reduction-relation? pict?)] + [render-reduction-relation-rules (parameter/c (or/c false/c (listof (or/c symbol? string?))))] + + [language->pict (-> compiled-lang? pict?)] + [render-language + (case-> (-> compiled-lang? pict?) + (-> compiled-lang? (or/c path? string?) void?))]) ; syntax (provide metafunction->pict - metafunction->ps) + render-metafunction) (provide/contract + [render-language-nts (parameter/c (or/c false/c (listof (or/c string? symbol?))))] + [extend-language-show-union (parameter/c boolean?)] [current-text (parameter/c (-> string? text-style/c number? pict?))]) (provide/contract diff --git a/collects/redex/private/bitmap-test.ss b/collects/redex/private/bitmap-test.ss index 0cfd3c56f7..eb2edaf4a5 100644 --- a/collects/redex/private/bitmap-test.ss +++ b/collects/redex/private/bitmap-test.ss @@ -13,13 +13,13 @@ number) (v number (λ (x) e)) ((x y) variable-not-otherwise-mentioned)) - (test (language->pict lang #f) "language.png") + (test (render-language lang) "language.png") (define-extended-language lang++ lang (e .... number (+ e e)) (v .... number)) - (test (language->pict lang++ #f) "extended-language.png") + (test (render-language lang++) "extended-language.png") (define red (reduction-relation @@ -27,17 +27,17 @@ (--> ((λ (x) e) v) (S x v e)))) ;; tests: reduction-relation - (test (reduction-relation->pict red) + (test (render-reduction-relation red) "reduction-relation.png") - (test (reduction-relation->pict + (test (render-reduction-relation (extend-reduction-relation red lang (--> 1 2))) "extended-reduction-relation.png") (define-metafunction lang [(S x v e) e]) - (test (metafunction->pict S) + (test (render-metafunction S) "metafunction.png") (printf "bitmap-test.ss: ") diff --git a/collects/redex/private/pict-test.ss b/collects/redex/private/pict-test.ss index 2783f97f7a..c4332fd564 100644 --- a/collects/redex/private/pict-test.ss +++ b/collects/redex/private/pict-test.ss @@ -10,32 +10,31 @@ (require (lib "mrpict.ss" "texpict") (lib "mred.ss" "mred") (lib "class.ss")) - (dc-for-text-size (make-object bitmap-dc% (make-object bitmap% 1 1))) (define-language empty-language) (define-language var-ab [var (a b)]) - (language->pict var-ab #f) + (render-language var-ab) (define-language var-not-ab [var (variable-except x y)]) - (language->pict var-not-ab #f) + (render-language var-not-ab) (let () (define-metafunction empty-language [(zero any_in) 0]) - (metafunction->pict zero)) + (render-metafunction zero)) - (reduction-relation->pict + (render-reduction-relation (reduction-relation empty-language (--> number_const ,(term (+ number_const 0))))) - (reduction-relation->pict + (render-reduction-relation (reduction-relation empty-language (--> a b @@ -49,6 +48,6 @@ (define-extended-language x0-10 x1-9 (x 0 .... 10)) - (language->pict x0-10 #f) + (render-language x0-10) (printf "pict-test.ss passed\n")) \ No newline at end of file diff --git a/collects/redex/private/pict.ss b/collects/redex/private/pict.ss index a64c41c045..493e12d5c6 100644 --- a/collects/redex/private/pict.ss +++ b/collects/redex/private/pict.ss @@ -12,11 +12,15 @@ (require (for-syntax scheme/base)) (provide language->pict - language->ps + render-language + render-language-nts + reduction-relation->pict - reduction-relation->ps + render-reduction-relation + render-reduction-relation-rules + metafunction->pict - metafunction->ps + render-metafunction basic-text @@ -43,13 +47,40 @@ extend-language-show-union set-arrow-pict!) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; reduction to pict -;; -(define reduction-relation->pict - (λ (rr [rules #f]) +; +; +; +; ;;;; ; ;; +; ;;;; ;; ;; +; ;;; ;;; ;;; ;;;;;;; ;;;; ;;;; ;;;;; ;;;;; ;;;; ;;;; ;;; +; ;;;;;;; ;;;;; ;;;;;;;; ;;;; ;;;; ;;;;;; ;;;;;; ;;;; ;;;;;; ;;;;;;;;; +; ;;;; ;; ;;;; ;; ;;;;;;;;; ;;;; ;;;; ;;;;;;; ;;;; ;;;; ;;;;;;;; ;;;; ;;;; +; ;;;; ;;;;;;; ;;;; ;;;; ;;;; ;;;; ;;;; ;;;; ;;;; ;;;; ;;; ;;;; ;;;; +; ;;;; ;;;;; ;;;;;;;;; ;;;; ;;;; ;;;;;;; ;;;;; ;;;; ;;;;;;;; ;;;; ;;;; +; ;;;; ;;;;;; ;;;;;;;; ;;;;;;;;; ;;;;;; ;;;;; ;;;; ;;;;;; ;;;; ;;;; +; ;;;; ;;;; ;;;;;;; ;;; ;;;; ;;;;; ;;;; ;;;; ;;;; ;;;; ;;;; +; +; +; +; +; +; +; ;;;; ; ;; +; ;;;; ;; ;; +; ;;; ;;; ;;; ;;;; ;;;;;;; ;;;;; ;;;; ;;;; ;;; +; ;;;;;;; ;;;;; ;;;; ;;;;;;;; ;;;;;; ;;;; ;;;;;; ;;;;;;;;; +; ;;;; ;; ;;;; ;; ;;;; ;;;; ;;;; ;;;; ;;;;;;;; ;;;; ;;;; +; ;;;; ;;;;;;; ;;;; ;;;;;;; ;;;; ;;;; ;;;; ;;; ;;;; ;;;; +; ;;;; ;;;;; ;;;; ;; ;;;; ;;;;; ;;;; ;;;;;;;; ;;;; ;;;; +; ;;;; ;;;;;; ;;;; ;;;;;;;; ;;;;; ;;;; ;;;;;; ;;;; ;;;; +; ;;;; ;;;; ;;;; ;; ;;;; ;;;; ;;;; ;;;; ;;;; ;;;; +; +; +; + +(define (do-reduction-relation->pict what rr) + (let ([rules (render-reduction-relation-rules)]) ((rule-pict-style->proc) (map (rr-lws->trees (language-nts (reduction-relation-lang rr))) (if rules @@ -60,16 +91,24 @@ (map (lambda (label) (hash-ref ht label (lambda () - (error 'reduction-relation->pict + (error what "no rule found for label: ~e" label)))) rules)) (reduction-relation-lws rr)))))) -(define reduction-relation->ps - (λ (rr filename [rules #f]) - (save-as-ps (λ () (reduction-relation->pict rr rules)) - filename))) +(define (reduction-relation->pict rr) (do-reduction-relation->pict 'reduction-relation->pict rr)) + +(define render-reduction-relation-rules (make-parameter #f)) + +(define render-reduction-relation + (case-lambda + [(rr) + (parameterize ([dc-for-text-size (make-object bitmap-dc% (make-object bitmap% 1 1))]) + (do-reduction-relation->pict 'render-reduction-relation rr))] + [(rr filename) + (save-as-ps (λ () (do-reduction-relation->pict 'render-reduction-relation rr)) + filename)])) (define ((rr-lws->trees nts) rp) (let ([tp (λ (x) (lw->pict nts x))]) @@ -330,10 +369,23 @@ [(--<<) (basic-text "\u291b" (default-style))] [else (error 'arrow->pict "unknown arrow ~s" arr)])))) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; language to pict -;; + + +; +; +; +; ;;;; +; ;;;; +; ;;;; ;;;;;;; ;;;; ;;; ;;;;;;; ;;;; ;;;; ;;;;;;; ;;;;;;; ;;; +; ;;;; ;;;;;;;; ;;;;;;;;; ;;;;;;;; ;;;; ;;;; ;;;;;;;; ;;;;;;;; ;;;;; +; ;;;; ;;;; ;;;; ;;;; ;;; ;;;; ;;;; ;;;; ;;;; ;;; ;;;; ;;;; ;; +; ;;;; ;;;;;;; ;;;; ;;;; ;;;;;;;; ;;;; ;;;; ;;;;;;; ;;;;;;;; ;;;;;;; +; ;;;; ;; ;;;; ;;;; ;;;; ;;;;;;; ;;;; ;;;; ;; ;;;; ;;;;;;; ;;;;; +; ;;;; ;;;;;;;; ;;;; ;;;; ; ;;;; ;;;;;;;;; ;;;;;;;; ; ;;;; ;;;;;; +; ;;;; ;; ;;;; ;;;; ;;;; ;;;;;;;; ;;; ;;;; ;; ;;;; ;;;;;;;; ;;;; +; ;;;;;;;; ;;;;;;;; +; ;;;;;; ;;;;;; +; ;; type flattened-language-pict-info = ;; (listof (cons (listof symbol[nt]) (listof loc-wrapper[rhs]))) @@ -341,21 +393,27 @@ ;; (union (vector flattened-language-pict-info language-pict-info) ;; flattened-language-pict-info) -(define (language->ps lang filename [non-terminals #f] #:pict-wrap [pict-wrap (lambda (p) p)]) - (when non-terminals - (check-non-terminals 'language->ps non-terminals lang)) - (save-as-ps (λ () (pict-wrap (language->pict lang non-terminals))) - filename)) +(define render-language + (case-lambda + [(lang) + (parameterize ([dc-for-text-size (make-object bitmap-dc% (make-object bitmap% 1 1))]) + (do-language->pict 'render-language lang))] + [(lang filename) + (save-as-ps (λ () (do-language->pict 'render-language lang)) filename)])) -(define (language->pict lang [non-terminals #f]) - (when non-terminals - (check-non-terminals 'language->pict non-terminals lang)) - (let* ([all-non-terminals (hash-map (compiled-lang-ht lang) (λ (x y) x))] - [non-terminals (or non-terminals all-non-terminals)]) +(define (language->pict lang) (do-language->pict 'language->pict lang)) + +(define (do-language->pict what lang) + (let ([specd-non-terminals (render-language-nts)] + [all-non-terminals (hash-map (compiled-lang-ht lang) (λ (x y) x))]) + (when specd-non-terminals + (check-non-terminals what specd-non-terminals lang)) (make-grammar-pict (compiled-lang-pict-builder lang) - non-terminals + (or specd-non-terminals all-non-terminals) all-non-terminals))) +(define render-language-nts (make-parameter #f)) + (define (check-non-terminals what nts lang) (let ([langs-nts (language-nts lang)]) (for-each @@ -555,10 +613,22 @@ bar (loop snd (cdr rst))))]))) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; metafunction to pict -;; + +; +; +; +; ; ;;; ; ;; +; ;; ;;;; ;; ;; +; ;;;;;;; ;;;; ;;; ;;;;; ;;;;;;; ;;;;; ;;;; ;;;; ;;;; ;;; ;;;;; ;;;;; ;;;; ;;;; ;;; +; ;;;;;;;;;;;;; ;;;;; ;;;;;; ;;;;;;;; ;;;; ;;;; ;;;; ;;;;;;;;; ;;;;;; ;;;;;; ;;;; ;;;;;; ;;;;;;;;; +; ;;;; ;;; ;;;; ;;;; ;; ;;;; ;;;; ;;;;;; ;;;; ;;;; ;;;; ;;;; ;;;;;;; ;;;; ;;;; ;;;;;;;; ;;;; ;;;; +; ;;;; ;;; ;;;; ;;;;;;; ;;;; ;;;;;;; ;;;;;; ;;;; ;;;; ;;;; ;;;; ;;;; ;;;; ;;;; ;;;; ;;; ;;;; ;;;; +; ;;;; ;;; ;;;; ;;;;; ;;;;; ;; ;;;; ;;;; ;;;; ;;;; ;;;; ;;;; ;;;;;;; ;;;;; ;;;; ;;;;;;;; ;;;; ;;;; +; ;;;; ;;; ;;;; ;;;;;; ;;;;; ;;;;;;;; ;;;; ;;;;;;;;; ;;;; ;;;; ;;;;;; ;;;;; ;;;; ;;;;;; ;;;; ;;;; +; ;;;; ;;; ;;;; ;;;; ;;;; ;; ;;;; ;;;; ;;; ;;;; ;;;; ;;;; ;;;;; ;;;; ;;;; ;;;; ;;;; ;;;; +; +; +; (define (make-=) (basic-text " = " (default-style))) @@ -568,11 +638,14 @@ (identifier? #'name) #'(metafunction->pict/proc (metafunction name))])) -(define-syntax (metafunction->ps stx) +(define-syntax (render-metafunction stx) (syntax-case stx () + [(_ name) + (identifier? #'name) + #'(render-metafunction/proc (metafunction name))] [(_ name file) (identifier? #'name) - #'(metafunction->ps/proc (metafunction name) file)])) + #'(render-metafunction/proc (metafunction name) file)])) (define linebreaks (make-parameter #f)) @@ -772,6 +845,12 @@ (basic-text "]" (default-style)))])] [else x])) -(define (metafunction->ps/proc mf filename) - (save-as-ps (λ () (metafunction->pict/proc mf)) - filename)) +(define render-metafunction/proc + (case-lambda + [(mf filename) + (save-as-ps (λ () (metafunction->pict/proc mf)) + filename)] + [(mf) + (parameterize ([dc-for-text-size (make-object bitmap-dc% (make-object bitmap% 1 1))]) + (metafunction->pict/proc mf))])) + diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl index beb8557602..42d8757da8 100644 --- a/collects/redex/redex.scrbl +++ b/collects/redex/redex.scrbl @@ -7,7 +7,7 @@ scheme/gui scheme/pretty scheme/contract - (only-in slideshow/pict text) + (only-in slideshow/pict text dc-for-text-size) redex)) @(define-syntax (defpattech stx) @@ -47,34 +47,6 @@ #'((tech "term") args ...)] [x (identifier? #'x) #'(tech "term")])) -@;{ - -I usually use an `ellipsis' non-terminal to make it more explicit that -the "..." (the only production of `ellipsis') is literal. -- Hide quoted text - - -At Wed, 30 Jul 2008 12:49:43 -0500, "Robby Findler" wrote: -> Also, how have you been notating a literal ellipsis in the docs? That -> is, the "c" below should really be a literal ellipsis (as disctinct -> from a repetition of "b")? - -} - - -@;{ - -I use `defidform'. See `else' for an example. -- Hide quoted text - - -At Wed, 30 Jul 2008 13:03:07 -0500, "Robby Findler" wrote: -> One more question: I export --> and fresh from collects/redex/main.ss -> so that I can signal a syntax error if they are used outside of -> reduction-relation. But this causes scribble to complain when I don't -> document them. Is there a standard way to document them? -> -> Robby -} - @title{@bold{PLT Redex}: an embedded DSL for debugging operational semantics} PLT Redex consists of a domain-specific language for specifying @@ -94,69 +66,6 @@ provides only the non-GUI portions of what is described in this manual (everything except the last two sections), making it suitable for use with @tt{mzscheme} scripts. -@;{ - _reduction-semantics.ss_: the core reduction semantics - library - - _gui.ss_: a _visualization tool for reduction sequences_. - - _pict.ss_: a library for _generating picts and postscript from semantics_ - -In addition, the examples subcollection contains several -small languages to demonstrate various different uses of -this tool: - - _arithmetic.ss_: an arithmetic language with every - possible order of evaluation - - _beginner.ss_: a PLT redex implementation of (much of) the - beginning student teaching language. - - _church.ss_: church numerals with call by name - normal order evaluation - - _combinators.ss_: fills in the gaps in a proof in - Barendregt that i and j (defined in the file) are - a combinator basis - - _compatible-closure.ss_: an example use of compatible - closure. Also, one of the first examples from Matthias - Felleisen and Matthew Flatt's monograph - - _eta.ss_: shows how eta is, in general, unsound. - - _ho-contracts.ss_: computes the mechanical portions of a - proof in the Contracts for Higher Order Functions paper - (ICFP 2002). Contains a sophisticated example use of an - alternative pretty printer. - - iswim.ss : see further below. - - _macro.ss_: models macro expansion as a reduction semantics. - - _letrec.ss_: shows how to model letrec with a store and - some infinite looping terms - - _omega.ss_: the call by value lambda calculus with call/cc. - Includes omega and two call/cc-based infinite loops, one of - which has an ever-expanding term size and one of which has - a bounded term size. - - _semaphores.ss_: a simple threaded language with semaphores - - _subject-reduction.ss_: demos traces/pred that type checks - the term. - - _threads.ss_: shows how non-deterministic choice can be - modeled in a reduction semantics. Contains an example use - of a simple alternative pretty printer. - - _types.ss_: shows how the simply-typed lambda calculus's - type system can be written as a rewritten system (see - Kuan, MacQueen, Findler in ESOP 2007 for more). - -} - @table-of-contents[] @section{Patterns} @@ -1246,26 +1155,98 @@ Be sure to remove the call to dc-for-text-size before you generate .ps files, otherwise the font spacing will be wrong in the .ps file. -@subsection{Pict & PostScript Generators} +@subsection{Picts & PostScript} + +This section documents two classes of operations, one for direct use +of creating postscript figures for use in papers: +@scheme[render-language], +@scheme[render-reduction-relation], and +@scheme[render-metafunction], and one +for use in combination with other libraries that operate on picts +(like @other-manual['scribblings/slideshow]): +@scheme[language->pict], +@scheme[reduction-relation->pict], and +@scheme[metafunction->pict]. +The primary difference between these functions is that the former list +sets @scheme[dc-for-text-size] and the latter does not. + +@defthing[render-language (case-> (-> compiled-lang? + pict?) + (-> compiled-lang? + (or/c string? pict?) + void?))]{ + +This function renders a language. If it receives just a +single argument, it produces a pict and if it receives two +arguments, it saves PostScript in the provided filename. + +That this function calls @scheme[dc-for-text-size] to set +the dc to a relevant dc (either a @scheme[bitmap-dc%] or a +@scheme[ps-dc%] depending if the function is called with one +or two arguments, respectively). + +See @scheme[language->pict] if you are using slideshow or +are otherwise setting @scheme[dc-for-text-size]. } + +@defproc[(language->pict (lang compiled-lang?)) pict?]{ +This function turns a languages into a picts. It is +primarily designed to be used with Slideshow, or with +other tools that combine picts together. It does not +set @scheme[dc-for-text-size]. +} + +@defthing[render-reduction-relation (case-> (-> reduction-relation? + pict?) + (-> reduction-relation? + (or/c string? path?) + pict?))]{ + +If provided with one argument, @scheme[render-reduction-relation] +produces a pict that renders properly in the definitions +window in DrScheme. If given two argument, it writes +postscript into the file named by its second argument. + +This function sets @scheme[dc-for-text-size]. See also +@scheme[reduction-relation->pict]. + +} + +@defproc[(reduction-relation->pict (r reduction-relation?)) pict?]{ + This produces a pict, but without setting @scheme[dc-for-text-size]. + It is suitable for use in Slideshow or other libraries that combine + picts. +} @deftogether[[ -@defproc[(language->pict (lang compiled-lang?) - (nts (or/c false/c (cons/c symbol? (listof symbol?))) #f)) - pict?]{} -@defproc[(language->ps (lang compiled-lang?) - (filename (or/c path? string?)) - (nts (or/c false/c (cons/c symbol? (listof symbol?))) #f)) - void?]{}]]{ +@defform[(render-metafunction metafunction-name)]{} +@defform/none[#:literals (render-metafunction) + (render-metafunction metafunction-name filename)]{}]]{ +If provided with one argument, @scheme[render-metafunction] +produces a pict that renders properly in the definitions +window in DrScheme. If given two argument, it writes +postscript into the file named by @scheme[filename] (which +may be either a string or bytes). -These two functions turn a languages into picts. The first -argument is the language, and the second is a list of -non-terminals that should appear in the pict. It may only -contain symbols that are in the language's set of -non-terminals. +This function sets @scheme[dc-for-text-size]. See also +@scheme[metafunction->pict]. +} -For @scheme[language->ps], the path argument is a filename for the -PostScript file. +@defform[(metafunction->pict metafunction-name)]{ + This produces a pict, but without setting @scheme[dc-for-text-size]. + It is suitable for use in Slideshow or other libraries that combine + picts. +} + +@subsection{Customization} + +@defparam[render-language-nts nts (or/c false/c (listof symbol?))]{ + The value of this parameter controls which non-terminals + @scheme[render-language] and @scheme[language->pict] render. If it + is @scheme[#f] (the default), all non-terminals are rendered. + If it is a list of symbols, only the listed symbols are rendered. + + See also @scheme[language-nts]. } @defparam[extend-language-show-union show? boolean?]{ @@ -1279,38 +1260,15 @@ four-period ellipses, just like in the concrete syntax). Defaultly @scheme[#f]. Note that the #t variant can look a little bit strange if -.... are used and the original version of the language has +@scheme[....] are used and the original version of the language has multi-line right-hand sides. } -@deftogether[[ -@defproc[(reduction-relation->pict - (r reduction-relation?) - (rules (or/c false/c (listof (union string? symbol?))) #f)) - pict?]{} -@defproc[(reduction-relation->ps - (r reduction-relation?) - (file (or/c string? path?)) - (rules (or/c false/c (listof (union string? symbol?))) #f)) - pict?]{}]]{ - -These two functions turn reduction relations into picts. - -The optional lists determine which reduction rules are shown -in the pict. +@defparam[render-reduction-relation-rules rules (or/c false/c (listof (or/c symbol? string?)))]{ + This parameter controls which rules in a reduction relation + will be rendered. } -@deftogether[[ -@defform[(metafunction->pict metafunction-name)]{} -@defform[(metafunction->ps metafunction-name filename)]{}]]{ - -These two syntactic forms turn metafunctions into picts. The second -accepts a string or a path for @scheme[filename] and saves the -PostScript in that file. -} - -@subsection{Customization} - @defparam[rule-pict-style style (symbols 'vertical 'compact-vertical