@[extern lean_mk_empty_byte_array]
Equations
- ByteArray.mkEmpty c = { data := #[] }
Equations
- ByteArray.instInhabitedByteArray = { default := ByteArray.empty }
Equations
- ByteArray.instEmptyCollectionByteArray = { emptyCollection := ByteArray.empty }
@[extern lean_byte_array_push]
Equations
- ByteArray.push x x = match x, x with | { data := bs }, b => { data := Array.push bs b }
@[extern lean_byte_array_size]
Equations
- ByteArray.size x = match x with | { data := bs } => Array.size bs
@[extern lean_byte_array_uget]
Equations
- ByteArray.uget x x x = match x, x, x with | { data := bs }, i, h => Array.uget bs i h
@[extern lean_byte_array_get]
Equations
- ByteArray.get! x x = match x, x with | { data := bs }, i => Array.get! bs i
@[extern lean_byte_array_fget]
Equations
- ByteArray.get x x = match x, x with | { data := bs }, i => Array.get bs i
@[inline]
Equations
- ByteArray.getOp self idx = ByteArray.get! self idx
@[extern lean_byte_array_set]
Equations
- ByteArray.set! x x x = match x, x, x with | { data := bs }, i, b => { data := Array.set! bs i b }
@[extern lean_byte_array_fset]
Equations
- ByteArray.set x x x = match x, x, x with | { data := bs }, i, b => { data := Array.set bs i b }
@[extern lean_byte_array_uset]
def
ByteArray.uset
(a : ByteArray)
(i : USize)
:
(a : UInt8) → USize.toNat i < ByteArray.size a → ByteArray
Equations
- ByteArray.uset x x x x = match x, x, x, x with | { data := bs }, i, v, h => { data := Array.uset bs i v h }
Equations
- ByteArray.isEmpty s = (ByteArray.size s == 0)
@[extern lean_byte_array_copy_slice]
def
ByteArray.copySlice
(src : ByteArray)
(srcOff : Nat)
(dest : ByteArray)
(destOff : Nat)
(len : Nat)
(exact : optParam Bool true)
:
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) }
Equations
- ByteArray.extract a b e = ByteArray.copySlice a b ByteArray.empty 0 (e - b)
Equations
- ByteArray.append a b = ByteArray.copySlice b 0 a (ByteArray.size a) (ByteArray.size b) false
Equations
- ByteArray.instAppendByteArray = { append := ByteArray.append }
Equations
- ByteArray.toList bs = (fun loop => loop 0 []) (ByteArray.toList.loop bs)
@[inline]
Equations
- ByteArray.findIdx? a p start = (fun loop => loop start) (ByteArray.findIdx?.loop a p)
@[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); (fun loop => loop 0 b) (ByteArray.forInUnsafe.loop as f sz)
@[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
@[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 = (fun loop => loop (ByteArray.size as) (_ : ByteArray.size as ≤ ByteArray.size as) b) (ByteArray.forIn.loop as f)
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)
@[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 = (fun fold => if start < stop then if stop ≤ ByteArray.size as then fold (USize.ofNat start) (USize.ofNat stop) init else pure init else pure init) (ByteArray.foldlMUnsafe.fold f as)
@[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
@[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 => (fun loop => loop (stop - start) start init) (ByteArray.foldlM.loop f as stop h); if h : stop ≤ ByteArray.size as then fold stop h else fold (ByteArray.size as) (_ : ByteArray.size as ≤ ByteArray.size as)
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
@[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)
Equations
- List.toByteArray bs = (fun loop => loop bs ByteArray.empty) List.toByteArray.loop
Equations
- List.toByteArray.loop [] x = x
- List.toByteArray.loop (b :: bs) x = List.toByteArray.loop bs (ByteArray.push x b)
Equations
- instToStringByteArray = { toString := fun bs => List.toString (ByteArray.toList bs) }
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 ")
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 ")