Module Ir.Ops

Canonical witnesses for every precision, including Void_prec. prec carries GADT witnesses, so its enumeration cannot use @@deriving enumerate. Keep the exhaustive sentinel beside this list: a new constructor requires an explicit enumeration decision here.

Families describe arithmetic, not the Bigarray representation: bf16 and fp8 are floats despite integer storage witnesses. Uint4x32_prec is packed RNG state, not a scalar integer; Void_prec represents no value and belongs to neither arithmetic family.

Scalar integer arithmetic only; excludes packed uint4x32 and Void_prec.

Scalar arithmetic formats, including integer and floating-point formats.

All storage-bearing formats, including packed RNG state; Void_prec is excluded. Backend rendering sweeps use this set even though individual operators can reject particular pairs.

Returns the precision to use for indexing arithmetic: signed int32, or int64 under the large_models setting (docs/proposals/signed-index-precision.md). Signedness makes machine index arithmetic agree with mathematical integers (no wrap traps for negative intermediates such as convolution offset = -padding forms), and is friendlier to C compilers than defined-wrap unsigned. Unsigned precisions remain for data domains only (uint4x32 RNG state, uint8/uint32 stored values such as class IDs). Int32 overflow is excluded by contract, not by widening: every per-node (padded) element count must fit int32 unless 64-bit indices are in use -- enforced once per node by Tnode.create forcing dims. large_models still selects the 64-bit width here pending the tnode-granular, interval-driven codegen resolution (which also needs a separate resolution for the Metal pool-slot width before the flag can be retired).

The floating-point formats narrower than f32: the ones a CPU has no arithmetic for, so that every operator over them is a widen/op/narrow round-trip through f32 (gh-ocannl-517). Integer precisions are excluded — their arithmetic is native at every width.

Whether a constant is too large to be safe in a half-precision node. The cutoff (check_half_prec_constants_cutoff, default 2^14) sits well below fp16's 65504 max finite: it is headroom against overflow during arithmetic on the constant, not a representability test.

Both infinities are therefore out of scope by construction, not by exception (gh-ocannl-547). They are exactly representable in IEEE binary16; they are emitted deliberately as reduction identities — see neutral_elem, whose Max is neg_infinity and Min is infinity, with C_syntax rendering them as (-INFINITY) / INFINITY and the GPU backends converting through __float2half / __double2half / a (half) cast, all of which map infinities per IEEE; and no arithmetic can push an infinity past a finite bound, so there is no headroom to preserve. An identity is a sentinel arithmetic is expected to consume, not to accumulate.

Refusing them made every fp16 max-reduction — hence every fp16 softmax, hence every attention model at f16 — fail during lowering, on every backend. NaN is likewise out of scope, by the comparison below being false for it.

Whether every value of precision from converts to to_ exactly, so that a conversion through to_ is the identity on it: equal precisions, or a float widening (fp8 into any wider float -- both e4m3 and e5m2 fit half's and bfloat16's exponent ranges and significands -- half or bfloat16 into single or double, single into double). Integer conversions are conservatively false (gh-ocannl-1788).

The significand width of a floating-point precision, the implicit leading bit included: a format with p such bits holds every integer up to 2^p exactly. 53 for double, 24 for single, 11 for half, 8 for bfloat16 and 3 for fp8 (e5m2: two stored mantissa bits). The one table behind exactness bounds such as schedule_bench's and the tests' Ll_test.exact_partials ~sig_bits (gh-ocannl-1741). Raises Invalid_argument on a non-float precision, which has no significand.

Prefer precision which is more likely to remain functional in the resulting computations. uint4x32 always dominates, because operations that work on uint4x32 do not support other precisions. Otherwise, fractional number precisions dominate; within them, larger dynamic range precisions dominate.

Either the left-neutral or right-neutral element of the operation. Unspecified if the operation does not have a neutral element.

Add's is +0., deliberately not IEEE's additive identity -0. (gh-ocannl-1457): two zeros sum to -0 only when both are -0, so a +0 start makes every all-zero sum +0 on every schedule, while zero-fringe padding, tensor-core K-padding and split partials add +0 terms that a -0 start would make the sign depend on. The decision record: docs/agent-notes/backend-precision-and-simd.md, pinned by test/operations/sum_signed_zero.

Note: currently the %cd syntax only supports infix binops as assignment ops.

In the %cd syntax, we support uncurried notation for binary ops in addition to the infix notation.

Note: currently we do not support unary prefix symbols.

In the %cd syntax, we use uncurried notation for ternary ops.

gh-ocannl-1785: what a plain conversion out of packed RNG state means -- nothing, on every backend. A uint4x32 block holds 128 random bits; which of them make a scalar, and how, is what the uniform operators name (Uint4x32_to_prec_uniform1, Uint4x32_to_prec_uniform, and Uint4x32_to_prec_uniform_lane, which names the lane). Metal used to read a plain conversion as the uniform one and CUDA/HIP as lane 0's bits; every backend's convert_precision now raises this one refusal instead.

One-step f64 -> e5m2, for the host side (an OCaml float is a double) and for the C backends' Double_prec sources. Narrowing via f32 first rounds twice, which disagrees with the GPU fp8 types for values just off an f32 tie (gh-ocannl-648).

Threefry4x32 PRNG - 20 round cryptographic version

Threefry4x32 PRNG - 2 round light version

Threefry4x32 PRNG - default version

Conversion from uint4x32 to various uniform distributions

Conversion to uint4x32 from various types

Returns true if the unary operation is homogeneous in precision, meaning its argument should be converted to the result precision.

Returns true if the vec_unop operation is homogeneous in precision, meaning its argument should be converted to the result precision.

Returns true if the binary operation is homogeneous in precision, meaning its arguments should be converted to the result precision.

Returns true if the ternary operation is homogeneous in precision, meaning its arguments should be converted to the result precision.

What an operator yields when it is evaluated at an integer compute precision, by which the renderer (C_syntax) and the simplifier (Low_level.float_valued, the classification's one reader over expression trees) agree on the rule: a float-valued subexpression is computed in float -- through the operators that follow their operands, as C's usual arithmetic conversions do -- and converted to the integer precision once, at the store or scope holding it, or at an operand of an Integer_only operator.

• Real_valued: a math function with no integer meaning; computed in float whatever its operand.
• Follows_operands: float-valued exactly when one of its value operands is.
• Truth: a comparison or logical connective; with a float-valued operand it compares in float, and its 0/1 result is an integer.
• Integer_only: its integer spelling takes integers only (Mod's %); a float-valued operand converts at the operand.
• Projection: the selected operand itself (binop_conditionality).
• Integer_table: rendered by the integer table as it stands, never float-valued: the heterogeneous RNG operators, and the operators refused at an integer precision (FMA, ToPowOf) -- an integer power is a meaning of its own, refused identically on every backend.

Where follows its two arms; its condition keeps its own precision and type, as in C.