diff --git a/collects/tests/typed-scheme/unit-tests/subtype-tests.rkt b/collects/tests/typed-scheme/unit-tests/subtype-tests.rkt index b6f5cf92..aa1b2256 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 37258bff..17e945a1 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 3a39da0b..a8df79be 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 813fa321..884cd50a 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 ce1f26f9..ef43a042 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 4cddd134..7c542d4e 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 843d7277..d5194b7b 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 57110cc4..407722a0 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 5d6fce86..076ffff8 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 6b3855f0..554a89b9 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 7e378710..272e0349 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)))