[ new ] Bytestrings and builders

Author: gallais

CHANGELOG.md

@@ -184,6 +184,16 @@ New modules
   Data.Word8.Literals
   ```
 
+* Bytestrings and builders:
+  ```agda
+  Data.Bytestring.Base
+  Data.Bytestring.Builder.Base
+  Data.Bytestring.Builder.Primitive
+  Data.Bytestring.IO
+  Data.Bytestring.IO.Primitive
+  Data.Bytestring.Primitive
+  ```
+
 Additions to existing modules
 -----------------------------
 

GenerateEverything.hs

@@ -44,6 +44,12 @@ unsafeModules = map modToFile
   , "Codata.Musical.Covec"
   , "Codata.Musical.Conversion"
   , "Codata.Musical.Stream"
+  , "Data.Bytestring.Base"
+  , "Data.Bytestring.Builder.Base"
+  , "Data.Bytestring.Builder.Primitive"
+  , "Data.Bytestring.IO"
+  , "Data.Bytestring.IO.Primitive"
+  , "Data.Bytestring.Primitive"
   , "Debug.Trace"
   , "Effect.Monad.IO"
   , "Effect.Monad.IO.Instances"

src/Data/Bytestring/Base.agda

@@ -0,0 +1,66 @@
+------------------------------------------------------------------------
+-- 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 Data.Nat.Base using (ℕ; _+_; _*_; _^_)
+open import Agda.Builtin.String using (String)
+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
+        )
+  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 * (2 ^ 8)) 0 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 * (2 ^ 8) + Word8.toℕ w) 0 ws)
+
+------------------------------------------------------------------------------
+-- Getting Word64
+
+getWord64LE : Bytestring → Word64 → Word64
+getWord64LE buf idx
+  = fromWord8sLE Word64.fromℕ (getWord8s 8 buf idx)
+
+getWord64BE : Bytestring → Word64 → Word64
+getWord64BE buf idx
+  = fromWord8sBE Word64.fromℕ (getWord8s 8 buf idx)

src/Data/Bytestring/Builder/Base.agda

@@ -0,0 +1,72 @@
+------------------------------------------------------------------------
+-- 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)

src/Data/Bytestring/Builder/Primitive.agda

@@ -0,0 +1,38 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Primitive Bytestrings: builder type and functions
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible #-}
+
+module Data.Bytestring.Builder.Primitive where
+
+open import Agda.Builtin.Nat
+open import Agda.Builtin.String
+
+open import Data.Word8.Primitive
+open import Data.Bytestring.Primitive using (Bytestring)
+
+infixr 6 _<>_
+
+postulate
+  -- Builder and execution
+  Builder : Set
+  toBytestring : Builder → Bytestring
+
+  -- Assembling a builder
+  bytestring : Bytestring → Builder
+  word8 : Word8 → Builder
+  empty : Builder
+  _<>_ : Builder → Builder → Builder
+
+{-# FOREIGN GHC import qualified Data.ByteString.Builder as Builder #-}
+{-# FOREIGN GHC import qualified Data.ByteString.Lazy as Lazy #-}
+{-# FOREIGN GHC import qualified Data.Text as T #-}
+{-# COMPILE GHC Builder = type Builder.Builder #-}
+{-# COMPILE GHC toBytestring = Lazy.toStrict . Builder.toLazyByteString #-}
+{-# COMPILE GHC bytestring = Builder.byteString #-}
+{-# COMPILE GHC word8 = Builder.word8 #-}
+{-# COMPILE GHC empty = mempty #-}
+{-# COMPILE GHC _<>_ = mappend #-}

src/Data/Bytestring/IO.agda

@@ -0,0 +1,22 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Bytestrings: IO operations
+------------------------------------------------------------------------
+
+{-# OPTIONS --guardedness --cubical-compatible #-}
+
+module Data.Bytestring.IO where
+
+open import Agda.Builtin.String
+open import IO using (IO; lift)
+open import Data.Bytestring.Base using (Bytestring)
+open import Data.Unit.Base using (⊤)
+
+import Data.Bytestring.IO.Primitive as Prim
+
+readFile : String → IO Bytestring
+readFile fp = lift (Prim.readFile fp)
+
+writeFile : String → Bytestring → IO ⊤
+writeFile fp str = lift (Prim.writeFile fp str)

src/Data/Bytestring/IO/Primitive.agda

@@ -0,0 +1,24 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Primitive Bytestrings: IO operations
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible #-}
+
+module Data.Bytestring.IO.Primitive where
+
+open import Agda.Builtin.String using (String)
+open import Agda.Builtin.Unit using (⊤)
+open import IO.Primitive.Core using (IO)
+
+open import Data.Bytestring.Primitive
+
+postulate
+  readFile : String → IO Bytestring
+  writeFile : String → Bytestring → IO ⊤
+
+{-# FOREIGN GHC import qualified Data.Text as T #-}
+{-# FOREIGN GHC import Data.ByteString #-}
+{-# COMPILE GHC readFile = Data.ByteString.readFile . T.unpack #-}
+{-# COMPILE GHC writeFile = Data.ByteString.writeFile . T.unpack #-}

src/Data/Bytestring/Primitive.agda

@@ -0,0 +1,39 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Primitive bytestrings: simple bindings to Haskell types and functions
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible #-}
+
+module Data.Bytestring.Primitive where
+
+open import Agda.Builtin.Nat
+open import Agda.Builtin.Word
+open import Data.Word8.Primitive
+
+-- NB: the bytestring package uses `Int` as the indexing type which
+-- Haskell's base specifies as:
+--
+-- > A fixed-precision integer type with at least the range
+-- > [-2^29 .. 2^29-1]. The exact range for a given implementation
+-- > can be determined by using minBound and maxBound from the
+-- > Bounded class.
+--
+-- There is no ergonomic way to encode that in a type-safe manner.
+-- For now we use `Word64` with the understanding that using indices
+-- greater than 2^29-1 may lead to undefined behaviours...
+
+postulate
+  Bytestring : Set
+  index : Bytestring → Word64 → Word8
+  length : Bytestring → Nat
+  take : Word64 → Bytestring → Bytestring
+  drop : Word64 → Bytestring → Bytestring
+
+{-# FOREIGN GHC import qualified Data.ByteString as B #-}
+{-# COMPILE GHC Bytestring = type B.ByteString #-}
+{-# COMPILE GHC index = \ buf idx -> B.index buf (fromIntegral idx) #-}
+{-# COMPILE GHC length = \ buf -> fromIntegral (B.length buf) #-}
+{-# COMPILE GHC take = B.take . fromIntegral #-}
+{-# COMPILE GHC drop = B.drop . fromIntegral #-}

src/Data/Word64/Base.agda

@@ -9,8 +9,9 @@
 module Data.Word64.Base where
 
 open import Level using (zero)
-import Data.Nat.Base as ℕ
-open import Function.Base using (_on_)
+open import Algebra.Core using (Op₂)
+open import Data.Nat.Base as ℕ using (ℕ)
+open import Function.Base using (_on_; _∘₂′_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
@@ -24,6 +25,9 @@ open import Agda.Builtin.Word public
   ; primWord64FromNat to fromℕ
   )
 
+liftOp₂ : Op₂ ℕ → Op₂ Word64
+liftOp₂ op = fromℕ ∘₂′ op on toℕ
+
 infix 4 _≈_
 _≈_ : Rel Word64 zero
 _≈_ = _≡_ on toℕ