Pointwise and family tensor operations #
Scalar maps, binary maps, finite tensor families, stacking, and rank-one list construction over native tensor storage.
const, map, zipWith, and stack have logical definitions and
implemented_by fast paths. The observation lemmas below reason about the
logical definitions; the compiler substitutes the fast bodies. The unstack
replacement is registered separately through a proved csimp equality.
Evaluate a finite family once per index in ascending order and retain indexed access.
The temporary buffer also supports dependent tensor families, which have no scalar Storage instance. Public construction APIs expose tensors or packs rather than this buffer.
Instances For
Pointwise algebraic structure #
Every algebraic operation on native tensors is the scalar operation applied coordinatewise. The
instances below are the only 0, -, and • on Rep α s; together with + above they form the
pointwise AddCommGroup and Module structures. The *_apply lemmas are the simp normal forms.
Tensor addition is a commutative monoid, coordinatewise.
Tensor subtraction and negation form a commutative group, coordinatewise.
Mapping the identity function leaves every tensor unchanged.
This is a deterministic simplification rule rather than a global e-matching rule. Combined with map composition, unrestricted congruence closure could otherwise manufacture arbitrarily many nested identity maps.
Two pointwise maps fuse to one scalar composition.
The theorem belongs to the canonical simplifier, but intentionally not to the
global grind set: composition-producing e-matching rules can repeatedly
instantiate through equal identity-map terms.
A scalar map after a pointwise binary operation fuses into that operation.
Pointwise maps on both inputs fuse into one pointwise binary operation.
Native implementation of leading-axis stacking.
For nonempty component shapes, each component is evaluated once in ascending order, and its
buffer is copied into the output with one appendSlice. Empty component shapes need no
component evaluation. The size check succeeds under the storage laws because every component has
Shape.size s entries; its fallback is the reference definition.
Instances For
Place a finite family of identically shaped tensors along a new leading axis.
The transparent definition is the proof semantics. Compiled code uses
stackFast, which evaluates each component once when its shape is nonempty
and skips component evaluation for empty shapes.
Instances For
Buffer of unstackSlice: the component's contiguous interval, copied into a fresh buffer.
Instances For
The copied interval is the matching extract of the source observation.
Leading-axis slice that copies the component's contiguous interval with one appendSlice.
unstack reads each entry through its coordinate, which linearizes the coordinate for every
scalar. The row-major layout puts component i at [i * size s, (i + 1) * size s), so compiled
code copies that interval directly.
Instances For
The contiguous-copy slice agrees with the coordinate definition of unstack.
Stack the tensors in a list along a new leading axis.
For example, two tensors of shape [3] give a tensor of shape [2, 3].
The first component's entries come before the second's in row-major storage.
stack asks for components by index. We cache the list as an array so each
lookup takes constant time. Reading the list directly would walk from its
front again for each component.
Instances For
Turn a list into a one-dimensional tensor in the same order.
For example, [x, y, z] gives shape [3], with x at coordinate zero.
We cache the list as an array before Storage.ofFn copies its entries into
the buffer selected by Storage α. Without the cache, requesting indices
0, ..., n - 1 would follow n * (n - 1) / 2 list links in total.
The array makes each indexed read constant time.
Instances For
Ordinary list notation constructs a rank-one tensor when the literal length matches the expected static dimension. Each list entry is copied into the tensor's storage in order.