From e56663c943fe4ae355b6d626d3c84b6ec8ea7fd1 Mon Sep 17 00:00:00 2001 From: Vincent St-Amour Date: Thu, 6 Jan 2011 17:57:11 -0500 Subject: [PATCH] Add a predicate field to base types, which makes checking for subtyping of value types easier. However, this means that base types can't be marshaled as before, since these predicates can't be marshaled. Instead, we now marshal base types as identifiers that refer to their base type object. --- .../typed-scheme/unit-tests/subtype-tests.rkt | 4 +- .../unit-tests/type-equal-tests.rkt | 2 +- collects/typed-scheme/env/init-envs.rkt | 2 +- collects/typed-scheme/infer/infer-unit.rkt | 6 +- .../typed-scheme/private/type-contract.rkt | 4 +- collects/typed-scheme/rep/type-rep.rkt | 9 +- collects/typed-scheme/types/abbrev.rkt | 67 +++++++----- collects/typed-scheme/types/numeric-tower.rkt | 100 ++++++++++++++---- collects/typed-scheme/types/printer.rkt | 10 +- .../typed-scheme/types/remove-intersect.rkt | 10 +- collects/typed-scheme/types/subtype.rkt | 22 +--- 11 files changed, 150 insertions(+), 86 deletions(-) diff --git a/collects/tests/typed-scheme/unit-tests/subtype-tests.rkt b/collects/tests/typed-scheme/unit-tests/subtype-tests.rkt index b6f5cf92f8..aa1b225646 100644 --- a/collects/tests/typed-scheme/unit-tests/subtype-tests.rkt +++ b/collects/tests/typed-scheme/unit-tests/subtype-tests.rkt @@ -112,12 +112,12 @@ [(-values (list -Number)) (-values (list Univ))] - [(-poly (b) ((Un (make-Base 'foo #'dummy) + [(-poly (b) ((Un (make-Base 'foo #'dummy values #'values) (-struct 'bar #f (list (make-fld -Number #'values #f) (make-fld b #'values #f)) #'values)) . -> . (-lst b))) - ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f)) #'values)) + ((Un (make-Base 'foo #'dummy values #'values) (-struct 'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f)) #'values)) . -> . (-lst (-pair -Number (-v a))))] [(-poly (b) ((-struct 'bar #f (list (make-fld -Number #'values #f) (make-fld b #'values #f)) #'values) . -> . (-lst b))) ((-struct 'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f)) #'values) . -> . (-lst (-pair -Number (-v a))))] diff --git a/collects/tests/typed-scheme/unit-tests/type-equal-tests.rkt b/collects/tests/typed-scheme/unit-tests/type-equal-tests.rkt index 37258bff61..17e945a13b 100644 --- a/collects/tests/typed-scheme/unit-tests/type-equal-tests.rkt +++ b/collects/tests/typed-scheme/unit-tests/type-equal-tests.rkt @@ -7,7 +7,7 @@ (provide type-equal-tests) -(define (-base x) (make-Base x #'dummy)) +(define (-base x) (make-Base x #'dummy values #'values)) (define-syntax (te-tests stx) diff --git a/collects/typed-scheme/env/init-envs.rkt b/collects/typed-scheme/env/init-envs.rkt index 3a39da0b35..a8df79be38 100644 --- a/collects/typed-scheme/env/init-envs.rkt +++ b/collects/typed-scheme/env/init-envs.rkt @@ -23,7 +23,7 @@ (string->symbol (string-append "make-" (substring (symbol->string sym) 7)))) (match v [(Union: elems) `(make-Union (sort (list ,@(map sub elems)) < #:key Type-seq))] - [(Base: n cnt) `(make-Base ',n (quote-syntax ,cnt))] + [(Base: n cnt pred marshaled) marshaled] [(Name: stx) `(make-Name (quote-syntax ,stx))] [(fld: t acc mut) `(make-fld ,(sub t) (quote-syntax ,acc) ,mut)] [(Struct: name parent flds proc poly? pred-id cert maker-id) diff --git a/collects/typed-scheme/infer/infer-unit.rkt b/collects/typed-scheme/infer/infer-unit.rkt index 813fa321e4..884cd50aa9 100644 --- a/collects/typed-scheme/infer/infer-unit.rkt +++ b/collects/typed-scheme/infer/infer-unit.rkt @@ -368,11 +368,11 @@ (cg t t*)))] [((Vector: t) (Sequence: (list t*))) (cg t t*)] - [((Base: 'String _) (Sequence: (list t*))) + [((Base: 'String _ _ _) (Sequence: (list t*))) (cg -Char t*)] - [((Base: 'Bytes _) (Sequence: (list t*))) + [((Base: 'Bytes _ _ _) (Sequence: (list t*))) (cg -Nat t*)] - [((Base: 'Input-Port _) (Sequence: (list t*))) + [((Base: 'Input-Port _ _ _) (Sequence: (list t*))) (cg -Nat t*)] [((Vector: t) (Sequence: (list t*))) (cg t t*)] diff --git a/collects/typed-scheme/private/type-contract.rkt b/collects/typed-scheme/private/type-contract.rkt index ce1f26f9b5..ef43a0421e 100644 --- a/collects/typed-scheme/private/type-contract.rkt +++ b/collects/typed-scheme/private/type-contract.rkt @@ -172,7 +172,7 @@ (inexact-real? (real-part x))))))] [(== t:-Number type-equal?) #'(flat-named-contract 'Number number?)] - [(Base: sym cnt) #`(flat-named-contract '#,sym (flat-contract-predicate #,cnt))] + [(Base: sym cnt _ _) #`(flat-named-contract '#,sym (flat-contract-predicate #,cnt))] [(Refinement: par p? cert) #`(and/c #,(t->c par) (flat-contract #,(cert p?)))] [(Union: elems) @@ -257,7 +257,7 @@ (maker fld-cnts ...))))]) rec))] [else #`(flat-named-contract '#,(syntax-e pred?) #,(cert pred?))])] - [(Syntax: (Base: 'Symbol _)) #'identifier?] + [(Syntax: (Base: 'Symbol _ _ _)) #'identifier?] [(Syntax: t) #`(syntax/c #,(t->c t))] [(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))] [(Param: in out) #`(parameter/c #,(t->c out))] diff --git a/collects/typed-scheme/rep/type-rep.rkt b/collects/typed-scheme/rep/type-rep.rkt index 4cddd13442..7c542d4e5a 100644 --- a/collects/typed-scheme/rep/type-rep.rkt +++ b/collects/typed-scheme/rep/type-rep.rkt @@ -131,7 +131,14 @@ [#:key 'channel]) ;; name is a Symbol (not a Name) -(dt Base ([name symbol?] [contract syntax?]) +;; contract is used when generating contracts from types +;; predicate is used to check (at compile-time) whether a value belongs +;; to that base type. This is used to check for subtyping between value +;; types and base types. +;; marshaled has to be a syntax object that refers to the base type +;; being created. this allows us to avoid reconstructing the base type +;; when using it from its marshaled representation +(dt Base ([name symbol?] [contract syntax?] [predicate procedure?] [marshaled syntax?]) [#:frees #f] [#:fold-rhs #:base] [#:intern name] [#:key (case name [(Number Integer) 'number] diff --git a/collects/typed-scheme/types/abbrev.rkt b/collects/typed-scheme/types/abbrev.rkt index 843d72775a..d5194b7bfa 100644 --- a/collects/typed-scheme/types/abbrev.rkt +++ b/collects/typed-scheme/types/abbrev.rkt @@ -11,7 +11,9 @@ (except-in racket/contract ->* ->) (prefix-in c: racket/contract) (for-syntax racket/base syntax/parse) - (for-template racket/base racket/contract racket/promise racket/tcp racket/flonum)) + (for-template racket/base racket/contract racket/promise racket/tcp racket/flonum) + ;; for base type predicates + racket/promise racket/tcp racket/flonum) (provide (all-defined-out) (rename-out [make-Listof -lst] @@ -106,32 +108,45 @@ (define -Listof (-poly (list-elem) (make-Listof list-elem))) -(define -Boolean (make-Base 'Boolean #'boolean?)) -(define -Symbol (make-Base 'Symbol #'symbol?)) -(define -Void (make-Base 'Void #'void?)) -(define -Undefined (make-Base 'Undefined #'(lambda (x) (equal? (letrec ([y y]) y) x)))) ; initial value of letrec bindings -(define -Bytes (make-Base 'Bytes #'bytes?)) -(define -Regexp (make-Base 'Regexp #'(and/c regexp? (not/c pregexp?) (not/c byte-regexp?)))) -(define -PRegexp (make-Base 'PRegexp #'(and/c pregexp? (not/c byte-pregexp?)))) -(define -Byte-Regexp (make-Base 'Byte-Regexp #'(and/c byte-regexp? (not/c byte-pregexp?)))) -(define -Byte-PRegexp (make-Base 'Byte-PRegexp #'byte-pregexp?)) -(define -String (make-Base 'String #'string?)) -(define -Keyword (make-Base 'Keyword #'keyword?)) -(define -Char (make-Base 'Char #'char?)) -(define -Thread (make-Base 'Thread #'thread?)) -(define -Resolved-Module-Path (make-Base 'Resolved-Module-Path #'resolved-module-path?)) -(define -Module-Path (make-Base 'Module-Path #'module-path?)) -(define -Module-Path-Index (make-Base 'Module-Path-Index #'module-path-index?)) -(define -Compiled-Module-Expression (make-Base 'Compiled-Module-Expression #'compiled-module-expression?)) -(define -Prompt-Tag (make-Base 'Prompt-Tag #'continuation-prompt-tag?)) -(define -Cont-Mark-Set (make-Base 'Continuation-Mark-Set #'continuation-mark-set?)) -(define -Path (make-Base 'Path #'path?)) -(define -Namespace (make-Base 'Namespace #'namespace?)) -(define -Output-Port (make-Base 'Output-Port #'output-port?)) -(define -Input-Port (make-Base 'Input-Port #'input-port?)) -(define -TCP-Listener (make-Base 'TCP-Listener #'tcp-listener?)) +(define -Boolean (make-Base 'Boolean #'boolean? boolean? #'-Boolean)) +(define -Symbol (make-Base 'Symbol #'symbol? symbol? #'-Symbol)) +(define -Void (make-Base 'Void #'void? void? #'-Void)) +(define -Undefined + (make-Base 'Undefined + #'(lambda (x) (equal? (letrec ([y y]) y) x)) ; initial value of letrec bindings + (lambda (x) (equal? (letrec ([y y]) y) x)) + #'-Undefined)) +(define -Bytes (make-Base 'Bytes #'bytes? bytes? #'-Bytes)) +(define -Regexp (make-Base 'Regexp + #'(and/c regexp? (not/c pregexp?) (not/c byte-regexp?)) + (conjoin regexp? (negate pregexp?) (negate byte-regexp?)) + #'-Regexp)) +(define -PRegexp (make-Base 'PRegexp + #'(and/c pregexp? (not/c byte-pregexp?)) + (conjoin pregexp? (negate byte-pregexp?)) + #'-PRegexp)) +(define -Byte-Regexp (make-Base 'Byte-Regexp + #'(and/c byte-regexp? (not/c byte-pregexp?)) + (conjoin byte-regexp? (negate byte-pregexp?)) + #'-Byte-Regexp)) +(define -Byte-PRegexp (make-Base 'Byte-PRegexp #'byte-pregexp? byte-pregexp? #'-Byte-PRegexp)) +(define -String (make-Base 'String #'string? string? #'-String)) +(define -Keyword (make-Base 'Keyword #'keyword? keyword? #'-Keyword)) +(define -Char (make-Base 'Char #'char? char? #'-Char)) +(define -Thread (make-Base 'Thread #'thread? thread? #'-Thread)) +(define -Resolved-Module-Path (make-Base 'Resolved-Module-Path #'resolved-module-path? resolved-module-path? #'-Resolved-Module-Path)) +(define -Module-Path (make-Base 'Module-Path #'module-path? module-path? #'-Module-Path)) +(define -Module-Path-Index (make-Base 'Module-Path-Index #'module-path-index? module-path-index? #'-Module-Path-Index)) +(define -Compiled-Module-Expression (make-Base 'Compiled-Module-Expression #'compiled-module-expression? compiled-module-expression? #'-Compiled-Module-Expression)) +(define -Prompt-Tag (make-Base 'Prompt-Tag #'continuation-prompt-tag? continuation-prompt-tag? #'-Prompt-Tag)) +(define -Cont-Mark-Set (make-Base 'Continuation-Mark-Set #'continuation-mark-set? continuation-mark-set? #'-Cont-Mark-Set)) +(define -Path (make-Base 'Path #'path? path? #'-Path)) +(define -Namespace (make-Base 'Namespace #'namespace? namespace? #'-Namespace)) +(define -Output-Port (make-Base 'Output-Port #'output-port? output-port? #'-Output-Port)) +(define -Input-Port (make-Base 'Input-Port #'input-port? input-port? #'-Input-Port)) +(define -TCP-Listener (make-Base 'TCP-Listener #'tcp-listener? tcp-listener? #'-TCP-Listener)) -(define -FlVector (make-Base 'FlVector #'flvector?)) +(define -FlVector (make-Base 'FlVector #'flvector? flvector? #'-FlVector)) (define -Syntax make-Syntax) (define -HT make-Hashtable) diff --git a/collects/typed-scheme/types/numeric-tower.rkt b/collects/typed-scheme/types/numeric-tower.rkt index 57110cc46f..407722a0a6 100644 --- a/collects/typed-scheme/types/numeric-tower.rkt +++ b/collects/typed-scheme/types/numeric-tower.rkt @@ -4,6 +4,7 @@ (require (types abbrev numeric-predicates) (rep type-rep) + unstable/function (for-template racket/base racket/contract racket/flonum (types numeric-predicates))) (provide (all-defined-out)) @@ -36,33 +37,47 @@ ;; Integers (define -Byte>1 (make-Base 'Byte-Larger-Than-One ; unsigned - #'(and/c byte? (lambda (x) (> x 1))))) + #'(and/c byte? (lambda (x) (> x 1))) + (conjoin byte? (lambda (x) (> x 1))) + #'-Byte>1)) (define -PosByte (*Un -One -Byte>1)) (define -Byte (*Un -Zero -PosByte)) (define -PosIndexNotByte (make-Base 'Positive-Index-Not-Byte - #'(and/c index? positive? (not/c byte?)))) + ;; index? will be checked at runtime, can be platform-specific + ;; portable-index? will be checked at compile-time, must be portable + #'(and/c index? positive? (not/c byte?)) + (conjoin portable-index? positive? (negate byte?)) + #'-PosIndexNotByte)) (define -PosIndex (*Un -One -Byte>1 -PosIndexNotByte)) (define -Index (*Un -Zero -PosIndex)) (define -PosFixnumNotIndex (make-Base 'Positive-Fixnum-Not-Index - #'(and/c fixnum? positive? (not/c index?)))) + #'(and/c fixnum? positive? (not/c index?)) + (conjoin portable-fixnum? positive? (negate portable-index?)) + #'-PosFixnumNotIndex)) (define -PosFixnum (*Un -PosFixnumNotIndex -PosIndex)) (define -NonNegFixnum (*Un -PosFixnum -Zero)) (define -NegFixnum (make-Base 'Negative-Fixnum-Not-Index - #'(and/c fixnum? negative?))) + #'(and/c fixnum? negative?) + (conjoin portable-fixnum? negative?) + #'-NegFixnum)) (define -NonPosFixnum (*Un -NegFixnum -Zero)) (define -Fixnum (*Un -NegFixnum -Zero -PosFixnum)) (define -PosIntNotFixnum (make-Base 'Positive-Integer-Not-Fixnum - #'(and/c exact-integer? positive? (not/c fixnum?)))) + #'(and/c exact-integer? positive? (not/c fixnum?)) + (conjoin exact-integer? positive? (negate portable-fixnum?)) + #'-PosIntNotFixnum)) (define -PosInt (*Un -PosIntNotFixnum -PosFixnum)) (define -NonNegInt (*Un -PosInt -Zero)) (define -Nat -NonNegInt) (define -NegIntNotFixnum (make-Base 'Negative-Integer-Not-Fixnum - #'(and/c exact-integer? negative? (not/c fixnum?)))) + #'(and/c exact-integer? negative? (not/c fixnum?)) + (conjoin exact-integer? negative? (negate portable-fixnum?)) + #'-NegIntNotFixnum)) (define -NegInt (*Un -NegIntNotFixnum -NegFixnum)) (define -NonPosInt (*Un -NegInt -Zero)) (define -Int (*Un -NegInt -Zero -PosInt)) @@ -70,31 +85,45 @@ ;; Rationals (define -PosRatNotInt (make-Base 'Positive-Rational-Not-Integer - #'(and/c exact-rational? positive? (not/c integer?)))) + #'(and/c exact-rational? positive? (not/c integer?)) + (conjoin exact-rational? positive? (negate integer?)) + #'-PosRatNotInt)) (define -PosRat (*Un -PosRatNotInt -PosInt)) (define -NonNegRat (*Un -PosRat -Zero)) (define -NegRatNotInt (make-Base 'Negative-Rational-Not-Integer - #'(and/c exact-rational? negative? (not/c integer?)))) + #'(and/c exact-rational? negative? (not/c integer?)) + (conjoin exact-rational? negative? (negate integer?)) + #'-NegRatNotInt)) (define -NegRat (*Un -NegRatNotInt -NegInt)) (define -NonPosRat (*Un -NegRat -Zero)) (define -Rat (*Un -NegRat -Zero -PosRat)) ;; Floating-point numbers (define -FlonumPosZero (make-Base 'Float-Positive-Zero - #'(lambda (x) (eq? x 0.0)))) + #'(lambda (x) (eq? x 0.0)) + (lambda (x) (eq? x 0.0)) + #'-FlonumPosZero)) (define -FlonumNegZero (make-Base 'Float-Negative-Zero - #'(lambda (x) (eq? x -0.0)))) + #'(lambda (x) (eq? x -0.0)) + (lambda (x) (eq? x -0.0)) + #'-FlonumNegZero)) (define -FlonumZero (*Un -FlonumPosZero -FlonumNegZero)) (define -FlonumNan (make-Base 'Float-Nan - #'(and/c flonum? (lambda (x) (eqv? x +nan.0))))) + #'(and/c flonum? (lambda (x) (eqv? x +nan.0))) + (conjoin flonum? (lambda (x) (eqv? x +nan.0))) + #'-FlonumNan)) (define -PosFlonum (make-Base 'Positive-Float - #'(and/c flonum? positive?))) + #'(and/c flonum? positive?) + (conjoin flonum? positive?) + #'-PosFlonum)) (define -NonNegFlonum (*Un -PosFlonum -FlonumPosZero)) (define -NegFlonum (make-Base 'Negative-Float - #'(and/c flonum? negative?))) + #'(and/c flonum? negative?) + (conjoin flonum? negative?) + #'-NegFlonum)) (define -NonPosFlonum (*Un -NegFlonum -FlonumNegZero)) (define -Flonum (*Un -NegFlonum -FlonumNegZero -FlonumPosZero -PosFlonum -FlonumNan)) ; 64-bit floats ;; inexact reals can be flonums (64-bit floats) or 32-bit floats @@ -103,27 +132,37 @@ ;; eqv? equates 0.0f0 with itself, but not eq? ;; we also need to check for small-float? since eqv? also equates ;; 0.0f0 and 0.0e0 - #'(and/c small-float? (lambda (x) (eqv? x 0.0f0))))) + #'(and/c small-float? (lambda (x) (eqv? x 0.0f0))) + (lambda (x) #f) ; can't assign that type at compile-time. see tc-lit for more explanation + #'-SmallFloatPosZero)) (define -SmallFloatNegZero (make-Base 'Small-Float-Negative-Zero - #'(and/c small-float? (lambda (x) (eqv? x -0.0f0))))) + #'(and/c small-float? (lambda (x) (eqv? x -0.0f0))) + (lambda (x) #f) + #'-SmallFloatNegZero)) (define -SmallFloatZero (*Un -SmallFloatPosZero -SmallFloatNegZero)) (define -SmallFloatNan (make-Base 'Small-Float-Nan #'(and/c small-float? ;; eqv? equates single and double precision nans - (lambda (x) (eqv? x +nan.0))))) + (lambda (x) (eqv? x +nan.0))) + (lambda (x) #f) + #'-SmallFloatNan)) (define -InexactRealPosZero (*Un -SmallFloatPosZero -FlonumPosZero)) (define -InexactRealNegZero (*Un -SmallFloatNegZero -FlonumNegZero)) (define -InexactRealZero (*Un -InexactRealPosZero -InexactRealNegZero)) (define -PosSmallFloat (make-Base 'Positive-Small-Float - #'(and/c small-float? positive?))) + #'(and/c small-float? positive?) + (lambda (x) #f) + #'-PosSmallFloat)) (define -PosInexactReal (*Un -PosSmallFloat -PosFlonum)) (define -NonNegSmallFloat (*Un -PosSmallFloat -SmallFloatPosZero)) (define -NonNegInexactReal (*Un -PosInexactReal -InexactRealPosZero)) (define -NegSmallFloat (make-Base 'Negative-Small-Float - #'(and/c small-float? negative?))) + #'(and/c small-float? negative?) + (lambda (x) #f) + #'-NegSmallFloat)) (define -NegInexactReal (*Un -NegSmallFloat -NegFlonum)) (define -NonPosSmallFloat (*Un -NegSmallFloat -SmallFloatNegZero)) (define -NonPosInexactReal (*Un -NegInexactReal -InexactRealNegZero)) @@ -156,17 +195,32 @@ #'(and/c number? (lambda (x) (and (flonum? (imag-part x)) - (flonum? (real-part x))))))) + (flonum? (real-part x))))) + (conjoin number? + (lambda (x) + (and (flonum? (imag-part x)) + (flonum? (real-part x))))) + #'-FloatComplex)) (define -SmallFloatComplex (make-Base 'Small-Float-Complex #'(and/c number? (lambda (x) (and (small-float? (imag-part x)) - (small-float? (real-part x))))))) + (small-float? (real-part x))))) + (conjoin number? + (lambda (x) + (and (small-float? (imag-part x)) + (small-float? (real-part x))))) + #'-SmallFloatComplex)) (define -InexactComplex (*Un -FloatComplex -SmallFloatComplex)) (define -ExactComplexNotReal - (make-Base 'Complex-Not-Real #'(and/c number? - (not/c real?) - (lambda (x) (exact? (imag-part x)))))) + (make-Base 'Complex-Not-Real + #'(and/c number? + (not/c real?) + (lambda (x) (exact? (imag-part x)))) + (conjoin number? + (negate real?) + (lambda (x) (exact? (imag-part x)))) + #'-ExactComplexNotReal)) (define -Complex (*Un -Real -InexactComplex -ExactComplexNotReal)) (define -Number -Complex) diff --git a/collects/typed-scheme/types/printer.rkt b/collects/typed-scheme/types/printer.rkt index 5d6fce8644..076ffff824 100644 --- a/collects/typed-scheme/types/printer.rkt +++ b/collects/typed-scheme/types/printer.rkt @@ -143,7 +143,7 @@ [else (fp "~a" v)])] [(? tuple? t) (fp "~a" (cons 'List (tuple-elems t)))] - [(Base: n cnt) (fp "~s" n)] + [(Base: n cnt _ _) (fp "~s" n)] [(Opaque: pred _) (fp "(Opaque ~a)" (syntax->datum pred))] [(Struct: (== promise-sym) #f (list (fld: t _ _)) _ _ _ _ _) (fp "(Promise ~a)" t)] [(Struct: nm par (list (fld: t _ _) ...) proc _ _ _ _) @@ -196,10 +196,10 @@ #; [(Mu-unsafe: b) (fp "(unsafe-mu ~a ~a)" (Type-seq c) b)] [(Mu: x (Syntax: (Union: (list - (Base: 'Number _) - (Base: 'Boolean _) - (Base: 'Symbol _) - (Base: 'String _) + (Base: 'Number _ _ _) + (Base: 'Boolean _ _ _) + (Base: 'Symbol _ _ _) + (Base: 'String _ _ _) (Mu: var (Union: (list (Value: '()) (Pair: (F: x) (F: var))))) (Mu: y (Union: (list (F: x) (Pair: (F: x) (F: y))))) (Vector: (F: x)) diff --git a/collects/typed-scheme/types/remove-intersect.rkt b/collects/typed-scheme/types/remove-intersect.rkt index 6b3855f0ef..554a89b9f5 100644 --- a/collects/typed-scheme/types/remove-intersect.rkt +++ b/collects/typed-scheme/types/remove-intersect.rkt @@ -38,16 +38,16 @@ (ormap (lambda (t*) (overlap t t*)) e)] [(or (list _ (? Poly?)) (list (? Poly?) _)) #t] ;; these can have overlap, conservatively - [(list (Base: s1 _) (Base: s2 _)) (or (subtype t1 t2) (subtype t2 t1))] - [(list (Base: _ _) (Value: _)) (subtype t2 t1)] ;; conservative - [(list (Value: _) (Base: _ _)) (subtype t1 t2)] ;; conservative + [(list (Base: s1 _ _ _) (Base: s2 _ _ _)) (or (subtype t1 t2) (subtype t2 t1))] + [(list (Base: _ _ _ _) (Value: _)) (subtype t2 t1)] ;; conservative + [(list (Value: _) (Base: _ _ _ _)) (subtype t1 t2)] ;; conservative [(list (Syntax: t) (Syntax: t*)) (overlap t t*)] [(or (list (Syntax: _) _) (list _ (Syntax: _))) #f] - [(list (Base: _ _) _) #f] - [(list _ (Base: _ _)) #f] + [(list (Base: _ _ _ _) _) #f] + [(list _ (Base: _ _ _ _)) #f] [(list (Value: (? pair? v)) (Pair: _ _)) #t] [(list (Pair: _ _) (Value: (? pair? v))) #t] [(list (Pair: a b) (Pair: a* b*)) diff --git a/collects/typed-scheme/types/subtype.rkt b/collects/typed-scheme/types/subtype.rkt index 7e37871045..272e034921 100644 --- a/collects/typed-scheme/types/subtype.rkt +++ b/collects/typed-scheme/types/subtype.rkt @@ -233,19 +233,7 @@ ;; value types [((Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))] ;; values are subtypes of their "type" - [((Value: (? exact-integer? n)) (Base: 'Integer _)) A0] - [((Value: (and n (? number?) (? exact?) (? rational?))) (Base: 'Exact-Rational _)) A0] - [((Value: (? exact-nonnegative-integer? n)) (== -Nat =t)) A0] - [((Value: (? exact-positive-integer? n)) (Base: 'Exact-Positive-Integer _)) A0] - [((Value: (? flonum? n)) (Base: 'Flonum _)) A0] - [((Value: (? real? n)) (== -Real =t)) A0] - [((Value: (? number? n)) (Base: 'Number _)) A0] - - [((Value: (? keyword?)) (Base: 'Keyword _)) A0] - [((Value: (? char?)) (Base: 'Char _)) A0] - [((Value: (? boolean? n)) (Base: 'Boolean _)) A0] - [((Value: (? symbol? n)) (Base: 'Symbol _)) A0] - [((Value: (? string? n)) (Base: 'String _)) A0] + [((Value: v) (Base: _ _ pred _)) (if (pred v) A0 (fail! s t))] ;; tvars are equal if they are the same variable [((F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))] ;; sequences are covariant @@ -259,11 +247,11 @@ (subtypes* A0 ts (map (λ _ t*) ts))] [((Vector: t) (Sequence: (list t*))) (subtype* A0 t t*)] - [((Base: 'String _) (Sequence: (list t*))) + [((Base: 'String _ _ _) (Sequence: (list t*))) (subtype* A0 -Char t*)] - [((Base: 'Bytes _) (Sequence: (list t*))) + [((Base: 'Bytes _ _ _) (Sequence: (list t*))) (subtype* A0 -Nat t*)] - [((Base: 'Input-Port _) (Sequence: (list t*))) + [((Base: 'Input-Port _ _ _) (Sequence: (list t*))) (subtype* A0 -Nat t*)] [((Hashtable: k v) (Sequence: (list k* v*))) (subtypes* A0 (list k v) (list k* v*))] @@ -384,4 +372,4 @@ ;(subtype (make-poly '(a) (make-tvar 'a)) (make-lst N)) ;;problem: -;; (subtype (make-Mu 'x (make-Syntax (make-Union (list (make-Base 'Number #'number?) (make-F 'x))))) (make-Syntax (make-Univ))) +;; (subtype (make-Mu 'x (make-Syntax (make-Union (list (make-Base 'Number #'number? number? #'-Number) (make-F 'x))))) (make-Syntax (make-Univ)))