float

machine.FloatFormat

record FloatFormat

A binary format: bits of precision, the greatest exponent, the width of an object of it in bits (its storage: what follows the value is padding), the width of the exponent, and whether the integer bit of the significand is stored (x87’s extended format) rather than hidden (IEEE 754’s interchange formats).

machine.FloatFormat.binary64

def FloatFormat.binary64 : FloatFormat

IEEE 754 binary64 (a double).

machine.FloatFormat.binary32

def FloatFormat.binary32 : FloatFormat

IEEE 754 binary32 (a float).

machine.FloatFormat.x87Extended

def FloatFormat.x87Extended : FloatFormat

The x87 extended format (x86-64 System V’s long double): a 64-bit significand with its integer bit stored, a 15-bit exponent and the sign, 80 bits kept in 16 bytes (the last 6 are padding).

machine.FloatFormat.same

def FloatFormat.same (f : FloatFormat) (g : FloatFormat) : Bool

Whether the formats f and g are the same format (same precision and exponent range).

machine.FloatFormat.minQuantum

def FloatFormat.minQuantum (f : FloatFormat) : Int

The exponent of the smallest subnormal step of the format f: 2 - maxExponent - precision.

machine.FloatFormat.maxQuantum

def FloatFormat.maxQuantum (f : FloatFormat) : Int

The exponent of the last step below infinity in the format f: maxExponent - precision + 1.

machine.Float

data Float

A floating-point value: NaN, a signed infinity, or negative-or-not mantissa * 2^exponent (zero has mantissa 0).

machine.Float.zero

def Float.zero (f : FloatFormat) (negative : Bool) : Float

Zero of the format f, negative when negative is true.

machine.Float.divideRounded

def Float.divideRounded (a : Nat) (b : Nat) : Nat

Division rounded to nearest, ties to even: round(a / b).

machine.Float.floorLog2

def Float.floorLog2 (n : Nat) (d : Nat) : Int

The floor of log2 (n / d) for positive n and d.

machine.Float.roundFinish

def Float.roundFinish (f : FloatFormat) (negative : Bool) (m : Nat) (k : Int) : Float

Finishes rounding to the format f the mantissa m at quantum k, with the sign negative: a mantissa that reached 2^precision carries into the exponent; past the range is infinity.

machine.Float.ofRatio

def Float.ofRatio (f : FloatFormat) (negative : Bool) (n : Nat) (d : Nat) : Float

Rounds the rational n / d (d > 0), negated when negative, to the format f; n = 0 is a signed zero.

machine.Float.ofBinary

def Float.ofBinary (f : FloatFormat) (negative : Bool) (m : Nat) (e : Int) : Float

Rounds the binary value m * 2^e, negated when negative, to the format f, without building 2^e as a numerator or denominator.

machine.Float.decimalNumerator

def Float.decimalNumerator (m : Nat) (e : Int) : Nat

The numerator of m * 10^e as a ratio: m * 10^e when e >= 0, else m.

machine.Float.decimalDenominator

def Float.decimalDenominator (e : Int) : Nat

The denominator of m * 10^e as a ratio: 10^-e when e < 0, else 1.

machine.Float.ofDecimal

def Float.ofDecimal (f : FloatFormat) (negative : Bool) (m : Nat) (e : Int) : Float

Rounds the decimal value m * 10^e, negated when negative, to the format f. A value at least 10^t, with 3t past the greatest exponent, is infinite; one below 10^t, with 3t under the smallest quantum, rounds to zero; neither builds 10^e.

machine.FloatFormat.hiddenBit

def FloatFormat.hiddenBit (f : FloatFormat) : Nat

The value of the hidden bit of the format f: 2^(precision - 1); a normal mantissa is at least this, a subnormal one below.

machine.FloatFormat.topExponent

def FloatFormat.topExponent (f : FloatFormat) : Nat

The all-ones biased exponent of the format f, which marks infinity and NaN.

machine.FloatFormat.fractionBits

def FloatFormat.fractionBits (f : FloatFormat) : Nat

The bits of the significand field of the format f: the precision with a stored integer bit, one fewer without.

machine.FloatFormat.valueWidth

def FloatFormat.valueWidth (f : FloatFormat) : Nat

The bits the value of the format f takes (the significand field, the exponent and the sign); the rest of f.width is padding.

machine.FloatFormat.signBit

def FloatFormat.signBit (f : FloatFormat) : Nat

The value of the sign bit of the format f: the bit above the exponent.

machine.FloatFormat.exponentUnit

def FloatFormat.exponentUnit (f : FloatFormat) : Nat

The value of the lowest exponent bit of the format f: the bit above the significand field.

machine.FloatFormat.quietFraction

def FloatFormat.quietFraction (f : FloatFormat) : Nat

The fraction of the quiet NaN of the format f: only its top bit set.

machine.Float.encode

def Float.encode (f : FloatFormat) (negative : Bool) (biased : Nat) (fraction : Nat) : Nat

Encodes the sign negative, the biased exponent and the significand field fraction into the bits of the format f.

machine.FloatFormat.storedInteger

def FloatFormat.storedInteger (f : FloatFormat) : Nat

The integer bit the significand field of the format f stores for a normal value, an infinity or a NaN: the hidden bit when it is stored, else nothing.

machine.Float.encodeFinite

def Float.encodeFinite (f : FloatFormat) (negative : Bool) (m : Nat) (e : Int) : Nat

The bits in the format f of the normalized finite value m * 2^e, negated when negative: a normal one stores its exponent biased (the smallest quantum is biased exponent 1) and its significand without the hidden bit (with it when the format stores the integer bit); a subnormal one or zero has biased exponent 0.

machine.Float.toBits

def Float.toBits (f : FloatFormat) (v : Float) : Nat

The encoding of the value v in the format f (IEEE 754’s, or x87’s with the integer bit stored), as a number below 2^(the value’s width). A finite value is first rounded to the format; NaN, which carries no payload here, is the positive quiet NaN (top fraction bit set).

machine.Float.ofBits

def Float.ofBits (f : FloatFormat) (bits : Nat) : Float

The value of the encoding bits in the format f (bits above the value’s width are ignored); every NaN encoding is NaN. With the integer bit stored (x87), an encoding whose integer bit disagrees with its exponent (an unnormal, a pseudo-infinity, a pseudo-NaN) is an invalid operand, read as NaN; a pseudo-denormal (exponent 0, integer bit set) has the value its bits give.

machine.Float.isNan

def Float.isNan (v : Float) : Bool

Whether the value v is NaN.

machine.Float.isZero

def Float.isZero (v : Float) : Bool

Whether the value v is a zero of either sign.

machine.Float.numerator

def Float.numerator (m : Nat) (e : Int) : Nat

The numerator of m * 2^e as a rational: m * 2^e when e >= 0, otherwise m.

machine.Float.denominator

def Float.denominator (e : Int) : Nat

The denominator of m * 2^e as a rational.

machine.Float.signed

def Float.signed (negative : Bool) (a : Nat) : Int

The integer with a sign: -a when negative.

machine.Float.negate

def Float.negate (v : Float) : Float

The negation of v (NaN stays NaN).

machine.Float.addFinite

def Float.addFinite (f : FloatFormat) (s1 : Bool) (m1 : Nat) (e1 : Int) (s2 : Bool) (m2 : Nat) (e2 : Int) : Float

The sum of the finite values m1 * 2^e1 (negative when s1) and m2 * 2^e2 (negative when s2): exact on a common exponent, then rounded to the format f.

machine.Float.add

def Float.add (f : FloatFormat) (x : Float) (y : Float) : Float

x + y, correctly rounded to the format f.

machine.Float.subtract

def Float.subtract (f : FloatFormat) (x : Float) (y : Float) : Float

x - y, correctly rounded to the format f.

machine.Float.multiply

def Float.multiply (f : FloatFormat) (x : Float) (y : Float) : Float

x * y, correctly rounded to the format f.

machine.Float.divide

def Float.divide (f : FloatFormat) (x : Float) (y : Float) : Float

x / y, correctly rounded to the format f (dividing a finite nonzero value by zero gives infinity; whether that is allowed is the language’s rule).

machine.Float.lessFinite

def Float.lessFinite (s1 : Bool) (m1 : Nat) (e1 : Int) (s2 : Bool) (m2 : Nat) (e2 : Int) : Bool

Whether the finite value m1 * 2^e1 (negative when s1) is below m2 * 2^e2 (negative when s2); zeros of either sign are equal.

machine.Float.less

def Float.less (x : Float) (y : Float) : Bool

Ordered less-than, x < y: false when either side is NaN.

machine.Float.equal

def Float.equal (x : Float) (y : Float) : Bool

Ordered equality of x and y: NaN equals nothing, +0 equals -0.

machine.Float.lessOrEqual

def Float.lessOrEqual (x : Float) (y : Float) : Bool

Ordered less-than-or-equal, x <= y: false when either side is NaN.

machine.Float.ofInt

def Float.ofInt (f : FloatFormat) (v : Int) : Float

The integer v rounded to the format f.

machine.Float.convert

def Float.convert (g : FloatFormat) (v : Float) : Float

The value v rounded to another format g.

machine.Float.truncate

def Float.truncate (v : Float) : Option Int

The integer part of v, rounding toward zero; none for NaN and infinities.

machine.Float.squareRootFinite

def Float.squareRootFinite (f : FloatFormat) (m : Nat) (e : Int) : Float

The square root of a positive finite value m * 2^e, rounded to the format f: the exponent is made even, the mantissa widened past twice the precision, and a sticky bit (2r + 1) keeps an inexact root from looking like an exact tie.

machine.Float.squareRoot

def Float.squareRoot (f : FloatFormat) (v : Float) : Float

The square root of v, correctly rounded to the format f: NaN for negative values and NaN; -0 stays -0.

machine.RoundingDirection

data RoundingDirection

Which way to round a value to an integer.

machine.RoundingDirection.roundsUp

def RoundingDirection.roundsUp (direction : RoundingDirection) (negative : Bool) (r : Nat) (d : Nat) : Bool

Whether rounding in direction takes the magnitude up, given the sign negative, the remainder r and the divisor d of m / d.

machine.Float.toIntegral

def Float.toIntegral (f : FloatFormat) (direction : RoundingDirection) (v : Float) : Float

The value v rounded to an integral value in direction, in the format f (exact; a signed zero keeps its sign).

machine.Float.absolute

def Float.absolute (v : Float) : Float

The absolute value of v (NaN stays NaN).

machine.Float.remainder

def Float.remainder (f : FloatFormat) (x : Float) (y : Float) : Float

The remainder x - trunc(x / y) * y in the format f, with the sign of x (exact): NaN when y is zero or x infinite; x when y is infinite.