Commit Graph

754 Commits

Author SHA1 Message Date
Burke Fetscher
4d9cce823b fix docs for redex-generator 2013-05-17 15:26:38 -05:00
Burke Fetscher
d001abc5dd Redex: fix a small bug in the list-machine example 2013-05-16 17:39:25 -05:00
James Swaine
a8d981230c Make sure the Redex pattern language's 'boolean' is rendered as a nonterminal 2013-05-16 16:17:04 -05:00
Robby Findler
f364871e7c Redex docs edits to be more precise about picts (versus just slideshow) 2013-05-16 07:21:11 -05:00
Robby Findler
e768461b72 adjust generate-term docs a little
move the examples into the itemized list and include judgment-form
and enumeration examples
2013-05-16 07:18:24 -05:00
Robby Findler
498815a225 add enum-tests into run-tests.rkt 2013-05-14 07:25:53 -05:00
Max New
e86e47a968 Removed tabs from redex enum code 2013-05-13 21:14:48 -05:00
Max New
d174a0c0a0 Added Redex enum tests 2013-05-13 20:40:50 -05:00
Max New
c31d0e02d4 Hacky fix to only flatten repeats 2013-05-13 20:40:50 -05:00
Max New
943179aab1 Fixed bad let syntax 2013-05-13 20:40:50 -05:00
Robby Findler
9932ef33f7 move the slideshow/pict library to its own collection
also, adjust all of the requires in the tree to point to the pict
collection
2013-05-12 22:07:58 -05:00
Robby Findler
119eab66d8 delay the unimplemented/unsupported errors until the enumeration is actually used 2013-05-09 17:22:58 -05:00
Max New
b8538ec135 Added Redex enumerators.
Supports names and recursive patterns.
Limited support for repeats and mismatches.
2013-05-09 16:32:53 -05:00
Burke Fetscher
172ea13552 redex: fix and clean up metafunction expansion
- defer disequation expansion so that generated code
  is linear w/r/t to the number of clauses
- fix variable renaming for disequations
2013-05-07 15:20:37 -05:00
Robby Findler
49225918d0 add an example use of the #:pp argument to the redex docs 2013-05-07 09:20:32 -05:00
Robby Findler
1e0625bd39 fix tests
The test cases in question never failed for what appears to be
an amazing fluke. I broke these test in Jan of 2012 (commit 2afda360)
and they don't seem to have failed since then, due to luck with
the random number generator
2013-05-07 07:13:58 -05:00
Robby Findler
d8a444dfef misc improvements to generate-term
- there should no longer be an internal errors (hopefully)
  that is, all of the errors with the form should be caught
  and reported properly now
- several of the options in generate-term now generate less code
- the blue box portion of the documentation is now more precise
2013-05-06 18:17:42 -05:00
Robby Findler
e5a84eff8d disable the extra information redex puts for check syntax
... because it results in programs that have different identifiers
with overlapping ranges in the editor, something that check syntax is
not yet prepared to deal with.
2013-05-05 15:43:17 -05:00
Robby Findler
48c719a3ee Refactor Redex so that it tells Check Syntax that non-terminal
references are binding/bound variables (beyond those appearing in the
define-language itself)

Specifically,

- change define-language (and friends) so they record binding and
  source location information for non-terminals in the identifier that
  names the language (and to expand to disappeared bindings);

- change rewrite-side-conditions/check-errs so that it accepts the
  language identifier (instead of a list of non-terminals) and returns
  one extra piece of syntax: that extra piece of syntax is just
  (void), but it has a bunch of disappeared uses on it that connect
  to the identifiers added to define-language;

- similarly, adjust (term ...) so that it puts disappeared uses for
  non-terminal references.
2013-05-05 15:43:16 -05:00
Burke Fetscher
601640c3b1 redex: fix generate-term error messages 2013-05-04 22:03:27 -05:00
Burke Fetscher
66824ec9a9 redex: fix unify coverage tests
expect `_' from match-a-pattern, instead of `else'
2013-05-04 20:22:10 -05:00
Robby Findler
f8e8c42780 more else -> _ conversions 2013-05-04 10:36:42 -05:00
Robby Findler
b9375bc7e3 remove some misleading uses of 'else' from Redex 2013-05-04 09:28:11 -05:00
Robby Findler
0aa8862109 add missing require 2013-05-04 07:52:12 -05:00
Robby Findler
7611e295f4 fix typesetting for empty reduction relations
closes PR 13346
2013-05-01 17:37:22 -05:00
John Clements
df319c2ee8 fixing error message in rewrite-side-conditions.rkt 2013-05-01 09:02:33 -07:00
Robby Findler
c9045abf4d add stub for enumeration support to Redex 2013-05-01 10:46:11 -05:00
Burke Fetscher
2ebc200d3d redex: unfold nts once during unification
Also:
* add a backtracking limit
* check for ground terms in both term and pat environments
  when filling in generated patterns
* update tests to be consistent with the above
2013-04-23 13:26:15 -05:00
Burke Fetscher
67daa276ff Remove uses of else in match.
Also, a few micellaneous fixes for the prototype trace browser
2013-04-15 18:17:57 -05:00
Burke Fetscher
41d90c6dd5 redex: syntax error fix for define-relation
please merge to the release branch
2013-04-11 22:34:29 -05:00
Burke Fetscher
3feb6cf039 add a consistency check on the final environment
Specifically, check that fully instantiated terms
with cstrs on them satisfy those cstrs.
2013-04-10 16:13:45 -05:00
Burke Fetscher
468d2b192e redex: elminate another #f/failure confusion 2013-04-10 12:59:15 -05:00
Burke Fetscher
495e5c94cf redex: bug fix for gerating terms including #f
please include in the release
2013-04-08 15:03:01 -05:00
Burke Fetscher
a97ff69cd0 test-equal->test for better drdr source loc info 2013-04-06 15:20:15 -05:00
Burke Fetscher
d00099dbdb Redex: pass language id through for term errors 2013-04-04 22:59:14 -05:00
Burke Fetscher
4410ecceb2 Redex: fix term-let/#:lang keyword interaction
Account for the fact that define-language bindings may get
shadowed by term-let when using the same identifier as the language.
2013-04-04 20:38:08 -05:00
Robby Findler
5a85af78ac add contracts to the "with-" macros in redex/pict 2013-04-01 22:39:21 -05:00
Robby Findler
06315bf0fa syntax error check fix
closes PR 13639
2013-03-29 11:58:52 -05:00
Burke Fetscher
fe0fd0d152 Redex: remove some now extraneous code 2013-03-22 16:14:03 -05:00
Burke Fetscher
ddf4945125 Redex: corrections for disequations in generator
- handle parameters correctly when simplifying disequations
- rework term generation/disequation checking for parameters
- fix define-extended-metafunction w/r/t the above
2013-03-22 15:28:36 -05:00
Burke Fetscher
40fc96cacf Redex: rework metafunction compilation/search for parameters 2013-03-22 15:28:35 -05:00
Burke Fetscher
bdf1866e80 Redex: parameterized disequations
refactor the pattern unifier and tests to handle
disequations with parameters correctly
2013-03-22 15:28:35 -05:00
Robby Findler
6c2ea3acbb add missing provides 2013-03-19 14:08:28 -05:00
Robby Findler
06696d67b4 add a #:pre keyword to define-metafunction
The keyword allows the specification of contracts
that relate different arguments

closes PR 13617
2013-03-18 12:54:27 -05:00
Robby Findler
1e910fcfbc make check-metafunction and check-reduction-relation
pay attention to the contract/#:domain spec

closes PR 13616
2013-03-17 20:50:23 -05:00
Robby Findler
b63aa6bbac adjust commit 99ff0adbfd to
be more friendly to the test suites
2013-03-17 20:50:22 -05:00
Robby Findler
4bfd6ff6e3 document define-metafunction's contract patterns properly
closes PR 13613
2013-03-17 09:47:42 -05:00
Robby Findler
0dd7d8f60b adjust docs for check-metafunction to make the example
use more representative

closes PR 13614
2013-03-17 09:47:42 -05:00
Robby Findler
99ff0adbfd check errors earlier in judgment-form
closes PR 13609
closes PR 13610
2013-03-16 21:32:14 -05:00
Robby Findler
a50dfcc670 add a test for drdr's consumption to keep the ryr models in sync 2013-03-16 11:20:44 -05:00