TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

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

Native-word division for binary32 #

Finite division uses native-word significands and quotient arithmetic, with Int exponents and natural-number coordinates for the final packing. Finite division by zero is handled here. divFiniteWord? returns none for NaN or infinity operands, and the caller applies their policy. Division.Proof has the proofs.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.roundRatScaledWord (sign : Bool) (num den : UInt64) (exponent : ℤ) :
UInt32

Round the signed magnitude (num / den) * 2^exponent to binary32 with native quotient arithmetic and an Int exponent.

Callers supply significands below 2^24, and the proof module shows that every shift and division stays within UInt64.

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

    Finite binary32 division with one-word significands and the native-word rounder.

    It returns none when an operand is a NaN or infinity.

    Instances For