more fixing redex / undefined interactions

pkgs/redex-pkgs/redex-lib/redex/private/defined-checks.rkt

@@ -1,14 +1,7 @@
 #lang racket/base
 
-(require "error.rkt"
+(require "error.rkt")
-         racket/undefined)
+(provide check-defined-module)
-(provide check-defined-lexical
-         check-defined-module)
-
-(define (check-defined-lexical value name desc)
-  ;; Needed?
-  (when (eq? undefined value)
-    (report-undefined name desc)))
 
 (define (check-defined-module thunk name desc)
   (with-handlers ([exn:fail:contract:variable?

pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt

@@ -528,6 +528,10 @@
   (define-values (judgment-form-name dup-form-names mode position-contracts clauses rule-names)
     (parse-judgment-form-body body syn-err-name stx (identifier? orig) is-relation?))
   (define definitions
+    (with-syntax ([judgment-form-runtime-proc
+                   (syntax-property (syntax/loc judgment-form-name judgment-form-runtime-proc)
+                                    'undefined-error-name
+                                    (syntax-e judgment-form-name))])
       #`(begin
           (define-syntax #,judgment-form-name 
             (judgment-form '#,judgment-form-name '#,(cdr (syntax->datum mode)) #'judgment-form-runtime-proc
@@ -539,7 +543,7 @@
           (define judgment-form-runtime-proc (mk-judgment-form-proc #,lang))
           (define jf-lws (compiled-judgment-form-lws #,clauses #,judgment-form-name #,stx))
           (define judgment-runtime-gen-clauses (mk-judgment-gen-clauses #,lang (λ () (judgment-runtime-gen-clauses))))
-        (define jf-term-proc (make-jf-term-proc #,judgment-form-name #,syn-err-name #,lang #,nts #,mode))))
+          (define jf-term-proc (make-jf-term-proc #,judgment-form-name #,syn-err-name #,lang #,nts #,mode)))))
   (syntax-property
    (values ;prune-syntax
     (if (eq? 'top-level (syntax-local-context))

pkgs/redex-pkgs/redex-lib/redex/private/term-fn.rkt

@@ -52,8 +52,8 @@
   (transformer-predicate defined-term? stx))
 
 (define (defined-check id desc #:external [external id])
-  (if (eq? (identifier-binding id) 'lexical)
+  (if (equal? (identifier-binding id) 'lexical)
-      (quasisyntax/loc external (check-defined-lexical #,id '#,external #,desc))
+      (datum->syntax id (syntax-e id) external id)
       (quasisyntax/loc external (check-defined-module (λ () #,id) '#,external #,desc))))
 
 (define (not-expression-context stx)

pkgs/redex-pkgs/redex-lib/redex/private/term.rkt

@@ -467,6 +467,9 @@
   (syntax-parse stx
                 [(_ x:id t:expr)
                  (not-expression-context stx)
+                 (with-syntax ([term-val (syntax-property (syntax/loc #'x term-val)
+                                                          'undefined-error-name
+                                                          (syntax-e #'x))])
                    #'(begin
                        (define term-val (term t))
-                     (define-syntax x (defined-term #'term-val)))]))
+                       (define-syntax x (defined-term #'term-val))))]))

pkgs/redex-pkgs/redex-test/redex/tests/run-err-tests/judgment-form-undefined.rktd

@@ -1,4 +1,4 @@
-("reference to judgment form q before its definition"
+("q: undefined;\n cannot use before initialization"
  ([use q]) ([def q])
  (let ()
    (judgment-holds (use 1))

pkgs/redex-pkgs/redex-test/redex/tests/run-err-tests/term.rktd

@@ -41,7 +41,7 @@
  ([rhs 'a]) ([ellipsis ...])
  (term-let ([(x ellipsis) rhs]) 3))
 
-("reference to term x before its definition"
+("x: undefined;\n cannot use before initialization"
  ([use x]) ([def x])
  (let ()
    (define t (term (use y)))