------------------------------------------------------------------------
-- The Agda standard library
--
-- Bytestrings: builder type and functions
------------------------------------------------------------------------

{-# 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 (_∘′_)

------------------------------------------------------------------------------
-- Re-export type and operations

open import Data.Bytestring.Builder.Primitive as Prim public
  using ( Builder
        ; toBytestring
        ; bytestring
        ; word8
        ; empty
        ; _<>_
        )

------------------------------------------------------------------------------
-- High-level combinators

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

------------------------------------------------------------------------------
-- Generic word-specific combinators

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)

------------------------------------------------------------------------------
-- Builders for Word64

word64LE : Word64 → Builder
word64LE w = wordN (toWord8sLE 8 Word64.toℕ w)

word64BE : Word64 → Builder
word64BE w = wordN (toWord8sBE 8 Word64.toℕ w)