suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

TR's numeric tower is now built from unions of non-overlapping base types.

Browse Source 
A lot of the work that was done by special-casing number types can now be
done by TR's handling of unions. This makes it easier to add more numeric
types to the tower and should make writing down types for numeric
primitives much less error-prone.

In addition, this commit adds several numeric types that will help get
tighter bounds on integer arithmetic, such as Index types. They will have
to be integrated to the base environment before they can be useful.

original commit: d4c93cc12e6df893ba2e782f0e0ea5529738315a
This commit is contained in:
Vincent St-Amour 2010-12-17 12:16:42 -05:00
parent ddd166c799
commit d5941cb2d6
17 changed files with 294 additions and 132 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/tests/typed-scheme/unit-tests/subst-tests.rkt
View File

@ -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)

2
collects/tests/typed-scheme/unit-tests/type-equal-tests.rkt
View File

@ -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)

2
collects/typed-scheme/optimizer/fixnum.rkt
View File

@ -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)

2
collects/typed-scheme/optimizer/float-complex.rkt
View File

@ -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

2
collects/typed-scheme/optimizer/float.rkt
View File

@ -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)

2
collects/typed-scheme/optimizer/unboxed-let.rkt
View File

@ -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))

2
collects/typed-scheme/private/base-env-indexing-abs.rkt
View File

@ -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)

2
collects/typed-scheme/private/base-env-indexing.rkt
View File

@ -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)))

2
collects/typed-scheme/private/base-env-numeric.rkt
View File

@ -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))

2
collects/typed-scheme/private/base-env.rkt
View File

@ -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))

58
collects/typed-scheme/private/base-types.rkt
View File

@ -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

59
collects/typed-scheme/typecheck/tc-expr-unit.rkt
View File

@ -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))]

44
collects/typed-scheme/types/abbrev.rkt
View File

@ -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

16
collects/typed-scheme/types/numeric-predicates.rkt Normal file
View File

@ -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))))

181
collects/typed-scheme/types/numeric-tower.rkt Normal file
View File

@ -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)

5
collects/typed-scheme/types/printer.rkt
View File

@ -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

43
collects/typed-scheme/types/subtype.rkt
View File

@ -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]