Module Tolk.Decomp_dtype

Emulated data types.

A target that lacks a data type computes with another one.

A 64-bit integer (Dtype.t.Int64, Dtype.t.Uint64) is two 32-bit words, low first, of Dtype.t.Int32 or Dtype.t.Uint32. Its storage holds twice as many words, and its operations are built from 32-bit ones.
A narrow float (Dtype.t.Float16, Dtype.t.Bfloat16 and the 8-bit floats) is stored in its own format, as the unsigned integer of its width, and computed with as a Dtype.t.Float32: a load converts it up, a store converts it down (f2f). A cast to it rounds its source to it, once; a source more precise than a Dtype.t.Float32 reaches one rounded to odd. An operation on it computes in Dtype.t.Float32, and its result is rounded to the narrow float only where a store converts it down: a later operation, or a cast of it to another type, reads the unrounded value. A copy or a selection keeps the stored bits.

The conversions are IEEE's: one rounding, to nearest with ties to even, gradual underflow, and infinities and NaNs kept where the format has them.

A type is emulated when the target does not support it (Renderer.supported_dtypes) or the setting Setting.emulated_dtypes names it.

Float conversion

#val f2f : ?sat:bool -> Ops.t -> Dtype.t -> Dtype.t -> Ops.t

f2f ~sat v fr to_ converts between a narrow float and Dtype.t.Float32, v being the bits of a float of type fr, as the unsigned integer of its width:

widening to Dtype.t.Float32, it is the value v encodes, subnormals included;
narrowing from Dtype.t.Float32, it is the bits, as the unsigned integer of to_'s width, of the value v encodes rounded to to_'s precision, to nearest with ties to even, into a subnormal below to_'s least normal. A value that rounds past to_'s greatest finite value, and an infinity, is an infinity, which a format without one holds as its NaN; but a finite value of an 8-bit float, if sat, is at most its greatest finite value.

A NaN stays a NaN, and a quiet one stays quiet; an fnuz format has one NaN, and no negative zero. sat defaults to true.

Raises Invalid_argument unless one of fr and to_ is Dtype.t.Float32 and the other a narrower float.

#val narrow : Ops.t -> Dtype.t -> Ops.t

narrow x dt is x cast to dt, but for a Dtype.t.Float32 from a Dtype.t.Float64 or an integer of 32 or 64 bits whose bounds (Ops.vmin, Ops.vmax) do not lie within 2{^24}, more precise than a float32: then it is x rounded to odd, towards zero with the last bit set if bits were dropped, so that a narrow float rounded to nearest from it is x rounded to nearest once.

It needs only that the target's conversion to Dtype.t.Float32 lands on one of the two float32 values around x, as C11 6.3.1.4p2 and 6.3.1.5p1 promise; not that it rounds to nearest.

Passes

#val computes : Renderer.t -> Dtype.t list

computes r is the data types of Dtype.all, in order, that r's target computes: those it supports (Renderer.supported_dtypes), and those pm_dtype_decomps emulates where it lacks them, the 8-bit floats, Dtype.t.Bfloat16, Dtype.t.Float16, Dtype.t.Int64 and Dtype.t.Uint64.

#val emulates : Renderer.t -> Dtype.t -> bool

emulates r dt is true iff code generation for r's target emulates dt: r does not support it (Renderer.supported_dtypes) or the setting Setting.emulated_dtypes names it, an unsigned 64-bit integer as the signed one that emulates it. The setting is read at emulates r.

#type ctx

The type for the context of pm_dtype_decomps: the types a kernel uses that may need emulation, and the target's renderer.

#val ctx : Renderer.t -> ctx

ctx r is the context for emulating on r's target, with no type found yet.

#val pm_dtype_decomps : (ctx, Ops.t) Ops.Pattern_matcher.t

pm_dtype_decomps notes the narrow floats and 64-bit integers a kernel uses, and at the kernel's Op.t.Sink rewrites it to emulate those that the target lacks, in the promotion order of their types (Dtype.compare). Unsigned 64-bit integers are emulated with signed ones.

Raises Invalid_argument if a 64-bit integer variable must be emulated, or if Setting.emulated_dtypes names no data type.