[ new ] Word8, Bytestring, Bytestring builder (#2376)

* [ admin ] deprecate Word -> Word64

* [ new ] a type of bytes

* [ new ] Bytestrings and builders

* [ test ] for bytestrings, builders, word conversion, show, etc.

* [ ci ] bump ghc & cabal numbers

* [ fix ] actually set the bits ya weapon

* [ ci ] bump options to match makefile

* [ ci ] more heap

* [ more ] add hexadecimal show functions too

Author: gallais

.github/workflows/ci-ubuntu.yml

@@ -47,11 +47,11 @@ on:
 ########################################################################
 
 env:
-  GHC_VERSION: 8.10.7
-  CABAL_VERSION: 3.6.2.0
+  GHC_VERSION: 9.8.2
+  CABAL_VERSION: 3.10.3.0
   CABAL_INSTALL: cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS'
   # CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
-  AGDA: agda -Werror +RTS -M3.5G -H3.5G -A128M -RTS -i. -isrc -idoc
+  AGDA: agda -Werror +RTS -M5G -H3.5G -A128M -RTS -i. -isrc -idoc
 
 jobs:
   test-stdlib:

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
 ------------------------
@@ -107,6 +109,16 @@ Deprecated names
   untilRight  ↦  untilInj₂
   ```
 
+* In `Data.Float.Base`:
+  ```agda
+  toWord ↦ toWord64
+  ```
+
+* In `Data.Float.Properties`:
+  ```agda
+  toWord-injective ↦ toWord64-injective
+  ```
+
 New modules
 -----------
 
@@ -231,6 +243,31 @@ New modules
   Data.Vec.Bounded.Show
   ```
 
+* Word64 literals and bit-based functions:
+  ```agda
+  Data.Word64.Literals
+  Data.Word64.Unsafe
+  Data.Word64.Show
+  ```
+
+* A type of bytes:
+  ```agda
+  Data.Word8.Primitive
+  Data.Word8.Base
+  Data.Word8.Literals
+  Data.Word8.Show
+  ```
+
+* 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
+  ```
+
 * Decidability for the subset relation on lists:
   ```agda
   Data.List.Relation.Binary.Subset.DecSetoid (_⊆?_)
@@ -402,6 +439,11 @@ Additions to existing modules
     *-cancelʳ-nonZero : AlmostRightCancellative 0# *
   ```
 
+* In `Data.Bool.Show`:
+  ```agda
+  showBit : Bool → Char
+  ```
+
 * In `Data.Container.Indexed.Core`:
   ```agda
   Subtrees o c = (r : Response c) → X (next c r)
@@ -711,9 +753,10 @@ Additions to existing modules
   _>>_ : IO A → IO B → IO B
   ```
 
-* In `Data.Word.Base`:
+* In `Data.Word64.Base`:
   ```agda
   _≤_ : Rel Word64 zero
+  show : Word64 → String
   ```
 
 * Added new definition in `Relation.Binary.Construct.Closure.Transitive`

GenerateEverything.hs

@@ -44,6 +44,18 @@ 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"
+  , "Data.Word8.Base"
+  , "Data.Word8.Literals"
+  , "Data.Word8.Primitive"
+  , "Data.Word64.Primitive"
+  , "Data.Word8.Show"
+  , "Data.Word64.Show"
   , "Debug.Trace"
   , "Effect.Monad.IO"
   , "Effect.Monad.IO.Instances"

src/Data/Bool/Show.agda

@@ -9,8 +9,13 @@
 module Data.Bool.Show where
 
 open import Data.Bool.Base using (Bool; false; true)
+open import Data.Char.Base using (Char)
 open import Data.String.Base using (String)
 
 show : Bool → String
 show true  = "true"
 show false = "false"
+
+showBit : Bool → Char
+showBit true = '1'
+showBit false = '0'

src/Data/Bytestring/Base.agda

@@ -0,0 +1,73 @@
+------------------------------------------------------------------------
+-- 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
+        ; 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 * (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)
+
+------------------------------------------------------------------------------
+-- Decoding to a vector of bytes
+
+toWord8s : (b : Bytestring) → Vec Word8 (length b)
+toWord8s b = getWord8s _ b (Word64.fromℕ 0)
+
+------------------------------------------------------------------------------
+-- 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 #-}