{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# 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
  ( BitwidthMismatch (..),
    IntN (..),
    WordN (..),
  )
where

import Control.Applicative (Alternative ((<|>)))
import Control.DeepSeq (NFData)
import Control.Exception
  ( ArithException (Overflow),
    Exception (displayException),
    throw,
  )
import Data.Bits
  ( Bits
      ( bit,
        bitSize,
        bitSizeMaybe,
        clearBit,
        complement,
        isSigned,
        popCount,
        rotateL,
        rotateR,
        shiftL,
        shiftR,
        testBit,
        xor,
        zeroBits,
        (.&.),
        (.|.)
      ),
    FiniteBits (finiteBitSize),
  )
import Data.Hashable (Hashable)
import Data.Maybe (fromMaybe, isJust)
import Data.Proxy (Proxy (Proxy))
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.BitVector
  ( SizedBV
      ( sizedBVConcat,
        sizedBVExt,
        sizedBVSelect,
        sizedBVSext,
        sizedBVZext
      ),
  )
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

data BitwidthMismatch = BitwidthMismatch
  deriving (Int -> BitwidthMismatch -> ShowS
[BitwidthMismatch] -> ShowS
BitwidthMismatch -> String
(Int -> BitwidthMismatch -> ShowS)
-> (BitwidthMismatch -> String)
-> ([BitwidthMismatch] -> ShowS)
-> Show BitwidthMismatch
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BitwidthMismatch -> ShowS
showsPrec :: Int -> BitwidthMismatch -> ShowS
$cshow :: BitwidthMismatch -> String
show :: BitwidthMismatch -> String
$cshowList :: [BitwidthMismatch] -> ShowS
showList :: [BitwidthMismatch] -> ShowS
Show, BitwidthMismatch -> BitwidthMismatch -> Bool
(BitwidthMismatch -> BitwidthMismatch -> Bool)
-> (BitwidthMismatch -> BitwidthMismatch -> Bool)
-> Eq BitwidthMismatch
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BitwidthMismatch -> BitwidthMismatch -> Bool
== :: BitwidthMismatch -> BitwidthMismatch -> Bool
$c/= :: BitwidthMismatch -> BitwidthMismatch -> Bool
/= :: BitwidthMismatch -> BitwidthMismatch -> Bool
Eq, Eq BitwidthMismatch
Eq BitwidthMismatch =>
(BitwidthMismatch -> BitwidthMismatch -> Ordering)
-> (BitwidthMismatch -> BitwidthMismatch -> Bool)
-> (BitwidthMismatch -> BitwidthMismatch -> Bool)
-> (BitwidthMismatch -> BitwidthMismatch -> Bool)
-> (BitwidthMismatch -> BitwidthMismatch -> Bool)
-> (BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch)
-> (BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch)
-> Ord BitwidthMismatch
BitwidthMismatch -> BitwidthMismatch -> Bool
BitwidthMismatch -> BitwidthMismatch -> Ordering
BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
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 :: BitwidthMismatch -> BitwidthMismatch -> Ordering
compare :: BitwidthMismatch -> BitwidthMismatch -> Ordering
$c< :: BitwidthMismatch -> BitwidthMismatch -> Bool
< :: BitwidthMismatch -> BitwidthMismatch -> Bool
$c<= :: BitwidthMismatch -> BitwidthMismatch -> Bool
<= :: BitwidthMismatch -> BitwidthMismatch -> Bool
$c> :: BitwidthMismatch -> BitwidthMismatch -> Bool
> :: BitwidthMismatch -> BitwidthMismatch -> Bool
$c>= :: BitwidthMismatch -> BitwidthMismatch -> Bool
>= :: BitwidthMismatch -> BitwidthMismatch -> Bool
$cmax :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
max :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
$cmin :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
min :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
Ord, (forall x. BitwidthMismatch -> Rep BitwidthMismatch x)
-> (forall x. Rep BitwidthMismatch x -> BitwidthMismatch)
-> Generic BitwidthMismatch
forall x. Rep BitwidthMismatch x -> BitwidthMismatch
forall x. BitwidthMismatch -> Rep BitwidthMismatch x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. BitwidthMismatch -> Rep BitwidthMismatch x
from :: forall x. BitwidthMismatch -> Rep BitwidthMismatch x
$cto :: forall x. Rep BitwidthMismatch x -> BitwidthMismatch
to :: forall x. Rep BitwidthMismatch x -> BitwidthMismatch
Generic)

instance Exception BitwidthMismatch where
  displayException :: BitwidthMismatch -> String
displayException BitwidthMismatch
BitwidthMismatch = String
"Bit width does not match"

-- |
-- Symbolic unsigned bit vectors.
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)

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

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

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
  String
r0 <- ReadPrec String
look
  case String
r0 of
    (Char
'-' : String
_) -> do
      Char
_ <- ReadPrec Char
get
      a -> a
forall a. Num a => a -> a
negate (a -> a) -> ReadPrec a -> ReadPrec a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadPrec a -> ReadPrec a
forall a. ReadPrec a -> ReadPrec a
parens ReadPrec a
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
      String
_ <- 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"
      Integer -> a
forall a. Num a => Integer -> a
fromInteger (Integer -> a) -> ReadPrec Integer -> ReadPrec a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadP Integer -> ReadPrec Integer
forall a. ReadP a -> ReadPrec a
Text.Read.lift (Integer -> (Char -> Bool) -> (Char -> Int) -> ReadP Integer
forall a. Num a => a -> (Char -> Bool) -> (Char -> Int) -> ReadP a
L.readIntP Integer
2 Char -> Bool
isDigit Char -> Int
forall {a}. Num a => Char -> a
valDigit)

instance (KnownNat n, 1 <= n) => Read (WordN n) where
  readPrec :: ReadPrec (WordN n)
readPrec = (Lexeme -> ReadPrec (WordN n)) -> ReadPrec (WordN n)
forall a. Num a => (Lexeme -> ReadPrec a) -> ReadPrec a
readNumber Lexeme -> ReadPrec (WordN n)
forall a. Num a => Lexeme -> ReadPrec a
convertInt ReadPrec (WordN n) -> ReadPrec (WordN n) -> ReadPrec (WordN n)
forall a. ReadPrec a -> ReadPrec a -> ReadPrec a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ReadPrec (WordN n)
forall a. Num a => ReadPrec a
readBinary
  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

-- |
-- Symbolic signed bit vectors.
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)

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) => Read (IntN n) where
  readPrec :: ReadPrec (IntN n)
readPrec = (Lexeme -> ReadPrec (IntN n)) -> ReadPrec (IntN n)
forall a. Num a => (Lexeme -> ReadPrec a) -> ReadPrec a
readNumber Lexeme -> ReadPrec (IntN n)
forall a. Num a => Lexeme -> ReadPrec a
convertInt ReadPrec (IntN n) -> ReadPrec (IntN n) -> ReadPrec (IntN n)
forall a. ReadPrec a -> ReadPrec a -> ReadPrec a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ReadPrec (IntN n)
forall a. Num a => ReadPrec a
readBinary
  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. 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. 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. 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. 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. HasCallStack => 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)