TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Value.Core

Representation interface for configured binary values #

A configured binary format chooses its storage plan statically, but numerical programs should not need separate APIs for byte, word, fixed-limb, and wide carriers. This module exposes one storage-independent boundary for packing, exact decoding, classification, and special values.

Conversions through the logical Model are explicit and exact. The module does not register arithmetic backends, so representation and conversion code can use configured values without importing the operation planner or native-width dispatch instances.

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

Decode the statically selected runtime carrier into the exact-width binary proof model.

This boundary does not expose whether the carrier is a byte, machine word, or wide model.

Instances For
    source
    @[inline]
    def FloatLib.Floats.ExecFloat.Binary.ofModel {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 an exact-width binary model into the statically selected runtime carrier.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.ExecFloat.Binary.ofNatBits {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (bits : ℕ) :
      ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)

      Construct a configured binary value from its complete unsigned interchange word.

      Inputs outside the configured width are reduced modulo 2 ^ format.bitWidth, matching Model.ofNatBits.

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

        Read the complete configured binary interchange word as an unsigned natural number.

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

          Decode the complete mathematical value, retaining signed zero and NaN metadata.

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

            Decode into the exact signed-rational semantic domain used by binary conversion.

            Finite values become exact rationals together with their sign bit, so a negative zero decodes to SignedRat.negZero rather than to 0. Infinities retain their sign, and NaNs carry their complete encoded word as payload. Use exactValue when signaling-NaN metadata is required, or toRat? when only the rational value of a finite number matters.

            Instances For
              source
              @[inline]
              def FloatLib.Floats.ExecFloat.Binary.toRat? {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
              Option ℚ

              Exact rational value of a finite configured binary number, or none for NaN and infinity.

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

                Whether the stored sign bit is set.

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

                  Whether the value is a NaN under its configured encoding policy.

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

                    Whether the value is a quiet NaN under its configured encoding policy.

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

                      Whether the value is a signaling NaN under its configured encoding policy.

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

                        Whether the value is an infinity; finite encodings always return false.

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

                          Whether the value denotes a finite number under its configured encoding policy.

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

                            Whether the value is zero under its configured encoding policy.

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

                              Whether the value is a finite subnormal.

                              Instances For
                                source
                                @[inline]
                                def FloatLib.Floats.ExecFloat.Binary.zero {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (sign : Bool) :
                                ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)

                                Construct zero with the requested sign.

                                Encodings with one unsigned zero canonicalize a requested negative zero to positive zero.

                                Instances For
                                  source
                                  @[inline]
                                  def FloatLib.Floats.ExecFloat.Binary.infinity? {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (sign : Bool) :
                                  Option (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))

                                  Construct signed infinity when the configured encoding represents it.

                                  IEEE encodings return some; finite-only, maximum-NaN, and FNUZ encodings return none.

                                  Instances For
                                    source
                                    @[inline]
                                    def FloatLib.Floats.ExecFloat.Binary.infinity {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (sign : Bool) (_supportsInfinity : format.supportsInfinity = true := by decide) :
                                    ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)

                                    Construct signed infinity when the configured encoding is statically known to support it.

                                    Calling this constructor for a finite encoding fails during elaboration.

                                    Instances For
                                      source
                                      @[inline]
                                      def FloatLib.Floats.ExecFloat.Binary.canonicalNaN? {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] :
                                      Option (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))

                                      Construct the encoding's canonical quiet NaN when it has a NaN representation.

                                      IEEE, maximum-NaN, and FNUZ encodings return some; fully finite encodings return none.

                                      Instances For
                                        source
                                        @[inline]
                                        def FloatLib.Floats.ExecFloat.Binary.canonicalNaN {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (_supportsNaN : format.supportsNaN = true := by decide) :
                                        ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)

                                        Construct the canonical quiet NaN when support is statically known.

                                        Fully finite encodings reject this constructor during elaboration.

                                        Instances For
                                          source
                                          @[inline]
                                          def FloatLib.Floats.ExecFloat.Binary.maxFinite {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (sign : Bool) :
                                          ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)

                                          Construct the finite value of greatest magnitude with the requested sign.

                                          Instances For