Add #:forall, #:∀ to contract-out
This commit is contained in:
parent
a5d1007696
commit
965a74453f
|
@ -169,7 +169,8 @@
|
||||||
;; compare raw identifiers for `struct' and `rename' just like provide does
|
;; compare raw identifiers for `struct' and `rename' just like provide does
|
||||||
(syntax-case* clause (struct rename) (λ (x y) (eq? (syntax-e x) (syntax-e y)))
|
(syntax-case* clause (struct rename) (λ (x y) (eq? (syntax-e x) (syntax-e y)))
|
||||||
[exists
|
[exists
|
||||||
(or (eq? '#:exists (syntax-e #'exists)) (eq? '#:∃ (syntax-e #'exists)))
|
(or (eq? '#:exists (syntax-e #'exists)) (eq? '#:∃ (syntax-e #'exists))
|
||||||
|
(eq? '#:forall (syntax-e #'exists)) (eq? '#:∀ (syntax-e #'exists)))
|
||||||
(cond
|
(cond
|
||||||
[(null? (cdr clauses))
|
[(null? (cdr clauses))
|
||||||
(raise-syntax-error who
|
(raise-syntax-error who
|
||||||
|
@ -184,7 +185,7 @@
|
||||||
(if just-check-errors?
|
(if just-check-errors?
|
||||||
(loop (cddr clauses) exists-binders)
|
(loop (cddr clauses) exists-binders)
|
||||||
(with-syntax ([(x-gen) (generate-temporaries #'(x))])
|
(with-syntax ([(x-gen) (generate-temporaries #'(x))])
|
||||||
(cons (code-for-one-exists-id #'x #'x-gen)
|
(cons (code-for-one-poly-id #'x #'x-gen #'exists)
|
||||||
(loop (cddr clauses)
|
(loop (cddr clauses)
|
||||||
(add-a-binder #'x #'x-gen exists-binders)))))]
|
(add-a-binder #'x #'x-gen exists-binders)))))]
|
||||||
[(x ...)
|
[(x ...)
|
||||||
|
@ -192,7 +193,7 @@
|
||||||
(if just-check-errors?
|
(if just-check-errors?
|
||||||
(loop (cddr clauses) exists-binders)
|
(loop (cddr clauses) exists-binders)
|
||||||
(with-syntax ([(x-gen ...) (generate-temporaries #'(x ...))])
|
(with-syntax ([(x-gen ...) (generate-temporaries #'(x ...))])
|
||||||
(append (map code-for-one-exists-id
|
(append (map (λ (x x-gen) (code-for-one-poly-id x x-gen #'exists))
|
||||||
(syntax->list #'(x ...))
|
(syntax->list #'(x ...))
|
||||||
(syntax->list #'(x-gen ...)))
|
(syntax->list #'(x-gen ...)))
|
||||||
(loop (cddr clauses)
|
(loop (cddr clauses)
|
||||||
|
@ -678,9 +679,11 @@
|
||||||
field-contract-id
|
field-contract-id
|
||||||
void?))))
|
void?))))
|
||||||
|
|
||||||
;; code-for-one-exists-id : syntax -> syntax
|
;; code-for-one-poly-id : syntax -> syntax
|
||||||
(define (code-for-one-exists-id x x-gen)
|
(define (code-for-one-poly-id x x-gen poly)
|
||||||
#`(define #,x-gen (new-∃/c '#,x)))
|
(if (or (eq? '#:exists (syntax-e poly)) (eq? '#:∃ (syntax-e poly)))
|
||||||
|
#`(define #,x-gen (new-∃/c '#,x))
|
||||||
|
#`(define #,x-gen (new-∀/c '#,x))))
|
||||||
|
|
||||||
(define (add-exists-binders stx exists-binders)
|
(define (add-exists-binders stx exists-binders)
|
||||||
(if (null? exists-binders)
|
(if (null? exists-binders)
|
||||||
|
|
|
@ -1081,10 +1081,12 @@ earlier fields.}}
|
||||||
(struct (id identifier) ((id contract-expr) ...))
|
(struct (id identifier) ((id contract-expr) ...))
|
||||||
(rename orig-id id contract-expr)
|
(rename orig-id id contract-expr)
|
||||||
(id contract-expr)
|
(id contract-expr)
|
||||||
(code:line #:∃ exists-variables)
|
(code:line #:∃ poly-variables)
|
||||||
(code:line #:exists exists-variables)]
|
(code:line #:poly exists-variables)
|
||||||
[exists-variables identifier
|
(code:line #:∀ poly-variables)
|
||||||
(identifier ...)])]{
|
(code:line #:forall poly-variables)]
|
||||||
|
[poly-variables identifier
|
||||||
|
(identifier ...)])]{
|
||||||
|
|
||||||
A @racket[_provide-spec] for use in @racket[provide] (currently only for
|
A @racket[_provide-spec] for use in @racket[provide] (currently only for
|
||||||
the same @tech{phase level} as the @racket[provide] form; for example,
|
the same @tech{phase level} as the @racket[provide] form; for example,
|
||||||
|
@ -1124,10 +1126,12 @@ the selector or mutators for the super-struct are not provided. The
|
||||||
exported structure-type name always doubles as a constructor, even if
|
exported structure-type name always doubles as a constructor, even if
|
||||||
the original structure-type name does not act as a constructor.
|
the original structure-type name does not act as a constructor.
|
||||||
|
|
||||||
The @racket[#:∃] and @racket[#:exists] clauses define new abstract
|
The @racket[#:∃], @racket[#:exists], @racket[#:∀], and @racket[#:forall]
|
||||||
contracts. The variables are bound in the remainder of the @racket[contract-out]
|
clauses define new abstract contracts. The variables are bound in the
|
||||||
form to new contracts that hide the values they accept and
|
remainder of the @racket[contract-out] form to new contracts that hide
|
||||||
ensure that the exported functions are treated parametrically.
|
the values they accept and ensure that the exported functions are treated
|
||||||
|
parametrically. See @racket[new-∃/c] and @racket[new-∀/c] for details
|
||||||
|
on how the clauses hide the values.
|
||||||
|
|
||||||
The implementation of @racket[contract-out] attaches uses
|
The implementation of @racket[contract-out] attaches uses
|
||||||
@racket[syntax-property] to attach properties to the code it generates
|
@racket[syntax-property] to attach properties to the code it generates
|
||||||
|
|
|
@ -13990,6 +13990,86 @@ so that propagation occurs.
|
||||||
|
|
||||||
(dynamic-require ''provide/contract38-b 'the-answer))
|
(dynamic-require ''provide/contract38-b 'the-answer))
|
||||||
#t)
|
#t)
|
||||||
|
|
||||||
|
;; #:forall contract-out clauses
|
||||||
|
(test/spec-passed/result
|
||||||
|
'provide/contract39
|
||||||
|
'(begin
|
||||||
|
(eval '(module provide/contract39-m1 racket/base
|
||||||
|
(require racket/contract)
|
||||||
|
(provide/contract
|
||||||
|
#:∀ x
|
||||||
|
[f (-> x (-> x x) x)])
|
||||||
|
(define (f x g) (g x))))
|
||||||
|
|
||||||
|
(eval '(module provide/contract39-m2 racket/base
|
||||||
|
(require racket/contract 'provide/contract39-m1)
|
||||||
|
(provide provide/contract39-x)
|
||||||
|
(define provide/contract39-x (f 10 (λ (x) x)))))
|
||||||
|
|
||||||
|
(eval '(require 'provide/contract39-m2))
|
||||||
|
(eval 'provide/contract39-x))
|
||||||
|
10)
|
||||||
|
|
||||||
|
(test/spec-passed/result
|
||||||
|
'provide/contract40
|
||||||
|
'(begin
|
||||||
|
(eval '(module provide/contract40-m1 racket/base
|
||||||
|
(require racket/contract)
|
||||||
|
(provide/contract
|
||||||
|
#:forall x
|
||||||
|
[f (-> x (-> x x) x)])
|
||||||
|
(define (f x g) (g x))))
|
||||||
|
|
||||||
|
(eval '(module provide/contract40-m2 racket/base
|
||||||
|
(require racket/contract 'provide/contract40-m1)
|
||||||
|
(provide provide/contract40-x)
|
||||||
|
(define provide/contract40-x (f 10 (λ (x) x)))))
|
||||||
|
|
||||||
|
(eval '(require 'provide/contract40-m2))
|
||||||
|
(eval 'provide/contract40-x))
|
||||||
|
10)
|
||||||
|
|
||||||
|
(test/spec-passed/result
|
||||||
|
'provide/contract41
|
||||||
|
'(begin
|
||||||
|
(eval '(module provide/contract41-m1 racket/base
|
||||||
|
(require racket/contract)
|
||||||
|
(provide/contract
|
||||||
|
#:forall (x)
|
||||||
|
[f (-> x (-> x x) x)])
|
||||||
|
(define (f x g) (g x))))
|
||||||
|
|
||||||
|
(eval '(module provide/contract41-m2 racket/base
|
||||||
|
(require racket/contract 'provide/contract41-m1)
|
||||||
|
(provide provide/contract41-x)
|
||||||
|
(define provide/contract41-x (f 10 (λ (x) x)))))
|
||||||
|
|
||||||
|
(eval '(require 'provide/contract41-m2))
|
||||||
|
(eval 'provide/contract41-x))
|
||||||
|
10)
|
||||||
|
|
||||||
|
(test/spec-passed/result
|
||||||
|
'provide/contract42
|
||||||
|
'(begin
|
||||||
|
(eval '(module provide/contract42-m1 racket/base
|
||||||
|
(require racket/contract)
|
||||||
|
(define x integer?)
|
||||||
|
(define g 11)
|
||||||
|
(provide/contract
|
||||||
|
[g x]
|
||||||
|
#:forall (x)
|
||||||
|
[f (-> x (-> x x) x)])
|
||||||
|
(define (f x g) (g x))))
|
||||||
|
|
||||||
|
(eval '(module provide/contract42-m2 racket/base
|
||||||
|
(require racket/contract 'provide/contract42-m1)
|
||||||
|
(provide provide/contract42-x)
|
||||||
|
(define provide/contract42-x (f 10 (λ (x) x)))))
|
||||||
|
|
||||||
|
(eval '(require 'provide/contract42-m2))
|
||||||
|
(eval 'provide/contract42-x))
|
||||||
|
10)
|
||||||
|
|
||||||
(contract-error-test
|
(contract-error-test
|
||||||
'contract-error-test8
|
'contract-error-test8
|
||||||
|
|
Loading…
Reference in New Issue
Block a user