Binary external character conversion

Decimal integers, fractions and e/E exponents use the shared exact scanner. Hexadecimal input follows IEEE 754 §5.12.3, including its mandatory p/P exponent. The older m * 2^e spelling remains accepted. ASCII edge whitespace is ignored. Finite conversion rounds once and reports the existing binary exception policy, including tininess after rounding. Syntax errors remain explicit ParseErrors.

Inf/Infinity/NaN/sNaN accept either case and an optional sign. A NaN's decimal suffix denotes its complete fraction field, including the quiet bit. Zero or an absent suffix chooses a default payload. Valid explicit payloads preserve sign and signaling state without invalid. A descriptor unable to encode a signaling NaN may quiet the default sNaN and raise invalid.

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

Why exact character input could not produce a value in the requested format.

• emptyInput : ParseError

  The input contains no non-whitespace characters.

• invalidSyntax (input : String) : ParseError

  The input is not a supported decimal, radix-two, infinity, or NaN spelling.

• unsupportedInfinity (negative : Bool) : ParseError

  The input requests an infinity from a finite-only encoding.

• unsupportedNaN : ParseError

  The input requests a NaN from an encoding with no NaN representation.

• inputTooLong (actual maximum : ℕ) : ParseError

  The input exceeds the caller's byte limit before character scanning.

• exponentTooLarge (actual maximum : ℕ) : ParseError

  The adjusted decimal or binary exponent exceeds the caller's magnitude limit.

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

@[instance_reducible]

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

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

@[instance_reducible]

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

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

Concise human-readable explanation of a character-input failure.

@[instance_reducible]

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

inductive FloatLib.Floats.Formats.BinaryInterchange.Model.TextValue : Type

Unrounded external text, retaining a decimal scale or binary scale and signed zero.

• decimal (value : Numerics.DecimalText.Decimal) : TextValue

  An exact decimal coefficient and written decimal exponent.

• dyadic (value : Numerics.Dyadic) : TextValue

  An exact dyadic from hexadecimal or legacy radix-two syntax.

• infinity (negative : Bool) : TextValue

  A signed infinity.

• nan (negative signaling : Bool) (payload : ℕ) : TextValue

  A signed NaN with signaling state and complete-fraction diagnostic suffix.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqTextValue : DecidableEq TextValue

def FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqTextValue.decEq (x✝ x✝¹ : TextValue) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instReprTextValue : Repr TextValue

def FloatLib.Floats.Formats.BinaryInterchange.Model.instReprTextValue.repr : TextValue → ℕ → Std.Format

def FloatLib.Floats.Formats.BinaryInterchange.Model.readLegacyDyadic (text : String) : Option Numerics.Dyadic

Decode the legacy exact radix-two spelling, using the common integer scanner.

def FloatLib.Floats.Formats.BinaryInterchange.Model.readText (text : String) : Option TextValue

Decode one complete trimmed string before choosing a destination format or rounding.

def FloatLib.Floats.Formats.BinaryInterchange.Model.convertDecimalText (fmt : FloatFormat) (mode : IEEERoundingMode) (exact : Numerics.DecimalText.Decimal) : IEEEOutcome fmt

One exact decimal-to-binary rounding, paired with the shared binary status calculation.

def FloatLib.Floats.Formats.BinaryInterchange.Model.convertDyadicText (fmt : FloatFormat) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) : IEEEOutcome fmt

One hexadecimal or legacy dyadic conversion with binary rounding status.

def FloatLib.Floats.Formats.BinaryInterchange.Model.convertNaNText (fmt : FloatFormat) (negative signaling : Bool) (payload : ℕ) : Except ParseError (IEEEOutcome fmt)

Interpret a NaN diagnostic according to the descriptor, rejecting unrepresentable payloads.

def FloatLib.Floats.Formats.BinaryInterchange.Model.convertText (fmt : FloatFormat) (mode : IEEERoundingMode) : TextValue → Except ParseError (IEEEOutcome fmt)

Convert a decoded text value. Unsupported specials and invalid diagnostics are explicit errors.

def FloatLib.Floats.Formats.BinaryInterchange.Model.TextParser.run (fmt : FloatFormat) (mode : IEEERoundingMode) (input : String) : Except ParseError (IEEEOutcome fmt)

Implementation core for character input, reporting all five IEEE exceptions. Finite input is converted from its complete exact value without resource limits. The caller-facing entrypoint is Model.parse in BoundedParsing.