Character input for configured binary values

Configured binary values use the descriptor model's exact character parser. A successful parse differs from the model's only in storage representation, so the decoded numerical value is the same.

def FloatLib.Floats.ExecFloat.Binary.parse {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (input : String) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode := Formats.BinaryInterchange.Model.IEEERoundingMode.nearest) (limits : Option Formats.BinaryInterchange.Model.ParseLimits := none) (status : Bool := false) : Except Formats.BinaryInterchange.Model.ParseError (match status with | true => IEEEOutcome | false => ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))

Parse decimal, hexadecimal, dyadic, or special text with nearest-even rounding by default.

Set mode to choose another direction. With limits := some bounds, bounds.maxBytes bounds the original UTF-8 input and bounds.maxExponent bounds its adjusted exponent before exact conversion, and some {} selects the default bounds. Set status := true to return the value together with all five IEEE exception flags and the ternary value. Malformed or oversized input returns Model.ParseError.

theorem FloatLib.Floats.ExecFloat.Binary.map_toModel_parse {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (input : String) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) (limits : Option Formats.BinaryInterchange.Model.ParseLimits) : Except.map toModel (parse input mode limits) = Formats.BinaryInterchange.Model.parse format input mode limits

Decoding a parsed configured value gives the descriptor-model result.

theorem FloatLib.Floats.ExecFloat.Binary.map_toModel_parse_status {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (input : String) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) (limits : Option Formats.BinaryInterchange.Model.ParseLimits) : Except.map IEEEOutcome.toModel (parse input mode limits true) = Formats.BinaryInterchange.Model.parse format input mode limits true

Requesting status preserves every model bit, IEEE flag, and the ternary value across the storage conversion.