------------------------------------------------------------------------
-- The Agda standard library
--
-- Machine words: unsafe functions using the FFI
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible #-}
module Data.Word64.Unsafe where
open import Agda.Builtin.Bool using (Bool; true; false)
open import Data.Fin.Base as Fin using (Fin)
open import Data.Product.Base using (proj₁)
open import Data.Vec.Base as Vec using (Vec)
open import Data.Word8.Base as Word8 using (Word8)
open import Data.Word64.Base using (Word64; fromℕ)
open import Function.Base using (_$_; _|>_)
------------------------------------------------------------------------
-- 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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4