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 legacy m * 2^e spelling is accepted too. ASCII edge whitespace is ignored. Finite conversion rounds once and reports the binary exception policy, including tininess after rounding, and the ternary value of that rounding. Syntax errors are 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. A valid written payload keeps its sign and signaling state without raising 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.

@[instance_reducible]

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

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

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✝¹)

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

@[instance_reducible]

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

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.convertDecimalTextExact (fmt : FloatFormat) (mode : IEEERoundingMode) (exact : Numerics.DecimalText.Decimal) : IEEEOutcome fmt

One exact decimal-to-binary rounding, paired with the shared binary status and ternary calculations.

This is the reference conversion. It forms the exact rational significand * 10^exponent, so its cost grows with the written exponent. convertDecimalText computes the same outcome after clamping the exponent with clampDecimalExponent.

def FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicLeadingExponent (value : Numerics.Dyadic) : ℤ

The binary leading exponent log2 significand + exponent of a dyadic.

def FloatLib.Floats.Formats.BinaryInterchange.Model.decimalSaturationHigh (fmt : FloatFormat) : ℤ

A binary leading exponent at or above which every rational rounds to the overflow result.

It exceeds the exponent tests of each rounder and the leading exponents of the overflow thresholds used by the status classifier, so both value and status are those of overflow.

def FloatLib.Floats.Formats.BinaryInterchange.Model.decimalSaturationLow (fmt : FloatFormat) : ℤ

A binary leading exponent at or below which every positive rational rounds to the same result.

It lies below each rounder's zero and least-subnormal cutoffs, below the least subnormal exponent, and below every threshold used by the status classifier, so the rounded value and its flags do not depend on the exact magnitude.

def FloatLib.Floats.Formats.BinaryInterchange.Model.clampDecimalExponent (fmt : FloatFormat) (exact : Numerics.DecimalText.Decimal) : Numerics.DecimalText.Decimal

Clamp a decimal exponent to a range where binary conversion is cheap and gives the same result.

A zero significand gets exponent zero. Otherwise the exponent is kept between a lower bound, where the magnitude is below every underflow threshold, and an upper bound, where it is above every overflow threshold. convertDecimalText_eq_exact proves that the clamp never changes the result.

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 and ternary calculations.

An exponent beyond the decimal range of the format is first clamped by clampDecimalExponent, so inputs such as 1e99999999999 finish at once. Exponents inside that range skip the clamp, which would cost more than the conversion itself. The outcome, ternary value included, equals convertDecimalTextExact for every input.

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 and ternary value.

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.

A NaN result has the ternary value .eq.

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 errors.

An infinity is delivered only by a format that has it, so its ternary value is .eq.

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

The value of convertText, with the same errors (Internal.Value.convertText_eq_map).

Decimal and dyadic text inline their converter and keep only its value, so finite numeric value parsing runs no rounding classifier. An infinity is delivered directly, and a NaN keeps the value of convertNaNText, which builds a constant outcome.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Value.convertText_eq_map (fmt : FloatFormat) (mode : IEEERoundingMode) (value : TextValue) : convertText fmt mode value = Except.map (fun (x : IEEEOutcome fmt) => x.value) (Model.convertText fmt mode value)

Value conversion is the value of the complete conversion, with the same 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. Exponents far outside the format's range are clamped first, which leaves the outcome unchanged, so no input length or exponent limit is needed for termination. The caller-facing entrypoint is Model.parse in BoundedParsing.