From c0625dc30c007c5dfa11c4cb01bc2e8c3b81466f Mon Sep 17 00:00:00 2001 From: Casey Klein Date: Tue, 30 Aug 2011 12:43:07 -0500 Subject: [PATCH] Adds define-term form --- collects/redex/private/defined-checks.rkt | 2 +- .../redex/private/reduction-semantics.rkt | 4 --- collects/redex/private/term-fn.rkt | 26 ++++++++++++---- collects/redex/private/term.rkt | 22 ++++++++++++- collects/redex/redex.scrbl | 7 +++-- collects/redex/reduction-semantics.rkt | 1 + collects/redex/tests/check-syntax-test.rkt | 21 +++++++++++++ .../judgment-form-undefined.rktd | 2 +- collects/redex/tests/run-err-tests/term.rktd | 9 +++++- collects/redex/tests/tl-test.rkt | 31 +++++++++++++++++-- 10 files changed, 107 insertions(+), 18 deletions(-) diff --git a/collects/redex/private/defined-checks.rkt b/collects/redex/private/defined-checks.rkt index 261866f2ab..8861097b8c 100644 --- a/collects/redex/private/defined-checks.rkt +++ b/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)) \ No newline at end of file + (redex-error #f "reference to ~a ~s before its definition" desc name)) \ No newline at end of file diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt index c2f3bfc6a6..d82651e81e 100644 --- a/collects/redex/private/reduction-semantics.rkt +++ b/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))) - ; ; ; diff --git a/collects/redex/private/term-fn.rkt b/collects/redex/private/term-fn.rkt index 1440fe2efb..3deb9c1b04 100644 --- a/collects/redex/private/term-fn.rkt +++ b/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 (judgment-form-id? stx) +(define ((transformer-predicate p?) 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)))) \ No newline at end of file + (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))) \ No newline at end of file diff --git a/collects/redex/private/term.rkt b/collects/redex/private/term.rkt index a64a39d00c..b6e6f0602c 100644 --- a/collects/redex/private/term.rkt +++ b/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)))])) \ No newline at end of file diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl index 2ff16ed1c8..25e9f61360 100644 --- a/collects/redex/redex.scrbl +++ b/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 -@tt{hole} (as below). } +@racket[term-let], @racket[define-term], or a @|pattern| variable or +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) diff --git a/collects/redex/reduction-semantics.rkt b/collects/redex/reduction-semantics.rkt index c04fd42205..a95d0b7b74 100644 --- a/collects/redex/reduction-semantics.rkt +++ b/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 diff --git a/collects/redex/tests/check-syntax-test.rkt b/collects/redex/tests/check-syntax-test.rkt index 357fd0c3a3..b173b35173 100644 --- a/collects/redex/tests/check-syntax-test.rkt +++ b/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) \ No newline at end of file diff --git a/collects/redex/tests/run-err-tests/judgment-form-undefined.rktd b/collects/redex/tests/run-err-tests/judgment-form-undefined.rktd index 04c37d2b03..0a4f2e6e66 100644 --- a/collects/redex/tests/run-err-tests/judgment-form-undefined.rktd +++ b/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)) diff --git a/collects/redex/tests/run-err-tests/term.rktd b/collects/redex/tests/run-err-tests/term.rktd index 0a6e36dd15..33d502408e 100644 --- a/collects/redex/tests/run-err-tests/term.rktd +++ b/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)) \ No newline at end of file + (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)) \ No newline at end of file diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt index e2853ea061..5a76e7589f 100644 --- a/collects/redex/tests/tl-test.rkt +++ b/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