From 8f840bd07b28ac9bff22c2fa728fb16a9857cdb4 Mon Sep 17 00:00:00 2001 From: Neil Toronto Date: Sat, 9 Jun 2012 17:45:22 -0600 Subject: [PATCH] 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 --- collects/racket/math.rkt | 3 +- collects/tests/racket/math.rktl | 2 +- collects/tests/typed-racket/random-real.rkt | 116 ++++++++++++++++++ .../tests/typed-racket/tr-random-testing.rkt | 97 ++++++++------- .../base-env/base-env-numeric.rkt | 101 +++++++++++++-- .../typed-racket/typecheck/tc-expr-unit.rkt | 5 +- collects/typed-racket/types/numeric-tower.rkt | 8 +- 7 files changed, 263 insertions(+), 69 deletions(-) create mode 100644 collects/tests/typed-racket/random-real.rkt diff --git a/collects/racket/math.rkt b/collects/racket/math.rkt index be1dc5b9e6..7b646964f2 100644 --- a/collects/racket/math.rkt +++ b/collects/racket/math.rkt @@ -65,7 +65,8 @@ (define (cosh z) (unless (number? z) (raise-argument-error 'cosh "number?" z)) - (/ (+ (exp z) (exp (- z))) 2)) + (cond [(and (real? z) (= z 0)) (if (single-flonum? z) 1.0f0 1.0)] + [else (/ (+ (exp z) (exp (- z))) 2)])) (define (tanh z) (unless (number? z) (raise-argument-error 'tanh "number?" z)) diff --git a/collects/tests/racket/math.rktl b/collects/tests/racket/math.rktl index 70dafb17ab..4a0dab02ec 100644 --- a/collects/tests/racket/math.rktl +++ b/collects/tests/racket/math.rktl @@ -174,7 +174,7 @@ (define cosh+1 #e1.5430806348152437784779056207570616826015291123659) (test #t double=? cosh+1 (cosh -1)) -(test 1 cosh 0) +(test 1.0 cosh 0) (test #t double=? cosh+1 (cosh 1)) (test +nan.f cosh +nan.f) diff --git a/collects/tests/typed-racket/random-real.rkt b/collects/tests/typed-racket/random-real.rkt new file mode 100644 index 0000000000..996e8b3a9c --- /dev/null +++ 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)])) diff --git a/collects/tests/typed-racket/tr-random-testing.rkt b/collects/tests/typed-racket/tr-random-testing.rkt index b38de94361..e50ce2c346 100644 --- 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) diff --git a/collects/typed-racket/base-env/base-env-numeric.rkt b/collects/typed-racket/base-env/base-env-numeric.rkt index df519e97ab..18f342baa7 100644 --- 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)] diff --git a/collects/typed-racket/typecheck/tc-expr-unit.rkt b/collects/typed-racket/typecheck/tc-expr-unit.rkt index 678a1aac7e..53072de85b 100644 --- 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 diff --git a/collects/typed-racket/types/numeric-tower.rkt b/collects/typed-racket/types/numeric-tower.rkt index b4a82be762..2d9d1cca8e 100644 --- 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