Documentation

Batteries.Data.ByteArray

source
instance ByteArray.instDecidableEq_batteries :
DecidableEq ByteArray
Equations
    source
    theorem ByteArray.getElem_eq_data_getElem {i : Nat} (a : ByteArray) (h : i < a.size) :
    a[i] = a.data[i]

    uget/uset #

    source
    @[simp]
    theorem ByteArray.uset_eq_set (a : ByteArray) {i : USize} (h : i.toNat < a.size) (v : UInt8) :
    a.uset i v h = a.set i.toNat v h

    empty #

    source
    @[simp]
    theorem ByteArray.data_mkEmpty (cap : Nat) :
    (emptyWithCapacity cap).data = #[]
    source
    @[simp]
    theorem ByteArray.data_empty :
    empty.data = #[]
    source
    @[simp]
    theorem ByteArray.size_empty :
    empty.size = 0

    push #

    source
    @[simp]
    theorem ByteArray.data_push (a : ByteArray) (b : UInt8) :
    (a.push b).data = a.data.push b
    source
    @[simp]
    theorem ByteArray.size_push (a : ByteArray) (b : UInt8) :
    (a.push b).size = a.size + 1
    source
    @[simp]
    theorem ByteArray.get_push_eq (a : ByteArray) (x : UInt8) :
    (a.push x)[a.size] = x
    source
    theorem ByteArray.get_push_lt (a : ByteArray) (x : UInt8) (i : Nat) (h : i < a.size) :
    (a.push x)[i] = a[i]

    set #

    source
    @[simp]
    theorem ByteArray.data_set (a : ByteArray) (i : Fin a.size) (v : UInt8) :
    (a.set (↑i) v ⋯).data = a.data.set (↑i) v ⋯
    source
    @[simp]
    theorem ByteArray.size_set (a : ByteArray) (i : Fin a.size) (v : UInt8) :
    (a.set (↑i) v ⋯).size = a.size
    source
    @[simp]
    theorem ByteArray.get_set_eq (a : ByteArray) (i : Fin a.size) (v : UInt8) :
    (a.set (↑i) v ⋯)[↑i] = v
    source
    theorem ByteArray.get_set_ne {j : Nat} (a : ByteArray) (i : Fin a.size) (v : UInt8) (hj : j < a.size) (h : ↑i ≠ j) :
    (a.set (↑i) v ⋯)[j] = a[j]
    source
    theorem ByteArray.set_set (a : ByteArray) (i : Fin a.size) (v v' : UInt8) :
    (a.set (↑i) v ⋯).set (↑i) v' ⋯ = a.set (↑i) v' ⋯

    copySlice #

    source
    @[simp]
    theorem ByteArray.data_copySlice (a : ByteArray) (i : Nat) (b : ByteArray) (j len : Nat) (exact : Bool) :
    (a.copySlice i b j len exact).data = b.data.extract 0 j ++ a.data.extract i (i + len) ++ b.data.extract (j + min len (a.data.size - i))

    append #

    source
    @[simp]
    theorem ByteArray.append_eq (a b : ByteArray) :
    a.append b = a ++ b
    source
    @[simp]
    theorem ByteArray.data_append (a b : ByteArray) :
    (a ++ b).data = a.data ++ b.data
    source
    theorem ByteArray.size_append (a b : ByteArray) :
    (a ++ b).size = a.size + b.size
    source
    theorem ByteArray.get_append_left {i : Nat} {a b : ByteArray} (hlt : i < a.size) (h : i < (a ++ b).size := ⋯) :
    (a ++ b)[i] = a[i]
    source
    theorem ByteArray.get_append_right {i : Nat} {a b : ByteArray} (hle : a.size ≤ i) (h : i < (a ++ b).size) (h' : i - a.size < b.size := ⋯) :
    (a ++ b)[i] = b[i - a.size]

    extract #

    source
    @[simp]
    theorem ByteArray.data_extract (a : ByteArray) (start stop : Nat) :
    (a.extract start stop).data = a.data.extract start stop
    source
    @[simp]
    theorem ByteArray.size_extract (a : ByteArray) (start stop : Nat) :
    (a.extract start stop).size = min stop a.size - start
    source
    theorem ByteArray.get_extract_aux {i : Nat} {a : ByteArray} {start stop : Nat} (h : i < (a.extract start stop).size) :
    start + i < a.size
    source
    @[simp]
    theorem ByteArray.get_extract {i : Nat} {a : ByteArray} {start stop : Nat} (h : i < (a.extract start stop).size) :
    (a.extract start stop)[i] = a[start + i]

    ofFn #

    source
    @[inline]
    def ByteArray.ofFn {n : Nat} (f : Fin n → UInt8) :
    ByteArray
    • ofFn f with f : Fin n → UInt8 returns the byte array whose ith element is f i. -
    Equations
      Instances For
        source
        @[simp]
        theorem ByteArray.ofFn_zero (f : Fin 0 → UInt8) :
        ofFn f = empty
        source
        theorem ByteArray.ofFn_succ {n : Nat} (f : Fin (n + 1) → UInt8) :
        ofFn f = (ofFn fun (i : Fin n) => f i.castSucc).push (f (Fin.last n))
        source
        @[simp]
        theorem ByteArray.data_ofFn {n : Nat} (f : Fin n → UInt8) :
        (ofFn f).data = Array.ofFn f
        source
        @[simp]
        theorem ByteArray.size_ofFn {n : Nat} (f : Fin n → UInt8) :
        (ofFn f).size = n
        source
        @[simp]
        theorem ByteArray.get_ofFn {n : Nat} (f : Fin n → UInt8) (i : Fin (ofFn f).size) :
        (ofFn f).get ↑i ⋯ = f (Fin.cast ⋯ i)
        source
        @[simp]
        theorem ByteArray.getElem_ofFn {n : Nat} (f : Fin n → UInt8) (i : Nat) (h : i < (ofFn f).size) :
        (ofFn f)[i] = f ⟨i, ⋯⟩

        map/mapM #

        source
        @[inline]
        unsafe def ByteArray.mapMUnsafe {m : Type → Type u_1} [Monad m] (a : ByteArray) (f : UInt8 → m UInt8) :
        m ByteArray

        Unsafe optimized implementation of mapM.

        This function is unsafe because it relies on the implementation limit that the size of an array is always less than USize.size.

        Equations
          Instances For
            source
            @[specialize #[]]
            unsafe def ByteArray.mapMUnsafe.loop {m : Type → Type u_1} [Monad m] (f : UInt8 → m UInt8) (a : ByteArray) (k s : USize) :
            m ByteArray

            Inner loop for mapMUnsafe.

            Equations
              Instances For
                source
                @[implemented_by ByteArray.mapMUnsafe]
                def ByteArray.mapM {m : Type → Type u_1} [Monad m] (a : ByteArray) (f : UInt8 → m UInt8) :
                m ByteArray

                mapM f a applies the monadic function f to each element of the array.

                Equations
                  Instances For
                    source
                    @[inline]
                    def ByteArray.map (a : ByteArray) (f : UInt8 → UInt8) :
                    ByteArray

                    map f a applies the function f to each element of the array.

                    Equations
                      Instances For