TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.IR.Binary

Mixed binary precision #

The shared interpreter can execute each numerical node at its declared FloatLib precision. Casts decode the source's exact interchange word and round in the destination format. Neither constants nor conversions pass through binary64.

This is CPU software execution of the IR, not a reproduction of XLA or LibTorch kernel schedules. In particular, reduction order belongs to the IR semantics. Elementary functions use the approximations supplied by FloatLib's Context. Pointwise operators use the dictionary's Context.pointwise entries; FloatLib has no error function, so erf and the exact GELU are reported as unsupported.

source
@[reducible, inline]
abbrev NN.IR.Binary.Scalar (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) :
Type

FloatLib's configured representation for the complete validated format descriptor.

Instances For
    source
    def NN.IR.Binary.scalar :
    DType → Type

    Unsupported descriptors have no values in this interpreter.

    Instances For
      source
      def NN.IR.Binary.cast (source target : DType) (rounding : FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode) (value : scalar source) :
      Except String (scalar target × FloatLib.Floats.ExecFloat.ConversionStatus)

      FloatLib's exact-source binary conversion, retaining its IEEE exception flags.

      Instances For
        source
        def NN.IR.Binary.tensor (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) (shape : Spec.Shape) (words : Array ℕ) :
        Except String (TorchLean.Tensor (Scalar format) shape)

        Load a shaped binary tensor from complete words, rejecting truncation or padding.

        Instances For
          source
          def NN.IR.Interpreter.binary :
          Interpreter

          Execute numerical nodes using configurable FloatLib binary arithmetic on CPU.

          Instances For
            source
            def NN.IR.Interpreter.Payload.binary (constants : ℕ → Option Interpreter.binary.Value := fun (x : ℕ) => none) :
            Interpreter.binary.Payload

            Constant-only payload for numerical primitives; other parameter stores remain explicit.

            Instances For
              source
              def NN.IR.Interpreter.Value.binary (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) (shape : Spec.Shape) (words : Array ℕ) :
              Except String Interpreter.binary.Value

              Load exact interchange words, rejecting truncation and shape mismatches.

              Instances For
                source
                def NN.IR.Interpreter.Value.words (value : Interpreter.binary.Value) :
                Except String (Array ℕ)

                Exact interchange words of a binary tensor, including signed zeros and NaN payloads.

                Instances For