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