Init.Data.ByteArray.Basic

ByteArray.set! _fun_discr _fun_discr _fun_discr = match _fun_discr, _fun_discr, _fun_discr with | { data := bs }, i, b => { data := Array.set! bs i b }

source

@[extern lean_byte_array_fset]

def ByteArray.set (a : ByteArray) :

Fin (ByteArray.size a) → UInt8 → ByteArray

Equations

ByteArray.set _fun_discr _fun_discr _fun_discr = match _fun_discr, _fun_discr, _fun_discr with | { data := bs }, i, b => { data := Array.set bs i b }

source

@[extern lean_byte_array_uset]

def ByteArray.uset (a : ByteArray) (i : USize) :

(a : UInt8) → USize.toNat i < ByteArray.size a → ByteArray

Equations

ByteArray.uset _fun_discr _fun_discr _fun_discr _fun_discr = match _fun_discr, _fun_discr, _fun_discr, _fun_discr with | { data := bs }, i, v, h => { data := Array.uset bs i v h }

source

def ByteArray.isEmpty (s : ByteArray) :

Bool

Equations

ByteArray.isEmpty s = (ByteArray.size s == 0)

source

@[extern lean_byte_array_copy_slice]

def ByteArray.copySlice (src : ByteArray) (srcOff : Nat) (dest : ByteArray) (destOff : Nat) (len : Nat) (exact : optParam Bool true) :

ByteArray

Equations

ByteArray.copySlice src srcOff dest destOff len exact = { data := Array.extract dest.data 0 destOff ++ Array.extract src.data srcOff (srcOff + len) ++ Array.extract dest.data (destOff + len) (Array.size dest.data) }

Copy the slice at [srcOff,srcOff+len) in src to [destOff,destOff+len) in dest, growing dest if necessary. If exact is false, the capacity will be doubled when grown.

source

def ByteArray.extract (a : ByteArray) (b : Nat) (e : Nat) :

ByteArray

Equations

ByteArray.extract a b e = ByteArray.copySlice a b ByteArray.empty 0 (e - b)

source

def ByteArray.append (a : ByteArray) (b : ByteArray) :

ByteArray

Equations

ByteArray.append a b = ByteArray.copySlice b 0 a (ByteArray.size a) (ByteArray.size b) false

source

instance ByteArray.instAppendByteArray :

Append ByteArray

Equations

ByteArray.instAppendByteArray = { append := ByteArray.append }

source

def ByteArray.toList (bs : ByteArray) :

List UInt8

Equations

ByteArray.toList bs = ByteArray.toList.loop bs 0 []

source

partial def ByteArray.toList.loop (bs : ByteArray) (i : Nat) (r : List UInt8) :

List UInt8

source

@[inline]

def ByteArray.findIdx? (a : ByteArray) (p : UInt8 → Bool) (start : optParam Nat 0) :

Option Nat

Equations

ByteArray.findIdx? a p start = ByteArray.findIdx?.loop a p start

source

@[specialize]

partial def ByteArray.findIdx?.loop (a : ByteArray) (p : UInt8 → Bool) (i : Nat) :

Option Nat

source

@[inline]

unsafe def ByteArray.forInUnsafe {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) :

m β

Equations

ByteArray.forInUnsafe as b f = let sz := USize.ofNat (ByteArray.size as); ByteArray.forInUnsafe.loop as f sz 0 b

source

@[specialize]

unsafe def ByteArray.forInUnsafe.loop {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : ByteArray) (f : UInt8 → β → m (ForInStep β)) (sz : USize) (i : USize) (b : β) :

m β

Equations

ByteArray.forInUnsafe.loop as f sz i b = if i < sz then let a := ByteArray.uget as i (_ : USize.toNat i < ByteArray.size as); do let a ← f a b match a with | ForInStep.done b => pure b | ForInStep.yield b => ByteArray.forInUnsafe.loop as f sz (i + 1) b else pure b

source

@[implementedBy ByteArray.forInUnsafe]

noncomputable def ByteArray.forIn {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) :

m β

Equations

ByteArray.forIn as b f = ByteArray.forIn.loop as f (ByteArray.size as) (_ : ByteArray.size as ≤ ByteArray.size as) b

source

def ByteArray.forIn.loop {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : ByteArray) (f : UInt8 → β → m (ForInStep β)) (i : Nat) (h : i ≤ ByteArray.size as) (b : β) :

m β

Equations

ByteArray.forIn.loop as f 0 x b = pure b
ByteArray.forIn.loop as f (Nat.succ i_2) h_2 b = (fun h' => let_fun this := (_ : ByteArray.size as - 1 < ByteArray.size as); let_fun this := (_ : ByteArray.size as - 1 - i_2 < ByteArray.size as); do let a ← f (ByteArray.get as { val := ByteArray.size as - 1 - i_2, isLt := this }) b match a with | ForInStep.done b => pure b | ForInStep.yield b => ByteArray.forIn.loop as f i_2 (_ : i_2 ≤ ByteArray.size as) b) (_ : i_2 < ByteArray.size as)

source

instance ByteArray.instForInByteArrayUInt8 {m : Type u_1 → Type u_2} :

ForIn m ByteArray UInt8

Equations

ByteArray.instForInByteArrayUInt8 = { forIn := fun {β} [Monad m] => ByteArray.forIn }

source

@[inline]

unsafe def ByteArray.foldlMUnsafe {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start : optParam Nat 0) (stop : optParam Nat (ByteArray.size as)) :

m β

Equations

ByteArray.foldlMUnsafe f init as start stop = if start < stop then if stop ≤ ByteArray.size as then ByteArray.foldlMUnsafe.fold f as (USize.ofNat start) (USize.ofNat stop) init else pure init else pure init

source

@[specialize]

unsafe def ByteArray.foldlMUnsafe.fold {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : β → UInt8 → m β) (as : ByteArray) (i : USize) (stop : USize) (b : β) :

m β

Equations

ByteArray.foldlMUnsafe.fold f as i stop b = if (i == stop) = true then pure b else do let a ← f b (ByteArray.uget as i (_ : USize.toNat i < ByteArray.size as)) ByteArray.foldlMUnsafe.fold f as (i + 1) stop a

source

@[implementedBy ByteArray.foldlMUnsafe]

noncomputable def ByteArray.foldlM {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start : optParam Nat 0) (stop : optParam Nat (ByteArray.size as)) :

m β

Equations

ByteArray.foldlM f init as start stop = let fold := fun stop h => ByteArray.foldlM.loop f as stop h (stop - start) start init; if h : stop ≤ ByteArray.size as then fold stop h else fold (ByteArray.size as) (_ : ByteArray.size as ≤ ByteArray.size as)

source

def ByteArray.foldlM.loop {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : β → UInt8 → m β) (as : ByteArray) (stop : Nat) (h : stop ≤ ByteArray.size as) (i : Nat) (j : Nat) (b : β) :

m β

Equations

ByteArray.foldlM.loop f as stop h 0 j b = if hlt : j < stop then pure b else pure b
ByteArray.foldlM.loop f as stop h (Nat.succ i') j b = if hlt : j < stop then do let a ← f b (ByteArray.get as { val := j, isLt := (_ : j < ByteArray.size as) }) ByteArray.foldlM.loop f as stop h i' (j + 1) a else pure b

source

@[inline]

def ByteArray.foldl {β : Type v} (f : β → UInt8 → β) (init : β) (as : ByteArray) (start : optParam Nat 0) (stop : optParam Nat (ByteArray.size as)) :

β

Equations

ByteArray.foldl f init as start stop = Id.run (ByteArray.foldlM f init as start stop)

source

def List.toByteArray (bs : List UInt8) :

ByteArray

Equations

List.toByteArray bs = List.toByteArray.loop bs ByteArray.empty

source

def List.toByteArray.loop :

List UInt8 → ByteArray → ByteArray

Equations

List.toByteArray.loop [] _fun_discr = _fun_discr
List.toByteArray.loop (b :: bs) _fun_discr = List.toByteArray.loop bs (ByteArray.push _fun_discr b)

source

instance instToStringByteArray :

ToString ByteArray

Equations

instToStringByteArray = { toString := fun bs => List.toString (ByteArray.toList bs) }

source

def ByteArray.toUInt64LE! (bs : ByteArray) :

UInt64

Equations

ByteArray.toUInt64LE! bs = if (ByteArray.size bs == 8) = true then UInt8.toUInt64 (ByteArray.get! bs 0) <<< 56 ||| UInt8.toUInt64 (ByteArray.get! bs 1) <<< 48 ||| UInt8.toUInt64 (ByteArray.get! bs 2) <<< 40 ||| UInt8.toUInt64 (ByteArray.get! bs 3) <<< 32 ||| UInt8.toUInt64 (ByteArray.get! bs 4) <<< 24 ||| UInt8.toUInt64 (ByteArray.get! bs 5) <<< 16 ||| UInt8.toUInt64 (ByteArray.get! bs 6) <<< 8 ||| UInt8.toUInt64 (ByteArray.get! bs 7) else panicWithPosWithDecl "Init.Data.ByteArray.Basic" "ByteArray.toUInt64LE!" 191 2 ("assertion violation: " ++ "bs.size == 8\n ")

Interpret a ByteArray of size 8 as a little-endian UInt64.

source

def ByteArray.toUInt64BE! (bs : ByteArray) :

UInt64

Equations

ByteArray.toUInt64BE! bs = if (ByteArray.size bs == 8) = true then UInt8.toUInt64 (ByteArray.get! bs 7) <<< 56 ||| UInt8.toUInt64 (ByteArray.get! bs 6) <<< 48 ||| UInt8.toUInt64 (ByteArray.get! bs 5) <<< 40 ||| UInt8.toUInt64 (ByteArray.get! bs 4) <<< 32 ||| UInt8.toUInt64 (ByteArray.get! bs 3) <<< 24 ||| UInt8.toUInt64 (ByteArray.get! bs 2) <<< 16 ||| UInt8.toUInt64 (ByteArray.get! bs 1) <<< 8 ||| UInt8.toUInt64 (ByteArray.get! bs 0) else panicWithPosWithDecl "Init.Data.ByteArray.Basic" "ByteArray.toUInt64BE!" 203 2 ("assertion violation: " ++ "bs.size == 8\n ")

Interpret a ByteArray of size 8 as a big-endian UInt64.