From 4c1cf6b520e27807e2c8dac603ad4a5790b27a14 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Thu, 4 Feb 2010 23:39:15 +0000 Subject: [PATCH] Add supertypes for mutable types, so that predicates work correctly. svn: r17971 original commit: 318833f4226d9249077c772f87ee705ecfd4c617 --- .../tests/typed-scheme/unit-tests/typecheck-tests.ss | 3 +++ collects/typed-scheme/private/base-env.ss | 10 ++++++---- collects/typed-scheme/rep/type-rep.ss | 8 +++++++- collects/typed-scheme/typecheck/tc-envops.ss | 2 +- collects/typed-scheme/typecheck/tc-structs.ss | 4 +++- collects/typed-scheme/types/printer.ss | 4 ++++ collects/typed-scheme/types/remove-intersect.ss | 8 ++------ collects/typed-scheme/types/subtype.ss | 6 ++++++ 8 files changed, 32 insertions(+), 13 deletions(-) diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss index 3488c93b..ba94933d 100644 --- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss +++ b/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" diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 72694527..6f8bad78 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/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)))] diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss index 5db6f744..9bcb03c9 100644 --- a/collects/typed-scheme/rep/type-rep.ss +++ 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] diff --git a/collects/typed-scheme/typecheck/tc-envops.ss b/collects/typed-scheme/typecheck/tc-envops.ss index 9acea43b..34a2280e 100644 --- a/collects/typed-scheme/typecheck/tc-envops.ss +++ b/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)) diff --git a/collects/typed-scheme/typecheck/tc-structs.ss b/collects/typed-scheme/typecheck/tc-structs.ss index 634d1dd9..337444f3 100644 --- a/collects/typed-scheme/typecheck/tc-structs.ss +++ b/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) diff --git a/collects/typed-scheme/types/printer.ss b/collects/typed-scheme/types/printer.ss index b81ca892..8d33892f 100644 --- a/collects/typed-scheme/types/printer.ss +++ b/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) diff --git a/collects/typed-scheme/types/remove-intersect.ss b/collects/typed-scheme/types/remove-intersect.ss index 1dce9f4d..ebcd2938 100644 --- a/collects/typed-scheme/types/remove-intersect.ss +++ b/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) diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss index 9c53bcb1..83a8adce 100644 --- a/collects/typed-scheme/types/subtype.ss +++ b/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)