From d93803cdeb39add1f832e549e541c835e5b74d37 Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Sun, 17 Jun 2012 22:14:19 -0700 Subject: [PATCH] Make TR compile cleanly with contracts enabled. Added a couple of contracts and fixed some others up as well. The two bugs were that with-contract was not imported, and that subtype could be called with Values and Results. original commit: 030e56311ec9196131e321129023c9ef21f39b32 --- collects/typed-racket/infer/infer-unit.rkt | 86 +++++++++++----------- collects/typed-racket/infer/signatures.rkt | 10 +-- collects/typed-racket/types/abbrev.rkt | 5 +- collects/typed-racket/types/subtype.rkt | 13 +++- collects/typed-racket/utils/utils.rkt | 4 +- 5 files changed, 64 insertions(+), 54 deletions(-) diff --git a/collects/typed-racket/infer/infer-unit.rkt b/collects/typed-racket/infer/infer-unit.rkt index 1e472ef2..1f29b896 100644 --- a/collects/typed-racket/infer/infer-unit.rkt +++ b/collects/typed-racket/infer/infer-unit.rkt @@ -333,6 +333,51 @@ ;; CG-Top [(_ (Univ:)) empty] + ;; check all non Type/c first so that calling subtype is safe + + ;; check each element + [((Result: s f-s o-s) + (Result: t f-t o-t)) + (cset-meet* (list (cg s t) + (cgen/filter-set V X Y f-s f-t) + (cgen/object V X Y o-s o-t)))] + + ;; values are covariant + [((Values: ss) (Values: ts)) + (unless (= (length ss) (length ts)) + (fail! ss ts)) + (cgen/list V X Y ss ts)] + + ;; this constrains `dbound' to be |ts| - |ss| + [((ValuesDots: ss s-dty dbound) (Values: ts)) + (unless (>= (length ts) (length ss)) (fail! ss ts)) + (unless (memq dbound Y) (fail! S T)) + + (let* ([vars (var-store-take dbound s-dty (- (length ts) (length ss)))] + ;; new-tys are dummy plain type variables, standing in for the elements of dbound that need to be generated + [new-tys (for/list ([var vars]) + (substitute (make-F var) dbound s-dty))] + ;; generate constraints on the prefixes, and on the dummy types + [new-cset (cgen/list V (append vars X) Y (append ss new-tys) ts)]) + ;; now take all the dummy types, and use them to constrain dbound appropriately + (move-vars-to-dmap new-cset dbound vars))] + + ;; identical bounds - just unify pairwise + [((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound)) + (when (memq dbound Y) (fail! ss ts)) + (cgen/list V X Y (cons s-dty ss) (cons t-dty ts))] + [((ValuesDots: ss s-dty (? (λ (db) (memq db Y)) s-dbound)) (ValuesDots: ts t-dty t-dbound)) + ;; What should we do if both are in Y? + (when (memq t-dbound Y) (fail! S T)) + (cset-meet + (cgen/list V X Y ss ts) + (move-dotted-rest-to-dmap (cgen V (cons s-dbound X) Y s-dty t-dty) s-dbound))] + [((ValuesDots: ss s-dty s-dbound) (ValuesDots: ts t-dty (? (λ (db) (memq db Y)) t-dbound))) + ;; s-dbound can't be in Y, due to previous rule + (cset-meet + (cgen/list V X Y ss ts) + (move-dotted-rest-to-dmap (cgen V (cons t-dbound X) Y s-dty t-dty) t-dbound))] + ;; they're subtypes. easy. [(a b) (=> nevermind) (if (subtype a b) @@ -472,41 +517,6 @@ (let ((T* (resolve-once T))) (if T* (cg S T*) (fail! S T)))] - ;; values are covariant - [((Values: ss) (Values: ts)) - (unless (= (length ss) (length ts)) - (fail! ss ts)) - (cgen/list V X Y ss ts)] - - ;; this constrains `dbound' to be |ts| - |ss| - [((ValuesDots: ss s-dty dbound) (Values: ts)) - (unless (>= (length ts) (length ss)) (fail! ss ts)) - (unless (memq dbound Y) (fail! S T)) - - (let* ([vars (var-store-take dbound s-dty (- (length ts) (length ss)))] - ;; new-tys are dummy plain type variables, standing in for the elements of dbound that need to be generated - [new-tys (for/list ([var vars]) - (substitute (make-F var) dbound s-dty))] - ;; generate constraints on the prefixes, and on the dummy types - [new-cset (cgen/list V (append vars X) Y (append ss new-tys) ts)]) - ;; now take all the dummy types, and use them to constrain dbound appropriately - (move-vars-to-dmap new-cset dbound vars))] - - ;; identical bounds - just unify pairwise - [((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound)) - (when (memq dbound Y) (fail! ss ts)) - (cgen/list V X Y (cons s-dty ss) (cons t-dty ts))] - [((ValuesDots: ss s-dty (? (λ (db) (memq db Y)) s-dbound)) (ValuesDots: ts t-dty t-dbound)) - ;; What should we do if both are in Y? - (when (memq t-dbound Y) (fail! S T)) - (cset-meet - (cgen/list V X Y ss ts) - (move-dotted-rest-to-dmap (cgen V (cons s-dbound X) Y s-dty t-dty) s-dbound))] - [((ValuesDots: ss s-dty s-dbound) (ValuesDots: ts t-dty (? (λ (db) (memq db Y)) t-dbound))) - ;; s-dbound can't be in Y, due to previous rule - (cset-meet - (cgen/list V X Y ss ts) - (move-dotted-rest-to-dmap (cgen V (cons t-dbound X) Y s-dty t-dty) t-dbound))] ;; vectors are invariant - generate constraints *both* ways [((Vector: e) (Vector: e*)) (cset-meet (cg e e*) (cg e* e))] @@ -554,12 +564,6 @@ ;; ensure that something produces a constraint set (when (null? results) (fail! S T)) (cset-combine results))))] - ;; check each element - [((Result: s f-s o-s) - (Result: t f-t o-t)) - (cset-meet* (list (cg s t) - (cgen/filter-set V X Y f-s f-t) - (cgen/object V X Y o-s o-t)))] [(_ _) ;; nothing worked, and we fail (fail! S T)])))) diff --git a/collects/typed-racket/infer/signatures.rkt b/collects/typed-racket/infer/signatures.rkt index 1b72a99f..0ce1a8ad 100644 --- a/collects/typed-racket/infer/signatures.rkt +++ b/collects/typed-racket/infer/signatures.rkt @@ -27,7 +27,7 @@ [cond-contracted c-meet ((c? c?) (symbol?) . ->* . c?)])) (define-signature restrict^ - ([cond-contracted restrict (Type/c Type/c . -> . Type/c)])) + ([cond-contracted restrict ((Type/c Type/c) ((or/c 'new 'orig)) ->* Type/c)])) (define-signature infer^ ([cond-contracted infer ((;; variables from the forall @@ -39,9 +39,9 @@ ;; domain (listof Type/c) ;; range - (or/c #f Type?)) + (or/c #f Values? ValuesDots? Result? Type/c)) ;; optional expected type - ((or/c #f Type?)) + ((or/c #f Values? ValuesDots? Result? Type/c)) . ->* . any)] [cond-contracted infer/vararg ((;; variables from the forall (listof symbol?) @@ -54,9 +54,9 @@ ;; rest (or/c #f Type/c) ;; range - (or/c #f Type?)) + (or/c #f Values? ValuesDots? Result? Type/c)) ;; [optional] expected type - ((or/c #f Type?)) . ->* . any)] + ((or/c #f Values? ValuesDots? Result? Type/c)) . ->* . any)] [cond-contracted infer/dots (((listof symbol?) symbol? (listof Type/c) (listof Type/c) Type/c Type? (listof symbol?)) diff --git a/collects/typed-racket/types/abbrev.rkt b/collects/typed-racket/types/abbrev.rkt index 1f716b3f..f305052d 100644 --- a/collects/typed-racket/types/abbrev.rkt +++ b/collects/typed-racket/types/abbrev.rkt @@ -58,9 +58,8 @@ ;; Simple union constructor. ;; Flattens nested unions and sorts types, but does not check for ;; overlapping subtypes. -(define-syntax *Un - (syntax-rules () - [(_ . args) (make-Union (remove-dups (sort (apply append (map flat (list . args))) type boolean -(define (subtype s t) +(define/cond-contract (subtype s t) + (c-> Type/c Type/c boolean?) (define k (cons (Type-seq s) (Type-seq t))) (define lookup? (hash-ref subtype-cache k 'no)) (if (eq? 'no lookup?) (let ([result (with-handlers ([exn:subtype? (lambda _ #f)]) - (subtype* (current-seen) s t))]) + (and (subtype* (current-seen) s t) #t))]) (hash-set! subtype-cache k result) result) lookup?)) @@ -193,7 +194,7 @@ [(not (apply = (length dom1) (map length dom))) #f] [(not (for/and ([rng2 (in-list rng)]) (type-equal? rng1 rng2))) #f] - [else (make-arr (apply map (lambda args (make-Union (sort args type Type/c Type/c boolean?)]) +(provide + type-compare? subtypes/varargs subtypes) ;(trace subtype*) ;(trace supertype-of-one/arr) diff --git a/collects/typed-racket/utils/utils.rkt b/collects/typed-racket/utils/utils.rkt index a8881634..0301654e 100644 --- a/collects/typed-racket/utils/utils.rkt +++ b/collects/typed-racket/utils/utils.rkt @@ -29,7 +29,9 @@ at least theoretically. (define-syntax do-contract-req (if enable-contracts? - (lambda (stx) (datum->syntax stx '(require racket/contract/base))) + (lambda (stx) (datum->syntax stx '(begin + (require racket/contract/base) + (require racket/contract/region)))) (syntax-rules () [(_) (begin)]))) (do-contract-req)