agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
575 stars 237 forks source link

[ new ] Word8, Bytestring, Bytestring builder #2376

Closed gallais closed 3 months ago

gallais commented 5 months ago

New modules:

Data.Bytestring.Base
Data.Bytestring.Builder.Base
Data.Bytestring.Builder.Primitive
Data.Bytestring.IO
Data.Bytestring.IO.Primitive
Data.Bytestring.Primitive

Data.Word8.Primitive
Data.Word8.Base
Data.Word8.Literals
Data.Word8.Show

Data.Word64.Literals
Data.Word64.Unsafe
Data.Word64.Show
gallais commented 3 months ago

I think that's now ready. Writing the test has, as always, revealed that some useful functions were missing and so I have added them.

jamesmckinna commented 3 months ago

Re: @JacquesCarette 's comments about --safe: Out of interest, what correctness guarantees/checks (if any) are provided for primitive machine arithmetic?

Do we have anywhere a reference implementation of eg octal, hex or higher word size operations?

cf. #2362

gallais commented 3 months ago

what correctness guarantees/checks (if any) are provided for primitive machine arithmetic?

None. IIRC the builtin Word64 is there primarily because of

primQNameToWord64s : Name → Σ Word64 (λ _ → Word64)

which gives us a way to define an order on QNames to e.g. put them as Map keys. No interest was paid to its computational content.