vectorof contract: add some tests and make flat variant subscribe to the val-first protocol
This commit is contained in:
parent
7abf555a8a
commit
81cd1e3404
|
@ -465,6 +465,11 @@
|
||||||
'pos
|
'pos
|
||||||
'neg))
|
'neg))
|
||||||
|
|
||||||
|
(context-test '("an element of")
|
||||||
|
'(contract (vectorof integer? #:flat? #t)
|
||||||
|
(vector-immutable #f)
|
||||||
|
'pos 'neg))
|
||||||
|
|
||||||
(let* ([blame-pos (contract-eval '(make-blame (srcloc #f #f #f #f #f)
|
(let* ([blame-pos (contract-eval '(make-blame (srcloc #f #f #f #f #f)
|
||||||
#f
|
#f
|
||||||
(λ () 'integer?)
|
(λ () 'integer?)
|
||||||
|
|
|
@ -44,6 +44,48 @@
|
||||||
0 #f)))
|
0 #f)))
|
||||||
|
|
||||||
|
|
||||||
|
(test/pos-blame
|
||||||
|
'vectorof7
|
||||||
|
'(contract (vectorof integer? #:immutable #t)
|
||||||
|
(vector-immutable #f)
|
||||||
|
'pos 'neg))
|
||||||
|
|
||||||
|
(test/pos-blame
|
||||||
|
'vectorof8
|
||||||
|
'(contract (vectorof integer? #:immutable #t)
|
||||||
|
11
|
||||||
|
'pos 'neg))
|
||||||
|
|
||||||
|
(test/pos-blame
|
||||||
|
'vectorof9
|
||||||
|
'(contract (vectorof integer? #:immutable #t)
|
||||||
|
(vector 11)
|
||||||
|
'pos 'neg))
|
||||||
|
|
||||||
|
(test/spec-passed
|
||||||
|
'vectorof10
|
||||||
|
'(contract (vectorof integer? #:flat? #t)
|
||||||
|
(vector 11)
|
||||||
|
'pos 'neg))
|
||||||
|
|
||||||
|
(test/pos-blame
|
||||||
|
'vectorof10
|
||||||
|
'(contract (vectorof integer? #:flat? #t)
|
||||||
|
(vector #f)
|
||||||
|
'pos 'neg))
|
||||||
|
|
||||||
|
(test/pos-blame
|
||||||
|
'vectorof11
|
||||||
|
'(contract (vectorof integer? #:flat? #t)
|
||||||
|
(vector-immutable #f)
|
||||||
|
'pos 'neg))
|
||||||
|
|
||||||
|
(test/spec-passed
|
||||||
|
'vectorof12
|
||||||
|
'(contract (vectorof integer? #:flat? #t)
|
||||||
|
(vector-immutable 11)
|
||||||
|
'pos 'neg))
|
||||||
|
|
||||||
(test/spec-passed
|
(test/spec-passed
|
||||||
'vector/c1
|
'vector/c1
|
||||||
'(let ([v (chaperone-vector (vector-immutable 1)
|
'(let ([v (chaperone-vector (vector-immutable 1)
|
||||||
|
@ -82,4 +124,10 @@
|
||||||
(λ (vec i v) v)
|
(λ (vec i v) v)
|
||||||
(λ (vec i v) v))])
|
(λ (vec i v) v))])
|
||||||
(vector-set! (contract (vector/c integer?) v 'pos 'neg)
|
(vector-set! (contract (vector/c integer?) v 'pos 'neg)
|
||||||
0 #f))))
|
0 #f)))
|
||||||
|
|
||||||
|
(test/pos-blame
|
||||||
|
'vector/c6
|
||||||
|
'(contract (vector/c integer? #:immutable #t)
|
||||||
|
(vector-immutable #f)
|
||||||
|
'pos 'neg)))
|
||||||
|
|
|
@ -68,6 +68,34 @@
|
||||||
(fail val '(expected: "~s for element ~s" given: "~e") (contract-name elem-ctc) n e))))
|
(fail val '(expected: "~s for element ~s" given: "~e") (contract-name elem-ctc) n e))))
|
||||||
#t)))
|
#t)))
|
||||||
|
|
||||||
|
(define (check-val-first-vectorof c)
|
||||||
|
(define immutable (base-vectorof-immutable c))
|
||||||
|
(λ (val blame)
|
||||||
|
(cond
|
||||||
|
[(vector? val)
|
||||||
|
(cond
|
||||||
|
[(eq? immutable #t)
|
||||||
|
(cond
|
||||||
|
[(immutable? val) #f]
|
||||||
|
[else
|
||||||
|
(λ (neg-party)
|
||||||
|
(raise-blame-error blame #:missing-party neg-party
|
||||||
|
val '(expected "an immutable vector" given: "~e") val))])]
|
||||||
|
[(eq? immutable #f)
|
||||||
|
(cond
|
||||||
|
[(immutable? val)
|
||||||
|
(λ (neg-party)
|
||||||
|
(raise-blame-error blame #:missing-party neg-party
|
||||||
|
val '(expected "an mutable vector" given: "~e" val)))]
|
||||||
|
[else #f])]
|
||||||
|
[else #f])]
|
||||||
|
[else
|
||||||
|
(λ (neg-party)
|
||||||
|
(raise-blame-error blame #:missing-party neg-party
|
||||||
|
val
|
||||||
|
'(expected "a vector," given: "~e")
|
||||||
|
val))])))
|
||||||
|
|
||||||
(define (vectorof-first-order ctc)
|
(define (vectorof-first-order ctc)
|
||||||
(let ([check (check-vectorof ctc)])
|
(let ([check (check-vectorof ctc)])
|
||||||
(λ (val)
|
(λ (val)
|
||||||
|
@ -80,6 +108,18 @@
|
||||||
(build-flat-contract-property
|
(build-flat-contract-property
|
||||||
#:name vectorof-name
|
#:name vectorof-name
|
||||||
#:first-order vectorof-first-order
|
#:first-order vectorof-first-order
|
||||||
|
#:val-first-projection (λ (ctc)
|
||||||
|
(define check (check-val-first-vectorof ctc))
|
||||||
|
(define vfp (get/build-val-first-projection (base-vectorof-elem ctc)))
|
||||||
|
(λ (blame)
|
||||||
|
(define ele-blame (blame-add-element-of-context blame))
|
||||||
|
(define vfp+blame (vfp ele-blame))
|
||||||
|
(λ (val)
|
||||||
|
(or (check val blame)
|
||||||
|
(λ (neg-party)
|
||||||
|
(for ([x (in-vector val)])
|
||||||
|
((vfp+blame x) neg-party))
|
||||||
|
val)))))
|
||||||
#:projection
|
#:projection
|
||||||
(λ (ctc)
|
(λ (ctc)
|
||||||
(define check (check-vectorof ctc))
|
(define check (check-vectorof ctc))
|
||||||
|
@ -94,16 +134,20 @@
|
||||||
(p e)))
|
(p e)))
|
||||||
val)))))
|
val)))))
|
||||||
|
|
||||||
|
(define (blame-add-element-of-context blame #:swap? [swap? #f])
|
||||||
|
(blame-add-context blame "an element of" #:swap? swap?))
|
||||||
|
|
||||||
(define (vectorof-val-first-ho-projection chaperone-or-impersonate-vector)
|
(define (vectorof-val-first-ho-projection chaperone-or-impersonate-vector)
|
||||||
(λ (ctc)
|
(λ (ctc)
|
||||||
(define elem-ctc (base-vectorof-elem ctc))
|
(define elem-ctc (base-vectorof-elem ctc))
|
||||||
(define immutable (base-vectorof-immutable ctc))
|
(define immutable (base-vectorof-immutable ctc))
|
||||||
(define check (check-vectorof ctc))
|
(define check (check-vectorof ctc))
|
||||||
(λ (blame)
|
(λ (blame)
|
||||||
(define pos-blame (blame-add-context blame "an element of"))
|
(define pos-blame (blame-add-element-of-context blame))
|
||||||
(define neg-blame (blame-add-context blame "an element of" #:swap? #t))
|
(define neg-blame (blame-add-element-of-context blame #:swap? #t))
|
||||||
(define elem-pos-proj ((get/build-val-first-projection elem-ctc) pos-blame))
|
(define vfp (get/build-val-first-projection elem-ctc))
|
||||||
(define elem-neg-proj ((get/build-val-first-projection elem-ctc) neg-blame))
|
(define elem-pos-proj (vfp pos-blame))
|
||||||
|
(define elem-neg-proj (vfp neg-blame))
|
||||||
(define checked-ref (λ (neg-party)
|
(define checked-ref (λ (neg-party)
|
||||||
(λ (vec i val)
|
(λ (vec i val)
|
||||||
(with-continuation-mark
|
(with-continuation-mark
|
||||||
|
@ -144,8 +188,10 @@
|
||||||
[immutable (base-vectorof-immutable ctc)]
|
[immutable (base-vectorof-immutable ctc)]
|
||||||
[check (check-vectorof ctc)])
|
[check (check-vectorof ctc)])
|
||||||
(λ (blame)
|
(λ (blame)
|
||||||
(let ([elem-pos-proj ((contract-projection elem-ctc) (blame-add-context blame "an element of"))]
|
(let ([elem-pos-proj ((contract-projection elem-ctc)
|
||||||
[elem-neg-proj ((contract-projection elem-ctc) (blame-add-context blame "an element of" #:swap? #t))])
|
(blame-add-element-of-context blame))]
|
||||||
|
[elem-neg-proj ((contract-projection elem-ctc)
|
||||||
|
(blame-add-element-of-context blame #:swap? #t))])
|
||||||
(define checked-ref (λ (vec i val)
|
(define checked-ref (λ (vec i val)
|
||||||
(with-continuation-mark
|
(with-continuation-mark
|
||||||
contract-continuation-mark-key blame
|
contract-continuation-mark-key blame
|
||||||
|
@ -204,19 +250,20 @@
|
||||||
'racket/contract:contract
|
'racket/contract:contract
|
||||||
(vector this-one (list #'vecof) null))))]))
|
(vector this-one (list #'vecof) null))))]))
|
||||||
|
|
||||||
(define (vectorof c #:immutable [immutable 'dont-care] #:flat? [flat? #f])
|
(define/subexpression-pos-prop (vectorof c #:immutable [immutable 'dont-care] #:flat? [flat? #f])
|
||||||
(let ([ctc (if flat?
|
(define ctc
|
||||||
|
(if flat?
|
||||||
(coerce-flat-contract 'vectorof c)
|
(coerce-flat-contract 'vectorof c)
|
||||||
(coerce-contract 'vectorof c))])
|
(coerce-contract 'vectorof c)))
|
||||||
(cond
|
(cond
|
||||||
[(or flat?
|
[(or flat?
|
||||||
(and (eq? immutable #t)
|
(and (equal? immutable #t)
|
||||||
(flat-contract? ctc)))
|
(flat-contract? ctc)))
|
||||||
(make-flat-vectorof ctc immutable)]
|
(make-flat-vectorof ctc immutable)]
|
||||||
[(chaperone-contract? ctc)
|
[(chaperone-contract? ctc)
|
||||||
(make-chaperone-vectorof ctc immutable)]
|
(make-chaperone-vectorof ctc immutable)]
|
||||||
[else
|
[else
|
||||||
(make-impersonator-vectorof ctc immutable)])))
|
(make-impersonator-vectorof ctc immutable)]))
|
||||||
|
|
||||||
(define/subexpression-pos-prop (vector-immutableof c)
|
(define/subexpression-pos-prop (vector-immutableof c)
|
||||||
(vectorof c #:immutable #t))
|
(vectorof c #:immutable #t))
|
||||||
|
@ -283,7 +330,7 @@
|
||||||
#:projection
|
#:projection
|
||||||
(λ (ctc)
|
(λ (ctc)
|
||||||
(λ (blame)
|
(λ (blame)
|
||||||
(define blame+ctxt (blame-add-context blame "an element of"))
|
(define blame+ctxt (blame-add-element-of-context blame))
|
||||||
(λ (val)
|
(λ (val)
|
||||||
(with-continuation-mark
|
(with-continuation-mark
|
||||||
contract-continuation-mark-key blame
|
contract-continuation-mark-key blame
|
||||||
|
@ -308,7 +355,8 @@
|
||||||
([c (in-list elem-ctcs)]
|
([c (in-list elem-ctcs)]
|
||||||
[i (in-naturals)])
|
[i (in-naturals)])
|
||||||
((contract-projection c)
|
((contract-projection c)
|
||||||
(blame-add-context blame (format "the ~a element of" (n->th i)) #:swap? #t)))])
|
(blame-add-context blame (format "the ~a element of" (n->th i))
|
||||||
|
#:swap? #t)))])
|
||||||
(λ (val)
|
(λ (val)
|
||||||
(check-vector/c ctc val blame)
|
(check-vector/c ctc val blame)
|
||||||
(if (and (immutable? val) (not (chaperone? val)))
|
(if (and (immutable? val) (not (chaperone? val)))
|
||||||
|
|
Loading…
Reference in New Issue
Block a user