The runtime representation of scalar arrays

ScalarArray.Raw exposes the Lean runtime's scalar array objects (lean_sarray_object), the representation behind ByteArray and FloatArray. A scalar array is a header recording the element size, the size and the capacity, followed by the elements stored unboxed.

This module binds the runtime functions on that header: allocation, size and capacity queries, copying, resizing and copies of raw bytes. The typed array modules use it as their runtime representation through import all ScalarArray.Internal, and reach it with unsafeCast. Their own externs are only those that are part of their API, such as size, decEq and markLinear, and the reads and writes uget and setUnsafe, whose C names the element type.

Only what the typed modules' inlined code calls is public: the type, size, capacity, resizeUnsafe and ensureExclusive. Inlined code can only use declarations of publicly imported modules, so the typed modules import this one publicly, and these are visible wherever ScalarArray is imported. They are not part of the API. The rest is private.

inductive ScalarArray.Raw : Type

A Lean runtime scalar array, whatever its element type.

• allocate (elemSize : UInt32) (size capacity : USize) (h : size ≤ capacity) : Raw

@[extern lean_sarray_size]

def ScalarArray.Raw.size : Raw → USize

The number of elements of a.

Equations

• (ScalarArray.Raw.allocate elemSize size capacity h).size = size

@[extern lean_sarray_capacity]

def ScalarArray.Raw.capacity : Raw → USize

The number of elements a has room for before it must be reallocated.

Equations

• (ScalarArray.Raw.allocate elemSize size capacity h).capacity = capacity

@[extern c inline "#1;\nlean_sarray_set_size(#1, #2)"]

unsafe def ScalarArray.Raw.resizeUnsafe (a : Raw) (size : USize) (h : size ≤ a.capacity) (_exclusive : isExclusiveUnsafe a = true := by rfl) : Raw

Sets the size of a to size, in place. Only valid when a is exclusive; the elements past the old size are uninitialized until they are stored.

Equations

• a.resizeUnsafe size h _exclusive = ScalarArray.Raw.allocate (ScalarArray.Raw.elemSize✝ a) size a.capacity h

@[never_extract, extern lean_sarray_ensure_exclusive]

def ScalarArray.Raw.ensureExclusive (a : Raw) : Raw

Returns a itself when it is not shared, and a copy otherwise.

Equations

• a.ensureExclusive = ScalarArray.Raw.copy✝ a

Loop indices