TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.Runtime

Static-byte exact conversion runtime #

Nominal families backed by StaticByte.Family decode through SignedRat and use the shared binary conversion policy and numerical contract.

The adapter uses the family descriptor and byte codec, independently of its arithmetic kernels. Typeclass installation lives in Conversion.Instances; correctness equations live in Conversion.Proof.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.decode {F : Type u} [Family F] (value : ExecFloat F) :
Numerics.NumericalValue Numerics.SignedRat

Decode a static-byte value into the signed-rational domain, keeping the sign of zero.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.pack {F : Type u} [Family F] (value : ModelValue (Family.format F)) :
    ExecFloat F

    Pack a rounded binary model into the nominal family's direct byte carrier.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.quantizeFinite {F : Type u} [Family F] (context : ExecFloat.Binary.Conversion.Context) (exact : Numerics.SignedRat) :
      ExecFloat.ConversionOutcome (ExecFloat F)

      Quantize one finite signed rational into the nominal static-byte destination.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.quantizeInfinity {F : Type u} [Family F] (context : ExecFloat.Binary.Conversion.Context) (negative : Bool) :
        ExecFloat.ConversionOutcome (ExecFloat F)

        Apply the explicit infinity policy to a nominal static-byte destination.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.quantizeExceptional {F : Type u} [Family F] (context : ExecFloat.Binary.Conversion.Context) (exceptional : Numerics.ExceptionalValue) :
          ExecFloat.ConversionOutcome (ExecFloat F)

          Apply the explicit exceptional-value policy to a nominal static-byte destination.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.run {F : Type u} [Family F] (context : ExecFloat.Binary.Conversion.Context) :
            Numerics.NumericalValue Numerics.SignedRat → ExecFloat.ConversionOutcome (ExecFloat F)

            Reference conversion for every complete exact observation.

            Instances For
              source
              def FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.spec {F : Type u} [Family F] :
              Numerics.Quantization.Spec ExecFloat.Binary.Conversion.Context (Numerics.NumericalValue Numerics.SignedRat) (ExecFloat.ConversionOutcome (ExecFloat F))

              Shared binary outcome and nearest-value contract, transported through the static-byte codec.

              Instances For
                source
                @[instance_reducible]
                instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.exactDecoder {F : Type u} [Family F] :
                ExecFloat.ExactDecoder (ExecFloat F) Numerics.SignedRat

                Every nominal static-byte binary source decodes exactly through SignedRat.