Module Tolk.Spec

The type for specifications.

shared accepts the operations of every stage:

• sinks, and constants and stacks of constants;
• arithmetic whose operands have its type: a Op.t.Where's condition is boolean and comparisons compare operands of one type; a shift's count may also be uint32; bitwise operations take no floats, and divisions and remainders only integers;
• casts, ranges, indexes with integer indexes, ends of bounded loops, and loop back-edges on a scalar boolean condition;
• parameters, local and register buffers, binaries, groups of effects, orderings of storage, calls of opaque bodies whose arguments start where their parameters assume (Shape.storage_phase), barriers and instructions;
• loads and stores through an index or a shrink, a gated load's alternative being of the load's type and a store's value of its target's type, and stores into storage;
• matrix multiply-accumulates.

A weak type (Dtype.weaks) matches any type of its kind (Dtype.weak), and Ops.invalid any type.

When Setting.check_oob holds, a load or store through an index into storage must be proved in bounds: the bounds of the index (Ops.vmin, Ops.vmax) must lie within the storage's Shape.max_numel. An index they do not prove fails, whatever its gate, and its bounds, the index and the gate are printed on standard error, saying that the bound cannot be proven without a solver.

tensor is shared with the operations of tensor graphs: float-only unary math; global buffers with a size and a device, and storage declared without a buffer (Op.t.Alloc); variables without a device; unlowered Op.t.Specials; movement, the shape of a reshape or an expand being integers; reductions; copies to a device other than a disk; Op.t.Detach, Op.t.Contiguous_backward and Op.t.Stage; programs as compilation fills them in: a sink, then its linear form, its source and its binary; and calls of opaque bodies wherever their arguments start, since scheduling decides what each becomes.

program is shared as programs restrict it: every width is stated, so a constant appears only under the cast that types it and nothing else is weak; there is no movement but a shrink of storage by a constant length, no global buffer, no parameter that names a device, since a program runs on the devices of its call's arguments, and no Ops.invalid. It adds conditionals (Op.t.If, Op.t.Endif) and lowered, int32 Op.t.Specials.

full is the rules of the forms between stages (ends of loops over any integers, any ordering, any load or store), then tensor's and program's rules, in that order.

kernel_graph accepts the graph of kernel calls: a sink of calls of opaque bodies over storage and parameters, with the constants, stacks, casts and bitcasts that make their arguments, and orderings of storage. A call may run in a loop, an Op.t.End of Ops.Axis_type.t.Loop ranges around it, and read views of storage (Op.t.Shrink) that move with those ranges, their bounds constants, loop ranges, and weak integer sums and products of them.

type_verify ~calls spec u checks every node of u's graph against spec, sources first (Ops.toposort ~calls u). When Setting.debug is 3 or more, a failure first prints the graph's nodes on standard error (Render.render_uir).

Raises Invalid_argument on the first node that fails, naming its position in that order, its operation, type and number of sources, each source's operation, type and argument, and its own argument.