Arrays of UInt64: basics

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

def ScalarArray.UInt64Array : Type

Arrays of UInt64 values, stored unboxed in a scalar array, 8 bytes per element.

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

Equations

• ScalarArray.UInt64Array = Quot fun (x x_1 : Array UInt64) => False

@[noinline, implemented_by ScalarArray.UInt64Array.mkImpl]

def ScalarArray.UInt64Array.mk (a : Array UInt64) : UInt64Array

The UInt64Array whose elements are a.

Equations

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

@[noinline]

def ScalarArray.UInt64Array.toArray (a : UInt64Array) : Array UInt64

The elements of a as an Array UInt64.

Equations

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

@[simp]

theorem ScalarArray.UInt64Array.toArray_mk (a : Array UInt64) : (mk a).toArray = a

@[simp]

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

@[extern lean_byte_array_size]

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

The number of elements of a.

Equations

• a.size = a.toArray.size

@[inline]

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

For internal use only.

Equations

• a.usizeImpl = (unsafeCast a).size

@[implemented_by ScalarArray.UInt64Array.usizeImpl]

def ScalarArray.UInt64Array.usize (a : UInt64Array) : 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.UInt64Array.toNat_usize_le (a : UInt64Array) : 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 "((uint64_t*)lean_sarray_cptr(#1))[#2]"]

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

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.UInt64Array.getImpl]

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

The element at index i.

Equations

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

@[inline]

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

For internal use only.

Equations

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

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

unsafe def ScalarArray.UInt64Array.setUnsafe (a : UInt64Array) (i : USize) (v : UInt64) : UInt64Array

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.UInt64Array.mk (a.toArray.uset i v ⋯)

@[never_extract, inline]

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

For internal use only.

Equations

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

@[never_extract, implemented_by ScalarArray.UInt64Array.ensureExclusiveImpl]

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

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.UInt64Array.ensureCapacityGrowUnsafe (a : UInt64Array) (n : Nat) : UInt64Array

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.UInt64Array.toUSizeChecked✝ (max n (unsafeCast a).size.toNat)) ⋯)

@[inline]

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

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.UInt64Array.ensureCapacityImpl]

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

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.UInt64Array.ensureExclusiveWithCapacityImpl (a : UInt64Array) (n : Nat) : UInt64Array

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.UInt64Array.ensureExclusiveWithCapacityImpl]

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

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.UInt64Array.mkImpl (a : Array UInt64) : UInt64Array

For internal use only.

Equations

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

def ScalarArray.UInt64Array.toArrayImpl (a : UInt64Array) : Array UInt64

For internal use only.

Equations

• a.toArrayImpl = if a.size < USize.size then ScalarArray.UInt64Array.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.UInt64Array.toArray_eq_toArrayImpl : toArray = toArrayImpl

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

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

Equations

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

@[implemented_by _private.ScalarArray.UInt64.Basic.0.ScalarArray.UInt64Array.emptyWithCapacityImpl]

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

An empty array with room for capacity elements before reallocating.

Equations

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

def ScalarArray.UInt64Array.empty : UInt64Array

The empty array.

Equations

• ScalarArray.UInt64Array.empty = ScalarArray.UInt64Array.emptyWithCapacity 0

@[instance_reducible]

instance ScalarArray.UInt64Array.instEmptyCollection : EmptyCollection UInt64Array

Equations

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

@[instance_reducible]

instance ScalarArray.UInt64Array.instInhabited : Inhabited UInt64Array

Equations

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

@[implemented_by ScalarArray.UInt64Array.usetImpl]

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

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.UInt64Array.mk (a.toArray.uset i v h)

@[inline]

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

For internal use only.

Equations

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

@[implemented_by ScalarArray.UInt64Array.setImpl]

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

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

Equations

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

@[inline]

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

For internal use only.

Equations

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

@[inline]

def ScalarArray.UInt64Array.get! (a : UInt64Array) (i : Nat) : UInt64

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.UInt64.Basic" "ScalarArray.UInt64Array.get!" 308 40 "index out of bounds"

@[inline]

def ScalarArray.UInt64Array.getD (a : UInt64Array) (i : Nat) (v₀ : UInt64) : UInt64

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.UInt64Array.set! (a : UInt64Array) (i : Nat) (v : UInt64) : UInt64Array

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.UInt64Array.instGetElemNatUInt64LtSize : GetElem UInt64Array Nat UInt64 fun (a : UInt64Array) (i : Nat) => i < a.size

Equations

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

@[instance_reducible]

instance ScalarArray.UInt64Array.instGetElemUSizeUInt64LtNatToNatSize : GetElem UInt64Array USize UInt64 fun (a : UInt64Array) (i : USize) => i.toNat < a.size

Equations

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

unsafe def ScalarArray.UInt64Array.pushGrowUnsafe (a : UInt64Array) (v : UInt64) : UInt64Array

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.UInt64Array.pushImpl (a : UInt64Array) (v : UInt64) : UInt64Array

For internal use only.

Equations

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

@[implemented_by ScalarArray.UInt64Array.pushImpl]

def ScalarArray.UInt64Array.push (a : UInt64Array) (v : UInt64) : UInt64Array

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.UInt64Array.mk (a.toArray.push v)

@[implemented_by _private.ScalarArray.UInt64.Basic.0.ScalarArray.UInt64Array.appendImpl]

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

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

Equations

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

@[instance_reducible]

instance ScalarArray.UInt64Array.instAppend : Append UInt64Array

Equations

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

@[implemented_by _private.ScalarArray.UInt64.Basic.0.ScalarArray.UInt64Array.copySliceImpl]

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

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.