Adds define-term form

collects/redex/private/defined-checks.rkt

@@ -14,4 +14,4 @@
     (thunk)))
 
 (define (report-undefined name desc)
-  (redex-error #f "~a ~s applied before its definition" desc name))
+  (redex-error #f "reference to ~a ~s before its definition" desc name))

collects/redex/private/reduction-semantics.rkt

@@ -1331,10 +1331,6 @@
     (map (λ (x) (to-lw/proc (datum->syntax #f (cdr (syntax-e x)) x)))
          (syntax->list #'(lhs-for-lw ...)))))
 
-(define-for-syntax (not-expression-context stx)
-  (when (eq? (syntax-local-context) 'expression)
-    (raise-syntax-error #f "not allowed in an expression context" stx)))
-
 ;                                                                                                          
 ;                                                                                                          
 ;                                                                                                          

collects/redex/private/term-fn.rkt

@@ -7,7 +7,10 @@
          (struct-out term-id)
          (struct-out judgment-form)
          judgment-form-id?
-         defined-check)
+         (struct-out defined-term)
+         defined-term-id?
+         defined-check
+         not-expression-context)
 
 (define-values (struct-type make-term-fn term-fn? term-fn-get term-fn-set!) 
   (make-struct-type 'term-fn #f 1 0))
@@ -15,13 +18,24 @@
 
 (define-struct term-id (id depth))
 
-(define-struct judgment-form (name mode proc lang lws))
+(define ((transformer-predicate p?) stx)
-
-(define (judgment-form-id? stx)
   (and (identifier? stx)
-       (judgment-form? (syntax-local-value stx (λ () 'not-a-judgment-form)))))
+       (cond [(syntax-local-value stx (λ () #f)) => p?]
+             [else #f])))
+
+(define-struct judgment-form (name mode proc lang lws))
+(define judgment-form-id? 
+  (transformer-predicate judgment-form?))
+
+(define-struct defined-term (value))
+(define defined-term-id?
+  (transformer-predicate defined-term?))
 
 (define (defined-check id desc #:external [external id])
   (if (eq? (identifier-binding id) 'lexical)
       (quasisyntax/loc external (check-defined-lexical #,id '#,external #,desc))
-      (quasisyntax/loc external (check-defined-module (λ () #,id) '#,external #,desc))))
+      (quasisyntax/loc external (check-defined-module (λ () #,id) '#,external #,desc))))
+
+(define (not-expression-context stx)
+  (when (eq? (syntax-local-context) 'expression)
+    (raise-syntax-error #f "not allowed in an expression context" stx)))

collects/redex/private/term.rkt

@@ -3,11 +3,14 @@
 (require (for-syntax scheme/base 
                      "term-fn.rkt"
                      syntax/boundmap
+                     syntax/parse
                      racket/syntax)
          "error.rkt"
          "matcher.rkt")
 
-(provide term term-let term-let/error-name term-let-fn term-define-fn hole in-hole)
+(provide term term-let define-term
+         hole in-hole
+         term-let/error-name term-let-fn term-define-fn)
 
 (define-syntax (hole stx) (raise-syntax-error 'hole "used outside of term"))
 (define-syntax (in-hole stx) (raise-syntax-error 'in-hole "used outside of term"))
@@ -69,6 +72,15 @@
        (let ([id (syntax-local-value/record (syntax x) (λ (x) #t))])
          (values (datum->syntax (term-id-id id) (syntax-e (term-id-id id)) (syntax x))
                  (term-id-depth id)))]
+      [x
+       (defined-term-id? #'x)
+       (let ([ref (syntax-property
+                   (defined-term-value (syntax-local-value #'x))
+                   'disappeared-use #'x)])
+         (with-syntax ([v #`(begin
+                              #,(defined-check ref "term" #:external #'x)
+                              #,ref)])
+           (values #'#,v 0)))]
       [(unquote x)
        (values (syntax (unsyntax x)) 0)]
       [(unquote . x)
@@ -208,3 +220,11 @@
       (term-let/error-name term-let ((x rhs) ...) body1 body2 ...))]
     [(_ x)
      (raise-syntax-error 'term-let "expected at least one body" stx)]))
+
+(define-syntax (define-term stx)
+  (syntax-parse stx
+    [(_ x:id t:expr)
+     (not-expression-context stx)
+     #'(begin
+         (define term-val (term t))
+         (define-syntax x (defined-term #'term-val)))]))

collects/redex/redex.scrbl

@@ -421,8 +421,8 @@ stands for repetition unless otherwise indicated):
 
 @item{A term written @racket[_identifier] is equivalent to the
 corresponding symbol, unless the identifier is bound by
-@racket[term-let] (or in a @|pattern| elsewhere) or is
+@racket[term-let], @racket[define-term], or a @|pattern| variable or
-@tt{hole} (as below).  }
+the identifier is @tt{hole} (as below).}
 
 @item{A term written @racket[(_term-sequence ...)] constructs a list of
 the terms constructed by the sequence elements.}
@@ -532,6 +532,9 @@ In some contexts, it may be more efficient to use @racket[term-match/single]
 The @racket[let*] analog of @racket[redex-let].
 }
 
+@defform[(define-term identifier @#,tttterm)]{
+Defines @racket[identifier] for use in @|tterm| templates.}
+
 @defform[(term-match language [@#,ttpattern expression] ...)]{
 
 This produces a procedure that accepts term (or quoted)

collects/redex/reduction-semantics.rkt

@@ -40,6 +40,7 @@
          term-match/single
          redex-let
          redex-let*
+         define-term
          match? match-bindings
          make-bind bind? bind-name bind-exp
          

collects/redex/tests/check-syntax-test.rkt

@@ -153,4 +153,25 @@
   (test (send annotations collected-rename-class contract-name)
         (expected-rename-class metafunction-binding)))
 
+;; define-term
+(let ([annotations (new collector%)])
+  (define-values (add-syntax done)
+    (make-traversal module-namespace #f))
+  
+  (define def-name (identifier x))
+  (define use-name (identifier x))
+  
+  (parameterize ([current-annotations annotations]
+                 [current-namespace module-namespace])
+    (add-syntax
+     (expand #`(let ()
+                 (define-term #,def-name a)
+                 (term (#,use-name b)))))
+    (done))
+  
+  (test (send annotations collected-rename-class def-name)
+        (expected-rename-class (list def-name use-name)))
+  (test (send annotations collected-rename-class def-name)
+        (expected-rename-class (list def-name use-name))))
+
 (print-tests-passed 'check-syntax-test.rkt)

collects/redex/tests/run-err-tests/judgment-form-undefined.rktd

@@ -1,4 +1,4 @@
-("judgment form q applied before its definition"
+("reference to judgment form q before its definition"
  ([use q]) ([def q])
  (let ()
    (judgment-holds (use 1))

collects/redex/tests/run-err-tests/term.rktd

@@ -39,4 +39,11 @@
 
 (#rx"term .* does not match pattern"
  ([rhs 'a]) ([ellipsis ...])
- (term-let ([(x ellipsis) rhs]) 3))
+ (term-let ([(x ellipsis) rhs]) 3))
+
+("reference to term x before its definition"
+ ([use x]) ([def x])
+ (let ()
+   (define t (term (use y)))
+   (define-term def z)
+   t))

collects/redex/tests/tl-test.rkt

@@ -989,14 +989,14 @@
           (with-handlers ([exn:fail:redex? exn-message])
             (eval '(require 'm))
             #f))
-        "metafunction q applied before its definition")
+        "reference to metafunction q before its definition")
   (test (with-handlers ([exn:fail:redex? exn-message])
           (let ()
             (term (q))
             (define-language L)
             (define-metafunction L [(q) ()])
             #f))
-        "metafunction q applied before its definition")
+        "reference to metafunction q before its definition")
   
   (exec-syntax-error-tests "syn-err-tests/metafunction-definition.rktd")
 ;                                                                                                 
@@ -2131,6 +2131,33 @@
       (eval '(require redex/reduction-semantics))
       (exec-runtime-error-tests "run-err-tests/judgment-form-undefined.rktd"))
     
+  
+;                                                                               
+;                                                                               
+;                                                                               
+;       ;            ;;    ;                                                    
+;       ;           ;      ;                          ;                         
+;       ;           ;                                 ;                         
+;    ;;;;   ;;;    ;;;     ;    ;;;;    ;;;          ;;;     ;;;   ; ;;   ;;;;; 
+;   ;   ;  ;   ;    ;      ;    ;   ;  ;   ;  ;;;;;   ;     ;   ;  ;;  ;  ; ; ; 
+;   ;   ;  ;;;;;    ;      ;    ;   ;  ;;;;;          ;     ;;;;;  ;   ;  ; ; ; 
+;   ;   ;  ;        ;      ;    ;   ;  ;              ;     ;      ;      ; ; ; 
+;   ;   ;  ;   ;    ;      ;    ;   ;  ;   ;          ;     ;   ;  ;      ; ; ; 
+;    ;;;;   ;;;     ;      ;    ;   ;   ;;;            ;;    ;;;   ;      ; ; ; 
+;                                                                               
+;                                                                               
+;                                                                               
+  
+  (test (let ()
+          (define-term x 1)
+          (term (x x)))
+        (term (1 1)))
+  (test (let ()
+          (define-term x 1)
+          (let ([x 'whatever])
+            (term (x x))))
+        (term (x x)))
+    
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   ;;
   ;; examples from doc.txt