racket / redex

Other
93 stars 36 forks source link

context well-formedness checking doesn't work when ellipses are nested #225

Closed rfindler closed 4 years ago

rfindler commented 4 years ago

The code below doesn't signal a syntax error, but it should. When the two + lines are swapped in the definition of C, an error is correctly signalled.

Bug identified by @mfelleisen.

#lang racket
(require redex/reduction-semantics)

(define-language L
  (e ::= number (+ e ...))
  (C ::=
     hole
     (+ (+ C ...) ...) ;; not correctly identified as a problem
     ; (+ C ...) ;; correctly identified as a problem
     ))

(redex-match L (in-hole C 1) (term (+ 1 2)))