Spencer Florence

`variable-not-in` uses wrong prefix when prefix ends in a number

1

`(variable-not-in 'S3 'S3)` Gives back `S1`, rather than `S31`. While this still does give back unique identifiers it can make the output harder to read in some cases.

Consider: ``` #lang racket (require redex/reduction-semantics) (define-language L) (define-metafunction L [(test any) #f (where/error 1 any)]) (term (test 2)) ``` Which gives the error message `define-metafunction: where/error did not match`....

Sometimes the argument to `#:prepare` will return a term that doesn't match the input pattern, which causes generation to fail. Usually, for me at least, this is an error. Ideally...

the program ``` #lang racket (require redex/reduction-semantics) (define-language L (b ::= a)) ((generate-term L (cross b_1)) 1) ``` Gives the error ``` redex/private/rg.rkt:182:2: hash-ref: no value found for key key:...

`render-reduction-relation` can't render all rules in an extended reduction relation

1

The program ``` #lang racket (require redex/reduction-semantics redex/pict) (define-language L) (define R1 (reduction-relation L (--> number number numbers))) (define R2 (extend-reduction-relation R1 L (--> string string strings))) (parameterize ([render-reduction-relation-rules '(numbers...

check syntax doesn't consider extensions to non-terminals as uses

3

In the program ``` #lang racket (require redex) (define-language a (on ::= 1)) (define-extended-language b a (on ::= .... (- 2 1))) (redex-match? b on (- 2 1)) ``` if...

In the program: ``` #lang racket (require redex) (define-language L) (redex-check L natural (number? (term natural)) #:prepare (lambda _ 'x)) ``` Produces `redex-check: no counterexamples in 1000 attempts`. I would...

`redex-check` doesn't warn about ellipsis in judgment-forms more than one level deep

1

``` racket #lang racket (require redex/reduction-semantics) (define-language simple-plus (M (e e)) (e natural)) (define-judgment-form simple-plus #:mode (okay1 I I) [ -------- (okay1 M (e ...))]) (define-judgment-form simple-plus #:mode (okay I)...

in ASL `(void)` doesn't print as `(void)`

10

This also manifests itself (I think) as `when`s not printing anything. Example: ``` > (void) > (when false (void)) > (when true (void)) > (define x 0) > (when true...

tracing+define-struct causes `syntax-original?` error

1

In ISL+ enable if tracing is enabled in the language menu then this program: ``` (define-struct test (field)) ``` results in the error `syntax-original?: expects a syntax, given '...signature-syntax.rkt:56:42`