Correctly rounded reductions for configured binary values

These functions lift the format-generic reduction kernel to the ordinary configured ExecFloat.Binary carrier. Operands are decoded into the exact model, reduced there, and the single final result is packed back into the configured carrier.

For finite operands, sum forms the exact mathematical sum and rounds once. dot forms every product exactly, sums those products exactly, and rounds once. The configured type fixes the source and destination format, and the rounding direction is an optional argument.

@[macro_inline]

def FloatLib.Floats.ExecFloat.Binary.sum {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (values : Array (Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode := Formats.BinaryInterchange.Model.IEEERoundingMode.nearest) (status : Bool := false) : match status with | true => IEEEOutcome | false => Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

Correctly rounded sum of configured values in mode (nearest-even by default).

Every operand is decoded exactly, the complete sum is accumulated without intermediate rounding, and the result is rounded once. With status := true the result also carries the IEEE exception indicators and the ternary value. The value form packs the value-only descriptor-model sum, which computes no exception indicators.

@[macro_inline]

def FloatLib.Floats.ExecFloat.Binary.sumList {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (values : List (Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode := Formats.BinaryInterchange.Model.IEEERoundingMode.nearest) (status : Bool := false) : match status with | true => IEEEOutcome | false => Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

List entry point for correctly rounded configured summation, with the options of sum.

@[macro_inline]

def FloatLib.Floats.ExecFloat.Binary.dot {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : Array (Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode := Formats.BinaryInterchange.Model.IEEERoundingMode.nearest) (status : Bool := false) : Except Numerics.ReductionError (match status with | true => IEEEOutcome | false => Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code)

Correctly rounded dot product of configured values in mode (nearest-even by default).

Products and their sum are exact until one final rounding. Unequal lengths return ReductionError.lengthMismatch, so no pair is silently dropped. With status := true a successful result also carries the IEEE exception indicators and the ternary value. The value form packs the value-only descriptor-model dot product, which computes no exception indicators.

@[macro_inline]

def FloatLib.Floats.ExecFloat.Binary.dotList {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : List (Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode := Formats.BinaryInterchange.Model.IEEERoundingMode.nearest) (status : Bool := false) : Except Numerics.ReductionError (match status with | true => IEEEOutcome | false => Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code)

List entry point for a correctly rounded configured dot product, with the options of dot.