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.
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
- handle parameters correctly when simplifying disequations
- rework term generation/disequation checking for parameters
- fix define-extended-metafunction w/r/t the above
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
