in-hole within #:refers-to causes contract violation

[MichaelBurge]

The intention of this program is for the scope of a define to be its entire surrounding context.

#lang racket

(require redex/reduction-semantics)

(define-language L
  [ x ::= variable-not-otherwise-mentioned]
  [ e ::= x natural ]
  [ s ::= (begin s ...) (define x e) e]
  [ S ::= hole (begin s ... S s ...)]
  #:binding-forms
  (in-hole S (define x e) #:refers-to x)
  )

(default-language L)

(test-equal (term (define foo 5))
            (term (define bar 5)))

(test-equal (term (begin (define foo 5)
                         (define bar 10)
                         bar
                         foo
                         ))
            (term (begin (define bar 5)
                         (define baz 10)
                         baz
                         bar)))

I'm not sure what I expected the semantics of this to be, but the error message should at least be different:

car: contract violation
  expected: pair?
  given: 5
  context...:
   /home/mburge/work/vendor/redex/redex-lib/redex/private/binding-forms.rkt:654:4: loop
   [repeats 4 more times]
   /home/mburge/work/vendor/redex/redex-lib/redex/private/binding-forms.rkt:651:0: rec-freshen-spec
   /home/mburge/work/vendor/redex/redex-lib/redex/private/binding-forms.rkt:184:0: canonicalize
   /home/mburge/work/vendor/redex/redex-lib/redex/private/binding-forms.rkt:152:0: α-equal?
   /home/mburge/work/vendor/redex/redex-lib/redex/private/reduction-semantics.rkt:3165:0: test-equal/proc
   "/home/mburge/work/tmp/a.rkt": [running body]
   for-loop
   run-module-instance!125
   perform-require!78

[MichaelBurge]

This variation also gives a weird error:

(define-language L
  [ x ::= variable-not-otherwise-mentioned]
  [ e ::= x natural ]
  [ s ::= (begin s ...) (define x e) e]
  [ s-no-define ::= (begin s ...) e]
  [ S ::= hole (begin s ... S s ...)]
  #:binding-forms
  (define x e_2) #:refers-to x
  (begin (define x e_2) #:...bind (defines x (shadow defines x)) s #:refers-to defines ...)
  )

I believe an ambiguous match within the begin binding form causes this error:

match: no matching clause for (list (mtch (bindings (list (bind '..._r3 0) (bind 'x '()) (bind 'e_2 '()) (bind 's '(#0=(define foo 5) #1=(define bar 10))))) '(begin #0# #1#) #<none>) (mtch (bindings (list (bind '..._r3 1) (bind 'x '(foo)) (bind 'e_2 '(5)) (bind 's '(#1#)))) '(begin ...

[rfindler]

Thanks for this (and for the other issues)!

I'll try to get to these as soon as I can, but it may be a little while before I really have the time. Apologies.

[rfindler]

In fixing #171, I made the original program in this issue be a syntax error.

In order to do what you want here, you need to use the binding form's language to bubble out the variable to the surrounding context (using the #:exports keyword).

More generally, in-hole lets you write patterns where the choice of variable to be the binder is ambiguous, and I can't really see a way clear to make sense of that, which is why it was disallowed.

[rfindler]

And I believe the fix to #171 fixed the problem in the second example.