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