numbers

python.Number

data Number

What a value is as a number: an int (a bool as 0 or 1), a float, or not a number.

python.Number.of

def Number.of (v : Value) : Number

The value v as a number.

python.Number.format

def Number.format : FloatFormat

binary64, Python’s float.

python.Number.isInfinite

def Number.isInfinite (x : Float) : Bool

Whether the float x is infinite.

python.Number.toFloat

def Number.toFloat (n : Int) : Option Float

The int n as a float, rounded; none when it is too large (Python raises OverflowError: “int too large to convert to float”).

python.Number.floorDivide

def Number.floorDivide (a : Int) (b : Int) : Int

a // b on ints (b not zero): the quotient rounded toward negative infinity.

python.Number.modulo

def Number.modulo (a : Int) (b : Int) : Int

a % b on ints (b not zero): a - b * (a // b), with the divisor’s sign.

python.Number.isNegative

def Number.isNegative (x : Float) : Bool

Whether the float x is negative (NaN counts as positive).

python.Number.floatModulo

def Number.floatModulo (x : Float) (y : Float) : Float

The floats’ x % y (CPython’s float_divmod): fmod, moved by the divisor y when the signs differ; a zero remainder has the divisor’s sign.

python.Number.floatFloorDivide

def Number.floatFloorDivide (x : Float) (y : Float) : Float

A float’s // (CPython’s float_divmod): (x - fmod) / y, one less when the signs differ, floored, and one more when the floor is more than half below; a zero quotient has the sign of x / y.

python.Rational

record Rational

A rational number: its sign, numerator and denominator (not zero).

python.Rational.ofInt

def Rational.ofInt (n : Int) : Rational

The int n as a rational.

python.Rational.ofFinite

def Rational.ofFinite (negative : Bool) (m : Nat) (e : Int) : Rational

The finite float with the mantissa m and the exponent e (m * 2^e), negative or not, as a rational.

python.Rational.sign

def Rational.sign (a : Rational) : Int

The sign of a rational: -1, 0 or 1.

python.Rational.compareNat

def Rational.compareNat (x : Nat) (y : Nat) : Int

Comparing the naturals x and y: -1, 0 or 1.

python.Rational.compare

def Rational.compare (a : Rational) (b : Rational) : Int

Comparing the rationals a and b: -1, 0 or 1 (the signs first, then the magnitudes cross-multiplied).

python.Number.compareIntFloat

def Number.compareIntFloat (n : Int) (y : Float) : Option Int

Comparing the int n with the float y exactly: -1, 0 or 1; none when the float is NaN.

python.Number.compareFloats

def Number.compareFloats (x : Float) (y : Float) : Option Int

Comparing the floats x and y: -1, 0 or 1; none when either is NaN.

python.Number.compare

def Number.compare (a : Number) (b : Number) : Option Int

Comparing the numbers a and b by their exact values: -1, 0 or 1; none when a NaN takes part or one is not a number.

python.Number.magnitude

def Number.magnitude (n : Int) : Nat

The magnitude of the int n.

python.Number.widthFor

def Number.widthFor (a : Int) (b : Int) : Nat

A two’s complement width that holds both ints a and b with room for the sign.

python.Number.signedAt

def Number.signedAt (width : Nat) (bits : Nat) : Int

The unsigned result bits at the width read as the signed int it is.

python.Number.bitAnd

def Number.bitAnd (a : Int) (b : Int) : Int

a & b on ints (infinite two’s complement).

python.Number.bitOr

def Number.bitOr (a : Int) (b : Int) : Int

a | b on ints (infinite two’s complement).

python.Number.bitXor

def Number.bitXor (a : Int) (b : Int) : Int

a ^ b on ints (infinite two’s complement).

python.Number.invert

def Number.invert (a : Int) : Int

~a on an int: -a - 1.

python.Number.shiftLeft

def Number.shiftLeft (a : Int) (k : Nat) : Int

a << k (k not negative).

python.Number.shiftRight

def Number.shiftRight (a : Int) (k : Nat) : Int

a >> k (k not negative): rounded toward negative infinity.

python.Number.truncate

def Number.truncate (x : Float) : Option Int

A float truncated toward zero as an int (int(x)): none for infinity or NaN (Python raises OverflowError for infinity and ValueError for NaN).

python.Number.index

def Number.index (v : Value) : Option Int

The int the value v stands for as an index (operator.index): an int, or a bool as 0 or 1.

python.Number.hashModulus

def Number.hashModulus : Nat

The modulus of numeric hashes, the prime 2^61 - 1.

python.Number.hashed

def Number.hashed (negative : Bool) (x : Nat) : Int

The hash x with its sign (minus when negative), -1 replaced by -2 (-1 is CPython’s error value).

python.Number.hashInt

def Number.hashInt (n : Int) : Int

hash(n) of an int.

python.Number.hashFloat

def Number.hashFloat (x : Float) : Option Int

hash(x) of a float: none for NaN. A finite x = m * 2^e hashes as m times the inverse of 2^-e modulo the prime, which is 2 to the power (-e mod 61) since 2^61 is 1 there.