cope with a possible ambiguity while parsing binding form patterns

closes #171

Author: rfindler

redex-lib/redex/private/binding-forms-compiler.rkt

@@ -297,7 +297,13 @@
               [rest-of-body ;; no imports or ...s
                (process-under #'rest-of-body #f #f)]))]
 
-         [atomic-pattern (values (syntax-e #'atomic-pattern) #'atomic-pattern)])))
+         [atomic-pattern
+          (begin
+            (when (equal? (syntax-e #'atomic-pattern) 'in-hole)
+              (raise-syntax-error 'define-language
+                                  "`in-hole` is illegal in a binding specification"
+                                  #'atomic-pattern))
+            (values (syntax-e #'atomic-pattern) #'atomic-pattern))])))
 
    (define import-names (names-imported-in-with-depths bspec-body form-name s-body))
    (define export-names (names-mentioned-in-beta-with-depths export-beta form-name s-body))

redex-lib/redex/private/binding-forms.rkt

@@ -236,7 +236,12 @@ to traverse the whole value at once, rather than one binding form at a time.
           (match match-res
             [#f (loop rest)]
             ;; "bindings" is what the rest of Redex calls what we call "red-match"
-            [`(,m) 
+            [(cons m _)
+             ;; we ignore the rest position because there should be no way to get
+             ;; information there that isn't redundant with what's in the first
+             ;; position. I belive the only way to even get a tail is to have an
+             ;; ambiguous match via context decomposition, but even then the bindings
+             ;; should all be the same, so we can safely take the first one. I hope.
              (when (binding-forms-opened?)
                    (set-box! (binding-forms-opened?) #t))
              (fn (splay-all-...binds (bindings-table (mtch-bindings m)) bspec)

redex-test/redex/tests/binding-forms-test.rkt

@@ -757,3 +757,18 @@
       (λ (x_1) e #:refers-to x_1))
     (check-equal? (term (substitute (x y) x y) #:lang L)
                   (term (y y))))
+
+
+(let ()
+  (define-language L
+    (e ::= (ζ (hide-hole E)))
+    (x ::= variable-not-otherwise-mentioned)
+    (E ::= hole (in-hole (natural E) E))
+    #:binding-forms
+    (ξ x e_1 #:refers-to x))
+
+  (check-true (pair?
+               (redex-match
+                L
+                (ξ x e)
+                (term (ξ x (ζ (1 (2 hole)))))))))