suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Allow separate read and write contracts for box/c

Browse Source
This commit is contained in:
Alex Knauth 2015-10-23 17:24:53 -04:00 committed by Robby Findler
parent c0209b1d80
commit 67e3899272
3 changed files with 91 additions and 48 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
pkgs/racket-doc/scribblings/reference/contracts.scrbl
View File

@ -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.

29
pkgs/racket-test/tests/racket/contract/box.rkt
View File

@ -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))))

102
racket/collects/racket/contract/private/box.rkt
View File

@ -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)])))