v8.17
* render-judgment-form and judgment-form->pict are functions, making
them suitable to abstract over (before, they required their
arguments to be identifiers bound to judgment forms)
* fixed the rendering of nonterminals that have both subscripts and primes
v8.16
* bug fixes
v8.15
no changes since 8.14
v8.14
* bug fix
v8.13
* bug fix
v8.12
* documentation improvements
v8.11
* added `redex-define` and `term-define`, thanks to Shu-Hung You
* documentation fixes
v8.10
* added judgment-form->rule-names
* unbreak traces/ps
v8.9
* bug fix
v8.8
* improved typesetting support when customized renders are used in
certain multi-line situations. Thanks to Shu-Hung You for
suggesting the fix.
* fixed more bugs in randomized testing for delimited continuations
v8.7
* fixed bugs in randomized testing for delimited continuations
v8.6
* added support for simultaneous substitutions, thanks to Phil Nguyen
* bug fixes
v8.5
* added the #:error-on-multiple? argument to apply-reduction-relation*
* bug fixes
v8.4
* bug fix
v8.3
* improve the stepper for IO judgment forms
* bug fixes
v8.2
* bug fixes
v8.1
* bug fixes and a documentation improvement
v8.0
* added define-overriding-judgment-form
* improved source location reporting for test- forms
v7.9
* added language-make-::=-pict
* misc bug fixes
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 ..._<id> 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