[ new ] Word8, Bytestring, Bytestring builder

CHANGELOG.md

@@ -30,6 +30,8 @@ Non-backwards compatible changes
 * The definitions in `Algebra.Module.Morphism.Construct.Identity` are now
   parametrized by _raw_ bundles, and as such take a proof of reflexivity.
 * The module `IO.Primitive` was moved to `IO.Primitive.Core`.
+* The modules in the `Data.Word` hierarchy were moved to the `Data.Word64`
+  one instead.
 
 Other major improvements
 ------------------------
@@ -75,6 +77,16 @@ Deprecated names
   untilRight  ↦  untilInj₂
   ```
 
+* In `Data.Float.Base`:
+  ```agda
+  toWord ↦ toWord64
+  ```
+
+* In `Data.Float.Properties`:
+  ```agda
+  toWord-injective ↦ toWord64-injective
+  ```
+
 New modules
 -----------
 
@@ -165,6 +177,23 @@ New modules
   Data.Vec.Bounded.Show
   ```
 
+* A type of bytes:
+  ```agda
+  Data.Word8.Primitive
+  Data.Word8.Base
+  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"
@@ -161,6 +167,9 @@ sizedTypesModules = map modToFile
   , "Codata.Sized.Thunk"
   , "Data.Container.Fixpoints.Sized"
   , "Data.W.Sized"
+  , "Data.Word8.Base"
+  , "Data.Word8.Literals"
+  , "Data.Word8.Primitive"
   , "Data.Nat.PseudoRandom.LCG.Unsafe"
   , "Data.Tree.Binary.Show"
   , "Data.Tree.Rose"

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/Float/Base.agda

@@ -9,7 +9,7 @@
 module Data.Float.Base where
 
 open import Data.Bool.Base using (T)
-import Data.Word.Base as Word
+import Data.Word64.Base as Word64
 import Data.Maybe.Base as Maybe
 open import Function.Base using (_on_; _∘_)
 open import Agda.Builtin.Equality
@@ -30,7 +30,7 @@ open import Agda.Builtin.Float public
   ; primFloatIsNegativeZero    to isNegativeZero
   ; primFloatIsSafeInteger     to isSafeInteger
   -- Conversions
-  ; primFloatToWord64          to toWord
+  ; primFloatToWord64          to toWord64
   ; primNatToFloat             to fromℕ
   ; primIntToFloat             to fromℤ
   ; primFloatRound             to round
@@ -69,9 +69,19 @@ open import Agda.Builtin.Float public
 infix 4 _≈_
 
 _≈_ : Rel Float _
-_≈_ = _≡_ on Maybe.map Word.toℕ ∘ toWord
+_≈_ = _≡_ on Maybe.map Word64.toℕ ∘ toWord64
 
 
 infix 4 _≤_
 _≤_ : Rel Float _
 x ≤ y = T (x ≤ᵇ y)
+
+
+------------------------------------------------------------------------
+-- DEPRECATIONS
+
+toWord = toWord64
+{-# WARNING_ON_USAGE toWord
+"Warning: toWord was deprecated in v2.1.
+Please use toWord64 instead."
+#-}