Robby Findler
e788c6f49e
adjust define-judgment-form so that it
...
a) avoids creating big intermediate lists of the same things over and over
(this closes PR 12380)
b) generates less code (by generating calls to local functions)
c) normalizes its output (sorts by the printed representation)
2011-11-20 22:50:07 -06:00
Robby Findler
0a75219438
added support for where & side-condition & judgment-holds to define-relation
...
closes PR 12382
2011-11-20 21:34:22 -06:00
Robby Findler
b93486ed69
compile the left-hand sides of define-judgment only once, not during each time we try to check a judgment
...
related to PR 12380
2011-11-17 20:55:05 -06:00
Robby Findler
755dc28e55
Fixes define-relation's handling of ellipses across clauses
...
closes PR 12378
2011-11-17 17:00:11 -06:00
Robby Findler
3379fb8df6
fix some redex bugs caught by drdr tests
2011-11-09 06:47:38 -06:00
Robby Findler
0ce6c75591
Rackety (mostly letrec-values => define and minimizing dependencies)
2011-10-31 09:14:34 -05:00
Robby Findler
64dfdb3c7f
Change the expansion of reduction-relation so that it generates less code
...
(by expanding into a call to a 30 or so line procedure, instead of putting
that code directly into the result of the macro).
This produces about a 6x speedup on this reduction-relation
(reduction-relation L (--> 0 1) (--> 1 2) ... (--> 99 100))
where L is
(define-language L)
The time it takes to run "racket r6rs.rkt" in the shell from the
directory collects/redex/examples/r6rs speeds up by about 10% (15%
with errortrace enabled), in the case where all .zo files are built,
except the ones in the r6rs directory. (Also worth noting that "racket
-l redex" takes more than 50% of that time.) And the change has no
noticeable effect on the time it takes to run r6rs-test.rkt.
2011-10-31 08:53:09 -05:00
Robby Findler
41f68af64a
delay the construction of the compatible-closure grammar (the 'cross' thing)
...
until it is actually used. (This can make a big difference for large grammars
in models that don't actually use the compatible closure stuff.)
2011-10-30 22:36:53 -05:00
Robby Findler
9d371153fd
add the #:stop-when argument to apply-reduction-relation*
2011-10-23 12:10:56 -05:00
Casey Klein
57a8ed5c79
Fixes matching of prefab struct literals
...
Fixes PR 12298
2011-10-17 19:37:16 -05:00
Robby Findler
9ab6a93127
fix the error check
...
closes PR 12290
2011-10-15 14:00:16 -05:00
Robby Findler
db2e13a09b
add a "Step Until Choice" option into the redex stepper
2011-10-14 13:37:12 -05:00
Robby Findler
a43973157b
add call to 'test-results'
2011-10-12 20:46:20 -05:00
Ryan Culpepper
7cc1476170
syntax/parse: fix bug: integrated stxclass might not bind pvar to syntax
2011-09-21 16:58:52 -06:00
Casey Klein
83451fea98
Add evaluation contexts for by-need letrec calculus as an example
2011-09-19 12:20:45 -05:00
Eli Barzilay
16cd1ad78d
Make `defproc' throw an error if two arguments have the same name.
...
Related to the already fixed PR 12114 and PR 12133, which motivated the
error, and a few additional typos of the same kind.
(Note that it uses the symbols, but that's how they'll render anyway.)
2011-09-16 11:14:18 -04:00
Casey Klein
9944e6b3f6
Adds missing test image
2011-09-08 10:43:23 -05:00
Casey Klein
634f5c9e0c
Removes now outdated comment
2011-09-08 09:11:52 -05:00
Casey Klein
97e792200f
Gives a function a better name
2011-09-08 09:11:52 -05:00
Casey Klein
6d43376f9c
Adds support for `judgment-holds' clauses in metafunctions
2011-09-08 09:11:52 -05:00
Casey Klein
ac7856a377
Moves metafunction construction to later expansion step
2011-09-08 09:11:51 -05:00
Casey Klein
2b4f604776
Replaces use of `define-syntax-set'
2011-09-08 09:11:51 -05:00
Casey Klein
145828527f
Fixes handling of pattern variables that look like metafunctions
2011-08-31 11:20:02 -05:00
Casey Klein
ecdd50da09
Tests defined-checks directly
2011-08-30 15:10:50 -05:00
Casey Klein
c25c0b2868
Deletes duplicate tests
2011-08-30 15:10:50 -05:00
Casey Klein
c0625dc30c
Adds define-term form
2011-08-30 15:10:50 -05:00
Eli Barzilay
1db5ad97f8
Fix another bunch of "language" typos.
2011-08-26 05:26:46 -04:00
Casey Klein
2eced78000
Fixes indentation
2011-08-17 11:59:43 -05:00
Casey Klein
cee4566ed4
Makes test work when compilation strips source locations
2011-08-16 19:18:18 -05:00
Casey Klein
e485e9f348
Tests define-judgment-form and metafunction renaming
...
Closes PR 11469
2011-08-16 14:32:34 -05:00
Casey Klein
9e2e11e9c4
Tests metafunction Check Syntax arrows
2011-08-16 14:32:33 -05:00
Casey Klein
efa04066c6
Tests define-judgment-form's Check Syntax interaction
2011-08-16 14:32:33 -05:00
Casey Klein
a0f2db7574
Drops `traces' call to make the file DrDr-friendly
2011-08-15 12:46:14 -05:00
Casey Klein
98eaaebc65
Improves error messages for Redex definition forms
2011-08-15 12:46:14 -05:00
Eli Barzilay
d61eb53686
Lots of documentation formatting.
...
Started as fixing misindented definitions, then more indentations, then
a bunch of similar things (square brackets, huge spaces at end-of-lines,
etc).
2011-08-15 07:50:04 -04:00
Casey Klein
cd1281fa65
Changes example from arithmetic to pairs
2011-08-12 04:33:38 -05:00
Casey Klein
66be55215a
Fixes Redex doc's links to examples
2011-08-10 15:20:13 -05:00
Casey Klein
4d1651645a
Improves error message for premise typos
2011-08-10 12:24:02 -05:00
Casey Klein
a2dc2d9540
Fixes arity checks outside define-judgment-form
2011-08-10 12:24:02 -05:00
Casey Klein
d66c48ecf7
Updates STLC example to use define-judgment-form
2011-08-10 12:24:01 -05:00
Casey Klein
87f3541979
Adds support for ellipsis-repeated premises
2011-08-10 12:24:01 -05:00
Casey Klein
f803f187bd
Adds bigger define-judgment-form examples
2011-08-10 12:24:01 -05:00
Casey Klein
31ec46170d
Adds STLC example to README
2011-08-10 12:24:01 -05:00
Casey Klein
88cd7cd303
Adds with-compound-rewriters typesetting form
2011-08-10 12:24:00 -05:00
Casey Klein
29ffea3b76
Uses examples' in explanation of judgment form
where' clauses
2011-08-10 12:24:00 -05:00
Casey Klein
d2a58bc05f
Restores the explanation of define-relation contracts.
2011-08-10 12:24:00 -05:00
Casey Klein
52c50dd67e
Adds an alternative syntax for define-judgment-form rules
...
The conclusion may come last instead of first when a sequence of
dashes precedes it.
2011-08-10 12:24:00 -05:00
Casey Klein
dbfbf59256
Changes syntax for define-judgment-form mode and contract specs
2011-08-10 12:23:59 -05:00
Casey Klein
d58a743b89
Fixes define-judgment-form at the top-level with errortrace enabled
2011-08-10 12:23:59 -05:00
Casey Klein
576272362b
Adds define-judgment-form form
2011-08-05 07:19:23 -05:00