Commit Graph

480 Commits

Author SHA1 Message Date
Burke Fetscher
44dd4acb44 Additional random test generation capability for Redex.
This adds the option to generate random terms that satisfy
judgment-forms and metafunctions.

Currently functionality does not include:
- patterns/terms using: ellipses, in-hole/hole and relatives, side-conditions, unquotes
- define-relation
- redex-check integration
2012-10-17 16:30:51 -05:00
Robby Findler
751dcb4bd1 adjust define-judgment-form's typesetting so that it
tracks the lines of the premises in the source when
deciding how to linebreak the premises of the typeest form
2012-10-09 09:06:09 -05:00
Robby Findler
d6a8ac85b4 added some pretty-print using term formatters and fixed the
docs for term->pict.

closes PR 13150
2012-10-01 23:27:48 -05:00
Robby Findler
d0f981f9cb fix a bug in color padding code
closes PR 13153
2012-10-01 22:53:58 -05:00
Robby Findler
9b0eb1ab78 fix redex pdf generation when a string is passed 2012-09-25 15:32:38 -05:00
Robby Findler
0e7688349e add syntax error check when the arrow in a reduction
relation isn't just an identifier

add a syntax error check when an identifier appears
under two different ellipses depths in the same pattern
2012-09-20 07:09:17 -05:00
Robby Findler
b8acee5655 small cleanup 2012-09-12 15:41:37 -05:00
Robby Findler
605e1b8c89 adjust redex so that identifiers preserve their syntax-original ness 2012-08-24 09:47:18 -05:00
Robby Findler
40e5b63bbc allow identifiers as names, not just strings 2012-08-09 15:28:42 -05:00
Robby Findler
97e3f56bf2 adjust bitmap tests to test judgment form labels (and fix expected result under mac os x) 2012-08-08 22:05:43 -05:00
Robby Findler
0369342bfe added names to clauses in define-judgment-form and added
judgment-form-cases to use the names to control typesetting
2012-08-08 21:34:28 -05:00
Burke Fetscher
29661cc675 add #:lang keyword to term, which checks that underscored symbols agree with patterns in the provided language...changed most internal uses of term to use this form 2012-08-08 11:09:01 -05:00
Matthew Flatt
0dbd3f1610 redex typesetting: make token splitter more tolerant
Possibily the typesetting enginer should reject an ill-formed
input, instead; I'm not sure what went wrong with the input.
2012-05-04 10:20:24 -06:00
Robby Findler
676f744c1d add 'match-pattern?' 2012-03-27 12:21:17 -05:00
Jay McCarthy
99f1cc44df redex-match violates its documented contract
This patch fixes the problem that the hole matcher may return an empty
list rather than a #f that gets sent to the caller of redex-match. I
re-ran the Redex tests and found no violations. However, I am not
confident that there isn't a more correct place to put this '() -> #f
replacement.

I will be immediately forwarding this push email to Robby to have him
check it.
2012-03-23 06:39:14 -06:00
Robby Findler
9d43203990 adjusted the render-* functions so they produce .pdf if the given
filename ends with #rx#"[.]pdf".
2012-03-17 08:36:34 -05:00
Robby Findler
4a304643d3 Rackety 2012-03-05 08:12:02 -06:00
Robby Findler
b7caf411ae added define-extended-judgment-form to Redex 2012-03-03 16:41:53 -06:00
Robby Findler
a0bb0430f2 separated the define-judgment-form implementation (and bind-withs)
into its own file
2012-03-03 16:41:52 -06:00
Robby Findler
a23f6dbca2 move the redex scrbl files into a scribblings subcollection and adjust timeouts 2012-02-29 07:13:36 -06:00
Eli Barzilay
f7c67b49a4 Big newline at EOF scan. 2012-02-29 00:28:11 -05:00
Robby Findler
c5193f7da7 fix a bug in define-union-language
(this bug was somehow already covered by the existing test suites
 and also make pretty much every define-union-language break)
2012-02-27 10:00:23 -06:00
Robby Findler
1945ff2709 add make-platform-bitmap
also: use it in pict's rendering and
remove redex's platform-specific font choice
(going back to using 'modern on all platforms)

closes PR 12554
2012-02-21 16:19:45 -06:00
Eli Barzilay
c007c345f9 A bunch of more typos like the ones in David's commit. 2012-02-21 14:21:43 -05:00
Robby Findler
df5e7efd5e Made an editing pass over the redex tutorial 2012-02-15 08:29:22 -06:00
Robby Findler
e4e4d70b6b added define-union-language 2012-02-10 17:10:47 -06:00
Robby Findler
b93ff24fee add two links to redex docs 2012-02-10 17:10:47 -06:00
Robby Findler
b3a9ae9ba2 change the font in the pink highlighting to avoid some
bad drawing behavior on the mac (that shows up in the
amb tutorial)
2012-02-08 16:23:13 -06:00
Robby Findler
55b3d99d78 adjust beaucoup places in redex where the source was being
included in the compiled files. (also, misc minor cleanups
notably a new exercise in tut.scrbl)

closes PR 12547 --- there are still a few uses left, but they do not
seem to be coming from Redex proper:

 - /Users/robby/git/plt/collects/racket/private/map.rkt still appears
   in a bunch of places (there is a separate PR for that I believe),
   and

 - /Users/robby/git/plt/collects/redex/../private/reduction-semantics.rkt
   appears in tl-test.rkt, but I do not see how it
   is coming in via Redex code, so hopefully one of the other
   PRs that Eli submitted is the real cause. If not, I'll revisit later
2012-02-08 09:59:44 -06:00
Robby Findler
4bac243efe put an expression to evaluate to find the path instead of the path
that was there when the html file was built.

closes PR 12545 (I do not agree with Eli's proposal for fixing this so I
did it differently)
2012-02-07 16:14:09 -06:00
Robby Findler
2ca0473f1c shrink longest line down to something more reasonable 2012-02-07 15:50:53 -06:00
Robby Findler
794240bf67 added a amb-based redex tutorial 2012-02-05 17:24:13 -06:00
Robby Findler
8bec634dcd adjust covered-cases so that it always returns deterministically
(sorting by the strings in the result)
2012-02-05 17:24:13 -06:00
Robby Findler
977659a118 fix redex's syntax pruning to not drop the #%top binding 2012-02-01 20:09:29 -06:00
Robby Findler
7cf563c4d9 fix some typos in a comment 2012-01-24 08:29:09 -06:00
Robby Findler
71595a55e6 adjust the names of the dot/neato binaries to be platform-specific 2012-01-17 12:42:42 -06:00
Robby Findler
b068d9583c Remove accidentally pushed commits
For the curious, this was an attempt to change the way context
matching works.  Currently, when matching a pattern, if 'hole' is
encountered, the match succeeds and the result just includes the term
at that point. This means that when matching (in-hole p1 p2), p1
generally returns multiple results and then those results are thinned
out by matching p2 against the thing actually at the hole.

Instead, one could pass along the function that does the matching and
then, when matching a hole pattern, it could decide right at that
point whether or not the match works.

This seems like it would be a win overall, but it interferes with
caching. Specifically, most reduction systems have lots of rules
that all begin

  (--> (in-hole E ...) ...)

and, in the strategy first described above, that matching can be cached.

But in the second, it cannot. Overall, this turns out to be a slight
lose in the current version of Redex. Maybe if other things change, however,
this tradeoff will change.

Revert "IN PROGRESS: more context speedup attempt"

This reverts commit 0134b8753d.

Revert "IN PROGRESS: a possible speed up attempt; match the thing in the hole before returning the context matches instead of afterwards"

This reverts commit 11059e2b5c.
2012-01-15 21:02:48 -06:00
Robby Findler
262931bb80 adjust typesetting so the ellipsis uses the default style, not
literal-style (unless an atomic-rewriter is in place)
2012-01-14 21:32:16 -06:00
Robby Findler
b3c450ffc9 add 'side-condition' to define-judgment-form (it does not have an implicit
unquote like the other side-condition's do, but it is still useful
for typesetting purposes)
2012-01-14 14:52:07 -06:00
Robby Findler
0134b8753d IN PROGRESS: more context speedup attempt 2012-01-11 13:16:47 -06:00
Robby Findler
11059e2b5c IN PROGRESS: a possible speed up attempt; match the thing in the hole before returning the context matches instead of afterwards 2012-01-11 13:16:46 -06:00
Robby Findler
f1a7864c63 fix bug in lw struct generation 2012-01-09 20:38:51 -06:00
Robby Findler
6cacd57ebc add check-redundancy, a parameter that causes redex to print some
debugging information about ambiguous matching (when the ambiguity
matters)
2012-01-09 12:57:24 -06:00
Robby Findler
a12df9cea6 redex: misc cleanups:
- remove cache instrumentation code
 - make hole->not-hole parsimonous
 - change the cache size back to 63
2012-01-09 12:57:23 -06:00
Robby Findler
4fab7f76af tweak the compiled representation of lw structs so they take less space
this shrinks the size of redex/examples/r6rs/r6rs.rkt's .zo file by about 25%
2012-01-09 12:57:21 -06:00
Robby Findler
2afda360d0 redex: adjust the test suites to clean up a few things; also make the
hole and the-not-hole equal? to each other (like they used to be)
2012-01-09 12:57:20 -06:00
Robby Findler
93c21e34de added a cycle check to define-language so grammars like this one:
(define-language L
     (e e))

are rejected as syntax errors
2012-01-09 12:57:19 -06:00
Robby Findler
fbed2d5af7 remove (broken) attempt at optimization Jay suggested
also clean up some test cases that I wasn't sure about earlier
2012-01-08 12:13:37 -06:00
Robby Findler
0459e4fbcd redex: when there are no duplicate names in a pattern, don't do the
same-name-same-bindings check

this seems to speed up the r6rs test suite by about 12% and the
lambdajs benchmark by about 25%
2012-01-08 12:13:36 -06:00
Robby Findler
ddecad0575 redex: adjust the way metafunction tracing is printed so you
don't see (list 'lambda (list 'x) 'x) but instead (lambda (x) x)
2012-01-08 12:13:36 -06:00
Robby Findler
160fcacad6 redex: fix bug introduced in recent optimization attempts 2012-01-02 22:21:21 -06:00
Robby Findler
83758881c3 Don't attempt to drop duplicates in the non-terminal case
This speeds up the lambdajs model considerably because the computation
to determine duplicates is expensive and no duplicates are really
ever dropped (and, in general, I think that duplicates will only
be dropped when the grammar is ambiguous; so maybe a better thing
is to just rewrite the grammar when that happens)
2012-01-02 10:08:34 -06:00
Robby Findler
6bf42855b8 adjust plug to be parsimonious and actually shortcircuit
when one hole has been found

This improves the lambdajs model example's running time, presumably
because the hole is generally found near the "beginning" of the
term
2012-01-02 10:08:33 -06:00
Robby Findler
5dcbedc768 redex: adjust the caching strategy
Instead of using a hash-table, use the equal-hash-code directly;
this lets me evict entries only when they clobber each other,
and generally keep good cache utilization.

Also, cut the cache size by a factor of 5 while still having a
slight performance improvement on the r6rs test suite benchmark.
On that same benchmark, there are 1714812 misses in the cache, but
only 3485 times is an entry in the cache clobbered
2012-01-02 10:08:31 -06:00
Robby Findler
a6a01fd7b8 redex: fix arity-1 cache key computation 2012-01-02 10:08:31 -06:00
Robby Findler
a7a70cbca9 redex: improved the definitely-not-list definitely-not-non-list
computation to be more accurate
2012-01-02 10:08:30 -06:00
Robby Findler
fe1df742b3 Tried to improve redex by detecting when a pattern does not
have any holes, hide-holes, or names and, in that case, just
combining booleans instead of building of mtch structs.

This does seem to work on a simple benchmark. The code below
gets about 6x faster. But on the r6rs test suite, there is
no substantial change (possibly because the caching obviates
this optimization?)

lang racket/base
(require redex/reduction-semantics)
(caching-enabled? #f)
(define-language L (e (+ e e) number))
(define t
  (let loop ([n 100])
    (cond
      [(zero? n) 1]
      [else `(+ 11 ,(loop (- n 1)))])))
(define f (redex-match L e))
(time (for ([x (in-range 1000)]) (f t)))
2012-01-02 10:08:29 -06:00
Robby Findler
6f97a3a783 disable attempt at Jay's optimization
When I enabled this, I don't see any speedup, on the R6RS test suite
benchmark (I see minor slowdown). Here are the numbers I get, on my
laptop:

   nt cache:  35537 msec
    neither: 844933 msec
 Jay's idea: 875306 msec

And with both on, I see a similar, minor slowdown (as compared to the
version with the nt cache).

The main difference seems to be that I'm getting about 6 "hits" per
test case on the nt-match structs (that is, I avoid work by finding an
nt-match struct) and I'm getting about 8,800 hits in the cache per
test case.
2012-01-02 10:08:29 -06:00
Robby Findler
424a535cf4 first attempt at Jay's optimization for redex
(only did enough to get the r6rs tests running)
2012-01-02 10:08:28 -06:00
Robby Findler
4c86e2fe86 redex: memoize only the non-terminal patterns
remarkably, this seems to cut the time for running
the r6rs test suite in about 1/2
2011-12-29 11:01:21 -06:00
Robby Findler
57f51cf5c8 redex: use predicate/c instead of (-> any/c boolean?)
and a few other, minor changes
2011-12-29 10:58:26 -06:00
Robby Findler
d6ce2b61bc redex: inline lookup-binding 2011-12-29 10:32:02 -06:00
Robby Findler
9bcb86eb0c redex: minor cleanup 2011-12-29 10:15:52 -06:00
Robby Findler
5b2d378a77 fixed a bug in recent Redex internal pattern rewrite
(discovered by the random testing done for the racket machine model)
2011-12-28 23:52:56 -06:00
Robby Findler
f1bacffbdc Adjusted rewrite-side-condition/check-errs so that it normalizes the internal
redex patterns a bunch:

- repeats are turned into wrappers in sequences,
- names are all explicit,
- non-terminals are wrapped with `nt',
- cross patterns always have the hyphens in them.
- ellipses names are normalized (so there are no "hidden"
  name equalities); this also means that repeat patterns
  can have both a regular name and a mismatch name

Also, added a match-a-pattern helper macro that checks to make sure
that functions that process patterns don't miss any cases
2011-12-28 09:46:43 -06:00
Robby Findler
a88d9ca116 missed a place to add an undatum 2011-12-15 08:44:39 -06:00
Robby Findler
c91d004729 more cleanup of the rendering for the case when (format "~s" x)
and (format "~a" x) are different (when 'x' is a symbol)
2011-12-15 08:44:39 -06:00
Matthew Flatt
25dd8727cb add datum-case', etc. as syntax/datum'
This library is used by Redex, which wants a `syntax'-like template
language, but for datum values instead of syntax objects. Using
`datum-case' and `datum' generates much less code. Redex uses
only a small part of the general functionality, so adding
`syntax/datum' could be overkill. It's implemented by generalizing
the `syntax-case' and `syntax' pattern matching and template
constructing code, though; it's not a lot of extra code, and it's
easiest to generalize completely. We may find other uses for
datum templates, too.
2011-12-12 08:13:20 -07:00
Robby Findler
622bec0719 avoid (format "~s" x) in favor of (symbol->string x) for symbols
when doing typesetting stuff in Redex, as the former seems to have
some kind of context dependency that makes it insert ||s around
some upper-case symbols sometimes
2011-12-10 02:55:47 -06:00
Robby Findler
e55ed2dc25 improve syntax error reporting for judgment-holds in reduction relations (and
probably elsewhere)
2011-12-08 20:35:46 -06:00
Robby Findler
447bd44a0c minor rackety 2011-12-05 01:14:54 -06:00
Robby Findler
f725066bf9 fix bug in the handling of side-conditions 2011-12-05 01:14:54 -06:00
Robby Findler
ce7523f01f more atoms can be shared now, so wrap 'em up 2011-12-02 16:38:56 -06:00
Robby Findler
458e2c2282 some long overdue Rackety: renaming the 'scheme:' exports of the framework to 'racket:' 2011-11-30 06:45:50 -06:00
Robby Findler
9db206b231 add in keymap mixin 2011-11-29 18:43:37 -06:00
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
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
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
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
9e2e11e9c4 Tests metafunction Check Syntax arrows 2011-08-16 14:32:33 -05:00
Casey Klein
98eaaebc65 Improves error messages for Redex definition forms 2011-08-15 12:46:14 -05:00
Casey Klein
4d1651645a Improves error message for premise typos 2011-08-10 12:24:02 -05:00