P3109 queries and adjacent values

Format queries expose the descriptor and its distinguished encoded values. Classification and adjacent-value operations inspect codes directly, so their cost does not depend on the decoded exponent. maxSubnormalOf returns NaN at precision one. nextGreaterThan maps positive infinity to NaN, and nextLessThan maps negative infinity to NaN: these are deliberately different from IEEE nextUp and nextDown.

Reference: P3109 unapproved interim report 4.0.3, revision 34f5964, §§4.13–4.16.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.bitwidthOf (format : Format) : ℕ

Total encoded width, as queried by §4.14.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.precisionOf (format : Format) : ℕ

Precision including the implicit leading bit.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.signednessOf (format : Format) : Signedness

Whether negative finite values are represented.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.domainOf (format : Format) : Domain

Whether infinities are represented.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.exponentBitwidthOf (format : Format) : ℕ

Width of the biased exponent.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.trailingSignificandBitwidthOf (format : Format) : ℕ

Width of the trailing significand field.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.exponentBiasOf (format : Format) : ℕ

Bias subtracted from nonzero encoded exponents.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.maxFiniteOf (format : Format) : ExecFloat.P3109 format

Largest finite value as a value of the queried format.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.minFiniteOf (format : Format) : ExecFloat.P3109 format

Smallest finite value; unsigned formats return zero.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.minPositiveOf (format : Format) : ExecFloat.P3109 format

Least strictly positive value.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.maxSubnormalOf (format : Format) : ExecFloat.P3109 format

Largest positive subnormal, or NaN when precision one leaves no subnormal values.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.minNormalOf (format : Format) : ExecFloat.P3109 format

Least positive normal value.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.isZero {format : Formats.P3109.Format} (value : P3109 format) : Bool

The format's unique zero has code zero.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.isNaN {format : Formats.P3109.Format} (value : P3109 format) : Bool

Test the unique NaN code.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.isInfinite {format : Formats.P3109.Format} (value : P3109 format) : Bool

Test either infinity, respecting signedness and the finite/extended domain.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.isFinite {format : Formats.P3109.Format} (value : P3109 format) : Bool

Finite excludes NaN and either infinity.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.isSignMinus {format : Formats.P3109.Format} (value : P3109 format) : Bool

Negative finite values and negative infinity have negative sign; NaN and zero do not.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.magnitudeBits {format : Formats.P3109.Format} (value : P3109 format) : ℕ

Unsigned magnitude code, removing the sign partition in signed formats.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.isOne {format : Formats.P3109.Format} (value : P3109 format) : Bool

Test exact numerical equality to one without constructing a large rational.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.isNormal {format : Formats.P3109.Format} (value : P3109 format) : Bool

Normal values are finite and have a nonzero biased exponent in their magnitude code.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.isSubnormal {format : Formats.P3109.Format} (value : P3109 format) : Bool

Nonzero finite values below the normal range.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.nextGreaterThan {format : Formats.P3109.Format} (value : P3109 format) : P3109 format

Least greater value, or NaN when there is no greater datum.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.nextLessThan {format : Formats.P3109.Format} (value : P3109 format) : P3109 format

Greatest lesser value, or NaN when there is no lesser datum.