Configured binary-interchange conversion instances

Configured binary-interchange destinations support signed-rational quantization with finite, infinity, and exceptional policies, and conversions into them accept all six rounding directions as (mode := ...).

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Binary.Conversion.quantizer {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] : Quantizer (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) Numerics.SignedRat

Every configured binary destination supports policy-aware signed-rational quantization.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Binary.Conversion.defaultQuantizer {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] : DefaultQuantizer (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) Numerics.SignedRat

Context-free conversion uses Context.default.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Binary.Conversion.roundingModes {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} : RoundingModes (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) Formats.BinaryInterchange.Model.IEEERoundingMode

Conversions into a binary destination take an IEEERoundingMode, nearest-even by default.

@[instance_reducible, inline]

instance FloatLib.Floats.ExecFloat.Binary.Conversion.modeContext {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : ModeContext (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) Numerics.SignedRat mode

A conversion's (mode := m) selects Context.withRounding m, and .nearest the canonical Context.default that it equals.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.context_modeContext {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : ModeContext.context = Context.withRounding mode

The context a binary conversion's (mode := m) selects is Context.withRounding m.

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.cast_eq_roundRat_of_decodeTo_eq_finite {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {F : Type u} [Numerics.EncodedFormat F] {SourceExact : Type v} [ExactDecoder (ExecFloat F) SourceExact] [ExactMap SourceExact Numerics.SignedRat] (value : ExecFloat F) (exact : Numerics.SignedRat) (hdecode : ExactDecoder.decodeTo value = Numerics.NumericalValue.finite exact) : value.cast (RoundingModes.default (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))) ModeContext.context = ConversionOutcome.success (ofModel (Formats.BinaryInterchange.Model.roundRat format exact.negative exact.value.num.natAbs exact.value.den)) (finiteStatus Context.default exact.value (Formats.BinaryInterchange.Model.roundRat format exact.negative exact.value.num.natAbs exact.value.den))

A cast whose source decodes to a finite exact value is the canonical nearest-even rounding of that value in the destination format.

The hypothesis names the decoded value, so the theorem applies to any source with an exact decoder and an embedding into SignedRat. For conventional IEEE destinations and finite results, Model.toReal_roundRatScaled_eq_roundAt supplies the corresponding real-number meaning.