------------------------------------------------------------------------
-- 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)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4