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

add stronger for parametric->/c

Browse Source 
(and test cases for stronger with new-∀/c)
This commit is contained in:
Robby Findler 2014-09-24 16:51:34 -05:00
parent 1f1479c7be
commit a41ba9d37f
2 changed files with 26 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
pkgs/racket-pkgs/racket-test/tests/racket/contract/stronger.rkt
View File

@ -233,6 +233,12 @@
(ctest #t contract-stronger? (syntax/c (<=/c 3)) (syntax/c (<=/c 4)))
(ctest #f contract-stronger? (syntax/c (<=/c 4)) (syntax/c (<=/c 3)))
(ctest #t contract-stronger? (parametric->/c (x) (-> x x)) (parametric->/c (x) (-> x (or/c x #f))))
(ctest #f contract-stronger? (parametric->/c (x y) (-> x y)) (parametric->/c (x y) (-> x x y)))
(contract-eval `(define α (new-∀/c)))
(ctest #t contract-stronger? (-> α α) (-> α (or/c #f α)))
(ctest #f contract-stronger? (-> α (or/c #f α)) (-> α α))
(ctest #t contract-stronger?
(class/c (m (-> any/c (<=/c 3))))
(class/c (m (-> any/c (<=/c 4)))))

21
racket/collects/racket/contract/private/parametric.rkt
View File

@ -30,6 +30,24 @@
#:name
(lambda (c)
`(parametric->/c ,(polymorphic-contract-vars c) ,(polymorphic-contract-body-src-exp c)))
#:stronger
(λ (this that)
(cond
[(polymorphic-contract? that)
(define this-vars (polymorphic-contract-vars this))
(define that-vars (polymorphic-contract-vars that))
(define this-barrier/c (polymorphic-contract-barrier this))
(define that-barrier/c (polymorphic-contract-barrier that))
(cond
[(and (eq? this-barrier/c that-barrier/c)
(= (length this-vars) (length that-vars)))
(define instances
(for/list ([var (in-list this-vars)])
(this-barrier/c #t var)))
(contract-stronger? (apply (polymorphic-contract-body this) instances)
(apply (polymorphic-contract-body that) instances))]
[else #f])]
[else #f]))
#:projection
(lambda (c)
(lambda (orig-blame)
@ -66,7 +84,7 @@
(define (opaque/c positive? name)
(define-values [ type make pred getter setter ]
(make-struct-type name #f 1 0))
(define (get x) (getter x 0))
(define get (make-struct-field-accessor getter 0))
(make-barrier-contract name positive? make pred get))
(define-struct barrier-contract [name positive? make pred get]
@ -75,6 +93,7 @@
(build-contract-property
#:name (lambda (c) (barrier-contract-name c))
#:first-order (λ (c) (barrier-contract-pred c))
#:stronger (λ (this that) (eq? this that))
#:projection
(lambda (c)
(define mk (barrier-contract-make c))