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
2012-06-17 22:14:19 -07:00 · 2012-06-17 22:14:19 -07:00 · d93803cdeb
commit d93803cdeb
parent 90e5702fb5
5 changed files with 64 additions and 54 deletions
--- 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)]))))
--- 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?))
--- 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<?)))]))
+(define (*Un . args)
+  (make-Union (remove-dups (sort (apply append (map flat args)) type<?))))


 (define (make-Listof elem) (-mu list-rec (*Un (-val null) (-pair elem list-rec))))
--- a/collects/typed-racket/types/subtype.rkt
+++ b/collects/typed-racket/types/subtype.rkt
@ -40,13 +40,14 @@

 ;; is s a subtype of t?
 ;; type 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<?))) (cons dom1 dom)) rng1 #f #f '())])]
+       [else (make-arr (apply map *Un (cons dom1 dom)) rng1 #f #f '())])]
    [_ #f]))

 (define-match-expander NameStruct:
@ -458,7 +459,11 @@
  (define (type-compare? a b)
  (and (subtype a b) (subtype b a)))

-(provide subtype type-compare? subtypes/varargs subtypes)
+
+(provide/cond-contract
+ [subtype (c-> Type/c Type/c boolean?)])
+(provide
+  type-compare? subtypes/varargs subtypes)

 ;(trace subtype*)
 ;(trace supertype-of-one/arr)
--- 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)