added unstable/redex with useful typesetting (rewriter) helpers
This commit is contained in:
Ryan Culpepper
parent
516f56fc83
commit
ffa589116f
356
collects/unstable/redex.rkt
Normal file
356
collects/unstable/redex.rkt
Normal file
|
|
@ -0,0 +1,356 @@
|
|||
#lang racket
|
||||
(require racket/contract
|
||||
redex/reduction-semantics
|
||||
redex/pict
|
||||
slideshow/pict
|
||||
racket/list)
|
||||
|
||||
;; TO DO:
|
||||
;; - chained binary operators
|
||||
;; eg (+ 1 2 3) => "1 + 2 + 3"
|
||||
;; - helper for thin spaces around operators/functions ?
|
||||
;; - rewriters for more conventions (eg subst, env, judgments, ...)
|
||||
|
||||
(provide
|
||||
(contract-out
|
||||
;; Using and controlling rewriters
|
||||
[with-rewriters
|
||||
(-> (-> any) any)]
|
||||
[current-atomic-rewriters
|
||||
(parameter/c (plistof symbol? atomic-rewriter/c))]
|
||||
[current-compound-rewriters
|
||||
(parameter/c (plistof symbol? compound-rewriter/c))]
|
||||
[current-unquote-rewriters
|
||||
(parameter/c (plistof (-> lw? any/c) (-> lw? lw?)))]
|
||||
[add-atomic-rewriters!
|
||||
(->* [] [] #:rest (plistof symbol? atomic-rewriter/c)
|
||||
void?)]
|
||||
[add-compound-rewriters!
|
||||
(->* [] [] #:rest (plistof symbol? compound-rewriter/c)
|
||||
void?)]
|
||||
[add-unquote-rewriters!
|
||||
(->* [] [] #:rest (plistof (-> lw? any/c) (-> lw? lw?))
|
||||
void?)]
|
||||
;; Rewriter constructors
|
||||
[only-first-rw
|
||||
(-> compound-rewriter/c)]
|
||||
[binary-rw
|
||||
(->* [content/c]
|
||||
[#:parenthesize-arg (or/c #t #f (listof symbol?) (-> lw? any/c))
|
||||
#:parenthesize-left (or/c #t #f (listof symbol?) (-> lw? any/c))
|
||||
#:parenthesize-right (or/c #t #f (listof symbol?) (-> lw? any/c))]
|
||||
compound-rewriter/c)]
|
||||
[prefix-rw
|
||||
(-> content/c
|
||||
compound-rewriter/c)]
|
||||
[postfix-rw
|
||||
(-> content/c
|
||||
compound-rewriter/c)]
|
||||
[function-rw
|
||||
(-> content/c
|
||||
compound-rewriter/c)]
|
||||
[splice-rw
|
||||
(-> compound-rewriter/c)]
|
||||
[constant-rw
|
||||
(-> content/c
|
||||
compound-rewriter/c)]
|
||||
[bracket-rw
|
||||
(->* [(or/c 'round 'square 'curly 'angle (list/c (or/c string? pict?) (or/c string? pict?)))]
|
||||
[#:comma? any/c]
|
||||
compound-rewriter/c)]
|
||||
[set-cons-rw
|
||||
(-> compound-rewriter/c)]
|
||||
;; Contracts
|
||||
[compound-rewriter/c
|
||||
contract?]
|
||||
[plistof
|
||||
(-> contract? contract? contract?)]
|
||||
#|
|
||||
[content/c
|
||||
contract?]
|
||||
|#))
|
||||
|
||||
(define (plistof key/c val/c)
|
||||
(letrec ([ctc
|
||||
(recursive-contract
|
||||
(or/c '()
|
||||
(cons/c key/c (cons/c val/c ctc))))])
|
||||
ctc))
|
||||
|
||||
(define content/c
|
||||
(or/c string? pict? lw? (-> (or/c string? pict? lw?))))
|
||||
|
||||
(define atomic-rewriter/c
|
||||
(or/c string? pict? (-> (or/c string? pict?))))
|
||||
|
||||
(define compound-rewriter/c
|
||||
(-> (listof lw?)
|
||||
(listof (or/c string? pict? lw?))))
|
||||
|
||||
;; ============================================================
|
||||
|
||||
(define current-atomic-rewriters (make-parameter null))
|
||||
(define current-compound-rewriters (make-parameter null))
|
||||
(define current-unquote-rewriters (make-parameter null))
|
||||
|
||||
(define (add-atomic-rewriters! . args)
|
||||
(push-rewriters! 'add-atomic-rewriters! current-atomic-rewriters args))
|
||||
(define (add-compound-rewriters! . args)
|
||||
(push-rewriters! 'add-compound-rewrites! current-compound-rewriters args))
|
||||
(define (add-unquote-rewriters! . args)
|
||||
(push-rewriters! 'add-unquote-rewrites! current-unquote-rewriters args))
|
||||
|
||||
(define (with-rewriters thunk)
|
||||
(with-atomic-rewriter*
|
||||
(lambda ()
|
||||
(with-compound-rewriter*
|
||||
(lambda ()
|
||||
(with-unquote-rewriter*
|
||||
(lambda ()
|
||||
(thunk))
|
||||
(reverse (current-unquote-rewriters))))
|
||||
(reverse (current-compound-rewriters))))
|
||||
(reverse (current-atomic-rewriters))))
|
||||
|
||||
;; ============================================================
|
||||
|
||||
(define (push-rewriters! who param args)
|
||||
(unless (even? (length args))
|
||||
(error who "expected even number of arguments, got: ~e" args))
|
||||
(param (append args (param))))
|
||||
|
||||
;; Note: l is reversed, so rewriter comes first, symbol/pred comes second.
|
||||
(define (with-atomic-rewriter* thunk l)
|
||||
(if (null? l)
|
||||
(thunk)
|
||||
(with-atomic-rewriter
|
||||
(cadr l)
|
||||
(let ([rw (car l)])
|
||||
(if (string? rw)
|
||||
(lambda () (text rw (default-style) (default-font-size)))
|
||||
rw))
|
||||
(with-atomic-rewriter* thunk (cddr l)))))
|
||||
(define (with-compound-rewriter* thunk l)
|
||||
(if (null? l)
|
||||
(thunk)
|
||||
(with-compound-rewriter
|
||||
(cadr l) (car l)
|
||||
(with-compound-rewriter* thunk (cddr l)))))
|
||||
(define (with-unquote-rewriter* thunk l)
|
||||
(with-unquote-rewriter
|
||||
(lambda (lw)
|
||||
(let loop ([l l])
|
||||
(cond [(null? l)
|
||||
lw]
|
||||
[else
|
||||
(let ([pred (cadr l)]
|
||||
[tx (car l)])
|
||||
(cond [(pred lw) (tx lw)]
|
||||
[else (loop (cddr l))]))])))
|
||||
(thunk)))
|
||||
|
||||
;; ============================================================
|
||||
|
||||
(define (only-first-rw)
|
||||
(compound-rw 'only-first-rw
|
||||
(lambda (lws)
|
||||
(let ([arg-lw (list-ref lws 2)])
|
||||
(list arg-lw)))))
|
||||
|
||||
(define (binary-rw op
|
||||
#:parenthesize-arg [parenthesize-arg #f]
|
||||
#:parenthesize-left [parenthesize-left parenthesize-arg]
|
||||
#:parenthesize-right [parenthesize-right parenthesize-arg])
|
||||
(compound-rw 'binary-rw
|
||||
(lambda (lws)
|
||||
(let ([left (list-ref lws 2)]
|
||||
[right (list-ref lws 3)])
|
||||
;; (list left (just-after op left) (between "" left right) right)
|
||||
;; (list left (just-after op left) "" right)
|
||||
(append (maybe-parenthesize left parenthesize-left)
|
||||
(list (between (->string/pict op) left right))
|
||||
(maybe-parenthesize right parenthesize-right))))
|
||||
2 2))
|
||||
|
||||
(define (prefix-rw pre
|
||||
#:parenthesize-arg [parenthesize-arg #f])
|
||||
(compound-rw 'prefix-rw
|
||||
(lambda (lws)
|
||||
(let ([arg-lw (list-ref lws 2)])
|
||||
(append (list (just-before (->string/pict pre) arg-lw))
|
||||
(maybe-parenthesize arg-lw parenthesize-arg))))
|
||||
1 1))
|
||||
|
||||
(define (postfix-rw post
|
||||
#:parenthesize-arg [parenthesize-arg #f])
|
||||
(compound-rw 'postfix-rw
|
||||
(lambda (lws)
|
||||
(let ([arg-lw (list-ref lws 2)])
|
||||
(append (maybe-parenthesize arg-lw parenthesize-arg)
|
||||
(list (just-after (->string/pict post) arg-lw)))))
|
||||
1 1))
|
||||
|
||||
(define (function-rw name)
|
||||
(compound-rw 'function-rw
|
||||
(lambda (lws)
|
||||
(list* (re-lw (->string/pict name) (list-ref lws 1))
|
||||
(between "(" (list-ref lws 1) (list-ref lws 2))
|
||||
(comma-ize (cddr lws) #t)))))
|
||||
|
||||
(define (bracket-rw brackets #:tall? [tall? #f] #:comma? [comma? #t])
|
||||
(let-values ([(left-bracket right-bracket)
|
||||
(cond [(symbol? brackets)
|
||||
(case brackets
|
||||
((round) (values "(" ")"))
|
||||
((square) (values "[" "]"))
|
||||
((curly) (values "{" "}"))
|
||||
((angle) (values "〈" "〉"))
|
||||
;; FIXME: more
|
||||
(else (error 'bracket-rw "unknown bracket kind: ~e" brackets)))]
|
||||
[(list? brackets)
|
||||
(values (first brackets) (second brackets))])])
|
||||
(compound-rw 'bracket-rw
|
||||
(lambda (lws)
|
||||
(let ([lwA (first lws)]
|
||||
[lwZ (last lws)]
|
||||
[elems (drop-right (drop lws 2) 1)])
|
||||
(append (list (re-lw (if tall? (taller left-bracket) left-bracket) lwA)
|
||||
"")
|
||||
(if comma? (comma-ize elems #f) elems)
|
||||
(list (re-lw (if tall? (taller right-bracket) right-bracket) lwZ))))))))
|
||||
|
||||
(define (splice-rw)
|
||||
(compound-rw 'splice-rw
|
||||
(lambda (lws)
|
||||
(drop-right (drop lws 2) 1))))
|
||||
|
||||
(define (constant-rw s)
|
||||
(compound-rw 'constant-rw
|
||||
(lambda (lws)
|
||||
(list (re-lw s (first lws))))))
|
||||
|
||||
(define (set-cons-rw)
|
||||
(compound-rw 'set-cons-rw
|
||||
(lambda (lws)
|
||||
(list (just-before "{" (list-ref lws 2))
|
||||
(list-ref lws 2)
|
||||
(just-after "}∪" (list-ref lws 2))
|
||||
(between "" (list-ref lws 2) (list-ref lws 3))
|
||||
(list-ref lws 3)))))
|
||||
|
||||
;; ============================================================
|
||||
|
||||
;; Content = (U string symbol pict (listof (U 'spring lw)))
|
||||
|
||||
;; between : Content lw lw -> lw
|
||||
;; Makes an lw with given content and location between given lws.
|
||||
(define (between s a b)
|
||||
(build-lw s
|
||||
(lw-line a)
|
||||
0
|
||||
(+ (lw-column a) (lw-column-span a))
|
||||
(max 0 (- (lw-column b)
|
||||
(+ (lw-column a) (lw-column-span a))))))
|
||||
|
||||
;; re-lw : Content lw -> lw
|
||||
;; Makes an lw with locations of old lw and new content.
|
||||
(define (re-lw new-e lw)
|
||||
(build-lw new-e
|
||||
(lw-line lw) (lw-line-span lw)
|
||||
(lw-column lw) (lw-column-span lw)))
|
||||
|
||||
;; refit : (listof lw) (listof lw) -> (listof lw)
|
||||
;; Add empty lws ("") around new based on locations of old lws (??)
|
||||
;; Soaks up logical space ????
|
||||
(define (refit orig new)
|
||||
(append (list (between "" (just-before "" (car orig)) (car new)))
|
||||
new
|
||||
(list (between "" (just-after "" (last new)) (just-after "" (last orig))))))
|
||||
|
||||
(define (compound-rw who proc [min-args 0] [max-args +inf.0]
|
||||
#:refit? [refit? #t])
|
||||
((if refit? refit-rw values)
|
||||
(lambda (lws)
|
||||
(unless (>= (length lws) 3)
|
||||
(error who "expected list of at least 3 lws, got: ~e" lws))
|
||||
(let ([lwA (first lws)]
|
||||
[lwB (second lws)]
|
||||
[lwZ (last lws)])
|
||||
(unless (member (lw-e lwA) '("(" "[" "{"))
|
||||
(error who "expected first lw to contain open-paren, got: ~e" lwA))
|
||||
(unless (symbol? (lw-e lwB))
|
||||
(error who "expected second lw to contain symbol, got: ~e" lwB))
|
||||
(unless (member (lw-e lwZ) '(")" "]" "}"))
|
||||
(error who "expected last lw to contain close-paren, got: ~e" lwZ))
|
||||
(let ([args (- (length lws) 3)])
|
||||
(unless (<= min-args args max-args)
|
||||
(if (= min-args max-args)
|
||||
(error who "expected ~s argument(s), got ~s: ~e"
|
||||
min-args args lws)
|
||||
(error who "expected between ~s and ~s arguments, got ~s: ~e"
|
||||
min-args max-args args lws))))
|
||||
(proc lws)))))
|
||||
|
||||
(define ((refit-rw proc) lws)
|
||||
(refit lws (proc lws)))
|
||||
|
||||
(define (taller s)
|
||||
(define p
|
||||
(cond [(string? s) (text s (default-style) (default-font-size))]
|
||||
[(pict? s) s]))
|
||||
(define h (pict-height p))
|
||||
(drop-below-ascent (scale (launder p) 1 1.3) (* 0.1 h)))
|
||||
|
||||
(define (comma-ize lws contains-close-paren?)
|
||||
(let loop ([lws lws])
|
||||
(cond [(and contains-close-paren?
|
||||
(or (null? (cdr lws))
|
||||
(null? (cddr lws))))
|
||||
lws]
|
||||
[(and (not contains-close-paren?)
|
||||
(or (null? lws)
|
||||
(null? (cdr lws))))
|
||||
lws]
|
||||
[(positive? (lw-line-span (car lws)))
|
||||
;; a line break?
|
||||
(cons (car lws) (loop (cdr lws)))]
|
||||
[else (list*
|
||||
(car lws)
|
||||
(between ", " (car lws) (cadr lws))
|
||||
(loop (cdr lws)))])))
|
||||
|
||||
;; ->string/pict : (U string pict (-> (U string pict)) -> (U string pict)
|
||||
(define (->string/pict c)
|
||||
(cond [(pict? c) c]
|
||||
[(string? c) c] ;; ((current-text) c (default-style) (default-font-size))
|
||||
[else (c)]))
|
||||
|
||||
;; maybe-parenthesize : lw _ -> (nonempty-listof lw)
|
||||
(define (maybe-parenthesize arg paren-spec)
|
||||
(if (parenthesize? arg paren-spec)
|
||||
(parenthesize-lws (list arg))
|
||||
(list arg)))
|
||||
|
||||
;; parenthesize? : lw (U #t #f (listof symbol) (-> lw boolean)) -> boolean
|
||||
(define (parenthesize? arg parenthesize-arg)
|
||||
(cond [(boolean? parenthesize-arg) parenthesize-arg]
|
||||
[(list? parenthesize-arg)
|
||||
(let ([contents (lw-e arg)])
|
||||
(and (not (lw-unq? arg))
|
||||
(not (lw-metafunction? arg))
|
||||
(list? contents)
|
||||
(>= (length contents) 3)
|
||||
(member (lw-e (first contents)) '("(" "[" "{"))
|
||||
(member (lw-e (last contents)) '(")" "]" "}"))
|
||||
(member (lw-e (second contents)) parenthesize-arg)
|
||||
#t))]
|
||||
[(procedure? parenthesize-arg)
|
||||
(parenthesize-arg arg)]))
|
||||
|
||||
;; parenthesize-lws : (nonempty-listof lw) -> (nonempty-listof lw)
|
||||
(define (parenthesize-lws lws)
|
||||
(let ([lwA (first lws)]
|
||||
[lwZ (last lws)])
|
||||
(append (list (just-before "(" lwA))
|
||||
lws
|
||||
(list (just-after ")" lwZ)))))
|
||||
343
collects/unstable/scribblings/redex.scrbl
Normal file
343
collects/unstable/scribblings/redex.scrbl
Normal file
|
|
@ -0,0 +1,343 @@
|
|||
#lang scribble/manual
|
||||
@(require racket/stxparam scribble/base scribble/eval "utils.rkt"
|
||||
(for-syntax racket/base syntax/srcloc)
|
||||
(for-label racket/base racket/contract slideshow/pict redex unstable/redex))
|
||||
|
||||
@(define the-eval (make-base-eval))
|
||||
@(the-eval '(require redex/reduction-semantics redex/pict unstable/redex slideshow/pict))
|
||||
|
||||
@title[#:tag "redex"]{Redex}
|
||||
@unstable-header[]
|
||||
|
||||
@defmodule[unstable/redex]
|
||||
|
||||
This library provides functions to help typesetting for
|
||||
@racketmodname[redex] models. The following example program provides
|
||||
an overview of the features:
|
||||
|
||||
@with-eval-preserve-source-locations[
|
||||
@interaction[#:eval the-eval
|
||||
(define-language ZF
|
||||
[e empty
|
||||
(Set e)
|
||||
(Union e_1 e_2)
|
||||
(Powerset e)
|
||||
ZZ
|
||||
variable-not-otherwise-mentioned]
|
||||
[formula (same? e_1 e_2)
|
||||
(in? e_1 e_2)
|
||||
true
|
||||
false
|
||||
(implies formula_1 formula_2)])
|
||||
]]
|
||||
|
||||
By default, Redex models are typeset as S-expressions with some basic
|
||||
styling that distinguishes literals from nonterminal names, handles
|
||||
subscripting, etc.
|
||||
|
||||
@with-eval-preserve-source-locations[
|
||||
@interaction[#:eval the-eval
|
||||
(language->pict ZF)
|
||||
(term->pict ZF (in? x (Set 1 2 3 ...)))
|
||||
]]
|
||||
|
||||
This library provides helper functions for creating and using
|
||||
rewriters that transform the S-expression model terms into other
|
||||
notations.
|
||||
|
||||
@with-eval-preserve-source-locations[
|
||||
@interaction[#:eval the-eval
|
||||
(add-atomic-rewriters!
|
||||
'empty "∅"
|
||||
'formula "φ"
|
||||
'ZZ "\u2124"
|
||||
'variable-not-otherwise-mentioned
|
||||
(lambda () (text "x, y, z, ..." (literal-style) (default-font-size)))
|
||||
'true (lambda () (text "true" '(caps . modern) (default-font-size)))
|
||||
'false (lambda () (text "false" '(caps . modern) (default-font-size))))
|
||||
(add-compound-rewriters!
|
||||
'same? (binary-rw " = ")
|
||||
'in? (binary-rw " ∈ ")
|
||||
'Set (bracket-rw 'curly)
|
||||
'Powerset (function-rw "𝒫 ")
|
||||
'Union (binary-rw "∪")
|
||||
'implies (binary-rw " ⇒ " #:parenthesize-left '(implies)))
|
||||
(with-rewriters
|
||||
(lambda ()
|
||||
(language->pict ZF)))
|
||||
(with-rewriters
|
||||
(lambda ()
|
||||
(render-term ZF (in? x (Set 1 2 3 ...)))))
|
||||
]]
|
||||
|
||||
@; ----------------------------------------
|
||||
|
||||
@defproc[(with-rewriters [proc (-> any)])
|
||||
any]{
|
||||
|
||||
Calls @racket[proc] with the rewriters of
|
||||
@racket[current-atomic-rewriters], @racket[current-compound-rewriters],
|
||||
and @racket[current-unquote-rewriters].
|
||||
}
|
||||
|
||||
@defparam[current-atomic-rewriters rewriters
|
||||
(let ([atomic-rewriter/c
|
||||
(or/c string? pict?
|
||||
(-> (or/c string? pict?)))])
|
||||
(plistof symbol? atomic-rewriter/c))]{
|
||||
|
||||
Parameter of atomic rewriters (as in @racket[with-atomic-rewriter])
|
||||
used by @racket[with-rewriters].
|
||||
}
|
||||
|
||||
@defparam[current-compound-rewriters rewriters
|
||||
(plistof symbol? compound-rewriter/c)]{
|
||||
|
||||
Parameter of compound rewriters (as in
|
||||
@racket[with-compound-rewriter]) used by @racket[with-rewriters].
|
||||
}
|
||||
|
||||
@defparam[current-unquote-rewriters rewriters
|
||||
(plistof (-> lw? any/c) (-> lw? lw?))]{
|
||||
|
||||
Parameter of unquote rewriters (as in @racket[with-unquote-rewriter])
|
||||
used by @racket[with-rewriters].
|
||||
}
|
||||
|
||||
@deftogether[[
|
||||
@defproc[(add-atomic-rewriters! [rewriters
|
||||
(let ([atomic-rewriter/c
|
||||
(or/c string? pict?
|
||||
(-> (or/c string? pict?)))])
|
||||
(plistof symbol? atomic-rewriter/c))])
|
||||
void?]
|
||||
@defproc[(add-compound-rewriters! [rewriters
|
||||
(plistof symbol? compound-rewriter/c)])
|
||||
void?]
|
||||
@defproc[(add-unquote-rewriters! [rewriters
|
||||
(plistof (-> lw? any/c) (-> lw? lw?))])
|
||||
void?]]]{
|
||||
|
||||
Add rewriters to the @racket[current-atomic-rewriters],
|
||||
@racket[current-compound-rewriters], or
|
||||
@racket[current-unquote-rewriters], respectively.
|
||||
}
|
||||
|
||||
@defproc[(plistof [key/c contract?] [value/c contract?])
|
||||
contract?]{
|
||||
|
||||
Contract for even-length lists of alternating @racket[key/c] and
|
||||
@racket[value/c] values.
|
||||
|
||||
Equivalent to
|
||||
@racketblock[
|
||||
(letrec ([ctc
|
||||
(recursive-contract
|
||||
(or/c '()
|
||||
(cons/c key/c (cons/c value/c ctc))))])
|
||||
ctc)
|
||||
]
|
||||
}
|
||||
|
||||
@defthing[compound-rewriter/c contract?]{
|
||||
|
||||
Contract for compound rewriters, which take a list of @racket[lw]
|
||||
structs and returns a list of @racket[lw]s, @racket[pict]s, or
|
||||
strings.
|
||||
|
||||
Equivalent to
|
||||
@racketblock[
|
||||
(-> (listof lw?)
|
||||
(listof (or/c lw? pict? string?)))
|
||||
]
|
||||
}
|
||||
|
||||
@defproc[(binary-rw [operator (or/c string? pict? (-> (or/c string? pict?)))]
|
||||
[#:parenthesize-arg parenthesize-arg
|
||||
(or/c #t #f (listof symbol?) (-> lw? any/c))
|
||||
#f]
|
||||
[#:parenthesize-left parenthesize-left
|
||||
(or/c #t #f (listof symbol?) (-> lw? any/c))
|
||||
parenthesize-arg]
|
||||
[#:parenthesize-right parenthesize-right
|
||||
(or/c #t #f (listof symbol?) (-> lw? any/c))
|
||||
parenthesize-arg])
|
||||
compound-rewriter/c]{
|
||||
|
||||
Typesets @racket[(_sym _term1 _term2)] using @racket[operator] as a
|
||||
binary operator between @racket[_term1] and @racket[_term2].
|
||||
|
||||
@with-eval-preserve-source-locations[
|
||||
@examples[#:eval the-eval
|
||||
(add-compound-rewriters!
|
||||
'plus (binary-rw " + "))
|
||||
(with-rewriters
|
||||
(lambda ()
|
||||
(term->pict ZF (plus 1 2))))
|
||||
]]
|
||||
|
||||
Redex terms may become ambiguous when typeset. To avoid ambiguity, use
|
||||
@racket[#:parenthesize-arg] to direct when arguments should be
|
||||
parenthesized. If @racket[parenthesize-arg] is @racket[#t], then
|
||||
arguments are always parenthesized; if it is @racket[#f], never; if it
|
||||
is a list of symbols, then an argument is parenthesized only if the
|
||||
argument is a term starting with a symbol in the list; if it is a
|
||||
procedure, then the argument is parenthesized if the procedure applied
|
||||
to the argument's @racket[lw] struct returns a true value.
|
||||
|
||||
@with-eval-preserve-source-locations[
|
||||
@interaction[#:eval the-eval
|
||||
(add-compound-rewriters!
|
||||
'times (binary-rw " × "))
|
||||
(with-rewriters
|
||||
(lambda ()
|
||||
(term->pict ZF (times (plus 1 2) 3))))
|
||||
(add-compound-rewriters!
|
||||
'times (binary-rw " × " #:parenthesize-arg '(plus)))
|
||||
(with-rewriters
|
||||
(lambda ()
|
||||
(term->pict ZF (times (plus 1 2) 3))))
|
||||
]]
|
||||
|
||||
The parenthesization rules for left and right arguments can be
|
||||
supplied separately through @racket[#:parenthesize-left] and
|
||||
@racket[#:parenthesize-right], for example to create left-associated
|
||||
or right-associated operators:
|
||||
|
||||
@with-eval-preserve-source-locations[
|
||||
@interaction[#:eval the-eval
|
||||
(add-compound-rewriters!
|
||||
'arrow (binary-rw " → " #:parenthesize-left '(arrow)))
|
||||
(with-rewriters
|
||||
(lambda ()
|
||||
(term->pict ZF (arrow (arrow A B) (arrow C D)))))
|
||||
]]
|
||||
}
|
||||
|
||||
@defproc[(prefix-rw [prefix (or/c string? pict? (-> (or/c string? pict?)))]
|
||||
[#:parenthesize-arg parenthesize-arg
|
||||
(or/c #f #t (listof symbol?) (-> lw? any/c))
|
||||
#f])
|
||||
compound-rewriter/c]{
|
||||
|
||||
Typesets @racket[(_sym _term)] by placing @racket[prefix] before
|
||||
@racket[_term].
|
||||
|
||||
@with-eval-preserve-source-locations[
|
||||
@examples[#:eval the-eval
|
||||
(add-compound-rewriters!
|
||||
'not (prefix-rw "¬ "))
|
||||
(with-rewriters
|
||||
(lambda ()
|
||||
(term->pict ZF (not (in? x empty)))))
|
||||
]]
|
||||
}
|
||||
|
||||
@defproc[(postfix-rw [postfix (or/c string? pict? (-> (or/c string? pict?)))]
|
||||
[#:parenthesize-arg parenthesize-arg
|
||||
(or/c #f #t (listof symbol?) (-> lw? any/c))
|
||||
#f])
|
||||
compound-rewriter/c]{
|
||||
|
||||
Typesets @racket[(_sym _term)] by placing @racket[postfix] after
|
||||
@racket[_term].
|
||||
|
||||
@with-eval-preserve-source-locations[
|
||||
@examples[#:eval the-eval
|
||||
(add-compound-rewriters!
|
||||
'nonempty (postfix-rw " is nonempty"))
|
||||
(with-rewriters
|
||||
(lambda ()
|
||||
(term->pict ZF (nonempty (Set x)))))
|
||||
]]
|
||||
}
|
||||
|
||||
@defproc[(function-rw [function (or/c string? pict? (-> (or/c string? pict?)))])
|
||||
compound-rewriter/c]{
|
||||
|
||||
Typesets @racket[(_sym _term ...)] by placing @racket[function] before
|
||||
the parenthesized, comma-separated list of @racket[_term]s.
|
||||
|
||||
@with-eval-preserve-source-locations[
|
||||
@examples[#:eval the-eval
|
||||
(add-compound-rewriters!
|
||||
'f (function-rw "f")
|
||||
'max (function-rw (text "max" '(bold . modern) (default-font-size))))
|
||||
(with-rewriters
|
||||
(lambda ()
|
||||
(term->pict ZF (max 1 2 (f 3)))))
|
||||
]]
|
||||
}
|
||||
|
||||
@defproc[(only-first-rw)
|
||||
compound-rewriter/c]{
|
||||
|
||||
Typesets @racket[(_sym _term1 _term2 ...)] as @racket[_term1]. Useful
|
||||
for hiding parameters that are necessary for defining the semantics
|
||||
but can be glossed over in its explanation, such as state parameters
|
||||
used for generating unique names.
|
||||
|
||||
@with-eval-preserve-source-locations[
|
||||
@examples[#:eval the-eval
|
||||
(add-compound-rewriters!
|
||||
'First (only-first-rw))
|
||||
(with-rewriters
|
||||
(lambda ()
|
||||
(term->pict ZF [First (in? x y) counter])))
|
||||
]]
|
||||
}
|
||||
|
||||
@defproc[(splice-rw)
|
||||
compound-rewriter/c]{
|
||||
|
||||
Typesets @racket[(_sym _term ...)] by rendering the @racket[_term]s
|
||||
side-by-side.
|
||||
}
|
||||
|
||||
@defproc[(constant-rw [constant (or/c string? pict? (-> (or/c string? pict?)))])
|
||||
compound-rewriter/c]{
|
||||
|
||||
Typesets @racket[(_sym _term ...)] as @racket[constant].
|
||||
}
|
||||
|
||||
@defproc[(bracket-rw [brackets (or/c 'round 'square 'curly 'angle
|
||||
(list (or/c string? pict?)
|
||||
(or/c string? pict?)))]
|
||||
[#:comma? comma? any/c #t])
|
||||
compound-rewriter/c]{
|
||||
|
||||
Typesets @racket[(_sym _term ...)] by surrounding the comma-separated
|
||||
(or space-separated, if @racket[comma?] is false) sequence of
|
||||
@racket[_term]s with brackets. If @racket[brackets] is a list, the
|
||||
first element is the left bracket and the second is the right bracket;
|
||||
@racket['round] is equivalent to @racket['("(" ")")]; @racket['square]
|
||||
is equivalent to @racket['("[" "]")]; @racket['curly] is equivalent to
|
||||
@racket['("{" "}")]; and @racket['angle] is equivalent to
|
||||
@racket['("〈" "〉")].
|
||||
|
||||
@with-eval-preserve-source-locations[
|
||||
@examples[#:eval the-eval
|
||||
(add-compound-rewriters!
|
||||
'Tuple (bracket-rw 'angle))
|
||||
(with-rewriters
|
||||
(lambda ()
|
||||
(term->pict ZF (Tuple 1 2 3))))
|
||||
]]
|
||||
}
|
||||
|
||||
@defproc[(set-cons-rw)
|
||||
compound-rewriter/c]{
|
||||
|
||||
Rewriter that typesets @racket[(_sym _elem-term _set-term)] as the
|
||||
union of the singleton set containing @racket[_elem-term] with the set
|
||||
@racket[_set-term].
|
||||
|
||||
@with-eval-preserve-source-locations[
|
||||
@examples[#:eval the-eval
|
||||
(add-compound-rewriters!
|
||||
'set-cons (set-cons-rw))
|
||||
(with-rewriters
|
||||
(lambda ()
|
||||
(term->pict ZF (set-cons x S))))
|
||||
]]
|
||||
}
|
||||
|
|
@ -99,6 +99,7 @@ Keep documentation and tests up to date.
|
|||
@include-section["parameter-group.scrbl"]
|
||||
@include-section["pretty.scrbl"]
|
||||
@include-section["recontract.scrbl"]
|
||||
@include-section["redex.scrbl"]
|
||||
@include-section["sandbox.scrbl"]
|
||||
@include-section["sequence.scrbl"]
|
||||
@include-section["string.scrbl"]
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user