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 final packing. Finite division by zero is handled here; divFiniteImpl? returns none for NaN or infinity operands so the caller can apply their policy. Correctness lives in Division.Proof.

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; the proof module establishes that every shift and division stays within UInt64.

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

    Fast finite binary32 division using one-word significands and the native-word rounder.

    none means at least one operand is a NaN or infinity; the caller applies the generic policy.

    Instances For