------------------------------------------------------------------------
-- The Agda standard library
--
-- Bytestrings: simple types and functions
-- Note that these functions do not perform bound checks.
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible #-}

module Data.Bytestring.Base where

open import Agda.Builtin.String using (String)
open import Data.Nat.Base using (ℕ; _+_; _*_; _^_)
import Data.Fin.Base as Fin
open import Data.Vec.Base as Vec using (Vec)
open import Data.Word8.Base as Word8 using (Word8)
open import Data.Word64.Base as Word64 using (Word64)
open import Function.Base using (const; _$_)

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

open import Data.Bytestring.Primitive as Prim public
  using ( Bytestring
        ; length
        ; take
        ; drop
        ; show
        )
  renaming (index to getWord8)

------------------------------------------------------------------------------
-- Operations

slice : Word64 → Word64 → Bytestring → Bytestring
slice start chunk buf = take chunk (drop start buf)

------------------------------------------------------------------------------
-- Generic combinators for fixed-size encodings

getWord8s : (n : ℕ) → Bytestring → Word64 → Vec Word8 n
getWord8s n buf idx
  = let idx = Word64.toℕ idx in
  Vec.map (λ k → getWord8 buf (Word64.fromℕ (idx + Fin.toℕ k)))
  $ Vec.allFin n

-- Little endian representation:
-- Low place values first
fromWord8sLE : ∀ {n w} {W : Set w} → (fromℕ : ℕ → W) → Vec Word8 n → W
fromWord8sLE f ws = f (Vec.foldr′ (λ w acc → Word8.toℕ w + acc * ( ^ ))  ws)

-- Big endian representation
-- Big place values first
fromWord8sBE : ∀ {n w} {W : Set w} → (fromℕ : ℕ → W) → Vec Word8 n → W
fromWord8sBE f ws = f (Vec.foldl′ (λ acc w → acc * ( ^ ) + Word8.toℕ w)  ws)

------------------------------------------------------------------------------
-- Decoding to a vector of bytes

toWord8s : (b : Bytestring) → Vec Word8 (length b)
toWord8s b = getWord8s _ b (Word64.fromℕ )

------------------------------------------------------------------------------
-- Getting Word64

getWord64LE : Bytestring → Word64 → Word64
getWord64LE buf idx
  = fromWord8sLE Word64.fromℕ (getWord8s  buf idx)

getWord64BE : Bytestring → Word64 → Word64
getWord64BE buf idx
  = fromWord8sBE Word64.fromℕ (getWord8s  buf idx)