122 lines
5.4 KiB
Plaintext
122 lines
5.4 KiB
Plaintext
;;;; The prelude's type limits, checked against something other than themselves.
|
|
;;;;
|
|
;;;; A wrong constant here would compile. That is the whole reason this program
|
|
;;;; exists: i32-max off by one, or f64-max one ulp low, is a number the
|
|
;;;; compiler has no opinion about, and it would sit in the prelude being
|
|
;;;; subtly wrong in every program that read it. So nothing below asserts a
|
|
;;;; constant against the way it is spelled in the prelude.
|
|
;;;;
|
|
;;;; The integers are checked by printing them. The expected output beside this
|
|
;;;; program in test_acceptance is the decimal spelling of each limit, written
|
|
;;;; out independently, and an integer's decimal rendering is exact — so the
|
|
;;;; comparison is the whole value and not an approximation of it. u64-max is
|
|
;;;; the one that matters most: it is written in hex in the prelude, because
|
|
;;;; the reader cannot take its decimal, and this is where that hex is read
|
|
;;;; back as the number it is supposed to name.
|
|
;;;;
|
|
;;;; The floats cannot be checked that way, because printing one is snprintf
|
|
;;;; "%g" and that is six significant digits — 3.40282e+38 is equally true of
|
|
;;;; f32-max and of a dozen values around it. So each is *derived* here by
|
|
;;;; exact power-of-two arithmetic and compared for equality. Every step of
|
|
;;;; that derivation is exact in IEEE-754: doubling and halving a float only
|
|
;;;; moves the exponent, and the one multiplication that is not a power of two
|
|
;;;; has both operands representable and a representable product. The
|
|
;;;; derivations are therefore a second, independent construction of the same
|
|
;;;; bit pattern, which is what a pin needs to be.
|
|
|
|
;; 2^n, built by repeated doubling from 1.0 and reciprocated for a negative n.
|
|
;; Exact for every n this program asks for: the largest is 2^1023, which is
|
|
;; half of f64-max and so is nowhere near overflowing, and the smallest is
|
|
;; 2^-1022, whose reciprocal partner 2^1022 is a normal value — so no step
|
|
;; passes through a subnormal, where the halving would start losing bits.
|
|
(defn p2-f64 [n i32] f64
|
|
(let [m (if (< n 0) (- 0 n) n)
|
|
x 1.0]
|
|
(dotimes [i m]
|
|
(set x (* x 2.0)))
|
|
(if (< n 0) (/ 1.0 x) x)))
|
|
|
|
;; The same, at f32's width and with f32's exponent range. 2^127 is the
|
|
;; largest normal power of two an f32 holds and 2^-126 the smallest, and both
|
|
;; are exactly the ends this file asks for.
|
|
(defn p2-f32 [n i32] f32
|
|
(let [m (if (< n 0) (- 0 n) n)
|
|
x (f32 1.0)]
|
|
(dotimes [i m]
|
|
(set x (* x (f32 2.0))))
|
|
(if (< n 0) (/ (f32 1.0) x) x)))
|
|
|
|
;; An infinity is a value that equals its own double and is not zero — the
|
|
;; same test format-f64 in the prelude uses, and the only one available with
|
|
;; no infinity literal to compare against.
|
|
(defn inf-f64? [x f64] bool
|
|
(and (= x (* x 2.0)) (!= x 0.0)))
|
|
|
|
(defn inf-f32? [x f32] bool
|
|
(and (= x (* x (f32 2.0))) (!= x (f32 0.0))))
|
|
|
|
(defn say [name string ok bool] ()
|
|
(print name)
|
|
(print " ")
|
|
(println (if ok "ok" "WRONG")))
|
|
|
|
(defn main [] i32
|
|
;; The integers, each printed as the exact decimal the expected output pins.
|
|
(println i8-max)
|
|
(println i8-min)
|
|
(println i16-max)
|
|
(println i16-min)
|
|
(println i32-max)
|
|
(println i32-min)
|
|
(println i64-max)
|
|
(println i64-min)
|
|
(println u8-max)
|
|
(println u8-min)
|
|
(println u16-max)
|
|
(println u16-min)
|
|
(println u32-max)
|
|
(println u32-min)
|
|
(println u64-max)
|
|
(println u64-min)
|
|
|
|
;; The floats, each against its derivation.
|
|
;;
|
|
;; An epsilon is the gap from 1.0 to the next value above it, which is
|
|
;; 2^-(mantissa bits): 23 for an f32, 52 for an f64. Derived that way here,
|
|
;; and then confirmed by the property the name actually promises — adding it
|
|
;; to 1.0 moves, adding half of it does not.
|
|
(say "f32-epsilon" (= f32-epsilon (p2-f32 -23)))
|
|
(say "f64-epsilon" (= f64-epsilon (p2-f64 -52)))
|
|
(say "f32-epsilon is the step above 1.0"
|
|
(and (!= (+ (f32 1.0) f32-epsilon) (f32 1.0))
|
|
(= (+ (f32 1.0) (/ f32-epsilon (f32 2.0))) (f32 1.0))))
|
|
(say "f64-epsilon is the step above 1.0"
|
|
(and (!= (+ 1.0 f64-epsilon) 1.0)
|
|
(= (+ 1.0 (/ f64-epsilon 2.0)) 1.0)))
|
|
|
|
;; The smallest positive *normal* value is 2^(1-bias): 2^-126 and 2^-1022.
|
|
;; Halving one leaves the normals, so the value below it is not simply half
|
|
;; — that is the property that says this is the boundary and not some value
|
|
;; near it.
|
|
(say "f32-min-positive" (= f32-min-positive (p2-f32 -126)))
|
|
(say "f64-min-positive" (= f64-min-positive (p2-f64 -1022)))
|
|
|
|
;; The greatest finite value is (2 - 2^-mantissa) * 2^maxexp. Both factors
|
|
;; are exactly representable and so is the product, which is why this
|
|
;; derivation is an equality and not a near-miss. Doubling it overflows to
|
|
;; an infinity, which is the other end of the same claim: there is nothing
|
|
;; finite above it.
|
|
(say "f32-max" (= f32-max (* (p2-f32 127) (- (f32 2.0) (p2-f32 -23)))))
|
|
(say "f64-max" (= f64-max (* (p2-f64 1023) (- 2.0 (p2-f64 -52)))))
|
|
(say "f32-max is the last finite f32" (inf-f32? (* f32-max (f32 2.0))))
|
|
(say "f64-max is the last finite f64" (inf-f64? (* f64-max 2.0)))
|
|
|
|
;; And the two the language does not need a constant for, said once so that
|
|
;; the absence is recorded rather than merely unmentioned: a float's least
|
|
;; value is the negation of its greatest, and there is nothing to derive.
|
|
(say "f32's least value negates its greatest"
|
|
(< (- (f32 0.0) f32-max) (- (f32 0.0) f32-min-positive)))
|
|
(say "f64's least value negates its greatest"
|
|
(< (- 0.0 f64-max) (- 0.0 f64-min-positive)))
|
|
0)
|