[ new ] a type of bytes

Author: gallais

CHANGELOG.md

@@ -177,6 +177,13 @@ New modules
   Data.Vec.Bounded.Show
   ```
 
+* A type of bytes:
+  ```agda
+  Data.Word8.Primitive
+  Data.Word8.Base
+  Data.Word8.Literals
+  ```
+
 Additions to existing modules
 -----------------------------
 

GenerateEverything.hs

@@ -161,6 +161,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/Word8/Base.agda

@@ -0,0 +1,30 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Bytes: base type and functions
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible #-}
+
+module Data.Word8.Base where
+
+open import Agda.Builtin.Bool using (Bool)
+open import Agda.Builtin.Nat using (Nat; _==_)
+open import Agda.Builtin.String using (String)
+open import Agda.Builtin.Unit using (⊤)
+
+------------------------------------------------------------------------------
+-- Re-export type and operations
+
+open import Data.Word8.Primitive as Prim public
+  using ( Word8
+        ; _+_)
+  renaming ( fromNat to fromℕ
+           ; toNat to toℕ
+           )
+
+------------------------------------------------------------------------------
+-- Basic functions
+
+_≡ᵇ_ : Word8 → Word8 → Bool
+w ≡ᵇ w′ = toℕ w == toℕ w′

src/Data/Word8/Literals.agda

@@ -0,0 +1,19 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Byte Literals
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible #-}
+
+module Data.Word8.Literals where
+
+open import Agda.Builtin.FromNat using (Number)
+open import Data.Unit.Base using (⊤)
+open import Data.Word8.Base using (Word8; fromℕ)
+
+number : Number Word8
+number = record
+  { Constraint = λ _ → ⊤
+  ; fromNat    = λ w → fromℕ w
+  }

src/Data/Word8/Primitive.agda

@@ -0,0 +1,24 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Bytes: simple bindings to Haskell types and functions
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible #-}
+
+module Data.Word8.Primitive where
+
+open import Agda.Builtin.Nat using (Nat)
+
+postulate
+  Word8 : Set
+  fromNat : Nat → Word8
+  toNat : Word8 → Nat
+  _+_ : Word8 → Word8 → Word8
+
+{-# FOREIGN GHC import GHC.Word #-}
+
+{-# COMPILE GHC Word8 = type Word8 #-}
+{-# COMPILE GHC fromNat = fromIntegral #-}
+{-# COMPILE GHC toNat = fromIntegral #-}
+{-# COMPILE GHC _+_ = (+) #-}