TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Configured.Value.Runtime

Runtime interface for configured posit values #

Configured posit values support packing, exact decoding, classification, and raw-word conversion independently of storage choice.

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

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

This boundary does not expose whether the carrier is a byte, machine word, packed pair, or wide bit vector.

Instances For
    source
    @[inline]
    def FloatLib.Floats.ExecFloat.Posit.ofModel {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : Formats.Posit.Model format) :
    ExecFloat (Formats.Posit.Configured.Family format code plan)

    Pack an exact-width posit model into the statically selected runtime carrier.

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

      Construct a configured posit from its complete unsigned word.

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

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

        Read the complete posit word as an unsigned natural number.

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

          Decode the tapered fields, retaining zero and NaR as separate constructors.

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

            Complete rational denotation; NaR remains an exceptional Not-a-Real observation.

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

              Exact rational value of an ordinary configured posit, or none exactly for NaR.

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

                Whether the configured value is the unique zero encoding.

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

                  Whether the configured value is the unique Not-a-Real encoding.

                  Instances For