Exact decimal character conversion

The reusable decimal carrier denotes an integer times an integral power of ten. Parsing accepts ASCII decimal integers, fractions, and e/E exponents with optional signs. Each successful parse denotes an exact rational, without host floating-point conversion.

Every dyadic has a terminating decimal expansion: m / 2^k = (m * 5^k) / 10^k. The formatter uses that identity, with decimal exponent notation for fractional values. Output size and exact-integer work grow with the magnitude of the binary exponent.

structure FloatLib.Numerics.DecimalText.Decimal : Type

An exact signed decimal significand and integral decimal scale.

• negative : Bool

  Sign of the decimal significand; signed zeros denote the same rational.

• significand : ℕ

  Magnitude of the integer significand.

• exponent : ℤ

  Power of ten multiplying the significand.

@[instance_reducible]

instance FloatLib.Numerics.DecimalText.instDecidableEqDecimal : DecidableEq Decimal

def FloatLib.Numerics.DecimalText.instDecidableEqDecimal.decEq (x✝ x✝¹ : Decimal) : Decidable (x✝ = x✝¹)

def FloatLib.Numerics.DecimalText.instReprDecimal.repr : Decimal → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Numerics.DecimalText.instReprDecimal : Repr Decimal

def FloatLib.Numerics.DecimalText.Decimal.toRat (value : Decimal) : ℚ

Exact rational meaning of a decimal record.

def FloatLib.Numerics.DecimalText.digitValue? (character : Char) : Option ℕ

Recognize precisely the ten ASCII decimal digits.

def FloatLib.Numerics.DecimalText.splitSign : List Char → Bool × List Char

Remove at most one leading sign; an absent sign is positive.

def FloatLib.Numerics.DecimalText.parseInteger (characters : List Char) : Option ℤ

Read a signed decimal integer, requiring at least one digit and complete consumption.

def FloatLib.Numerics.DecimalText.parseExponent : List Char → Option ℤ

Read an optional decimal exponent, rejecting incomplete or trailing input.

def FloatLib.Numerics.DecimalText.parseCharacters (characters : List Char) : Option Decimal

Parse decimal characters with an optional leading sign.

def FloatLib.Numerics.DecimalText.parse (text : String) : Option ℚ

Parse an exact decimal rational. Whitespace and nondecimal notation are rejected.

def FloatLib.Numerics.DecimalText.integerDigits : ℤ → List Char

Print an integral exponent with an explicit minus sign only when negative.

def FloatLib.Numerics.DecimalText.Decimal.characters (value : Decimal) : List Char

Print a decimal record as a decimal significand with an optional e exponent.

def FloatLib.Numerics.DecimalText.Decimal.format (value : Decimal) : String

Character-string representation of the exact decimal record.

def FloatLib.Numerics.DecimalText.ofDyadic (value : Dyadic) : Decimal

Convert a dyadic to an equal decimal using powers of five for negative binary exponents.

def FloatLib.Numerics.DecimalText.formatDyadic (value : Dyadic) : String

Exact decimal formatting of a dyadic; every finite input has decimal output.