From a41ba9d37f2c352d176b5b6a7088f93a67e25fd1 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Wed, 24 Sep 2014 16:51:34 -0500 Subject: [PATCH] add stronger for parametric->/c MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit (and test cases for stronger with new-∀/c) --- .../tests/racket/contract/stronger.rkt | 6 ++++++ .../racket/contract/private/parametric.rkt | 21 ++++++++++++++++++- 2 files changed, 26 insertions(+), 1 deletion(-) diff --git a/pkgs/racket-pkgs/racket-test/tests/racket/contract/stronger.rkt b/pkgs/racket-pkgs/racket-test/tests/racket/contract/stronger.rkt index 4e810aa9d3..141660f596 100644 --- a/pkgs/racket-pkgs/racket-test/tests/racket/contract/stronger.rkt +++ b/pkgs/racket-pkgs/racket-test/tests/racket/contract/stronger.rkt @@ -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))))) diff --git a/racket/collects/racket/contract/private/parametric.rkt b/racket/collects/racket/contract/private/parametric.rkt index fd2ed00969..ec781c5062 100644 --- a/racket/collects/racket/contract/private/parametric.rkt +++ b/racket/collects/racket/contract/private/parametric.rkt @@ -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))