Fixed erroneously imprecise type for +nan.f literal (now Single-Flonum-Nan)

Types for nan?, infinite?, pi.f, exact-round, exact-floor, exact-ceiling, exact-truncate, degrees->radians, radians->degrees Extended tc-random-testing: generates exact integers and rationals now Fixed types of sinh, cosh and tanh to account for underflow and NaNs original commit: 8f840bd07b28ac9bff22c2fa728fb16a9857cdb4
2012-06-09 17:45:22 -06:00 · 2012-06-09 17:45:22 -06:00 · 7f9aef2321
commit 7f9aef2321
parent 4b1a1cacd4
5 changed files with 260 additions and 67 deletions
--- a/collects/tests/typed-racket/random-real.rkt
+++ b/collects/tests/typed-racket/random-real.rkt
@ -0,0 +1,116 @@
+#lang racket
+
+(require unstable/flonum)
+
+(provide random-exponential random-laplace
+         random-flonum random-single-flonum
+         random-integer->random-exact-rational
+         random-integer->random-flonum
+         random-integer->random-single-flonum
+         random-integer->random-real)
+
+;; Returns a rational flonum from an exponential distribution
+;; About half the numbers from this distribution are < scale, and half are > scale
+(define (random-exponential [scale 1.0])
+  (let loop ()
+    (define r (random))
+    ;; appx. probability 1.11e-16 this loops:
+    (cond [(= r 0)  (loop)]
+          [else  (exact->inexact (* (- (log (random))) scale))])))
+
+;; Randomly signs a flonum from random-exponential
+(define (random-laplace [scale 1.0])
+  (define r (random-exponential scale))
+  (if ((random) . < . 0.5) r (- r)))
+
+;; Returns an integer from Uniform(0,2^64-1)
+(define (random-flonum-bits)
+  (for/fold ([i 0]) ([_  (in-range 4)])
+    (+ (* i #x10000) (random #x10000))))
+
+;; Returns a rational flonum with bits uniformly distributed
+(define (random-flonum)
+  (let loop ()
+    (define x (bit-field->flonum (random-flonum-bits)))
+    ;; appx. 0.0005 probability this loops
+    (if (rational? x) x (loop))))
+
+;; Returns a single flonum with bits uniformly distributed; sometimes -inf.f or +inf.f
+(define (random-single-flonum*)
+  (define s (random #b10))  ; sign bit
+  (define e (random #b100000000))  ; exponent
+  (define f (random #b100000000000000000000000))  ; fractional part
+  ;; Formula from Wikipedia page on IEEE 754 binary32 format
+  (real->single-flonum
+   (* (if (= s 0) 1 -1)
+      (+ 1 (/ f #b100000000000000000000000))
+      (expt 2 (- e 127)))))
+
+;; Returns a rational single flonum with bits uniformly distributed
+(define (random-single-flonum)
+  (let loop ()
+    (define x (random-single-flonum*))
+    (if (rational? x) x (loop))))
+
+;; Converts random integers to random exact rationals
+(define (random-integer->random-exact-rational E)
+  (cond
+    [(= E 0)  0]  ; code below would pick 0/0
+    [else
+     ;; random fraction
+     (define n (exact-ceiling (random-exponential E)))
+     (define d (exact-ceiling (random-exponential E)))
+     (cond
+       [(= d 0)  0]  ; appx. probability 1.11e-16
+       [else
+        (define x (/ n d))
+        (if ((random) . < . 0.5) x (- x))])]))
+
+;; Converts random integers to random double flonums
+;; Often returns very large or small numbers (near the limits of floating-point range)
+;; Sometimes returns +nan.0, +inf.0 or -inf.0
+(define (random-integer->random-flonum E)
+  (define r (random))
+  (cond
+    ;; probability 0.25: random flonum, laplace-distributed with scale E
+    [(r . < . 0.25)  (random-laplace (abs E))]
+    ;; probability 0.25: random flonum with uniform bits
+    [(r . < . 0.50)  (random-flonum)]
+    ;; probability 0.35: very small or very large flonum
+    [(r . < . 0.85)
+     (define r (random))
+     (cond [(r . < . 0.5)
+            (define x (ordinal->flonum E))
+            (cond [(= x 0.0)  (if ((random) . < . 0.5) 0.0 -0.0)]
+                  [else  x])]
+           [(r . < . 0.75)
+            (flstep -inf.0 (abs E))]
+           [else
+            (flstep +inf.0 (- (abs E)))])]
+    ;; probability 0.05 each: +nan.0, +inf.0, -inf.0
+    [(r . < . 0.90)  +nan.0]
+    [(r . < . 0.95)  +inf.0]
+    [else            -inf.0]))
+
+;; Converts random integers to random single flonums
+;; Sometimes returns +nan.f, +inf.f or -inf.f
+(define (random-integer->random-single-flonum E)
+  (define r (random))
+  (cond
+    ;; probability 0.50: random single flonum, laplace-distributed with scale E
+    [(r . < . 0.50)  (real->single-flonum (random-laplace (abs E)))]
+    ;; probability 0.35: random single flonum with uniform bits
+    [(r . < . 0.85)  (random-single-flonum)]
+    ;; probability 0.05 each: +nan.f, +inf.f, -inf.f
+    [(r . < . 0.90)  +nan.f]
+    [(r . < . 0.95)  +inf.f]
+    [else            -inf.f]))
+
+;; Converts random integers to random reals
+(define (random-integer->random-real E)
+  (define r (random))
+  ;; probability 0.25 each
+  (cond [(r . < . 0.25)  r]
+        [(r . < . 0.50)  (random-integer->random-exact-rational E)]
+        [(r . < . 0.75)  (random-integer->random-flonum E)]
+        [else            (random-integer->random-single-flonum E)]))
--- a/collects/tests/typed-racket/tr-random-testing.rkt
+++ b/collects/tests/typed-racket/tr-random-testing.rkt
@ -1,10 +1,11 @@
 #lang racket

-;; Random testing of type preservation for floats.
+;; Random testing of type preservation for reals.

 (require redex
-         racket/flonum racket/unsafe/ops unstable/flonum
-         racket/sandbox)
+         racket/flonum racket/unsafe/ops
+         racket/sandbox
+         "random-real.rkt")

 (require (except-in typed-racket/utils/utils infer)
         (typecheck typechecker)
@ -18,12 +19,26 @@
 (b:init) (n:init)
 (define-namespace-anchor anch)

-;; TODO exact numbers
-
-(define-language tr-arith ; to stay within floats, removed some numeric ops
+(define-language tr-arith
  [n real]
-  [E n
-     (* E)
+  ;; randomly generate F, not E, because literal numbers self-evaluate
+  ;; (i.e. generates a useless test)
+  [E n F]
+  #;; racket/math
+  [F (degrees->radians E)
+     (radians->degrees E)
+     (exact-round E)
+     (exact-floor E)
+     (exact-ceiling E)
+     (exact-truncate E)
+     (sinh E)
+     (cosh E)
+     (tanh E)
+     (nan? E)
+     (infinite? E)
+     ]
+  ;; racket/base, racket/flonum, racket/unsafe/ops
+  [F (* E)
     (* E E)
     (* E E E)
     (+ E)
@ -48,7 +63,9 @@
     (ceiling E)
     (truncate E)
     (round E)
-     (log E)
+     ;; uncomment when single-flonum complex types are fixed
+     ;(sqrt E)
+     ;(log E)
     (exp E)
     (cos E)
     (sin E)
@ -96,50 +113,34 @@

 (define (right-type? before)
  (define type-before (match (get-type before) [(tc-result1: b) b]))
-  (define after (eval before (namespace-anchor->namespace anch)))
-  (define type-after (get-type after tc-literal))
-  (define subtype? (subtype type-after type-before))
-  subtype?)
+  (define after (with-handlers ([values values])
+                  (eval before (namespace-anchor->namespace anch))))
+  (cond [(exn? after)  #t]
+        [else
+         (define type-after (get-type after tc-literal))
+         (define subtype? (subtype type-after type-before))
+         (unless subtype?
+           (printf "type-before = ~v~ntype-after = ~v~n" type-before type-after))
+         subtype?]))

-;; Takes random redex reals (mostly integers, sometimes rationals, floats
-;; once in a blue moon).
-(define (random->random-float E)
-  (define r (random))
-  (cond
-    ;; probability 1/4: noisify and convert to single flonum
-    [(r . < . 0.25)
-     (real->single-flonum (* (random) E))]
-    ;; probability 1/4: noisify and convert to double flonum
-    [(r . < . 0.5)
-     (real->double-flonum (* (random) E))]
-    ;; probability 1/4: convert to very small double flonum
-    [(r . < . 0.75)
-     (define x (ordinal->flonum (round (inexact->exact E))))
-     (cond [(= x 0.0)  (if ((random) . < . 0.5) 0.0 -0.0)]
-           [else  x])]
-    ;; probability 1/20: +nan.0
-    [(r . < . 0.8)
-     +nan.0]
-    ;; remaining probability: convert to very large double flonum
-    [else
-     (if ((random) . < . 0.5)
-         (flstep -inf.0 (round (inexact->exact E)))
-         (flstep +inf.0 (- (round (inexact->exact E)))))]))
-
-;; Redex can't generate floats, so we convert ints to floats.
-(define (exp->float-exp E) ; numbers or symbols or lists
+;; Redex can't generate reals, so we convert ints to reals.
+(define (exp->real-exp E) ; numbers or symbols or lists
  (cond [(number? E)
-         (random->random-float E)]
+         (random-integer->random-real (exact-round E))]
        [(list? E)
-         (map exp->float-exp E)]
+         (map exp->real-exp E)]
        [else
         E]))

-(define (check-all-floats sexp)
+(define num-exceptions 0)
+
+(define (check-all-reals sexp)
  (or (with-handlers
          ;; something went wrong, almost certainly typechecking failed
          ;; in which case we ignore the expression
-          ([exn? (const #t)])
+          ([exn?  (λ (e)
+                    (set! num-exceptions (+ num-exceptions 1))
+                    #t)])
        (get-type sexp)
        #f) ; go on and check preservation
      (right-type? sexp)))
@ -147,6 +148,8 @@
 (call-with-limits
 #f 1000
 (lambda ()
-   (redex-check tr-arith E (check-all-floats (term E))
-                #:attempts 500
-                #:prepare exp->float-exp)))
+   (redex-check tr-arith F (check-all-reals (term F))
+                #:attempts 1000
+                #:prepare exp->real-exp)))
+
+;(printf "bad tests (usually typechecking failed): ~v~n" num-exceptions)
--- a/collects/typed-racket/base-env/base-env-numeric.rkt
+++ b/collects/typed-racket/base-env/base-env-numeric.rkt
@ -91,7 +91,22 @@
                       -InexactRealPosZero -InexactRealNegZero -InexactRealZero
                       -NonNegInexactReal -NonPosInexactReal -InexactReal
                       -RealZero -NonNegReal -NonPosReal -Real)))))
-
+  
+  (define (inexact-zero->exact-zero-type)
+    (for/list ([t  (list -FlonumPosZero -FlonumNegZero -FlonumZero
+                         -SingleFlonumPosZero -SingleFlonumNegZero -SingleFlonumZero
+                         -InexactRealPosZero -InexactRealNegZero -InexactRealZero
+                         -RealZero)])
+      (-> t -Zero)))
+  
+  (define (exact-round-type) ; also used for exact-truncate
+    (from-cases
+     (map unop all-int-types)
+     (inexact-zero->exact-zero-type)
+     (-> (Un -NonNegRat -NonNegFlonum -NonNegSingleFlonum -NonNegInexactReal -NonNegReal) -Nat)
+     (-> (Un -NonPosRat -NonPosFlonum -NonPosSingleFlonum -NonPosInexactReal -NonPosReal) -NonPosInt)
+     (-> (Un -Rat -Flonum -SingleFlonum -InexactReal -Real) -Int)))
+  
  (define fl-unop (lambda () (unop -Flonum)))

  ;; types for specific operations, to avoid repetition between safe and unsafe versions
@ -1810,6 +1825,7 @@
            (-Real . -> . -Real))]

 [pi -PosFlonum]
+[pi.f -PosSingleFlonum]
 [sqr (from-cases (map unop (list -Zero -One))
                 (-> -PosByte -PosIndex)
                 (-> -Byte -Index)
@ -1836,29 +1852,90 @@
            (N . -> . N))]
 [sinh (from-cases
       (unop -Zero) ; only exact case
-       ((Un -PosRat -PosFlonum) . -> . -PosFlonum)
-       ((Un -NegRat -NegFlonum) . -> . -NegFlonum)
-       (map unop (list -NonNegFlonum -NonPosFlonum
-                       -PosSingleFlonum -NonNegSingleFlonum -NegSingleFlonum -NonPosSingleFlonum -SingleFlonum
+       ((Un -PosRat -PosFlonum) . -> . -NonNegFlonum) ; possible underflow, no pos -> pos
+       ((Un -NegRat -NegFlonum) . -> . -NonPosFlonum)
+       ((Un -PosSingleFlonum) . -> . -NonNegSingleFlonum)
+       ((Un -NegSingleFlonum) . -> . -NonPosSingleFlonum)
+       (map unop (list -FlonumNan -NonNegFlonum -NonPosFlonum -Flonum
+                       -SingleFlonumNan -PosSingleFlonum -NonNegSingleFlonum -NegSingleFlonum -NonPosSingleFlonum -SingleFlonum
                       -PosInexactReal -NonNegInexactReal -NegInexactReal -NonPosInexactReal -InexactReal
                       -PosReal -NonNegReal -NegReal -NonPosReal -Real
                       -FloatComplex -SingleFlonumComplex -InexactComplex N)))]
 [cosh (from-cases ; no exact cases
-       ((Un -Rat -Flonum) . -> . -PosFlonum)
-       (-SingleFlonum . -> . -PosSingleFlonum)
-       (-InexactReal . -> . -PosInexactReal)
+       (map unop (list -FlonumNan -SingleFlonumNan))
+       ((Un -Rat -Flonum) . -> . (Un -PosFlonum -FlonumNan))
+       (-SingleFlonum . -> . (Un -PosSingleFlonum -SingleFlonumNan))
+       (-InexactReal . -> . (Un -PosInexactReal -InexactRealNan))
       (-Real . -> . -PosReal)
       (map unop (list -FloatComplex -SingleFlonumComplex -InexactComplex N)))]
 [tanh (from-cases ; same as sinh
       (unop -Zero) ; only exact case
-       ((Un -PosRat -PosFlonum) . -> . -PosFlonum)
-       ((Un -NegRat -NegFlonum) . -> . -NegFlonum)
-       (map unop (list -NonNegFlonum -NonPosFlonum
-                       -PosSingleFlonum -NonNegSingleFlonum -NegSingleFlonum -NonPosSingleFlonum -SingleFlonum
+       ((Un -PosRat -PosFlonum) . -> . -NonNegFlonum) ; possible underflow, no pos -> pos
+       ((Un -NegRat -NegFlonum) . -> . -NonPosFlonum)
+       ((Un -PosSingleFlonum) . -> . -NonNegSingleFlonum)
+       ((Un -NegSingleFlonum) . -> . -NonPosSingleFlonum)
+       (map unop (list -FlonumNan -NonNegFlonum -NonPosFlonum -Flonum
+                       -SingleFlonumNan -PosSingleFlonum -NonNegSingleFlonum -NegSingleFlonum -NonPosSingleFlonum -SingleFlonum
                       -PosInexactReal -NonNegInexactReal -NegInexactReal -NonPosInexactReal -InexactReal
                       -PosReal -NonNegReal -NegReal -NonPosReal -Real
                       -FloatComplex -SingleFlonumComplex -InexactComplex N)))]

+[degrees->radians
+ (from-cases
+  (unop -Zero) ; only exact case
+  ((Un -PosRat -PosFlonum) . -> . -NonNegFlonum) ; possible underflow, no pos -> pos
+  ((Un -NegRat -NegFlonum) . -> . -NonPosFlonum)
+  ((Un -PosSingleFlonum) . -> . -NonNegSingleFlonum)
+  ((Un -NegSingleFlonum) . -> . -NonPosSingleFlonum)
+  (map unop (list -FlonumNan -SingleFlonumNan
+                  -NonNegFlonum -NonPosFlonum -Flonum
+                  -NonNegSingleFlonum -NonPosSingleFlonum -SingleFlonum
+                  -PosInexactReal -NonNegInexactReal -NegInexactReal -NonPosInexactReal -InexactReal
+                  -PosReal -NonNegReal -NegReal -NonPosReal -Real)))]
+
+[radians->degrees
+ (from-cases
+  (unop -Zero) ; only exact case
+  ((Un -PosRat -PosFlonum) . -> . -PosFlonum)
+  ((Un -NegRat -NegFlonum) . -> . -NegFlonum)
+  (map unop (list -FlonumNan -SingleFlonumNan
+                  -NonNegFlonum -NonPosFlonum -Flonum
+                  -PosSingleFlonum -NonNegSingleFlonum -NegSingleFlonum -NonPosSingleFlonum -SingleFlonum
+                  -PosInexactReal -NonNegInexactReal -NegInexactReal -NonPosInexactReal -InexactReal
+                  -PosReal -NonNegReal -NegReal -NonPosReal -Real)))]
+
+[exact-round (exact-round-type)]
+[exact-truncate (exact-round-type)]
+
+[exact-floor
+ (from-cases
+  (map unop all-int-types)
+  (inexact-zero->exact-zero-type)
+  (-> (Un -NonNegRat -NonNegFlonum -NonNegSingleFlonum -NonNegInexactReal -NonNegReal) -Nat)
+  (-> (Un -NegRat -NegFlonum -NegSingleFlonum -NegInexactReal -NegReal) -NegInt)
+  (-> (Un -NonPosRat -NonPosFlonum -NonPosSingleFlonum -NonPosInexactReal -NonPosReal) -NonPosInt)
+  (-> (Un -Rat -Flonum -SingleFlonum -InexactReal -Real) -Int))]
+
+[exact-ceiling
+ (from-cases
+  (map unop all-int-types)
+  (inexact-zero->exact-zero-type)
+  (-> (Un -PosRat -PosFlonum -PosSingleFlonum -PosInexactReal -PosReal) -PosInt)
+  (-> (Un -NonNegRat -NonNegFlonum -NonNegSingleFlonum -NonNegInexactReal -NonNegReal) -Nat)
+  (-> (Un -NonPosRat -NonPosFlonum -NonPosSingleFlonum -NonPosInexactReal -NonPosReal) -NonPosInt)
+  (-> (Un -Rat -Flonum -SingleFlonum -InexactReal -Real) -Int))]
+
+[nan? (from-cases
+       (-> (Un -PosFlonum -NonPosFlonum -PosSingleFlonum -NonPosSingleFlonum -Rat) (-val #f))
+       (-> (Un -FlonumNan -SingleFlonumNan) (-val #t))
+       (-> -Real B))]
+
+[infinite? (from-cases
+            (-> (Un -FlonumNan -FlonumNegZero -FlonumPosZero
+                    -SingleFlonumNan -SingleFlonumNegZero -SingleFlonumPosZero
+                    -Rat)
+                (-val #f))
+            (-> -Real B))]

 ;; scheme/fixnum
 [fx+ (fx+-type)]
--- a/collects/typed-racket/typecheck/tc-expr-unit.rkt
+++ b/collects/typed-racket/typecheck/tc-expr-unit.rkt
@ -49,14 +49,13 @@
      [(~var i (3d (conjoin number? exact? rational? negative?))) -NegRat]
      [(~var i (3d (lambda (x) (eqv? x 0.0)))) -FlonumPosZero]
      [(~var i (3d (lambda (x) (eqv? x -0.0)))) -FlonumNegZero]
-      ;; eqv? equates single and double flonum NaNs
-      [(~var i (3d (lambda (x) (and (flonum? x) (eqv? x +nan.0))))) -FlonumNan]
+      [(~var i (3d (lambda (x) (eqv? x +nan.0)))) -FlonumNan]
      [(~var i (3d (conjoin flonum? positive?))) -PosFlonum]
      [(~var i (3d (conjoin flonum? negative?))) -NegFlonum]
      [(~var i (3d flonum?)) -Flonum] ; for nan
      [(~var i (3d (lambda (x) (eqv? x 0.0f0)))) -SingleFlonumPosZero]
      [(~var i (3d (lambda (x) (eqv? x -0.0f0)))) -SingleFlonumNegZero]
-      [(~var i (3d (lambda (x) (and (single-flonum? x) (eqv? x +nan.0))))) -SingleFlonumNan]
+      [(~var i (3d (lambda (x) (eqv? x +nan.f)))) -SingleFlonumNan]
      [(~var i (3d (conjoin single-flonum? positive?))) -PosSingleFlonum]
      [(~var i (3d (conjoin single-flonum? negative?))) -NegSingleFlonum]
      [(~var i (3d single-flonum?)) -SingleFlonum] ; for nan
--- a/collects/typed-racket/types/numeric-tower.rkt
+++ b/collects/typed-racket/types/numeric-tower.rkt
@ -173,11 +173,9 @@
 	     #'-SingleFlonumNegZero))
 (define -SingleFlonumZero (*Un -SingleFlonumPosZero -SingleFlonumNegZero))
 (define -SingleFlonumNan (make-Base 'Single-Flonum-Nan
-                                  #'(and/c single-flonum?
-                                           ;; eqv? equates single and double precision nans
-                                           (lambda (x) (eqv? x +nan.0)))
-                                  (lambda (x) #f)
-				  #'-SingleFlonumNan))
+                                    #'(and/c single-flonum? (lambda (x) (eqv? x +nan.f)))
+                                    (lambda (x) (and (single-flonum? x) (eqv? x +nan.f)))
+                                    #'-SingleFlonumNan))
 (define -InexactRealPosZero (*Un -SingleFlonumPosZero -FlonumPosZero))
 (define -InexactRealNegZero (*Un -SingleFlonumNegZero -FlonumNegZero))
 (define -InexactRealZero    (*Un -InexactRealPosZero