{-# 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 TemplateHaskellQuotes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -funbox-strict-fields #-}

-- |
-- Module      :   Grisette.Core.Data.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.Core.Data.BV
  ( BitwidthMismatch (..),
    IntN (..),
    WordN (..),
    SomeIntN (..),
    SomeWordN (..),
    unarySomeIntN,
    unarySomeIntNR1,
    binSomeIntN,
    binSomeIntNR1,
    binSomeIntNR2,
    unarySomeWordN,
    unarySomeWordNR1,
    binSomeWordN,
    binSomeWordNR1,
    binSomeWordNR2,
  )
where

import Control.Applicative (Alternative ((<|>)))
import Control.DeepSeq (NFData (rnf))
import Control.Exception
  ( ArithException (Overflow),
    Exception (displayException),
    throw,
  )
import Data.Bits
  ( Bits
      ( bit,
        bitSize,
        bitSizeMaybe,
        clearBit,
        complement,
        complementBit,
        isSigned,
        popCount,
        rotate,
        rotateL,
        rotateR,
        setBit,
        shift,
        shiftL,
        shiftR,
        testBit,
        unsafeShiftL,
        unsafeShiftR,
        xor,
        zeroBits,
        (.&.),
        (.|.)
      ),
    FiniteBits (countLeadingZeros, countTrailingZeros, finiteBitSize),
  )
import Data.Hashable (Hashable (hashWithSalt))
import Data.Maybe (fromMaybe, isJust)
import Data.Proxy (Proxy (Proxy))
import Data.Typeable (type (:~:) (Refl))
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,
    sameNat,
    type (+),
    type (<=),
  )
import Grisette.Core.Data.Class.BitVector
  ( BV (bvConcat, bvExt, bvSelect, bvSext, bvZext),
    BVSignConversion (toSigned, toUnsigned),
    SizedBV (sizedBVConcat, sizedBVExt, sizedBVSelect, sizedBVSext, sizedBVZext),
  )
import Grisette.Utils.Parameterized
  ( KnownProof (KnownProof),
    LeqProof (LeqProof),
    knownAdd,
    leqAddPos,
    unsafeKnownProof,
    unsafeLeqProof,
  )
import Language.Haskell.TH.Syntax (Lift (liftTyped))
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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BitwidthMismatch] -> ShowS
$cshowList :: [BitwidthMismatch] -> ShowS
show :: BitwidthMismatch -> String
$cshow :: BitwidthMismatch -> String
showsPrec :: Int -> BitwidthMismatch -> ShowS
$cshowsPrec :: Int -> BitwidthMismatch -> ShowS
Show, BitwidthMismatch -> BitwidthMismatch -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BitwidthMismatch -> BitwidthMismatch -> Bool
$c/= :: BitwidthMismatch -> BitwidthMismatch -> Bool
== :: BitwidthMismatch -> BitwidthMismatch -> Bool
$c== :: BitwidthMismatch -> BitwidthMismatch -> Bool
Eq, Eq 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
min :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
$cmin :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
max :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
$cmax :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
>= :: BitwidthMismatch -> BitwidthMismatch -> Bool
$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
compare :: BitwidthMismatch -> BitwidthMismatch -> Ordering
$ccompare :: BitwidthMismatch -> BitwidthMismatch -> Ordering
Ord, 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
$cto :: forall x. Rep BitwidthMismatch x -> BitwidthMismatch
$cfrom :: forall x. BitwidthMismatch -> Rep BitwidthMismatch x
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 :: Natural). WordN n -> Integer
unWordN :: Integer}
  deriving (WordN n -> WordN n -> Bool
forall (n :: Natural). WordN n -> WordN n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WordN n -> WordN n -> Bool
$c/= :: forall (n :: Natural). WordN n -> WordN n -> Bool
== :: WordN n -> WordN n -> Bool
$c== :: forall (n :: Natural). WordN n -> WordN n -> Bool
Eq, WordN n -> WordN n -> Bool
WordN n -> WordN n -> Ordering
WordN n -> WordN n -> WordN n
forall (n :: Natural). Eq (WordN n)
forall (n :: Natural). WordN n -> WordN n -> Bool
forall (n :: Natural). WordN n -> WordN n -> Ordering
forall (n :: Natural). 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
min :: WordN n -> WordN n -> WordN n
$cmin :: forall (n :: Natural). WordN n -> WordN n -> WordN n
max :: WordN n -> WordN n -> WordN n
$cmax :: forall (n :: Natural). WordN n -> WordN n -> WordN n
>= :: WordN n -> WordN n -> Bool
$c>= :: forall (n :: Natural). WordN n -> WordN n -> Bool
> :: WordN n -> WordN n -> Bool
$c> :: forall (n :: Natural). WordN n -> WordN n -> Bool
<= :: WordN n -> WordN n -> Bool
$c<= :: forall (n :: Natural). WordN n -> WordN n -> Bool
< :: WordN n -> WordN n -> Bool
$c< :: forall (n :: Natural). WordN n -> WordN n -> Bool
compare :: WordN n -> WordN n -> Ordering
$ccompare :: forall (n :: Natural). WordN n -> WordN n -> Ordering
Ord, forall (n :: Natural) x. Rep (WordN n) x -> WordN n
forall (n :: Natural) x. WordN n -> Rep (WordN n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (n :: Natural) x. Rep (WordN n) x -> WordN n
$cfrom :: forall (n :: Natural) x. WordN n -> Rep (WordN n) x
Generic, forall (n :: Natural) (m :: * -> *). Quote m => WordN n -> m Exp
forall (n :: Natural) (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)
liftTyped :: forall (m :: * -> *). Quote m => WordN n -> Code m (WordN n)
$cliftTyped :: forall (n :: Natural) (m :: * -> *).
Quote m =>
WordN n -> Code m (WordN n)
lift :: forall (m :: * -> *). Quote m => WordN n -> m Exp
$clift :: forall (n :: Natural) (m :: * -> *). Quote m => WordN n -> m Exp
Lift, Int -> WordN n -> Int
WordN n -> Int
forall (n :: Natural). Eq (WordN n)
forall (n :: Natural). Int -> WordN n -> Int
forall (n :: Natural). WordN n -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: WordN n -> Int
$chash :: forall (n :: Natural). WordN n -> Int
hashWithSalt :: Int -> WordN n -> Int
$chashWithSalt :: forall (n :: Natural). Int -> WordN n -> Int
Hashable, WordN n -> ()
forall (n :: Natural). WordN n -> ()
forall a. (a -> ()) -> NFData a
rnf :: WordN n -> ()
$crnf :: forall (n :: Natural). WordN n -> ()
NFData)

-- |
-- A non-indexed version of 'WordN'.
data SomeWordN where
  SomeWordN :: (KnownNat n, 1 <= n) => WordN n -> SomeWordN

unarySomeWordN :: (forall n. (KnownNat n, 1 <= n) => WordN n -> r) -> SomeWordN -> r
unarySomeWordN :: forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> r
op (SomeWordN (WordN n
w :: WordN w)) = forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> r
op WordN n
w
{-# INLINE unarySomeWordN #-}

unarySomeWordNR1 :: (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n) -> SomeWordN -> SomeWordN
unarySomeWordNR1 :: (forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n
op (SomeWordN (WordN n
w :: WordN w)) = forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n
op WordN n
w
{-# INLINE unarySomeWordNR1 #-}

binSomeWordN :: (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> r) -> SomeWordN -> SomeWordN -> r
binSomeWordN :: forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN forall (n :: Natural).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> r
op (SomeWordN (WordN n
l :: WordN l)) (SomeWordN (WordN n
r :: WordN r)) =
  case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl -> forall (n :: Natural).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> r
op WordN n
l WordN n
r
    Maybe (n :~: n)
Nothing -> forall a e. Exception e => e -> a
throw BitwidthMismatch
BitwidthMismatch
{-# INLINE binSomeWordN #-}

binSomeWordNR1 :: (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> WordN n) -> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 :: (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall (n :: Natural).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
op (SomeWordN (WordN n
l :: WordN l)) (SomeWordN (WordN n
r :: WordN r)) =
  case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl -> forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
op WordN n
l WordN n
r
    Maybe (n :~: n)
Nothing -> forall a e. Exception e => e -> a
throw BitwidthMismatch
BitwidthMismatch
{-# INLINE binSomeWordNR1 #-}

binSomeWordNR2 :: (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> (WordN n, WordN n)) -> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
binSomeWordNR2 :: (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> (WordN n, WordN n))
-> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
binSomeWordNR2 forall (n :: Natural).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> (WordN n, WordN n)
op (SomeWordN (WordN n
l :: WordN l)) (SomeWordN (WordN n
r :: WordN r)) =
  case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl ->
      case forall (n :: Natural).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> (WordN n, WordN n)
op WordN n
l WordN n
r of
        (WordN n
a, WordN n
b) -> (forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN WordN n
a, forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN WordN n
b)
    Maybe (n :~: n)
Nothing -> forall a e. Exception e => e -> a
throw BitwidthMismatch
BitwidthMismatch
{-# INLINE binSomeWordNR2 #-}

instance Eq SomeWordN where
  SomeWordN (WordN n
l :: WordN l) == :: SomeWordN -> SomeWordN -> Bool
== SomeWordN (WordN n
r :: WordN r) =
    case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
      Just n :~: n
Refl -> WordN n
l forall a. Eq a => a -> a -> Bool
== WordN n
r
      Maybe (n :~: n)
Nothing -> Bool
False
  {-# INLINE (==) #-}
  SomeWordN (WordN n
l :: WordN l) /= :: SomeWordN -> SomeWordN -> Bool
/= SomeWordN (WordN n
r :: WordN r) =
    case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
      Just n :~: n
Refl -> WordN n
l forall a. Eq a => a -> a -> Bool
/= WordN n
r
      Maybe (n :~: n)
Nothing -> Bool
True
  {-# INLINE (/=) #-}

instance Ord SomeWordN where
  <= :: SomeWordN -> SomeWordN -> Bool
(<=) = forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN forall a. Ord a => a -> a -> Bool
(<=)
  {-# INLINE (<=) #-}
  < :: SomeWordN -> SomeWordN -> Bool
(<) = forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN forall a. Ord a => a -> a -> Bool
(<)
  {-# INLINE (<) #-}
  >= :: SomeWordN -> SomeWordN -> Bool
(>=) = forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN forall a. Ord a => a -> a -> Bool
(>=)
  {-# INLINE (>=) #-}
  > :: SomeWordN -> SomeWordN -> Bool
(>) = forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN forall a. Ord a => a -> a -> Bool
(>)
  {-# INLINE (>) #-}
  max :: SomeWordN -> SomeWordN -> SomeWordN
max = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Ord a => a -> a -> a
max
  {-# INLINE max #-}
  min :: SomeWordN -> SomeWordN -> SomeWordN
min = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Ord a => a -> a -> a
min
  {-# INLINE min #-}
  compare :: SomeWordN -> SomeWordN -> Ordering
compare = forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN forall a. Ord a => a -> a -> Ordering
compare
  {-# INLINE compare #-}

instance Lift SomeWordN where
  liftTyped :: forall (m :: * -> *). Quote m => SomeWordN -> Code m SomeWordN
liftTyped (SomeWordN WordN n
w) = [||SomeWordN w||]

instance Hashable SomeWordN where
  Int
s hashWithSalt :: Int -> SomeWordN -> Int
`hashWithSalt` (SomeWordN (WordN n
w :: WordN n)) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy @n) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` WordN n
w

instance NFData SomeWordN where
  rnf :: SomeWordN -> ()
rnf (SomeWordN WordN n
w) = forall a. NFData a => a -> ()
rnf WordN n
w

instance (KnownNat n, 1 <= n) => Show (WordN n) where
  show :: WordN n -> String
show (WordN Integer
w) = if (Natural
bitwidth forall a. Integral a => a -> a -> a
`mod` Natural
4) forall a. Eq a => a -> a -> Bool
== Natural
0 then String
hexRepPre forall a. [a] -> [a] -> [a]
++ String
hexRep else String
binRepPre forall a. [a] -> [a] -> [a]
++ String
binRep
    where
      bitwidth :: Natural
bitwidth = forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
      hexRepPre :: String
hexRepPre = String
"0x" forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural
bitwidth forall a. Integral a => a -> a -> a
`div` Natural
4) forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length String
hexRep) Char
'0'
      hexRep :: String
hexRep = forall a. (Integral a, Show a) => a -> ShowS
showHex Integer
w String
""
      binRepPre :: String
binRepPre = String
"0b" forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate (forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
bitwidth forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length String
binRep) Char
'0'
      binRep :: String
binRep = forall a. (Integral a, Show a) => a -> (Int -> Char) -> a -> ShowS
showIntAtBase Integer
2 (\Int
x -> if Int
x 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 = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Num a => Integer -> a
fromInteger Integer
i)
convertInt Lexeme
_ = forall a. ReadPrec a
pfail

readBinary :: (Num a) => ReadPrec a
readBinary :: forall a. Num a => ReadPrec a
readBinary = forall a. ReadPrec a -> ReadPrec a
parens forall a b. (a -> b) -> a -> b
$ do
  String
r0 <- ReadPrec String
look
  case String
r0 of
    (Char
'-' : String
_) -> do
      Char
_ <- ReadPrec Char
get
      forall a. Num a => a -> a
negate forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ReadPrec a -> ReadPrec a
parens ReadPrec a
parse0b
    String
_ -> ReadPrec a
parse0b
  where
    isDigit :: Char -> Bool
isDigit Char
c = forall a. Maybe a -> Bool
isJust (forall {a}. Num a => Char -> Maybe a
valDig Char
c)
    valDigit :: Char -> a
valDigit Char
c = forall a. a -> Maybe a -> a
fromMaybe a
0 (forall {a}. Num a => Char -> Maybe a
valDig Char
c)
    valDig :: Char -> Maybe a
valDig Char
'0' = forall a. a -> Maybe a
Just a
0
    valDig Char
'1' = forall a. a -> Maybe a
Just a
1
    valDig Char
_ = forall a. Maybe a
Nothing
    parse0b :: ReadPrec a
parse0b = do
      String
_ <- forall a. ReadP a -> ReadPrec a
Text.Read.lift forall a b. (a -> b) -> a -> b
$ String -> ReadP String
string String
"0b"
      forall a. Num a => Integer -> a
fromInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ReadP a -> ReadPrec a
Text.Read.lift (forall a. Num a => a -> (Char -> Bool) -> (Char -> Int) -> ReadP a
L.readIntP Integer
2 Char -> Bool
isDigit forall {a}. Num a => Char -> a
valDigit)

instance (KnownNat n, 1 <= n) => Read (WordN n) where
  readPrec :: ReadPrec (WordN n)
readPrec = forall a. Num a => (Lexeme -> ReadPrec a) -> ReadPrec a
readNumber forall a. Num a => Lexeme -> ReadPrec a
convertInt forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Num a => ReadPrec a
readBinary
  readListPrec :: ReadPrec [WordN n]
readListPrec = forall a. Read a => ReadPrec [a]
readListPrecDefault
  readList :: ReadS [WordN n]
readList = forall a. Read a => ReadS [a]
readListDefault

instance Show SomeWordN where
  show :: SomeWordN -> String
show (SomeWordN WordN n
w) = forall a. Show a => a -> String
show WordN n
w

-- |
-- Symbolic signed bit vectors.
newtype IntN (n :: Nat) = IntN {forall (n :: Natural). IntN n -> Integer
unIntN :: Integer}
  deriving (IntN n -> IntN n -> Bool
forall (n :: Natural). IntN n -> IntN n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IntN n -> IntN n -> Bool
$c/= :: forall (n :: Natural). IntN n -> IntN n -> Bool
== :: IntN n -> IntN n -> Bool
$c== :: forall (n :: Natural). IntN n -> IntN n -> Bool
Eq, forall (n :: Natural) x. Rep (IntN n) x -> IntN n
forall (n :: Natural) x. IntN n -> Rep (IntN n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (n :: Natural) x. Rep (IntN n) x -> IntN n
$cfrom :: forall (n :: Natural) x. IntN n -> Rep (IntN n) x
Generic, forall (n :: Natural) (m :: * -> *). Quote m => IntN n -> m Exp
forall (n :: Natural) (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)
liftTyped :: forall (m :: * -> *). Quote m => IntN n -> Code m (IntN n)
$cliftTyped :: forall (n :: Natural) (m :: * -> *).
Quote m =>
IntN n -> Code m (IntN n)
lift :: forall (m :: * -> *). Quote m => IntN n -> m Exp
$clift :: forall (n :: Natural) (m :: * -> *). Quote m => IntN n -> m Exp
Lift, Int -> IntN n -> Int
IntN n -> Int
forall (n :: Natural). Eq (IntN n)
forall (n :: Natural). Int -> IntN n -> Int
forall (n :: Natural). IntN n -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: IntN n -> Int
$chash :: forall (n :: Natural). IntN n -> Int
hashWithSalt :: Int -> IntN n -> Int
$chashWithSalt :: forall (n :: Natural). Int -> IntN n -> Int
Hashable, IntN n -> ()
forall (n :: Natural). IntN n -> ()
forall a. (a -> ()) -> NFData a
rnf :: IntN n -> ()
$crnf :: forall (n :: Natural). IntN n -> ()
NFData)

-- |
-- A non-indexed version of 'IntN'.
data SomeIntN where
  SomeIntN :: (KnownNat n, 1 <= n) => IntN n -> SomeIntN

unarySomeIntN :: (forall n. (KnownNat n, 1 <= n) => IntN n -> r) -> SomeIntN -> r
unarySomeIntN :: forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> r
op (SomeIntN (IntN n
w :: IntN w)) = forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> r
op IntN n
w
{-# INLINE unarySomeIntN #-}

unarySomeIntNR1 :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n) -> SomeIntN -> SomeIntN
unarySomeIntNR1 :: (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n
op (SomeIntN (IntN n
w :: IntN w)) = forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n
op IntN n
w
{-# INLINE unarySomeIntNR1 #-}

binSomeIntN :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n -> r) -> SomeIntN -> SomeIntN -> r
binSomeIntN :: forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN forall (n :: Natural).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> r
op (SomeIntN (IntN n
l :: IntN l)) (SomeIntN (IntN n
r :: IntN r)) =
  case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl -> forall (n :: Natural).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> r
op IntN n
l IntN n
r
    Maybe (n :~: n)
Nothing -> forall a e. Exception e => e -> a
throw BitwidthMismatch
BitwidthMismatch
{-# INLINE binSomeIntN #-}

binSomeIntNR1 :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n -> IntN n) -> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 :: (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall (n :: Natural).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
op (SomeIntN (IntN n
l :: IntN l)) (SomeIntN (IntN n
r :: IntN r)) =
  case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl -> forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
op IntN n
l IntN n
r
    Maybe (n :~: n)
Nothing -> forall a e. Exception e => e -> a
throw BitwidthMismatch
BitwidthMismatch
{-# INLINE binSomeIntNR1 #-}

binSomeIntNR2 :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n -> (IntN n, IntN n)) -> SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
binSomeIntNR2 :: (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> (IntN n, IntN n))
-> SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
binSomeIntNR2 forall (n :: Natural).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> (IntN n, IntN n)
op (SomeIntN (IntN n
l :: IntN l)) (SomeIntN (IntN n
r :: IntN r)) =
  case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl ->
      case forall (n :: Natural).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> (IntN n, IntN n)
op IntN n
l IntN n
r of
        (IntN n
a, IntN n
b) -> (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN IntN n
a, forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN IntN n
b)
    Maybe (n :~: n)
Nothing -> forall a e. Exception e => e -> a
throw BitwidthMismatch
BitwidthMismatch
{-# INLINE binSomeIntNR2 #-}

instance Eq SomeIntN where
  SomeIntN (IntN n
l :: IntN l) == :: SomeIntN -> SomeIntN -> Bool
== SomeIntN (IntN n
r :: IntN r) =
    case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
      Just n :~: n
Refl -> IntN n
l forall a. Eq a => a -> a -> Bool
== IntN n
r
      Maybe (n :~: n)
Nothing -> Bool
False
  {-# INLINE (==) #-}
  SomeIntN (IntN n
l :: IntN l) /= :: SomeIntN -> SomeIntN -> Bool
/= SomeIntN (IntN n
r :: IntN r) =
    case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
      Just n :~: n
Refl -> IntN n
l forall a. Eq a => a -> a -> Bool
/= IntN n
r
      Maybe (n :~: n)
Nothing -> Bool
True
  {-# INLINE (/=) #-}

instance Ord SomeIntN where
  <= :: SomeIntN -> SomeIntN -> Bool
(<=) = forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN forall a. Ord a => a -> a -> Bool
(<=)
  {-# INLINE (<=) #-}
  < :: SomeIntN -> SomeIntN -> Bool
(<) = forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN forall a. Ord a => a -> a -> Bool
(<)
  {-# INLINE (<) #-}
  >= :: SomeIntN -> SomeIntN -> Bool
(>=) = forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN forall a. Ord a => a -> a -> Bool
(>=)
  {-# INLINE (>=) #-}
  > :: SomeIntN -> SomeIntN -> Bool
(>) = forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN forall a. Ord a => a -> a -> Bool
(>)
  {-# INLINE (>) #-}
  max :: SomeIntN -> SomeIntN -> SomeIntN
max = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Ord a => a -> a -> a
max
  {-# INLINE max #-}
  min :: SomeIntN -> SomeIntN -> SomeIntN
min = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Ord a => a -> a -> a
min
  {-# INLINE min #-}
  compare :: SomeIntN -> SomeIntN -> Ordering
compare = forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN forall a. Ord a => a -> a -> Ordering
compare
  {-# INLINE compare #-}

instance Lift SomeIntN where
  liftTyped :: forall (m :: * -> *). Quote m => SomeIntN -> Code m SomeIntN
liftTyped (SomeIntN IntN n
w) = [||SomeIntN w||]

instance Hashable SomeIntN where
  Int
s hashWithSalt :: Int -> SomeIntN -> Int
`hashWithSalt` (SomeIntN (IntN n
w :: IntN n)) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy @n) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` IntN n
w

instance NFData SomeIntN where
  rnf :: SomeIntN -> ()
rnf (SomeIntN IntN n
w) = forall a. NFData a => a -> ()
rnf IntN n
w

instance (KnownNat n, 1 <= n) => Show (IntN n) where
  show :: IntN n -> String
show (IntN Integer
w) = if (Natural
bitwidth forall a. Integral a => a -> a -> a
`mod` Natural
4) forall a. Eq a => a -> a -> Bool
== Natural
0 then String
hexRepPre forall a. [a] -> [a] -> [a]
++ String
hexRep else String
binRepPre forall a. [a] -> [a] -> [a]
++ String
binRep
    where
      bitwidth :: Natural
bitwidth = forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
      hexRepPre :: String
hexRepPre = String
"0x" forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural
bitwidth forall a. Integral a => a -> a -> a
`div` Natural
4) forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length String
hexRep) Char
'0'
      hexRep :: String
hexRep = forall a. (Integral a, Show a) => a -> ShowS
showHex Integer
w String
""
      binRepPre :: String
binRepPre = String
"0b" forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate (forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
bitwidth forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length String
binRep) Char
'0'
      binRep :: String
binRep = forall a. (Integral a, Show a) => a -> (Int -> Char) -> a -> ShowS
showIntAtBase Integer
2 (\Int
x -> if Int
x 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 = forall a. Num a => (Lexeme -> ReadPrec a) -> ReadPrec a
readNumber forall a. Num a => Lexeme -> ReadPrec a
convertInt forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Num a => ReadPrec a
readBinary
  readListPrec :: ReadPrec [IntN n]
readListPrec = forall a. Read a => ReadPrec [a]
readListPrecDefault
  readList :: ReadS [IntN n]
readList = forall a. Read a => ReadS [a]
readListDefault

instance Show SomeIntN where
  show :: SomeIntN -> String
show (SomeIntN IntN n
w) = forall a. Show a => a -> String
show IntN n
w

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

  -- shift use default implementation
  -- rotate use default implementation
  zeroBits :: WordN n
zeroBits = forall (n :: Natural). Integer -> WordN n
WordN Integer
0
  bit :: Int -> WordN n
bit Int
i
    | Int
i forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
i forall a. Ord a => a -> a -> Bool
>= forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) = forall a. Bits a => a
zeroBits
    | Bool
otherwise = forall (n :: Natural). Integer -> WordN n
WordN (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 = forall (n :: Natural). Integer -> WordN n
WordN (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) = forall a. Bits a => a -> Int -> Bool
testBit Integer
a
  bitSizeMaybe :: WordN n -> Maybe Int
bitSizeMaybe = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b. FiniteBits b => b -> Int
finiteBitSize
  bitSize :: WordN n -> Int
bitSize = forall b. FiniteBits b => b -> Int
finiteBitSize
  isSigned :: WordN n -> Bool
isSigned WordN n
_ = Bool
False
  shiftL :: WordN n -> Int -> WordN n
shiftL (WordN Integer
a) Int
i = forall (n :: Natural). Integer -> WordN n
WordN (Integer
a forall a. Bits a => a -> Int -> a
`shiftL` Int
i) forall a. Bits a => a -> a -> a
.&. forall a. Bounded a => a
maxBound

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

instance Bits SomeWordN where
  .&. :: SomeWordN -> SomeWordN -> SomeWordN
(.&.) = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Bits a => a -> a -> a
(.&.)
  .|. :: SomeWordN -> SomeWordN -> SomeWordN
(.|.) = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Bits a => a -> a -> a
(.|.)
  xor :: SomeWordN -> SomeWordN -> SomeWordN
xor = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Bits a => a -> a -> a
xor
  complement :: SomeWordN -> SomeWordN
complement = (forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 forall a. Bits a => a -> a
complement
  shift :: SomeWordN -> Int -> SomeWordN
shift SomeWordN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`shift` Int
i) SomeWordN
s
  rotate :: SomeWordN -> Int -> SomeWordN
rotate SomeWordN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`rotate` Int
i) SomeWordN
s
  zeroBits :: SomeWordN
zeroBits = forall a. HasCallStack => String -> a
error String
"zeroBits is not defined for SomeWordN as no bitwidth is known"
  bit :: Int -> SomeWordN
bit = forall a. HasCallStack => String -> a
error String
"bit is not defined for SomeWordN as no bitwidth is known"
  setBit :: SomeWordN -> Int -> SomeWordN
setBit SomeWordN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`setBit` Int
i) SomeWordN
s
  clearBit :: SomeWordN -> Int -> SomeWordN
clearBit SomeWordN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`clearBit` Int
i) SomeWordN
s
  complementBit :: SomeWordN -> Int -> SomeWordN
complementBit SomeWordN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`complementBit` Int
i) SomeWordN
s
  testBit :: SomeWordN -> Int -> Bool
testBit SomeWordN
s Int
i = forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN (forall a. Bits a => a -> Int -> Bool
`testBit` Int
i) SomeWordN
s
  bitSizeMaybe :: SomeWordN -> Maybe Int
bitSizeMaybe = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b. FiniteBits b => b -> Int
finiteBitSize
  bitSize :: SomeWordN -> Int
bitSize = forall b. FiniteBits b => b -> Int
finiteBitSize
  isSigned :: SomeWordN -> Bool
isSigned SomeWordN
_ = Bool
False
  shiftL :: SomeWordN -> Int -> SomeWordN
shiftL SomeWordN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`shiftL` Int
i) SomeWordN
s
  unsafeShiftL :: SomeWordN -> Int -> SomeWordN
unsafeShiftL SomeWordN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`unsafeShiftL` Int
i) SomeWordN
s
  shiftR :: SomeWordN -> Int -> SomeWordN
shiftR SomeWordN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`shiftR` Int
i) SomeWordN
s
  unsafeShiftR :: SomeWordN -> Int -> SomeWordN
unsafeShiftR SomeWordN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`unsafeShiftR` Int
i) SomeWordN
s
  rotateL :: SomeWordN -> Int -> SomeWordN
rotateL SomeWordN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`rotateL` Int
i) SomeWordN
s
  rotateR :: SomeWordN -> Int -> SomeWordN
rotateR SomeWordN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`rotateR` Int
i) SomeWordN
s
  popCount :: SomeWordN -> Int
popCount = forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN forall a. Bits a => a -> Int
popCount

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

instance FiniteBits SomeWordN where
  finiteBitSize :: SomeWordN -> Int
finiteBitSize (SomeWordN (WordN n
n :: WordN n)) = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal WordN n
n
  countLeadingZeros :: SomeWordN -> Int
countLeadingZeros = forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN forall b. FiniteBits b => b -> Int
countLeadingZeros
  countTrailingZeros :: SomeWordN -> Int
countTrailingZeros = forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN forall b. FiniteBits b => b -> Int
countTrailingZeros

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

instance Enum SomeWordN where
  toEnum :: Int -> SomeWordN
toEnum = forall a. HasCallStack => String -> a
error String
"SomeWordN is not really a Enum type as the bit width is unknown, please consider using WordN instead"
  fromEnum :: SomeWordN -> Int
fromEnum = forall a. HasCallStack => String -> a
error String
"SomeWordN is not really a Enum type as the bit width is unknown, please consider using WordN instead"

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

instance Real SomeWordN where
  toRational :: SomeWordN -> Rational
toRational = forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN forall a. Real a => a -> Rational
toRational

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

instance Integral SomeWordN where
  quot :: SomeWordN -> SomeWordN -> SomeWordN
quot = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Integral a => a -> a -> a
quot
  rem :: SomeWordN -> SomeWordN -> SomeWordN
rem = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Integral a => a -> a -> a
rem
  quotRem :: SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
quotRem = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> (WordN n, WordN n))
-> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
binSomeWordNR2 forall a. Integral a => a -> a -> (a, a)
quotRem
  div :: SomeWordN -> SomeWordN -> SomeWordN
div = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Integral a => a -> a -> a
div
  mod :: SomeWordN -> SomeWordN -> SomeWordN
mod = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Integral a => a -> a -> a
mod
  divMod :: SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
divMod = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> (WordN n, WordN n))
-> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
binSomeWordNR2 forall a. Integral a => a -> a -> (a, a)
divMod
  toInteger :: SomeWordN -> Integer
toInteger = forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN forall a. Integral a => a -> Integer
toInteger

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

instance Num SomeWordN where
  + :: SomeWordN -> SomeWordN -> SomeWordN
(+) = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Num a => a -> a -> a
(+)
  (-) = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 (-)
  * :: SomeWordN -> SomeWordN -> SomeWordN
(*) = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Num a => a -> a -> a
(*)
  negate :: SomeWordN -> SomeWordN
negate = (forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 forall a. Num a => a -> a
negate
  abs :: SomeWordN -> SomeWordN
abs = (forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 forall a. Num a => a -> a
abs
  signum :: SomeWordN -> SomeWordN
signum = (forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 forall a. Num a => a -> a
signum
  fromInteger :: Integer -> SomeWordN
fromInteger = forall a. HasCallStack => String -> a
error String
"fromInteger is not defined for SomeWordN as no bitwidth is known"

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

minusOneIntN :: forall proxy n. (KnownNat n) => proxy n -> IntN n
minusOneIntN :: forall (proxy :: Natural -> *) (n :: Natural).
KnownNat n =>
proxy n -> IntN n
minusOneIntN proxy n
_ = forall (n :: Natural). Integer -> IntN n
IntN (Integer
1 forall a. Bits a => a -> Int -> a
`shiftL` forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) 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 = forall (n :: Natural). Integer -> IntN n
IntN (Integer
a forall a. Bits a => a -> a -> a
.&. Integer
b)
  IntN Integer
a .|. :: IntN n -> IntN n -> IntN n
.|. IntN Integer
b = forall (n :: Natural). Integer -> IntN n
IntN (Integer
a forall a. Bits a => a -> a -> a
.|. Integer
b)
  IntN Integer
a xor :: IntN n -> IntN n -> IntN n
`xor` IntN Integer
b = forall (n :: Natural). Integer -> IntN n
IntN (Integer
a forall a. Bits a => a -> a -> a
`xor` Integer
b)
  complement :: IntN n -> IntN n
complement IntN n
a = forall (proxy :: Natural -> *) (n :: Natural).
KnownNat n =>
proxy n -> IntN n
minusOneIntN (forall {k} (t :: k). Proxy t
Proxy :: Proxy n) forall a. Bits a => a -> a -> a
`xor` IntN n
a

  -- shift use default implementation
  -- rotate use default implementation
  zeroBits :: IntN n
zeroBits = forall (n :: Natural). Integer -> IntN n
IntN Integer
0
  bit :: Int -> IntN n
bit Int
i = forall (n :: Natural). Integer -> IntN n
IntN (forall (n :: Natural). WordN n -> Integer
unWordN (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 = forall (n :: Natural). Integer -> IntN n
IntN (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) = forall a. Bits a => a -> Int -> Bool
testBit Integer
a
  bitSizeMaybe :: IntN n -> Maybe Int
bitSizeMaybe = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b. FiniteBits b => b -> Int
finiteBitSize
  bitSize :: IntN n -> Int
bitSize = 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 = forall (n :: Natural). Integer -> IntN n
IntN (forall (n :: Natural). WordN n -> Integer
unWordN forall a b. (a -> b) -> a -> b
$ (forall (n :: Natural). Integer -> WordN n
WordN Integer
a :: 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 forall a. Ord a => a -> a -> Bool
>= Int
n = if Bool
b then forall (n :: Natural). Integer -> IntN n
IntN (Integer
maxi forall a. Num a => a -> a -> a
- Integer
1) else forall (n :: Natural). Integer -> IntN n
IntN Integer
0
    | Bool
otherwise = if Bool
b then forall (n :: Natural). Integer -> IntN n
IntN (Integer
maxi forall a. Num a => a -> a -> a
- Integer
noi forall a. Num a => a -> a -> a
+ (Integer
i forall a. Bits a => a -> Int -> a
`shiftR` Int
k)) else forall (n :: Natural). Integer -> IntN n
IntN (Integer
i forall a. Bits a => a -> Int -> a
`shiftR` Int
k)
    where
      b :: Bool
b = forall a. Bits a => a -> Int -> Bool
testBit Integer
i (Int
n forall a. Num a => a -> a -> a
- Int
1)
      n :: Int
n = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
      maxi :: Integer
maxi = (Integer
1 :: Integer) forall a. Bits a => a -> Int -> a
`shiftL` Int
n
      noi :: Integer
noi = (Integer
1 :: Integer) forall a. Bits a => a -> Int -> a
`shiftL` (Int
n 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 = forall (n :: Natural). Integer -> IntN n
IntN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). WordN n -> Integer
unWordN forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> Int -> a
rotateL (forall (n :: Natural). Integer -> WordN n
WordN Integer
i :: WordN n) Int
k
  rotateR :: IntN n -> Int -> IntN n
rotateR (IntN Integer
i) Int
k = forall (n :: Natural). Integer -> IntN n
IntN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). WordN n -> Integer
unWordN forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> Int -> a
rotateR (forall (n :: Natural). Integer -> WordN n
WordN Integer
i :: WordN n) Int
k
  popCount :: IntN n -> Int
popCount (IntN Integer
i) = forall a. Bits a => a -> Int
popCount Integer
i

instance Bits SomeIntN where
  .&. :: SomeIntN -> SomeIntN -> SomeIntN
(.&.) = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Bits a => a -> a -> a
(.&.)
  .|. :: SomeIntN -> SomeIntN -> SomeIntN
(.|.) = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Bits a => a -> a -> a
(.|.)
  xor :: SomeIntN -> SomeIntN -> SomeIntN
xor = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Bits a => a -> a -> a
xor
  complement :: SomeIntN -> SomeIntN
complement = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 forall a. Bits a => a -> a
complement
  shift :: SomeIntN -> Int -> SomeIntN
shift SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`shift` Int
i) SomeIntN
s
  rotate :: SomeIntN -> Int -> SomeIntN
rotate SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`rotate` Int
i) SomeIntN
s
  zeroBits :: SomeIntN
zeroBits = forall a. HasCallStack => String -> a
error String
"zeroBits is not defined for SomeIntN as no bitwidth is known"
  bit :: Int -> SomeIntN
bit = forall a. HasCallStack => String -> a
error String
"bit is not defined for SomeIntN as no bitwidth is known"
  setBit :: SomeIntN -> Int -> SomeIntN
setBit SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`setBit` Int
i) SomeIntN
s
  clearBit :: SomeIntN -> Int -> SomeIntN
clearBit SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`clearBit` Int
i) SomeIntN
s
  complementBit :: SomeIntN -> Int -> SomeIntN
complementBit SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`complementBit` Int
i) SomeIntN
s
  testBit :: SomeIntN -> Int -> Bool
testBit SomeIntN
s Int
i = forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN (forall a. Bits a => a -> Int -> Bool
`testBit` Int
i) SomeIntN
s
  bitSizeMaybe :: SomeIntN -> Maybe Int
bitSizeMaybe = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b. FiniteBits b => b -> Int
finiteBitSize
  bitSize :: SomeIntN -> Int
bitSize = forall b. FiniteBits b => b -> Int
finiteBitSize
  isSigned :: SomeIntN -> Bool
isSigned SomeIntN
_ = Bool
False
  shiftL :: SomeIntN -> Int -> SomeIntN
shiftL SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`shiftL` Int
i) SomeIntN
s
  unsafeShiftL :: SomeIntN -> Int -> SomeIntN
unsafeShiftL SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`unsafeShiftL` Int
i) SomeIntN
s
  shiftR :: SomeIntN -> Int -> SomeIntN
shiftR SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`shiftR` Int
i) SomeIntN
s
  unsafeShiftR :: SomeIntN -> Int -> SomeIntN
unsafeShiftR SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`unsafeShiftR` Int
i) SomeIntN
s
  rotateL :: SomeIntN -> Int -> SomeIntN
rotateL SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`rotateL` Int
i) SomeIntN
s
  rotateR :: SomeIntN -> Int -> SomeIntN
rotateR SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`rotateR` Int
i) SomeIntN
s
  popCount :: SomeIntN -> Int
popCount = forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN forall a. Bits a => a -> Int
popCount

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

instance FiniteBits SomeIntN where
  finiteBitSize :: SomeIntN -> Int
finiteBitSize (SomeIntN (IntN n
n :: IntN n)) = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal IntN n
n
  countLeadingZeros :: SomeIntN -> Int
countLeadingZeros = forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN forall b. FiniteBits b => b -> Int
countLeadingZeros
  countTrailingZeros :: SomeIntN -> Int
countTrailingZeros = forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN forall b. FiniteBits b => b -> Int
countTrailingZeros

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

instance Enum SomeIntN where
  toEnum :: Int -> SomeIntN
toEnum = forall a. HasCallStack => String -> a
error String
"SomeIntN is not really a Enum type as the bit width is unknown, please consider using IntN instead"
  fromEnum :: SomeIntN -> Int
fromEnum = forall a. HasCallStack => String -> a
error String
"SomeIntN is not really a Enum type as the bit width is unknown, please consider using IntN instead"

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

instance Real SomeIntN where
  toRational :: SomeIntN -> Rational
toRational = forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN forall a. Real a => a -> Rational
toRational

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

instance Integral SomeIntN where
  quot :: SomeIntN -> SomeIntN -> SomeIntN
quot = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Integral a => a -> a -> a
quot
  rem :: SomeIntN -> SomeIntN -> SomeIntN
rem = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Integral a => a -> a -> a
rem
  quotRem :: SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
quotRem = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> (IntN n, IntN n))
-> SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
binSomeIntNR2 forall a. Integral a => a -> a -> (a, a)
quotRem
  div :: SomeIntN -> SomeIntN -> SomeIntN
div = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Integral a => a -> a -> a
div
  mod :: SomeIntN -> SomeIntN -> SomeIntN
mod = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Integral a => a -> a -> a
mod
  divMod :: SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
divMod = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> (IntN n, IntN n))
-> SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
binSomeIntNR2 forall a. Integral a => a -> a -> (a, a)
divMod
  toInteger :: SomeIntN -> Integer
toInteger = forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN forall a. Integral a => a -> Integer
toInteger

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

instance Num SomeIntN where
  + :: SomeIntN -> SomeIntN -> SomeIntN
(+) = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Num a => a -> a -> a
(+)
  (-) = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 (-)
  * :: SomeIntN -> SomeIntN -> SomeIntN
(*) = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Num a => a -> a -> a
(*)
  negate :: SomeIntN -> SomeIntN
negate = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 forall a. Num a => a -> a
negate
  abs :: SomeIntN -> SomeIntN
abs = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 forall a. Num a => a -> a
abs
  signum :: SomeIntN -> SomeIntN
signum = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 forall a. Num a => a -> a
signum
  fromInteger :: Integer -> SomeIntN
fromInteger = forall a. HasCallStack => String -> a
error String
"fromInteger is not defined for SomeIntN as no bitwidth is known"

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 forall a. Ord a => a -> a -> Bool
<= Integer
b
    where
      n :: Int
n = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
      as :: Bool
as = forall a. Bits a => a -> Int -> Bool
testBit Integer
a (Int
n forall a. Num a => a -> a -> a
- Int
1)
      bs :: Bool
bs = forall a. Bits a => a -> Int -> Bool
testBit Integer
b (Int
n forall a. Num a => a -> a -> a
- Int
1)

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

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 :: Natural) (r :: Natural).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
WordN l -> WordN r -> WordN (l + r)
sizedBVConcat (WordN Integer
a) (WordN Integer
b) = forall (n :: Natural). Integer -> WordN n
WordN ((Integer
a forall a. Bits a => a -> Int -> a
`shiftL` forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy r))) forall a. Bits a => a -> a -> a
.|. Integer
b)
  sizedBVZext :: forall (l :: Natural) (r :: Natural) (proxy :: Natural -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
sizedBVZext proxy r
_ (WordN Integer
v) = forall (n :: Natural). 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 :: Natural) (r :: Natural) (proxy :: Natural -> *).
(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 forall (n :: Natural). Integer -> WordN n
WordN (Integer
maxi forall a. Num a => a -> a -> a
- Integer
noi forall a. Num a => a -> a -> a
+ Integer
v) else forall (n :: Natural). Integer -> WordN n
WordN Integer
v
    where
      r :: Int
r = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal proxy r
pr
      l :: Int
l = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy l)
      s :: Bool
s = forall a. Bits a => a -> Int -> Bool
testBit Integer
v (Int
l forall a. Num a => a -> a -> a
- Int
1)
      maxi :: Integer
maxi = (Integer
1 :: Integer) forall a. Bits a => a -> Int -> a
`shiftL` Int
r
      noi :: Integer
noi = (Integer
1 :: Integer) forall a. Bits a => a -> Int -> a
`shiftL` Int
l
  sizedBVExt :: forall (l :: Natural) (r :: Natural) (proxy :: Natural -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
sizedBVExt = forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(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 :: Natural) (ix :: Natural) (w :: Natural)
       (p :: Natural -> *) (q :: Natural -> *).
(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) = forall (n :: Natural). Integer -> WordN n
WordN ((Integer
v forall a. Bits a => a -> Int -> a
`shiftR` Int
ix) forall a. Bits a => a -> a -> a
.&. Integer
mask)
    where
      ix :: Int
ix = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal p ix
pix
      w :: Int
w = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal q w
pw
      mask :: Integer
mask = (Integer
1 forall a. Bits a => a -> Int -> a
`shiftL` Int
w) 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 :: Natural) (r :: Natural).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
IntN l -> IntN r -> IntN (l + r)
sizedBVConcat (IntN Integer
a) (IntN Integer
b) = forall (n :: Natural). Integer -> IntN n
IntN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). WordN n -> Integer
unWordN forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (l :: Natural) (r :: Natural).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat (forall (n :: Natural). Integer -> WordN n
WordN Integer
a :: WordN l) (forall (n :: Natural). Integer -> WordN n
WordN Integer
b :: WordN r)
  sizedBVZext :: forall (l :: Natural) (r :: Natural) (proxy :: Natural -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> IntN l -> IntN r
sizedBVZext proxy r
_ (IntN Integer
v) = forall (n :: Natural). 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 :: Natural) (r :: Natural) (proxy :: Natural -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> IntN l -> IntN r
sizedBVSext proxy r
pr (IntN Integer
v) = forall (n :: Natural). Integer -> IntN n
IntN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). WordN n -> Integer
unWordN forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVSext proxy r
pr (forall (n :: Natural). Integer -> WordN n
WordN Integer
v :: WordN l)
  sizedBVExt :: forall (l :: Natural) (r :: Natural) (proxy :: Natural -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> IntN l -> IntN r
sizedBVExt = forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(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 :: Natural) (ix :: Natural) (w :: Natural)
       (p :: Natural -> *) (q :: Natural -> *).
(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) = forall (n :: Natural). Integer -> IntN n
IntN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). WordN n -> Integer
unWordN forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (n :: Natural) (ix :: Natural)
       (w :: Natural) (p :: Natural -> *) (q :: Natural -> *).
(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 (forall (n :: Natural). Integer -> WordN n
WordN Integer
v :: WordN n)

instance BV SomeWordN where
  bvConcat :: SomeWordN -> SomeWordN -> SomeWordN
bvConcat (SomeWordN (WordN n
a :: WordN l)) (SomeWordN (WordN n
b :: WordN r)) =
    case (forall (m :: Natural) (n :: Natural) (p :: Natural -> *)
       (q :: Natural -> *).
(1 <= m, 1 <= n) =>
p m -> q n -> LeqProof 1 (m + n)
leqAddPos (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r), forall (m :: Natural) (n :: Natural).
KnownProof m -> KnownProof n -> KnownProof (m + n)
knownAdd @l @r forall (n :: Natural). KnownNat n => KnownProof n
KnownProof forall (n :: Natural). KnownNat n => KnownProof n
KnownProof) of
      (LeqProof 1 (n + n)
LeqProof, KnownProof (n + n)
KnownProof) ->
        forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (l :: Natural) (r :: Natural).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat WordN n
a WordN n
b
  {-# INLINE bvConcat #-}
  bvZext :: Int -> SomeWordN -> SomeWordN
bvZext Int
l (SomeWordN (WordN n
a :: WordN n))
    | Int
l forall a. Ord a => a -> a -> Bool
< Int
n = forall a. HasCallStack => String -> a
error String
"bvZext: trying to zero extend a value to a smaller size"
    | Bool
otherwise = forall (l :: Natural). Proxy l -> SomeWordN
res (forall {k} (t :: k). Proxy t
Proxy @n)
    where
      n :: Int
n = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy @n)
      res :: forall (l :: Nat). Proxy l -> SomeWordN
      res :: forall (l :: Natural). Proxy l -> SomeWordN
res Proxy l
p =
        case (forall (n :: Natural). Natural -> KnownProof n
unsafeKnownProof @l (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l), forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @1 @l, forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @n @l) of
          (KnownProof l
KnownProof, LeqProof 1 l
LeqProof, LeqProof n l
LeqProof) -> forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVZext Proxy l
p WordN n
a
  bvSext :: Int -> SomeWordN -> SomeWordN
bvSext Int
l (SomeWordN (WordN n
a :: WordN n))
    | Int
l forall a. Ord a => a -> a -> Bool
< Int
n = forall a. HasCallStack => String -> a
error String
"bvSext: trying to zero extend a value to a smaller size"
    | Bool
otherwise = forall (l :: Natural). Proxy l -> SomeWordN
res (forall {k} (t :: k). Proxy t
Proxy @n)
    where
      n :: Int
n = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy @n)
      res :: forall (l :: Nat). Proxy l -> SomeWordN
      res :: forall (l :: Natural). Proxy l -> SomeWordN
res Proxy l
p =
        case (forall (n :: Natural). Natural -> KnownProof n
unsafeKnownProof @l (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l), forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @1 @l, forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @n @l) of
          (KnownProof l
KnownProof, LeqProof 1 l
LeqProof, LeqProof n l
LeqProof) -> forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVSext Proxy l
p WordN n
a
  bvExt :: Int -> SomeWordN -> SomeWordN
bvExt = forall bv. BV bv => Int -> bv -> bv
bvZext
  bvSelect :: Int -> Int -> SomeWordN -> SomeWordN
bvSelect Int
ix Int
w (SomeWordN (WordN n
a :: WordN n))
    | Int
ix forall a. Num a => a -> a -> a
+ Int
w forall a. Ord a => a -> a -> Bool
> Int
n = forall a. HasCallStack => String -> a
error String
"bvSelect: trying to select a bitvector outside the bounds of the input"
    | Int
w forall a. Eq a => a -> a -> Bool
== Int
0 = forall a. HasCallStack => String -> a
error String
"bvSelect: trying to select a bitvector of size 0"
    | Bool
otherwise = forall (w :: Natural) (ix :: Natural).
Proxy w -> Proxy ix -> SomeWordN
res (forall {k} (t :: k). Proxy t
Proxy @n) (forall {k} (t :: k). Proxy t
Proxy @n)
    where
      n :: Int
n = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy @n)
      res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> SomeWordN
      res :: forall (w :: Natural) (ix :: Natural).
Proxy w -> Proxy ix -> SomeWordN
res Proxy w
_ Proxy ix
_ =
        case ( forall (n :: Natural). Natural -> KnownProof n
unsafeKnownProof @ix (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
ix),
               forall (n :: Natural). Natural -> KnownProof n
unsafeKnownProof @w (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
w),
               forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @1 @w,
               forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @(ix + w) @n
             ) of
          (KnownProof ix
KnownProof, KnownProof w
KnownProof, LeqProof 1 w
LeqProof, LeqProof (ix + w) n
LeqProof) ->
            forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (n :: Natural) (ix :: Natural)
       (w :: Natural) (p :: Natural -> *) (q :: Natural -> *).
(SizedBV bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
p ix -> q w -> bv n -> bv w
sizedBVSelect (forall {k} (t :: k). Proxy t
Proxy @ix) (forall {k} (t :: k). Proxy t
Proxy @w) WordN n
a

instance BV SomeIntN where
  bvConcat :: SomeIntN -> SomeIntN -> SomeIntN
bvConcat SomeIntN
l SomeIntN
r = forall ubv sbv. BVSignConversion ubv sbv => ubv -> sbv
toSigned forall a b. (a -> b) -> a -> b
$ forall bv. BV bv => bv -> bv -> bv
bvConcat (forall ubv sbv. BVSignConversion ubv sbv => sbv -> ubv
toUnsigned SomeIntN
l) (forall ubv sbv. BVSignConversion ubv sbv => sbv -> ubv
toUnsigned SomeIntN
r)
  {-# INLINE bvConcat #-}
  bvZext :: Int -> SomeIntN -> SomeIntN
bvZext Int
l = forall ubv sbv. BVSignConversion ubv sbv => ubv -> sbv
toSigned forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall bv. BV bv => Int -> bv -> bv
bvZext Int
l forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ubv sbv. BVSignConversion ubv sbv => sbv -> ubv
toUnsigned
  {-# INLINE bvZext #-}
  bvSext :: Int -> SomeIntN -> SomeIntN
bvSext Int
l = forall ubv sbv. BVSignConversion ubv sbv => ubv -> sbv
toSigned forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall bv. BV bv => Int -> bv -> bv
bvSext Int
l forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ubv sbv. BVSignConversion ubv sbv => sbv -> ubv
toUnsigned
  {-# INLINE bvSext #-}
  bvExt :: Int -> SomeIntN -> SomeIntN
bvExt Int
l = forall ubv sbv. BVSignConversion ubv sbv => ubv -> sbv
toSigned forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall bv. BV bv => Int -> bv -> bv
bvExt Int
l forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ubv sbv. BVSignConversion ubv sbv => sbv -> ubv
toUnsigned
  {-# INLINE bvExt #-}
  bvSelect :: Int -> Int -> SomeIntN -> SomeIntN
bvSelect Int
ix Int
w = forall ubv sbv. BVSignConversion ubv sbv => ubv -> sbv
toSigned forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall bv. BV bv => Int -> Int -> bv -> bv
bvSelect Int
ix Int
w forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ubv sbv. BVSignConversion ubv sbv => sbv -> ubv
toUnsigned
  {-# INLINE bvSelect #-}

instance (KnownNat n, 1 <= n) => BVSignConversion (WordN n) (IntN n) where
  toSigned :: WordN n -> IntN n
toSigned (WordN Integer
i) = forall (n :: Natural). Integer -> IntN n
IntN Integer
i
  toUnsigned :: IntN n -> WordN n
toUnsigned (IntN Integer
i) = forall (n :: Natural). Integer -> WordN n
WordN Integer
i

instance BVSignConversion SomeWordN SomeIntN where
  toSigned :: SomeWordN -> SomeIntN
toSigned (SomeWordN WordN n
i) = forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN forall a b. (a -> b) -> a -> b
$ forall ubv sbv. BVSignConversion ubv sbv => ubv -> sbv
toSigned WordN n
i
  toUnsigned :: SomeIntN -> SomeWordN
toUnsigned (SomeIntN IntN n
i) = forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN forall a b. (a -> b) -> a -> b
$ forall ubv sbv. BVSignConversion ubv sbv => sbv -> ubv
toUnsigned IntN n
i