v7.8 * change the typesetting of `(in-hole E hole)` from something like E to something like E[]. * bug fixes v7.7 * change modeless judgment forms to check for moded subderivations (instead of synthesizing them itself) * generalize typesetting to accept pict-convertibles, not just picts * bug fixes v7.6 * bug fixes v7.5 * add modeless judgment forms * relicense under Apache v2 and MIT licenses * add test-match and test-no-match * bug fixes v7.4 * added default-relation-clause-combine and relation-clause-combine * bug fixes and documentation improvements v7.3 * added compatible-closure-context v7.2 * misc minor bug fixes v7.2 * added derivation->pict * brought the letrec model up to date with modern Racket * misc minor bug fixes and documentation improvements v7.1 * added make-immutable-binding-hash and make-binding-hash * various bug fixes v7.0 * various bug fixes v6.12 * typeset prime characters better, e.g. when writing e_′, don't use the subscript style for the ′ character * various bug fixes v6.11 * various bug fixes * added #:codomain clause to `reduction-relation` v6.10 * added a two argument version of `alpha-equivalent?` * added `sc-linebreaks` * use the atomic rewriters when rendering a metafunction's name in its type signature * added judgment-form-show-rule-names * improved the binding-forms documentation * misc bug fixes v6.9 * add mf-apply * improve define-relation's cooperation with judgment-holds and related constructs * various bug fixes v6.8 * improved the ambiguity checker * minor bug fixes v6.7 * performance improvements * minor bug fixes v6.6 * added test-judgment-holds * bug fixes and performance improvements v6.5 * bug fixes v6.4 * add support for variable binding declarations in define-language and have pattern match now preserve alpha equivalence, based on those declarations. This improvement is based on the ideas in Paul Stansifer's dissertation and is implemented by Paul Stansifer. * changed shortcuts in --> so that non-terminals are no longer allowed for the names in the shortcut "parameters" These shortcut names were never constrained to actually be non-terminals, so this change is intended entirely to be able to give a helpful error message in an attempt to avoid confusion v6.3 * Add new syntax error checking that ensures that each pattern generates either exactly one hole or zero holes. * Add a number of new parameters for finer-grained control of rendering. * Added a new, in-depth tutorial and some extended exercises * Added the #:all? argument to apply-reduction-relation* * check-metafunction and check-reduction-relation (and redex-check with the #:source keyword) no longer check the "extras" clauses and instead just blindly generate from the left-hand side patterns. (This speeds up compilation of Redex programs that use define-metafunction and reduction-relation.) * Judgment forms that have the mode (I O) can be used as reduction-relations * misc bug fixes v6.2 * Performance improvements for example generation, both for enumerators (#:i-th in generate-term) and judgment forms (#:satisfying in generate-term) * Add short discussion of each of the benchmark programs * Use unicode whitebracket characters for metafunction typesetting * add support for "big left curly bracket"-style conditionals when typesetting metafunctions v6.1 * changed the semantics for _!_ variables when they are under ellipses, making them less insane. There is now a much simpler description of how these two interact (in the docs) * improved the performance of term generation from judgment-forms (when using the #:satisfying keyword argument) * lots of improvements to the enumeration test case generator * metafunctions can now typeset their contracts * added #:equiv option to test-equal * added default-equiv * added the #:enum-p keyword (based on statistics help from Neil Toronto) * change the default strategy of redex-check to do enumeration first, then interleave random generation and enumeration and then just do random generation v6.0 * Added an enumerator for patterns. For example, here's how to get the first 100 untyped LC terms (over 3 variables) and the 10^10000-th: #lang racket (require redex) (define-language L (e (e e) x (λ (x) e)) (x a b c)) (for/list ([i (in-range 100)]) (generate-term L e #:i-th i)) (generate-term L e #:i-th (expt 10 10000)) Thanks to Max New for the enumerator. * More patterns that match no terms are now syntax errors, e.g.: (any_1 ..._!_1 any_2 ..._!_1 (any_1 any_2) ...) * added where-make-prefix-pict and where-combine parameters. * added #:keep-going to redex-check * added #:satisfying to redex-check * added #:reduce argument to traces * DrRacket's Check Syntax now works better with Redex pattern variables * The pattern _ now matches anything but does not bind a variable * bug fixes v5.3.4 * adjusted define-union-language to allow the unioned languages to have overlapping non-terminals; in that case the productions are combined * Adjust check-metafunction and check-reduction-relation so that they skip over randomly generated terms that don't match the contract spec (or #:domain spec). This means that when there is a case in the metafunction (or reduction-relation) whose nominal pattern is more general than the contract would allow, that those terms are discarded instead of used as inputs to the predicate. * Added the #:pre keyword to define-metafunction. It allows contracts that have to relate different arguments to a metafunction. * Fixed the way random generation for define-judgment-form works so that it properly handles metafunctions (i.e., it properly takes into account that previous patterns in a metafunction must not match when generating a particular clause) v5.3.3 No changes v5.3.2 * added random-generation based on define-judgment-form (which allows Redex to more effectively generate things like well-typed terms) * removed the restriction on unquotes in define-judgment-form * added the option to use judgment-forms with only I mode positions in terms * added 'boolean' as a new pattern * define-relation now compiles to judgment-form (instead of a metafunction) * added show-derivations to visualize judgment form derivations v5.3.1 * added optional #:lang keyword to term * added the ability to name clauses to define-judgment-form * added judgment-form-cases * adjust define-judgment-form typesetting so that it uses the line breaks in a premise to determine how to line break the typeset version v5.3 * added the amb tutorial. * added define-union-language * added define-extended-judgment-form * extended render-* functions so they can produce PDF v5.2.1 * rewrote the internals of the pattern matcher to be more consistent (centralized more error checking, moving more of it to compile time, and various other internal cleanups). * improved the way caching works so it uses about 1/5th memory and speeds up the R6RS test suite by about a factor of 2. * added a number of optimizations to the pattern matcher that speed up the R6RS test suite by 50% or so and speed up a lambdaJS benchmark by about a factor of 25. * added support for side-conditions and where clauses to define-relation, also added support for side-conditions to define-judgment-form * added the List-machine benchmark (by Appel, Dockins & Leroy) v5.2 * added define-judgment-form form * added define-term form * added with-compound-rewriters form * added Ariola-Felleisen by-need evaluation contexts to examples * improved error message for definition forms in expression contexts v5.1.2 * added support for typsetting define-relation relations * made apply-reduction-relation* call remove-duplicates on the result of apply-reduction-relation * extended render-reduction-relation-rules to accept rule indices in addition to rule names * added the to-lw/stx procedure * fixed domain checking for unioned reduction relations * added the #:cache-all? argument to apply-reduction-relation* and the current-cache-all? parameter * fixed stepper's handling of symbols that required || quoting * removed all undocumented exports * added the redex-let form * added the #:source argument to generate-term * changed redex-match to hide bindings for named ellipses such as ..._x * improve test-->E failure message * fixed misc. bugs in examples and typos in documentation v5.1.1 * changed pattern language to disallow unquote * fixed matching of ..._x and ..._!_x within ellipses * fixed bugs in stepper's diff highlighting * improved rendering of arrows in typesetting * added support for unioned metafunction codomains * fixed typesetting of the pattern (hole p_0 p_1 ...) * added arrow->pict, which shows how reduction relation are rendered in typesetting * added a parameter that provides the default for redex-check's #:attempts argument * changed the random term generator to produce shorter sequences * added a Redex model of the system in Jay McCarthy's ICFP '09 paper "Automatically RESTful Web Applications Or, Marking Modular Serializable Continuations" to the examples directory * resolved PRs 10665, 11174, 11579, 11041, 10837, and 11853 v5.1 * adds an optional #:pred keyword argument to `test-->>' form * added the `redex-pseudo-random-generator' parameter * added option `::=' syntax to non-terminal definitions * added contract support to `define-relation' * added the `test-->∃' form * fixed minor bugs v5.0.2 * added `pretty-print-parameters' to control term pretty-printing * added `grammar-style' and `paren-style' typesetting parameters * added support for computed reduction rule names * added delimited control model to examples * added optional #:attempt-size and #:prepare keyword arguments to random testing forms * fixed minor bugs v5.0.1 * changed the matching of `where' clauses in a backwards-incompatible way. Previously, pattern variables bound by a `where' left-hand side shadowed bindings from earlier clauses and the case's left-hand side; now, `where' clauses match only when their bindings match the existing ones. * fixed minor bugs v5.0 * added an optional term-equivalence predicate to the test--> and test-->> forms * added R6RS and Racket VM models to examples sub-collection * fixed minor bugs v4.2.5 * reversed the order in which `where' and `side-condition' clauses appear in typeset definitions * added support for `where' and `side-condition' clauses that do not appear in the metafunction's typeset definition * added a #:print? flag to redex-check, to control whether it prints or returns its result * renamed the #:attempts keyword to #:attempt-num in the `generate-term' form * changed typesetting to render `where' clauses as `fresh' clauses when the right-hand side is a call to `variable-not-in' or `variables-not-in' * changed typesetting of meta-variables to render anything following a caret (^) as a superscript * minor bug fixes v4.2.4 * minor bug fixes v4.2.3 * added support for collecting metafunction coverage, using the 'relation-coverage' parameter. This includes a backwards incompatible change: the parameter's value is now a list of coverage structures, to allow coverage collection for multiple metafunctions and reduction relations at once. * redex/reduction-semantics exports the names `hole' and `in-hole' (and `term' no longer captures those names). * minor bug fixes v4.2.2 * minor bug fixes v4.2.1 * improved 'where' conditions in metafunctions and reduction-relations so that they work with Redex's full pattern language. This is a backwards incompatible change. In old versions, variables used in a where clause were independent of the pattern language. Now, if the variable in a where clause is a literal in the grammar, the result of the where clause must be that literal. Similarly, if the variable is a non-terminal, the result must match that non-terminal. * added 'define-relation' * relaxed the restrictions on metafunctions so that multiple pattern matches are allowed, as long as the right-hand side has the same value for each different pattern binding * added metafunction styles 'up-down/compact-side-conditions, 'left-right/compact-side-conditions, and 'left-right/beside-side-conditions. * added #:x-spacing and #:y-spacing parameters to traces and traces/ps * changed the grammar for 'side-condition' clauses from (side-condition scheme-expression ... ) to (side-condition scheme-expression) v4.2 * minor bug fixes v4.1.5 * renamed test--> to test-->> * added a new test--> that only tests for a single step in the reduction sequence * added #:cycles-ok flag to (what is now called) test-->> * define-metafunction and reduction-relation now work better with Check Syntax * added the #:arrow keyword to reduction-relation, which lets you use a different main arrow (mostly useful for the typesetting) * added domain specifications to reduction relations via the #:domain keyword * 'traces' copes better with errors during reduction * initial-char-width now accepts functions to give finer grained control of the initial widths of the terms. * traces & traces/ps: added the ability to specify a mixin to be mixed into the graph pasteboard * added built-in patterns natural, integer, and real v4.1.4 * added redex-check, a tool for automatically generating test cases for Redex specifications. * improved traces for use in generating PostScript: - added traces/ps - added more coloring arguments to traces: #:scheme-colors? #:default-arrow-highlight-color, and #:default-arrow-color - added the #:layout argument to traces - added term-node-set-position! and related term-node functions * Added tracing to metafunctions (see current-traced-metafunctions) * added caching-enabled? parameter (changed how set-cache-size! works) v4.1.2 - added white-bracket-sizing to control how the brackets are typeset when rendering a metafunction. - added render-* functions that make it easier to experiment with typesetting at the REPL. - where clauses in metafunctions now are implicitly in `term's (they were not documented at all before) v4.1 (this is the first version that was included in the PLT distribution. Before this, Redex was in PLaneT). EXTENSIONS: - added test-equal, test-pred, test-reduces, and test-results - removed restriction on apply-reduction-relation* replaced it with additional work while matching non-terminals to remove the redundancy - added `in-domain?' CHANGES: - define-metafunction and co. now use a different syntax. - got rid of named holes. This means, eg, that (hole #f) now matches a two element list, not just the hole directly. - zero occurrences of a hole when matching an `in-hole' now correctly fails. - the `where' keyword in reduction-relation became `with' (and the arguments reversed order) - renamed the `rib' struct to `bind' (and mismatch-rib => mismatch-bind) - merged the various traces functions into a single function that accepts keyword arguments. - renamed the loc-wrapper struct to lw. - language->ps and language->pict's listof-symbols is now optional and thus the language->ps's arguments changed order to make that work. - renamed test-match to redex-match - no long export mtch struct or bindings struct and test-match's result is not simplified. - extend-reduction-relation now uses the names of the rules to replace existing rules (instead of just unioning the rules) - in-hole used to substitute into named holes, but now it only substitutes into unnamed holes. Use in-named-hole on the right-hand side to do the substitution - removed hole-here BUG FIXES: - fixed a (not easily noticed) bug in the way hole matching worked for named holes. - extending a non-terminal that's been defined together with other non-terminals now works as expected. - handling of non-terminals uses that have underscores in them now works properly (only showed up when using them in the definition of a language) - an extended language can now define multiple non-terminals together -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- below here were the versions of Redex that appeared in PLaneT -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- ("robby" "redex.plt" 4 4) - undid some changes that broke backwards compatibility ("robby" "redex.plt" 4 3) - added extend-reduction-relation - fixed a bug whereby reduction relations that reduced to false were always ignored ("robby" "redex.plt" 4 2) - fixed a bug in the way `in-hole' inside an ellipsis on the right-hand side of a reduction rule. ("robby" "redex.plt" 4 1) - improved stepper so that scrolling works when large terms are present. ("robby" "redex.plt" 4 0) - changed conventions for subscripts. Now, non-terminals w/out subscripts bind in reduction rules (but they still do not bind in grammar definitions). - wheres and side-conditions now bind as expected in reduction-rules - fixed a bug in metafunction pict generation (parallel fix from 3.28) - renamed horizontal-arrow-space to arrow-space. - renamed horizontal-label-space to label-space. ("robby" "redex.plt" 3 27) - added horizontal-arrow-space, horizontal-label-space - number & variable now typeset in italics (to match the other non-terminals) - improved fresh variable generation - added `where' for bindings in metafunctions - added 'up-down mode for metafunction typesetting - added optional argument to reduction-relation->pict & reduction-relation->ps - PR 8957 ("robby" "redex.plt" 3 26) - fixed a bug in pict generation ("robby" "redex.plt" 3 25) - added hole-here support for `term' ("robby" "redex.plt" 3 24) - added curly-quotes-for-strings and current-text ("robby" "redex.plt" 3 23) - fixed a bug that cause typesetting of grammars that defined hole as the first production of some non-terminal. - added hide-hole pattern ("robby" "redex.plt" 3 22) - ?? ("robby" "redex.plt" 3 21) - added `where' as a binding form in the individual clauses of a reduction-relation. - typesetting: - improved handling of nested term, quote, unquote, and unquote-splicing. - fixed up in-named-hole and (hole x) to use subscripts. - improved the docs for the loc wrappers to explain logical spacing. - improved typesetting of languages built with extend-language. See extend-language-show-union. - added set-arrow-pict! ("robby" "redex.plt" 3 20) - improved the interface for rewriting aspects of the typesetting. - added linebreaks, with-compound-rewriter, and with-atomic-rewriter ("robby" "redex.plt" 3 19) - improved source locations for error messages when misusing ellipses, eg: (term-let ([(x ...) '(1 2)] [(y ...) '(1 2 3)]) (term ((x y) ...))) or similar things via reduction-relation, metafunctions, etc. - fixed PR 8752: `name' patterns only show the name, leaving the thing defined to the where clause ("robby" "redex.plt" 3 18) - fixed PRS relating to pict generation: 8749 8751 8750 and a few other bugs along the way. ("robby" "redex.plt" 3 17) - initial-char-width now controls both the stepper & traces ("robby" "redex.plt" 3 16) - added define-multi-args-metafunction - finished first pass of the pict generation rewriting ("robby" "redex.plt" 3 15) - fixed a bug in stepper/seed ("robby" "redex.plt" 3 14) - fixed some silly mistakes in the packaging ("robby" "redex.plt" 3 13) - added variable-not-otherwise-mentioned as a new pattern - added stepper/seed - added an optional pretty-printing argument to stepper. - improved the ps rendering of the arrows for --> -> => ==> ~> and ~~> - rewrote internals of pict rendering (hopefully no change yet, but there may be bugs introduced ...). ("robby" "redex.plt" 3 12) - Added pict and .ps generation functions for reduction-relations, metafunctions, and grammars. These are still primitive; the most obvious missing feature is the inability (without secret knowledge) to replace the pink stuff. - fixed a bug in the way the stepper highlights differences in the presence of quote (by disabling the ' shortcuts printing) NOTE this version of redex requires not just any 369.100, but one from 5/19 in the afternoon (or newer). ("robby" "redex.plt" 3 11) - changed the order of the arguments in the new `fresh' clauses introduced in the last release. ("robby" "redex.plt" 3 10) - fixed bugs in the way that ..._x patterns work (they didn't handle binding well). - fixed misc bugs in the stepper - added the ability to generate a sequence of fresh variables in a single rule ("robby" "redex.plt" 3 9) - added side-condition specs to metafunctions - added test-reduces and test-reduces/multiple to schemeunit.ss - fixed a bug in the handling of _!_ - improved the "found the same binder" error message to show the source locations of the two offending binders ("robby" "redex.plt" 3 8) - fixed a bug in the way (hole #f) patterns matched. - fixed a bug in the initial height of the boxes in `traces' - added reduction->relation-names - added ability to step until a particular reduction (and the reduction labels) in the stepper. ("robby" "redex.plt" 3 7) - improved syntax error message (PR 8576) - added difference highlighting for adjacent terms in the stepper ("robby" "redex.plt" 3 6) - added stepper ("robby" "redex.plt" 3 5) - bugfix (I think ... this version's changes seem to have been forgotten) ("robby" "redex.plt" 3 4) - added term-node-children ("robby" "redex.plt" 3 3) - added term-match and term-match/single - added variables-not-in - fixed a bug in metafunctions ("robby" "redex.plt" 3 2) - added language-nts - added better error messages when using parts of the pattern language as ordinary things in the grammar. ("robby" "redex.plt" 3 1) - adds the ability to have multi-colored terms, not just pink ones. ("robby" "redex.plt" 3 0) This release changes the syntax of the reduction relations to make it more consistent and more in line with the way reduction relations are written in papers. This is the precise set of removals and additions: - added extend-language - added reduction-rule & apply-reduction-relation - added union-reduction-relations - added define-language - changed compatible-closure & context-closure so that the pattern argument is not quoted, but is just the pattern in the last argument. - changed term-node-labels so that it can return #f (in the list) when a reduction doesn't have a label. - removed language->predicate, compile-pattern, match-pattern (use test-match instead) - removed reduction, reduction/name, reduction/context, reduction/context/name (use reduction-relation instead) - removed red? (use reduction-relation? instead) - removed reduce (use apply-reduction-relation instead) - removed reduce-all (use apply-reduction-relation* insetad) - removed reduce/tag-with-reduction (use apply-reduction-relation/tag-with-names instead) - removed red-name, reduction->name, give-name - removed language (use define-language instead) - removed helper.ss Other improvements: - check syntax draws arrows for the non-terminals in a `language' now, both to the language and to the reduction rules. ("robby" "redex.plt" 2 6) - added reduce-all and note about bad parsing performance issues. - added `test-match' and note about how to debug redex programs to doc.txt - added redex-specific 'check' functions for use with schemeunit. - add `metafunction' for defining meta functions using the pattern matching notation used in reductions and grammars. ("robby" "redex.plt" 2 5) - fixed bugs in compatible-closure & context-closure ("robby" "redex.plt" 2 4) - reduced the amount of memory used for caching significantly (with some small speedup for a largeish reduction semantics test suite) - added set-cache-size! - added variable-prefix pattern - added ..._ pattern that can be used to ensure matching lengths of repeated patterns. - added _!_ subscripts (both in ... and regular) to ensure that the matched things are different (or have different lengths in the case of ..._!_ subscripts) ("robby" "redex.plt" 2 3) - added the ability to traverse the graph generated by traces in order to decide if a term should be highlighted in red. See the traces/pred documentation for details. - added term-node functions - added red-name function - removed make-plt.ss from archive ("robby" "redex.plt" 2 2) - added a blurb, fixed a typo in the docs. ("robby" "redex.plt" 2 1) - changed the way a contract is specified on the matcher to get a 30% speed up on the beginner test suite. Thanks, Matthew for spotting that! ("robby" "redex.plt" 2 0) - fixed a bug in compatible-closure handling that could result in duplicate matches when there should only have been a single match. - added labels to edges for reductions when shown in GUI. See docs for reduction/name - small performance improvement to matcher (10-20% on non-trivial examples) - added letrec.ss example (and improved some of the examples to use labels) ("robby" "redex.plt" 1 3) - Fixed a bug in the compatible closure function; otherwise the same as 1.1 ("robby" "redex.plt" 1 2) - Obsolete'd version. It used to be a first attempt at the 2.0 revision, but now should be avoided. Use 2.0 instead of this version. ("robby" "redex.plt" 1 1) - fixed packaging error ("robby" "redex.plt" 1 0) - initial release to PLaneT