{-# 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 {forall (n :: Nat). WordN n -> Integer
unWordN :: Integer}
  deriving (WordN n -> WordN n -> Bool
(WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool) -> Eq (WordN n)
forall (n :: Nat). WordN n -> WordN n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Nat). WordN n -> WordN n -> Bool
== :: WordN n -> WordN n -> Bool
$c/= :: forall (n :: Nat). WordN n -> WordN n -> Bool
/= :: WordN n -> WordN n -> Bool
Eq, Eq (WordN n)
Eq (WordN n) =>
(WordN n -> WordN n -> Ordering)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> WordN n)
-> (WordN n -> WordN n -> WordN n)
-> Ord (WordN n)
WordN n -> WordN n -> Bool
WordN n -> WordN n -> Ordering
WordN n -> WordN n -> WordN n
forall (n :: Nat). Eq (WordN n)
forall (n :: Nat). WordN n -> WordN n -> Bool
forall (n :: Nat). WordN n -> WordN n -> Ordering
forall (n :: Nat). WordN n -> WordN n -> WordN n
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: forall (n :: Nat). WordN n -> WordN n -> Ordering
compare :: WordN n -> WordN n -> Ordering
$c< :: forall (n :: Nat). WordN n -> WordN n -> Bool
< :: WordN n -> WordN n -> Bool
$c<= :: forall (n :: Nat). WordN n -> WordN n -> Bool
<= :: WordN n -> WordN n -> Bool
$c> :: forall (n :: Nat). WordN n -> WordN n -> Bool
> :: WordN n -> WordN n -> Bool
$c>= :: forall (n :: Nat). WordN n -> WordN n -> Bool
>= :: WordN n -> WordN n -> Bool
$cmax :: forall (n :: Nat). WordN n -> WordN n -> WordN n
max :: WordN n -> WordN n -> WordN n
$cmin :: forall (n :: Nat). WordN n -> WordN n -> WordN n
min :: WordN n -> WordN n -> WordN n
Ord, (forall x. WordN n -> Rep (WordN n) x)
-> (forall x. Rep (WordN n) x -> WordN n) -> Generic (WordN n)
forall (n :: Nat) x. Rep (WordN n) x -> WordN n
forall (n :: Nat) x. WordN n -> Rep (WordN n) x
forall x. Rep (WordN n) x -> WordN n
forall x. WordN n -> Rep (WordN n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (n :: Nat) x. WordN n -> Rep (WordN n) x
from :: forall x. WordN n -> Rep (WordN n) x
$cto :: forall (n :: Nat) x. Rep (WordN n) x -> WordN n
to :: forall x. Rep (WordN n) x -> WordN n
Generic, (forall (m :: * -> *). Quote m => WordN n -> m Exp)
-> (forall (m :: * -> *). Quote m => WordN n -> Code m (WordN n))
-> Lift (WordN n)
forall (n :: Nat) (m :: * -> *). Quote m => WordN n -> m Exp
forall (n :: Nat) (m :: * -> *).
Quote m =>
WordN n -> Code m (WordN n)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => WordN n -> m Exp
forall (m :: * -> *). Quote m => WordN n -> Code m (WordN n)
$clift :: forall (n :: Nat) (m :: * -> *). Quote m => WordN n -> m Exp
lift :: forall (m :: * -> *). Quote m => WordN n -> m Exp
$cliftTyped :: forall (n :: Nat) (m :: * -> *).
Quote m =>
WordN n -> Code m (WordN n)
liftTyped :: forall (m :: * -> *). Quote m => WordN n -> Code m (WordN n)
Lift, Eq (WordN n)
Eq (WordN n) =>
(Int -> WordN n -> Int) -> (WordN n -> Int) -> Hashable (WordN n)
Int -> WordN n -> Int
WordN n -> Int
forall (n :: Nat). Eq (WordN n)
forall (n :: Nat). Int -> WordN n -> Int
forall (n :: Nat). WordN n -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: forall (n :: Nat). Int -> WordN n -> Int
hashWithSalt :: Int -> WordN n -> Int
$chash :: forall (n :: Nat). WordN n -> Int
hash :: WordN n -> Int
Hashable, WordN n -> ()
(WordN n -> ()) -> NFData (WordN n)
forall (n :: Nat). WordN n -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall (n :: Nat). WordN n -> ()
rnf :: WordN n -> ()
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 n -> String
show (WordN Integer
w) = if (Nat
bitwidth Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`mod` Nat
4) Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
0 then String
hexRepPre String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
hexRep else String
binRepPre String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
binRep
    where
      bitwidth :: Nat
bitwidth = Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
      hexRepPre :: String
hexRepPre = String
"0x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat
bitwidth Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`div` Nat
4) Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
hexRep) Char
'0'
      hexRep :: String
hexRep = Integer -> ShowS
forall a. Integral a => a -> ShowS
showHex Integer
w String
""
      binRepPre :: String
binRepPre = String
"0b" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
bitwidth Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
binRep) Char
'0'
      binRep :: String
binRep = Integer -> (Int -> Char) -> Integer -> ShowS
forall a. Integral a => a -> (Int -> Char) -> a -> ShowS
showIntAtBase Integer
2 (\Int
x -> if Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Char
'0' else Char
'1') Integer
w String
""

instance (KnownNat n, 1 <= n) => Serial (WordN n) where
  serialize :: forall (m :: * -> *). MonadPut m => WordN n -> m ()
serialize (WordN Integer
w) = Integer -> m ()
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => Integer -> m ()
serialize Integer
w
  deserialize :: forall (m :: * -> *). MonadGet m => m (WordN n)
deserialize = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer -> WordN n) -> m Integer -> m (WordN n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Integer
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m Integer
deserialize

instance (KnownNat n, 1 <= n) => Cereal.Serialize (WordN n) where
  put :: Putter (WordN n)
put = Putter (WordN n)
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => WordN n -> m ()
serialize
  get :: Get (WordN n)
get = Get (WordN n)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (WordN n)
deserialize

instance (KnownNat n, 1 <= n) => Binary.Binary (WordN n) where
  put :: WordN n -> Put
put = WordN n -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => WordN n -> m ()
serialize
  get :: Get (WordN n)
get = Get (WordN n)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (WordN n)
deserialize

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

-- | Read a binary number.
readBinary :: (Num a) => ReadPrec a
readBinary :: forall a. Num a => ReadPrec a
readBinary = ReadPrec a -> ReadPrec a
forall a. ReadPrec a -> ReadPrec a
parens (ReadPrec a -> ReadPrec a) -> ReadPrec a -> ReadPrec a
forall a b. (a -> b) -> a -> b
$ do
  r0 <- ReadPrec String
look
  case r0 of
    (Char
'-' : String
_) -> do
      _ <- ReadPrec Char
get
      negate <$> parens parse0b
    String
_ -> ReadPrec a
parse0b
  where
    isDigit :: Char -> Bool
isDigit Char
c = Maybe Integer -> Bool
forall a. Maybe a -> Bool
isJust (Char -> Maybe Integer
forall {a}. Num a => Char -> Maybe a
valDig Char
c)
    valDigit :: Char -> a
valDigit Char
c = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
0 (Char -> Maybe a
forall {a}. Num a => Char -> Maybe a
valDig Char
c)
    valDig :: Char -> Maybe a
valDig Char
'0' = a -> Maybe a
forall a. a -> Maybe a
Just a
0
    valDig Char
'1' = a -> Maybe a
forall a. a -> Maybe a
Just a
1
    valDig Char
_ = Maybe a
forall a. Maybe a
Nothing
    parse0b :: ReadPrec a
parse0b = do
      _ <- ReadP String -> ReadPrec String
forall a. ReadP a -> ReadPrec a
Text.Read.lift (ReadP String -> ReadPrec String)
-> ReadP String -> ReadPrec String
forall a b. (a -> b) -> a -> b
$ String -> ReadP String
string 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 :: forall a. Num a => ReadPrec a
readBV = (Lexeme -> ReadPrec a) -> ReadPrec a
forall a. Num a => (Lexeme -> ReadPrec a) -> ReadPrec a
readNumber Lexeme -> ReadPrec a
forall a. Num a => Lexeme -> ReadPrec a
convertInt ReadPrec a -> ReadPrec a -> ReadPrec a
forall a. ReadPrec a -> ReadPrec a -> ReadPrec a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ReadPrec a
forall a. Num a => ReadPrec a
readBinary
#endif

instance (KnownNat n, 1 <= n) => Read (WordN n) where
  readPrec :: ReadPrec (WordN n)
readPrec = ReadPrec (WordN n)
forall a. Num a => ReadPrec a
readBV
  readListPrec :: ReadPrec [WordN n]
readListPrec = ReadPrec [WordN n]
forall a. Read a => ReadPrec [a]
readListPrecDefault
  readList :: ReadS [WordN n]
readList = ReadS [WordN n]
forall a. Read a => ReadS [a]
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 {forall (n :: Nat). IntN n -> Integer
unIntN :: Integer}
  deriving (IntN n -> IntN n -> Bool
(IntN n -> IntN n -> Bool)
-> (IntN n -> IntN n -> Bool) -> Eq (IntN n)
forall (n :: Nat). IntN n -> IntN n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Nat). IntN n -> IntN n -> Bool
== :: IntN n -> IntN n -> Bool
$c/= :: forall (n :: Nat). IntN n -> IntN n -> Bool
/= :: IntN n -> IntN n -> Bool
Eq, (forall x. IntN n -> Rep (IntN n) x)
-> (forall x. Rep (IntN n) x -> IntN n) -> Generic (IntN n)
forall (n :: Nat) x. Rep (IntN n) x -> IntN n
forall (n :: Nat) x. IntN n -> Rep (IntN n) x
forall x. Rep (IntN n) x -> IntN n
forall x. IntN n -> Rep (IntN n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (n :: Nat) x. IntN n -> Rep (IntN n) x
from :: forall x. IntN n -> Rep (IntN n) x
$cto :: forall (n :: Nat) x. Rep (IntN n) x -> IntN n
to :: forall x. Rep (IntN n) x -> IntN n
Generic, (forall (m :: * -> *). Quote m => IntN n -> m Exp)
-> (forall (m :: * -> *). Quote m => IntN n -> Code m (IntN n))
-> Lift (IntN n)
forall (n :: Nat) (m :: * -> *). Quote m => IntN n -> m Exp
forall (n :: Nat) (m :: * -> *).
Quote m =>
IntN n -> Code m (IntN n)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => IntN n -> m Exp
forall (m :: * -> *). Quote m => IntN n -> Code m (IntN n)
$clift :: forall (n :: Nat) (m :: * -> *). Quote m => IntN n -> m Exp
lift :: forall (m :: * -> *). Quote m => IntN n -> m Exp
$cliftTyped :: forall (n :: Nat) (m :: * -> *).
Quote m =>
IntN n -> Code m (IntN n)
liftTyped :: forall (m :: * -> *). Quote m => IntN n -> Code m (IntN n)
Lift, Eq (IntN n)
Eq (IntN n) =>
(Int -> IntN n -> Int) -> (IntN n -> Int) -> Hashable (IntN n)
Int -> IntN n -> Int
IntN n -> Int
forall (n :: Nat). Eq (IntN n)
forall (n :: Nat). Int -> IntN n -> Int
forall (n :: Nat). IntN n -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: forall (n :: Nat). Int -> IntN n -> Int
hashWithSalt :: Int -> IntN n -> Int
$chash :: forall (n :: Nat). IntN n -> Int
hash :: IntN n -> Int
Hashable, IntN n -> ()
(IntN n -> ()) -> NFData (IntN n)
forall (n :: Nat). IntN n -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall (n :: Nat). IntN n -> ()
rnf :: IntN n -> ()
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 n -> String
show (IntN Integer
w) = if (Nat
bitwidth Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`mod` Nat
4) Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
0 then String
hexRepPre String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
hexRep else String
binRepPre String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
binRep
    where
      bitwidth :: Nat
bitwidth = Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
      hexRepPre :: String
hexRepPre = String
"0x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat
bitwidth Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`div` Nat
4) Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
hexRep) Char
'0'
      hexRep :: String
hexRep = Integer -> ShowS
forall a. Integral a => a -> ShowS
showHex Integer
w String
""
      binRepPre :: String
binRepPre = String
"0b" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
bitwidth Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
binRep) Char
'0'
      binRep :: String
binRep = Integer -> (Int -> Char) -> Integer -> ShowS
forall a. Integral a => a -> (Int -> Char) -> a -> ShowS
showIntAtBase Integer
2 (\Int
x -> if Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Char
'0' else Char
'1') Integer
w String
""

instance (KnownNat n, 1 <= n) => Serial (IntN n) where
  serialize :: forall (m :: * -> *). MonadPut m => IntN n -> m ()
serialize (IntN Integer
w) = Integer -> m ()
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => Integer -> m ()
serialize Integer
w
  deserialize :: forall (m :: * -> *). MonadGet m => m (IntN n)
deserialize = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> m Integer -> m (IntN n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Integer
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m Integer
deserialize

instance (KnownNat n, 1 <= n) => Cereal.Serialize (IntN n) where
  put :: Putter (IntN n)
put = Putter (IntN n)
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => IntN n -> m ()
serialize
  get :: Get (IntN n)
get = Get (IntN n)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (IntN n)
deserialize

instance (KnownNat n, 1 <= n) => Binary.Binary (IntN n) where
  put :: IntN n -> Put
put = IntN n -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => IntN n -> m ()
serialize
  get :: Get (IntN n)
get = Get (IntN n)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (IntN n)
deserialize

instance (KnownNat n, 1 <= n) => Read (IntN n) where
  readPrec :: ReadPrec (IntN n)
readPrec = ReadPrec (IntN n)
forall a. Num a => ReadPrec a
readBV
  readListPrec :: ReadPrec [IntN n]
readListPrec = ReadPrec [IntN n]
forall a. Read a => ReadPrec [a]
readListPrecDefault
  readList :: ReadS [IntN n]
readList = ReadS [IntN n]
forall a. Read a => ReadS [a]
readListDefault

instance (KnownNat n, 1 <= n) => Bits (WordN n) where
  WordN Integer
a .&. :: WordN n -> WordN n -> WordN n
.&. WordN Integer
b = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
b)
  WordN Integer
a .|. :: WordN n -> WordN n -> WordN n
.|. WordN Integer
b = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
b)
  WordN Integer
a xor :: WordN n -> WordN n -> WordN n
`xor` WordN Integer
b = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer
b)
  complement :: WordN n -> WordN n
complement WordN n
a = WordN n
forall a. Bounded a => a
maxBound WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
`xor` WordN n
a

  -- shift use default implementation
  -- rotate use default implementation
  zeroBits :: WordN n
zeroBits = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
0
  bit :: Int -> WordN n
bit Int
i
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) = WordN n
forall a. Bits a => a
zeroBits
    | Bool
otherwise = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Int -> Integer
forall a. Bits a => Int -> a
bit Int
i)

  -- setBit use default implementation
  clearBit :: WordN n -> Int -> WordN n
clearBit (WordN Integer
a) Int
i = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
clearBit Integer
a Int
i)

  -- complementBit use default implementation
  testBit :: WordN n -> Int -> Bool
testBit (WordN Integer
a) = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a
  bitSizeMaybe :: WordN n -> Maybe Int
bitSizeMaybe = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (WordN n -> Int) -> WordN n -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize
  bitSize :: WordN n -> Int
bitSize = WordN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize
  isSigned :: WordN n -> Bool
isSigned WordN n
_ = Bool
False
  shiftL :: WordN n -> Int -> WordN n
shiftL WordN n
w Int
i | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= WordN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize WordN n
w = WordN n
0
  shiftL (WordN Integer
a) Int
i = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
i) WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
.&. WordN n
forall a. Bounded a => a
maxBound

  -- unsafeShiftL use default implementation
  shiftR :: WordN n -> Int -> WordN n
shiftR WordN n
w Int
i | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= WordN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize WordN n
w = WordN n
0
  shiftR (WordN Integer
a) Int
i = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
i)

  -- unsafeShiftR use default implementation
  rotateL :: WordN n -> Int -> WordN n
rotateL WordN n
a Int
0 = WordN n
a
  rotateL (WordN Integer
a) Int
k
    | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
rotateL (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
a) (Int
k Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n)
    | Bool
otherwise = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer -> WordN n) -> Integer -> WordN n
forall a b. (a -> b) -> a -> b
$ Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
h
    where
      n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
      s :: Int
s = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k
      l :: Integer
l = Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
s
      h :: Integer
h = (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- (Integer
l Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
s)) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
k
  rotateR :: WordN n -> Int -> WordN n
rotateR WordN n
a Int
0 = WordN n
a
  rotateR (WordN Integer
a) Int
k
    | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
rotateR (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
a) (Int
k Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n)
    | Bool
otherwise = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer -> WordN n) -> Integer -> WordN n
forall a b. (a -> b) -> a -> b
$ Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
h
    where
      n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
      s :: Int
s = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k
      l :: Integer
l = Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
k
      h :: Integer
h = (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- (Integer
l Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
k)) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
s
  popCount :: WordN n -> Int
popCount (WordN Integer
n) = Integer -> Int
forall a. Bits a => a -> Int
popCount Integer
n

instance (KnownNat n, 1 <= n) => FiniteBits (WordN n) where
  finiteBitSize :: WordN n -> Int
finiteBitSize WordN n
_ = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))

instance (KnownNat n, 1 <= n) => Bounded (WordN n) where
  maxBound :: WordN n
maxBound = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN ((Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
  minBound :: WordN n
minBound = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
0

instance (KnownNat n, 1 <= n) => Enum (WordN n) where
  succ :: WordN n -> WordN n
succ WordN n
x
    | WordN n
x WordN n -> WordN n -> Bool
forall a. Eq a => a -> a -> Bool
/= WordN n
forall a. Bounded a => a
maxBound = WordN n
x WordN n -> WordN n -> WordN n
forall a. Num a => a -> a -> a
+ WordN n
1
    | Bool
otherwise = String -> WordN n
forall a. String -> a
succError (String -> WordN n) -> String -> WordN n
forall a b. (a -> b) -> a -> b
$ String
"WordN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
  pred :: WordN n -> WordN n
pred WordN n
x
    | WordN n
x WordN n -> WordN n -> Bool
forall a. Eq a => a -> a -> Bool
/= WordN n
forall a. Bounded a => a
minBound = WordN n
x WordN n -> WordN n -> WordN n
forall a. Num a => a -> a -> a
- WordN n
1
    | Bool
otherwise = String -> WordN n
forall a. String -> a
predError (String -> WordN n) -> String -> WordN n
forall a b. (a -> b) -> a -> b
$ String
"WordN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
  toEnum :: Int -> WordN n
toEnum Int
i
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= WordN n -> Integer
forall a. Integral a => a -> Integer
toInteger (WordN n
forall a. Bounded a => a
maxBound :: WordN n) = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i)
    | Bool
otherwise = String -> Int -> (WordN n, WordN n) -> WordN n
forall a b. Show a => String -> Int -> (a, a) -> b
toEnumError (String
"WordN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))) Int
i (WordN n
forall a. Bounded a => a
minBound :: WordN n, WordN n
forall a. Bounded a => a
maxBound :: WordN n)
  fromEnum :: WordN n -> Int
fromEnum (WordN Integer
n) = Integer -> Int
forall a. Enum a => a -> Int
fromEnum Integer
n
  enumFrom :: WordN n -> [WordN n]
enumFrom = WordN n -> [WordN n]
forall a. (Enum a, Bounded a) => a -> [a]
boundedEnumFrom
  {-# INLINE enumFrom #-}
  enumFromThen :: WordN n -> WordN n -> [WordN n]
enumFromThen = WordN n -> WordN n -> [WordN n]
forall a. (Enum a, Bounded a) => a -> a -> [a]
boundedEnumFromThen
  {-# INLINE enumFromThen #-}

instance (KnownNat n, 1 <= n) => Real (WordN n) where
  toRational :: WordN n -> Rational
toRational (WordN Integer
n) = Integer
n Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1

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

instance (KnownNat n, 1 <= n) => Num (WordN n) where
  WordN Integer
x + :: WordN n -> WordN n -> WordN n
+ WordN Integer
y = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y) WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
.&. WordN n
forall a. Bounded a => a
maxBound
  WordN Integer
x * :: WordN n -> WordN n -> WordN n
* WordN Integer
y = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y) WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
.&. WordN n
forall a. Bounded a => a
maxBound
  WordN Integer
x - :: WordN n -> WordN n -> WordN n
- WordN Integer
y
    | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
y = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)
    | Bool
otherwise = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN ((Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)
  negate :: WordN n -> WordN n
negate (WordN Integer
0) = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
0
  negate WordN n
a = WordN n -> WordN n
forall a. Bits a => a -> a
complement WordN n
a WordN n -> WordN n -> WordN n
forall a. Num a => a -> a -> a
+ Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
1
  abs :: WordN n -> WordN n
abs WordN n
x = WordN n
x
  signum :: WordN n -> WordN n
signum (WordN Integer
0) = WordN n
0
  signum WordN n
_ = WordN n
1
  fromInteger :: Integer -> WordN n
fromInteger !Integer
x
    | Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
0
    | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN n
forall a. Bounded a => a
maxBound :: WordN n))
    | Bool
otherwise = -Integer -> WordN n
forall a. Num a => Integer -> a
fromInteger (-Integer
x)

instance (KnownNat n, 1 <= n) => QC.Arbitrary (WordN n) where
  arbitrary :: Gen (WordN n)
arbitrary = Gen (WordN n)
forall a. (Bounded a, Integral a) => Gen a
QC.arbitrarySizedBoundedIntegral

  -- QC.shrinkIntegral assumes that 2 is representable by the number, which is
  -- not the case for 1-bit bit vector.
  shrink :: WordN n -> [WordN n]
shrink WordN n
i
    | WordN n
i WordN n -> WordN n -> Bool
forall a. Eq a => a -> a -> Bool
== WordN n
0 = []
    | WordN n
i WordN n -> WordN n -> Bool
forall a. Eq a => a -> a -> Bool
== WordN n
1 = [WordN n
0]
    | Bool
otherwise = WordN n -> [WordN n]
forall a. Integral a => a -> [a]
QC.shrinkIntegral WordN n
i

minusOneIntN :: forall proxy n. (KnownNat n) => proxy n -> IntN n
minusOneIntN :: forall (proxy :: Nat -> *) (n :: Nat).
KnownNat n =>
proxy n -> IntN n
minusOneIntN proxy n
_ = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)

instance (KnownNat n, 1 <= n) => Bits (IntN n) where
  IntN Integer
a .&. :: IntN n -> IntN n -> IntN n
.&. IntN Integer
b = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
b)
  IntN Integer
a .|. :: IntN n -> IntN n -> IntN n
.|. IntN Integer
b = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
b)
  IntN Integer
a xor :: IntN n -> IntN n -> IntN n
`xor` IntN Integer
b = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer
b)
  complement :: IntN n -> IntN n
complement IntN n
a = Proxy n -> IntN n
forall (proxy :: Nat -> *) (n :: Nat).
KnownNat n =>
proxy n -> IntN n
minusOneIntN (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) IntN n -> IntN n -> IntN n
forall a. Bits a => a -> a -> a
`xor` IntN n
a

  -- shift use default implementation
  -- rotate use default implementation
  zeroBits :: IntN n
zeroBits = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
0
  bit :: Int -> IntN n
bit Int
i = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (Int -> WordN n
forall a. Bits a => Int -> a
bit Int
i :: WordN n))

  -- setBit use default implementation
  clearBit :: IntN n -> Int -> IntN n
clearBit (IntN Integer
a) Int
i = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
clearBit Integer
a Int
i)

  -- complementBit use default implementation
  testBit :: IntN n -> Int -> Bool
testBit (IntN Integer
a) = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a
  bitSizeMaybe :: IntN n -> Maybe Int
bitSizeMaybe = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (IntN n -> Int) -> IntN n -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize
  bitSize :: IntN n -> Int
bitSize = IntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize
  isSigned :: IntN n -> Bool
isSigned IntN n
_ = Bool
True

  shiftL :: IntN n -> Int -> IntN n
shiftL (IntN Integer
a) Int
i = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN n -> Integer) -> WordN n -> Integer
forall a b. (a -> b) -> a -> b
$ (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
a :: WordN n) WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
`shiftL` Int
i)

  -- unsafeShiftL use default implementation
  shiftR :: IntN n -> Int -> IntN n
shiftR IntN n
i Int
0 = IntN n
i
  shiftR (IntN Integer
i) Int
k
    | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = if Bool
b then Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
maxi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) else Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
0
    | Bool
otherwise = if Bool
b then Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
maxi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
noi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
k)) else Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
k)
    where
      b :: Bool
b = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
i (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
      n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
      maxi :: Integer
maxi = (Integer
1 :: Integer) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
n
      noi :: Integer
noi = (Integer
1 :: Integer) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k)

  -- unsafeShiftR use default implementation
  rotateL :: IntN n -> Int -> IntN n
rotateL (IntN Integer
i) Int
k = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> Integer -> IntN n
forall a b. (a -> b) -> a -> b
$ WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN n -> Integer) -> WordN n -> Integer
forall a b. (a -> b) -> a -> b
$ WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
rotateL (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
i :: WordN n) Int
k
  rotateR :: IntN n -> Int -> IntN n
rotateR (IntN Integer
i) Int
k = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> Integer -> IntN n
forall a b. (a -> b) -> a -> b
$ WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN n -> Integer) -> WordN n -> Integer
forall a b. (a -> b) -> a -> b
$ WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
rotateR (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
i :: WordN n) Int
k
  popCount :: IntN n -> Int
popCount (IntN Integer
i) = Integer -> Int
forall a. Bits a => a -> Int
popCount Integer
i

instance (KnownNat n, 1 <= n) => FiniteBits (IntN n) where
  finiteBitSize :: IntN n -> Int
finiteBitSize IntN n
_ = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))

instance (KnownNat n, 1 <= n) => Bounded (IntN n) where
  maxBound :: IntN n
maxBound = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
  minBound :: IntN n
minBound = IntN n
forall a. Bounded a => a
maxBound IntN n -> IntN n -> IntN n
forall a. Num a => a -> a -> a
+ IntN n
1

instance (KnownNat n, 1 <= n) => Enum (IntN n) where
  succ :: IntN n -> IntN n
succ IntN n
x
    | IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
/= IntN n
forall a. Bounded a => a
maxBound = IntN n
x IntN n -> IntN n -> IntN n
forall a. Num a => a -> a -> a
+ IntN n
1
    | Bool
otherwise = String -> IntN n
forall a. String -> a
succError (String -> IntN n) -> String -> IntN n
forall a b. (a -> b) -> a -> b
$ String
"IntN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
  pred :: IntN n -> IntN n
pred IntN n
x
    | IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
/= IntN n
forall a. Bounded a => a
minBound = IntN n
x IntN n -> IntN n -> IntN n
forall a. Num a => a -> a -> a
- IntN n
1
    | Bool
otherwise = String -> IntN n
forall a. String -> a
predError (String -> IntN n) -> String -> IntN n
forall a b. (a -> b) -> a -> b
$ String
"IntN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
  toEnum :: Int -> IntN n
toEnum Int
i
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= IntN n -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (IntN n
forall a. Bounded a => a
minBound :: IntN n) Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= IntN n -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (IntN n
forall a. Bounded a => a
maxBound :: IntN n) = Int -> IntN n
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i
    | Bool
otherwise = String -> Int -> (WordN n, WordN n) -> IntN n
forall a b. Show a => String -> Int -> (a, a) -> b
toEnumError (String
"IntN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))) Int
i (WordN n
forall a. Bounded a => a
minBound :: WordN n, WordN n
forall a. Bounded a => a
maxBound :: WordN n)
  fromEnum :: IntN n -> Int
fromEnum = Integer -> Int
forall a. Enum a => a -> Int
fromEnum (Integer -> Int) -> (IntN n -> Integer) -> IntN n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger
  enumFrom :: IntN n -> [IntN n]
enumFrom = IntN n -> [IntN n]
forall a. (Enum a, Bounded a) => a -> [a]
boundedEnumFrom
  {-# INLINE enumFrom #-}
  enumFromThen :: IntN n -> IntN n -> [IntN n]
enumFromThen = IntN n -> IntN n -> [IntN n]
forall a. (Enum a, Bounded a) => a -> a -> [a]
boundedEnumFromThen
  {-# INLINE enumFromThen #-}

instance (KnownNat n, 1 <= n) => Real (IntN n) where
  toRational :: IntN n -> Rational
toRational IntN n
i = IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
i Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1

instance (KnownNat n, 1 <= n) => Integral (IntN n) where
  quot :: IntN n -> IntN n -> IntN n
quot IntN n
x IntN n
y =
    if IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& IntN n
y IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== -IntN n
1
      then ArithException -> IntN n
forall a e. (?callStack::CallStack, Exception e) => e -> a
throw ArithException
Overflow
      else Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
y)
  rem :: IntN n -> IntN n -> IntN n
rem IntN n
x IntN n
y = Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
y)
  quotRem :: IntN n -> IntN n -> (IntN n, IntN n)
quotRem IntN n
x IntN n
y =
    if IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& IntN n
y IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== -IntN n
1
      then ArithException -> (IntN n, IntN n)
forall a e. (?callStack::CallStack, Exception e) => e -> a
throw ArithException
Overflow
      else case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
quotRem (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x) (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
y) of
        (Integer
q, Integer
r) -> (Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger Integer
q, Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger Integer
r)
  div :: IntN n -> IntN n -> IntN n
div IntN n
x IntN n
y =
    if IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& IntN n
y IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== -IntN n
1
      then ArithException -> IntN n
forall a e. (?callStack::CallStack, Exception e) => e -> a
throw ArithException
Overflow
      else Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
y)
  mod :: IntN n -> IntN n -> IntN n
mod IntN n
x IntN n
y = Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
y)
  divMod :: IntN n -> IntN n -> (IntN n, IntN n)
divMod IntN n
x IntN n
y =
    if IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& IntN n
y IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== -IntN n
1
      then ArithException -> (IntN n, IntN n)
forall a e. (?callStack::CallStack, Exception e) => e -> a
throw ArithException
Overflow
      else case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x) (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
y) of
        (Integer
q, Integer
r) -> (Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger Integer
q, Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger Integer
r)
  toInteger :: IntN n -> Integer
toInteger i :: IntN n
i@(IntN Integer
n) = case IntN n -> IntN n
forall a. Num a => a -> a
signum IntN n
i of
    IntN n
0 -> Integer
0
    -1 ->
      let x :: IntN n
x = IntN n -> IntN n
forall a. Num a => a -> a
negate IntN n
i
       in if IntN n -> IntN n
forall a. Num a => a -> a
signum IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== -IntN n
1 then -Integer
n else Integer -> Integer
forall a. Num a => a -> a
negate (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x)
    IntN n
1 -> Integer
n
    IntN n
_ -> Integer
forall a. (?callStack::CallStack) => a
undefined

instance (KnownNat n, 1 <= n) => Num (IntN n) where
  IntN Integer
x + :: IntN n -> IntN n -> IntN n
+ IntN Integer
y = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y) IntN n -> IntN n -> IntN n
forall a. Bits a => a -> a -> a
.&. Proxy n -> IntN n
forall (proxy :: Nat -> *) (n :: Nat).
KnownNat n =>
proxy n -> IntN n
minusOneIntN (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
  IntN Integer
x * :: IntN n -> IntN n -> IntN n
* IntN Integer
y = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y) IntN n -> IntN n -> IntN n
forall a. Bits a => a -> a -> a
.&. Proxy n -> IntN n
forall (proxy :: Nat -> *) (n :: Nat).
KnownNat n =>
proxy n -> IntN n
minusOneIntN (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
  IntN Integer
x - :: IntN n -> IntN n -> IntN n
- IntN Integer
y
    | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
y = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)
    | Bool
otherwise = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN ((Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)
  negate :: IntN n -> IntN n
negate (IntN Integer
0) = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
0
  negate IntN n
a = IntN n -> IntN n
forall a. Bits a => a -> a
complement IntN n
a IntN n -> IntN n -> IntN n
forall a. Num a => a -> a -> a
+ Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
1
  abs :: IntN n -> IntN n
abs IntN n
x = if IntN n -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit IntN n
x (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) then IntN n -> IntN n
forall a. Num a => a -> a
negate IntN n
x else IntN n
x
  signum :: IntN n -> IntN n
signum (IntN Integer
0) = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
0
  signum IntN n
i = if IntN n -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit IntN n
i (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) then -IntN n
1 else IntN n
1
  fromInteger :: Integer -> IntN n
fromInteger !Integer
x = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> Integer -> IntN n
forall a b. (a -> b) -> a -> b
$ if Integer
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 then Integer
v else (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
n) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
v
    where
      v :: Integer
v = WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (Integer -> WordN n
forall a. Num a => Integer -> a
fromInteger (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
maxn) :: WordN n) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
maxn
      n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
      maxn :: Integer
maxn = Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1

instance (KnownNat n, 1 <= n) => Ord (IntN n) where
  IntN Integer
a <= :: IntN n -> IntN n -> Bool
<= IntN Integer
b
    | Bool
as Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
bs = Bool
True
    | Bool -> Bool
not Bool
as Bool -> Bool -> Bool
&& Bool
bs = Bool
False
    | Bool
otherwise = Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
b
    where
      n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
      as :: Bool
as = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
      bs :: Bool
bs = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
b (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

instance (KnownNat n, 1 <= n) => QC.Arbitrary (IntN n) where
  arbitrary :: Gen (IntN n)
arbitrary = Gen (IntN n)
forall a. (Bounded a, Integral a) => Gen a
QC.arbitrarySizedBoundedIntegral

  -- QC.shrinkIntegral assumes that 2 is representable by the number, which is
  -- not the case for 1-bit bit vector.
  shrink :: IntN n -> [IntN n]
shrink IntN n
i
    | IntN n
i IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
0 = []
    | IntN n
i IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
1 = [IntN n
0]
    | Bool
otherwise = IntN n -> [IntN n]
forall a. Integral a => a -> [a]
QC.shrinkIntegral IntN n
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 :: forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
WordN l -> WordN r -> WordN (l + r)
sizedBVConcat (WordN Integer
a) (WordN Integer
b) = Integer -> WordN (l + r)
forall (n :: Nat). Integer -> WordN n
WordN ((Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy r -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy r
forall {k} (t :: k). Proxy t
Proxy :: Proxy r))) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
b)
  sizedBVZext :: forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
sizedBVZext proxy r
_ (WordN Integer
v) = Integer -> WordN r
forall (n :: Nat). Integer -> WordN n
WordN Integer
v
  sizedBVSext :: forall l r proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r
  sizedBVSext :: forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
sizedBVSext proxy r
pr (WordN Integer
v) = if Bool
s then Integer -> WordN r
forall (n :: Nat). Integer -> WordN n
WordN (Integer
maxi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
noi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
v) else Integer -> WordN r
forall (n :: Nat). Integer -> WordN n
WordN Integer
v
    where
      r :: Int
r = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ proxy r -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal proxy r
pr
      l :: Int
l = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy l -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy l
forall {k} (t :: k). Proxy t
Proxy :: Proxy l)
      s :: Bool
s = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
v (Int
l Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
      maxi :: Integer
maxi = (Integer
1 :: Integer) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
r
      noi :: Integer
noi = (Integer
1 :: Integer) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
l
  sizedBVExt :: forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
sizedBVExt = proxy r -> WordN l -> WordN r
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
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 :: forall (n :: Nat) (ix :: Nat) (w :: Nat) (p :: Nat -> *)
       (q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
p ix -> q w -> WordN n -> WordN w
sizedBVSelect p ix
pix q w
pw (WordN Integer
v) = Integer -> WordN w
forall (n :: Nat). Integer -> WordN n
WordN ((Integer
v Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
ix) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask)
    where
      ix :: Int
ix = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ p ix -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal p ix
pix
      w :: Int
w = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ q w -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal q w
pw
      mask :: Integer
mask = (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
w) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
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 :: forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
IntN l -> IntN r -> IntN (l + r)
sizedBVConcat (IntN Integer
a) (IntN Integer
b) = Integer -> IntN (l + r)
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN (l + r)) -> Integer -> IntN (l + r)
forall a b. (a -> b) -> a -> b
$ WordN (l + r) -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN (l + r) -> Integer) -> WordN (l + r) -> Integer
forall a b. (a -> b) -> a -> b
$ WordN l -> WordN r -> WordN (l + r)
forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
WordN l -> WordN r -> WordN (l + r)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat (Integer -> WordN l
forall (n :: Nat). Integer -> WordN n
WordN Integer
a :: WordN l) (Integer -> WordN r
forall (n :: Nat). Integer -> WordN n
WordN Integer
b :: WordN r)
  sizedBVZext :: forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> IntN l -> IntN r
sizedBVZext proxy r
_ (IntN Integer
v) = Integer -> IntN r
forall (n :: Nat). Integer -> IntN n
IntN Integer
v
  sizedBVSext :: forall l r proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r
  sizedBVSext :: forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> IntN l -> IntN r
sizedBVSext proxy r
pr (IntN Integer
v) = Integer -> IntN r
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN r) -> Integer -> IntN r
forall a b. (a -> b) -> a -> b
$ WordN r -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN r -> Integer) -> WordN r -> Integer
forall a b. (a -> b) -> a -> b
$ proxy r -> WordN l -> WordN r
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVSext proxy r
pr (Integer -> WordN l
forall (n :: Nat). Integer -> WordN n
WordN Integer
v :: WordN l)
  sizedBVExt :: forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> IntN l -> IntN r
sizedBVExt = proxy r -> IntN l -> IntN r
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> IntN l -> IntN r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
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 :: forall (n :: Nat) (ix :: Nat) (w :: Nat) (p :: Nat -> *)
       (q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
p ix -> q w -> IntN n -> IntN w
sizedBVSelect p ix
pix q w
pw (IntN Integer
v) = Integer -> IntN w
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN w) -> Integer -> IntN w
forall a b. (a -> b) -> a -> b
$ WordN w -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN w -> Integer) -> WordN w -> Integer
forall a b. (a -> b) -> a -> b
$ p ix -> q w -> WordN n -> WordN w
forall (n :: Nat) (ix :: Nat) (w :: Nat) (p :: Nat -> *)
       (q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
p ix -> q w -> WordN n -> WordN w
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
       (p :: Nat -> *) (q :: Nat -> *).
(SizedBV bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
p ix -> q w -> bv n -> bv w
sizedBVSelect p ix
pix q w
pw (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
v :: WordN n)

instance (KnownNat n, 1 <= n) => SignConversion (WordN n) (IntN n) where
  toSigned :: WordN n -> IntN n
toSigned (WordN Integer
i) = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
i
  toUnsigned :: IntN n -> WordN n
toUnsigned (IntN Integer
i) = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
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 n -> IntN n
bitCast (WordN Integer
i) = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
i

instance (KnownNat n, 1 <= n) => BitCast (IntN n) (WordN n) where
  bitCast :: IntN n -> WordN n
bitCast (IntN Integer
i) = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
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 :: Bool -> WordN 1
bitCast Bool
False = WordN 1
0
  bitCast Bool
True = WordN 1
1

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

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

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

instance Apply (IntN n) where
  type FunType (IntN n) = IntN n
  apply :: IntN n -> FunType (IntN n)
apply = IntN n -> FunType (IntN n)
IntN n -> IntN n
forall a. a -> a
id

instance Apply (WordN n) where
  type FunType (WordN n) = WordN n
  apply :: WordN n -> FunType (WordN n)
apply = WordN n -> FunType (WordN n)
WordN n -> WordN n
forall a. a -> a
id