TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Configured.Conversion.Integer.Unsigned.Runtime

Configured unsigned integer conversions #

These adapters apply the Posit Standard (2022) §6.4 word-sentinel policy through any lawful configured codec. Integer width is independent of posit width. The shared model kernel handles all numerical rounding and range decisions.

source
@[inline]
def FloatLib.Floats.ExecFloat.Posit.ofUnsigned {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] {width : ℕ} (value : BitVec width) (hwidth : 0 < width := by decide) :
ExecFloat (Formats.Posit.Configured.Family format code plan)

Convert unsigned bits to posit, reserving the MSB-only input word for NaR.

Instances For
    source
    @[inline]
    def FloatLib.Floats.ExecFloat.Posit.toUnsigned {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (width : ℕ) (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hwidth : 0 < width := by decide) :
    BitVec width

    Convert posit to unsigned bits, with nearest-even rounding before the range check.

    Instances For