TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.ExecFloat.Backends.Word.Full.Division.Runtime

Native binary64 division runtime #

The normal-result binary64 path performs restoring division on UInt64. Inputs outside that kernel fall back to the exact generic finite implementation. Division.Proof has the proofs.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.divNormalWord? (xBits yBits : UInt64) :
Option UInt64

Divide two binary64 storage words on the common path whose rounded result is normal, returning the packed result word. Carriers that store binary64 as a UInt64 call it on their words, so a normal quotient never becomes an exact-width model value.

It returns none for zeros, subnormal or overflowing results, and exceptional encodings. Declined finite cases go to the generic finite kernel, and the dispatcher sends exceptional operands to Spec.divSpecial.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.divNormal? (x y : Value) :
    Option Value

    divNormalWord? as a model value.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.divFinite? (x y : Value) :
      Option Value

      Finite binary64 division through the native normal-result divider, falling back to the generic component kernel divFiniteComponents?.

      Instances For