diff --git a/collects/tests/typed-scheme/fail/nonnegative-float.rkt b/collects/tests/typed-scheme/fail/nonnegative-float.rkt new file mode 100644 index 0000000000..ac7974818a --- /dev/null +++ b/collects/tests/typed-scheme/fail/nonnegative-float.rkt @@ -0,0 +1,5 @@ +#; +(exn-pred 1) +#lang typed/scheme + +(ann (- 1.0 0.5) Nonnegative-Float) ; can't prove it's nonnegative diff --git a/collects/tests/typed-scheme/succeed/nonnegative-float.rkt b/collects/tests/typed-scheme/succeed/nonnegative-float.rkt new file mode 100644 index 0000000000..de361d7650 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/nonnegative-float.rkt @@ -0,0 +1,6 @@ +#lang typed/scheme + +(ann (+ 1.0 2.1) Nonnegative-Float) +(ann (+ 1 2.1) Nonnegative-Float) +(ann (* 1.2 3.1) Nonnegative-Float) +(ann (sqrt 3.5) Nonnegative-Float) diff --git a/collects/tests/typed-scheme/succeed/pair-test3.rkt b/collects/tests/typed-scheme/succeed/pair-test3.rkt index 460b6cf9bd..e45bd796fa 100644 --- a/collects/tests/typed-scheme/succeed/pair-test3.rkt +++ b/collects/tests/typed-scheme/succeed/pair-test3.rkt @@ -11,7 +11,7 @@ '((((1 . "1") . (#t)) . ((#f . #\f) . ("2"))) . ((("3" . 4) . (1.0)) - . ((#(2.0 3.0 4.0) . #t) + . ((#(2.0 3.0 -4.0) . #t) . ((2.0 3.0 4.0) . #f))))) diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt b/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt index 46c300abd9..36f097a664 100644 --- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt +++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt @@ -38,7 +38,6 @@ (define Sym -Symbol) (define -Pos -ExactPositiveInteger) (define R -Real) -(define F -Flonum) (define (g) (run typecheck-tests)) @@ -798,7 +797,8 @@ Univ] [tc-e (floor 1/2) -Integer] [tc-e (ceiling 1/2) -Integer] - [tc-e (truncate 0.5) -Flonum] + [tc-e (truncate 0.5) -NonnegativeFlonum] + [tc-e (truncate -0.5) -Flonum] [tc-e/t (ann (lambda (x) (lambda (x) x)) (Integer -> (All (X) (X -> X)))) (t:-> -Integer (-poly (x) (t:-> x x)))] @@ -838,10 +838,14 @@ (tc-l 5 -PositiveFixnum) (tc-l -5 -NegativeFixnum) (tc-l 0 -Zero) - (tc-l 0.0 -Flonum) - (tc-l 5# -Flonum) - (tc-l 5.0 -Flonum) - (tc-l 5.1 -Flonum) + (tc-l 0.0 -NonnegativeFlonum) + (tc-l -0.0 -Flonum) + (tc-l 5# -NonnegativeFlonum) + (tc-l 5.0 -NonnegativeFlonum) + (tc-l 5.1 -NonnegativeFlonum) + (tc-l -5# -Flonum) + (tc-l -5.0 -Flonum) + (tc-l -5.1 -Flonum) (tc-l 1+1i N) (tc-l 1+1.0i -InexactComplex) (tc-l 1.0+1i -InexactComplex) diff --git a/collects/typed-scheme/private/base-env-numeric.rkt b/collects/typed-scheme/private/base-env-numeric.rkt index b4365578f2..11e8414c2f 100644 --- a/collects/typed-scheme/private/base-env-numeric.rkt +++ b/collects/typed-scheme/private/base-env-numeric.rkt @@ -26,6 +26,7 @@ (-> -Pos -Pos) (-> -Nat -Nat) (-> -ExactRational -Integer) + (-> -NonnegativeFlonum -NonnegativeFlonum) (-> -Flonum -Flonum) (-> -Real -Real))) @@ -34,7 +35,9 @@ (define-for-syntax fl-comp (binop -Flonum B)) (define-for-syntax fl-op (binop -Flonum)) (define-for-syntax fl-unop (unop -Flonum)) - + (define-for-syntax fl-rounder + (cl->* (-> -NonnegativeFlonum -NonnegativeFlonum) + (-> -Flonum -Flonum))) (define-for-syntax int-op (binop -Integer)) (define-for-syntax nat-op (binop -Nat)) @@ -91,10 +94,49 @@ (-> -Integer -Pos B : (-FS (-filter -Pos 0) -top)) (-> -Integer -Nat B : (-FS (-filter -Nat 0) -top)) fx-comp)) + (define-for-syntax fxmin-type + (cl->* + (-> -NegativeFixnum -Integer -NegativeFixnum) + (-> -Integer -NegativeFixnum -NegativeFixnum) + (-> -Pos -Pos -PositiveFixnum) + (-> -Nat -Nat -NonnegativeFixnum) + (-> -Integer -Integer -Fixnum))) + (define-for-syntax fxmax-type + (cl->* + (-> -NegativeFixnum -NegativeFixnum -NegativeFixnum) + (-> -Pos -Integer -PositiveFixnum) + (-> -Integer -Pos -PositiveFixnum) + (-> -Nat -Integer -NonnegativeFixnum) + (-> -Integer -Nat -NonnegativeFixnum) + (-> -Integer -Integer -Fixnum))) + + (define-for-syntax fl+*-type + (cl->* (-NonnegativeFlonum -NonnegativeFlonum . -> . -NonnegativeFlonum) + (-Flonum -Flonum . -> . -Flonum))) + (define-for-syntax fl=-type + (cl->* + (-> -Flonum -NonnegativeFlonum B : (-FS (-filter -NonnegativeFlonum 0) -top)) + (-> -NonnegativeFlonum -Flonum B : (-FS (-filter -NonnegativeFlonum 1) -top)) + fl-comp)) + (define-for-syntax fl<-type + (cl->* + (-> -NonnegativeFlonum -Flonum B : (-FS (-filter -NonnegativeFlonum 1) -top)) + fl-comp)) + (define-for-syntax fl>-type + (cl->* + (-> -Flonum -NonnegativeFlonum B : (-FS (-filter -NonnegativeFlonum 0) -top)) + fl-comp)) + (define-for-syntax flmin-type + (cl->* (-> -NonnegativeFlonum -NonnegativeFlonum -NonnegativeFlonum) + (-> -Flonum -Flonum -Flonum))) + (define-for-syntax flmax-type + (cl->* (-> -NonnegativeFlonum -Flonum -NonnegativeFlonum) + (-> -Flonum -NonnegativeFlonum -NonnegativeFlonum) + (-> -Flonum -Flonum -Flonum))) ) ;; numeric predicates -[zero? (asym-pred N B (-FS (-filter (Un -Flonum -Zero) 0) +[zero? (asym-pred N B (-FS (-filter (Un -NonnegativeFlonum -Zero) 0) (-not-filter -Zero 0)))] [number? (make-pred-ty N)] [integer? (asym-pred Univ B (-FS (-filter (Un -Integer -Flonum) 0) @@ -109,9 +151,11 @@ [fixnum? (make-pred-ty -Fixnum)] [positive? (cl->* (-> -Fixnum B : (-FS (-filter -PositiveFixnum 0) -top)) (-> -Integer B : (-FS (-filter -ExactPositiveInteger 0) -top)) + (-> -Flonum B : (-FS (-filter -NonnegativeFlonum 0) -top)) (-> -Real B))] [negative? (cl->* (-> -Fixnum B : (-FS (-filter -NegativeFixnum 0) (-filter -NonnegativeFixnum 0))) (-> -Integer B : (-FS -top (-filter -Nat 0))) + (-> -Flonum B : (-FS -top (-filter -NonnegativeFlonum 0))) (-> -Real B))] [exact-positive-integer? (make-pred-ty -Pos)] [exact-nonnegative-integer? (make-pred-ty -Nat)] @@ -146,6 +190,8 @@ (-> -Fixnum -NonnegativeFixnum B : (-FS (-filter -PositiveFixnum 1) -top)) (-> -Fixnum -Nat B : (-FS (-filter -Fixnum 1) -top)) (-> -Integer -Nat B : (-FS (-filter -ExactPositiveInteger 0) -top)) + (-> -Flonum -NonnegativeFlonum B : (-FS (-filter -NonnegativeFlonum 0) -top)) + (-> -NonnegativeFlonum -Flonum B : (-FS -top (-filter -NonnegativeFlonum 1))) real-comp)] [>= (cl->* (-> -Fixnum (-val 0) B : (-FS (-filter -NonnegativeFixnum 0) (-filter -NegativeFixnum 0))) @@ -156,6 +202,8 @@ (-> -Fixnum -Nat B : (-FS (-filter -NonnegativeFixnum 1) -top)) (-> -Integer -Pos B : (-FS (-filter -Pos 0) -top)) (-> -Integer -Nat B : (-FS (-filter -Nat 0) -top)) + (-> -Flonum -NonnegativeFlonum B : (-FS (-filter -NonnegativeFlonum 0) -top)) + (-> -NonnegativeFlonum -Flonum B : (-FS -top (-filter -NonnegativeFlonum 1))) real-comp)] [< (cl->* (-> -Fixnum (-val 0) B : (-FS (-filter -NegativeFixnum 0) (-filter -NonnegativeFixnum 0))) @@ -165,6 +213,8 @@ (-> -Nat -Fixnum B : (-FS (-filter -NonnegativeFixnum 0) -top)) (-> -Nat -Integer B : (-FS (-filter -Pos 1) -top)) (-> -Integer -Nat B : (-FS -top (-filter -Nat 0))) + (-> -NonnegativeFlonum -Flonum B : (-FS (-filter -NonnegativeFlonum 1) -top)) + (-> -Flonum -NonnegativeFlonum B : (-FS -top (-filter -NonnegativeFlonum 0))) real-comp)] [<= (cl->* (-> -Fixnum (-val 0) B : (-FS -top (-filter -PositiveFixnum 0))) @@ -175,18 +225,26 @@ (-> -Nat -Fixnum B : (-FS (-filter -NonnegativeFixnum 0) -top)) (-> -Pos -Integer B : (-FS (-filter -Pos 1) -top)) (-> -Nat -Integer B : (-FS (-filter -Nat 1) -top)) + (-> -NonnegativeFlonum -Flonum B : (-FS (-filter -NonnegativeFlonum 1) -top)) + (-> -Flonum -NonnegativeFlonum B : (-FS -top (-filter -NonnegativeFlonum 0))) real-comp)] [* (apply cl->* - (append (for/list ([t (list -Pos -Nat -Integer -ExactRational -Flonum)]) (->* (list) t t)) + (append (for/list ([t (list -Pos -Nat -Integer -ExactRational -NonnegativeFlonum -Flonum)]) (->* (list) t t)) + (list (->* (list -Pos) -NonnegativeFlonum -NonnegativeFlonum)) + (list (->* (list -NonnegativeFlonum) -Pos -NonnegativeFlonum)) + (list (->* (list -Pos) -Flonum -Flonum)) + (list (->* (list -Flonum) -Pos -Flonum)) (list (->* (list) -Real -Real)) (list (->* (list) -InexactComplex -InexactComplex)) (list (->* (list) N N))))] [+ (apply cl->* (append (list (->* (list -Pos) -Nat -Pos)) (list (->* (list -Nat) -Pos -Pos)) - (for/list ([t (list -Nat -Integer -ExactRational -Flonum)]) (->* (list) t t)) + (for/list ([t (list -Nat -Integer -ExactRational -NonnegativeFlonum -Flonum)]) (->* (list) t t)) + (list (->* (list -Nat) -NonnegativeFlonum -NonnegativeFlonum)) + (list (->* (list -NonnegativeFlonum) -Nat -NonnegativeFlonum)) ;; special cases for promotion to inexact, not exhaustive ;; valid for + and -, but not for * and /, since (* 0) is exact 0 (i.e. not a float) (list (->* (list -Flonum) -Real -Flonum)) @@ -225,6 +283,7 @@ (->* (list -Nat) -Integer -Nat) (->* (list -Integer) -Integer -Integer) (->* (list -ExactRational) -ExactRational -ExactRational) + (->* (list -NonnegativeFlonum) -Flonum -NonnegativeFlonum) (->* (list -Flonum) -Flonum -Flonum) (->* (list -Real) -Real -Real))] [min (cl->* (->* (list -PositiveFixnum) -PositiveFixnum -PositiveFixnum) @@ -236,6 +295,7 @@ (->* (list -Nat) -Nat -Nat) (->* (list -Integer) -Integer -Integer) (->* (list -ExactRational) -ExactRational -ExactRational) + (->* (list -NonnegativeFlonum) -NonnegativeFlonum -NonnegativeFlonum) (->* (list -Flonum) -Flonum -Flonum) (->* (list -Real) -Real -Real))] @@ -244,6 +304,7 @@ (-> -Nat -Pos) (-> -Integer -Integer) (-> -ExactRational -ExactRational) + (-> -NonnegativeFlonum -NonnegativeFlonum) (-> -Flonum -Flonum) (-> -Real -Real) (-> -InexactComplex -InexactComplex) @@ -291,8 +352,11 @@ [bitwise-bit-field (-> -Integer -Integer -Integer -Integer)] [integer-length (-> -Integer -NonnegativeFixnum)] -[abs (cl->* (-Fixnum . -> . -NonnegativeFixnum) +[abs (cl->* (-PositiveFixnum . -> . -PositiveFixnum) + (-Fixnum . -> . -NonnegativeFixnum) + (-Pos . -> . -Pos) (-Integer . -> . -Nat) + (-Flonum . -> . -NonnegativeFlonum) (-Real . -> . -Real))] ;; exactness @@ -333,13 +397,15 @@ (N N . -> . N))] [sqrt (cl->* (-Nat . -> . -Real) + (-NonnegativeFlonum . -> . -NonnegativeFlonum) (-InexactComplex . -> . -InexactComplex) (N . -> . N))] [log (cl->* (-Pos . -> . -Real) (-InexactComplex . -> . -InexactComplex) (N . -> . N))] -[exp (cl->* (-Real . -> . -Real) +[exp (cl->* (-Flonum . -> . -Flonum) + (-Real . -> . -Real) (-InexactComplex . -> . -InexactComplex) (N . -> . N))] [cos (cl->* (-Flonum . -> . -Flonum) (-Real . -> . -Real) (-InexactComplex . -> . -InexactComplex) (N . -> . N))] @@ -354,11 +420,12 @@ ;; scheme/math [sgn (-Real . -> . -Real)] -[pi -Flonum] +[pi -NonnegativeFlonum] [sqr (cl->* (-> -Pos -Pos) - (-> -Nat -Nat) + (-> -Nat -Nat) (-> -Integer -Integer) (-> -ExactRational -ExactRational) + (-> -NonnegativeFlonum -NonnegativeFlonum) (-> -Flonum -Flonum) (-> -Real -Real) (-> -InexactComplex -InexactComplex) @@ -373,22 +440,22 @@ (N . -> . N))] ;; unsafe numeric ops -[unsafe-flabs fl-unop] -[unsafe-fl+ fl-op] +[unsafe-flabs (-> -Flonum -NonnegativeFlonum)] +[unsafe-fl+ fl+*-type] [unsafe-fl- fl-op] -[unsafe-fl* fl-op] +[unsafe-fl* fl+*-type] [unsafe-fl/ fl-op] -[unsafe-fl= fl-comp] -[unsafe-fl<= fl-comp] -[unsafe-fl>= fl-comp] -[unsafe-fl> fl-comp] -[unsafe-fl< fl-comp] -[unsafe-flmin fl-op] -[unsafe-flmax fl-op] -[unsafe-flround fl-unop] -[unsafe-flfloor fl-unop] -[unsafe-flceiling fl-unop] -[unsafe-fltruncate fl-unop] +[unsafe-fl= fl=-type] +[unsafe-fl<= fl<-type] +[unsafe-fl>= fl>-type] +[unsafe-fl> fl>-type] +[unsafe-fl< fl<-type] +[unsafe-flmin flmin-type] +[unsafe-flmax flmax-type] +[unsafe-flround fl-rounder] +[unsafe-flfloor fl-rounder] +[unsafe-flceiling fl-rounder] +[unsafe-fltruncate fl-rounder] [unsafe-flsin fl-unop] [unsafe-flcos fl-unop] [unsafe-fltan fl-unop] @@ -396,9 +463,9 @@ [unsafe-flasin fl-unop] [unsafe-flacos fl-unop] [unsafe-fllog fl-unop] -[unsafe-flexp fl-unop] -[unsafe-flsqrt fl-unop] -[unsafe-fx->fl (-Integer . -> . -Flonum)] +[unsafe-flexp fl-rounder] +[unsafe-flsqrt fl-rounder] +[unsafe-fx->fl (cl->* (-Nat . -> . -NonnegativeFlonum) (-Integer . -> . -Flonum))] [unsafe-fx+ fx+-type] [unsafe-fx- fx-intop] @@ -450,22 +517,22 @@ ;; safe flonum ops -[flabs fl-unop] -[fl+ fl-op] +[flabs (-> -Flonum -NonnegativeFlonum)] +[fl+ fl+*-type] [fl- fl-op] -[fl* fl-op] +[fl* fl+*-type] [fl/ fl-op] -[fl= fl-comp] -[fl<= fl-comp] -[fl>= fl-comp] -[fl> fl-comp] -[fl< fl-comp] -[flmin fl-op] -[flmax fl-op] -[flround fl-unop] -[flfloor fl-unop] -[flceiling fl-unop] -[fltruncate fl-unop] +[fl= fl=-type] +[fl<= fl<-type] +[fl>= fl>-type] +[fl> fl>-type] +[fl< fl<-type] +[flmin flmin-type] +[flmax flmax-type] +[flround fl-rounder] +[flfloor fl-rounder] +[flceiling fl-rounder] +[fltruncate fl-rounder] [flsin fl-unop] [flcos fl-unop] [fltan fl-unop] diff --git a/collects/typed-scheme/private/base-types.rkt b/collects/typed-scheme/private/base-types.rkt index 9f8f775c23..5b51c82907 100644 --- a/collects/typed-scheme/private/base-types.rkt +++ b/collects/typed-scheme/private/base-types.rkt @@ -7,6 +7,7 @@ [Real -Real] [Exact-Rational -ExactRational] [Float -Flonum] +[Nonnegative-Float -NonnegativeFlonum] [Exact-Positive-Integer -ExactPositiveInteger] [Exact-Nonnegative-Integer -ExactNonnegativeInteger] [Positive-Fixnum -PositiveFixnum] diff --git a/collects/typed-scheme/private/optimize.rkt b/collects/typed-scheme/private/optimize.rkt index 72c519a175..a3922b871f 100644 --- a/collects/typed-scheme/private/optimize.rkt +++ b/collects/typed-scheme/private/optimize.rkt @@ -6,22 +6,26 @@ (types abbrev type-table utils subtype)) (provide optimize) +;; for use in match +(define (subtypeof x y) + (subtype y x)) + (define-syntax-class float-opt-expr (pattern e:opt-expr #:when (match (type-of #'e) - [(tc-result1: (== -Flonum type-equal?)) #t] [_ #f]) + [(tc-result1: (== -Flonum subtypeof)) #t] [_ #f]) #:with opt #'e.opt)) (define-syntax-class int-opt-expr (pattern e:opt-expr #:when (match (type-of #'e) - [(tc-result1: (== -Integer (lambda (x y) (subtype y x)))) #t] [_ #f]) + [(tc-result1: (== -Integer subtypeof)) #t] [_ #f]) #:with opt #'e.opt)) (define-syntax-class fixnum-opt-expr (pattern e:opt-expr #:when (match (type-of #'e) - [(tc-result1: (== -Fixnum (lambda (x y) (subtype y x)))) #t] [_ #f]) + [(tc-result1: (== -Fixnum subtypeof)) #t] [_ #f]) #:with opt #'e.opt)) (define-syntax-class nonzero-fixnum-opt-expr (pattern e:opt-expr @@ -154,7 +158,7 @@ (pattern (~and res (#%plain-app (~var op (float-op binary-float-ops)) f1:float-arg-expr f2:float-arg-expr fs:float-arg-expr ...)) #:when (match (type-of #'res) ;; if the result is a float, we can coerce integers to floats and optimize - [(tc-result1: (== -Flonum type-equal?)) #t] [_ #f]) + [(tc-result1: (== -Flonum subtypeof)) #t] [_ #f]) #:with opt (begin (log-optimization "binary float" #'op) (n-ary->binary #'op.unsafe #'f1.opt #'f2.opt #'(fs.opt ...)))) diff --git a/collects/typed-scheme/scribblings/ts-reference.scrbl b/collects/typed-scheme/scribblings/ts-reference.scrbl index e96d08ef22..4e063ef263 100644 --- a/collects/typed-scheme/scribblings/ts-reference.scrbl +++ b/collects/typed-scheme/scribblings/ts-reference.scrbl @@ -37,6 +37,7 @@ any expression of this type will not evaluate to a value.} @defidform[Inexact-Complex] @defidform[Real] @defidform[Float] +@defidform[Nonnegative-Float] @defidform[Exact-Rational] @defidform[Integer] @defidform[Natural] diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.rkt b/collects/typed-scheme/typecheck/tc-expr-unit.rkt index 2a2139872a..cc65b03fb1 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.rkt +++ b/collects/typed-scheme/typecheck/tc-expr-unit.rkt @@ -41,6 +41,10 @@ [(~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 inexact-real? + (lambda (x) (or (positive? x) (zero? x))) + (lambda (x) (not (eq? x -0.0)))))) + -NonnegativeFlonum] [(~var i (3d inexact-real?)) -Flonum] [(~var i (3d real?)) -Real] ;; a complex number can't have an inexact imaginary part and an exact real part diff --git a/collects/typed-scheme/types/abbrev.rkt b/collects/typed-scheme/types/abbrev.rkt index bf40ffd2ab..a8203f4e7b 100644 --- a/collects/typed-scheme/types/abbrev.rkt +++ b/collects/typed-scheme/types/abbrev.rkt @@ -154,6 +154,9 @@ (define -InexactComplex (make-Base 'InexactComplex #'(and/c number? (lambda (x) (inexact-real? (imag-part x)))))) (define -Flonum (make-Base 'Flonum #'inexact-real?)) +(define -NonnegativeFlonum (make-Base 'Nonnegative-Flonum #'(and/c inexact-real? + (or/c positive? zero?) + (lambda (x) (not (eq? x -0.0)))))) (define -ExactRational (make-Base 'Exact-Rational #'(and/c number? rational? exact?))) diff --git a/collects/typed-scheme/types/subtype.rkt b/collects/typed-scheme/types/subtype.rkt index 8b9047c32b..6fa2969c8c 100644 --- a/collects/typed-scheme/types/subtype.rkt +++ b/collects/typed-scheme/types/subtype.rkt @@ -264,6 +264,10 @@ [((== -Fixnum =t) (Base: 'Exact-Rational _)) A0] [((== -Fixnum =t) (Base: 'Integer _)) A0] + [((Base: 'Nonnegative-Flonum _) (Base: 'Flonum _)) A0] + [((Base: 'Nonnegative-Flonum _) (Base: 'InexactComplex _)) A0] + [((Base: 'Nonnegative-Flonum _) (Base: 'Number _)) A0] + [((Base: 'InexactComplex _) (Base: 'Number _)) A0]