Add supertypes for mutable types, so that predicates work correctly.

svn: r17971

original commit: 318833f4226d9249077c772f87ee705ecfd4c617

collects/tests/typed-scheme/unit-tests/typecheck-tests.ss

@@ -791,6 +791,9 @@
               #:ret (ret -Number (-FS (list) (list (make-Bot)))))
         [tc-e (let ([x 1]) (if x x (add1 x))) 
               #:ret (ret -Pos (-FS (list) (list (make-Bot))))]
+        [tc-e (let: ([x : (U (Vectorof Number) String) (vector 1 2 3)])
+                (if (vector? x) (vector-ref x 0) (string-length x)))
+         -Number]
         )
   (test-suite
    "check-type tests"

collects/typed-scheme/private/base-env.ss

@@ -11,7 +11,8 @@
  scheme/promise scheme/system
  (only-in string-constants/private/only-once maybe-print-message)
  (only-in scheme/match/runtime match:error matchable? match-equality-test)
- (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym])))
+ (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym])
+             (only-in (rep type-rep) make-HashtableTop make-MPairTop make-BoxTop make-VectorTop)))
 
 [raise (Univ . -> . (Un))]
 
@@ -92,9 +93,9 @@
 [box (-poly (a) (a . -> . (-box a)))]
 [unbox (-poly (a) ((-box a) . -> . a))]
 [set-box! (-poly (a) ((-box a) a . -> . -Void))]
-[box? (make-pred-ty (-box Univ))]
+[box? (make-pred-ty (make-BoxTop))]
 [cons? (make-pred-ty (-pair Univ Univ))]
-[pair? (make-pred-ty (-pair Univ Univ)) #;(-poly (a b) (make-pred-ty (-pair a b)))]
+[pair? (make-pred-ty (-pair Univ Univ))]
 [empty? (make-pred-ty (-val null))]
 [empty (-val null)]
 
@@ -330,7 +331,7 @@
 [keyword->string (-Keyword . -> . -String)]
 
 ;; vectors
-[vector? (make-pred-ty (-vec Univ))]
+[vector? (make-pred-ty (make-VectorTop))]
 
 [vector->list (-poly (a) (-> (-vec a) (-lst a)))]
 [list->vector (-poly (a) (-> (-lst a) (-vec a)))]
@@ -363,6 +364,7 @@
 [directory-list (cl-> [() (-lst -Path)]
                       [(-Path) (-lst -Path)])]
 
+[hash? (make-pred-ty (make-HashtableTop))]
 [make-hash (-poly (a b) (-> (-HT a b)))]
 [make-hasheq (-poly (a b) (-> (-HT a b)))]
 [make-weak-hash (-poly (a b) (-> (-HT a b)))]

collects/typed-scheme/rep/type-rep.ss

@@ -218,8 +218,14 @@
                          poly?
                          pred-id
                          cert)]
-    [#:key #f #;(gensym)])
+    [#:key #f])
 
+;; the supertype of all of these values
+(dt BoxTop () [#:fold-rhs #:base] [#:key 'box])
+(dt VectorTop () [#:fold-rhs #:base] [#:key 'vector])
+(dt HashtableTop () [#:fold-rhs #:base] [#:key 'hash])
+(dt MPairTop () [#:fold-rhs #:base] [#:key 'mpair])
+(dt StructTop ([name Struct?]) [#:key #f])
 
 ;; v : Scheme Value
 (dt Value (v) [#:frees #f] [#:fold-rhs #:base] [#:key (cond [(number? v) 'number]

collects/typed-scheme/typecheck/tc-envops.ss

@@ -11,7 +11,7 @@
          (types resolve)
          (only-in (env type-environments lexical-env) env? update-type/lexical env-map env-props replace-props)
          scheme/contract scheme/match
-         mzlib/trace
+         mzlib/trace unstable/debug
          (typecheck tc-metafunctions)
          (for-syntax scheme/base))
 

collects/typed-scheme/typecheck/tc-structs.ss

@@ -131,7 +131,9 @@
      (list (cons (or maker* maker) 
                  (wrapper (->* external-fld-types (if cret cret name))))
            (cons (or pred* pred)
-                 (make-pred-ty (pred-wrapper name))))
+                 (make-pred-ty (if setters?
+                                   (make-StructTop sty)
+                                   (pred-wrapper name)))))
      (for/list ([g (in-list getters)] [t (in-list external-fld-types/no-parent)] [i (in-naturals)])
        (let ([func (if setters? 
                        (->* (list name) t)

collects/typed-scheme/types/printer.ss

@@ -146,6 +146,10 @@
     ;; special case number until something better happens
     [(Base: 'Number _) (fp "Number")]
     [(? has-name?) (fp "~a" (has-name? c))]
+    [(StructTop: st) (fp "~a" st)]
+    [(BoxTop:) (fp "Box")]
+    [(VectorTop:) (fp "Vector")]
+    [(MPairTop:) (fp "MPair")]
     ;; names are just the printed as the original syntax
     [(Name: stx) (fp "~a" (syntax-e stx))]
     [(App: rator rands stx) 

collects/typed-scheme/types/remove-intersect.ss

@@ -3,7 +3,7 @@
 (require "../utils/utils.ss" 
 	 (rep type-rep rep-utils)
 	 (types union subtype resolve convenience utils)
-         scheme/match mzlib/trace)
+         scheme/match mzlib/trace unstable/debug)
 
 (provide (rename-out [*remove remove]) overlap)
 
@@ -65,14 +65,11 @@
 
 ;(trace overlap)
 
-
-;(trace restrict)
-
 ;; also not yet correct
 ;; produces old without the contents of rem
 (define (*remove old rem)
   (define initial
-    (if (subtype old rem) 
+    (if (subtype old rem)
         (Un) ;; the empty type
         (match (list old rem)
           [(list (or (App: _ _ _) (Name: _)) t)
@@ -87,4 +84,3 @@
   (if (subtype old initial) old initial))
 
 ;(trace *remove)
-;(trace restrict)

collects/typed-scheme/types/subtype.ss

@@ -306,6 +306,12 @@
 	       (subtypes* A0 flds flds*)]
 	      [((Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _))
 	       (subtypes* A0 (cons proc flds) (cons proc* flds*))]
+              [((Struct: _ _ _ _ _ _ _) (StructTop: (? (lambda (s2) (type-equal? s2 s)))))
+               A0]
+              [((Box: _) (BoxTop:)) A0]
+              [((Vector: _) (VectorTop:)) A0]
+              [((MPair: _ _) (MPairTop:)) A0]
+              [((Hashtable: _ _) (HashtableTop:)) A0]
 	      ;; subtyping on structs follows the declared hierarchy
 	      [((Struct: nm (? Type? parent) flds proc _ _ _) other) 
                ;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other)