    ------------------------------------------------------------------------
    -- 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