Configured binary-interchange conversion instances #
Configured binary-interchange destinations support signed-rational quantization with explicit finite, infinity, and exceptional policies.
@[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.
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 = 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.