From 937d2efab3af91834a1796793a1894d765c3981e Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Fri, 4 Sep 2009 04:52:02 +0000 Subject: [PATCH] added exists to provide/contract svn: r15871 --- collects/scheme/private/contract.ss | 114 ++++++++++++-- .../scribblings/reference/contracts.scrbl | 43 +++++- collects/tests/mzscheme/contract-test.ss | 144 ++++++++++++++++++ 3 files changed, 282 insertions(+), 19 deletions(-) diff --git a/collects/scheme/private/contract.ss b/collects/scheme/private/contract.ss index 9375ec245f..3995cbc26b 100644 --- a/collects/scheme/private/contract.ss +++ b/collects/scheme/private/contract.ss @@ -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)) diff --git a/collects/scribblings/reference/contracts.scrbl b/collects/scribblings/reference/contracts.scrbl index 63bedcc9be..bb5a5223c5 100644 --- a/collects/scribblings/reference/contracts.scrbl +++ b/collects/scribblings/reference/contracts.scrbl @@ -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 ...+) diff --git a/collects/tests/mzscheme/contract-test.ss b/collects/tests/mzscheme/contract-test.ss index 4b75569c54..b1b480345a 100644 --- a/collects/tests/mzscheme/contract-test.ss +++ b/collects/tests/mzscheme/contract-test.ss @@ -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