See also: mim::plug::buffer

A shared, low-level buffer abstraction. A buffer.Buf (r, s, T) is a dependent array of rank r and shape s holding elements of type T, but backed by real memory. Elements are accessed via buffer.read / buffer.write and buffers are created via buffer.alloc, all threading the mem.M memory monad. The buffer.lower_ptr phase lowers this layer to mem.Ptr + mem.lea / mem.load / mem.store. Both the tensor and btensor plugins bufferize their operations onto this layer.

Dependencies

import mem;
import core;
import compile;

Types

Buf

A buffer of rank r, shape s, holding elements of type T. Equivalent to the dependent array «s; T» but backed by memory. Literal size-1 axes are normalized away (buffer.Buf (2, (3, 1), T) ≡ buffer.Buf (1, 3, T)), mirroring the folding of the corresponding array types («3, 1; T» ≡ «3; T»), so buffer types derived from logical shapes agree with the (folded) boundary types.

axm Buf: [r: Nat, s: «r; Nat», T: *] → *, normalize_Buf;

Operations

alloc

Allocate a fresh (uninitialized) buffer.

axm alloc: [r: Nat, s: «r; Nat», T: *] as rsT → mem.M 0 → [mem.M 0, Buf rsT];

read

Read the element at idx.

axm read: [r: Nat, s: «r; Nat», T: *] as rsT

→ [mem.M 0, Buf rsT, idx: «i: r; Idx s#i»] → [mem.M 0, T], normalize_read;

write

Write val at idx in place and return the same buffer.

axm write: [r: Nat, s: «r; Nat», T: *] as rsT

→ [mem.M 0, Buf rsT, idx: «i: r; Idx s#i», val: T] → [mem.M 0, Buf rsT], normalize_write;

init

A buffer initialized with the contents of the SSA array value val. This is the boundary conversion from the value world into the buffer world.

axm init: [r: Nat, s: «r; Nat», T: *] as rsT → [mem.M 0, val: «s; T»] → [mem.M 0, Buf rsT];

lit

A buffer initialized with a constant value in every element.

axm lit: [r: Nat, s: «r; Nat», T: *] as rsT → [mem.M 0, T] → [mem.M 0, Buf rsT];

shape

Yields the size of the buffer along dimension i (resolved from the type).

axm shape: [r: Nat, s: «r; Nat», T: *] as rsT → [Buf rsT, i: Idx r] → Nat, normalize_shape;

copy

Copy the whole contents of src into dst and return the updated memory.

axm copy: [r: Nat, s: «r; Nat», T: *] as rsT

→ [mem.M 0, dst src: Buf rsT] → mem.M 0;

Phases

lower_ptr

Lowers Buf / alloc / read / write to mem.Ptr + mem.lea / mem.load / mem.store.

axm lower_ptr: compile.Phase;