Posit decimal input

Decimal integers, fractions, and decimal exponents denote exact rationals, rounded once according to Posit Standard (2022), §4.1. NaR names the unique exceptional value. Empty or malformed input returns an explicit error. The decimal grammar does not accept whitespace or radix-two notation.

Together with decimal display, this implements the value-preserving decimal character conversion described in §6.3. The character and posit round-trip proofs are in Formatting.Proof.

References

• Posit Working Group, Standard for Posit Arithmetic (2022), March 2, 2022, §§4.1, 6.3, https://posithub.org/docs/posit_standard-2.pdf.

inductive FloatLib.Floats.Formats.Posit.Model.ParseError : Type

A decimal-input failure, distinct from the explicit NaR spelling.

• emptyInput : ParseError

  The supplied string has no characters.

• invalidSyntax (input : String) : ParseError

  The string is neither decimal syntax nor NaR.

@[instance_reducible]

instance FloatLib.Floats.Formats.Posit.Model.instDecidableEqParseError : DecidableEq ParseError

def FloatLib.Floats.Formats.Posit.Model.instDecidableEqParseError.decEq (x✝ x✝¹ : ParseError) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.Posit.Model.instReprParseError : Repr ParseError

def FloatLib.Floats.Formats.Posit.Model.instReprParseError.repr : ParseError → ℕ → Std.Format

def FloatLib.Floats.Formats.Posit.Model.ParseError.message : ParseError → String

Human-readable explanation of a decimal-input failure.

@[instance_reducible]

instance FloatLib.Floats.Formats.Posit.Model.instToStringParseError : ToString ParseError

def FloatLib.Floats.Formats.Posit.Model.decimalSaturationExponent (format : Format) : ℤ

A decimal exponent at which every nonzero significand already reaches maxPos.

It is one more than the bit length of the numerator of maxPos, so ten to this power exceeds maxPos.

def FloatLib.Floats.Formats.Posit.Model.decimalVanishingExponent (format : Format) (significand : ℕ) : ℤ

A decimal exponent at which the given significand, scaled by ten to this power, lies below minPos.

The bound adds the bit lengths of the significand and of the denominator of minPos.

def FloatLib.Floats.Formats.Posit.Model.clampDecimal (format : Format) (value : Numerics.DecimalText.Decimal) : Numerics.DecimalText.Decimal

Move a decimal exponent into the range where it can still affect posit rounding.

Posits saturate: every positive value at or above maxPos rounds to maxPos, and every positive value below minPos rounds to minPos. Exponents beyond these points are replaced by the nearest endpoint, and the exponent of a zero significand becomes zero. roundRat_clampDecimal proves that rounding the clamped decimal gives the same posit, so the parser never builds a huge power of ten.

def FloatLib.Floats.Formats.Posit.Model.parse (format : Format) (input : String) : Except ParseError (Model format)

Read a decimal rational and round it once to the requested posit width.

Accepted finite syntax includes 12, -0.125, .5, 1., and +25e-3. Only NaR requests the exceptional value; invalid syntax never silently becomes zero or NaR. Written exponents far outside the posit range are clamped first (see clampDecimal), which leaves the rounded result unchanged and keeps inputs such as 1e1000000000 cheap.