TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Conversion.Runtime

Configured binary-interchange conversion runtime #

This adapter supplies the configured carrier's ofModel bridge to the representation-independent binary conversion policy. Exact rounding happens before packing, so storage and backend selection cannot change conversion semantics. The exact domain is SignedRat, which carries the sign of zero to the quantizer; the destination's encoding policy determines whether that sign is retained.

source
@[inline]
def FloatLib.Floats.ExecFloat.Binary.Conversion.configuredPack {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Formats.BinaryInterchange.Model format) :
ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)

Pack a rounded binary model through the configured destination codec.

Instances For
    source
    @[inline]
    def FloatLib.Floats.ExecFloat.Binary.Conversion.quantizeFinite {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (context : Context) (exact : Numerics.SignedRat) :
    ConversionOutcome (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))

    Quantize one finite signed rational into the configured binary destination.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.ExecFloat.Binary.Conversion.quantizeExceptional {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (context : Context) (exceptional : Numerics.ExceptionalValue) :
      ConversionOutcome (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))

      Apply the explicit exceptional-value policy to a configured binary destination.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.ExecFloat.Binary.Conversion.quantizeInfinity {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (context : Context) (negative : Bool) :
        ConversionOutcome (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))

        Apply the explicit infinity policy to a configured binary destination.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.ExecFloat.Binary.Conversion.run {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (context : Context) :
          Numerics.NumericalValue Numerics.SignedRat → ConversionOutcome (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))

          Reference conversion for every complete exact observation.

          Instances For
            source
            def FloatLib.Floats.ExecFloat.Binary.Conversion.spec {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] :
            Numerics.Quantization.Spec Context (Numerics.NumericalValue Numerics.SignedRat) (ConversionOutcome (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)))

            Complete configured outcome with the default IEEE nearest-value contract.

            Binary.Conversion.specWith supplies the independent finite-denotation clause and retains the complete word, status, and explicit policy behavior.

            Instances For
              source
              @[instance_reducible]
              instance FloatLib.Floats.ExecFloat.Binary.Conversion.exactDecoder {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] :
              ExactDecoder (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) Numerics.SignedRat

              Configured binary decoding selects the signed-rational exact domain, keeping signed zero.