{-# OPTIONS --cubical-compatible #-}
module Data.Bytestring.Builder.Base where
open import Data.Nat.Base using (ℕ; zero; suc; _/_; _%_; _^_)
open import Data.Word8.Base as Word8 using (Word8)
open import Data.Word64.Base as Word64 using (Word64)
open import Function.Base using (_∘′_)
open import Data.Bytestring.Builder.Primitive as Prim public
using ( Builder
; toBytestring
; bytestring
; word8
; empty
; _<>_
)
module List where
open import Data.List.Base as List using (List)
concat : List Builder → Builder
concat = List.foldr _<>_ empty
module Vec where
open import Data.Vec.Base as Vec using (Vec)
concat : ∀ {n} → Vec Builder n → Builder
concat = Vec.foldr′ _<>_ empty
open Vec
open import Data.Vec.Base as Vec using (Vec; []; _∷_)
wordN : ∀ {n} → Vec Word8 n → Builder
wordN = concat ∘′ Vec.map word8
toWord8sLE : ∀ {w} {W : Set w} (n : ℕ) (toℕ : W → ℕ) → W → Vec Word8 n
toWord8sLE n toℕ w = loop (toℕ w) n where
loop : ℕ → (n : ℕ) → Vec Word8 n
loop acc 0 = []
loop acc 1 = Word8.fromℕ acc ∷ []
loop acc (suc n) = Word8.fromℕ (acc % 2 ^ 8) ∷ loop (acc / 2 ^ 8) n
toWord8sBE : ∀ {w} {W : Set w} (n : ℕ) (toℕ : W → ℕ) → W → Vec Word8 n
toWord8sBE n toℕ w = Vec.reverse (toWord8sLE n toℕ w)
word64LE : Word64 → Builder
word64LE w = wordN (toWord8sLE 8 Word64.toℕ w)
word64BE : Word64 → Builder
word64BE w = wordN (toWord8sBE 8 Word64.toℕ w)