racket-doc 6.7-3 / usr / share / doc / racket / redex / blueboxes.rktd

14670
((3) 0 () 11 ((q lib "redex/pict.rkt") (q lib "redex/reduction-semantics.rkt") (q lib "redex/benchmark.rkt") (q 39775 . 20) (q lib "redex/gui.rkt") (q 10895 . 6) (q 16495 . 5) (q 16360 . 5) (q 41947 . 5) (q 42447 . 3) (q 1582 . 5)) () (h ! (equal) ((c def c (c (? . 0) q metafunction-combine-contract-and-rules)) q (38385 . 5)) ((c form c (c (? . 1) q judgment-holds)) q (10741 . 5)) ((c def c (c (? . 2) q bmark-log-directory)) q (42616 . 6)) ((c form c (c (? . 0) q with-compound-rewriters)) q (39653 . 3)) ((c form c (c (? . 1) q hole)) q (2029 . 2)) ((c def c (c (? . 4) q derivation/ps)) q (24160 . 13)) ((c def c (c (? . 1) q variable-not-in)) q (2658 . 4)) ((c form c (c (? . 1) q context-closure)) q (6563 . 2)) ((c form c (c (? . 1) q extend-reduction-relation)) q (6219 . 2)) ((c form c (c (? . 0) q term->pict)) q (27606 . 2)) ((c def c (c (? . 0) q make-lw)) c (? . 3)) ((c def c (c (? . 1) q make-derivation)) c (? . 5)) ((c form c (c (? . 2) q define-rewrite)) q (41271 . 6)) ((c def c (c (? . 1) q exn:fail:redex?)) q (2857 . 3)) ((c def c (c (? . 0) q homemade-white-square-bracket)) q (33472 . 3)) ((c def c (c (? . 2) q bmark-log-data-data)) c (? . 9)) ((c def c (c (? . 1) q variables-not-in)) q (2749 . 4)) ((c def c (c (? . 2) q run-results?)) c (? . 8)) ((c form c (c (? . 1) q in-domain?)) q (9103 . 2)) ((c def c (c (? . 1) q alpha-equivalent?)) q (4589 . 5)) ((c def c (c (? . 1) q struct:counterexample)) c (? . 7)) ((c def c (c (? . 1) q apply-reduction-relation/tag-with-names)) q (6825 . 6)) ((c def c (c (? . 0) q non-terminal-gap-space)) q (30225 . 4)) ((c form c (c (? . 2) q define-rewrite/compose)) q (41426 . 2)) ((c form c (c (? . 1) q redex-generator)) q (16150 . 7)) ((c form c (c (? . 1) q redex-check)) q (14886 . 29)) ((c def c (c (? . 0) q set-lw-column-span!)) c (? . 3)) ((c def c (c (? . 0) q rule-pict-style)) q (31112 . 4)) ((c def c (c (? . 2) q run-gen-and-check/mods)) q (42086 . 9)) ((c def c (c (? . 4) q stepper/seed)) q (23261 . 7)) ((c def c (c (? . 0) q paren-style)) q (35154 . 4)) ((c def c (c (? . 1) q match-bindings)) q (1514 . 3)) ((c def c (c (? . 4) q initial-font-size)) q (26005 . 4)) ((c def c (c (? . 0) q rule-pict-info-computed-label)) q (31753 . 4)) ((c form c (c (? . 1) q compatible-closure)) q (6495 . 2)) ((c def c (c (? . 1) q exn:fail:redex:test)) c (? . 6)) ((c form c (c (? . 0) q render-term)) q (27541 . 3)) ((c def c (c (? . 0) q metafunction-pict-style)) q (32305 . 17)) ((c def c (c (? . 4) q term-node-set-color!)) q (25034 . 4)) ((c form c (c (? . 1) q test-->>∃)) q (12341 . 10)) ((c def c (c (? . 0) q set-arrow-pict!)) q (37370 . 4)) ((c form c (c (? . 1) q test-->>E)) q (12650 . 2)) ((c def c (c (? . 1) q coverage?)) q (13013 . 3)) ((c def c (c (? . 0) q render-language)) q (28274 . 6)) ((c form c (c (? . 1) q generate-term)) q (13299 . 35)) ((c def c (c (? . 0) q current-text)) q (37143 . 4)) ((c def c (c (? . 4) q term-node-y)) q (25642 . 3)) ((c def c (c (? . 0) q to-lw/stx)) q (40749 . 3)) ((c form c (c (? . 1) q with)) q (7730 . 2)) ((c def c (c (? . 1) q default-check-attempts)) q (17797 . 4)) ((c def c (c (? . 0) q where-combine)) q (38938 . 4)) ((c form c (c (? . 1) q redex-let*)) q (2330 . 2)) ((c def c (c (? . 0) q judgment-form-cases)) q (34386 . 11)) ((c form c (c (? . 1) q make-coverage)) q (12926 . 5)) ((c def c (c (? . 0) q horizontal-bar-spacing)) q (37699 . 5)) ((c def c (c (? . 0) q default-style)) q (35864 . 4)) ((c def c (c (? . 1) q exn:fail:redex:generation-failure?)) q (18103 . 3)) ((c form c (c (? . 0) q with-compound-rewriter)) q (39496 . 4)) ((c def c (c (? . 1) q set-cache-size!)) q (1798 . 3)) ((c def c (c (? . 1) q compiled-lang?)) q (4382 . 3)) ((c form c (c (? . 1) q define-term)) q (2402 . 2)) ((c def c (c (? . 1) q reduction-relation?)) q (6623 . 3)) ((c form c (c (? . 1) q ::=)) q (3706 . 2)) ((c form c (c (? . 1) q -->)) q (7706 . 2)) ((c def c (c (? . 1) q judgment-form?)) q (11390 . 3)) ((c def c (c (? . 0) q default-font-size)) q (36364 . 4)) ((c def c (c (? . 1) q derivation)) c (? . 5)) ((c def c (c (? . 1) q bind-name)) c (? . 10)) ((c def c (c (? . 0) q set-lw-metafunction?!)) c (? . 3)) ((c def c (c (? . 0) q reduction-relation-rule-line-separation)) q (36858 . 5)) ((c def c (c (? . 0) q label-space)) q (32196 . 4)) ((c form c (c (? . 1) q test-predicate)) q (12728 . 2)) ((c def c (c (? . 0) q rule-pict-info-label)) q (31640 . 3)) ((c def c (c (? . 4) q light-brush-color)) q (26742 . 4)) ((c def c (c (? . 1) q apply-reduction-relation)) q (6688 . 4)) ((c def c (c (? . 4) q term-node-height)) q (25768 . 3)) ((c form c (c (? . 1) q nothing)) q (3731 . 2)) ((c def c (c (? . 0) q metafunction-rule-gap-space)) q (37998 . 4)) ((c form c (c (? . 0) q metafunctions->pict)) q (29727 . 2)) ((c form c (c (? . 1) q define-extended-judgment-form)) q (10609 . 6)) ((c def c (c (? . 0) q lw-column-span)) c (? . 3)) ((c def c (c (? . 0) q lw-metafunction?)) c (? . 3)) ((c def c (c (? . 1) q check-redundancy)) q (1874 . 4)) ((c def c (c (? . 4) q light-pen-color)) q (26585 . 4)) ((c def c (c (? . 1) q make-exn:fail:redex:test)) c (? . 6)) ((c def c (c (? . 1) q reduction-relation->rule-names)) q (6396 . 3)) ((c def c (c (? . 1) q derivation-name)) c (? . 5)) ((c def c (c (? . 0) q just-before)) q (41062 . 4)) ((c def c (c (? . 0) q render-language-nts)) q (30068 . 4)) ((c def c (c (? . 0) q lw->pict)) q (40934 . 4)) ((c def c (c (? . 0) q render-term/pretty-write)) q (27638 . 9)) ((c form c (c (? . 1) q build-derivations)) q (10858 . 2)) ((c def c (c (? . 1) q redex-pseudo-random-generator)) q (17934 . 4)) ((c form c (c (? . 1) q redex-match?)) q (1386 . 3)) ((c def c (c (? . 4) q dark-text-color)) q (26903 . 4)) ((c form c (c (? . 0) q render-relation)) q (29780 . 2)) ((c def c (c (? . 0) q delimit-ellipsis-arguments?)) q (33170 . 4)) ((c def c (c (? . 0) q metafunction-up/down-indent)) q (33041 . 4)) ((c def c (c (? . 1) q counterexample?)) c (? . 7)) ((c def c (c (? . 0) q term->pict/pretty-write)) q (27952 . 9)) ((q def ((lib "redex/benchmark/models/all-info.rkt") all-mods)) q (42853 . 3)) ((c def c (c (? . 0) q set-lw-e!)) c (? . 3)) ((c form c (c (? . 1) q term)) q (1979 . 3)) ((c def c (c (? . 0) q lw-unq?)) c (? . 3)) ((c form c (c (? . 1) q redex-match)) q (1310 . 3)) ((c form c (c (? . 1) q term-let)) q (2056 . 8)) ((c def c (c (? . 4) q traces/ps)) q (20557 . 45)) ((c form c (c (? . 1) q O)) q (11087 . 2)) ((c def c (c (? . 0) q build-lw)) q (40360 . 10)) ((c form c (c (? . 0) q relation->pict)) q (29980 . 2)) ((c def c (c (? . 4) q traces)) q (18183 . 45)) ((c def c (c (? . 2) q struct:run-results)) c (? . 8)) ((c def c (c (? . 0) q where-make-prefix-pict)) q (38775 . 4)) ((c def c (c (? . 0) q struct:lw)) c (? . 3)) ((c def c (c (? . 0) q extend-language-show-union)) q (30342 . 4)) ((c form c (c (? . 1) q define-union-language)) q (4171 . 5)) ((c def c (c (? . 0) q metafunction-cases)) q (33774 . 11)) ((c def c (c (? . 4) q term-node-set-position!)) q (25430 . 5)) ((c def c (c (? . 2) q run-results-tries)) c (? . 8)) ((c form c (c (? . 1) q test-equal)) q (11716 . 7)) ((c form c (c (? . 0) q with-atomic-rewriter)) q (39323 . 4)) ((c def c (c (? . 1) q match?)) q (1458 . 3)) ((c def c (c (? . 0) q white-square-bracket)) q (33295 . 4)) ((c form c (c (? . 1) q define-relation)) q (11096 . 10)) ((c def c (c (? . 0) q lw-line-span)) c (? . 3)) ((c form c (c (? . 1) q define-extended-language)) q (3746 . 11)) ((c def c (c (? . 4) q stepper)) q (22982 . 7)) ((c def c (c (? . 1) q union-reduction-relations)) q (6295 . 3)) ((c def c (c (? . 4) q term-node-children)) q (24774 . 3)) ((c form c (c (? . 0) q judgment-form->pict)) q (30019 . 2)) ((c def c (c (? . 0) q literal-style)) q (35255 . 4)) ((c def c (c (? . 0) q grammar-style)) q (35049 . 4)) ((c def c (c (? . 0) q reduction-relation-rule-extra-separation)) q (36686 . 5)) ((c def c (c (? . 1) q apply-reduction-relation*)) q (7056 . 12)) ((c def c (c (? . 0) q set-lw-line!)) c (? . 3)) ((c def c (c (? . 0) q reduction-rule-style/c)) q (31241 . 2)) ((c def c (c (? . 0) q reduction-relation->pict)) q (29044 . 4)) ((c form c (c (? . 1) q test-->)) q (12116 . 9)) ((c form c (c (? . 1) q substitute)) q (4713 . 2)) ((c def c (c (? . 2) q struct:bmark-log-data)) c (? . 9)) ((c def c (c (? . 1) q plug)) q (2564 . 4)) ((c form c (c (? . 1) q reduction-relation)) q (4762 . 39)) ((c def c (c (? . 0) q rule-pict-info->side-condition-pict)) q (31874 . 5)) ((c def c (c (? . 0) q lw-line)) c (? . 3)) ((c def c (c (? . 1) q default-equiv)) q (12795 . 4)) ((c form c (c (? . 1) q define-metafunction/extension)) q (8961 . 5)) ((c def c (c (? . 0) q linebreaks)) q (33637 . 4)) ((c def c (c (? . 1) q struct:exn:fail:redex:test)) c (? . 6)) ((c def c (c (? . 4) q term-node-x)) q (25581 . 3)) ((c form c (c (? . 0) q with-unquote-rewriter)) q (39274 . 2)) ((c def c (c (? . 0) q default-white-square-bracket)) q (33555 . 3)) ((c def c (c (? . 0) q render-lw)) q (40805 . 4)) ((c def c (c (? . 1) q derivation?)) c (? . 5)) ((c def c (c (? . 0) q set-lw-unq?!)) c (? . 3)) ((c def c (c (? . 0) q just-after)) q (41167 . 4)) ((c def c (c (? . 4) q light-text-color)) q (27060 . 4)) ((c def c (c (? . 4) q pretty-print-parameters)) q (27219 . 4)) ((c form c (c (? . 1) q term-match/single)) q (2499 . 2)) ((c def c (c (? . 1) q make-bind)) c (? . 10)) ((c def c (c (? . 0) q label-style)) q (34948 . 4)) ((c def c (c (? . 2) q run-results-cexps)) c (? . 8)) ((c form c (c (? . 2) q include/rewrite)) q (41474 . 2)) ((c def c (c (? . 0) q lw?)) c (? . 3)) ((c form c (c (? . 1) q shadow)) q (3717 . 2)) ((c def c (c (? . 1) q bind)) c (? . 10)) ((c def c (c (? . 1) q exn:fail:redex:test-source)) c (? . 6)) ((c def c (c (? . 1) q current-traced-metafunctions)) q (11513 . 4)) ((c form c (c (? . 1) q test-->>)) q (11845 . 11)) ((c def c (c (? . 1) q language-nts)) q (4300 . 3)) ((c def c (c (? . 4) q dark-pen-color)) q (26271 . 4)) ((c def c (c (? . 0) q arrow-space)) q (32087 . 4)) ((c def c (c (? . 2) q run-results-time)) c (? . 8)) ((c form c (c (? . 0) q to-lw)) q (40729 . 2)) ((c def c (c (? . 1) q counterexample-term)) c (? . 7)) ((c form c (c (? . 1) q term-match)) q (2441 . 2)) ((c def c (c (? . 4) q show-derivations)) q (23578 . 11)) ((c def c (c (? . 0) q non-terminal-superscript-style)) q (35725 . 4)) ((c def c (c (? . 4) q default-pretty-printer)) q (27360 . 6)) ((c def c (c (? . 0) q non-terminal-style)) q (35475 . 4)) ((c def c (c (? . 1) q default-attempt-size)) q (17712 . 3)) ((c def c (c (? . 0) q relation-clauses-combine)) q (38581 . 5)) ((c def c (c (? . 2) q run-results)) c (? . 8)) ((c form c (c (? . 1) q define-metafunction)) q (7742 . 31)) ((c def c (c (? . 1) q bind-exp)) c (? . 10)) ((c def c (c (? . 4) q term-node?)) q (25834 . 3)) ((c def c (c (? . 4) q term-node-parents)) q (24857 . 3)) ((c def c (c (? . 1) q default-language)) q (4442 . 4)) ((c def c (c (? . 0) q non-terminal-subscript-style)) q (35590 . 4)) ((c def c (c (? . 1) q relation-coverage)) q (13068 . 4)) ((c def c (c (? . 0) q set-lw-line-span!)) c (? . 3)) ((c form c (c (? . 1) q redex-let)) q (2259 . 2)) ((c def c (c (? . 0) q lw-e)) c (? . 3)) ((c def c (c (? . 0) q set-lw-column!)) c (? . 3)) ((c form c (c (? . 1) q I)) q (11078 . 2)) ((c def c (c (? . 0) q arrow->pict)) q (37306 . 3)) ((c def c (c (? . 0) q render-reduction-relation)) q (28718 . 8)) ((c def c (c (? . 0) q lw-column)) c (? . 3)) ((c form c (c (? . 1) q define-judgment-form)) q (9155 . 50)) ((c form c (c (? . 0) q render-metafunction)) q (29202 . 2)) ((c def c (c (? . 2) q bmark-log-data)) c (? . 9)) ((c def c (c (? . 0) q curly-quotes-for-strings)) q (37028 . 4)) ((c def c (c (? . 0) q language->pict)) q (28534 . 5)) ((c def c (c (? . 1) q exn:fail:redex:test-term)) c (? . 6)) ((c def c (c (? . 4) q term-node-labels)) q (24939 . 3)) ((c def c (c (? . 0) q white-bracket-sizing)) q (37469 . 5)) ((c def c (c (? . 1) q struct:derivation)) c (? . 5)) ((c def c (c (? . 1) q test-results)) q (12759 . 2)) ((c form c (c (? . 1) q fresh)) q (7717 . 2)) ((c def c (c (? . 0) q metafunction-style)) q (35360 . 4)) ((c def c (c (? . 4) q term-node-expr)) q (25368 . 3)) ((c def c (c (? . 0) q current-render-pict-adjust)) q (39103 . 4)) ((c def c (c (? . 1) q make-counterexample)) c (? . 7)) ((c def c (c (? . 1) q covered-cases)) q (13199 . 3)) ((c def c (c (? . 0) q rule-pict-info-lhs)) q (31446 . 3)) ((c def c (c (? . 1) q exn:fail:redex:test?)) c (? . 6)) ((c def c (c (? . 4) q dark-brush-color)) q (26426 . 4)) ((c def c (c (? . 1) q depth-dependent-order?)) q (15968 . 5)) ((c def c (c (? . 0) q metafunction-font-size)) q (36128 . 6)) ((c def c (c (? . 0) q rule-pict-info-arrow)) q (31345 . 3)) ((c def c (c (? . 4) q term-node-width)) q (25703 . 3)) ((c form c (c (? . 0) q render-judgment-form)) q (29870 . 2)) ((c form c (c (? . 0) q render-metafunctions)) q (29340 . 10)) ((c def c (c (? . 1) q bind?)) c (? . 10)) ((c form c (c (? . 1) q test-judgment-holds)) q (12667 . 2)) ((c def c (c (? . 0) q rule-pict-info-rhs)) q (31543 . 3)) ((c def c (c (? . 1) q derivation-subs)) c (? . 5)) ((c def c (c (? . 1) q caching-enabled?)) q (1699 . 4)) ((c form c (c (? . 1) q in-hole)) q (2041 . 2)) ((c def c (c (? . 4) q initial-char-width)) q (26106 . 4)) ((c def c (c (? . 0) q rule-pict-info?)) q (31284 . 3)) ((c def c (c (? . 1) q struct:bind)) c (? . 10)) ((c def c (c (? . 2) q benchmark-logging-to)) q (42504 . 4)) ((c def c (c (? . 0) q metafunction-line-gap-space)) q (38125 . 4)) ((c def c (c (? . 4) q reduction-steps-cutoff)) q (25890 . 4)) ((c def c (c (? . 0) q metafunction-gap-space)) q (37881 . 4)) ((c def c (c (? . 0) q lw)) c (? . 3)) ((c form c (c (? . 1) q check-reduction-relation)) q (16666 . 15)) ((c def c (c (? . 0) q metafunction-fill-acceptable-width)) q (38252 . 4)) ((c def c (c (? . 0) q extend-language-show-extended-order)) q (30465 . 4)) ((c def c (c (? . 1) q current-cache-all?)) q (7589 . 4)) ((c def c (c (? . 0) q render-reduction-relation-rules)) q (30616 . 11)) ((c form c (c (? . 1) q check-metafunction)) q (17175 . 15)) ((c def c (c (? . 1) q IO-judgment-form?)) q (11450 . 3)) ((c form c (c (? . 1) q define-language)) q (2918 . 21)) ((c def c (c (? . 2) q run-gen-and-check)) q (41530 . 11)) ((c def c (c (? . 2) q bmark-log-data?)) c (? . 9)) ((c def c (c (? . 0) q reduction-relation-rule-separation)) q (36527 . 4)) ((c form c (c (? . 0) q metafunction->pict)) q (29663 . 2)) ((c def c (c (? . 1) q counterexample)) c (? . 7)) ((c def c (c (? . 0) q label-font-size)) q (35969 . 4)) ((c def c (c (? . 4) q term-node-color)) q (25169 . 3)) ((c def c (c (? . 1) q derivation-term)) c (? . 5)) ((c def c (c (? . 4) q term-node-set-red!)) q (25272 . 4))))

Goals
— abstract syntax
— notions of reduction, substitution
— reductions and calculations
— semantics
— standard reduction
— abstract register machines
— types

Goals
— Redex versus Racket
— define languages
— develop metafunctions, includes basic testing, submodules
— extend languages
— generalizing with any

Goals
— developing meta-functions
— discovering Redex patterns

Goals
— extend languages with concepts needed for reduction relations
— developing reduction relations
— defining a semantics
— testing against a language

Goals
— developing reductions
— semantics

Goals
— typed languages
— developing type judgments
— subject reduction

Goals
— subject reduction testing with trace
— typing judgments

Goals
— revise the language for assignment statements
— a standard reduction system for expression-store tuples
— revise the language for raising exceptions
— a general reduction system for exceptions

Goals
— develop a general reduction system for Lambda with assignments
— develop a standard reduction system for Lambda with exceptions

Goals
— why these three machines: CC machine, CK machine, CEK machine
— theorems connecting the machines, theorems for debugging
— equivalence theorems

Goals
— develop the CESK machine
syntax
(redex-match lang pattern term-expr)
(redex-match lang pattern)
syntax
(redex-match? lang pattern any)
(redex-match? lang pattern)
procedure
(match? val) -> boolean?
  val : any/c
procedure
(match-bindings m) -> (listof bind?)
  m : match?
struct
(struct bind (name exp)
    #:extra-constructor-name make-bind)
  name : symbol?
  exp : any/c
parameter
(caching-enabled?) -> boolean?
(caching-enabled? on?) -> void?
  on? : boolean?
procedure
(set-cache-size! size) -> void?
  size : positive-integer?
parameter
(check-redundancy) -> boolean?
(check-redundancy check?) -> void?
  check? : boolean?
syntax
(term term)
(term term #:lang lang-id)
syntax
hole
syntax
in-hole
syntax
(term-let ([tl-pat expr] ...) body)
 
    tl-pat = identifier
           | (tl-pat-ele ...)
              
tl-pat-ele = tl-pat
           | tl-pat ... ; a literal ellipsis
syntax
(redex-let language ([pattern expression] ...) body ...+)
syntax
(redex-let* language ([pattern expression] ...) body ...+)
syntax
(define-term identifier term)
syntax
(term-match language [pattern expression] ...)
syntax
(term-match/single language [pattern expression] ...)
procedure
(plug context expression) -> any
  context : any/c
  expression : any/c
procedure
(variable-not-in t prefix) -> symbol?
  t : any/c
  prefix : symbol?
procedure
(variables-not-in t vars) -> (listof symbol?)
  t : any/c
  vars : (listof symbol?)
procedure
(exn:fail:redex? v) -> boolean?
  v : any/c
syntax
(define-language lang-name
  non-terminal-def ...
  maybe-binding-spec)
 
   non-terminal-def = (non-terminal-name ...+ ::= pattern ...+)
                    | (non-terminal-name pattern ...+)
                    | ((non-terminal-name ...+) pattern ...+)
                       
 maybe-binding-spec = 
                    | #:binding-forms binding-declaration ...
                       
binding-declaration = binding-pattern
                    | binding-pattern #:exports beta
                       
               beta = nothing
                    | symbol
                    | (shadow beta-seqence ...)
                       
      beta-sequence = beta
                    | ... ; literal ellipsis
syntax
::=
syntax
shadow
syntax
nothing
syntax
(define-extended-language extended-lang base-lang
  non-terminal-def ...
  maybe-binding-spec)
 
  non-terminal-def = (non-terminal-name ...+ ::= pattern ...+)
                   | (non-terminal-name pattern ...+)
                   | ((non-terminal-name ...+) pattern ...+)
                      
maybe-binding-spec = 
                   | #:binding-forms binding-declaration ...
syntax
(define-union-language L base/prefix-lang ...)
 
base/prefix-lang = lang-id
                 | (prefix lang-id)
procedure
(language-nts lang) -> (listof symbol?)
  lang : compiled-lang?
procedure
(compiled-lang? l) -> boolean?
  l : any/c
parameter
(default-language) -> (or/c false/c compiled-lang?)
(default-language lang) -> void?
  lang : (or/c false/c compiled-lang?)
procedure
(alpha-equivalent? lang lhs rhs) -> boolean?
  lang : compiled-lang?
  lhs : any/c
  rhs : any/c
metafunction
(substitute val old-var new-val)
syntax
(reduction-relation language domain base-arrow
                    reduction-case ...
                    shortcuts)
 
        domain = 
               | #:domain pattern
                  
    base-arrow = 
               | #:arrow base-arrow-name
                  
reduction-case = (arrow-name pattern term red-extras ...)
                  
    red-extras = rule-name
               | (fresh fresh-clause ...)
               | (side-condition racket-expression)
               | (where pattern term)
               | (where/hidden pattern term)
               | (where/error pattern term)
               | (bind pattern term)
               | (bind/hidden pattern term)
               | (judgment-holds (judgment-form-id pat/term ...))
               | (side-condition/hidden racket-expression)
                  
     shortcuts = 
               | with shortcut ...
                  
      shortcut = [(old-arrow-name pattern term)
                  (new-arrow-name identifier identifier)]
                  
     rule-name = identifier
               | string
               | (computed-name racket-expression)
                  
  fresh-clause = var
               | ((var1 ...) (var2 ...))
                  
      pat/term = pattern
               | term
syntax
(extend-reduction-relation reduction-relation language more ...)
procedure
(union-reduction-relations r ...) -> reduction-relation?
  r : reduction-relation?
procedure
(reduction-relation->rule-names r) -> (listof symbol?)
  r : reduction-relation?
syntax
(compatible-closure reduction-relation lang non-terminal)
syntax
(context-closure reduction-relation lang pattern)
procedure
(reduction-relation? v) -> boolean?
  v : any/c
procedure
(apply-reduction-relation r t) -> (listof any/c)
  r : (or/c reduction-relation? IO-judgment-form?)
  t : any/c
procedure
(apply-reduction-relation/tag-with-names r  
                                         t) 
 -> (listof (list/c (or/c #f string?) any/c))
  r : (or/c reduction-relation? IO-judgment-form?)
  t : any/c
procedure
(apply-reduction-relation*  r                       
                            t                       
                           [#:all? all              
                            #:cache-all? cache-all? 
                            #:stop-when stop-when]) 
 -> (listof any/c)
  r : (or/c reduction-relation? IO-judgment-form?)
  t : any/c
  all : boolean? = #f
  cache-all? : boolean? = (or all? (current-cache-all?))
  stop-when : (-> any/c any) = (λ (x) #f)
parameter
(current-cache-all?) -> boolean?
(current-cache-all? cache-all?) -> void?
  cache-all? : boolean?
syntax
-->
syntax
fresh
syntax
with
syntax
(define-metafunction language
  metafunction-contract
  [(name pattern ...) term metafunction-extras ...]
  ...)
 
metafunction-contract = 
                      | id : pattern-sequence ... -> range
                        maybe-pre-condition
                        maybe-post-condition
                         
  maybe-pre-condition = #:pre term
                      | 
                         
 maybe-post-condition = #:post term
                      | 
                         
                range = pattern
                      | pattern or range
                      | pattern ∨ range
                      | pattern ∪ range
                         
  metafunction-extras = (side-condition racket-expression)
                      | (side-condition/hidden racket-expression)
                      | (where pat term)
                      | (where/hidden pat term)
                      | (where/error pat term)
                      | (judgment-holds
                         (judgment-form-id pat/term ...))
                      | (clause-name name)
                      | or term
syntax
(define-metafunction/extension f language
  metafunction-contract
  [(g pattern ...) term metafunction-extras ...]
  ...)
syntax
(in-domain? (metafunction-name term ...))
syntax
(define-judgment-form language
  mode-spec
  contract-spec
  invariant-spec
  rule rule ...)
 
     mode-spec = #:mode (form-id pos-use ...)
                  
 contract-spec = 
               | #:contract (form-id pattern-sequence ...)
                  
invariant-spec = #:inv term
               | 
                  
       pos-use = I
               | O
                  
          rule = [premise
                  ...
                  dashes rule-name
                  conclusion]
               | [conclusion
                  premise
                  ...
                  rule-name]
                  
    conclusion = (form-id pat/term ...)
                  
       premise = (judgment-form-id pat/term ...) maybe-ellipsis
               | (where pattern term)
               | (where/hidden pattern term)
               | (where/error pattern term)
               | (side-condition term)
               | (side-condition/hidden term)
                  
     rule-name = 
               | string
               | non-ellipsis-non-hypens-var
                  
      pat/term = pattern
               | term
                  
maybe-ellipsis = 
               | ...
                  
        dashes = ---
               | ----
               | -----
               | etc.
syntax
(define-extended-judgment-form language judgment-form-id
  mode-spec
  contract-spec
  invariant-spec
  rule ...)
syntax
(judgment-holds judgment)
(judgment-holds judgment term)
 
judgment = (judgment-form-id pat/term ...)
syntax
(build-derivations judgment)
struct
(struct derivation (term name subs)
    #:extra-constructor-name make-derivation)
  term : any/c
  name : (or/c string? #f)
  subs : (listof derivation?)
syntax
I
syntax
O
syntax
(define-relation language
  relation-contract
  [(name pattern ...)
   term ...
   metafunction-extras ...] ...)
 
relation-contract = 
                  | form-id ⊂ pattern x ... x pattern
                  | form-id ⊆ pattern × ... × pattern
procedure
(judgment-form? v) -> boolean?
  v : any/c
procedure
(IO-judgment-form? v) -> boolean?
  v : any/c
parameter
(current-traced-metafunctions) -> (or/c 'all (listof symbol?))
(current-traced-metafunctions traced-metafunctions) -> void?
  traced-metafunctions : (or/c 'all (listof symbol?))
syntax
(test-equal e1 e2 option)
 
option = #:equiv pred-expr
       | 
 
  pred-expr : (-> any/c any/c any/c)
syntax
(test-->> rel-expr option ... e1-expr e2-expr ...)
 
option = #:cycles-ok
       | #:equiv pred-expr
       | #:pred pred-expr
 
  rel-expr : reduction-relation?
  pred-expr : (--> any/c any)
  e1-expr : any/c
  e2-expr : any/c
syntax
(test--> rel-expr option ... e1-expr e2-expr ...)
 
option = #:equiv pred-expr
 
  rel-expr : reduction-relation?
  pred-expr : (--> any/c any/c any/c)
  e1-expr : any/c
  e2-expr : any/c
syntax
(test-->>∃ option ... rel-expr start-expr goal-expr)
 
option = #:steps steps-expr
 
  rel-expr : reduction-relation?
  start-expr : any/c
  goal-expr : (or/c (-> any/c any/c)
                    (not/c procedure?))
  steps-expr : (or/c natural-number/c +inf.0)
syntax
test-->>E
syntax
(test-judgment-holds (judgment-form pat/term ...))
syntax
(test-predicate p? e)
procedure
(test-results) -> void?
parameter
(default-equiv) -> (-> any/c any/c any/c)
(default-equiv equiv) -> void?
  equiv : (-> any/c any/c any/c)
syntax
(make-coverage subject)
 
subject = metafunction
        | relation-expr
procedure
(coverage? v) -> boolean?
  v : any/c
parameter
(relation-coverage) -> (listof coverage?)
(relation-coverage tracked) -> void?
  tracked : (listof coverage?)
procedure
(covered-cases c) -> (listof (cons/c string? natural-number/c))
  c : coverage?
syntax
(generate-term from-pattern)
(generate-term from-judgment-form)
(generate-term from-metafunction)
(generate-term from-reduction-relation)
 
           from-pattern = language pattern size-expr kw-args ...
                        | language pattern
                        | language pattern #:i-th index-expr
                        | language pattern #:i-th
                           
     from-judgment-form = language #:satisfying
                          (judgment-form-id pattern ...)
                        | language #:satisfying
                          (judgment-form-id pattern ...)
                          size-expr
                           
      from-metafunction = language #:satisfying
                          (metafunction-id pattern ...) = pattern
                        | language #:satisfying
                          (metafunction-id pattern ...) = pattern
                          size-expr
                        | #:source metafunction size-expr kw-args
                        | #:source metafunction
                           
from-reduction-relation = #:source reduction-relation-expr
                          size-expr kw-args ...
                        | #:source reduction-relation-expr
                           
                kw-args = #:attempt-num attempts-expr
                        | #:retries retries-expr
 
  size-expr : natural-number/c
  attempt-num-expr : natural-number/c
  retries-expr : natural-number/c
syntax
(redex-check template property-expr kw-arg ...)
 
template = language pattern
         | language pattern #:ad-hoc
         | language pattern #:in-order
         | language pattern #:uniform-at-random p-value
         | language pattern #:enum bound
         | language #:satisfying
           (judgment-form-id pattern ...)
         | language #:satisfying
           (metafunction-id pattern ...) = pattern
            
  kw-arg = #:attempts attempts-expr
         | #:source metafunction
         | #:source relation-expr
         | #:retries retries-expr
         | #:print? print?-expr
         | #:attempt-size attempt-size-expr
         | #:prepare prepare-expr
         | #:keep-going? keep-going?-expr
 
  property-expr : any/c
  attempts-expr : natural-number/c
  relation-expr : reduction-relation?
  retries-expr : natural-number/c
  print?-expr : any/c
  attempt-size-expr : (-> natural-number/c natural-number/c)
  prepare-expr : (-> any/c any/c)
parameter
(depth-dependent-order?) -> (or/c boolean? 'random)
(depth-dependent-order? depth-dependent) -> void?
  depth-dependent : (or/c boolean? 'random)
 = 'random
syntax
(redex-generator language-id satisfying size-expr)
 
satisfying = (judgment-form-id pattern ...)
           | (metafunction-id pattern ...) = pattern
 
  size-expr : natural-number/c
struct
(struct counterexample (term)
    #:extra-constructor-name make-counterexample
    #:transparent)
  term : any/c
struct
(struct exn:fail:redex:test exn:fail:redex (source term)
    #:extra-constructor-name make-exn:fail:redex:test)
  source : exn:fail?
  term : any/c
syntax
(check-reduction-relation relation property kw-args ...)
 
kw-arg = #:attempts attempts-expr
       | #:retries retries-expr
       | #:print? print?-expr
       | #:attempt-size attempt-size-expr
       | #:prepare prepare-expr
 
  property : (-> any/c any/c)
  attempts-expr : natural-number/c
  retries-expr : natural-number/c
  print?-expr : any/c
  attempt-size-expr : (-> natural-number/c natural-number/c)
  prepare-expr : (-> any/c any/c)
syntax
(check-metafunction metafunction property kw-args ...)
 
kw-arg = #:attempts attempts-expr
       | #:retries retries-expr
       | #:print? print?-expr
       | #:attempt-size attempt-size-expr
       | #:prepare prepare-expr
 
  property : (-> (listof any/c) any/c)
  attempts-expr : natural-number/c
  retries-expr : natural-number/c
  print?-expr : any/c
  attempt-size-expr : (-> natural-number/c natural-number/c)
  prepare-expr : (-> (listof any/c) (listof any/c))
procedure
(default-attempt-size n) -> natural-number/c
  n : natural-number/c
parameter
(default-check-attempts) -> natural-number/c
(default-check-attempts attempts) -> void?
  attempts : natural-number/c
parameter
(redex-pseudo-random-generator) -> pseudo-random-generator?
(redex-pseudo-random-generator generator) -> void?
  generator : pseudo-random-generator?
procedure
(exn:fail:redex:generation-failure? v) -> boolean?
  v : any/c
procedure
(traces  reductions                                        
         expr                                              
        [#:multiple? multiple?                             
         #:reduce reduce                                   
         #:pred pred                                       
         #:pp pp                                           
         #:colors colors                                   
         #:racket-colors? racket-colors?                   
         #:scheme-colors? scheme-colors?                   
         #:filter term-filter                              
         #:x-spacing x-spacing                             
         #:y-spacing y-spacing                             
         #:layout layout                                   
         #:edge-labels? edge-labels?                       
         #:edge-label-font edge-label-font                 
         #:graph-pasteboard-mixin graph-pasteboard-mixin]) 
 -> void?
  reductions : (or/c reduction-relation? IO-judgment-form?)
  expr : (or/c any/c (listof any/c))
  multiple? : boolean? = #f
  reduce : (-> reduction-relation? any/c
               (listof (list/c (union false/c string?) any/c)))
         = apply-reduction-relation/tag-with-names
  pred : (or/c (-> sexp any)             = (λ (x) #t)
               (-> sexp term-node? any))
  pp : (or/c (any -> string)
             (any output-port number (is-a?/c text%) -> void))
     = default-pretty-printer
  colors : (listof
            (cons/c string?
                    (and/c (listof (or/c string? (is-a?/c color%)))
                           (λ (x) (<= 0 (length x) 6)))))
         = '()
  racket-colors? : boolean? = #t
  scheme-colors? : boolean? = racket-colors?
  term-filter : (-> any/c (or/c #f string?) any/c)
              = (λ (x y) #t)
  x-spacing : real? = 15
  y-spacing : real? = 15
  layout : (-> (listof term-node?) void?) = void
  edge-labels? : boolean? = #t
  edge-label-font : (or/c #f (is-a?/c font%)) = #f
  graph-pasteboard-mixin : (make-mixin-contract graph-pasteboard<%>)
                         = values
procedure
(traces/ps  reductions                                       
            expr                                             
            file                                             
           [#:multiple? multiple?                            
            #:reduce reduce                                  
            #:pred pred                                      
            #:pp pp                                          
            #:colors colors                                  
            #:filter term-filter                             
            #:layout layout                                  
            #:x-spacing x-spacing                            
            #:y-spacing y-spacing                            
            #:edge-labels? edge-labels?                      
            #:edge-label-font edge-label-font                
            #:graph-pasteboard-mixin graph-pasteboard-mixin] 
            #:post-process post-process)                     
 -> void?
  reductions : (or/c reduction-relation? IO-judgment-form?)
  expr : (or/c any/c (listof any/c))
  file : (or/c path-string? path?)
  multiple? : boolean? = #f
  reduce : (-> reduction-relation? any/c
               (listof (list/c (union false/c string?) any/c)))
         = apply-reduction-relation/tag-with-names
  pred : (or/c (-> sexp any)             = (λ (x) #t)
               (-> sexp term-node? any))
  pp : (or/c (any -> string)
             (any output-port number (is-a?/c text%) -> void))
     = default-pretty-printer
  colors : (listof
            (cons/c string?
                    (and/c (listof (or/c string? (is-a?/c color%)))
                           (λ (x) (<= 0 (length x) 6)))))
         = '()
  term-filter : (-> any/c (or/c #f string?) any/c)
              = (λ (x y) #t)
  layout : (-> (listof term-node?) void?) = void
  x-spacing : number? = 15
  y-spacing : number? = 15
  edge-labels? : boolean? = #t
  edge-label-font : (or/c #f (is-a?/c font%)) = #f
  graph-pasteboard-mixin : (make-mixin-contract graph-pasteboard<%>)
                         = values
  post-process : (-> (is-a?/c graph-pasteboard<%>) any/c)
procedure
(stepper reductions t [pp]) -> void?
  reductions : (or/c reduction-relation? IO-judgment-form?)
  t : any/c
  pp : (or/c (any -> string)
             (any output-port number (is-a?/c text%) -> void))
     = default-pretty-printer
procedure
(stepper/seed reductions seed [pp]) -> void?
  reductions : (or/c reduction-relation? IO-judgment-form?)
  seed : (cons/c any/c (listof any/c))
  pp : (or/c (any -> string)
             (any output-port number (is-a?/c text%) -> void))
     = default-pretty-printer
procedure
(show-derivations  derivations                             
                  [#:pp pp                                 
                   #:racket-colors? racket-colors?         
                   #:init-derivation init-derivation]) -> any
  derivations : (cons/c derivation? (listof derivation?))
  pp : (or/c (any -> string)
             (any output-port number (is-a?/c text%) -> void))
     = default-pretty-printer
  racket-colors? : boolean? = #f
  init-derivation : exact-nonnegative-integer? = 0
procedure
(derivation/ps  derivation                           
                filename                             
               [#:pp pp                              
                #:racket-colors? racket-colors?]     
                #:post-process post-process)     -> void?
  derivation : derivation?
  filename : path-string?
  pp : (or/c (any -> string)
             (any output-port number (is-a?/c text%) -> void))
     = default-pretty-printer
  racket-colors? : boolean? = #f
  post-process : (-> (is-a?/c pasteboard%) any)
procedure
(term-node-children tn) -> (listof term-node?)
  tn : term-node?
procedure
(term-node-parents tn) -> (listof term-node?)
  tn : term-node?
procedure
(term-node-labels tn) -> (listof (or/c false/c string?))
  tn : term-node?
procedure
(term-node-set-color! tn color) -> void?
  tn : term-node?
  color : (or/c string? (is-a?/c color%) false/c)
procedure
(term-node-color tn) -> (or/c string? (is-a?/c color%) false/c)
  tn : term-node?
procedure
(term-node-set-red! tn red?) -> void?
  tn : term-node?
  red? : boolean?
procedure
(term-node-expr tn) -> any
  tn : term-node?
procedure
(term-node-set-position! tn x y) -> void?
  tn : term-node?
  x : (and/c real? positive?)
  y : (and/c real? positive?)
procedure
(term-node-x tn) -> real?
  tn : term-node?
procedure
(term-node-y tn) -> real?
  tn : term-node?
procedure
(term-node-width tn) -> real?
  tn : term-node?
procedure
(term-node-height tn) -> real?
  tn : term-node?
procedure
(term-node? v) -> boolean?
  v : any/c
parameter
(reduction-steps-cutoff) -> number?
(reduction-steps-cutoff cutoff) -> void?
  cutoff : number?
parameter
(initial-font-size) -> number?
(initial-font-size size) -> void?
  size : number?
parameter
(initial-char-width) -> (or/c number? (-> any/c number?))
(initial-char-width width) -> void?
  width : (or/c number? (-> any/c number?))
parameter
(dark-pen-color) -> (or/c string? (is-a?/c color<%>))
(dark-pen-color color) -> void?
  color : (or/c string? (is-a?/c color<%>))
parameter
(dark-brush-color) -> (or/c string? (is-a?/c color<%>))
(dark-brush-color color) -> void?
  color : (or/c string? (is-a?/c color<%>))
parameter
(light-pen-color) -> (or/c string? (is-a?/c color<%>))
(light-pen-color color) -> void?
  color : (or/c string? (is-a?/c color<%>))
parameter
(light-brush-color) -> (or/c string? (is-a?/c color<%>))
(light-brush-color color) -> void?
  color : (or/c string? (is-a?/c color<%>))
parameter
(dark-text-color) -> (or/c string? (is-a?/c color<%>))
(dark-text-color color) -> void?
  color : (or/c string? (is-a?/c color<%>))
parameter
(light-text-color) -> (or/c string? (is-a?/c color<%>))
(light-text-color color) -> void?
  color : (or/c string? (is-a?/c color<%>))
parameter
(pretty-print-parameters) -> (-> (-> any/c) any/c)
(pretty-print-parameters f) -> void?
  f : (-> (-> any/c) any/c)
procedure
(default-pretty-printer v port width text) -> void?
  v : any/c
  port : output-port?
  width : exact-nonnegative-integer?
  text : (is-a?/c text%)
syntax
(render-term lang term)
(render-term lang term file)
syntax
(term->pict lang term)
procedure
(render-term/pretty-write lang               
                          term               
                          filename           
                          #:width width) -> void?
  lang : compiled-lang?
  term : any/c
  filename : path-string?
  width : #f
procedure
(term->pict/pretty-write lang               
                         term               
                         filename           
                         #:width width) -> pict?
  lang : compiled-lang?
  term : any/c
  filename : (or/c path-string? #f)
  width : #f
procedure
(render-language lang [file #:nts nts]) -> (if file void? pict?)
  lang : compiled-lang?
  file : (or/c false/c path-string?) = #f
  nts : (or/c false/c (listof (or/c string? symbol?)))
      = (render-language-nts)
procedure
(language->pict lang [#:nts nts]) -> pict?
  lang : compiled-lang?
  nts : (or/c false/c (listof (or/c string? symbol?)))
      = (render-language-nts)
procedure
(render-reduction-relation  rel             
                           [file            
                            #:style style]) 
 -> (if file void? pict?)
  rel : reduction-relation?
  file : (or/c false/c path-string?) = #f
  style : reduction-rule-style/c = (rule-pict-style)
procedure
(reduction-relation->pict r [#:style style]) -> pict?
  r : reduction-relation?
  style : reduction-rule-style/c = (rule-pict-style)
syntax
(render-metafunction metafunction-name maybe-contract)
syntax
(render-metafunction metafunction-name filename maybe-contract)
syntax
(render-metafunctions metafunction-name ...
                      maybe-filename maybe-contract)
 
 maybe-filename = 
                | #:file filename
                | #:filename filename
                   
maybe-contract? = 
                | #:contract? bool-expr
syntax
(metafunction->pict metafunction-name maybe-contract?)
syntax
(metafunctions->pict metafunction-name ...)
syntax
(render-relation relation-name)
syntax
(render-relation relation-name filename)
syntax
(render-judgment-form judgment-form-name)
syntax
(render-judgment-form judgment-form-name filename)
syntax
(relation->pict relation-name)
syntax
(judgment-form->pict judgment-form-name)
parameter
(render-language-nts) -> (or/c false/c (listof symbol?))
(render-language-nts nts) -> void?
  nts : (or/c false/c (listof symbol?))
parameter
(non-terminal-gap-space) -> real?
(non-terminal-gap-space gap-space) -> void?
  gap-space : real?
parameter
(extend-language-show-union) -> boolean?
(extend-language-show-union show?) -> void?
  show? : boolean?
parameter
(extend-language-show-extended-order) -> boolean?
(extend-language-show-extended-order ext-order?) -> void?
  ext-order? : boolean?
parameter
(render-reduction-relation-rules)
 -> (or/c false/c
          (listof (or/c symbol?
                        string?
                        exact-nonnegative-integer?)))
(render-reduction-relation-rules rules) -> void?
  rules : (or/c false/c
                (listof (or/c symbol?
                              string?
                              exact-nonnegative-integer?)))
parameter
(rule-pict-style) -> reduction-rule-style/c
(rule-pict-style style) -> void?
  style : reduction-rule-style/c
value
reduction-rule-style/c : contract?
procedure
(rule-pict-info? x) -> boolean?
  x : any/c
procedure
(rule-pict-info-arrow rule-pict-info) -> symbol?
  rule-pict-info : rule-pict-info?
procedure
(rule-pict-info-lhs rule-pict-info) -> pict?
  rule-pict-info : rule-pict-info?
procedure
(rule-pict-info-rhs rule-pict-info) -> pict?
  rule-pict-info : rule-pict-info?
procedure
(rule-pict-info-label rule-pict-info) -> (or/c symbol? #f)
  rule-pict-info : rule-pict-info?
procedure
(rule-pict-info-computed-label rule-pict-info)
 -> (or/c pict? #f)
  rule-pict-info : rule-pict-info?
procedure
(rule-pict-info->side-condition-pict  rule-pict-info     
                                     [max-width])    -> pict?
  rule-pict-info : rule-pict-info?
  max-width : real? = +inf.0
parameter
(arrow-space) -> natural-number/c
(arrow-space space) -> void?
  space : natural-number/c
parameter
(label-space) -> natural-number/c
(label-space space) -> void?
  space : natural-number/c
parameter
(metafunction-pict-style)
 -> (or/c 'left-right
          'up-down
          'left-right/vertical-side-conditions
          'up-down/vertical-side-conditions
          'left-right/compact-side-conditions
          'up-down/compact-side-conditions
          'left-right/beside-side-conditions)
(metafunction-pict-style style) -> void?
  style : (or/c 'left-right
                'up-down
                'left-right/vertical-side-conditions
                'up-down/vertical-side-conditions
                'left-right/compact-side-conditions
                'up-down/compact-side-conditions
                'left-right/beside-side-conditions)
parameter
(metafunction-up/down-indent) -> (>=/c 0)
(metafunction-up/down-indent indent) -> void?
  indent : (>=/c 0)
parameter
(delimit-ellipsis-arguments?) -> any/c
(delimit-ellipsis-arguments? delimit?) -> void?
  delimit? : any/c
parameter
(white-square-bracket) -> (-> boolean? pict?)
(white-square-bracket make-white-square-bracket) -> void?
  make-white-square-bracket : (-> boolean? pict?)
procedure
(homemade-white-square-bracket open?) -> pict?
  open? : boolean?
procedure
(default-white-square-bracket open?) -> pict?
  open? : boolean?
parameter
(linebreaks) -> (or/c #f (listof boolean?))
(linebreaks breaks) -> void?
  breaks : (or/c #f (listof boolean?))
parameter
(metafunction-cases)
 -> (or/c #f (and/c (listof (or/c symbol?
                                  string?
                                  exact-nonnegative-integer?))
                    pair?))
(metafunction-cases cases) -> void?
  cases : (or/c #f (and/c (listof (or/c symbol?
                                        string?
                                        exact-nonnegative-integer?))
                          pair?))
parameter
(judgment-form-cases)
 -> (or/c #f
          (non-empty-listof (or/c symbol?
                                  string?
                                  exact-nonnegative-integer?)))
(judgment-form-cases cases) -> void?
  cases : (or/c #f
                (non-empty-listof (or/c symbol?
                                        string?
                                        exact-nonnegative-integer?)))
parameter
(label-style) -> text-style/c
(label-style style) -> void?
  style : text-style/c
parameter
(grammar-style) -> text-style/c
(grammar-style style) -> void?
  style : text-style/c
parameter
(paren-style) -> text-style/c
(paren-style style) -> void?
  style : text-style/c
parameter
(literal-style) -> text-style/c
(literal-style style) -> void?
  style : text-style/c
parameter
(metafunction-style) -> text-style/c
(metafunction-style style) -> void?
  style : text-style/c
parameter
(non-terminal-style) -> text-style/c
(non-terminal-style style) -> void?
  style : text-style/c
parameter
(non-terminal-subscript-style) -> text-style/c
(non-terminal-subscript-style style) -> void?
  style : text-style/c
parameter
(non-terminal-superscript-style) -> text-style/c
(non-terminal-superscript-style style) -> void?
  style : text-style/c
parameter
(default-style) -> text-style/c
(default-style style) -> void?
  style : text-style/c
parameter
(label-font-size) -> (and/c (between/c 1 255) integer?)
(label-font-size size) -> void?
  size : (and/c (between/c 1 255) integer?)
parameter
(metafunction-font-size) -> (and/c (between/c 1 255)
                                   integer?)
(metafunction-font-size size) -> void?
  size : (and/c (between/c 1 255)
                integer?)
parameter
(default-font-size) -> (and/c (between/c 1 255) integer?)
(default-font-size size) -> void?
  size : (and/c (between/c 1 255) integer?)
parameter
(reduction-relation-rule-separation) -> (parameter/c real?)
(reduction-relation-rule-separation sep) -> void?
  sep : (parameter/c real?)
parameter
(reduction-relation-rule-extra-separation)
 -> (parameter/c real?)
(reduction-relation-rule-extra-separation sep) -> void?
  sep : (parameter/c real?)
parameter
(reduction-relation-rule-line-separation)
 -> (parameter/c real?)
(reduction-relation-rule-line-separation sep) -> void?
  sep : (parameter/c real?)
parameter
(curly-quotes-for-strings) -> boolean?
(curly-quotes-for-strings on?) -> void?
  on? : boolean?
parameter
(current-text) -> (-> string? text-style/c number? pict?)
(current-text proc) -> void?
  proc : (-> string? text-style/c number? pict?)
procedure
(arrow->pict arrow) -> pict?
  arrow : symbol?
procedure
(set-arrow-pict! arrow proc) -> void?
  arrow : symbol?
  proc : (-> pict?)
parameter
(white-bracket-sizing)
 -> (-> string? number? (values number? number? number? number?))
(white-bracket-sizing proc) -> void?
  proc : (-> string? number? (values number? number? number? number?))
parameter
(horizontal-bar-spacing)
 -> (parameter/c exact-nonnegative-integer?)
(horizontal-bar-spacing space) -> void?
  space : (parameter/c exact-nonnegative-integer?)
parameter
(metafunction-gap-space) -> real?
(metafunction-gap-space gap-space) -> void?
  gap-space : real?
parameter
(metafunction-rule-gap-space) -> real?
(metafunction-rule-gap-space gap-space) -> void?
  gap-space : real?
parameter
(metafunction-line-gap-space) -> real?
(metafunction-line-gap-space gap-space) -> void?
  gap-space : real?
parameter
(metafunction-fill-acceptable-width) -> real?
(metafunction-fill-acceptable-width width) -> void?
  width : real?
parameter
(metafunction-combine-contract-and-rules)
 -> (pict? pict? . -> . pict?)
(metafunction-combine-contract-and-rules combine) -> void?
  combine : (pict? pict? . -> . pict?)
parameter
(relation-clauses-combine)
 -> (parameter/c (-> (listof pict?) pict?))
(relation-clauses-combine combine) -> void?
  combine : (parameter/c (-> (listof pict?) pict?))
parameter
(where-make-prefix-pict) -> (parameter/c (-> pict?))
(where-make-prefix-pict make-prefix) -> void?
  make-prefix : (parameter/c (-> pict?))
parameter
(where-combine) -> (parameter/c (-> pict? pict? pict?))
(where-combine combine) -> void?
  combine : (parameter/c (-> pict? pict? pict?))
parameter
(current-render-pict-adjust) -> (pict? symbol? . -> . pict?)
(current-render-pict-adjust adjust) -> void?
  adjust : (pict? symbol? . -> . pict?)
syntax
(with-unquote-rewriter proc expression)
syntax
(with-atomic-rewriter name-symbol
                      string-or-thunk-returning-pict
                      expression)
syntax
(with-compound-rewriter name-symbol
                        proc
                        expression)
syntax
(with-compound-rewriters ([name-symbol proc] ...)
                         expression)
struct
(struct lw (e
            line
            line-span
            column
            column-span
            unq?
            metafunction?)
    #:extra-constructor-name make-lw
    #:mutable)
  e : (or/c string?
            symbol?
            pict?
            (listof (or/c (symbols 'spring) lw?)))
  line : exact-positive-integer?
  line-span : exact-positive-integer?
  column : exact-positive-integer?
  column-span : exact-positive-integer?
  unq? : boolean?
  metafunction? : boolean?
procedure
(build-lw e line line-span column column-span) -> lw?
  e : (or/c string?
            symbol?
            pict?
            (listof (or/c (symbols 'spring) lw?)))
  line : exact-positive-integer?
  line-span : exact-positive-integer?
  column : exact-positive-integer?
  column-span : exact-positive-integer?
syntax
(to-lw arg)
procedure
(to-lw/stx stx) -> lw?
  stx : syntax?
procedure
(render-lw language/nts lw) -> pict?
  language/nts : (or/c (listof symbol?) compiled-lang?)
  lw : lw?
procedure
(lw->pict language/ntw lw) -> pict?
  language/ntw : (or/c (listof symbol?) compiled-lang?)
  lw : lw?
procedure
(just-before stuff lw) -> lw?
  stuff : (or/c pict? string? symbol?)
  lw : lw?
procedure
(just-after stuff lw) -> lw?
  stuff : (or/c pict? string? symbol?)
  lw : lw?
syntax
(define-rewrite id from ==> to
  [#:context (context-id ...)
   #:variables (variable-id ...)
   #:once-only
   #:exactly-once])
syntax
(define-rewrite/compose id rw-id ...)
syntax
(include/rewrite path-spec mod-id rw-id ...)
procedure
(run-gen-and-check  get-gen           
                    check             
                    seconds           
                   [#:name name       
                    #:type type]) -> run-results?
  get-gen : (-> (-> any/c))
  check : (-> any/c boolean?)
  seconds : natural-number/c
  name : string? = "unknown"
  type : symbol? = 'unknown
struct
(struct run-results (tries time cexps))
  tries : natural-number/c
  time : natural-number/c
  cexps : natural-number/c
procedure
(run-gen-and-check/mods  gen-mod-path       
                         check-mod-path     
                         seconds            
                        [#:name name])  -> run-results?
  gen-mod-path : module-path?
  check-mod-path : module-path?
  seconds : natural-number/c
  name : string? = "unknown"
struct
(struct bmark-log-data (data))
  data : any/c
procedure
(benchmark-logging-to filename thunk) -> any/c
  filename : string?
  thunk : (-> any/c)
parameter
(bmark-log-directory)
 -> (or/c path-string? path-for-some-system? 'up 'same)
(bmark-log-directory directory) -> void?
  directory : (or/c path-string? path-for-some-system? 'up 'same)
 = (current-directory)
procedure
(all-mods)
 -> (listof (list/c string? module-path? module-path?))