TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.P3109.Arithmetic.Instances

Public P3109 arithmetic capabilities #

Every valid P3109 descriptor supplies addition, subtraction, multiplication, division, square root, and fused multiply-add through common ExecFloat dispatch. Each has one exact arithmetic kernel followed by the report projection. The caller's backend planning policy is kept.

Context-free operations use FloatLib's nearest-even, no-saturation projection policy. Other rounding modes, stochastic random words, saturation, and mixed-format destinations are available through the mode, saturation, and target options of ExecFloat.P3109.add and its siblings. These operations neither raise nor synthesize IEEE exception flags.

Literals round once from their exact rational value with the same default policy, and == is numerical equality: NaN compares unequal to every value, itself included.

The rational real-embedding and decoding proofs are in Arithmetic.Proof. The irrational-root refinement and decoding proofs are in Arithmetic.Sqrt.Proof.

source
def FloatLib.Floats.ExecFloat.P3109.Plan.estimate (format : Formats.P3109.Format) (operation : Backend.Operation) :
Backend.Candidate

Planner metadata for the exact arithmetic implementation.

The storage class describes the encoded operand, not an intermediate-size bound. Exact rational arithmetic can allocate integers whose sizes depend on the descriptor's exponent range.

Instances For
    source
    @[instance_reducible, always_inline]
    def FloatLib.Floats.ExecFloat.P3109.Plan.capability {format : Formats.P3109.Format} [Backend.PolicyFor (Codebook.Family format.codebook)] (operation : Backend.Operation) (kernel : OperationSignature (Codebook.Family format.codebook) operation) :
    Capability (Codebook.Family format.codebook) operation

    Package the single exact kernel without changing the caller's planning policy.

    Instances For
      source
      @[instance_reducible]
      instance FloatLib.Floats.ExecFloat.P3109.negInstance {format : Formats.P3109.Format} :
      Neg (P3109 format)

      Report-default negation, including projection of unsigned results.

      source
      @[instance_reducible]
      instance FloatLib.Floats.ExecFloat.P3109.instOfNat {format : Formats.P3109.Format} (value : ℕ) :
      OfNat (P3109 format) value

      A natural literal rounds once, nearest-even with no saturation request.

      source
      @[instance_reducible]
      instance FloatLib.Floats.ExecFloat.P3109.instOfScientific {format : Formats.P3109.Format} :
      OfScientific (P3109 format)

      A decimal or scientific literal rounds once from its exact rational value.

      source
      @[instance_reducible]
      instance FloatLib.Floats.ExecFloat.P3109.comparison {format : Formats.P3109.Format} :
      Comparison (Codebook.Family format.codebook)

      == is numerical equality, so NaN compares unequal to every value, itself included.

      source
      @[instance_reducible, always_inline]
      instance FloatLib.Floats.ExecFloat.P3109.addCapability {format : Formats.P3109.Format} [Backend.PolicyFor (Codebook.Family format.codebook)] :
      Add (Codebook.Family format.codebook)

      Exact addition with one nearest-even report projection.

      source
      @[instance_reducible, always_inline]
      instance FloatLib.Floats.ExecFloat.P3109.subCapability {format : Formats.P3109.Format} [Backend.PolicyFor (Codebook.Family format.codebook)] :
      Sub (Codebook.Family format.codebook)

      Exact subtraction with one nearest-even report projection.

      source
      @[instance_reducible, always_inline]
      instance FloatLib.Floats.ExecFloat.P3109.mulCapability {format : Formats.P3109.Format} [Backend.PolicyFor (Codebook.Family format.codebook)] :
      Mul (Codebook.Family format.codebook)

      Exact multiplication with one nearest-even report projection.

      source
      @[instance_reducible, always_inline]
      instance FloatLib.Floats.ExecFloat.P3109.divCapability {format : Formats.P3109.Format} [Backend.PolicyFor (Codebook.Family format.codebook)] :
      Div (Codebook.Family format.codebook)

      Exact division with the report's NaN result for every zero denominator.

      source
      @[instance_reducible, always_inline]
      instance FloatLib.Floats.ExecFloat.P3109.sqrtCapability {format : Formats.P3109.Format} [Backend.PolicyFor (Codebook.Family format.codebook)] :
      Sqrt (Codebook.Family format.codebook)

      Square root rounded by exact comparisons with the irrational result.

      source
      @[instance_reducible, always_inline]
      instance FloatLib.Floats.ExecFloat.P3109.fmaCapability {format : Formats.P3109.Format} [Backend.PolicyFor (Codebook.Family format.codebook)] :
      Fma (Codebook.Family format.codebook)

      Fused multiply-add with no rounded or saturated intermediate product.