{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -funbox-strict-fields #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.BV
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.BV
  ( IntN (..),
    IntN8,
    IntN16,
    IntN32,
    IntN64,
    WordN (..),
    WordN8,
    WordN16,
    WordN32,
    WordN64,
    readBinary,
  )
where

import Control.Applicative (Alternative ((<|>)))
import Control.DeepSeq (NFData)
import Control.Exception
  ( ArithException (Overflow),
    throw,
  )
import qualified Data.Binary as Binary
import Data.Bits
  ( Bits
      ( bit,
        bitSize,
        bitSizeMaybe,
        clearBit,
        complement,
        isSigned,
        popCount,
        rotateL,
        rotateR,
        shiftL,
        shiftR,
        testBit,
        xor,
        zeroBits,
        (.&.),
        (.|.)
      ),
    FiniteBits (finiteBitSize),
  )
import Data.Bytes.Serial (Serial (deserialize, serialize))
import Data.Hashable (Hashable)
import Data.Maybe (fromMaybe, isJust)
import Data.Proxy (Proxy (Proxy))
import Data.SBV (Int16, Int32, Int64, Int8, Word8)
import qualified Data.Serialize as Cereal
import Data.Word (Word16, Word32, Word64)
import GHC.Enum
  ( boundedEnumFrom,
    boundedEnumFromThen,
    predError,
    succError,
    toEnumError,
  )
import GHC.Generics (Generic)
import GHC.Read
  ( Read (readListPrec, readPrec),
    parens,
    readListDefault,
    readListPrecDefault,
    readNumber,
  )
import GHC.Real ((%))
import GHC.TypeNats
  ( KnownNat,
    Nat,
    natVal,
    type (+),
    type (<=),
  )
import Grisette.Internal.Core.Data.Class.BitCast (BitCast (bitCast))
import Grisette.Internal.Core.Data.Class.BitVector
  ( SizedBV
      ( sizedBVConcat,
        sizedBVExt,
        sizedBVSelect,
        sizedBVSext,
        sizedBVZext
      ),
  )
import Grisette.Internal.Core.Data.Class.Function (Apply (FunType, apply))
import Grisette.Internal.Core.Data.Class.SignConversion
  ( SignConversion (toSigned, toUnsigned),
  )
import Grisette.Internal.Core.Data.Class.SymRotate
  ( DefaultFiniteBitsSymRotate (DefaultFiniteBitsSymRotate),
    SymRotate,
  )
import Grisette.Internal.Core.Data.Class.SymShift
  ( DefaultFiniteBitsSymShift (DefaultFiniteBitsSymShift),
    SymShift,
  )
import Language.Haskell.TH.Syntax (Lift)
import Numeric (showHex, showIntAtBase)
import qualified Test.QuickCheck as QC
import Text.ParserCombinators.ReadP (string)
import Text.ParserCombinators.ReadPrec
  ( ReadPrec,
    get,
    look,
    pfail,
  )
import Text.Read (lift)
import qualified Text.Read.Lex as L

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim
-- >>> import Grisette.Backend
-- >>> import Data.Proxy

-- |
-- Unsigned bit vector type. Indexed with the bit width. Signedness affect the
-- semantics of the operations, including comparison/extension, etc.
--
-- >>> 3 + 5 :: WordN 5
-- 0b01000
-- >>> sizedBVConcat (0b101 :: WordN 3) (0b110 :: WordN 3)
-- 0b101110
-- >>> sizedBVExt (Proxy @6) (0b101 :: WordN 3)
-- 0b000101
-- >>> (8 :: WordN 4) < (7 :: WordN 4)
-- False
--
-- More operations are available. Please refer to "Grisette.Core#g:symops" for
-- more information.
newtype WordN (n :: Nat) = WordN {unWordN :: Integer}
  deriving (Eq, Ord, Generic, Lift, Hashable, NFData)

-- | 8-bit unsigned bit-vector
type WordN8 = WordN 8

-- | 16-bit unsigned bit-vector
type WordN16 = WordN 16

-- | 32-bit unsigned bit-vector
type WordN32 = WordN 32

-- | 64-bit unsigned bit-vector
type WordN64 = WordN 64

instance (KnownNat n, 1 <= n) => Show (WordN n) where
  show (WordN w) = if (bitwidth `mod` 4) == 0 then hexRepPre ++ hexRep else binRepPre ++ binRep
    where
      bitwidth = natVal (Proxy :: Proxy n)
      hexRepPre = "0x" ++ replicate (fromIntegral (bitwidth `div` 4) - length hexRep) '0'
      hexRep = showHex w ""
      binRepPre = "0b" ++ replicate (fromIntegral bitwidth - length binRep) '0'
      binRep = showIntAtBase 2 (\x -> if x == 0 then '0' else '1') w ""

instance (KnownNat n, 1 <= n) => Serial (WordN n) where
  serialize (WordN w) = serialize w
  deserialize = WordN <$> deserialize

instance (KnownNat n, 1 <= n) => Cereal.Serialize (WordN n) where
  put = serialize
  get = deserialize

instance (KnownNat n, 1 <= n) => Binary.Binary (WordN n) where
  put = serialize
  get = deserialize

convertInt :: (Num a) => L.Lexeme -> ReadPrec a
convertInt (L.Number n)
  | Just i <- L.numberToInteger n = return (fromInteger i)
convertInt _ = pfail

-- | Read a binary number.
readBinary :: (Num a) => ReadPrec a
readBinary = parens $ do
  r0 <- look
  case r0 of
    ('-' : _) -> do
      _ <- get
      negate <$> parens parse0b
    _ -> parse0b
  where
    isDigit c = isJust (valDig c)
    valDigit c = fromMaybe 0 (valDig c)
    valDig '0' = Just 0
    valDig '1' = Just 1
    valDig _ = Nothing
    parse0b = do
      _ <- Text.Read.lift $ string "0b"
      fromInteger <$> Text.Read.lift (L.readIntP 2 isDigit valDigit)

#if MIN_VERSION_base(4,21,0)
readBV :: Num a => ReadPrec a
readBV = readNumber convertInt
#else
readBV :: Num a => ReadPrec a
readBV = readNumber convertInt <|> readBinary
#endif

instance (KnownNat n, 1 <= n) => Read (WordN n) where
  readPrec = readBV
  readListPrec = readListPrecDefault
  readList = readListDefault

-- |
-- Signed bit vector type. Indexed with the bit width. Signedness affects the
-- semantics of the operations, including comparison/extension, etc.
--
-- >>> 3 + 5 :: IntN 5
-- 0b01000
-- >>> sizedBVConcat (0b101 :: IntN 3) (0b110 :: IntN 3)
-- 0b101110
-- >>> sizedBVExt (Proxy @6) (0b101 :: IntN 3)
-- 0b111101
-- >>> (8 :: IntN 4) < (7 :: IntN 4)
-- True
--
-- More operations are available. Please refer to "Grisette.Core#g:symops" for
-- more information.
newtype IntN (n :: Nat) = IntN {unIntN :: Integer}
  deriving (Eq, Generic, Lift, Hashable, NFData)

-- | 8-bit signed bit-vector
type IntN8 = IntN 8

-- | 16-bit signed bit-vector
type IntN16 = IntN 16

-- | 32-bit signed bit-vector
type IntN32 = IntN 32

-- | 64-bit signed bit-vector
type IntN64 = IntN 64

instance (KnownNat n, 1 <= n) => Show (IntN n) where
  show (IntN w) = if (bitwidth `mod` 4) == 0 then hexRepPre ++ hexRep else binRepPre ++ binRep
    where
      bitwidth = natVal (Proxy :: Proxy n)
      hexRepPre = "0x" ++ replicate (fromIntegral (bitwidth `div` 4) - length hexRep) '0'
      hexRep = showHex w ""
      binRepPre = "0b" ++ replicate (fromIntegral bitwidth - length binRep) '0'
      binRep = showIntAtBase 2 (\x -> if x == 0 then '0' else '1') w ""

instance (KnownNat n, 1 <= n) => Serial (IntN n) where
  serialize (IntN w) = serialize w
  deserialize = IntN <$> deserialize

instance (KnownNat n, 1 <= n) => Cereal.Serialize (IntN n) where
  put = serialize
  get = deserialize

instance (KnownNat n, 1 <= n) => Binary.Binary (IntN n) where
  put = serialize
  get = deserialize

instance (KnownNat n, 1 <= n) => Read (IntN n) where
  readPrec = readBV
  readListPrec = readListPrecDefault
  readList = readListDefault

instance (KnownNat n, 1 <= n) => Bits (WordN n) where
  WordN a .&. WordN b = WordN (a .&. b)
  WordN a .|. WordN b = WordN (a .|. b)
  WordN a `xor` WordN b = WordN (a `xor` b)
  complement a = maxBound `xor` a

  -- shift use default implementation
  -- rotate use default implementation
  zeroBits = WordN 0
  bit i
    | i < 0 || i >= fromIntegral (natVal (Proxy :: Proxy n)) = zeroBits
    | otherwise = WordN (bit i)

  -- setBit use default implementation
  clearBit (WordN a) i = WordN (clearBit a i)

  -- complementBit use default implementation
  testBit (WordN a) = testBit a
  bitSizeMaybe = Just . finiteBitSize
  bitSize = finiteBitSize
  isSigned _ = False
  shiftL w i | i >= finiteBitSize w = 0
  shiftL (WordN a) i = WordN (a `shiftL` i) .&. maxBound

  -- unsafeShiftL use default implementation
  shiftR w i | i >= finiteBitSize w = 0
  shiftR (WordN a) i = WordN (a `shiftR` i)

  -- unsafeShiftR use default implementation
  rotateL a 0 = a
  rotateL (WordN a) k
    | k >= n = rotateL (WordN a) (k `mod` n)
    | otherwise = WordN $ l + h
    where
      n = fromIntegral $ natVal (Proxy :: Proxy n)
      s = n - k
      l = a `shiftR` s
      h = (a - (l `shiftL` s)) `shiftL` k
  rotateR a 0 = a
  rotateR (WordN a) k
    | k >= n = rotateR (WordN a) (k `mod` n)
    | otherwise = WordN $ l + h
    where
      n = fromIntegral $ natVal (Proxy :: Proxy n)
      s = n - k
      l = a `shiftR` k
      h = (a - (l `shiftL` k)) `shiftL` s
  popCount (WordN n) = popCount n

instance (KnownNat n, 1 <= n) => FiniteBits (WordN n) where
  finiteBitSize _ = fromIntegral (natVal (Proxy :: Proxy n))

instance (KnownNat n, 1 <= n) => Bounded (WordN n) where
  maxBound = WordN ((1 `shiftL` fromIntegral (natVal (Proxy :: Proxy n))) - 1)
  minBound = WordN 0

instance (KnownNat n, 1 <= n) => Enum (WordN n) where
  succ x
    | x /= maxBound = x + 1
    | otherwise = succError $ "WordN " ++ show (natVal (Proxy :: Proxy n))
  pred x
    | x /= minBound = x - 1
    | otherwise = predError $ "WordN " ++ show (natVal (Proxy :: Proxy n))
  toEnum i
    | i >= 0 && toInteger i <= toInteger (maxBound :: WordN n) = WordN (toInteger i)
    | otherwise = toEnumError ("WordN " ++ show (natVal (Proxy :: Proxy n))) i (minBound :: WordN n, maxBound :: WordN n)
  fromEnum (WordN n) = fromEnum n
  enumFrom = boundedEnumFrom
  {-# INLINE enumFrom #-}
  enumFromThen = boundedEnumFromThen
  {-# INLINE enumFromThen #-}

instance (KnownNat n, 1 <= n) => Real (WordN n) where
  toRational (WordN n) = n % 1

instance (KnownNat n, 1 <= n) => Integral (WordN n) where
  quot (WordN x) (WordN y) = WordN (x `quot` y)
  rem (WordN x) (WordN y) = WordN (x `rem` y)
  quotRem (WordN x) (WordN y) = case quotRem x y of
    (q, r) -> (WordN q, WordN r)
  div = quot
  mod = rem
  divMod = quotRem
  toInteger (WordN n) = n

instance (KnownNat n, 1 <= n) => Num (WordN n) where
  WordN x + WordN y = WordN (x + y) .&. maxBound
  WordN x * WordN y = WordN (x * y) .&. maxBound
  WordN x - WordN y
    | x >= y = WordN (x - y)
    | otherwise = WordN ((1 `shiftL` fromIntegral (natVal (Proxy :: Proxy n))) + x - y)
  negate (WordN 0) = WordN 0
  negate a = complement a + WordN 1
  abs x = x
  signum (WordN 0) = 0
  signum _ = 1
  fromInteger !x
    | x == 0 = WordN 0
    | x > 0 = WordN (x .&. unWordN (maxBound :: WordN n))
    | otherwise = -fromInteger (-x)

instance (KnownNat n, 1 <= n) => QC.Arbitrary (WordN n) where
  arbitrary = QC.arbitrarySizedBoundedIntegral

  -- QC.shrinkIntegral assumes that 2 is representable by the number, which is
  -- not the case for 1-bit bit vector.
  shrink i
    | i == 0 = []
    | i == 1 = [0]
    | otherwise = QC.shrinkIntegral i

minusOneIntN :: forall proxy n. (KnownNat n) => proxy n -> IntN n
minusOneIntN _ = IntN (1 `shiftL` fromIntegral (natVal (Proxy :: Proxy n)) - 1)

instance (KnownNat n, 1 <= n) => Bits (IntN n) where
  IntN a .&. IntN b = IntN (a .&. b)
  IntN a .|. IntN b = IntN (a .|. b)
  IntN a `xor` IntN b = IntN (a `xor` b)
  complement a = minusOneIntN (Proxy :: Proxy n) `xor` a

  -- shift use default implementation
  -- rotate use default implementation
  zeroBits = IntN 0
  bit i = IntN (unWordN (bit i :: WordN n))

  -- setBit use default implementation
  clearBit (IntN a) i = IntN (clearBit a i)

  -- complementBit use default implementation
  testBit (IntN a) = testBit a
  bitSizeMaybe = Just . finiteBitSize
  bitSize = finiteBitSize
  isSigned _ = True

  shiftL (IntN a) i = IntN (unWordN $ (WordN a :: WordN n) `shiftL` i)

  -- unsafeShiftL use default implementation
  shiftR i 0 = i
  shiftR (IntN i) k
    | k >= n = if b then IntN (maxi - 1) else IntN 0
    | otherwise = if b then IntN (maxi - noi + (i `shiftR` k)) else IntN (i `shiftR` k)
    where
      b = testBit i (n - 1)
      n = fromIntegral $ natVal (Proxy :: Proxy n)
      maxi = (1 :: Integer) `shiftL` n
      noi = (1 :: Integer) `shiftL` (n - k)

  -- unsafeShiftR use default implementation
  rotateL (IntN i) k = IntN $ unWordN $ rotateL (WordN i :: WordN n) k
  rotateR (IntN i) k = IntN $ unWordN $ rotateR (WordN i :: WordN n) k
  popCount (IntN i) = popCount i

instance (KnownNat n, 1 <= n) => FiniteBits (IntN n) where
  finiteBitSize _ = fromIntegral (natVal (Proxy :: Proxy n))

instance (KnownNat n, 1 <= n) => Bounded (IntN n) where
  maxBound = IntN (1 `shiftL` (fromIntegral (natVal (Proxy :: Proxy n)) - 1) - 1)
  minBound = maxBound + 1

instance (KnownNat n, 1 <= n) => Enum (IntN n) where
  succ x
    | x /= maxBound = x + 1
    | otherwise = succError $ "IntN " ++ show (natVal (Proxy :: Proxy n))
  pred x
    | x /= minBound = x - 1
    | otherwise = predError $ "IntN " ++ show (natVal (Proxy :: Proxy n))
  toEnum i
    | i >= fromIntegral (minBound :: IntN n) && i <= fromIntegral (maxBound :: IntN n) = fromIntegral i
    | otherwise = toEnumError ("IntN " ++ show (natVal (Proxy :: Proxy n))) i (minBound :: WordN n, maxBound :: WordN n)
  fromEnum = fromEnum . toInteger
  enumFrom = boundedEnumFrom
  {-# INLINE enumFrom #-}
  enumFromThen = boundedEnumFromThen
  {-# INLINE enumFromThen #-}

instance (KnownNat n, 1 <= n) => Real (IntN n) where
  toRational i = toInteger i % 1

instance (KnownNat n, 1 <= n) => Integral (IntN n) where
  quot x y =
    if x == minBound && y == -1
      then throw Overflow
      else fromInteger (toInteger x `quot` toInteger y)
  rem x y = fromInteger (toInteger x `rem` toInteger y)
  quotRem x y =
    if x == minBound && y == -1
      then throw Overflow
      else case quotRem (toInteger x) (toInteger y) of
        (q, r) -> (fromInteger q, fromInteger r)
  div x y =
    if x == minBound && y == -1
      then throw Overflow
      else fromInteger (toInteger x `div` toInteger y)
  mod x y = fromInteger (toInteger x `mod` toInteger y)
  divMod x y =
    if x == minBound && y == -1
      then throw Overflow
      else case divMod (toInteger x) (toInteger y) of
        (q, r) -> (fromInteger q, fromInteger r)
  toInteger i@(IntN n) = case signum i of
    0 -> 0
    -1 ->
      let x = negate i
       in if signum x == -1 then -n else negate (toInteger x)
    1 -> n
    _ -> undefined

instance (KnownNat n, 1 <= n) => Num (IntN n) where
  IntN x + IntN y = IntN (x + y) .&. minusOneIntN (Proxy :: Proxy n)
  IntN x * IntN y = IntN (x * y) .&. minusOneIntN (Proxy :: Proxy n)
  IntN x - IntN y
    | x >= y = IntN (x - y)
    | otherwise = IntN ((1 `shiftL` fromIntegral (natVal (Proxy :: Proxy n))) + x - y)
  negate (IntN 0) = IntN 0
  negate a = complement a + IntN 1
  abs x = if testBit x (fromIntegral $ natVal (Proxy :: Proxy n) - 1) then negate x else x
  signum (IntN 0) = IntN 0
  signum i = if testBit i (fromIntegral $ natVal (Proxy :: Proxy n) - 1) then -1 else 1
  fromInteger !x = IntN $ if v >= 0 then v else (1 `shiftL` n) + v
    where
      v = unWordN (fromInteger (x + maxn) :: WordN n) - maxn
      n = fromIntegral (natVal (Proxy :: Proxy n))
      maxn = 1 `shiftL` (n - 1) - 1

instance (KnownNat n, 1 <= n) => Ord (IntN n) where
  IntN a <= IntN b
    | as && not bs = True
    | not as && bs = False
    | otherwise = a <= b
    where
      n = fromIntegral (natVal (Proxy :: Proxy n))
      as = testBit a (n - 1)
      bs = testBit b (n - 1)

instance (KnownNat n, 1 <= n) => QC.Arbitrary (IntN n) where
  arbitrary = QC.arbitrarySizedBoundedIntegral

  -- QC.shrinkIntegral assumes that 2 is representable by the number, which is
  -- not the case for 1-bit bit vector.
  shrink i
    | i == 0 = []
    | i == 1 = [0]
    | otherwise = QC.shrinkIntegral i

instance SizedBV WordN where
  sizedBVConcat :: forall l r. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => WordN l -> WordN r -> WordN (l + r)
  sizedBVConcat (WordN a) (WordN b) = WordN ((a `shiftL` fromIntegral (natVal (Proxy :: Proxy r))) .|. b)
  sizedBVZext _ (WordN v) = WordN v
  sizedBVSext :: forall l r proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r
  sizedBVSext pr (WordN v) = if s then WordN (maxi - noi + v) else WordN v
    where
      r = fromIntegral $ natVal pr
      l = fromIntegral $ natVal (Proxy :: Proxy l)
      s = testBit v (l - 1)
      maxi = (1 :: Integer) `shiftL` r
      noi = (1 :: Integer) `shiftL` l
  sizedBVExt = sizedBVZext
  sizedBVSelect ::
    forall n ix w p q.
    (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) =>
    p ix ->
    q w ->
    WordN n ->
    WordN w
  sizedBVSelect pix pw (WordN v) = WordN ((v `shiftR` ix) .&. mask)
    where
      ix = fromIntegral $ natVal pix
      w = fromIntegral $ natVal pw
      mask = (1 `shiftL` w) - 1

instance SizedBV IntN where
  sizedBVConcat :: forall l r. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => IntN l -> IntN r -> IntN (l + r)
  sizedBVConcat (IntN a) (IntN b) = IntN $ unWordN $ sizedBVConcat (WordN a :: WordN l) (WordN b :: WordN r)
  sizedBVZext _ (IntN v) = IntN v
  sizedBVSext :: forall l r proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r
  sizedBVSext pr (IntN v) = IntN $ unWordN $ sizedBVSext pr (WordN v :: WordN l)
  sizedBVExt = sizedBVSext
  sizedBVSelect ::
    forall n ix w p q.
    (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) =>
    p ix ->
    q w ->
    IntN n ->
    IntN w
  sizedBVSelect pix pw (IntN v) = IntN $ unWordN $ sizedBVSelect pix pw (WordN v :: WordN n)

instance (KnownNat n, 1 <= n) => SignConversion (WordN n) (IntN n) where
  toSigned (WordN i) = IntN i
  toUnsigned (IntN i) = WordN i

deriving via
  (DefaultFiniteBitsSymShift (IntN n))
  instance
    (KnownNat n, 1 <= n) => SymShift (IntN n)

deriving via
  (DefaultFiniteBitsSymShift (WordN n))
  instance
    (KnownNat n, 1 <= n) => SymShift (WordN n)

deriving via
  (DefaultFiniteBitsSymRotate (IntN n))
  instance
    (KnownNat n, 1 <= n) => SymRotate (IntN n)

deriving via
  (DefaultFiniteBitsSymRotate (WordN n))
  instance
    (KnownNat n, 1 <= n) => SymRotate (WordN n)

#define BITCAST_FROM_INTEGRAL(from, to) \
  instance BitCast (from) (to) where \
    bitCast = fromIntegral

#if 1
BITCAST_FROM_INTEGRAL(WordN 8, Word8)
BITCAST_FROM_INTEGRAL(WordN 16, Word16)
BITCAST_FROM_INTEGRAL(WordN 32, Word32)
BITCAST_FROM_INTEGRAL(WordN 64, Word64)
BITCAST_FROM_INTEGRAL(WordN 8, Int8)
BITCAST_FROM_INTEGRAL(WordN 16, Int16)
BITCAST_FROM_INTEGRAL(WordN 32, Int32)
BITCAST_FROM_INTEGRAL(WordN 64, Int64)

BITCAST_FROM_INTEGRAL(Word8, WordN 8)
BITCAST_FROM_INTEGRAL(Word16, WordN 16)
BITCAST_FROM_INTEGRAL(Word32, WordN 32)
BITCAST_FROM_INTEGRAL(Word64, WordN 64)
BITCAST_FROM_INTEGRAL(Int8, WordN 8)
BITCAST_FROM_INTEGRAL(Int16, WordN 16)
BITCAST_FROM_INTEGRAL(Int32, WordN 32)
BITCAST_FROM_INTEGRAL(Int64, WordN 64)

BITCAST_FROM_INTEGRAL(IntN 8, Word8)
BITCAST_FROM_INTEGRAL(IntN 16, Word16)
BITCAST_FROM_INTEGRAL(IntN 32, Word32)
BITCAST_FROM_INTEGRAL(IntN 64, Word64)
BITCAST_FROM_INTEGRAL(IntN 8, Int8)
BITCAST_FROM_INTEGRAL(IntN 16, Int16)
BITCAST_FROM_INTEGRAL(IntN 32, Int32)
BITCAST_FROM_INTEGRAL(IntN 64, Int64)

BITCAST_FROM_INTEGRAL(Word8, IntN 8)
BITCAST_FROM_INTEGRAL(Word16, IntN 16)
BITCAST_FROM_INTEGRAL(Word32, IntN 32)
BITCAST_FROM_INTEGRAL(Word64, IntN 64)
BITCAST_FROM_INTEGRAL(Int8, IntN 8)
BITCAST_FROM_INTEGRAL(Int16, IntN 16)
BITCAST_FROM_INTEGRAL(Int32, IntN 32)
BITCAST_FROM_INTEGRAL(Int64, IntN 64)
#endif

instance (KnownNat n, 1 <= n) => BitCast (WordN n) (IntN n) where
  bitCast (WordN i) = IntN i

instance (KnownNat n, 1 <= n) => BitCast (IntN n) (WordN n) where
  bitCast (IntN i) = WordN i

#define BITCAST_VIA_WORDx(from, to, intermediate) \
  instance BitCast (from) (to) where \
    bitCast x = bitCast (bitCast x :: intermediate)

#if 1
BITCAST_VIA_WORDx(WordN64, Double, Word64)
BITCAST_VIA_WORDx(Double, WordN64, Word64)
BITCAST_VIA_WORDx(IntN64, Double, Word64)
BITCAST_VIA_WORDx(Double, IntN64, Word64)
BITCAST_VIA_WORDx(WordN32, Float, Word32)
BITCAST_VIA_WORDx(Float, WordN32, Word32)
BITCAST_VIA_WORDx(IntN32, Float, Word32)
BITCAST_VIA_WORDx(Float, IntN32, Word32)
#endif

instance BitCast Bool (WordN 1) where
  bitCast False = 0
  bitCast True = 1

instance BitCast (WordN 1) Bool where
  bitCast 0 = False
  bitCast _ = True

instance BitCast Bool (IntN 1) where
  bitCast False = 0
  bitCast True = 1

instance BitCast (IntN 1) Bool where
  bitCast 0 = False
  bitCast _ = True

instance Apply (IntN n) where
  type FunType (IntN n) = IntN n
  apply = id

instance Apply (WordN n) where
  type FunType (WordN n) = WordN n
  apply = id