diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index ec9ae5c501..5086e96696 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.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: diff --git a/CHANGELOG.md b/CHANGELOG.md index 9f8d6de9bd..a243edfd5f 100644 --- a/CHANGELOG.md +++ b/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` diff --git a/GenerateEverything.hs b/GenerateEverything.hs index d7895f96db..801c1b7e35 100644 --- a/GenerateEverything.hs +++ b/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" diff --git a/src/Data/Bool/Show.agda b/src/Data/Bool/Show.agda index 21f2ec1a55..075efaa63b 100644 --- a/src/Data/Bool/Show.agda +++ b/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' diff --git a/src/Data/Bytestring/Base.agda b/src/Data/Bytestring/Base.agda new file mode 100644 index 0000000000..69bdb23db4 --- /dev/null +++ b/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) diff --git a/src/Data/Bytestring/Builder/Base.agda b/src/Data/Bytestring/Builder/Base.agda new file mode 100644 index 0000000000..728ceb3896 --- /dev/null +++ b/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) diff --git a/src/Data/Bytestring/Builder/Primitive.agda b/src/Data/Bytestring/Builder/Primitive.agda new file mode 100644 index 0000000000..b9f2bd8937 --- /dev/null +++ b/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 #-} diff --git a/src/Data/Bytestring/IO.agda b/src/Data/Bytestring/IO.agda new file mode 100644 index 0000000000..e79bc2c8a6 --- /dev/null +++ b/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) diff --git a/src/Data/Bytestring/IO/Primitive.agda b/src/Data/Bytestring/IO/Primitive.agda new file mode 100644 index 0000000000..113ef19e86 --- /dev/null +++ b/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 #-} diff --git a/src/Data/Bytestring/Primitive.agda b/src/Data/Bytestring/Primitive.agda new file mode 100644 index 0000000000..94e0d64b2c --- /dev/null +++ b/src/Data/Bytestring/Primitive.agda @@ -0,0 +1,44 @@ +------------------------------------------------------------------------ +-- 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 using (Nat) +open import Agda.Builtin.String using (String) +open import Agda.Builtin.Word using (Word64) +open import Data.Word8.Primitive using (Word8) + +-- 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 + show : Bytestring → String + +{-# FOREIGN GHC import qualified Data.ByteString as B #-} +{-# FOREIGN GHC import qualified Data.Text as T #-} + +{-# 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 #-} +{-# COMPILE GHC show = T.pack . Prelude.show #-} diff --git a/src/Data/Float/Base.agda b/src/Data/Float/Base.agda index fdc7dab2db..a991c119a9 100644 --- a/src/Data/Float/Base.agda +++ b/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." +#-} diff --git a/src/Data/Float/Properties.agda b/src/Data/Float/Properties.agda index fab340ea0e..6975804193 100644 --- a/src/Data/Float/Properties.agda +++ b/src/Data/Float/Properties.agda @@ -13,8 +13,8 @@ open import Data.Float.Base import Data.Maybe.Base as Maybe import Data.Maybe.Properties as Maybe import Data.Nat.Properties as ℕ -import Data.Word.Base as Word -import Data.Word.Properties as Word +import Data.Word64.Base as Word64 +import Data.Word64.Properties as Word64 open import Function.Base using (_∘_) open import Relation.Nullary.Decidable as RN using (map′) open import Relation.Binary.Core using (_⇒_) @@ -33,17 +33,17 @@ open import Relation.Binary.PropositionalEquality.Properties -- Primitive properties open import Agda.Builtin.Float.Properties - renaming (primFloatToWord64Injective to toWord-injective) + renaming (primFloatToWord64Injective to toWord64-injective) public ------------------------------------------------------------------------ -- Properties of _≈_ ≈⇒≡ : _≈_ ⇒ _≡_ -≈⇒≡ eq = toWord-injective _ _ (Maybe.map-injective Word.≈⇒≡ eq) +≈⇒≡ eq = toWord64-injective _ _ (Maybe.map-injective Word64.≈⇒≡ eq) ≈-reflexive : _≡_ ⇒ _≈_ -≈-reflexive eq = cong (Maybe.map Word.toℕ ∘ toWord) eq +≈-reflexive eq = cong (Maybe.map Word64.toℕ ∘ toWord64) eq ≈-refl : Reflexive _≈_ ≈-refl = refl @@ -59,7 +59,7 @@ open import Agda.Builtin.Float.Properties infix 4 _≈?_ _≈?_ : Decidable _≈_ -_≈?_ = On.decidable (Maybe.map Word.toℕ ∘ toWord) _≡_ (Maybe.≡-dec ℕ._≟_) +_≈?_ = On.decidable (Maybe.map Word64.toℕ ∘ toWord64) _≡_ (Maybe.≡-dec ℕ._≟_) ≈-isEquivalence : IsEquivalence _≈_ ≈-isEquivalence = record @@ -95,3 +95,13 @@ x ≟ y = map′ ≈⇒≡ ≈-reflexive (x ≈? y) ≡-decSetoid : DecSetoid _ _ ≡-decSetoid = decSetoid _≟_ + + +------------------------------------------------------------------------ +-- DEPRECATIONS + +toWord-injective = toWord64-injective +{-# WARNING_ON_USAGE toWord-injective +"Warning: toWord-injective was deprecated in v2.1. +Please use toWord64-injective instead." +#-} diff --git a/src/Data/Word.agda b/src/Data/Word.agda index 8c07cac9c7..df6594641c 100644 --- a/src/Data/Word.agda +++ b/src/Data/Word.agda @@ -1,15 +1,15 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Machine words +-- This module is DEPRECATED. Please use Data.Word64 instead ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Data.Word where ------------------------------------------------------------------------- --- Re-export base definitions and decidability of equality +open import Data.Word64 public -open import Data.Word.Base public -open import Data.Word.Properties using (_≈?_; _ B.testBit w . fromIntegral #-} +{-# COMPILE GHC setBit = \ w -> B.setBit w . fromIntegral #-} +{-# COMPILE GHC clearBit = \ w -> B.clearBit w . fromIntegral #-} +{-# COMPILE GHC show = T.pack . Prelude.show #-} diff --git a/src/Data/Word64/Properties.agda b/src/Data/Word64/Properties.agda new file mode 100644 index 0000000000..0f5b4d8fe5 --- /dev/null +++ b/src/Data/Word64/Properties.agda @@ -0,0 +1,108 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of operations on machine words +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.Word64.Properties where + +import Data.Nat.Base as ℕ +open import Data.Bool.Base using (Bool) +open import Data.Word64.Base using (_≈_; toℕ; Word64; _<_) +import Data.Nat.Properties as ℕ +open import Relation.Nullary.Decidable.Core using (map′; ⌊_⌋) +open import Relation.Binary + using ( _⇒_; Reflexive; Symmetric; Transitive; Substitutive + ; Decidable; DecidableEquality; IsEquivalence; IsDecEquivalence + ; Setoid; DecSetoid; StrictTotalOrder) +import Relation.Binary.Construct.On as On +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong; sym; trans; subst) +open import Relation.Binary.PropositionalEquality.Properties + using (setoid; decSetoid) + +------------------------------------------------------------------------ +-- Primitive properties + +open import Agda.Builtin.Word.Properties + renaming (primWord64ToNatInjective to toℕ-injective) + public + +------------------------------------------------------------------------ +-- Properties of _≈_ + +≈⇒≡ : _≈_ ⇒ _≡_ +≈⇒≡ = toℕ-injective _ _ + +≈-reflexive : _≡_ ⇒ _≈_ +≈-reflexive = cong toℕ + +≈-refl : Reflexive _≈_ +≈-refl = refl + +≈-sym : Symmetric _≈_ +≈-sym = sym + +≈-trans : Transitive _≈_ +≈-trans = trans + +≈-subst : ∀ {ℓ} → Substitutive _≈_ ℓ +≈-subst P x≈y p = subst P (≈⇒≡ x≈y) p + +infix 4 _≈?_ +_≈?_ : Decidable _≈_ +x ≈? y = toℕ x ℕ.≟ toℕ y + +≈-isEquivalence : IsEquivalence _≈_ +≈-isEquivalence = record + { refl = λ {i} → ≈-refl {i} + ; sym = λ {i j} → ≈-sym {i} {j} + ; trans = λ {i j k} → ≈-trans {i} {j} {k} + } + +≈-setoid : Setoid _ _ +≈-setoid = record + { isEquivalence = ≈-isEquivalence + } + +≈-isDecEquivalence : IsDecEquivalence _≈_ +≈-isDecEquivalence = record + { isEquivalence = ≈-isEquivalence + ; _≟_ = _≈?_ + } + +≈-decSetoid : DecSetoid _ _ +≈-decSetoid = record + { isDecEquivalence = ≈-isDecEquivalence + } +------------------------------------------------------------------------ +-- Properties of _≡_ + +infix 4 _≟_ +_≟_ : DecidableEquality Word64 +x ≟ y = map′ ≈⇒≡ ≈-reflexive (x ≈? y) + +≡-setoid : Setoid _ _ +≡-setoid = setoid Word64 + +≡-decSetoid : DecSetoid _ _ +≡-decSetoid = decSetoid _≟_ + +------------------------------------------------------------------------ +-- Boolean equality test. + +infix 4 _==_ +_==_ : Word64 → Word64 → Bool +w₁ == w₂ = ⌊ w₁ ≟ w₂ ⌋ + +------------------------------------------------------------------------ +-- Properties of _<_ + +infix 4 __) + +------------------------------------------------------------------------ +-- Re-export primitives publicly + +open import Data.Word64.Primitive as Prim public + using ( show ) + +testBit : Word64 → Fin 64 → Bool +testBit w i = Prim.testBit w (Fin.toℕ i) + +_[_]≔_ : Word64 → Fin 64 → Bool → Word64 +w [ i ]≔ false = Prim.clearBit w (Fin.toℕ i) +w [ i ]≔ true = Prim.setBit w (Fin.toℕ i) + +------------------------------------------------------------------------ +-- Convert to its components + +toBits : Word64 → Vec Bool 64 +toBits w = Vec.tabulate (testBit w) + +fromBits : Vec Bool 64 → Word64 +fromBits bs = Vec.foldl′ _|>_ (fromℕ 0) + $ Vec.zipWith (λ i b → _[ i ]≔ b) (Vec.allFin 64) bs + +toWord64s : Word64 → Vec Word8 8 +toWord64s w = + let ws = proj₁ (Vec.group 8 8 (toBits w)) in + Vec.map Word8.fromBits ws diff --git a/src/Data/Word8/Base.agda b/src/Data/Word8/Base.agda new file mode 100644 index 0000000000..142b544d78 --- /dev/null +++ b/src/Data/Word8/Base.agda @@ -0,0 +1,51 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Bytes: base type and functions +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible #-} + +module Data.Word8.Base where + +open import Agda.Builtin.Bool using (Bool; true; false) +open import Agda.Builtin.Char using (Char) +open import Agda.Builtin.Nat using (Nat; _==_) +open import Agda.Builtin.Unit using (⊤) + +open import Data.Fin.Base as Fin using (Fin) +open import Data.Vec.Base as Vec using (Vec; []; _∷_) + +open import Function.Base using (_$_; _|>_) + +------------------------------------------------------------------------------ +-- Re-export type and operations + +open import Data.Word8.Primitive as Prim public + using ( Word8 + ; _+_ + ; show + ) + renaming ( fromNat to fromℕ + ; toNat to toℕ + ) + +testBit : Word8 → Fin 8 → Bool +testBit w i = Prim.testBit w (Fin.toℕ i) + +_[_]≔_ : Word8 → Fin 8 → Bool → Word8 +w [ i ]≔ false = Prim.clearBit w (Fin.toℕ i) +w [ i ]≔ true = Prim.setBit w (Fin.toℕ i) + +------------------------------------------------------------------------------ +-- Basic functions + +toBits : Word8 → Vec Bool 8 +toBits w = Vec.tabulate (testBit w) + +fromBits : Vec Bool 8 → Word8 +fromBits bs = Vec.foldl′ _|>_ (fromℕ 0) + $ Vec.zipWith (λ i b → _[ i ]≔ b) (Vec.allFin 8) bs + +_≡ᵇ_ : Word8 → Word8 → Bool +w ≡ᵇ w′ = toℕ w == toℕ w′ diff --git a/src/Data/Word8/Literals.agda b/src/Data/Word8/Literals.agda new file mode 100644 index 0000000000..acc608f899 --- /dev/null +++ b/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 + } diff --git a/src/Data/Word8/Primitive.agda b/src/Data/Word8/Primitive.agda new file mode 100644 index 0000000000..e0d2ac87c7 --- /dev/null +++ b/src/Data/Word8/Primitive.agda @@ -0,0 +1,36 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Bytes: simple bindings to Haskell types and functions +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible #-} + +module Data.Word8.Primitive where + +open import Agda.Builtin.Bool using (Bool) +open import Agda.Builtin.Nat using (Nat) +open import Agda.Builtin.String using (String) + +postulate + Word8 : Set + testBit : Word8 → Nat → Bool + setBit : Word8 → Nat → Word8 + clearBit : Word8 → Nat → Word8 + fromNat : Nat → Word8 + toNat : Word8 → Nat + _+_ : Word8 → Word8 → Word8 + show : Word8 → String + +{-# FOREIGN GHC import GHC.Word #-} +{-# FOREIGN GHC import qualified Data.Bits as B #-} +{-# FOREIGN GHC import qualified Data.Text as T #-} + +{-# COMPILE GHC Word8 = type Word8 #-} +{-# COMPILE GHC testBit = \ w -> B.testBit w . fromIntegral #-} +{-# COMPILE GHC setBit = \ w -> B.setBit w . fromIntegral #-} +{-# COMPILE GHC clearBit = \ w -> B.clearBit w . fromIntegral #-} +{-# COMPILE GHC fromNat = fromIntegral #-} +{-# COMPILE GHC toNat = fromIntegral #-} +{-# COMPILE GHC _+_ = (+) #-} +{-# COMPILE GHC show = T.pack . Prelude.show #-} diff --git a/src/Data/Word8/Show.agda b/src/Data/Word8/Show.agda new file mode 100644 index 0000000000..0cc5b5d7b5 --- /dev/null +++ b/src/Data/Word8/Show.agda @@ -0,0 +1,33 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Bytes: showing bit patterns +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible #-} + +module Data.Word8.Show where + +open import Agda.Builtin.String using (String) + +open import Data.Bool.Show using (showBit) +open import Data.Fin.Base as Fin using (Fin) +import Data.Nat.Show as ℕ +open import Data.String using (_++_; fromVec; padLeft) +open import Data.Vec.Base as Vec using (Vec; []; _∷_) +open import Data.Word8.Base +open import Function.Base using (_$_) + +showBits : Word8 → String +showBits w + = "0b" ++_ + $ fromVec + $ Vec.reverse + $ Vec.map showBit + $ toBits w + +showHexa : Word8 → String +showHexa w + = "0x" ++_ + $ padLeft '0' 2 + $ ℕ.showInBase 16 (toℕ w) diff --git a/src/Reflection/AST/Literal.agda b/src/Reflection/AST/Literal.agda index abdd2b08a6..540e150169 100644 --- a/src/Reflection/AST/Literal.agda +++ b/src/Reflection/AST/Literal.agda @@ -13,7 +13,7 @@ import Data.Char.Properties as Char import Data.Float.Properties as Float import Data.Nat.Properties as ℕ import Data.String.Properties as String -import Data.Word.Properties as Word +import Data.Word64.Properties as Word64 import Reflection.AST.Meta as Meta import Reflection.AST.Name as Name open import Relation.Nullary.Decidable.Core using (yes; no; map′; isYes) @@ -60,7 +60,7 @@ nat x ≟ char x₁ = no (λ ()) nat x ≟ string x₁ = no (λ ()) nat x ≟ name x₁ = no (λ ()) nat x ≟ meta x₁ = no (λ ()) -word64 x ≟ word64 x₁ = map′ (cong word64) word64-injective (x Word.≟ x₁) +word64 x ≟ word64 x₁ = map′ (cong word64) word64-injective (x Word64.≟ x₁) word64 x ≟ nat x₁ = no (λ ()) word64 x ≟ float x₁ = no (λ ()) word64 x ≟ char x₁ = no (λ ()) diff --git a/src/Reflection/AST/Name.agda b/src/Reflection/AST/Name.agda index c386912f08..5ceb025126 100644 --- a/src/Reflection/AST/Name.agda +++ b/src/Reflection/AST/Name.agda @@ -10,7 +10,7 @@ module Reflection.AST.Name where open import Data.List.Base using (List) import Data.Product.Properties as Prodₚ using (≡-dec) -import Data.Word.Properties as Wₚ using (_≟_) +import Data.Word64.Properties as Wₚ using (_≟_) open import Function.Base using (_on_) open import Relation.Nullary.Decidable.Core using (map′) open import Relation.Binary.Core using (Rel) diff --git a/src/Reflection/AST/Show.agda b/src/Reflection/AST/Show.agda index 5d748e089b..a9de9a2993 100644 --- a/src/Reflection/AST/Show.agda +++ b/src/Reflection/AST/Show.agda @@ -18,7 +18,7 @@ import Data.Nat.Show as ℕ open import Data.String.Base as String using (String; _++_; intersperse; braces; parens; _<+>_) open import Data.String as String using (parensIfSpace) open import Data.Product.Base using (_×_; _,_) -import Data.Word.Base as Word +import Data.Word64.Base as Word64 open import Function.Base using (id; _∘′_; case_of_) open import Relation.Nullary.Decidable.Core using (yes; no) @@ -60,7 +60,7 @@ showVisibility instance′ = "instance" showLiteral : Literal → String showLiteral (nat x) = ℕ.show x -showLiteral (word64 x) = ℕ.show (Word.toℕ x) +showLiteral (word64 x) = ℕ.show (Word64.toℕ x) showLiteral (float x) = Float.show x showLiteral (char x) = Char.show x showLiteral (string x) = String.show x diff --git a/src/System/Directory/Primitive.agda b/src/System/Directory/Primitive.agda index 57da7461bb..d5bae96742 100644 --- a/src/System/Directory/Primitive.agda +++ b/src/System/Directory/Primitive.agda @@ -21,12 +21,12 @@ open import System.FilePath.Posix.Primitive {-# FOREIGN GHC import Data.Text #-} data XdgDirectory : Set where - XdgData XdgConfig XdgCache : XdgDirectory + XdgData XdgConfig XdgCache XdgState : XdgDirectory data XdgDirectoryList : Set where XdgDataDirs XdgConfigDirs : XdgDirectoryList -{-# COMPILE GHC XdgDirectory = data XdgDirectory (XdgData|XdgConfig|XdgCache) #-} +{-# COMPILE GHC XdgDirectory = data XdgDirectory (XdgData|XdgConfig|XdgCache|XdgState) #-} {-# COMPILE GHC XdgDirectoryList = data XdgDirectoryList (XdgDataDirs|XdgConfigDirs) #-} private diff --git a/src/System/Random.agda b/src/System/Random.agda index fa327939d6..3587a0b927 100644 --- a/src/System/Random.agda +++ b/src/System/Random.agda @@ -89,7 +89,7 @@ module ℕ where module Word64 where - open import Data.Word.Base using (Word64; _≤_) + open import Data.Word64.Base using (Word64; _≤_) randomIO : IO Word64 randomIO = lift Prim.randomIO-Word64 diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda index 80cc7ec6d4..6fea3dd1e0 100644 --- a/src/Tactic/Cong.agda +++ b/src/Tactic/Cong.agda @@ -35,7 +35,7 @@ open import Data.List.Base as List using ([]; _∷_) open import Data.Maybe.Base as Maybe using (Maybe; just; nothing) open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _≡ᵇ_; _+_) open import Data.Unit.Base using (⊤) -open import Data.Word.Base as Word using (toℕ) +open import Data.Word64.Base as Word64 using (toℕ) open import Data.Product.Base using (_×_; map₁; _,_) open import Function using (flip; case_of_) diff --git a/tests/data/bytestring/Main.agda b/tests/data/bytestring/Main.agda new file mode 100644 index 0000000000..85721598da --- /dev/null +++ b/tests/data/bytestring/Main.agda @@ -0,0 +1,66 @@ +{-# OPTIONS --guardedness #-} + +module Main where + +open import Agda.Builtin.FromNat + +open import Data.Bytestring.Base as Bytestring +open import Data.Bytestring.Builder.Base +open import Data.List.Base using ([]; _∷_) +import Data.Nat.Literals; instance numberNat = Data.Nat.Literals.number +open import Data.Product.Base using (_×_; _,_) +open import Data.String using (String; _++_; fromVec) +open import Data.Unit.Base using (⊤; tt) +import Data.Vec.Base as Vec +open import Data.Word8.Base as Word8 +import Data.Word8.Show as Word8 +import Data.Word8.Literals; instance numberWord8 = Data.Word8.Literals.number +open import Data.Word64.Base as Word64 using (Word64) +import Data.Word64.Unsafe as Word64 +import Data.Word64.Show as Word64 +import Data.Word64.Literals; instance numberWord64 = Data.Word64.Literals.number + +open import Function.Base using (_$_) + +open import IO.Base +open import IO.Finite + +1⋯3 : Bytestring +1⋯3 = toBytestring + $ List.concat + $ word8 1 + ∷ word64LE 2 + ∷ word64BE 3 + ∷ [] + +1,⋯,3 : Word8 × Word64 × Word64 +1,⋯,3 = getWord8 1⋯3 0 + , getWord64LE 1⋯3 1 + , getWord64BE 1⋯3 9 + +main : Main +main = run $ do + let separation = fromVec (Vec.replicate 72 '-') + putStrLn (Bytestring.show 1⋯3) + putStrLn separation + let (one , two , three) = 1,⋯,3 + + let word8test : Word8 → IO _ + word8test w = do + putStrLn (Word8.show w ++ " = " ++ Word8.showBits w) + putStrLn (Word8.show w ++ " = " ++ Word8.showHexa w) + putStrLn (Word8.show w ++ " = " ++ Word8.show (Word8.fromBits (Word8.toBits w))) + + + let word64test : Word64 → IO _ + word64test w = do + putStrLn separation + putStrLn (Word64.show w ++ " = " ++ Word64.showBits w) + putStrLn (Word64.show w ++ " = " ++ Word64.showHexa w) + putStrLn (Word64.show w ++ " = " ++ Word64.show (Word64.fromBits (Word64.toBits w))) + + word8test one + word8test (Word8.fromℕ 144) + word64test two + word64test three + word64test (Word64.fromℕ 2024) diff --git a/tests/data/bytestring/bytestring.agda-lib b/tests/data/bytestring/bytestring.agda-lib new file mode 100644 index 0000000000..325830a199 --- /dev/null +++ b/tests/data/bytestring/bytestring.agda-lib @@ -0,0 +1,2 @@ +name: bytestring +include: ../../../src/ . diff --git a/tests/data/bytestring/expected b/tests/data/bytestring/expected new file mode 100644 index 0000000000..240520e413 --- /dev/null +++ b/tests/data/bytestring/expected @@ -0,0 +1,20 @@ +"\SOH\STX\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\ETX" +------------------------------------------------------------------------ +1 = 0b00000001 +1 = 0x01 +1 = 1 +144 = 0b10010000 +144 = 0x90 +144 = 144 +------------------------------------------------------------------------ +2 = 0b0000000000000000000000000000000000000000000000000000000000000010 +2 = 0x00000002 +2 = 2 +------------------------------------------------------------------------ +3 = 0b0000000000000000000000000000000000000000000000000000000000000011 +3 = 0x00000003 +3 = 3 +------------------------------------------------------------------------ +2024 = 0b0000000000000000000000000000000000000000000000000000011111101000 +2024 = 0x000007e8 +2024 = 2024 diff --git a/tests/data/bytestring/run b/tests/data/bytestring/run new file mode 100644 index 0000000000..f6e7c9b3c0 --- /dev/null +++ b/tests/data/bytestring/run @@ -0,0 +1,5 @@ +$1 --compile-dir=../../_build -c Main.agda > log +./../../_build/Main > output + +rm ../../_build/Main +rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file diff --git a/tests/runtests.agda b/tests/runtests.agda index c6ad22e0ce..480b890d72 100644 --- a/tests/runtests.agda +++ b/tests/runtests.agda @@ -16,6 +16,7 @@ dataTests = mkTestPool "Data structures" ∷ "rational" ∷ "rational-unnormalised" ∷ "trie" + ∷ "bytestring" ∷ [] systemTests : TestPool