Decimal character conversion

Finite text uses the shared exact decimal scanner. The coefficient and quantum are kept separately until one destination rounding, with the written quantum as the preferred exponent. Exact output uses coefficient/exponent notation: 120e-2 and 12e-1 have equal values but preserve different representations.

This binding accepts ASCII decimal syntax without whitespace, and case-insensitive Inf, Infinity, NaN, and sNaN, with an optional sign. NaN names may have decimal payload digits. Output preserves NaN sign, signaling state, and payload; reading an sNaN spelling creates a signaling NaN without raising invalid. Malformed text or an unrepresentable NaN payload produces positive quiet NaN with payload zero and the invalid flag. Finite conversion uses all five rounding modes and the projection layer's tininess-before-rounding policy.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Formatting.parseSpecial (negative : Bool) (characters : List Char) : Option Datum

Interpret the shared special spellings as decimal datums.

def FloatLib.Floats.Formats.DecimalInterchange.Formatting.readCharacters (characters : List Char) : Option Datum

Parse an unbounded decimal datum, before applying a destination format.

def FloatLib.Floats.Formats.DecimalInterchange.Formatting.read (text : String) : Option Datum

Exact character decoding, including the written quantum and the sign of zero.

def FloatLib.Floats.Formats.DecimalInterchange.Formatting.invalidText : Outcome

The default result for a syntax error or an oversized diagnostic payload.

def FloatLib.Floats.Formats.DecimalInterchange.Formatting.convert (f : Format) (mode : RoundingMode) : Datum → Outcome

Round a decoded datum into a destination format. Special spellings do not perform arithmetic.

def FloatLib.Floats.Formats.DecimalInterchange.Formatting.parse (f : Format) (mode : RoundingMode) (text : String) : Outcome

Convert a complete string, reporting IEEE status flags for finite rounding and invalid text.

def FloatLib.Floats.Formats.DecimalInterchange.Formatting.characters : Datum → List Char

An exact spelling preserves every component of a datum, including zero's quantum.

def FloatLib.Floats.Formats.DecimalInterchange.Formatting.formatExact (value : Datum) : String

Exact coefficient/quantum output; no rounding or floating-point exceptions occur.