TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Parsing

Character input for configured binary values #

Configured binary values use the descriptor model's exact character parser. A successful parse changes only the storage representation; the decoded numerical value is unchanged.

source
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) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode := Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven) (limits : Bool := false) (maxBytes : ℕ := 4096) (maxExponent : ℕ := 10000) (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 rounding to choose another direction. With limits := true, maxBytes bounds the original UTF-8 input and maxExponent bounds its adjusted exponent before exact conversion. Set status := true to return the value together with all five IEEE exception flags. Malformed or oversized input returns Model.ParseError.

Instances For
    source
    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) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) (limits : Bool) (maxBytes maxExponent : ℕ) :
    Except.map toModel (parse input rounding limits maxBytes maxExponent) = Formats.BinaryInterchange.Model.parse format input rounding limits maxBytes maxExponent

    Decoding a parsed configured value recovers exactly the descriptor-model result.

    source
    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) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) (limits : Bool) (maxBytes maxExponent : ℕ) :
    Except.map IEEEOutcome.toModel (parse input rounding limits maxBytes maxExponent true) = Formats.BinaryInterchange.Model.parse format input rounding limits maxBytes maxExponent true

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