added exists to provide/contract
svn: r15871
This commit is contained in:
Robby Findler
parent
5d000d425e
commit
937d2efab3
|
|
@ -15,7 +15,8 @@ improve method arity mismatch contract violation error messages?
|
|||
define-struct/contract
|
||||
define/contract
|
||||
with-contract
|
||||
current-contract-region)
|
||||
current-contract-region
|
||||
new-∃/c)
|
||||
|
||||
(require (for-syntax scheme/base)
|
||||
(for-syntax "contract-opt-guts.ss")
|
||||
|
|
@ -683,9 +684,6 @@ improve method arity mismatch contract violation error messages?
|
|||
(quasisyntax/loc stx (#%expression #,stx)))))))
|
||||
|
||||
|
||||
;; (provide/contract p/c-ele ...)
|
||||
;; p/c-ele = (id expr) | (rename id id expr) | (struct id (id expr) ...)
|
||||
;; provides each `id' with the contract `expr'.
|
||||
(define-syntax (provide/contract provide-stx)
|
||||
(syntax-case provide-stx (struct)
|
||||
[(_ p/c-ele ...)
|
||||
|
|
@ -725,19 +723,62 @@ improve method arity mismatch contract violation error messages?
|
|||
;; code-for-each-clause : (listof syntax) -> (listof syntax)
|
||||
;; constructs code for each clause of a provide/contract
|
||||
(define (code-for-each-clause clauses)
|
||||
(cond
|
||||
(let loop ([clauses clauses]
|
||||
[exists-binders '()])
|
||||
(cond
|
||||
[(null? clauses) null]
|
||||
[else
|
||||
(let ([clause (car clauses)])
|
||||
;; 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)))
|
||||
[exists
|
||||
(or (eq? '#:exists (syntax-e #'exists)) (eq? '#:∃ (syntax-e #'exists)))
|
||||
(cond
|
||||
[(null? (cdr clauses))
|
||||
(raise-syntax-error 'provide/conract
|
||||
(format "expected either a single variable or a sequence of variables to follow ~a, but found nothing"
|
||||
(syntax-e #'exists))
|
||||
provide-stx
|
||||
clause)]
|
||||
[else
|
||||
(syntax-case (cadr clauses) ()
|
||||
[x
|
||||
(identifier? #'x)
|
||||
(with-syntax ([(x-gen) (generate-temporaries #'(x))])
|
||||
(cons (code-for-one-exists-id #'x #'x-gen)
|
||||
(loop (cddr clauses)
|
||||
(add-a-binder #'x #'x-gen exists-binders))))]
|
||||
[(x ...)
|
||||
(andmap identifier? (syntax->list #'(x ...)))
|
||||
(with-syntax ([(x-gen ...) (generate-temporaries #'(x ...))])
|
||||
(append (map code-for-one-exists-id
|
||||
(syntax->list #'(x ...))
|
||||
(syntax->list #'(x-gen ...)))
|
||||
(loop (cddr clauses)
|
||||
(let loop ([binders exists-binders]
|
||||
[xs (syntax->list #'(x ...))]
|
||||
[x-gens (syntax->list #'(x-gen ...))])
|
||||
(cond
|
||||
[(null? xs) binders]
|
||||
[else (loop (add-a-binder (car xs) (car x-gens) binders)
|
||||
(cdr xs)
|
||||
(cdr x-gens))])))))]
|
||||
[else
|
||||
(raise-syntax-error 'provide/contract
|
||||
(format "expected either a single variable or a sequence of variables to follow ~a"
|
||||
(syntax-e #'exists))
|
||||
provide-stx
|
||||
(cadr clauses))])])]
|
||||
[(rename this-name new-name contract)
|
||||
(and (identifier? (syntax this-name))
|
||||
(identifier? (syntax new-name)))
|
||||
(begin
|
||||
(add-to-dups-table #'new-name)
|
||||
(cons (code-for-one-id provide-stx (syntax this-name) (syntax contract) (syntax new-name))
|
||||
(code-for-each-clause (cdr clauses))))]
|
||||
(cons (code-for-one-id provide-stx
|
||||
(syntax this-name)
|
||||
(add-exists-binders (syntax contract) exists-binders)
|
||||
(syntax new-name))
|
||||
(loop (cdr clauses) exists-binders)))]
|
||||
[(rename this-name new-name contract)
|
||||
(identifier? (syntax this-name))
|
||||
(raise-syntax-error 'provide/contract
|
||||
|
|
@ -758,9 +799,10 @@ improve method arity mismatch contract violation error messages?
|
|||
(let ([sc (build-struct-code provide-stx
|
||||
(syntax struct-name)
|
||||
(syntax->list (syntax (field-name ...)))
|
||||
(syntax->list (syntax (contract ...))))])
|
||||
(map (λ (x) (add-exists-binders x exists-binders))
|
||||
(syntax->list (syntax (contract ...)))))])
|
||||
(add-to-dups-table #'struct-name)
|
||||
(cons sc (code-for-each-clause (cdr clauses))))]
|
||||
(cons sc (loop (cdr clauses) exists-binders)))]
|
||||
[(struct name)
|
||||
(identifier? (syntax name))
|
||||
(raise-syntax-error 'provide/contract
|
||||
|
|
@ -801,8 +843,12 @@ improve method arity mismatch contract violation error messages?
|
|||
(identifier? (syntax name))
|
||||
(begin
|
||||
(add-to-dups-table #'name)
|
||||
(cons (code-for-one-id provide-stx (syntax name) (syntax contract) #f)
|
||||
(code-for-each-clause (cdr clauses))))]
|
||||
(cons (code-for-one-id provide-stx
|
||||
(syntax name)
|
||||
(add-exists-binders (syntax contract)
|
||||
exists-binders)
|
||||
#f)
|
||||
(loop (cdr clauses) exists-binders)))]
|
||||
[(name contract)
|
||||
(raise-syntax-error 'provide/contract
|
||||
"expected identifier"
|
||||
|
|
@ -812,7 +858,7 @@ improve method arity mismatch contract violation error messages?
|
|||
(raise-syntax-error 'provide/contract
|
||||
"malformed clause"
|
||||
provide-stx
|
||||
(syntax unk))]))]))
|
||||
(syntax unk))]))])))
|
||||
|
||||
;; well-formed-struct-name? : syntax -> bool
|
||||
(define (well-formed-struct-name? stx)
|
||||
|
|
@ -1159,6 +1205,16 @@ improve method arity mismatch contract violation error messages?
|
|||
field-contract-id
|
||||
void?))))
|
||||
|
||||
;; 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))
|
||||
|
||||
(define (add-a-binder id id-gen binders)
|
||||
(cons #`[#,id #,id-gen] binders))
|
||||
|
||||
;; code-for-one-id : syntax syntax syntax (union syntax #f) -> syntax
|
||||
;; given the syntax for an identifier and a contract,
|
||||
;; builds a begin expression for the entire contract and provide
|
||||
|
|
@ -1209,7 +1265,9 @@ improve method arity mismatch contract violation error messages?
|
|||
|
||||
#,@(if no-need-to-check-ctrct?
|
||||
(list)
|
||||
(list #'(define contract-id (verify-contract 'provide/contract ctrct))))
|
||||
(list #'(define contract-id
|
||||
(let ([id ctrct]) ;; let is here to give the right name.
|
||||
(verify-contract 'provide/contract id)))))
|
||||
(define-syntax id-rename
|
||||
(make-provide/contract-transformer (quote-syntax contract-id)
|
||||
(quote-syntax id)
|
||||
|
|
@ -2571,3 +2629,33 @@ improve method arity mismatch contract violation error messages?
|
|||
#:property stronger-prop
|
||||
(λ (this that)
|
||||
#f))
|
||||
|
||||
(define (∃-proj ctc)
|
||||
(let ([in (∃/c-in ctc)]
|
||||
[out (∃/c-out ctc)]
|
||||
[pred? (∃/c-pred? ctc)])
|
||||
(λ (pos-blame neg-blame src-info orig-str positive-position?)
|
||||
(if positive-position?
|
||||
in
|
||||
(λ (val)
|
||||
(if (pred? val)
|
||||
(out val)
|
||||
(raise-contract-error val src-info pos-blame orig-str
|
||||
"non-polymorphic value: ~e"
|
||||
val)))))))
|
||||
|
||||
(define-struct ∃/c (in out pred? name)
|
||||
#:omit-define-syntaxes
|
||||
#:property proj-prop ∃-proj
|
||||
#:property name-prop (λ (ctc) (∃/c-name ctc))
|
||||
#:property first-order-prop
|
||||
(λ (ctc) (λ (x) #t)) ;; ???
|
||||
|
||||
#:property stronger-prop
|
||||
(λ (this that) #f))
|
||||
|
||||
(define (new-∃/c raw-name)
|
||||
(define name (string->symbol (format "~a/∃" raw-name)))
|
||||
(define-values (struct-type constructor predicate accessor mutator)
|
||||
(make-struct-type name #f 1 0))
|
||||
(make-∃/c constructor (λ (x) (accessor x 0)) predicate raw-name))
|
||||
|
|
|
|||
|
|
@ -11,6 +11,10 @@ another. Programmers specify the behavior of a module exports via
|
|||
@scheme[provide/contract] and the contract system enforces those
|
||||
constraints.
|
||||
|
||||
@note-lib[scheme/contract #:use-sources (scheme/private/contract-ds
|
||||
scheme/private/contract
|
||||
scheme/private/contract-guts)]
|
||||
|
||||
@deftech{Contracts} come in two forms: those constructed by the
|
||||
various operations listed in this section of the manual, and various
|
||||
ordinary Scheme values that double as contracts, including
|
||||
|
|
@ -34,10 +38,6 @@ failed, and anything else to indicate it passed.}
|
|||
|
||||
]
|
||||
|
||||
@note-lib[scheme/contract #:use-sources (scheme/private/contract-ds
|
||||
scheme/private/contract
|
||||
scheme/private/contract-guts)]
|
||||
|
||||
@local-table-of-contents[]
|
||||
|
||||
@; ----------------------------------------
|
||||
|
|
@ -368,6 +368,27 @@ Constructs a contract on a promise. The contract does not force the
|
|||
promise, but when the promise is forced, the contract checks that the
|
||||
result value meets the contract produced by @scheme[expr].}
|
||||
|
||||
@defproc[(new-∃/c [name symbol?]) contract?]{
|
||||
Constructs a new existential contract.
|
||||
|
||||
Existential contracts accept all values when in positive positions (e.g., function
|
||||
returns) and wraps the value in an opaque struct, hiding the precise value.
|
||||
In negative positions (e.g. function inputs),
|
||||
it accepts only values that were previously accepted in negative positions (by checking
|
||||
for the wrappers).
|
||||
|
||||
For example, this contract:
|
||||
@schemeblock[(let ([a (new-∃/c 'a)])
|
||||
(-> (-> a a)
|
||||
any/c))]
|
||||
describes a function that accepts the identity function (or a non-terminating function)
|
||||
and returns an arbitrary value. That is, the first use of the @scheme[a] appears in a
|
||||
positive position and thus inputs to that function are wrapped with an opaque struct.
|
||||
Then, when the function returns, it is checked to see if the result is wrapped, since
|
||||
the second @scheme[a] appears in a negative position.
|
||||
|
||||
}
|
||||
|
||||
@; ------------------------------------------------------------------------
|
||||
|
||||
@section{Function Contracts}
|
||||
|
|
@ -669,7 +690,11 @@ lazy contract.}
|
|||
(struct id ((id contract-expr) ...))
|
||||
(struct (id identifier) ((id contract-expr) ...))
|
||||
(rename orig-id id contract-expr)
|
||||
(id contract-expr)])]{
|
||||
(id contract-expr)
|
||||
(code:line #:∃ exists-variables)
|
||||
(code:line #:exists exists-variables)]
|
||||
[exists-variables identifier
|
||||
(identifier ...)])]{
|
||||
|
||||
Can only appear at the top-level of a @scheme[module]. As with
|
||||
@scheme[provide], each @scheme[id] is provided from the module. In
|
||||
|
|
@ -699,7 +724,13 @@ referring to the parent struct. Unlike @scheme[define-struct],
|
|||
however, all of the fields (and their contracts) must be listed. The
|
||||
contract on the fields that the sub-struct shares with its parent are
|
||||
only used in the contract for the sub-struct's maker, and the selector
|
||||
or mutators for the super-struct are not provided.}
|
||||
or mutators for the super-struct are not provided.
|
||||
|
||||
The @scheme[#:∃] and @scheme[#:exists] clauses define new abstract
|
||||
contracts. The variables are bound in the remainder of the @scheme[provide/contract]
|
||||
expression to new contracts that hide the values they accept and
|
||||
ensure that the exported functions are treated parametrically.
|
||||
}
|
||||
|
||||
@defform/subs[
|
||||
(with-contract blame-id (wc-export ...) free-var-list body ...+)
|
||||
|
|
|
|||
|
|
@ -6153,6 +6153,52 @@ so that propagation occurs.
|
|||
'neg))
|
||||
(f 10)))
|
||||
|
||||
|
||||
;
|
||||
;
|
||||
;
|
||||
;
|
||||
;
|
||||
; ;;;;;;
|
||||
; ; ;
|
||||
; ; ;
|
||||
; ; ;; ;;;;
|
||||
; ;;;;;; ; ;;;;;;
|
||||
; ; ; ;;;
|
||||
; ; ; ;;;
|
||||
; ; ;; ;;;;;;
|
||||
; ;;;;;; ; ;;;;
|
||||
;
|
||||
;
|
||||
;
|
||||
;
|
||||
|
||||
(test/spec-passed
|
||||
'∃1
|
||||
'(contract (new-∃/c 'pair)
|
||||
1
|
||||
'pos
|
||||
'neg))
|
||||
|
||||
(test/neg-blame
|
||||
'∃2
|
||||
'((contract (-> (new-∃/c 'pair) any/c)
|
||||
(λ (x) x)
|
||||
'pos
|
||||
'neg)
|
||||
1))
|
||||
|
||||
(test/spec-passed/result
|
||||
'∃3
|
||||
'(let ([pair (new-∃/c 'pair)])
|
||||
((contract (-> (-> pair pair) any/c)
|
||||
(λ (f) (f 11))
|
||||
'pos
|
||||
'neg)
|
||||
(λ (x) x)))
|
||||
11)
|
||||
|
||||
|
||||
;
|
||||
;
|
||||
;
|
||||
|
|
@ -6683,6 +6729,104 @@ so that propagation occurs.
|
|||
(eval 'provide/contract29-res))
|
||||
(list #t 3))
|
||||
|
||||
;; for this test I have to be able to track back thru the requirees to find the right
|
||||
;; name for the negative blame (currently it blames m3, but it should blame m2).
|
||||
#;
|
||||
(test/spec-failed
|
||||
'provide/contract30
|
||||
'(begin
|
||||
(eval '(module provide/contract30-m1 scheme/base
|
||||
(require scheme/contract)
|
||||
(provide/contract [f (-> integer? integer?)])
|
||||
(define (f x) x)))
|
||||
(eval '(module provide/contract30-m2 scheme/base
|
||||
(require 'provide/contract30-m1)
|
||||
(provide f)))
|
||||
(eval '(module provide/contract30-m3 scheme/base
|
||||
(require 'provide/contract30-m2)
|
||||
(f #f)))
|
||||
(eval '(require 'provide/contract30-m3)))
|
||||
"'provide/contract30-m2")
|
||||
|
||||
(test/spec-passed/result
|
||||
'provide/contract31
|
||||
'(begin
|
||||
(eval '(module provide/contract31-m1 scheme/base
|
||||
(require scheme/contract)
|
||||
(provide/contract
|
||||
#:∃ x
|
||||
[f (-> (-> x x) 10)])
|
||||
(define (f g) (g 10))))
|
||||
|
||||
(eval '(module provide/contract31-m2 scheme/base
|
||||
(require scheme/contract 'provide/contract31-m1)
|
||||
(provide provide/contract31-x)
|
||||
(define provide/contract31-x (f (λ (x) x)))))
|
||||
|
||||
(eval '(require 'provide/contract31-m2))
|
||||
(eval 'provide/contract31-x))
|
||||
10)
|
||||
|
||||
(test/spec-passed/result
|
||||
'provide/contract32
|
||||
'(begin
|
||||
(eval '(module provide/contract32-m1 scheme/base
|
||||
(require scheme/contract)
|
||||
(provide/contract
|
||||
#:exists x
|
||||
[f (-> (-> x x) 10)])
|
||||
(define (f g) (g 10))))
|
||||
|
||||
(eval '(module provide/contract32-m2 scheme/base
|
||||
(require scheme/contract 'provide/contract32-m1)
|
||||
(provide provide/contract32-x)
|
||||
(define provide/contract32-x (f (λ (x) x)))))
|
||||
|
||||
(eval '(require 'provide/contract32-m2))
|
||||
(eval 'provide/contract32-x))
|
||||
10)
|
||||
|
||||
(test/spec-passed/result
|
||||
'provide/contract33
|
||||
'(begin
|
||||
(eval '(module provide/contract33-m1 scheme/base
|
||||
(require scheme/contract)
|
||||
(provide/contract
|
||||
#:exists (x)
|
||||
[f (-> (-> x x) 10)])
|
||||
(define (f g) (g 10))))
|
||||
|
||||
(eval '(module provide/contract33-m2 scheme/base
|
||||
(require scheme/contract 'provide/contract33-m1)
|
||||
(provide provide/contract33-x)
|
||||
(define provide/contract33-x (f (λ (x) x)))))
|
||||
|
||||
(eval '(require 'provide/contract33-m2))
|
||||
(eval 'provide/contract33-x))
|
||||
10)
|
||||
|
||||
(test/spec-passed/result
|
||||
'provide/contract34
|
||||
'(begin
|
||||
(eval '(module provide/contract34-m1 scheme/base
|
||||
(require scheme/contract)
|
||||
(define x integer?)
|
||||
(define g 11)
|
||||
(provide/contract
|
||||
[g x]
|
||||
#:exists (x)
|
||||
[f (-> (-> x x) 10)])
|
||||
(define (f g) (g 10))))
|
||||
|
||||
(eval '(module provide/contract34-m2 scheme/base
|
||||
(require scheme/contract 'provide/contract34-m1)
|
||||
(provide provide/contract34-x)
|
||||
(define provide/contract34-x (f (λ (x) x)))))
|
||||
|
||||
(eval '(require 'provide/contract34-m2))
|
||||
(eval 'provide/contract34-x))
|
||||
10)
|
||||
|
||||
(contract-error-test
|
||||
#'(begin
|
||||
(eval '(module pce1-bug scheme/base
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user