This module defines the `ByteSlice` structure. It's a modified version of the `SubArray` code, with some functions specific to `ByteSlice`.

source
structure Std.Slice.Internal.ByteSliceData :
Type

Internal representation of `ByteSlice`, which is an abbreviation for `Slice ByteSliceData`.

- byteArray : ByteArray

  The underlying byte array.

- start : Nat

  The starting index of the region of interest (inclusive).

- stop : Nat

  The ending index of the region of interest (exclusive).

- start_le_stop : self.start ≤ self.stop

  The starting index is no later than the ending index.

  The ending index is exclusive. If the starting and ending indices are equal, then the byte slice is empty.

- stop_le_size_byteArray : self.stop ≤ self.byteArray.size

  The stopping index is no later than the end of the byte array.

  The ending index is exclusive. If it is equal to the size of the byte array, then the last byte of the byte array is in the byte slice.

Instances For

source
@[reducible, inline]
abbrev ByteSlice :
Type

A region of some underlying byte array.

A byte slice contains a byte array together with the start and end indices of a region of interest. Byte slices can be used to avoid copying or allocating space, while being more convenient than tracking the bounds by hand. The region of interest consists of every index that is both greater than or equal to `start` and strictly less than `stop`.

Equations

- ByteSlice = Std.Slice Std.Slice.Internal.ByteSliceData

Instances For

source
instance instSelfSliceByteSliceDataByteSlice :
Std.Slice.Self (Std.Slice Std.Slice.Internal.ByteSliceData) ByteSlice
source
@[inline]
def ByteSlice.byteArray (xs : ByteSlice) :
ByteArray

The underlying byte array.

Equations

- xs.byteArray = xs.internalRepresentation.byteArray

Instances For

source
@[inline]
def ByteSlice.start (xs : ByteSlice) :
Nat

The starting index of the region of interest (inclusive).

Equations

- xs.start = xs.internalRepresentation.start

Instances For

source
@[inline]
def ByteSlice.stop (xs : ByteSlice) :
Nat

The ending index of the region of interest (exclusive).

Equations

- xs.stop = xs.internalRepresentation.stop

Instances For

source
theorem ByteSlice.start_le_stop (xs : ByteSlice) :
xs.start ≤ xs.stop

The starting index is no later than the ending index.

The ending index is exclusive. If the starting and ending indices are equal, then the byte slice is empty.

source
theorem ByteSlice.stop_le_size_byteArray (xs : ByteSlice) :
xs.stop ≤ xs.byteArray.size

The stopping index is no later than the end of the byte array.

The ending index is exclusive. If it is equal to the size of the byte array, then the last byte of the byte array is in the byte slice.

source
def ByteSlice.size (s : ByteSlice) :
Nat

Computes the size of the byte slice.

Equations

- s.size = s.stop - s.start

Instances For

source
theorem ByteSlice.size_le_size_byteArray {s : ByteSlice} :
s.size ≤ s.byteArray.size
source
def ByteSlice.get (s : ByteSlice) (i : Fin s.size) :
UInt8

Extracts a byte from the byte slice.

The index is relative to the start of the byte slice, rather than the underlying byte array.

Equations

- s.get i = s.byteArray[s.start + ↑i]

Instances For

source
instance ByteSlice.instGetElemNatUInt8LtSize :
GetElem ByteSlice Nat UInt8 fun (xs : ByteSlice) (i : Nat) => i < xs.size
Equations

- ByteSlice.instGetElemNatUInt8LtSize = { getElem := fun (xs : ByteSlice) (i : Nat) (h : i < xs.size) => xs.get ⟨i, h⟩ }

source
@[inline]
def ByteSlice.getD (s : ByteSlice) (i : Nat) (v₀ : UInt8) :
UInt8

Extracts a byte from the byte slice, or returns a default value `v₀` when the index is out of bounds.

The index is relative to the start and end of the byte slice, rather than the underlying byte array.

Equations

- s.getD i v₀ = if h : i < s.size then s[i] else v₀

Instances For

source
@[reducible, inline]
abbrev ByteSlice.get! (s : ByteSlice) (i : Nat) :
UInt8

Extracts a byte from the byte slice, or returns a default value when the index is out of bounds.

The index is relative to the start and end of the byte slice, rather than the underlying byte array. The default value is 0.

Equations

- s.get! i = s.getD i 0

Instances For

source
def ByteSlice.empty :
ByteSlice

The empty byte slice.

This empty byte slice is backed by an empty byte array.

Equations

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

Instances For

source
def ByteSlice.ofByteArray (ba : ByteArray) :
ByteSlice

Creates a new ByteSlice of a ByteArray

Equations

- ByteSlice.ofByteArray ba = { internalRepresentation := { byteArray := ba, start := 0, stop := ba.size, start_le_stop := ⋯, stop_le_size_byteArray := ⋯ } }

Instances For

source
instance ByteSlice.instEmptyCollection :
EmptyCollection ByteSlice
Equations

- ByteSlice.instEmptyCollection = { emptyCollection := ByteSlice.empty }

source
instance ByteSlice.instInhabited :
Inhabited ByteSlice
Equations

- ByteSlice.instInhabited = { default := ∅ }

source
def ByteSlice.toByteArray (s : ByteSlice) :
ByteArray

Converts a byte slice back to a byte array by copying the relevant portion.

Equations

- s.toByteArray = s.byteArray.extract s.start (s.start + s.size)

Instances For

source
@[extern lean_byteslice_beq]
def ByteSlice.beq (a b : ByteSlice) :
Bool

Comparison function

Equations

- a.beq b = (a.toByteArray == b.toByteArray)

Instances For

source
instance ByteSlice.instBEq :
BEq ByteSlice
Equations

- ByteSlice.instBEq = { beq := ByteSlice.beq }

source
@[inline]
def ByteSlice.foldrM {β : Type v} {m : Type v → Type w} [Monad m] (f : UInt8 → β → m β) (init : β) (as : ByteSlice) :
m β

Folds a monadic operation from right to left over the bytes in a byte slice.

An accumulator of type `β` is constructed by starting with `init` and monadically combining each byte of the byte slice with the current accumulator value in turn, moving from the end to the start. The monad in question may permit early termination or repetition.

Examples:

    #eval (ByteArray.mk #[1, 2, 3]).toByteSlice.foldrM (init := 0) fun x acc =>
      some x.toNat + acc

    some 6

Equations

- ByteSlice.foldrM f init as = ByteSlice.foldrM.loop✝ f as 0 init

Instances For

source
@[inline]
def ByteSlice.forM {m : Type v → Type w} [Monad m] (f : UInt8 → m PUnit) (as : ByteSlice) :
m PUnit

Runs a monadic action on each byte of a byte slice.

The bytes are processed starting at the lowest index and moving up.

Equations

- ByteSlice.forM f as = ByteSlice.forM.loop✝ f as 0

Instances For

source
@[inline]
def ByteSlice.foldr {β : Type v} (f : UInt8 → β → β) (init : β) (as : ByteSlice) :
β

Folds an operation from right to left over the bytes in a byte slice.

An accumulator of type `β` is constructed by starting with `init` and combining each byte of the byte slice with the current accumulator value in turn, moving from the end to the start.

Examples:

- `(ByteArray.mk #[1, 2, 3]).toByteSlice.foldr (·.toNat + ·) 0 = 6`
- `(ByteArray.mk #[1, 2, 3]).toByteSlice.popFront.foldr (·.toNat + ·) 0 = 5`

Equations

- ByteSlice.foldr f init as = (ByteSlice.foldrM (fun (x1 : UInt8) (x2 : β) => pure (f x1 x2)) init as).run

Instances For

source
def ByteSlice.slice (s : ByteSlice) (start : Nat := 0) (stop : Nat := s.size) :
ByteSlice

Creates a sub-slice of the byte slice with the given bounds.

If `start` or `stop` are not valid bounds for a sub-slice, then they are clamped to the slice's size. Additionally, the starting index is clamped to the ending index.

The indices are relative to the current slice, not the underlying byte array.

Equations

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

Instances For

source
def ByteSlice.contains (s : ByteSlice) (byte : UInt8) :
Bool

Checks if the byte slice contains a specific byte value.

Returns `true` if any byte in the slice equals the given value, `false` otherwise.

Equations

- s.contains byte = ByteSlice.contains.loop✝ s byte 0

Instances For

source
def ByteArray.toByteSlice (as : ByteArray) (start : Nat := 0) (stop : Nat := as.size) :
ByteSlice

Returns a byte slice of a byte array, with the given bounds.

If `start` or `stop` are not valid bounds for a byte slice, then they are clamped to byte array's size. Additionally, the starting index is clamped to the ending index.

Equations

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

Instances For

source
instance instSliceableByteArrayNatByteSlice :
Std.Rcc.Sliceable ByteArray Nat ByteSlice
Equations

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

source
instance instSliceableByteArrayNatByteSlice_1 :
Std.Rco.Sliceable ByteArray Nat ByteSlice
Equations

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

source
instance instSliceableByteArrayNatByteSlice_2 :
Std.Rci.Sliceable ByteArray Nat ByteSlice
Equations

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

source
instance instSliceableByteArrayNatByteSlice_3 :
Std.Roc.Sliceable ByteArray Nat ByteSlice
Equations

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

source
instance instSliceableByteArrayNatByteSlice_4 :
Std.Roo.Sliceable ByteArray Nat ByteSlice
Equations

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

source
instance instSliceableByteArrayNatByteSlice_5 :
Std.Roi.Sliceable ByteArray Nat ByteSlice
Equations

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

source
instance instSliceableByteArrayNatByteSlice_6 :
Std.Ric.Sliceable ByteArray Nat ByteSlice
Equations

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

source
instance instSliceableByteArrayNatByteSlice_7 :
Std.Rio.Sliceable ByteArray Nat ByteSlice
Equations

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

source
instance instSliceableByteArrayNatByteSlice_8 :
Std.Rii.Sliceable ByteArray Nat ByteSlice
Equations

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

source
instance instSliceableByteSliceNat :
Std.Rcc.Sliceable ByteSlice Nat ByteSlice
Equations

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

source
instance instSliceableByteSliceNat_1 :
Std.Rco.Sliceable ByteSlice Nat ByteSlice
Equations

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

source
instance instSliceableByteSliceNat_2 :
Std.Rci.Sliceable ByteSlice Nat ByteSlice
Equations

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

source
instance instSliceableByteSliceNat_3 :
Std.Roc.Sliceable ByteSlice Nat ByteSlice
Equations

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

source
instance instSliceableByteSliceNat_4 :
Std.Roo.Sliceable ByteSlice Nat ByteSlice
Equations

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

source
instance instSliceableByteSliceNat_5 :
Std.Roi.Sliceable ByteSlice Nat ByteSlice
Equations

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

source
instance instSliceableByteSliceNat_6 :
Std.Ric.Sliceable ByteSlice Nat ByteSlice
Equations

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

source
instance instSliceableByteSliceNat_7 :
Std.Rio.Sliceable ByteSlice Nat ByteSlice
Equations

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

source
instance instSliceableByteSliceNat_8 :
Std.Rii.Sliceable ByteSlice Nat ByteSlice
Equations

- instSliceableByteSliceNat_8 = { mkSlice := fun (xs : ByteSlice) (x : Std.Rii Nat) => have halfOpenRange := 0...xs.size; xs.slice halfOpenRange.lower halfOpenRange.upper }