simplified typesetting interface somewhat

svn: r11159
This commit is contained in:
Robby Findler 2008-08-09 04:14:37 +00:00
parent 15e0bbcff8
commit 4c567d72a0
6 changed files with 235 additions and 205 deletions

View File

@ -4,4 +4,5 @@
"pict.ss")
(provide (all-from-out "reduction-semantics.ss"
"gui.ss"
"pict.ss"))
"pict.ss"))
(provide render-language)

View File

@ -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

View File

@ -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: ")

View File

@ -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"))

View File

@ -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))]))

View File

@ -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