{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -funbox-strict-fields #-}
module Grisette.IR.SymPrim.Data.BV (IntN (..), WordN (..)) where
import Control.DeepSeq
import Control.Exception
import Data.Bits
import Data.Hashable
import Data.Proxy
import GHC.Enum
import GHC.Generics
import GHC.Real
import GHC.TypeNats
import Grisette.Core.Data.Class.BitVector
import Language.Haskell.TH.Syntax
import Numeric
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)
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
""
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)
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) => 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
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)
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)
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 WordN n
_ = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ 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))
bitSize :: WordN n -> Int
bitSize 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))
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
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)
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 (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 (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 (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 (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 (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)
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
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))
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)
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 IntN n
_ = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ 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))
bitSize :: IntN n -> Int
bitSize 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))
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)
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)
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 (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 (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 (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 (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 =
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
`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 =
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
`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 (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 (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, KnownNat m, 1 <= m, KnownNat w, 1 <= w, w ~ (n + m)) =>
BVConcat (WordN n) (WordN m) (WordN w)
where
bvconcat :: WordN n -> WordN m -> WordN w
bvconcat (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 m))) forall a. Bits a => a -> a -> a
.|. Integer
b)
instance
(KnownNat n, 1 <= n, KnownNat m, 1 <= m, KnownNat w, 1 <= w, w ~ (n + m)) =>
BVConcat (IntN n) (IntN m) (IntN w)
where
bvconcat :: IntN n -> IntN m -> IntN w
bvconcat (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 bv1 bv2 bv3. BVConcat bv1 bv2 bv3 => bv1 -> bv2 -> bv3
bvconcat (forall (n :: Natural). Integer -> WordN n
WordN Integer
a :: WordN n) (forall (n :: Natural). Integer -> WordN n
WordN Integer
b :: WordN m)
instance (KnownNat n, 1 <= n, KnownNat r, n <= r) => BVExtend (WordN n) r (WordN r) where
bvzeroExtend :: forall (proxy :: Natural -> *). proxy r -> WordN n -> WordN r
bvzeroExtend proxy r
_ (WordN Integer
v) = forall (n :: Natural). Integer -> WordN n
WordN Integer
v
bvsignExtend :: forall (proxy :: Natural -> *). proxy r -> WordN n -> WordN r
bvsignExtend 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
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 :: Bool
s = forall a. Bits a => a -> Int -> Bool
testBit Integer
v (Int
n 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
n
bvextend :: forall (proxy :: Natural -> *). proxy r -> WordN n -> WordN r
bvextend = forall bv1 (n :: Natural) bv2 (proxy :: Natural -> *).
BVExtend bv1 n bv2 =>
proxy n -> bv1 -> bv2
bvzeroExtend
instance (KnownNat n, 1 <= n, KnownNat r, n <= r) => BVExtend (IntN n) r (IntN r) where
bvzeroExtend :: forall (proxy :: Natural -> *). proxy r -> IntN n -> IntN r
bvzeroExtend proxy r
_ (IntN Integer
v) = forall (n :: Natural). Integer -> IntN n
IntN Integer
v
bvsignExtend :: forall (proxy :: Natural -> *). proxy r -> IntN n -> IntN r
bvsignExtend 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 bv1 (n :: Natural) bv2 (proxy :: Natural -> *).
BVExtend bv1 n bv2 =>
proxy n -> bv1 -> bv2
bvsignExtend proxy r
pr (forall (n :: Natural). Integer -> WordN n
WordN Integer
v :: WordN n)
bvextend :: forall (proxy :: Natural -> *). proxy r -> IntN n -> IntN r
bvextend = forall bv1 (n :: Natural) bv2 (proxy :: Natural -> *).
BVExtend bv1 n bv2 =>
proxy n -> bv1 -> bv2
bvsignExtend
instance (KnownNat n, 1 <= n, KnownNat ix, KnownNat w, 1 <= w, ix + w <= n) => BVSelect (WordN n) ix w (WordN w) where
bvselect :: forall (proxy :: Natural -> *).
proxy ix -> proxy w -> WordN n -> WordN w
bvselect proxy ix
pix proxy 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 proxy 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 proxy 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 (KnownNat n, 1 <= n, KnownNat ix, KnownNat w, 1 <= w, ix + w <= n) => BVSelect (IntN n) ix w (IntN w) where
bvselect :: forall (proxy :: Natural -> *).
proxy ix -> proxy w -> IntN n -> IntN w
bvselect proxy ix
pix proxy 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 bv1 (ix :: Natural) (w :: Natural) bv2
(proxy :: Natural -> *).
BVSelect bv1 ix w bv2 =>
proxy ix -> proxy w -> bv1 -> bv2
bvselect proxy ix
pix proxy w
pw (forall (n :: Natural). Integer -> WordN n
WordN Integer
v :: WordN n)