Arrays of UInt16: basics

The type, its model, and the operations compiled to the runtime: reads, writes, push, capacity, append and copySlice.

def ScalarArray.UInt16Array : Type

Arrays of UInt16 values, stored unboxed in a scalar array, 2 bytes per element.

The logical model is an Array UInt16: UInt16Array.mk and UInt16Array.toArray convert between the two. cases and induction split a UInt16Array as mk a.

Equations

• ScalarArray.UInt16Array = Quot fun (x x_1 : Array UInt16) => False

@[noinline, implemented_by ScalarArray.UInt16Array.mkImpl]

def ScalarArray.UInt16Array.mk (a : Array UInt16) : UInt16Array

The UInt16Array whose elements are a.

Equations

• ScalarArray.UInt16Array.mk a = Quot.mk (fun (x x_1 : Array UInt16) => False) a

@[noinline]

def ScalarArray.UInt16Array.toArray (a : UInt16Array) : Array UInt16

The elements of a as an Array UInt16.

Equations

• a.toArray = Quot.lift id ScalarArray.UInt16Array.toArray._proof_1 a

@[simp]

theorem ScalarArray.UInt16Array.toArray_mk (a : Array UInt16) : (mk a).toArray = a

@[simp]

theorem ScalarArray.UInt16Array.mk_toArray (a : UInt16Array) : mk a.toArray = a

@[extern lean_byte_array_size]

def ScalarArray.UInt16Array.size (a : UInt16Array) : Nat

The number of elements of a.

Equations

• a.size = a.toArray.size

@[inline]

unsafe def ScalarArray.UInt16Array.usizeImpl (a : UInt16Array) : USize

For internal use only.

Equations

• a.usizeImpl = (unsafeCast a).size

@[implemented_by ScalarArray.UInt16Array.usizeImpl]

def ScalarArray.UInt16Array.usize (a : UInt16Array) : USize

The size of a as a USize. Since USize can address all memory, no array has more elements than USize can count.

Equations

• a.usize = a.size.toUSize

theorem ScalarArray.UInt16Array.toNat_usize_le (a : UInt16Array) : a.usize.toNat ≤ a.size

a.usize is at most the size, so it bounds the indices of loops that stop at a.usize.

@[extern c inline "((uint16_t*)lean_sarray_cptr(#1))[#2]"]

def ScalarArray.UInt16Array.uget (a : UInt16Array) (i : USize) (h : i.toNat < a.size := by get_elem_tactic) : UInt16

The element at the USize index i. It compiles to an inline load.

Equations

• a.uget i h = a.toArray.uget i h

@[implemented_by ScalarArray.UInt16Array.getImpl]

def ScalarArray.UInt16Array.get (a : UInt16Array) (i : Nat) (h : i < a.size := by get_elem_tactic) : UInt16

The element at index i.

Equations

• a.get i h = a.toArray[i]

@[inline]

unsafe def ScalarArray.UInt16Array.getImpl (a : UInt16Array) (i : Nat) (h : i < a.size := by get_elem_tactic) : UInt16

For internal use only.

Equations

• a.getImpl i x✝ = a.uget i.toUSize ⋯

@[never_extract, extern c inline "#1;\n((uint16_t*)lean_sarray_cptr(#1))[#2] = #3"]

unsafe def ScalarArray.UInt16Array.setUnsafe (a : UInt16Array) (i : USize) (v : UInt16) : UInt16Array

Stores v at index i in place. Only valid when a is exclusive and i is in bounds. Public only so that uset can be inlined into code in other modules.

Equations

• a.setUnsafe i v = ScalarArray.UInt16Array.mk (a.toArray.uset i v ⋯)

@[never_extract, inline]

unsafe def ScalarArray.UInt16Array.ensureExclusiveImpl (a : UInt16Array) : UInt16Array

For internal use only.

Equations

• a.ensureExclusiveImpl = unsafeCast (unsafeCast a).ensureExclusive

@[never_extract, implemented_by ScalarArray.UInt16Array.ensureExclusiveImpl]

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

Returns a itself when it is not shared, and a copy otherwise. Logically this is the identity. It is useful before a run of in-place writes, so that only the first one can copy.

Equations

• a.ensureExclusive = a

@[never_extract]

unsafe def ScalarArray.UInt16Array.ensureCapacityGrowUnsafe (a : UInt16Array) (n : Nat) : UInt16Array

ensureCapacity and ensureExclusiveWithCapacity when a lacks room for n elements: copies a with room for exactly max n a.size elements. Out of line so that inlined call sites stay small. Public only so that those functions can be inlined into code in other modules.

Equations

• a.ensureCapacityGrowUnsafe n = unsafeCast (ScalarArray.Raw.copyWithCapacity✝ (unsafeCast a) (ScalarArray.UInt16Array.toUSizeChecked✝ (max n (unsafeCast a).size.toNat)) ⋯)

@[inline]

unsafe def ScalarArray.UInt16Array.ensureCapacityImpl (a : UInt16Array) (n : Nat) : UInt16Array

For internal use only.

Equations

• a.ensureCapacityImpl n = if n ≤ (unsafeCast a).capacity.toNat then a else a.ensureCapacityGrowUnsafe n

@[never_extract, implemented_by ScalarArray.UInt16Array.ensureCapacityImpl]

def ScalarArray.UInt16Array.ensureCapacity (a : UInt16Array) (n : Nat) : UInt16Array

Returns a itself when it has room for n elements, and otherwise a copy with room for exactly max n a.size elements. Logically this is the identity. Unlike ensureExclusiveWithCapacity, it does not copy a just because it is shared.

Equations

• a.ensureCapacity n = a

@[inline]

unsafe def ScalarArray.UInt16Array.ensureExclusiveWithCapacityImpl (a : UInt16Array) (n : Nat) : UInt16Array

For internal use only.

Equations

• a.ensureExclusiveWithCapacityImpl n = if n ≤ (unsafeCast a).capacity.toNat then a.ensureExclusive else a.ensureCapacityGrowUnsafe n

@[never_extract, implemented_by ScalarArray.UInt16Array.ensureExclusiveWithCapacityImpl]

def ScalarArray.UInt16Array.ensureExclusiveWithCapacity (a : UInt16Array) (n : Nat) : UInt16Array

Returns a itself when it is not shared and has room for n elements, and otherwise a single copy with room for exactly max n a.size elements. Logically this is the identity. It is useful before a run of in-place writes and pushes, so that none of them copies.

Equations

• a.ensureExclusiveWithCapacity n = a

unsafe def ScalarArray.UInt16Array.mkImpl (a : Array UInt16) : UInt16Array

For internal use only.

Equations

• ScalarArray.UInt16Array.mkImpl a = ScalarArray.UInt16Array.mkWithCapacityImpl✝ a

def ScalarArray.UInt16Array.toArrayImpl (a : UInt16Array) : Array UInt16

For internal use only.

Equations

• a.toArrayImpl = if a.size < USize.size then ScalarArray.UInt16Array.toArrayImpl.loop✝ a a.usize ⋯ 0 (Array.replicate a.size default) ⋯ else Array.ofFn fun (i : Fin a.size) => a.get ↑i ⋯

@[csimp]

theorem ScalarArray.UInt16Array.toArray_eq_toArrayImpl : toArray = toArrayImpl

def ScalarArray.UInt16Array.casesMk {motive : UInt16Array → Sort u} (mk : (a : Array UInt16) → motive (mk a)) (a : UInt16Array) : motive a

Case analysis on a UInt16Array as mk a. It is the default for cases and induction.

Equations

• ScalarArray.UInt16Array.casesMk mk a = ⋯ ▸ mk a.toArray

@[implemented_by _private.ScalarArray.UInt16.Basic.0.ScalarArray.UInt16Array.emptyWithCapacityImpl]

def ScalarArray.UInt16Array.emptyWithCapacity (capacity : Nat) : UInt16Array

An empty array with room for capacity elements before reallocating.

Equations

• ScalarArray.UInt16Array.emptyWithCapacity capacity = ScalarArray.UInt16Array.mk #[]

def ScalarArray.UInt16Array.empty : UInt16Array

The empty array.

Equations

• ScalarArray.UInt16Array.empty = ScalarArray.UInt16Array.emptyWithCapacity 0

@[instance_reducible]

instance ScalarArray.UInt16Array.instEmptyCollection : EmptyCollection UInt16Array

Equations

• ScalarArray.UInt16Array.instEmptyCollection = { emptyCollection := ScalarArray.UInt16Array.empty }

@[instance_reducible]

instance ScalarArray.UInt16Array.instInhabited : Inhabited UInt16Array

Equations

• ScalarArray.UInt16Array.instInhabited = { default := ScalarArray.UInt16Array.empty }

@[implemented_by ScalarArray.UInt16Array.usetImpl]

def ScalarArray.UInt16Array.uset (a : UInt16Array) (i : USize) (v : UInt16) (h : i.toNat < a.size := by get_elem_tactic) : UInt16Array

Replaces the element at index i, in place when a is not shared. It compiles to inline C: one check that a is exclusive, copying it if not, and one store.

Equations

• a.uset i v h = ScalarArray.UInt16Array.mk (a.toArray.uset i v h)

@[inline]

unsafe def ScalarArray.UInt16Array.usetImpl (a : UInt16Array) (i : USize) (v : UInt16) (h : i.toNat < a.size := by get_elem_tactic) : UInt16Array

For internal use only.

Equations

• a.usetImpl i v x✝ = a.ensureExclusive.setUnsafe i v

@[implemented_by ScalarArray.UInt16Array.setImpl]

def ScalarArray.UInt16Array.set (a : UInt16Array) (i : Nat) (v : UInt16) (h : i < a.size := by get_elem_tactic) : UInt16Array

Replaces the element at index i, in place when a is not shared, like uset.

Equations

• a.set i v h = ScalarArray.UInt16Array.mk (a.toArray.set i v h)

@[inline]

unsafe def ScalarArray.UInt16Array.setImpl (a : UInt16Array) (i : Nat) (v : UInt16) (h : i < a.size := by get_elem_tactic) : UInt16Array

For internal use only.

Equations

• a.setImpl i v x✝ = a.uset i.toUSize v ⋯

@[inline]

def ScalarArray.UInt16Array.get! (a : UInt16Array) (i : Nat) : UInt16

The element at index i. Panics if i is out of bounds, and then returns default.

Equations

• a.get! i = if h : i < a.size then a.get i h else panicWithPosWithDecl "ScalarArray.UInt16.Basic" "ScalarArray.UInt16Array.get!" 308 40 "index out of bounds"

@[inline]

def ScalarArray.UInt16Array.getD (a : UInt16Array) (i : Nat) (v₀ : UInt16) : UInt16

The element at index i, or v₀ if i is out of bounds.

Equations

• a.getD i v₀ = if h : i < a.size then a.get i h else v₀

@[inline]

def ScalarArray.UInt16Array.set! (a : UInt16Array) (i : Nat) (v : UInt16) : UInt16Array

Replaces the element at index i. If i is out of bounds, the array is returned unmodified.

Equations

• a.set! i v = if h : i < a.size then a.set i v h else a

@[instance_reducible]

instance ScalarArray.UInt16Array.instGetElemNatUInt16LtSize : GetElem UInt16Array Nat UInt16 fun (a : UInt16Array) (i : Nat) => i < a.size

Equations

• ScalarArray.UInt16Array.instGetElemNatUInt16LtSize = { getElem := fun (a : ScalarArray.UInt16Array) (i : Nat) (h : i < a.size) => a.get i h }

@[instance_reducible]

instance ScalarArray.UInt16Array.instGetElemUSizeUInt16LtNatToNatSize : GetElem UInt16Array USize UInt16 fun (a : UInt16Array) (i : USize) => i.toNat < a.size

Equations

• ScalarArray.UInt16Array.instGetElemUSizeUInt16LtNatToNatSize = { getElem := fun (a : ScalarArray.UInt16Array) (i : USize) (h : i.toNat < a.size) => a.uget i h }

unsafe def ScalarArray.UInt16Array.pushGrowUnsafe (a : UInt16Array) (v : UInt16) : UInt16Array

push when a is full: copies a with capacity 2 * capacity + 1, then appends v. Out of line so that inlined push call sites stay small. Public only so that push can be inlined into code in other modules.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

unsafe def ScalarArray.UInt16Array.pushImpl (a : UInt16Array) (v : UInt16) : UInt16Array

For internal use only.

Equations

• One or more equations did not get rendered due to their size.

@[implemented_by ScalarArray.UInt16Array.pushImpl]

def ScalarArray.UInt16Array.push (a : UInt16Array) (v : UInt16) : UInt16Array

Appends v to a, in place when a is not shared and has room. A full array grows to capacity 2 * capacity + 1, so repeated pushes take amortized constant time.

Equations

• a.push v = ScalarArray.UInt16Array.mk (a.toArray.push v)

@[implemented_by _private.ScalarArray.UInt16.Basic.0.ScalarArray.UInt16Array.appendImpl]

def ScalarArray.UInt16Array.append (a b : UInt16Array) : UInt16Array

Appends the elements of b to a, in place when a is not shared and has room.

Equations

• a.append b = ScalarArray.UInt16Array.mk (a.toArray ++ b.toArray)

@[instance_reducible]

instance ScalarArray.UInt16Array.instAppend : Append UInt16Array

Equations

• ScalarArray.UInt16Array.instAppend = { append := ScalarArray.UInt16Array.append }

@[implemented_by _private.ScalarArray.UInt16.Basic.0.ScalarArray.UInt16Array.copySliceImpl]

def ScalarArray.UInt16Array.copySlice (src : UInt16Array) (srcOff : Nat) (dest : UInt16Array) (destOff len : Nat) (exact : Bool := true) : UInt16Array

Copies the elements of src from index srcOff up to, but not including, srcOff + len into dest starting at index destOff, growing dest if necessary. The copy works in place when dest is not shared and has room. If exact is false, the capacity is doubled when dest grows.

Equations

• One or more equations did not get rendered due to their size.