{-# 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
-- 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.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

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

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

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

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

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

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

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

  -- 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 (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)