Lean 语言参考手册

20.17. 字节数组🔗

字节数组是一种专门化的数组类型，只能包含类型为 UInt8 的元素。 由于这一限制，它们可以采用高效得多的表示，不需要指针间接访问。 与其他数组一样，字节数组在编译后的代码中表示为 动态数组，Lean 运行时还会专门优化其数组操作。 修改字节数组的操作会先检查该数组的 引用计数；如果没有其他引用指向该数组，就会原地修改它。

字节数组没有字面量语法。 可以使用 List.toByteArray 从列表字面量构造字节数组。

🔗结构体
ByteArray : Type
ByteArray : Type

ByteArray 类似于 Array UInt8，但具有高效的运行时表示，即紧凑存储的字节缓冲区。

构造子

ByteArray.mk

将字节数组打包为 ByteArray。

在 Array 与 ByteArray 之间转换需要线性时间。

字段

data : Array UInt8

字节数组中包含的数据。

在 Array 与 ByteArray 之间转换需要线性时间。

20.17.1. 接口参考🔗

20.17.1.1. 构造字节数组🔗

🔗定义
ByteArray.empty : ByteArray
ByteArray.empty : ByteArray

构造初始容量为 0 的新空字节数组。

使用 ByteArray.emptyWithCapacity 可创建初始容量更大的数组。

🔗定义
ByteArray.emptyWithCapacity (c : Nat) : ByteArray
ByteArray.emptyWithCapacity (c : Nat) :
  ByteArray

构造初始容量为 c 的新空字节数组。

🔗定义
ByteArray.append (a b : ByteArray) : ByteArray
ByteArray.append (a b : ByteArray) :
  ByteArray

拼接两个字节数组。

在编译后的代码中，对 ByteArray.append 的调用会被替换为效率高得多的 ByteArray.fastAppend。

🔗定义
ByteArray.fastAppend (a b : ByteArray) : ByteArray
ByteArray.fastAppend (a b : ByteArray) :
  ByteArray

使用快速数组原语拼接两个字节数组，而不是先转换为列表再转回数组。

在编译后的代码中，此函数会替换对 ByteArray.append 的调用。

🔗定义
ByteArray.copySlice (src : ByteArray) (srcOff : Nat) (dest : ByteArray)
  (destOff len : Nat) (exact : Bool := true) : ByteArray
ByteArray.copySlice (src : ByteArray)
  (srcOff : Nat) (dest : ByteArray)
  (destOff len : Nat)
  (exact : Bool := true) : ByteArray

将位于 [srcOff, srcOff + len) 的切片从 src 复制到 [destOff, destOff + len) 在 dest 中对应的位置；必要时扩展 dest。如果 exact 为 false，扩展时容量会加倍。

20.17.1.2. 大小🔗

🔗定义
ByteArray.size : ByteArray → Nat
ByteArray.size : ByteArray → Nat

返回字节数组中的字节数。

这是数组中实际包含的字节数，不同于容量；容量是当前为数组分配的内存量。

🔗定义
ByteArray.usize (a : ByteArray) : USize
ByteArray.usize (a : ByteArray) : USize

以平台相关的定宽整数形式获取数组大小。

由于 USize 足以寻址 Lean 所支持的每个平台上的全部内存，实际不会有元素数量超出 ByteArray 所用 USize 计数范围的实例。

🔗定义
ByteArray.isEmpty (s : ByteArray) : Bool
ByteArray.isEmpty (s : ByteArray) : Bool

如果结果为 true，则 s 包含零个字节。

20.17.1.3. 查找🔗

🔗定义
ByteArray.get (a : ByteArray) (i : Nat)
  (h : i < a.size := by get_elem_tactic) : UInt8
ByteArray.get (a : ByteArray) (i : Nat)
  (h : i < a.size := by get_elem_tactic) :
  UInt8

获取指定索引处的字节。调用者必须证明索引未越界。

可使用 uget 作为更高效的替代方案；也可使用 get!，它在索引越界时触发 panic。

🔗定义
ByteArray.uget (a : ByteArray) (i : USize)
  (h : i.toNat < a.size := by get_elem_tactic) : UInt8
ByteArray.uget (a : ByteArray) (i : USize)
  (h : i.toNat < a.size := by
    get_elem_tactic) :
  UInt8

获取指定索引处的字节。调用者必须证明索引未越界。索引用平台相关的定宽整数表示（32 位或 64 位）。

由于 USize 足以寻址 Lean 所支持的每个平台上的全部内存，实际不会存在其所有元素无法由某个 ByteArray 的 uget 获取的情况。

🔗定义
ByteArray.get! : ByteArray → Nat → UInt8
ByteArray.get! : ByteArray → Nat → UInt8

获取指定索引处的字节。如果索引越界，则触发 panic。

🔗定义
ByteArray.extract (a : ByteArray) (b e : Nat) : ByteArray
ByteArray.extract (a : ByteArray)
  (b e : Nat) : ByteArray

将索引从 b（含）到 e（不含）的字节复制到新的 ByteArray。

20.17.1.4. 转换🔗

🔗定义
ByteArray.toList (bs : ByteArray) : List UInt8
ByteArray.toList (bs : ByteArray) :
  List UInt8

将紧凑存储的字节数组转换为链表。

🔗定义
ByteArray.toUInt64BE! (bs : ByteArray) : UInt64
ByteArray.toUInt64BE! (bs : ByteArray) :
  UInt64

将大小为 8 的 ByteArray 解释为大端序 UInt64。

如果数组大小不是 8，则触发 panic。

🔗定义
ByteArray.toUInt64LE! (bs : ByteArray) : UInt64
ByteArray.toUInt64LE! (bs : ByteArray) :
  UInt64

将大小为 8 的 ByteArray 解释为小端序 UInt64。

如果数组大小不是 8，则触发 panic。

20.17.1.4.1. UTF-8🔗

🔗定义
ByteArray.utf8Decode? (b : ByteArray) : Option (Array Char)
ByteArray.utf8Decode? (b : ByteArray) :
  Option (Array Char)

从 UTF-8 表示中解码字符序列。如果这些字节不构成 Unicode 标量值序列，则返回 none。

🔗定义
ByteArray.utf8DecodeChar? (bytes : ByteArray) (i : Nat) : Option Char
ByteArray.utf8DecodeChar?
  (bytes : ByteArray) (i : Nat) :
  Option Char

解码并返回 Char，其 UTF-8 编码从 i 开始，位于 bytes 中。

如果结果为 none，则 i 不是某个字符的有效 UTF-8 编码起点。

🔗定义
ByteArray.utf8DecodeChar (bytes : ByteArray) (i : Nat)
  (h : (bytes.utf8DecodeChar? i).isSome = true) : Char
ByteArray.utf8DecodeChar
  (bytes : ByteArray) (i : Nat)
  (h :
    (bytes.utf8DecodeChar? i).isSome =
      true) :
  Char

解码并返回 Char，其 UTF-8 编码从 i 开始，位于 bytes 中。

此函数要求证明存在有效的 Char，且它确实位于 i。utf8DecodeChar? 是另一种选择：它返回 Option Char，而不要求预先提供证明。

20.17.1.5. 修改🔗

🔗定义
ByteArray.push : ByteArray → UInt8 → ByteArray
ByteArray.push :
  ByteArray → UInt8 → ByteArray

在数组末尾添加一个元素。所得数组的大小比输入数组大一。如果该数组没有其他引用，则会原地修改。

此操作的摊还时间复杂度为 O(1)，因为 ByteArray 以动态数组表示。

🔗定义
ByteArray.set (a : ByteArray) (i : Nat) :
  UInt8 → (h : autoParam (i < a.size) ByteArray.set._auto_1) → ByteArray
ByteArray.set (a : ByteArray) (i : Nat) :
  UInt8 →
    (h :
        autoParam (i < a.size)
          ByteArray.set._auto_1) →
      ByteArray

替换给定索引处的字节。

此函数不执行边界检查，但要求提供索引未越界的证明。通常可以省略该证明，系统会自动合成。

如果数组没有其他引用，则会原地修改。

🔗定义
ByteArray.uset (a : ByteArray) (i : USize) :
  UInt8 →
    (h : autoParam (i.toNat < a.size) ByteArray.uset._auto_1) →
      ByteArray
ByteArray.uset (a : ByteArray)
  (i : USize) :
  UInt8 →
    (h :
        autoParam (i.toNat < a.size)
          ByteArray.uset._auto_1) →
      ByteArray

替换给定索引处的字节。

此函数不执行边界检查，但要求提供索引未越界的证明。通常可以省略该证明，系统会自动合成。

如果数组没有其他引用，则会原地修改。

🔗定义
ByteArray.set! : ByteArray → Nat → UInt8 → ByteArray
ByteArray.set! :
  ByteArray → Nat → UInt8 → ByteArray

替换给定索引处的字节。

如果数组没有其他引用，则会原地修改。

如果索引越界，则原样返回数组。

20.17.1.6. 迭代🔗

🔗定义
ByteArray.foldl.{v} {β : Type v} (f : β → UInt8 → β) (init : β)
  (as : ByteArray) (start : Nat := 0) (stop : Nat := as.size) : β
ByteArray.foldl.{v} {β : Type v}
  (f : β → UInt8 → β) (init : β)
  (as : ByteArray) (start : Nat := 0)
  (stop : Nat := as.size) : β

对 ByteArray 执行左折叠：按索引从小到大遍历数组，并计算一个累积值。

数组的每个元素都通过函数 f 与此前元素得到的值合并。初始值 init 是处理任何元素之前的起始值。

ByteArray.foldlM 是此函数的单子版本。

🔗定义
ByteArray.foldlM.{v, w} {β : Type v} {m : Type v → Type w} [Monad m]
  (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start : Nat := 0)
  (stop : Nat := as.size) : m β
ByteArray.foldlM.{v, w} {β : Type v}
  {m : Type v → Type w} [Monad m]
  (f : β → UInt8 → m β) (init : β)
  (as : ByteArray) (start : Nat := 0)
  (stop : Nat := as.size) : m β

对 ByteArray 执行单子左折叠：按索引从小到大遍历数组，并计算一个累积值。

数组的每个元素都通过单子函数 f 与此前元素得到的值合并。初始值 init 是处理任何元素之前的起始值。

🔗定义
ByteArray.forIn.{v, w} {β : Type v} {m : Type v → Type w} [Monad m]
  (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) : m β
ByteArray.forIn.{v, w} {β : Type v}
  {m : Type v → Type w} [Monad m]
  (as : ByteArray) (b : β)
  (f : UInt8 → β → m (ForInStep β)) : m β

这是 ForIn.forIn 针对 ByteArray 的参考实现。

在编译后的代码中，它会被更高效的 ByteArray.forInUnsafe 替换。

20.17.1.7. 迭代器🔗

🔗定义
ByteArray.iter (arr : ByteArray) : ByteArray.Iterator
ByteArray.iter (arr : ByteArray) :
  ByteArray.Iterator

创建位于数组开头的迭代器。

🔗结构体
ByteArray.Iterator : Type
ByteArray.Iterator : Type

遍历字节（UInt8）的迭代器，其对象是一个 ByteArray。

通常通过 arr.iter 创建，其中 arr 是一个 ByteArray。

如果位置 i 对数组 arr 有效，即 0 ≤ i ≤ arr.size，则称迭代器有效。

如果迭代器无效，大多数迭代器操作都会返回任意值。ByteArray.Iterator API 中的函数应当排除无效迭代器的产生，但有两个例外：

  • Iterator.next iter 会无效，如果 iter 已位于数组末尾，即 iter.atEnd 为 true

  • Iterator.forward iter n/Iterator.nextn iter n 会无效，如果 n 严格大于剩余字节数

构造子

ByteArray.Iterator.mk

字段

array : ByteArray

迭代器所针对的数组。

idx : Nat

当前位置。

此位置对数组而言不一定有效，例如在 Iterator.atEnd 为真时仍持续调用 Iterator.next。若位置无效，则当前字节为 (default : UInt8)。

🔗定义
ByteArray.Iterator.pos (self : ByteArray.Iterator) : Nat
ByteArray.Iterator.pos
  (self : ByteArray.Iterator) : Nat

当前位置。

此位置对数组而言不一定有效，例如持续调用 Iterator.next，即使 Iterator.atEnd 已为真。若位置无效，则当前字节为 (default : UInt8)。

🔗定义
ByteArray.Iterator.atEnd : ByteArray.Iterator → Bool
ByteArray.Iterator.atEnd :
  ByteArray.Iterator → Bool

如果迭代器已经越过数组的最后一个字节，则为真。

🔗定义
ByteArray.Iterator.hasNext : ByteArray.Iterator → Bool
ByteArray.Iterator.hasNext :
  ByteArray.Iterator → Bool

如果迭代器有效，即尚未越过数组的最后一个字节，则为真。

🔗定义
ByteArray.Iterator.hasPrev : ByteArray.Iterator → Bool
ByteArray.Iterator.hasPrev :
  ByteArray.Iterator → Bool

如果位置不为零，则为真。

🔗定义
ByteArray.Iterator.curr : ByteArray.Iterator → UInt8
ByteArray.Iterator.curr :
  ByteArray.Iterator → UInt8

当前位置的字节。

位置无效时返回 (default : UInt8)。

🔗定义
ByteArray.Iterator.curr' (it : ByteArray.Iterator)
  (h : it.hasNext = true) : UInt8
ByteArray.Iterator.curr'
  (it : ByteArray.Iterator)
  (h : it.hasNext = true) : UInt8

当前位置的字节。-

🔗定义
ByteArray.Iterator.next : ByteArray.Iterator → ByteArray.Iterator
ByteArray.Iterator.next :
  ByteArray.Iterator → ByteArray.Iterator

无条件将迭代器的位置向前移动一个字节。

只有当迭代器不在数组末尾时，调用此函数才有效，即 Iterator.atEnd 为 false；否则所得迭代器将无效。

🔗定义
ByteArray.Iterator.next' (it : ByteArray.Iterator)
  (_h : it.hasNext = true) : ByteArray.Iterator
ByteArray.Iterator.next'
  (it : ByteArray.Iterator)
  (_h : it.hasNext = true) :
  ByteArray.Iterator

将迭代器的位置向前移动一个字节。-

🔗定义
ByteArray.Iterator.forward :
  ByteArray.Iterator → Nat → ByteArray.Iterator
ByteArray.Iterator.forward :
  ByteArray.Iterator →
    Nat → ByteArray.Iterator

将迭代器的位置向前移动若干字节。

仅当要跳过的字节数小于或等于迭代器中的剩余字节数时，所得迭代器才有效。

🔗定义
ByteArray.Iterator.nextn : ByteArray.Iterator → Nat → ByteArray.Iterator
ByteArray.Iterator.nextn :
  ByteArray.Iterator →
    Nat → ByteArray.Iterator

将迭代器的位置向前移动若干字节。

仅当要跳过的字节数小于或等于迭代器中的剩余字节数时，所得迭代器才有效。

🔗定义
ByteArray.Iterator.prev : ByteArray.Iterator → ByteArray.Iterator
ByteArray.Iterator.prev :
  ByteArray.Iterator → ByteArray.Iterator

减小迭代器的位置。

如果位置为零，则此函数不改变迭代器。

🔗定义
ByteArray.Iterator.prevn : ByteArray.Iterator → Nat → ByteArray.Iterator
ByteArray.Iterator.prevn :
  ByteArray.Iterator →
    Nat → ByteArray.Iterator

将迭代器的位置向后移动若干字节。

如果要求后退的字节数多于可用字节数，则停在数组开头。

🔗定义
ByteArray.Iterator.remainingBytes : ByteArray.Iterator → Nat
ByteArray.Iterator.remainingBytes :
  ByteArray.Iterator → Nat

迭代器中剩余的字节数。

🔗定义
ByteArray.Iterator.toEnd : ByteArray.Iterator → ByteArray.Iterator
ByteArray.Iterator.toEnd :
  ByteArray.Iterator → ByteArray.Iterator

将迭代器的位置移至数组末尾。

给定 i : ByteArray.Iterator，请注意 i.toEnd.atEnd 始终为 true。

20.17.1.8. 切片🔗

🔗定义
ByteArray.toByteSlice (as : ByteArray) (start : Nat := 0)
  (stop : Nat := as.size) : ByteSlice
ByteArray.toByteSlice (as : ByteArray)
  (start : Nat := 0)
  (stop : Nat := as.size) : ByteSlice

返回字节数组中具有给定边界的字节切片。

如果 start 或 stop 不是字节切片的有效边界，则将其限制在字节数组大小以内。此外，起始索引会被限制为不超过结束索引。

🔗定义
ByteSlice : Type
ByteSlice : Type

某个底层字节数组的一段区域。

字节切片包含一个字节数组，以及感兴趣区域的起始和结束索引。字节切片既能避免复制或分配空间，又比手动追踪边界更方便。感兴趣区域由所有大于或等于 start 且严格小于 stop 的索引组成。

🔗定义
ByteSlice.beq (a b : ByteSlice) : Bool
ByteSlice.beq (a b : ByteSlice) : Bool

比较函数

🔗定义
ByteSlice.byteArray (xs : ByteSlice) : ByteArray
ByteSlice.byteArray (xs : ByteSlice) :
  ByteArray

底层字节数组。

🔗定义
ByteSlice.contains (s : ByteSlice) (byte : UInt8) : Bool
ByteSlice.contains (s : ByteSlice)
  (byte : UInt8) : Bool

检查字节切片是否包含指定的字节值。

如果切片中任一字节等于给定值，则返回 true，否则返回 false。

🔗定义
ByteSlice.empty : ByteSlice
ByteSlice.empty : ByteSlice

空字节切片。

此空字节切片以空字节数组为底层存储。

🔗定义
ByteSlice.foldr.{v} {β : Type v} (f : UInt8 → β → β) (init : β)
  (as : ByteSlice) : β
ByteSlice.foldr.{v} {β : Type v}
  (f : UInt8 → β → β) (init : β)
  (as : ByteSlice) : β

从右向左对字节切片中的字节执行折叠操作。

构造类型为 β 的累加器：从 init 开始，从末尾移向开头，依次将字节切片中的每个字节与当前累加器值合并。

示例：

🔗定义
ByteSlice.foldrM.{v, w} {β : Type v} {m : Type v → Type w} [Monad m]
  (f : UInt8 → β → m β) (init : β) (as : ByteSlice) : m β
ByteSlice.foldrM.{v, w} {β : Type v}
  {m : Type v → Type w} [Monad m]
  (f : UInt8 → β → m β) (init : β)
  (as : ByteSlice) : m β

从右向左对字节切片中的字节执行单子折叠操作。

构造类型为 β 的累加器：从 init 开始，从末尾移向开头，依次以单子方式将字节切片中的每个字节与当前累加器值合并。所用单子可以允许提前终止或重复。

示例：

#eval (ByteArray.mk #[1, 2, 3]).toByteSlice.foldrM (init := 0) fun x acc =>
  some x.toNat + acc
some 6
🔗定义
ByteSlice.forM.{v, w} {m : Type v → Type w} [Monad m]
  (f : UInt8 → m PUnit) (as : ByteSlice) : m PUnit
ByteSlice.forM.{v, w}
  {m : Type v → Type w} [Monad m]
  (f : UInt8 → m PUnit) (as : ByteSlice) :
  m PUnit

对字节切片中的每个字节执行单子动作。

从最小索引开始，按索引递增的顺序处理字节。

🔗定义
ByteSlice.get (s : ByteSlice) (i : Fin s.size) : UInt8
ByteSlice.get (s : ByteSlice)
  (i : Fin s.size) : UInt8

从字节切片中取出一个字节。

索引相对于字节切片的起点，而非底层字节数组。

🔗定义
ByteSlice.get! (s : ByteSlice) (i : Nat) : UInt8
ByteSlice.get! (s : ByteSlice) (i : Nat) :
  UInt8

从字节切片中取出一个字节；索引越界时返回默认值。

索引相对于字节切片的起点和终点，而非底层字节数组。默认值为 0。

🔗定义
ByteSlice.getD (s : ByteSlice) (i : Nat) (v₀ : UInt8) : UInt8
ByteSlice.getD (s : ByteSlice) (i : Nat)
  (v₀ : UInt8) : UInt8

从字节切片中取出一个字节；索引越界时返回默认值 v₀。

索引相对于字节切片的起点和终点，而非底层字节数组。

🔗定义
ByteSlice.ofByteArray (ba : ByteArray) : ByteSlice
ByteSlice.ofByteArray (ba : ByteArray) :
  ByteSlice

从 ByteArray 创建新的 ByteSlice

🔗定义
ByteSlice.size (s : ByteSlice) : Nat
ByteSlice.size (s : ByteSlice) : Nat

计算字节切片的大小。

🔗定义
ByteSlice.slice (s : ByteSlice) (start : Nat := 0)
  (stop : Nat := s.size) : ByteSlice
ByteSlice.slice (s : ByteSlice)
  (start : Nat := 0)
  (stop : Nat := s.size) : ByteSlice

以给定边界创建字节切片的子切片。

如果 start 或 stop 不是子切片的有效边界，则将其限制在切片大小以内。此外，起始索引会被限制为不超过结束索引。

索引相对于当前切片，而非底层字节数组。

🔗定义
ByteSlice.start (xs : ByteSlice) : Nat
ByteSlice.start (xs : ByteSlice) : Nat

感兴趣区域的起始索引（含）。

🔗定义
ByteSlice.stop (xs : ByteSlice) : Nat
ByteSlice.stop (xs : ByteSlice) : Nat

感兴趣区域的结束索引（不含）。

🔗定义
ByteSlice.toByteArray (s : ByteSlice) : ByteArray
ByteSlice.toByteArray (s : ByteSlice) :
  ByteArray

复制相关部分，将字节切片转换回字节数组。

20.17.1.9. 元素判定🔗

🔗定义
ByteArray.findIdx? (a : ByteArray) (p : UInt8 → Bool)
  (start : Nat := 0) : Option Nat
ByteArray.findIdx? (a : ByteArray)
  (p : UInt8 → Bool) (start : Nat := 0) :
  Option Nat

查找 a 中第一个使 p 返回 true 的字节的索引。如果 a 中没有字节满足 p，则结果为 none。

变体 findFinIdx? 还会返回“找到的索引未越界”的证明。

🔗定义
ByteArray.findFinIdx? (a : ByteArray) (p : UInt8 → Bool)
  (start : Nat := 0) : Option (Fin a.size)
ByteArray.findFinIdx? (a : ByteArray)
  (p : UInt8 → Bool) (start : Nat := 0) :
  Option (Fin a.size)

查找 a 中第一个使 p 返回 true 的字节的索引。如果 a 中没有字节满足 p，则结果为 none。

返回索引时还会附带它是数组中有效索引的证明。