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

Added the Nonnegative-Float type.

Browse Source
This commit is contained in:
Vincent St-Amour 2010-06-29 12:12:41 -04:00
parent f026da5ecf
commit 62a15df3eb
11 changed files with 149 additions and 50 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
collects/tests/typed-scheme/fail/nonnegative-float.rkt Normal file
View File

@ -0,0 +1,5 @@
#;
(exn-pred 1)
#lang typed/scheme
(ann (- 1.0 0.5) Nonnegative-Float) ; can't prove it's nonnegative

6
collects/tests/typed-scheme/succeed/nonnegative-float.rkt Normal file
View File

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

2
collects/tests/typed-scheme/succeed/pair-test3.rkt
View File

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

16
collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt
View File

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

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

@ -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 (* <float> 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)
(-> -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]

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

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

12
collects/typed-scheme/private/optimize.rkt
View File

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

1
collects/typed-scheme/scribblings/ts-reference.scrbl
View File

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

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

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

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

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

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

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