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