diff --git a/collects/tests/typed-scheme/unit-tests/subst-tests.rkt b/collects/tests/typed-scheme/unit-tests/subst-tests.rkt index 42332056..413e8176 100644 --- a/collects/tests/typed-scheme/unit-tests/subst-tests.rkt +++ b/collects/tests/typed-scheme/unit-tests/subst-tests.rkt @@ -2,7 +2,7 @@ (require "test-utils.ss" (for-syntax scheme/base) (rep type-rep) - (types utils abbrev substitute) + (types utils abbrev numeric-tower substitute) rackunit) (define-syntax-rule (s img var tgt result) 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 3aa1b6f6..37258bff 100644 --- a/collects/tests/typed-scheme/unit-tests/type-equal-tests.rkt +++ b/collects/tests/typed-scheme/unit-tests/type-equal-tests.rkt @@ -2,7 +2,7 @@ (require "test-utils.ss" (for-syntax scheme/base) (rep type-rep) - (types comparison abbrev union) + (types comparison abbrev numeric-tower union) rackunit) (provide type-equal-tests) diff --git a/collects/typed-scheme/optimizer/fixnum.rkt b/collects/typed-scheme/optimizer/fixnum.rkt index 0573112c..db6764fb 100644 --- a/collects/typed-scheme/optimizer/fixnum.rkt +++ b/collects/typed-scheme/optimizer/fixnum.rkt @@ -3,7 +3,7 @@ (require syntax/parse "../utils/utils.rkt" (for-template scheme/base scheme/fixnum scheme/unsafe/ops) - (types abbrev) + (types numeric-tower) (optimizer utils)) (provide fixnum-expr fixnum-opt-expr) diff --git a/collects/typed-scheme/optimizer/float-complex.rkt b/collects/typed-scheme/optimizer/float-complex.rkt index 421cc50d..e974e6d6 100644 --- a/collects/typed-scheme/optimizer/float-complex.rkt +++ b/collects/typed-scheme/optimizer/float-complex.rkt @@ -3,7 +3,7 @@ (require syntax/parse syntax/id-table scheme/dict unstable/syntax "../utils/utils.rkt" racket/unsafe/ops (for-template scheme/base scheme/math racket/flonum scheme/unsafe/ops) - (types abbrev) + (types numeric-tower) (optimizer utils float)) (provide float-complex-opt-expr diff --git a/collects/typed-scheme/optimizer/float.rkt b/collects/typed-scheme/optimizer/float.rkt index 058ec28b..a6cf1263 100644 --- a/collects/typed-scheme/optimizer/float.rkt +++ b/collects/typed-scheme/optimizer/float.rkt @@ -4,7 +4,7 @@ racket/dict racket/flonum (for-template scheme/base racket/flonum scheme/unsafe/ops) "../utils/utils.rkt" - (types abbrev) + (types numeric-tower) (optimizer utils fixnum)) (provide float-opt-expr float-coerce-expr) diff --git a/collects/typed-scheme/optimizer/unboxed-let.rkt b/collects/typed-scheme/optimizer/unboxed-let.rkt index 6d9c1f0d..57e4f111 100644 --- a/collects/typed-scheme/optimizer/unboxed-let.rkt +++ b/collects/typed-scheme/optimizer/unboxed-let.rkt @@ -5,7 +5,7 @@ "../utils/utils.rkt" "../utils/tc-utils.rkt" (for-template scheme/base) - (types abbrev utils type-table) + (types numeric-tower utils type-table) (rep type-rep) (optimizer utils float-complex)) diff --git a/collects/typed-scheme/private/base-env-indexing-abs.rkt b/collects/typed-scheme/private/base-env-indexing-abs.rkt index 48150e6d..c0f50f0f 100644 --- a/collects/typed-scheme/private/base-env-indexing-abs.rkt +++ b/collects/typed-scheme/private/base-env-indexing-abs.rkt @@ -14,7 +14,7 @@ racket/unsafe/ops) (utils tc-utils) (types union convenience) - (rename-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym])) + (rename-in (types abbrev numeric-tower) [-Number N] [-Boolean B] [-Symbol Sym])) (provide indexing) diff --git a/collects/typed-scheme/private/base-env-indexing.rkt b/collects/typed-scheme/private/base-env-indexing.rkt index 04035590..87721351 100644 --- a/collects/typed-scheme/private/base-env-indexing.rkt +++ b/collects/typed-scheme/private/base-env-indexing.rkt @@ -2,7 +2,7 @@ (require (rename-in "../utils/utils.rkt" [infer r:infer]) - (types abbrev) (env init-envs) (r:infer infer-dummy infer) + (types abbrev numeric-tower) (env init-envs) (r:infer infer-dummy infer) "base-env-indexing-abs.rkt") (define e (parameterize ([infer-param infer]) (indexing -Integer))) diff --git a/collects/typed-scheme/private/base-env-numeric.rkt b/collects/typed-scheme/private/base-env-numeric.rkt index 111e2484..a2ec325f 100644 --- a/collects/typed-scheme/private/base-env-numeric.rkt +++ b/collects/typed-scheme/private/base-env-numeric.rkt @@ -3,7 +3,7 @@ (begin (require (for-template racket/flonum racket/fixnum racket/math racket/unsafe/ops racket/base) - (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym] [-Real R] [-ExactPositiveInteger -Pos])) + (only-in (types abbrev numeric-tower) [-Number N] [-Boolean B] [-Symbol Sym] [-Real R] [-ExactPositiveInteger -Pos])) (define all-num-types (list -Pos -Nat -Integer -ExactRational -Flonum -InexactReal -Real N)) diff --git a/collects/typed-scheme/private/base-env.rkt b/collects/typed-scheme/private/base-env.rkt index 4eccedf0..0a999d24 100644 --- a/collects/typed-scheme/private/base-env.rkt +++ b/collects/typed-scheme/private/base-env.rkt @@ -22,7 +22,7 @@ (only-in mzscheme make-namespace) (only-in racket/match/runtime match:error matchable? match-equality-test)) (only-in racket/private/pre-base new-apply-proc) - (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym]) + (only-in (types abbrev numeric-tower) [-Number N] [-Boolean B] [-Symbol Sym]) (only-in (rep type-rep) make-HashtableTop make-MPairTop make-BoxTop make-ChannelTop make-VectorTop make-HeterogenousVector)) diff --git a/collects/typed-scheme/private/base-types.rkt b/collects/typed-scheme/private/base-types.rkt index 8d3e658a..bfd92656 100644 --- a/collects/typed-scheme/private/base-types.rkt +++ b/collects/typed-scheme/private/base-types.rkt @@ -1,23 +1,55 @@ #lang s-exp "type-env-lang.rkt" [Complex -Number] -[Float-Complex -FloatComplex] ; for consistency with float vs inexact-real -[Inexact-Complex -FloatComplex] ; for backward compatiblity [Number -Number] -[Integer -Integer] +[Inexact-Complex -InexactComplex] +[Small-Float-Complex -SmallFloatComplex] +[Float-Complex -FloatComplex] [Real -Real] -[Exact-Rational -ExactRational] -[Float -Flonum] ;; these 2 are the default, 64-bit floats, can be optimized -[Nonnegative-Float -NonnegativeFlonum] ;; associated test is: flonum? -[Inexact-Real -InexactReal] ;; any inexact real. could be 32- or 64-bit float - ;; associated test is: inexact-real? -[Exact-Positive-Integer -ExactPositiveInteger] -[Exact-Nonnegative-Integer -ExactNonnegativeInteger] -[Positive-Fixnum -PositiveFixnum] -[Nonnegative-Fixnum -NonnegativeFixnum] +[Nonpositive-Real -NonPosReal] +[Negative-Real -NegReal] +[Nonnegative-Real -NonNegReal] +[Positive-Real -PosReal] +[Real-Zero -RealZero] +[Inexact-Real -InexactReal] +[Small-Float -SmallFloat] +[Nonpositive-Inexact-Real -NonPosInexactReal] +[Nonpositive-Small-Float -NonPosSmallFloat] +[Negative-Inexact-Real -NegInexactReal] +[Nonnegative-Inexact-Real -NonNegInexactReal] +[Nonnegative-Small-Float -NonNegSmallFloat] +[Positive-Inexact-Real -PosInexactReal] +[Inexact-Real-Zero -InexactRealZero] +[Inexact-Real-Negative-Zero -InexactRealNegZero] +[Inexact-Real-Positive-Zero -InexactRealPosZero] +[Small-Float-Zero -SmallFloatZero] +[Float -Flonum] ; these are the default, 64-bit floats, can be optimized +[Nonpositive-Float -NonPosFlonum] +[Nonnegative-Float -NonNegFlonum] +[Float-Zero -FlonumZero] +[Exact-Rational -Rat] +[Nonpositive-Exact-Rational -NonPosRat] +[Negative-Exact-Rational -NegRat] +[Nonnegative-Exact-Rational -NonNegRat] +[Positive-Exact-Rational -PosRat] +[Integer -Integer] +[Nonpositive-Integer -NonPosInt] +[Negative-Integer -NegInt] +[Exact-Nonnegative-Integer -Nat] ; both of these are valid +[Natural -Nat] +[Exact-Positive-Integer -PosInt] ; both of these are valid +[Positive-Integer -PosInt] [Fixnum -Fixnum] -[Natural -ExactNonnegativeInteger] +[Nonpositive-Fixnum -NonPosFixnum] +[Nonnegative-Fixnum -NonNegFixnum] +[Positive-Fixnum -PosFixnum] +[Index -Index] +[Positive-Index -PosIndex] +[Byte -Byte] +[Positive-Byte -PosByte] [Zero (-val 0)] +[One (-val 1)] + [Void -Void] [Undefined -Undefined] ; initial value of letrec bindings diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.rkt b/collects/typed-scheme/typecheck/tc-expr-unit.rkt index 2a25971d..f6af9405 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.rkt +++ b/collects/typed-scheme/typecheck/tc-expr-unit.rkt @@ -21,15 +21,6 @@ (import tc-if^ tc-lambda^ tc-app^ tc-let^ check-subforms^) (export tc-expr^) -;; Is the number a fixnum on *all* the platforms Racket supports? This -;; works because Racket compiles only on 32+ bit systems. This check is -;; done at compile time to typecheck literals -- so use it instead of -;; `fixnum?' to avoid creating platform-dependent .zo files. -(define (portable-fixnum? n) - (and (exact-integer? n) - (< n (expt 2 30)) - (>= n (- (expt 2 30))))) - ;; return the type of a literal value ;; scheme-value -> type (define (tc-literal v-stx [expected #f]) @@ -42,25 +33,47 @@ [i:exp expected] [i:boolean (-val (syntax-e #'i))] [i:identifier (-val (syntax-e #'i))] + + ;; Numbers [0 -Zero] - [(~var i (3d (conjoin portable-fixnum? positive?))) -PositiveFixnum] - [(~var i (3d (conjoin portable-fixnum? negative?))) -NegativeFixnum] - [(~var i (3d (conjoin portable-fixnum?))) -Fixnum] - [(~var i (3d exact-positive-integer?)) -ExactPositiveInteger] - [(~var i (3d exact-nonnegative-integer?)) -ExactNonnegativeInteger] - [(~var i (3d exact-integer?)) -Integer] - [(~var i (3d (conjoin number? exact? rational?))) -ExactRational] - [(~var i (3d (conjoin flonum? - (lambda (x) (or (positive? x) (zero? x))) - (lambda (x) (not (eq? x -0.0)))))) - -NonnegativeFlonum] - [(~var i (3d flonum?)) -Flonum] - [(~var i (3d real?)) -Real] + [1 -One] + [(~var i (3d (conjoin byte? positive?))) -PosByte] + [(~var i (3d byte?)) -Byte] + [(~var i (3d (conjoin portable-index? positive?))) -PosIndex] + [(~var i (3d (conjoin portable-fixnum? positive?))) -PosFixnum] + [(~var i (3d (conjoin portable-fixnum? negative?))) -NegFixnum] + [(~var i (3d exact-positive-integer?)) -PosInt] + [(~var i (3d (conjoin exact-integer? negative?))) -NegInt] + [(~var i (3d (conjoin number? exact? rational? positive?))) -PosRat] + [(~var i (3d (conjoin number? exact? rational? negative?))) -NegRat] + [(~var i (3d (lambda (x) (eq? x 0.0)))) -FlonumPosZero] + [(~var i (3d (lambda (x) (eq? x -0.0)))) -FlonumNegZero] + [(~var i (3d (conjoin flonum? positive?))) -PosFlonum] + [(~var i (3d (conjoin flonum? negative?))) -NegFlonum] + [(~var i (3d flonum?)) -Flonum] ; for nan + ;; Small float literals can't be assigned a type normally. + ;; Since small floats can't live in a zo, the compilation process + ;; promotes them silently to plain floats. Thus, a small float + ;; literal can, at runtime turn into either a small float (if the + ;; program is not compiled) or a plain float (if it is). + ;; That means that if we see a small float literal, we have to + ;; give it an Inexact-Real type, which covers both cases. + [(~var i (3d (lambda (x) (eq? x 0.0f0)))) -InexactRealPosZero] + [(~var i (3d (lambda (x) (eq? x -0.0f0)))) -InexactRealNegZero] + [(~var i (3d (conjoin inexact-real? positive?))) -PosInexactReal] + [(~var i (3d (conjoin inexact-real? negative?))) -NegInexactReal] + [(~var i (3d inexact-real?)) -InexactReal] ; for nan + [(~var i (3d real?)) -Real] ; catch-all, just in case ;; a complex number can't have a float imaginary part and an exact real part [(~var i (3d (conjoin number? (lambda (x) (and (flonum? (imag-part x)) (flonum? (real-part x))))))) -FloatComplex] - [(~var i (3d number?)) -Number] + ;; same issue as small floats + [(~var i (3d (conjoin number? (lambda (x) (and (inexact-real? (imag-part x)) + (inexact-real? (real-part x))))))) + -InexactComplex] + [(~var i (3d number?)) -Number] ; otherwise, Number + [i:str -String] [i:char -Char] [i:keyword (-val (syntax-e #'i))] diff --git a/collects/typed-scheme/types/abbrev.rkt b/collects/typed-scheme/types/abbrev.rkt index fb089202..843d7277 100644 --- a/collects/typed-scheme/types/abbrev.rkt +++ b/collects/typed-scheme/types/abbrev.rkt @@ -6,7 +6,8 @@ "resolve.rkt" (utils tc-utils) racket/list - racket/match + racket/match + unstable/function (except-in racket/contract ->* ->) (prefix-in c: racket/contract) (for-syntax racket/base syntax/parse) @@ -162,47 +163,6 @@ (define -cdr (make-CdrPE)) (define -syntax-e (make-SyntaxPE)) -;; Numeric hierarchy -(define -Number (make-Base 'Number #'number?)) - -(define -FloatComplex (make-Base 'Float-Complex - #'(and/c number? - (lambda (x) - (and (flonum? (imag-part x)) - (flonum? (real-part x))))))) - -;; default 64-bit floats -(define -Flonum (make-Base 'Flonum #'flonum?)) -(define -NonnegativeFlonum (make-Base 'Nonnegative-Flonum - #'(and/c flonum? - (or/c positive? zero?) - (lambda (x) (not (eq? x -0.0)))))) -;; could be 32- or 64-bit floats -(define -InexactReal (make-Base 'Inexact-Real #'inexact-real?)) - -(define -ExactRational - (make-Base 'Exact-Rational #'(and/c number? rational? exact?))) -(define -Integer (make-Base 'Integer #'exact-integer?)) -(define -ExactPositiveInteger - (make-Base 'Exact-Positive-Integer #'exact-positive-integer?)) - -;; We're generating a reference to fixnum? rather than calling it, so -;; we're safe from fixnum size issues on different platforms. -(define -PositiveFixnum - (make-Base 'Positive-Fixnum #'(and/c fixnum? positive?))) -(define -NegativeFixnum - (make-Base 'Negative-Fixnum #'(and/c fixnum? negative?))) - -(define -Zero (-val 0)) -(define -Real (*Un -InexactReal -ExactRational)) -(define -Fixnum (*Un -PositiveFixnum -NegativeFixnum -Zero)) -(define -NonnegativeFixnum (*Un -PositiveFixnum -Zero)) -(define -ExactNonnegativeInteger (*Un -ExactPositiveInteger -Zero)) -(define -Nat -ExactNonnegativeInteger) - -(define -Byte -NonnegativeFixnum) - - ;; convenient syntax diff --git a/collects/typed-scheme/types/numeric-predicates.rkt b/collects/typed-scheme/types/numeric-predicates.rkt new file mode 100644 index 00000000..bd18c522 --- /dev/null +++ b/collects/typed-scheme/types/numeric-predicates.rkt @@ -0,0 +1,16 @@ +#lang racket/base + +(require unstable/function) + +(provide index? exact-rational? small-float?) + +;; this is required for template in numeric-tower.rkt + +;; we assume indexes are 2 bits shorter than fixnums +;; We're generating a reference to fixnum? rather than calling it, so +;; we're safe from fixnum size issues on different platforms. +(define (index? x) (and (fixnum? x) (fixnum? (* x 4)))) + +(define exact-rational? (conjoin rational? exact?)) + +(define (small-float? x) (and (inexact-real? x) (not (flonum? x)))) diff --git a/collects/typed-scheme/types/numeric-tower.rkt b/collects/typed-scheme/types/numeric-tower.rkt new file mode 100644 index 00000000..57110cc4 --- /dev/null +++ b/collects/typed-scheme/types/numeric-tower.rkt @@ -0,0 +1,181 @@ +#lang racket/base + +(require "../utils/utils.rkt") + +(require (types abbrev numeric-predicates) + (rep type-rep) + (for-template racket/base racket/contract racket/flonum (types numeric-predicates))) + +(provide (all-defined-out)) + +;; Numeric hierarchy +;; All built as unions of non-overlapping base types. +;; This should make encoding mathematical properties in the base env easier. +;; Most of the weird base types will probably never be exposed to the user +;; and some probably won't show up in the base env either. +;; A lot of these contracts will be overriden in type->contract, so their +;; hairiness should not be of much consequence. + +;; Is the number a fixnum on *all* the platforms Racket supports? This +;; works because Racket compiles only on 32+ bit systems. This check is +;; done at compile time to typecheck literals -- so use it instead of +;; `fixnum?' to avoid creating platform-dependent .zo files. +(define (portable-fixnum? n) + (and (exact-integer? n) + (< n (expt 2 30)) + (>= n (- (expt 2 30))))) +;; same, for indexes +(define (portable-index? n) + (and (exact-integer? n) + (< n (expt 2 28)) + (>= n (- (expt 2 28))))) + +;; Singletons +(define -Zero (-val 0)) ; exact +(define -One (-val 1)) + +;; Integers +(define -Byte>1 (make-Base 'Byte-Larger-Than-One ; unsigned + #'(and/c byte? (lambda (x) (> x 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?)))) +(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?)))) +(define -PosFixnum (*Un -PosFixnumNotIndex -PosIndex)) +(define -NonNegFixnum (*Un -PosFixnum -Zero)) +(define -NegFixnum + (make-Base 'Negative-Fixnum-Not-Index + #'(and/c fixnum? negative?))) +(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?)))) +(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?)))) +(define -NegInt (*Un -NegIntNotFixnum -NegFixnum)) +(define -NonPosInt (*Un -NegInt -Zero)) +(define -Int (*Un -NegInt -Zero -PosInt)) + +;; Rationals +(define -PosRatNotInt + (make-Base 'Positive-Rational-Not-Integer + #'(and/c exact-rational? positive? (not/c integer?)))) +(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?)))) +(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)))) +(define -FlonumNegZero (make-Base 'Float-Negative-Zero + #'(lambda (x) (eq? x -0.0)))) +(define -FlonumZero (*Un -FlonumPosZero -FlonumNegZero)) +(define -FlonumNan (make-Base 'Float-Nan + #'(and/c flonum? (lambda (x) (eqv? x +nan.0))))) +(define -PosFlonum + (make-Base 'Positive-Float + #'(and/c flonum? positive?))) +(define -NonNegFlonum (*Un -PosFlonum -FlonumPosZero)) +(define -NegFlonum + (make-Base 'Negative-Float + #'(and/c flonum? negative?))) +(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 +(define -SmallFloatPosZero ; disjoint from Flonum 0s + (make-Base 'Small-Float-Positive-Zero + ;; 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))))) +(define -SmallFloatNegZero + (make-Base 'Small-Float-Negative-Zero + #'(and/c small-float? (lambda (x) (eqv? x -0.0f0))))) +(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))))) +(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?))) +(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?))) +(define -NegInexactReal (*Un -NegSmallFloat -NegFlonum)) +(define -NonPosSmallFloat (*Un -NegSmallFloat -SmallFloatNegZero)) +(define -NonPosInexactReal (*Un -NegInexactReal -InexactRealNegZero)) +(define -SmallFloat (*Un -NegSmallFloat -SmallFloatNegZero -SmallFloatPosZero -PosSmallFloat -SmallFloatNan)) +(define -InexactReal (*Un -SmallFloat -Flonum)) + +;; Reals +(define -RealZero (*Un -Zero -InexactRealZero)) +(define -PosReal (*Un -PosRat -PosInexactReal)) +(define -NonNegReal (*Un -NonNegRat -NonNegInexactReal)) +(define -NegReal (*Un -NegRat -NegInexactReal)) +(define -NonPosReal (*Un -NonPosRat -NonPosInexactReal)) +(define -Real (*Un -Rat -InexactReal)) + +;; Complexes +;; We could go into _much_ more precision here. +;; We could have types that reflect the size/exactness of both components +;; (e.g. PosFixnumNonNegIntComplex), to give more interesting types to +;; real-part, imag-part and others. +;; We could have Complex be a 2-argument type constructor (although it +;; could construct uninhabitable types like (Complex Integer Float), which +;; can't exist in Racket (parts must be both exact or both inexact)). +;; Imaginaries could have their own type hierarchy as well. +;; That's future work. + +;; Both parts of a complex number must be of the same exactness. +;; Thus, the only possible kinds of complex numbers are: +;; Real/Real, Flonum/Flonum, SmallFloat/SmallFloat +(define -FloatComplex (make-Base 'Float-Complex + #'(and/c number? + (lambda (x) + (and (flonum? (imag-part x)) + (flonum? (real-part x))))))) +(define -SmallFloatComplex (make-Base 'Small-Float-Complex + #'(and/c number? + (lambda (x) + (and (small-float? (imag-part x)) + (small-float? (real-part x))))))) +(define -InexactComplex (*Un -FloatComplex -SmallFloatComplex)) +(define -ExactComplexNotReal + (make-Base 'Complex-Not-Real #'(and/c number? + (not/c real?) + (lambda (x) (exact? (imag-part x)))))) +(define -Complex (*Un -Real -InexactComplex -ExactComplexNotReal)) +(define -Number -Complex) + +;; TODO for compatibility +(define -NonnegativeFlonum -NonNegFlonum) +(define -ExactRational -Rat) +(define -Integer -Int) +(define -ExactPositiveInteger -PosInt) +(define -PositiveFixnum -PosFixnum) +(define -NegativeFixnum -NegFixnum) +(define -NonnegativeFixnum -NonNegFixnum) +(define -ExactNonnegativeInteger -Nat) diff --git a/collects/typed-scheme/types/printer.rkt b/collects/typed-scheme/types/printer.rkt index d92c6cc1..5d6fce86 100644 --- a/collects/typed-scheme/types/printer.rkt +++ b/collects/typed-scheme/types/printer.rkt @@ -1,8 +1,9 @@ #lang scheme/base (require unstable/sequence racket/require racket/match - (path-up "rep/type-rep.rkt" "rep/filter-rep.rkt" "rep/object-rep.rkt" "types/abbrev.rkt" - "rep/rep-utils.rkt" "utils/utils.rkt" "utils/tc-utils.rkt")) + (path-up "rep/type-rep.rkt" "rep/filter-rep.rkt" "rep/object-rep.rkt" "rep/rep-utils.rkt" + "types/abbrev.rkt" "types/numeric-tower.rkt" "types/subtype.rkt" + "utils/utils.rkt" "utils/tc-utils.rkt")) ;; do we attempt to find instantiations of polymorphic types to print? ;; FIXME - currently broken diff --git a/collects/typed-scheme/types/subtype.rkt b/collects/typed-scheme/types/subtype.rkt index a13328e3..7e378710 100644 --- a/collects/typed-scheme/types/subtype.rkt +++ b/collects/typed-scheme/types/subtype.rkt @@ -2,7 +2,7 @@ (require "../utils/utils.rkt" (rep type-rep filter-rep object-rep rep-utils) (utils tc-utils) - (types utils comparison resolve abbrev substitute) + (types utils comparison resolve abbrev numeric-tower substitute) (env type-name-env) (only-in (infer infer-dummy) unify) racket/match unstable/match @@ -232,47 +232,6 @@ [((Union: (list)) _) A0] ;; value types [((Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))] - ;; now we encode the numeric hierarchy - bletch - [((Base: 'Integer _) (== -Real =t)) A0] - [((Base: 'Integer _) (Base: 'Number _)) A0] - [((Base: 'Flonum _) (Base: 'Inexact-Real _)) A0] - [((Base: 'Flonum _) (== -Real =t)) A0] - [((Base: 'Flonum _) (Base: 'Number _)) A0] - [((Base: 'Exact-Rational _) (Base: 'Number _)) A0] - [((Base: 'Integer _) (Base: 'Exact-Rational _)) A0] - [((Base: 'Exact-Positive-Integer _) (Base: 'Exact-Rational _)) A0] - [((Base: 'Exact-Positive-Integer _) (Base: 'Number _)) A0] - [((Base: 'Exact-Positive-Integer _) (== -Nat =t)) A0] - [((Base: 'Exact-Positive-Integer _) (Base: 'Integer _)) A0] - - [((Base: 'Positive-Fixnum _) (Base: 'Exact-Positive-Integer _)) A0] - [((Base: 'Positive-Fixnum _) (Base: 'Exact-Rational _)) A0] - [((Base: 'Positive-Fixnum _) (Base: 'Number _)) A0] - [((Base: 'Positive-Fixnum _) (== -Nat =t)) A0] - [((Base: 'Positive-Fixnum _) (Base: 'Integer _)) A0] - - [((Base: 'Negative-Fixnum _) (Base: 'Exact-Rational _)) A0] - [((Base: 'Negative-Fixnum _) (Base: 'Number _)) A0] - [((Base: 'Negative-Fixnum _) (Base: 'Integer _)) A0] - - [((== -Nat =t) (Base: 'Number _)) A0] - [((== -Nat =t) (Base: 'Exact-Rational _)) A0] - [((== -Nat =t) (Base: 'Integer _)) A0] - - [((== -Fixnum =t) (Base: 'Number _)) A0] - [((== -Fixnum =t) (Base: 'Exact-Rational _)) A0] - [((== -Fixnum =t) (Base: 'Integer _)) A0] - - [((Base: 'Nonnegative-Flonum _) (Base: 'Flonum _)) A0] - [((Base: 'Nonnegative-Flonum _) (Base: 'Inexact-Real _)) A0] - [((Base: 'Nonnegative-Flonum _) (Base: 'Number _)) A0] - - [((Base: 'Inexact-Real _) (== -Real =t)) A0] - [((Base: 'Inexact-Real _) (Base: 'Number _)) A0] - - [((Base: 'Float-Complex _) (Base: 'Number _)) A0] - - ;; values are subtypes of their "type" [((Value: (? exact-integer? n)) (Base: 'Integer _)) A0] [((Value: (and n (? number?) (? exact?) (? rational?))) (Base: 'Exact-Rational _)) A0]