suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

add #:lang keyword to term, which checks that underscored symbols agree with patterns in the provided language...changed most internal uses of term to use this form

Browse Source
This commit is contained in:
Burke Fetscher 2012-08-08 11:09:01 -05:00
parent d5024f0f20
commit 29661cc675
15 changed files with 173 additions and 70 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
collects/redex/examples/delim-cont/reduce.rkt
View File

@ -112,8 +112,8 @@
;; thunk and then tries again to invoke the continuation --- but inside a
;; `dw' for the already-run pre-thunk, so that it's treated as shared and not
;; run again.
(~~> (% v_1 (in-hole D_2 (in-hole W_3 ((cont v_1 (name k_1 (in-hole D_6 (in-hole W_4 (dw x_1 e_1 (hide-hole E_5) e_2))))) v_2))) v_3)
(% v_1 (in-hole D_6 (in-hole W_4 (begin e_1 (dw x_1 e_1 ((cont v_1 k_1) v_2) e_2)))) v_3)
(~~> (% v_1 (in-hole D_2 (in-hole W_3 ((cont v_1 (name k (in-hole D_6 (in-hole W_4 (dw x_1 e_1 (hide-hole E_5) e_2))))) v_2))) v_3)
(% v_1 (in-hole D_6 (in-hole W_4 (begin e_1 (dw x_1 e_1 ((cont v_1 k) v_2) e_2)))) v_3)
(side-condition (term (noMatch (in-hole D_2 W_3) E (% v_1 E v))))
(side-condition (term (sameDWs D_2 D_6)))
(side-condition (term (noShared W_3 (in-hole W_4 (dw x_1 e_1 E_5 e_2)))))

6
collects/redex/examples/racket-machine/util.rkt
View File

@ -5,12 +5,12 @@
(provide (all-defined-out))
(define-language any)
(define-language any-L)
(define-metafunction any
(define-metafunction any-L
[(count-up number)
,(build-list (term number) (λ (x) x))])
(define-metafunction any
(define-metafunction any-L
concat : (any ...) ... -> (any ...)
[(concat any ...) ,(apply append (term (any ...)))])

36
collects/redex/private/compiler/match.rkt
View File

@ -907,40 +907,40 @@
bool))
(in-hole Context
(letrec ((match-repeat
(λ (z binding_temp ... bound_temp ...)
(λ (z any_binding_temp ... any_bound_temp ...)
(begin
(when (and (null? bound_temp) ...)
(when (and (null? any_bound_temp) ...)
(Build-Let ;reverse
(let ([pvar_11 binding_temp] ...)
(let ([pvar_11 any_binding_temp] ...)
(matrix (z x_2 ...)
(((p_4 p_5 ... -> r_2) ,@(term (Add-Repeat-Vars (eqs_2 ...) (pvar_11 ...) (binding_temp ...)))))
(((Get-Pvar pvar_22) bound_temp) ...)
(((p_4 p_5 ... -> r_2) ,@(term (Add-Repeat-Vars (eqs_2 ...) (pvar_11 ...) (any_binding_temp ...)))))
(((Get-Pvar pvar_22) any_bound_temp) ...)
(pvar_3 ...) ; fix this
natural
bool))
(binding_temp ...)))
(when (and (cons? z) (cons? bound_temp) ...)
(any_binding_temp ...)))
(when (and (cons? z) (cons? any_bound_temp) ...)
(let ((carz (car z))
(car_bound_temp (car bound_temp))
(any_car_bound_temp (car any_bound_temp))
...)
(matrix (carz)
(((p_3 -> (match-repeat
(cdr z)
(cons pvar_11 binding_temp) ...
(cdr bound_temp) ...))
(cons pvar_11 any_binding_temp) ...
(cdr any_bound_temp) ...))
eqs_2 ...))
(((Get-Pvar pvar_22) car_bound_temp) ...)
(((Get-Pvar pvar_22) any_car_bound_temp) ...)
(pvar_3 ...)
,(+ 1 (term natural))
bool))
)))))
(Build-Temp-Let natural
(bound_temp ...)
(any_bound_temp ...)
(pvar_22 ...)
(Build-Let-Empty natural ,(map (λ (x) (term (Get-Pvar ,x))) (term (binding_temp ...)))
(Build-Let-Empty natural ,(map (λ (x) (term (Get-Pvar ,x))) (term (any_binding_temp ...)))
;,(if (zero? (term natural))
(match-repeat x_1 binding_temp ... bound_temp ...)
;(term (match-repeat x_1 binding_temp ... (car bound_temp) ...))
(match-repeat x_1 any_binding_temp ... any_bound_temp ...)
;(term (match-repeat x_1 any_binding_temp ... (car any_bound_temp) ...))
;)
)
)
@ -958,13 +958,13 @@
(fresh match-repeat)
(fresh z)
(fresh carz)
(fresh ((binding_temp ...)
(fresh ((any_binding_temp ...)
(pvar_11 ...)))
(fresh ((single_binding_temp ...)
(pvar_11 ...)))
(fresh ((bound_temp ...)
(fresh ((any_bound_temp ...)
(pvar_22 ...)))
(fresh ((car_bound_temp ...)
(fresh ((any_car_bound_temp ...)
(pvar_22 ...)))
(side-condition (not (term (Flushable?
(eqs_2 ...)))))

17
collects/redex/private/judgment-form.rkt
View File

@ -105,7 +105,8 @@
lang-nts
'reduction-relation
#t
#'x)])
#'x)]
[lang-stx lang])
(define-values (binding-constraints temporaries env+)
(generate-binding-constraints (syntax->list #'(names ...))
(syntax->list #'(names/ellipses ...))
@ -120,7 +121,7 @@
[(predicate)
#'combine-where-results/predicate]
[else (error 'unknown-where-mode "~s" where-mode)])
(match-pattern (compile-pattern #,lang `side-conditions-rewritten #t) (term e))
(match-pattern (compile-pattern #,lang `side-conditions-rewritten #t) (term/nts e #,lang-nts))
(λ (bindings)
(let ([x (lookup-binding bindings 'names)] ...)
(and binding-constraints ...
@ -184,7 +185,7 @@
(generate-binding-constraints output-names output-names/ellipses env orig-name)]
[(rest-body) (loop rest-clauses #`(list judgment-output #,to-not-be-in) env+)]
[(call)
(let ([input (quasisyntax/loc premise (term #,input-template))])
(let ([input (quasisyntax/loc premise (term/nts #,input-template #,lang-nts))])
(define (make-traced input)
(quasisyntax/loc premise
(call-judgment-form 'form-name #,judgment-proc '#,mode #,input)))
@ -341,10 +342,10 @@
(define definitions
#`(begin
(define-syntax #,judgment-form-name
(judgment-form '#,judgment-form-name '#,(cdr (syntax->datum mode)) #'judgment-form-proc #'mk-judgment-form-proc #'#,lang #'judgment-form-lws))
(judgment-form '#,judgment-form-name '#,(cdr (syntax->datum mode)) #'judgment-form-runtime-proc #'mk-judgment-form-proc #'#,lang #'judgment-form-lws))
(define mk-judgment-form-proc
(compile-judgment-form-proc #,judgment-form-name #,mode #,lang #,clauses #,position-contracts #,orig #,stx #,syn-err-name))
(define judgment-form-proc (mk-judgment-form-proc #,lang))
(define judgment-form-runtime-proc (mk-judgment-form-proc #,lang))
(define judgment-form-lws
(compiled-judgment-form-lws #,clauses))))
(syntax-property
@ -353,7 +354,7 @@
; Introduce the names before using them, to allow
; judgment form definition at the top-level.
#`(begin
(define-syntaxes (judgment-form-proc judgment-form-lws) (values))
(define-syntaxes (judgment-form-runtime-proc judgment-form-lws) (values))
#,definitions)
definitions))
'disappeared-use
@ -455,7 +456,7 @@
[judgment (syntax-case stx () [(_ judgment _) #'judgment])])
(check-judgment-arity stx judgment)
#`(sort #,(bind-withs syn-err-name '() lang nts (list judgment)
'flatten #`(list (term #,#'tmpl)) '() '() #f)
'flatten #`(list (term #,#'tmpl #:lang #,lang)) '() '() #f)
string<=?
#:key (λ (x) (format "~s" x))))]
[(_ (not-form-name . _) . _)
@ -492,7 +493,7 @@
(struct-copy judgment-form (lookup-judgment-form-id name)
[proc #'recur]))])
(bind-withs syn-error-name '() #'lang nts (syntax->list #'prems)
'flatten #`(list (term (#,@output-pats)))
'flatten #`(list (term/nts (#,@output-pats) #,nts))
(syntax->list #'(names ...))
(syntax->list #'(names/ellipses ...))
#f)))

6
collects/redex/private/reduction-semantics.rkt
View File

@ -662,7 +662,7 @@
(λ (bindings rhs-binder)
(term-let ([lhs-to-id rhs-binder]
[names/ellipses (lookup-binding bindings 'names)] ...)
(term rhs-to)))
(term rhs-to #:lang lang)))
#,child-proc
`fresh-rhs-from))
(get-choices stx orig-name bm #'lang
@ -721,7 +721,7 @@
sides/withs/freshs
'flatten
#`(list (cons #,(or computed-name #'none)
(term #,to)))
(term #,to #:lang #,lang)))
(syntax->list #'(names ...))
(syntax->list #'(names/ellipses ...))
#t))
@ -1243,7 +1243,7 @@
syn-error-name '()
#'effective-lang lang-nts
sc/b 'flatten
#`(list (term #,rhs))
#`(list (term #,rhs #:lang lang))
(syntax->list names)
(syntax->list names/ellipses)
#t))

13
collects/redex/private/rewrite-side-conditions.rkt
View File

@ -3,6 +3,7 @@
(require mzlib/list
"underscore-allowed.rkt")
(require "term.rkt"
"term-fn.rkt"
setup/path-to-relative
(for-template
mzscheme
@ -18,18 +19,6 @@
(provide (struct-out id/depth))
(define-values (language-id make-language-id language-id? language-id-get language-id-set) (make-struct-type 'language-id #f 2 0 #f '() #f 0))
(define (language-id-nts stx id) (language-id-getter stx id 1))
(define (language-id-getter stx id n)
(unless (identifier? stx)
(raise-syntax-error id "expected an identifier defined by define-language" stx))
(let ([val (syntax-local-value stx (λ () #f))])
(unless (and (set!-transformer? val)
(language-id? (set!-transformer-procedure val)))
(raise-syntax-error id "expected an identifier defined by define-language" stx))
(language-id-get (set!-transformer-procedure val) n)))
(define (rewrite-side-conditions/check-errs all-nts what bind-names? orig-stx)
(define (expected-exact name n stx)
(raise-syntax-error what (format "~a expected to have ~a arguments"

20
collects/redex/private/term-fn.rkt
View File

@ -11,7 +11,10 @@
(struct-out defined-term)
defined-term-id?
defined-check
not-expression-context)
not-expression-context
make-language-id
language-id-nts
pattern-symbols)
(define-values (struct-type make-term-fn term-fn? term-fn-get term-fn-set!)
(make-struct-type 'term-fn #f 1 0))
@ -38,3 +41,18 @@
(define (not-expression-context stx)
(when (eq? (syntax-local-context) 'expression)
(raise-syntax-error #f "not allowed in an expression context" stx)))
(define-values (language-id make-language-id language-id? language-id-get language-id-set) (make-struct-type 'language-id #f 2 0 #f '() #f 0))
(define (language-id-nts stx id) (language-id-getter stx id 1))
(define (language-id-getter stx id n)
(unless (identifier? stx)
(raise-syntax-error id "expected an identifier defined by define-language" stx))
(let ([val (syntax-local-value stx (λ () #f))])
(unless (and (set!-transformer? val)
(language-id? (set!-transformer-procedure val)))
(raise-syntax-error id "expected an identifier defined by define-language" stx))
(language-id-get (set!-transformer-procedure val) n)))
(define pattern-symbols '(any number natural integer real string variable
variable-not-otherwise-mentioned hole symbol))

80
collects/redex/private/term.rkt
View File

@ -4,14 +4,17 @@
"term-fn.rkt"
syntax/boundmap
syntax/parse
racket/syntax)
racket/syntax
"keyword-macros.rkt"
"matcher.rkt")
syntax/datum
"error.rkt"
"matcher.rkt")
(provide term term-let define-term
hole in-hole
term-let/error-name term-let-fn term-define-fn)
term-let/error-name term-let-fn term-define-fn
term/nts)
(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"))
@ -21,14 +24,37 @@
[(_ () e) (syntax e)]
[(_ (a b ...) e) (syntax (with-syntax (a) (with-syntax* (b ...) e)))]))
(define-syntax-rule (term t)
(#%expression (term/private t)))
(define-for-syntax lang-keyword
(list '#:lang #f))
(define-syntax (term stx)
(syntax-case stx ()
[(term t . kw-args)
(with-syntax ([(lang-stx) (parse-kw-args (list lang-keyword)
(syntax kw-args)
stx
(syntax-e #'form))])
(if (syntax->datum #'lang-stx)
(let ([lang-nts (language-id-nts #'lang-stx 'term)])
#`(term/nts t #,lang-nts))
#'(term/nts t #f)))]))
(define-syntax (term/nts stx)
(syntax-case stx ()
[(_ arg nts)
#'(#%expression (term/private arg nts))]))
(define-syntax (term/private orig-stx)
(define lang-nts #f)
(define outer-bindings '())
(define applied-metafunctions
(make-free-identifier-mapping))
(define error-stx
(syntax-case orig-stx ()
[(_ e-stx nts-stx)
#'e-stx]))
(define (rewrite stx)
(let-values ([(rewritten _) (rewrite/max-depth stx 0)])
rewritten))
@ -71,6 +97,7 @@
(and (identifier? (syntax x))
(term-id? (syntax-local-value (syntax x) (λ () #f))))
(let ([id (syntax-local-value/record (syntax x) (λ (x) #t))])
(check-id (syntax->datum (term-id-id id)) stx)
(values (datum->syntax (term-id-id id) (syntax-e (term-id-id id)) (syntax x))
(term-id-depth id)))]
[x
@ -78,6 +105,7 @@
(let ([ref (syntax-property
(defined-term-value (syntax-local-value #'x))
'disappeared-use #'x)])
(check-id (syntax->datum #'x) stx)
(with-syntax ([v #`(begin
#,(defined-check ref "term" #:external #'x)
#,ref)])
@ -95,6 +123,10 @@
[(in-hole . x)
(raise-syntax-error 'term "malformed in-hole" orig-stx stx)]
[hole (values (syntax (undatum the-hole)) 0)]
[x
(and (identifier? (syntax x))
(check-id (syntax->datum #'x) stx))
(values stx 0)]
[() (values stx 0)]
@ -121,22 +153,32 @@
[_ (values stx 0)]))
(define (check-id id stx)
(when lang-nts
(define m (regexp-match #rx"^([^_]*)_" (symbol->string id)))
(when m
(unless (memq (string->symbol (list-ref m 1)) (append pattern-symbols lang-nts))
(raise-syntax-error 'term "before underscore must be either a non-terminal or a built-in pattern" error-stx stx)))))
(syntax-case orig-stx ()
[(_ arg)
(with-disappeared-uses
(with-syntax ([rewritten (rewrite (syntax arg))])
#`(begin
#,@(free-identifier-mapping-map
applied-metafunctions
(λ (f _) (defined-check f "metafunction")))
#,(let loop ([bs (reverse outer-bindings)])
(cond
[(null? bs) (syntax (quasidatum rewritten))]
[else (with-syntax ([rec (loop (cdr bs))]
[fst (car bs)])
(syntax (with-datum (fst)
rec)))])))))]))
[(_ arg nts-stx)
(begin
(when (syntax->datum #'nts-stx)
(set! lang-nts (syntax->datum #'nts-stx)))
(with-disappeared-uses
(with-syntax ([rewritten (rewrite (syntax arg))])
#`(begin
#,@(free-identifier-mapping-map
applied-metafunctions
(λ (f _) (defined-check f "metafunction")))
#,(let loop ([bs (reverse outer-bindings)])
(cond
[(null? bs) (syntax (quasidatum rewritten))]
[else (with-syntax ([rec (loop (cdr bs))]
[fst (car bs)])
(syntax (with-datum (fst)
rec)))]))))))]))
(define-syntax (term-let-fn stx)
(syntax-case stx ()
[(_ ([f rhs] ...) body1 body2 ...)

14
collects/redex/scribblings/ref.scrbl
View File

@ -450,9 +450,9 @@ them.}
produces the boolean or the string.}
]
@defform[(term @#,tttterm)]{
@defform*[[(term @#,tttterm) (term @#,tttterm #:lang lang-id)]]{
This form is used for construction of a term.
Used for construction of a term.
It behaves similarly to @racket[quasiquote], except for a few special
forms that are recognized (listed below) and that names bound by
@ -460,6 +460,16 @@ forms that are recognized (listed below) and that names bound by
those names were bound to, expanding ellipses as in-place sublists (in
the same manner as syntax-case patterns).
The optional @racket[#:lang] keyword must supply an identifier bound
by @racket[define-language], and adds a check that any symbol containing
an underscore in @tttterm could have been bound by a pattern in the
language referenced by @racket[lang-id]. In practice, this means that the
underscore must be preceded by a non-terminal in that langauge or a
built-in @ttpattern such as @racket[number]. This form of @racket[term]
is used internally by default, so this check is applied to terms
that are constructed by Redex forms such as @racket[reduction-relation]
and @racket[define-metafunction].
For example,
@racketblock[

4
collects/redex/tests/rg-test.rkt
View File

@ -1201,12 +1201,12 @@
(define-extended-language M L (x 2))
(define-metafunction L
[(f)
_
?
(where x 2)])
(define-metafunction/extension f M
g : any -> any)
(test (with-handlers ([exn:fail:redex:generation-failure? (const #f)])
(check-metafunction g (λ (_) #t) #:attempts 1 #:print? #f))
(check-metafunction g (λ (?) #t) #:attempts 1 #:print? #f))
#t))
(test (output (λ () (check-metafunction m (λ (_) #t)))) #rx"no counterexamples")

6
collects/redex/tests/syn-err-tests/metafunction-definition.rktd
View File

@ -18,3 +18,9 @@
(#rx"expected an identifier"
([not-id junk])
(define-metafunction not-id also-junk))
(#rx"before underscore"
([not-non-term z!_1])
(define-metafunction syn-err-lang
[(func M_1 E_2)
(M_1 (E_2 not-non-term) M_1)]))

7
collects/redex/tests/syn-err-tests/reduction-relation-definition.rktd
View File

@ -136,3 +136,10 @@
syn-err-lang
(--> 1 1
(judgment-holds bad-judgment)))))
(#rx"before underscore"
([not-non-term Z_1])
(reduction-relation
syn-err-lang
(--> (in-hole E (Q_1 M_1))
(in-hole E (M_1 not-non-term)))))

7
collects/redex/tests/syn-err-tests/term-lang.rktd Normal file
View File

@ -0,0 +1,7 @@
(#rx"before underscore"
([not-a-non-term Z_1])
(term not-a-non-term #:lang syn-err-lang))
(#rx"before underscore"
([not-a-non-term AA_1])
(term (Q_1 Q_2 (Q_3 not-a-non-term)) #:lang syn-err-lang))

19
collects/redex/tests/tl-test.rkt
View File

@ -435,6 +435,25 @@
(exec-runtime-error-tests "run-err-tests/define-union-language.rktd"))
(exec-syntax-error-tests "syn-err-tests/language-definition.rktd")
;; term with #:lang tests
(exec-syntax-error-tests "syn-err-tests/term-lang.rktd")
(let ()
(define-language L
(a number)
(b (a a))
(c (b b)))
(test (term 1 #:lang L) 1)
(test (term ((1 2) (3 4)) #:lang L) '((1 2) (3 4)))
(test (term (1 2 3 4) #:lang L) '(1 2 3 4))
(test (redex-let L ([a_1 5])
(term (a_1 6) #:lang L))
'(5 6))
(test (redex-let L ([number_1 5])
(term (number_1 6) #:lang L))
'(5 6)))
;
;
; ;;; ;

4
doc/release-notes/redex/HISTORY.txt
View File

@ -1,3 +1,7 @@
v5.3.1
* added optional #:lang keyword to term
v5.3
* added the amb tutorial.