Added syntax properties to provide/contract so that the contracts on exported variables can be recovered from the fully expanded program.
This commit is contained in:
parent
e28b60e44f
commit
f7c1a97c0b
|
@ -636,9 +636,11 @@
|
|||
;; code-for-one-exists-id : syntax -> syntax
|
||||
(define (code-for-one-exists-id x x-gen)
|
||||
#`(define #,x-gen (new-∃/c '#,x)))
|
||||
|
||||
|
||||
(define (add-exists-binders stx exists-binders)
|
||||
#`(let #,exists-binders #,stx))
|
||||
(if (null? exists-binders)
|
||||
stx
|
||||
#`(let #,exists-binders #,stx)))
|
||||
|
||||
(define (add-a-binder id id-gen binders)
|
||||
(cons #`[#,id #,id-gen] binders))
|
||||
|
@ -692,25 +694,28 @@
|
|||
(procedure-arity-includes? id #,(length (syntax->list #'(dom ...)))))]
|
||||
[_ #f])])
|
||||
(with-syntax ([code
|
||||
(quasisyntax/loc stx
|
||||
(begin
|
||||
(define pos-module-source (quote-module-path))
|
||||
|
||||
#,@(if no-need-to-check-ctrct?
|
||||
(list)
|
||||
(list #'(define contract-id
|
||||
(let ([ex-id ctrct]) ;; let is here to give the right name.
|
||||
(verify-contract 'provide/contract ex-id)))))
|
||||
(define-syntax id-rename
|
||||
(make-provide/contract-transformer (quote-syntax contract-id)
|
||||
(quote-syntax id)
|
||||
(quote-syntax reflect-external-name)
|
||||
(quote-syntax pos-module-source)))
|
||||
|
||||
#,@(if provide?
|
||||
(list #`(provide (rename-out [id-rename external-name])))
|
||||
null)))])
|
||||
|
||||
(syntax-property
|
||||
(quasisyntax/loc stx
|
||||
(begin
|
||||
(define pos-module-source (quote-module-path))
|
||||
|
||||
#,@(if no-need-to-check-ctrct?
|
||||
(list)
|
||||
(list #'(define contract-id
|
||||
(let ([ex-id ctrct]) ;; let is here to give the right name.
|
||||
(verify-contract 'provide/contract ex-id)))))
|
||||
(define-syntax id-rename
|
||||
(make-provide/contract-transformer (quote-syntax contract-id)
|
||||
(quote-syntax id)
|
||||
(quote-syntax reflect-external-name)
|
||||
(quote-syntax pos-module-source)))
|
||||
|
||||
#,@(if provide?
|
||||
(list #`(provide (rename-out [id-rename external-name])))
|
||||
null)))
|
||||
'provide/contract-original-contract
|
||||
(vector #'external-name #'ctrct))])
|
||||
|
||||
(syntax-local-lift-module-end-declaration
|
||||
#`(begin
|
||||
(unless extra-test
|
||||
|
|
|
@ -748,6 +748,14 @@ The @racket[#:∃] and @racket[#:exists] clauses define new abstract
|
|||
contracts. The variables are bound in the remainder of the @racket[provide/contract]
|
||||
expression to new contracts that hide the values they accept and
|
||||
ensure that the exported functions are treated parametrically.
|
||||
|
||||
The implementation of @scheme[provide/contract] attaches uses
|
||||
@scheme[syntax-property] to attach properties to the code it generates
|
||||
that records the syntax of the contracts in the fully expanded program.
|
||||
Specifically, the symbol @scheme['provide/contract-original-contract]
|
||||
is bound to vectors of two elements, the exported identifier and a
|
||||
syntax object for the expression that produces the contract controlling
|
||||
the export.
|
||||
}
|
||||
|
||||
@defform*/subs[
|
||||
|
|
Loading…
Reference in New Issue
Block a user