From 67e3899272792c2e510abdf39865b3a40dfd8a8d Mon Sep 17 00:00:00 2001 From: Alex Knauth Date: Fri, 23 Oct 2015 17:24:53 -0400 Subject: [PATCH] Allow separate read and write contracts for box/c --- .../scribblings/reference/contracts.scrbl | 8 +- .../racket-test/tests/racket/contract/box.rkt | 29 +++++ .../collects/racket/contract/private/box.rkt | 102 ++++++++++-------- 3 files changed, 91 insertions(+), 48 deletions(-) diff --git a/pkgs/racket-doc/scribblings/reference/contracts.scrbl b/pkgs/racket-doc/scribblings/reference/contracts.scrbl index 6360ea9e34..d22ffc44cc 100644 --- a/pkgs/racket-doc/scribblings/reference/contracts.scrbl +++ b/pkgs/racket-doc/scribblings/reference/contracts.scrbl @@ -363,14 +363,16 @@ Returns the same contract as @racket[(vector/c c ... #:immutable #t)]. This form reasons of backwards compatibility.} -@defproc[(box/c [c contract?] +@defproc[(box/c [in-c contract?] + [c contract? in-c] [#:immutable immutable (or/c #t #f 'dont-care) 'dont-care] [#:flat? flat? boolean? #f]) contract?]{ -Returns a contract that recognizes boxes. The content of the box must match @racket[c]. +Returns a contract that recognizes boxes. The content of the box must match @racket[c], +and mutations on mutable boxes must match @racket[in-c]. If the @racket[flat?] argument is @racket[#t], then the resulting contract is -a flat contract, and the @racket[c] argument must also be a flat contract. Such +a flat contract, and the @racket[out] argument must also be a flat contract. Such flat contracts will be unsound if applied to mutable boxes, as they will not check future operations on the box. diff --git a/pkgs/racket-test/tests/racket/contract/box.rkt b/pkgs/racket-test/tests/racket/contract/box.rkt index 083c8f2438..4538f25f34 100644 --- a/pkgs/racket-test/tests/racket/contract/box.rkt +++ b/pkgs/racket-test/tests/racket/contract/box.rkt @@ -6,6 +6,18 @@ (λ (box v) v) (λ (box v) v))]) (contract (box/c any/c) v 'pos 'neg))) + + (test/no-error + '(let ([v (chaperone-box (box-immutable 1) + (λ (box v) v) + (λ (box v) v))]) + (contract (box/c none/c any/c) v 'pos 'neg))) + + (test/no-error + '(let ([v (chaperone-box (box 1) + (λ (box v) v) + (λ (box v) v))]) + (set-box! (contract (box/c boolean? none/c) v 'pos 'neg) #t))) (test/pos-blame 'box/c1 @@ -30,10 +42,18 @@ (test/neg-blame 'box/c6 '(set-box! (contract (box/c boolean?) (box #f) 'pos 'neg) 11)) + + (test/neg-blame + 'box/c6 + '(set-box! (contract (box/c boolean? any/c) (box #f) 'pos 'neg) 11)) (test/neg-blame 'box/c7 '(set-box! (contract (box/c boolean?) (box 12) 'pos 'neg) 11)) + + (test/neg-blame + 'box/c7 + '(set-box! (contract (box/c boolean? any/c) (box 12) 'pos 'neg) 11)) (test/neg-blame @@ -43,4 +63,13 @@ (box (list values)) 'pos 'neg)]) + ((car (unbox f)) 3))) + + (test/neg-blame + 'box/c-with-cons/c-inside + '(let ([f + (contract (box/c (cons/c (-> boolean? boolean?) '()) any/c) + (box (list values)) + 'pos + 'neg)]) ((car (unbox f)) 3)))) diff --git a/racket/collects/racket/contract/private/box.rkt b/racket/collects/racket/contract/private/box.rkt index b6a8bd8ef7..5f2c1a2e2b 100644 --- a/racket/collects/racket/contract/private/box.rkt +++ b/racket/collects/racket/contract/private/box.rkt @@ -12,10 +12,9 @@ (define/subexpression-pos-prop (box-immutable/c elem) (box/c elem #:immutable #t)) -(define-struct base-box/c (content immutable)) +(define-struct base-box/c (content-w content-r immutable)) (define (check-box/c ctc val blame) - (define elem-ctc (base-box/c-content ctc)) (define immutable (base-box/c-immutable ctc)) (unless (box? val) (raise-blame-error blame val '(expected "a box" given: "~e") val)) @@ -29,7 +28,6 @@ [(dont-care) (void)])) (define (check-box/c-np ctc val blame) - (define elem-ctc (base-box/c-content ctc)) (define immutable (base-box/c-immutable ctc)) (cond [(box? val) @@ -55,7 +53,7 @@ val '(expected "a box" given: "~e") val))])) (define (box/c-first-order ctc) - (define elem-ctc (base-box/c-content ctc)) + (define elem-r-ctc (base-box/c-content-r ctc)) (define immutable (base-box/c-immutable ctc)) (λ (val) (and (box? val) @@ -63,43 +61,50 @@ [(#t) (immutable? val)] [(#f) (not (immutable? val))] [(dont-care) #t]) - (contract-first-order-passes? elem-ctc (unbox val))))) + (contract-first-order-passes? elem-r-ctc (unbox val))))) (define (box/c-name ctc) - (let ([elem-name (contract-name (base-box/c-content ctc))] + (let ([elem-w-name (contract-name (base-box/c-content-w ctc))] + [elem-r-name (contract-name (base-box/c-content-r ctc))] [immutable (base-box/c-immutable ctc)] [flat? (flat-box/c? ctc)]) (apply build-compound-type-name 'box/c - elem-name - (if (and flat? (eq? immutable #t)) - (list '#:immutable #t) - (append - (if (not (eq? immutable 'dont-care)) - (list '#:immutable immutable) - null) - (if flat? - (list '#:flat? #t) - null)))))) + elem-w-name + (append + (if (not (equal? elem-w-name elem-r-name)) + (list elem-r-name) + null) + (if (and flat? (eq? immutable #t)) + (list '#:immutable #t) + (append + (if (not (eq? immutable 'dont-care)) + (list '#:immutable immutable) + null) + (if flat? + (list '#:flat? #t) + null))))))) (define (add-box-context blame) (blame-add-context blame "the content of")) (define (box/c-stronger this that) - (define this-content (base-box/c-content this)) + (define this-content-w (base-box/c-content-w this)) + (define this-content-r (base-box/c-content-r this)) (define this-immutable (base-box/c-immutable this)) (cond [(base-box/c? that) - (define that-content (base-box/c-content that)) + (define that-content-w (base-box/c-content-w that)) + (define that-content-r (base-box/c-content-r that)) (define that-immutable (base-box/c-immutable that)) (cond [(and (equal? this-immutable #t) (equal? that-immutable #t)) - (contract-stronger? this-content that-content)] + (contract-stronger? this-content-r that-content-r)] [(or (equal? that-immutable 'dont-care) (equal? this-immutable that-immutable)) - (and (contract-stronger? this-content that-content) - (contract-stronger? that-content this-content))] + (and (contract-stronger? this-content-r that-content-r) + (contract-stronger? that-content-w this-content-w))] [else #f])] [else #f])) @@ -113,7 +118,7 @@ #:stronger box/c-stronger #:late-neg-projection (λ (ctc) - (define content-ctc (get/build-late-neg-projection (base-box/c-content ctc))) + (define content-ctc (get/build-late-neg-projection (base-box/c-content-w ctc))) (λ (blame) (define box-blame (add-box-context blame)) (define late-neg-proj (content-ctc box-blame)) @@ -129,35 +134,38 @@ (λ (blame) (λ (val) (check-box/c ctc val blame) - (((contract-projection (base-box/c-content ctc)) blame) (unbox val)) + (((contract-projection (base-box/c-content-w ctc)) blame) (unbox val)) val))))) (define (ho-projection box-wrapper) (λ (ctc) - (let ([elem-ctc (base-box/c-content ctc)] + (let ([elem-w-ctc (base-box/c-content-w ctc)] + [elem-r-ctc (base-box/c-content-r ctc)] [immutable (base-box/c-immutable ctc)]) (λ (blame) - (let ([pos-elem-proj ((contract-projection elem-ctc) blame)] - [neg-elem-proj ((contract-projection elem-ctc) (blame-swap blame))]) + (let ([pos-elem-r-proj ((contract-projection elem-r-ctc) blame)] + [neg-elem-w-proj ((contract-projection elem-w-ctc) (blame-swap blame))]) (λ (val) (check-box/c ctc val blame) (if (and (immutable? val) (not (chaperone? val))) - (box-immutable (pos-elem-proj (unbox val))) + (box-immutable (pos-elem-r-proj (unbox val))) (box-wrapper val - (λ (b v) (pos-elem-proj v)) - (λ (b v) (neg-elem-proj v)) + (λ (b v) (pos-elem-r-proj v)) ; unbox-proc + (λ (b v) (neg-elem-w-proj v)) ; set-proc impersonator-prop:contracted ctc impersonator-prop:blame blame)))))))) (define (ho-late-neg-projection chaperone/impersonate-box) (λ (ctc) - (define elem-ctc (base-box/c-content ctc)) + (define elem-w-ctc (base-box/c-content-w ctc)) + (define elem-r-ctc (base-box/c-content-r ctc)) (define immutable (base-box/c-immutable ctc)) - (define vfp (get/build-late-neg-projection elem-ctc)) + (define w-vfp (get/build-late-neg-projection elem-w-ctc)) + (define r-vfp (get/build-late-neg-projection elem-r-ctc)) (λ (blame) (define box-blame (add-box-context blame)) - (define pos-elem-proj (vfp box-blame)) - (define neg-elem-proj (vfp (blame-swap box-blame))) + (define pos-elem-r-proj (r-vfp box-blame)) + (define neg-elem-w-proj (w-vfp (blame-swap box-blame))) (λ (val neg-party) (cond [(check-box/c-np ctc val blame) @@ -165,11 +173,11 @@ (λ (f) (f neg-party))] [else (if (and (immutable? val) (not (chaperone? val))) - (box-immutable (pos-elem-proj (unbox val) neg-party)) + (box-immutable (pos-elem-r-proj (unbox val) neg-party)) (chaperone/impersonate-box val - (λ (b v) (pos-elem-proj v neg-party)) - (λ (b v) (neg-elem-proj v neg-party)) + (λ (b v) (pos-elem-r-proj v neg-party)) + (λ (b v) (neg-elem-w-proj v neg-party)) impersonator-prop:contracted ctc impersonator-prop:blame (blame-add-missing-party blame neg-party)))]))))) @@ -231,17 +239,21 @@ 'racket/contract:contract (vector this-one (list #'b/c) null))))])) -(define (box/c elem #:immutable [immutable 'dont-care] #:flat? [flat? #f]) - (let ([ctc (if flat? - (coerce-flat-contract 'box/c elem) - (coerce-contract 'box/c elem))]) +(define (box/c elem-w [elem-r elem-w] #:immutable [immutable 'dont-care] #:flat? [flat? #f]) + (let ([ctc-w (if flat? + (coerce-flat-contract 'box/c elem-w) + (coerce-contract 'box/c elem-w))] + [ctc-r (if flat? + (coerce-flat-contract 'box/c elem-r) + (coerce-contract 'box/c elem-w))]) (cond [(or flat? (and (eq? immutable #t) - (flat-contract? ctc))) - (make-flat-box/c ctc immutable)] - [(chaperone-contract? ctc) - (make-chaperone-box/c ctc immutable)] + (flat-contract? ctc-r))) + (make-flat-box/c ctc-w ctc-r immutable)] + [(and (chaperone-contract? ctc-w) + (chaperone-contract? ctc-r)) + (make-chaperone-box/c ctc-w ctc-r immutable)] [else - (make-impersonator-box/c ctc immutable)]))) + (make-impersonator-box/c ctc-w ctc-r immutable)])))