------------------------------------------------------------------------
-- The Agda standard library
--
-- Word64: simple bindings to Haskell types and functions
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible #-}

module Data.Word64.Primitive where

open import Agda.Builtin.Bool using (Bool)
open import Agda.Builtin.Nat using (Nat)
open import Agda.Builtin.String using (String)
open import Agda.Builtin.Word using (Word64)

postulate
  testBit : Word64 → Nat → Bool
  setBit : Word64 → Nat → Word64
  clearBit : Word64 → Nat → Word64
  show : Word64 → String

{-# FOREIGN GHC import GHC.Word #-}
{-# FOREIGN GHC import qualified Data.Bits as B #-}
{-# FOREIGN GHC import qualified Data.Text as T #-}

{-# 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 show = T.pack . Prelude.show #-}