{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -funbox-strict-fields #-}
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),
SizedBV
( sizedBVConcat,
sizedBVExt,
sizedBVSelect,
sizedBVSext,
sizedBVZext
),
)
import Grisette.Core.Data.Class.SignConversion
( SignConversion (toSigned, toUnsigned),
)
import Grisette.Core.Data.Class.SymRotate
( DefaultFiniteBitsSymRotate (DefaultFiniteBitsSymRotate),
SymRotate,
)
import Grisette.Core.Data.Class.SymShift
( DefaultFiniteBitsSymShift (DefaultFiniteBitsSymShift),
SymShift,
)
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
(Int -> BitwidthMismatch -> ShowS)
-> (BitwidthMismatch -> String)
-> ([BitwidthMismatch] -> ShowS)
-> Show BitwidthMismatch
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BitwidthMismatch -> ShowS
showsPrec :: Int -> BitwidthMismatch -> ShowS
$cshow :: BitwidthMismatch -> String
show :: BitwidthMismatch -> String
$cshowList :: [BitwidthMismatch] -> ShowS
showList :: [BitwidthMismatch] -> ShowS
Show, BitwidthMismatch -> BitwidthMismatch -> Bool
(BitwidthMismatch -> BitwidthMismatch -> Bool)
-> (BitwidthMismatch -> BitwidthMismatch -> Bool)
-> Eq BitwidthMismatch
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BitwidthMismatch -> BitwidthMismatch -> Bool
== :: BitwidthMismatch -> BitwidthMismatch -> Bool
$c/= :: BitwidthMismatch -> BitwidthMismatch -> Bool
/= :: BitwidthMismatch -> BitwidthMismatch -> Bool
Eq, Eq BitwidthMismatch
Eq BitwidthMismatch =>
(BitwidthMismatch -> BitwidthMismatch -> Ordering)
-> (BitwidthMismatch -> BitwidthMismatch -> Bool)
-> (BitwidthMismatch -> BitwidthMismatch -> Bool)
-> (BitwidthMismatch -> BitwidthMismatch -> Bool)
-> (BitwidthMismatch -> BitwidthMismatch -> Bool)
-> (BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch)
-> (BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch)
-> Ord BitwidthMismatch
BitwidthMismatch -> BitwidthMismatch -> Bool
BitwidthMismatch -> BitwidthMismatch -> Ordering
BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: BitwidthMismatch -> BitwidthMismatch -> Ordering
compare :: BitwidthMismatch -> BitwidthMismatch -> Ordering
$c< :: BitwidthMismatch -> BitwidthMismatch -> Bool
< :: BitwidthMismatch -> BitwidthMismatch -> Bool
$c<= :: BitwidthMismatch -> BitwidthMismatch -> Bool
<= :: BitwidthMismatch -> BitwidthMismatch -> Bool
$c> :: BitwidthMismatch -> BitwidthMismatch -> Bool
> :: BitwidthMismatch -> BitwidthMismatch -> Bool
$c>= :: BitwidthMismatch -> BitwidthMismatch -> Bool
>= :: BitwidthMismatch -> BitwidthMismatch -> Bool
$cmax :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
max :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
$cmin :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
min :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
Ord, (forall x. BitwidthMismatch -> Rep BitwidthMismatch x)
-> (forall x. Rep BitwidthMismatch x -> BitwidthMismatch)
-> Generic BitwidthMismatch
forall x. Rep BitwidthMismatch x -> BitwidthMismatch
forall x. BitwidthMismatch -> Rep BitwidthMismatch x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. BitwidthMismatch -> Rep BitwidthMismatch x
from :: forall x. BitwidthMismatch -> Rep BitwidthMismatch x
$cto :: forall x. Rep BitwidthMismatch x -> BitwidthMismatch
to :: forall x. Rep BitwidthMismatch x -> BitwidthMismatch
Generic)
instance Exception BitwidthMismatch where
displayException :: BitwidthMismatch -> String
displayException BitwidthMismatch
BitwidthMismatch = String
"Bit width does not match"
newtype WordN (n :: Nat) = WordN {forall (n :: Nat). WordN n -> Integer
unWordN :: Integer}
deriving (WordN n -> WordN n -> Bool
(WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool) -> Eq (WordN n)
forall (n :: Nat). WordN n -> WordN n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Nat). WordN n -> WordN n -> Bool
== :: WordN n -> WordN n -> Bool
$c/= :: forall (n :: Nat). WordN n -> WordN n -> Bool
/= :: WordN n -> WordN n -> Bool
Eq, Eq (WordN n)
Eq (WordN n) =>
(WordN n -> WordN n -> Ordering)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> WordN n)
-> (WordN n -> WordN n -> WordN n)
-> Ord (WordN n)
WordN n -> WordN n -> Bool
WordN n -> WordN n -> Ordering
WordN n -> WordN n -> WordN n
forall (n :: Nat). Eq (WordN n)
forall (n :: Nat). WordN n -> WordN n -> Bool
forall (n :: Nat). WordN n -> WordN n -> Ordering
forall (n :: Nat). WordN n -> WordN n -> WordN n
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: forall (n :: Nat). WordN n -> WordN n -> Ordering
compare :: WordN n -> WordN n -> Ordering
$c< :: forall (n :: Nat). WordN n -> WordN n -> Bool
< :: WordN n -> WordN n -> Bool
$c<= :: forall (n :: Nat). WordN n -> WordN n -> Bool
<= :: WordN n -> WordN n -> Bool
$c> :: forall (n :: Nat). WordN n -> WordN n -> Bool
> :: WordN n -> WordN n -> Bool
$c>= :: forall (n :: Nat). WordN n -> WordN n -> Bool
>= :: WordN n -> WordN n -> Bool
$cmax :: forall (n :: Nat). WordN n -> WordN n -> WordN n
max :: WordN n -> WordN n -> WordN n
$cmin :: forall (n :: Nat). WordN n -> WordN n -> WordN n
min :: WordN n -> WordN n -> WordN n
Ord, (forall x. WordN n -> Rep (WordN n) x)
-> (forall x. Rep (WordN n) x -> WordN n) -> Generic (WordN n)
forall (n :: Nat) x. Rep (WordN n) x -> WordN n
forall (n :: Nat) x. WordN n -> Rep (WordN n) x
forall x. Rep (WordN n) x -> WordN n
forall x. WordN n -> Rep (WordN n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (n :: Nat) x. WordN n -> Rep (WordN n) x
from :: forall x. WordN n -> Rep (WordN n) x
$cto :: forall (n :: Nat) x. Rep (WordN n) x -> WordN n
to :: forall x. Rep (WordN n) x -> WordN n
Generic, (forall (m :: * -> *). Quote m => WordN n -> m Exp)
-> (forall (m :: * -> *). Quote m => WordN n -> Code m (WordN n))
-> Lift (WordN n)
forall (n :: Nat) (m :: * -> *). Quote m => WordN n -> m Exp
forall (n :: Nat) (m :: * -> *).
Quote m =>
WordN n -> Code m (WordN n)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => WordN n -> m Exp
forall (m :: * -> *). Quote m => WordN n -> Code m (WordN n)
$clift :: forall (n :: Nat) (m :: * -> *). Quote m => WordN n -> m Exp
lift :: forall (m :: * -> *). Quote m => WordN n -> m Exp
$cliftTyped :: forall (n :: Nat) (m :: * -> *).
Quote m =>
WordN n -> Code m (WordN n)
liftTyped :: forall (m :: * -> *). Quote m => WordN n -> Code m (WordN n)
Lift, Eq (WordN n)
Eq (WordN n) =>
(Int -> WordN n -> Int) -> (WordN n -> Int) -> Hashable (WordN n)
Int -> WordN n -> Int
WordN n -> Int
forall (n :: Nat). Eq (WordN n)
forall (n :: Nat). Int -> WordN n -> Int
forall (n :: Nat). WordN n -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: forall (n :: Nat). Int -> WordN n -> Int
hashWithSalt :: Int -> WordN n -> Int
$chash :: forall (n :: Nat). WordN n -> Int
hash :: WordN n -> Int
Hashable, WordN n -> ()
(WordN n -> ()) -> NFData (WordN n)
forall (n :: Nat). WordN n -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall (n :: Nat). WordN n -> ()
rnf :: WordN n -> ()
NFData)
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 :: Nat). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> r
op (SomeWordN (WordN n
w :: WordN w)) = WordN n -> r
forall (n :: Nat). (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 :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n
op (SomeWordN (WordN n
w :: WordN w)) = WordN n -> SomeWordN
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN (WordN n -> SomeWordN) -> WordN n -> SomeWordN
forall a b. (a -> b) -> a -> b
$ WordN n -> WordN n
forall (n :: Nat). (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 :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n -> r
op (SomeWordN (WordN n
l :: WordN l)) (SomeWordN (WordN n
r :: WordN r)) =
case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
Just n :~: n
Refl -> WordN n -> WordN n -> r
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n -> r
op WordN n
l WordN n
WordN n
r
Maybe (n :~: n)
Nothing -> BitwidthMismatch -> r
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 :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
op (SomeWordN (WordN n
l :: WordN l)) (SomeWordN (WordN n
r :: WordN r)) =
case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
Just n :~: n
Refl -> WordN n -> SomeWordN
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN (WordN n -> SomeWordN) -> WordN n -> SomeWordN
forall a b. (a -> b) -> a -> b
$ WordN n -> WordN n -> WordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
op WordN n
l WordN n
WordN n
r
Maybe (n :~: n)
Nothing -> BitwidthMismatch -> SomeWordN
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 :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> (WordN n, WordN n))
-> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
binSomeWordNR2 forall (n :: Nat).
(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 Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
Just n :~: n
Refl ->
case WordN n -> WordN n -> (WordN n, WordN n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> (WordN n, WordN n)
op WordN n
l WordN n
WordN n
r of
(WordN n
a, WordN n
b) -> (WordN n -> SomeWordN
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN WordN n
a, WordN n -> SomeWordN
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN WordN n
b)
Maybe (n :~: n)
Nothing -> BitwidthMismatch -> (SomeWordN, SomeWordN)
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 Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
Just n :~: n
Refl -> WordN n
l WordN n -> WordN n -> Bool
forall a. Eq a => a -> a -> Bool
== WordN n
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 Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
Just n :~: n
Refl -> WordN n
l WordN n -> WordN n -> Bool
forall a. Eq a => a -> a -> Bool
/= WordN n
WordN n
r
Maybe (n :~: n)
Nothing -> Bool
True
{-# INLINE (/=) #-}
instance Ord SomeWordN where
<= :: SomeWordN -> SomeWordN -> Bool
(<=) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> Bool)
-> SomeWordN -> SomeWordN -> Bool
forall r.
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN WordN n -> WordN n -> Bool
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> Bool
forall a. Ord a => a -> a -> Bool
(<=)
{-# INLINE (<=) #-}
< :: SomeWordN -> SomeWordN -> Bool
(<) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> Bool)
-> SomeWordN -> SomeWordN -> Bool
forall r.
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN WordN n -> WordN n -> Bool
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> Bool
forall a. Ord a => a -> a -> Bool
(<)
{-# INLINE (<) #-}
>= :: SomeWordN -> SomeWordN -> Bool
(>=) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> Bool)
-> SomeWordN -> SomeWordN -> Bool
forall r.
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN WordN n -> WordN n -> Bool
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> Bool
forall a. Ord a => a -> a -> Bool
(>=)
{-# INLINE (>=) #-}
> :: SomeWordN -> SomeWordN -> Bool
(>) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> Bool)
-> SomeWordN -> SomeWordN -> Bool
forall r.
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN WordN n -> WordN n -> Bool
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> Bool
forall a. Ord a => a -> a -> Bool
(>)
{-# INLINE (>) #-}
max :: SomeWordN -> SomeWordN -> SomeWordN
max = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 WordN n -> WordN n -> WordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
forall a. Ord a => a -> a -> a
max
{-# INLINE max #-}
min :: SomeWordN -> SomeWordN -> SomeWordN
min = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 WordN n -> WordN n -> WordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
forall a. Ord a => a -> a -> a
min
{-# INLINE min #-}
compare :: SomeWordN -> SomeWordN -> Ordering
compare = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> Ordering)
-> SomeWordN -> SomeWordN -> Ordering
forall r.
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN WordN n -> WordN n -> Ordering
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> Ordering
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) = [||WordN n -> SomeWordN
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN WordN n
w||]
instance Hashable SomeWordN where
Int
s hashWithSalt :: Int -> SomeWordN -> Int
`hashWithSalt` (SomeWordN (WordN n
w :: WordN n)) = Int
s Int -> Nat -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) Int -> WordN n -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` WordN n
w
instance NFData SomeWordN where
rnf :: SomeWordN -> ()
rnf (SomeWordN WordN n
w) = WordN n -> ()
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 (Nat
bitwidth Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`mod` Nat
4) Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
0 then String
hexRepPre String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
hexRep else String
binRepPre String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
binRep
where
bitwidth :: Nat
bitwidth = Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
hexRepPre :: String
hexRepPre = String
"0x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat
bitwidth Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`div` Nat
4) Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
hexRep) Char
'0'
hexRep :: String
hexRep = Integer -> ShowS
forall a. Integral a => a -> ShowS
showHex Integer
w String
""
binRepPre :: String
binRepPre = String
"0b" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
bitwidth Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
binRep) Char
'0'
binRep :: String
binRep = Integer -> (Int -> Char) -> Integer -> ShowS
forall a. Integral a => a -> (Int -> Char) -> a -> ShowS
showIntAtBase Integer
2 (\Int
x -> if Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Char
'0' else Char
'1') Integer
w String
""
convertInt :: (Num a) => L.Lexeme -> ReadPrec a
convertInt :: forall a. Num a => Lexeme -> ReadPrec a
convertInt (L.Number Number
n)
| Just Integer
i <- Number -> Maybe Integer
L.numberToInteger Number
n = a -> ReadPrec a
forall a. a -> ReadPrec a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> a
forall a. Num a => Integer -> a
fromInteger Integer
i)
convertInt Lexeme
_ = ReadPrec a
forall a. ReadPrec a
pfail
readBinary :: (Num a) => ReadPrec a
readBinary :: forall a. Num a => ReadPrec a
readBinary = ReadPrec a -> ReadPrec a
forall a. ReadPrec a -> ReadPrec a
parens (ReadPrec a -> ReadPrec a) -> ReadPrec a -> ReadPrec a
forall a b. (a -> b) -> a -> b
$ do
String
r0 <- ReadPrec String
look
case String
r0 of
(Char
'-' : String
_) -> do
Char
_ <- ReadPrec Char
get
a -> a
forall a. Num a => a -> a
negate (a -> a) -> ReadPrec a -> ReadPrec a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadPrec a -> ReadPrec a
forall a. ReadPrec a -> ReadPrec a
parens ReadPrec a
parse0b
String
_ -> ReadPrec a
parse0b
where
isDigit :: Char -> Bool
isDigit Char
c = Maybe Integer -> Bool
forall a. Maybe a -> Bool
isJust (Char -> Maybe Integer
forall {a}. Num a => Char -> Maybe a
valDig Char
c)
valDigit :: Char -> a
valDigit Char
c = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
0 (Char -> Maybe a
forall {a}. Num a => Char -> Maybe a
valDig Char
c)
valDig :: Char -> Maybe a
valDig Char
'0' = a -> Maybe a
forall a. a -> Maybe a
Just a
0
valDig Char
'1' = a -> Maybe a
forall a. a -> Maybe a
Just a
1
valDig Char
_ = Maybe a
forall a. Maybe a
Nothing
parse0b :: ReadPrec a
parse0b = do
String
_ <- ReadP String -> ReadPrec String
forall a. ReadP a -> ReadPrec a
Text.Read.lift (ReadP String -> ReadPrec String)
-> ReadP String -> ReadPrec String
forall a b. (a -> b) -> a -> b
$ String -> ReadP String
string String
"0b"
Integer -> a
forall a. Num a => Integer -> a
fromInteger (Integer -> a) -> ReadPrec Integer -> ReadPrec a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadP Integer -> ReadPrec Integer
forall a. ReadP a -> ReadPrec a
Text.Read.lift (Integer -> (Char -> Bool) -> (Char -> Int) -> ReadP Integer
forall a. Num a => a -> (Char -> Bool) -> (Char -> Int) -> ReadP a
L.readIntP Integer
2 Char -> Bool
isDigit Char -> Int
forall {a}. Num a => Char -> a
valDigit)
instance (KnownNat n, 1 <= n) => Read (WordN n) where
readPrec :: ReadPrec (WordN n)
readPrec = (Lexeme -> ReadPrec (WordN n)) -> ReadPrec (WordN n)
forall a. Num a => (Lexeme -> ReadPrec a) -> ReadPrec a
readNumber Lexeme -> ReadPrec (WordN n)
forall a. Num a => Lexeme -> ReadPrec a
convertInt ReadPrec (WordN n) -> ReadPrec (WordN n) -> ReadPrec (WordN n)
forall a. ReadPrec a -> ReadPrec a -> ReadPrec a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ReadPrec (WordN n)
forall a. Num a => ReadPrec a
readBinary
readListPrec :: ReadPrec [WordN n]
readListPrec = ReadPrec [WordN n]
forall a. Read a => ReadPrec [a]
readListPrecDefault
readList :: ReadS [WordN n]
readList = ReadS [WordN n]
forall a. Read a => ReadS [a]
readListDefault
instance Show SomeWordN where
show :: SomeWordN -> String
show (SomeWordN WordN n
w) = WordN n -> String
forall a. Show a => a -> String
show WordN n
w
newtype IntN (n :: Nat) = IntN {forall (n :: Nat). IntN n -> Integer
unIntN :: Integer}
deriving (IntN n -> IntN n -> Bool
(IntN n -> IntN n -> Bool)
-> (IntN n -> IntN n -> Bool) -> Eq (IntN n)
forall (n :: Nat). IntN n -> IntN n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Nat). IntN n -> IntN n -> Bool
== :: IntN n -> IntN n -> Bool
$c/= :: forall (n :: Nat). IntN n -> IntN n -> Bool
/= :: IntN n -> IntN n -> Bool
Eq, (forall x. IntN n -> Rep (IntN n) x)
-> (forall x. Rep (IntN n) x -> IntN n) -> Generic (IntN n)
forall (n :: Nat) x. Rep (IntN n) x -> IntN n
forall (n :: Nat) x. IntN n -> Rep (IntN n) x
forall x. Rep (IntN n) x -> IntN n
forall x. IntN n -> Rep (IntN n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (n :: Nat) x. IntN n -> Rep (IntN n) x
from :: forall x. IntN n -> Rep (IntN n) x
$cto :: forall (n :: Nat) x. Rep (IntN n) x -> IntN n
to :: forall x. Rep (IntN n) x -> IntN n
Generic, (forall (m :: * -> *). Quote m => IntN n -> m Exp)
-> (forall (m :: * -> *). Quote m => IntN n -> Code m (IntN n))
-> Lift (IntN n)
forall (n :: Nat) (m :: * -> *). Quote m => IntN n -> m Exp
forall (n :: Nat) (m :: * -> *).
Quote m =>
IntN n -> Code m (IntN n)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => IntN n -> m Exp
forall (m :: * -> *). Quote m => IntN n -> Code m (IntN n)
$clift :: forall (n :: Nat) (m :: * -> *). Quote m => IntN n -> m Exp
lift :: forall (m :: * -> *). Quote m => IntN n -> m Exp
$cliftTyped :: forall (n :: Nat) (m :: * -> *).
Quote m =>
IntN n -> Code m (IntN n)
liftTyped :: forall (m :: * -> *). Quote m => IntN n -> Code m (IntN n)
Lift, Eq (IntN n)
Eq (IntN n) =>
(Int -> IntN n -> Int) -> (IntN n -> Int) -> Hashable (IntN n)
Int -> IntN n -> Int
IntN n -> Int
forall (n :: Nat). Eq (IntN n)
forall (n :: Nat). Int -> IntN n -> Int
forall (n :: Nat). IntN n -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: forall (n :: Nat). Int -> IntN n -> Int
hashWithSalt :: Int -> IntN n -> Int
$chash :: forall (n :: Nat). IntN n -> Int
hash :: IntN n -> Int
Hashable, IntN n -> ()
(IntN n -> ()) -> NFData (IntN n)
forall (n :: Nat). IntN n -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall (n :: Nat). IntN n -> ()
rnf :: IntN n -> ()
NFData)
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 :: Nat). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> r
op (SomeIntN (IntN n
w :: IntN w)) = IntN n -> r
forall (n :: Nat). (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 :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n
op (SomeIntN (IntN n
w :: IntN w)) = IntN n -> SomeIntN
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN (IntN n -> SomeIntN) -> IntN n -> SomeIntN
forall a b. (a -> b) -> a -> b
$ IntN n -> IntN n
forall (n :: Nat). (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 :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> r
op (SomeIntN (IntN n
l :: IntN l)) (SomeIntN (IntN n
r :: IntN r)) =
case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
Just n :~: n
Refl -> IntN n -> IntN n -> r
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> r
op IntN n
l IntN n
IntN n
r
Maybe (n :~: n)
Nothing -> BitwidthMismatch -> r
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 :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
op (SomeIntN (IntN n
l :: IntN l)) (SomeIntN (IntN n
r :: IntN r)) =
case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
Just n :~: n
Refl -> IntN n -> SomeIntN
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN (IntN n -> SomeIntN) -> IntN n -> SomeIntN
forall a b. (a -> b) -> a -> b
$ IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
op IntN n
l IntN n
IntN n
r
Maybe (n :~: n)
Nothing -> BitwidthMismatch -> SomeIntN
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 :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> (IntN n, IntN n))
-> SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
binSomeIntNR2 forall (n :: Nat).
(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 Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
Just n :~: n
Refl ->
case IntN n -> IntN n -> (IntN n, IntN n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> (IntN n, IntN n)
op IntN n
l IntN n
IntN n
r of
(IntN n
a, IntN n
b) -> (IntN n -> SomeIntN
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN IntN n
a, IntN n -> SomeIntN
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN IntN n
b)
Maybe (n :~: n)
Nothing -> BitwidthMismatch -> (SomeIntN, SomeIntN)
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 Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
Just n :~: n
Refl -> IntN n
l IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
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 Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
Just n :~: n
Refl -> IntN n
l IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
/= IntN n
IntN n
r
Maybe (n :~: n)
Nothing -> Bool
True
{-# INLINE (/=) #-}
instance Ord SomeIntN where
<= :: SomeIntN -> SomeIntN -> Bool
(<=) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> Bool)
-> SomeIntN -> SomeIntN -> Bool
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN IntN n -> IntN n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> Bool
forall a. Ord a => a -> a -> Bool
(<=)
{-# INLINE (<=) #-}
< :: SomeIntN -> SomeIntN -> Bool
(<) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> Bool)
-> SomeIntN -> SomeIntN -> Bool
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN IntN n -> IntN n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> Bool
forall a. Ord a => a -> a -> Bool
(<)
{-# INLINE (<) #-}
>= :: SomeIntN -> SomeIntN -> Bool
(>=) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> Bool)
-> SomeIntN -> SomeIntN -> Bool
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN IntN n -> IntN n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> Bool
forall a. Ord a => a -> a -> Bool
(>=)
{-# INLINE (>=) #-}
> :: SomeIntN -> SomeIntN -> Bool
(>) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> Bool)
-> SomeIntN -> SomeIntN -> Bool
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN IntN n -> IntN n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> Bool
forall a. Ord a => a -> a -> Bool
(>)
{-# INLINE (>) #-}
max :: SomeIntN -> SomeIntN -> SomeIntN
max = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Ord a => a -> a -> a
max
{-# INLINE max #-}
min :: SomeIntN -> SomeIntN -> SomeIntN
min = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Ord a => a -> a -> a
min
{-# INLINE min #-}
compare :: SomeIntN -> SomeIntN -> Ordering
compare = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> Ordering)
-> SomeIntN -> SomeIntN -> Ordering
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN IntN n -> IntN n -> Ordering
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> Ordering
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) = [||IntN n -> SomeIntN
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN IntN n
w||]
instance Hashable SomeIntN where
Int
s hashWithSalt :: Int -> SomeIntN -> Int
`hashWithSalt` (SomeIntN (IntN n
w :: IntN n)) = Int
s Int -> Nat -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) Int -> IntN n -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` IntN n
w
instance NFData SomeIntN where
rnf :: SomeIntN -> ()
rnf (SomeIntN IntN n
w) = IntN n -> ()
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 (Nat
bitwidth Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`mod` Nat
4) Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
0 then String
hexRepPre String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
hexRep else String
binRepPre String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
binRep
where
bitwidth :: Nat
bitwidth = Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
hexRepPre :: String
hexRepPre = String
"0x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat
bitwidth Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`div` Nat
4) Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
hexRep) Char
'0'
hexRep :: String
hexRep = Integer -> ShowS
forall a. Integral a => a -> ShowS
showHex Integer
w String
""
binRepPre :: String
binRepPre = String
"0b" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
bitwidth Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
binRep) Char
'0'
binRep :: String
binRep = Integer -> (Int -> Char) -> Integer -> ShowS
forall a. Integral a => a -> (Int -> Char) -> a -> ShowS
showIntAtBase Integer
2 (\Int
x -> if Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Char
'0' else Char
'1') Integer
w String
""
instance (KnownNat n, 1 <= n) => Read (IntN n) where
readPrec :: ReadPrec (IntN n)
readPrec = (Lexeme -> ReadPrec (IntN n)) -> ReadPrec (IntN n)
forall a. Num a => (Lexeme -> ReadPrec a) -> ReadPrec a
readNumber Lexeme -> ReadPrec (IntN n)
forall a. Num a => Lexeme -> ReadPrec a
convertInt ReadPrec (IntN n) -> ReadPrec (IntN n) -> ReadPrec (IntN n)
forall a. ReadPrec a -> ReadPrec a -> ReadPrec a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ReadPrec (IntN n)
forall a. Num a => ReadPrec a
readBinary
readListPrec :: ReadPrec [IntN n]
readListPrec = ReadPrec [IntN n]
forall a. Read a => ReadPrec [a]
readListPrecDefault
readList :: ReadS [IntN n]
readList = ReadS [IntN n]
forall a. Read a => ReadS [a]
readListDefault
instance Show SomeIntN where
show :: SomeIntN -> String
show (SomeIntN IntN n
w) = IntN n -> String
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 = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
b)
WordN Integer
a .|. :: WordN n -> WordN n -> WordN n
.|. WordN Integer
b = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
b)
WordN Integer
a xor :: WordN n -> WordN n -> WordN n
`xor` WordN Integer
b = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer
b)
complement :: WordN n -> WordN n
complement WordN n
a = WordN n
forall a. Bounded a => a
maxBound WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
`xor` WordN n
a
zeroBits :: WordN n
zeroBits = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
0
bit :: Int -> WordN n
bit Int
i
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) = WordN n
forall a. Bits a => a
zeroBits
| Bool
otherwise = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Int -> Integer
forall a. Bits a => Int -> a
bit Int
i)
clearBit :: WordN n -> Int -> WordN n
clearBit (WordN Integer
a) Int
i = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
clearBit Integer
a Int
i)
testBit :: WordN n -> Int -> Bool
testBit (WordN Integer
a) = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a
bitSizeMaybe :: WordN n -> Maybe Int
bitSizeMaybe = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (WordN n -> Int) -> WordN n -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize
bitSize :: WordN n -> Int
bitSize = WordN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize
isSigned :: WordN n -> Bool
isSigned WordN n
_ = Bool
False
shiftL :: WordN n -> Int -> WordN n
shiftL WordN n
w Int
i | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= WordN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize WordN n
w = WordN n
0
shiftL (WordN Integer
a) Int
i = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
i) WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
.&. WordN n
forall a. Bounded a => a
maxBound
shiftR :: WordN n -> Int -> WordN n
shiftR WordN n
w Int
i | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= WordN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize WordN n
w = WordN n
0
shiftR (WordN Integer
a) Int
i = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
i)
rotateL :: WordN n -> Int -> WordN n
rotateL WordN n
a Int
0 = WordN n
a
rotateL (WordN Integer
a) Int
k
| Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
rotateL (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
a) (Int
k Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n)
| Bool
otherwise = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer -> WordN n) -> Integer -> WordN n
forall a b. (a -> b) -> a -> b
$ Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
h
where
n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
s :: Int
s = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k
l :: Integer
l = Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
s
h :: Integer
h = (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- (Integer
l Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
s)) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
k
rotateR :: WordN n -> Int -> WordN n
rotateR WordN n
a Int
0 = WordN n
a
rotateR (WordN Integer
a) Int
k
| Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
rotateR (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
a) (Int
k Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n)
| Bool
otherwise = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer -> WordN n) -> Integer -> WordN n
forall a b. (a -> b) -> a -> b
$ Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
h
where
n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
s :: Int
s = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k
l :: Integer
l = Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
k
h :: Integer
h = (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- (Integer
l Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
k)) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
s
popCount :: WordN n -> Int
popCount (WordN Integer
n) = Integer -> Int
forall a. Bits a => a -> Int
popCount Integer
n
instance Bits SomeWordN where
.&. :: SomeWordN -> SomeWordN -> SomeWordN
(.&.) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 WordN n -> WordN n -> WordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
(.&.)
.|. :: SomeWordN -> SomeWordN -> SomeWordN
(.|.) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 WordN n -> WordN n -> WordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
(.|.)
xor :: SomeWordN -> SomeWordN -> SomeWordN
xor = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 WordN n -> WordN n -> WordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
xor
complement :: SomeWordN -> SomeWordN
complement = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 WordN n -> WordN n
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n
forall a. Bits a => a -> a
complement
shift :: SomeWordN -> Int -> SomeWordN
shift SomeWordN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
`shift` Int
i) SomeWordN
s
rotate :: SomeWordN -> Int -> SomeWordN
rotate SomeWordN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
`rotate` Int
i) SomeWordN
s
zeroBits :: SomeWordN
zeroBits = String -> SomeWordN
forall a. HasCallStack => String -> a
error String
"zeroBits is not defined for SomeWordN as no bitwidth is known"
bit :: Int -> SomeWordN
bit = String -> Int -> SomeWordN
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 :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
`setBit` Int
i) SomeWordN
s
clearBit :: SomeWordN -> Int -> SomeWordN
clearBit SomeWordN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
`clearBit` Int
i) SomeWordN
s
complementBit :: SomeWordN -> Int -> SomeWordN
complementBit SomeWordN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
`complementBit` Int
i) SomeWordN
s
testBit :: SomeWordN -> Int -> Bool
testBit SomeWordN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> Bool)
-> SomeWordN -> Bool
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN (WordN n -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
i) SomeWordN
s
bitSizeMaybe :: SomeWordN -> Maybe Int
bitSizeMaybe = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (SomeWordN -> Int) -> SomeWordN -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeWordN -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize
bitSize :: SomeWordN -> Int
bitSize = SomeWordN -> Int
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 :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
`shiftL` Int
i) SomeWordN
s
unsafeShiftL :: SomeWordN -> Int -> SomeWordN
unsafeShiftL SomeWordN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
`unsafeShiftL` Int
i) SomeWordN
s
shiftR :: SomeWordN -> Int -> SomeWordN
shiftR SomeWordN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
`shiftR` Int
i) SomeWordN
s
unsafeShiftR :: SomeWordN -> Int -> SomeWordN
unsafeShiftR SomeWordN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
`unsafeShiftR` Int
i) SomeWordN
s
rotateL :: SomeWordN -> Int -> SomeWordN
rotateL SomeWordN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
`rotateL` Int
i) SomeWordN
s
rotateR :: SomeWordN -> Int -> SomeWordN
rotateR SomeWordN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
`rotateR` Int
i) SomeWordN
s
popCount :: SomeWordN -> Int
popCount = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> Int)
-> SomeWordN -> Int
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN WordN n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> Int
forall a. Bits a => a -> Int
popCount
instance (KnownNat n, 1 <= n) => FiniteBits (WordN n) where
finiteBitSize :: WordN n -> Int
finiteBitSize WordN n
_ = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
instance FiniteBits SomeWordN where
finiteBitSize :: SomeWordN -> Int
finiteBitSize (SomeWordN (WordN n
n :: WordN n)) = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ WordN n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal WordN n
n
countLeadingZeros :: SomeWordN -> Int
countLeadingZeros = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> Int)
-> SomeWordN -> Int
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN WordN n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> Int
forall b. FiniteBits b => b -> Int
countLeadingZeros
countTrailingZeros :: SomeWordN -> Int
countTrailingZeros = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> Int)
-> SomeWordN -> Int
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN WordN n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> Int
forall b. FiniteBits b => b -> Int
countTrailingZeros
instance (KnownNat n, 1 <= n) => Bounded (WordN n) where
maxBound :: WordN n
maxBound = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN ((Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
minBound :: WordN n
minBound = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
0
instance (KnownNat n, 1 <= n) => Enum (WordN n) where
succ :: WordN n -> WordN n
succ WordN n
x
| WordN n
x WordN n -> WordN n -> Bool
forall a. Eq a => a -> a -> Bool
/= WordN n
forall a. Bounded a => a
maxBound = WordN n
x WordN n -> WordN n -> WordN n
forall a. Num a => a -> a -> a
+ WordN n
1
| Bool
otherwise = String -> WordN n
forall a. String -> a
succError (String -> WordN n) -> String -> WordN n
forall a b. (a -> b) -> a -> b
$ String
"WordN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
pred :: WordN n -> WordN n
pred WordN n
x
| WordN n
x WordN n -> WordN n -> Bool
forall a. Eq a => a -> a -> Bool
/= WordN n
forall a. Bounded a => a
minBound = WordN n
x WordN n -> WordN n -> WordN n
forall a. Num a => a -> a -> a
- WordN n
1
| Bool
otherwise = String -> WordN n
forall a. String -> a
predError (String -> WordN n) -> String -> WordN n
forall a b. (a -> b) -> a -> b
$ String
"WordN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
toEnum :: Int -> WordN n
toEnum Int
i
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= WordN n -> Integer
forall a. Integral a => a -> Integer
toInteger (WordN n
forall a. Bounded a => a
maxBound :: WordN n) = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i)
| Bool
otherwise = String -> Int -> (WordN n, WordN n) -> WordN n
forall a b. Show a => String -> Int -> (a, a) -> b
toEnumError (String
"WordN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))) Int
i (WordN n
forall a. Bounded a => a
minBound :: WordN n, WordN n
forall a. Bounded a => a
maxBound :: WordN n)
fromEnum :: WordN n -> Int
fromEnum (WordN Integer
n) = Integer -> Int
forall a. Enum a => a -> Int
fromEnum Integer
n
enumFrom :: WordN n -> [WordN n]
enumFrom = WordN n -> [WordN n]
forall a. (Enum a, Bounded a) => a -> [a]
boundedEnumFrom
{-# INLINE enumFrom #-}
enumFromThen :: WordN n -> WordN n -> [WordN n]
enumFromThen = WordN n -> WordN n -> [WordN n]
forall a. (Enum a, Bounded a) => a -> a -> [a]
boundedEnumFromThen
{-# INLINE enumFromThen #-}
instance Enum SomeWordN where
toEnum :: Int -> SomeWordN
toEnum = String -> Int -> SomeWordN
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 = String -> SomeWordN -> Int
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 Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1
instance Real SomeWordN where
toRational :: SomeWordN -> Rational
toRational = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> Rational)
-> SomeWordN -> Rational
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN WordN n -> Rational
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> Rational
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) = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
y)
rem :: WordN n -> WordN n -> WordN n
rem (WordN Integer
x) (WordN Integer
y) = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` Integer
y)
quotRem :: WordN n -> WordN n -> (WordN n, WordN n)
quotRem (WordN Integer
x) (WordN Integer
y) = case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
quotRem Integer
x Integer
y of
(Integer
q, Integer
r) -> (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
q, Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
r)
div :: WordN n -> WordN n -> WordN n
div = WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
quot
mod :: WordN n -> WordN n -> WordN n
mod = WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
rem
divMod :: WordN n -> WordN n -> (WordN n, WordN n)
divMod = WordN n -> WordN n -> (WordN n, WordN n)
forall a. Integral a => a -> a -> (a, a)
quotRem
toInteger :: WordN n -> Integer
toInteger (WordN Integer
n) = Integer
n
instance Integral SomeWordN where
quot :: SomeWordN -> SomeWordN -> SomeWordN
quot = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 WordN n -> WordN n -> WordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
quot
rem :: SomeWordN -> SomeWordN -> SomeWordN
rem = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 WordN n -> WordN n -> WordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
rem
quotRem :: SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
quotRem = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> (WordN n, WordN n))
-> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
binSomeWordNR2 WordN n -> WordN n -> (WordN n, WordN n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> (WordN n, WordN n)
forall a. Integral a => a -> a -> (a, a)
quotRem
div :: SomeWordN -> SomeWordN -> SomeWordN
div = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 WordN n -> WordN n -> WordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
div
mod :: SomeWordN -> SomeWordN -> SomeWordN
mod = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 WordN n -> WordN n -> WordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
mod
divMod :: SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
divMod = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> (WordN n, WordN n))
-> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
binSomeWordNR2 WordN n -> WordN n -> (WordN n, WordN n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> (WordN n, WordN n)
forall a. Integral a => a -> a -> (a, a)
divMod
toInteger :: SomeWordN -> Integer
toInteger = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> Integer)
-> SomeWordN -> Integer
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN WordN n -> Integer
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> Integer
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 = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y) WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
.&. WordN n
forall a. Bounded a => a
maxBound
WordN Integer
x * :: WordN n -> WordN n -> WordN n
* WordN Integer
y = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y) WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
.&. WordN n
forall a. Bounded a => a
maxBound
WordN Integer
x - :: WordN n -> WordN n -> WordN n
- WordN Integer
y
| Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
y = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)
| Bool
otherwise = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN ((Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)
negate :: WordN n -> WordN n
negate (WordN Integer
0) = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
0
negate WordN n
a = WordN n -> WordN n
forall a. Bits a => a -> a
complement WordN n
a WordN n -> WordN n -> WordN n
forall a. Num a => a -> a -> a
+ Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
1
abs :: WordN n -> WordN n
abs WordN n
x = WordN n
x
signum :: WordN n -> WordN n
signum (WordN Integer
0) = WordN n
0
signum WordN n
_ = WordN n
1
fromInteger :: Integer -> WordN n
fromInteger !Integer
x
| Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
0
| Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN n
forall a. Bounded a => a
maxBound :: WordN n))
| Bool
otherwise = -Integer -> WordN n
forall a. Num a => Integer -> a
fromInteger (-Integer
x)
instance Num SomeWordN where
+ :: SomeWordN -> SomeWordN -> SomeWordN
(+) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 WordN n -> WordN n -> WordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
forall a. Num a => a -> a -> a
(+)
(-) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 (-)
* :: SomeWordN -> SomeWordN -> SomeWordN
(*) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 WordN n -> WordN n -> WordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
forall a. Num a => a -> a -> a
(*)
negate :: SomeWordN -> SomeWordN
negate = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 WordN n -> WordN n
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n
forall a. Num a => a -> a
negate
abs :: SomeWordN -> SomeWordN
abs = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 WordN n -> WordN n
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n
forall a. Num a => a -> a
abs
signum :: SomeWordN -> SomeWordN
signum = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 WordN n -> WordN n
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> WordN n
forall a. Num a => a -> a
signum
fromInteger :: Integer -> SomeWordN
fromInteger = String -> Integer -> SomeWordN
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 = Gen (WordN n)
forall a. (Bounded a, Integral a) => Gen a
QC.arbitrarySizedBoundedIntegral
shrink :: WordN n -> [WordN n]
shrink WordN n
i
| WordN n
i WordN n -> WordN n -> Bool
forall a. Eq a => a -> a -> Bool
== WordN n
0 = []
| WordN n
i WordN n -> WordN n -> Bool
forall a. Eq a => a -> a -> Bool
== WordN n
1 = [WordN n
0]
| Bool
otherwise = WordN n -> [WordN n]
forall a. Integral a => a -> [a]
QC.shrinkIntegral WordN n
i
minusOneIntN :: forall proxy n. (KnownNat n) => proxy n -> IntN n
minusOneIntN :: forall (proxy :: Nat -> *) (n :: Nat).
KnownNat n =>
proxy n -> IntN n
minusOneIntN proxy n
_ = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
instance (KnownNat n, 1 <= n) => Bits (IntN n) where
IntN Integer
a .&. :: IntN n -> IntN n -> IntN n
.&. IntN Integer
b = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
b)
IntN Integer
a .|. :: IntN n -> IntN n -> IntN n
.|. IntN Integer
b = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
b)
IntN Integer
a xor :: IntN n -> IntN n -> IntN n
`xor` IntN Integer
b = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer
b)
complement :: IntN n -> IntN n
complement IntN n
a = Proxy n -> IntN n
forall (proxy :: Nat -> *) (n :: Nat).
KnownNat n =>
proxy n -> IntN n
minusOneIntN (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) IntN n -> IntN n -> IntN n
forall a. Bits a => a -> a -> a
`xor` IntN n
a
zeroBits :: IntN n
zeroBits = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
0
bit :: Int -> IntN n
bit Int
i = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (Int -> WordN n
forall a. Bits a => Int -> a
bit Int
i :: WordN n))
clearBit :: IntN n -> Int -> IntN n
clearBit (IntN Integer
a) Int
i = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
clearBit Integer
a Int
i)
testBit :: IntN n -> Int -> Bool
testBit (IntN Integer
a) = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a
bitSizeMaybe :: IntN n -> Maybe Int
bitSizeMaybe = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (IntN n -> Int) -> IntN n -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize
bitSize :: IntN n -> Int
bitSize = IntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize
isSigned :: IntN n -> Bool
isSigned IntN n
_ = Bool
True
shiftL :: IntN n -> Int -> IntN n
shiftL (IntN Integer
a) Int
i = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN n -> Integer) -> WordN n -> Integer
forall a b. (a -> b) -> a -> b
$ (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
a :: WordN n) WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
`shiftL` Int
i)
shiftR :: IntN n -> Int -> IntN n
shiftR IntN n
i Int
0 = IntN n
i
shiftR (IntN Integer
i) Int
k
| Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = if Bool
b then Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
maxi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) else Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
0
| Bool
otherwise = if Bool
b then Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
maxi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
noi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
k)) else Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
k)
where
b :: Bool
b = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
i (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
maxi :: Integer
maxi = (Integer
1 :: Integer) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
n
noi :: Integer
noi = (Integer
1 :: Integer) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k)
rotateL :: IntN n -> Int -> IntN n
rotateL (IntN Integer
i) Int
k = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> Integer -> IntN n
forall a b. (a -> b) -> a -> b
$ WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN n -> Integer) -> WordN n -> Integer
forall a b. (a -> b) -> a -> b
$ WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
rotateL (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
i :: WordN n) Int
k
rotateR :: IntN n -> Int -> IntN n
rotateR (IntN Integer
i) Int
k = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> Integer -> IntN n
forall a b. (a -> b) -> a -> b
$ WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN n -> Integer) -> WordN n -> Integer
forall a b. (a -> b) -> a -> b
$ WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
rotateR (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
i :: WordN n) Int
k
popCount :: IntN n -> Int
popCount (IntN Integer
i) = Integer -> Int
forall a. Bits a => a -> Int
popCount Integer
i
instance Bits SomeIntN where
.&. :: SomeIntN -> SomeIntN -> SomeIntN
(.&.) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Bits a => a -> a -> a
(.&.)
.|. :: SomeIntN -> SomeIntN -> SomeIntN
(.|.) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Bits a => a -> a -> a
(.|.)
xor :: SomeIntN -> SomeIntN -> SomeIntN
xor = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Bits a => a -> a -> a
xor
complement :: SomeIntN -> SomeIntN
complement = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 IntN n -> IntN n
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n
forall a. Bits a => a -> a
complement
shift :: SomeIntN -> Int -> SomeIntN
shift SomeIntN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (IntN n -> Int -> IntN n
forall a. Bits a => a -> Int -> a
`shift` Int
i) SomeIntN
s
rotate :: SomeIntN -> Int -> SomeIntN
rotate SomeIntN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (IntN n -> Int -> IntN n
forall a. Bits a => a -> Int -> a
`rotate` Int
i) SomeIntN
s
zeroBits :: SomeIntN
zeroBits = String -> SomeIntN
forall a. HasCallStack => String -> a
error String
"zeroBits is not defined for SomeIntN as no bitwidth is known"
bit :: Int -> SomeIntN
bit = String -> Int -> SomeIntN
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 :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (IntN n -> Int -> IntN n
forall a. Bits a => a -> Int -> a
`setBit` Int
i) SomeIntN
s
clearBit :: SomeIntN -> Int -> SomeIntN
clearBit SomeIntN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (IntN n -> Int -> IntN n
forall a. Bits a => a -> Int -> a
`clearBit` Int
i) SomeIntN
s
complementBit :: SomeIntN -> Int -> SomeIntN
complementBit SomeIntN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (IntN n -> Int -> IntN n
forall a. Bits a => a -> Int -> a
`complementBit` Int
i) SomeIntN
s
testBit :: SomeIntN -> Int -> Bool
testBit SomeIntN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> Bool)
-> SomeIntN -> Bool
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN (IntN n -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
i) SomeIntN
s
bitSizeMaybe :: SomeIntN -> Maybe Int
bitSizeMaybe = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (SomeIntN -> Int) -> SomeIntN -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeIntN -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize
bitSize :: SomeIntN -> Int
bitSize = SomeIntN -> Int
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 :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (IntN n -> Int -> IntN n
forall a. Bits a => a -> Int -> a
`shiftL` Int
i) SomeIntN
s
unsafeShiftL :: SomeIntN -> Int -> SomeIntN
unsafeShiftL SomeIntN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (IntN n -> Int -> IntN n
forall a. Bits a => a -> Int -> a
`unsafeShiftL` Int
i) SomeIntN
s
shiftR :: SomeIntN -> Int -> SomeIntN
shiftR SomeIntN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (IntN n -> Int -> IntN n
forall a. Bits a => a -> Int -> a
`shiftR` Int
i) SomeIntN
s
unsafeShiftR :: SomeIntN -> Int -> SomeIntN
unsafeShiftR SomeIntN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (IntN n -> Int -> IntN n
forall a. Bits a => a -> Int -> a
`unsafeShiftR` Int
i) SomeIntN
s
rotateL :: SomeIntN -> Int -> SomeIntN
rotateL SomeIntN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (IntN n -> Int -> IntN n
forall a. Bits a => a -> Int -> a
`rotateL` Int
i) SomeIntN
s
rotateR :: SomeIntN -> Int -> SomeIntN
rotateR SomeIntN
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (IntN n -> Int -> IntN n
forall a. Bits a => a -> Int -> a
`rotateR` Int
i) SomeIntN
s
popCount :: SomeIntN -> Int
popCount = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> Int)
-> SomeIntN -> Int
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN IntN n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> Int
forall a. Bits a => a -> Int
popCount
instance (KnownNat n, 1 <= n) => FiniteBits (IntN n) where
finiteBitSize :: IntN n -> Int
finiteBitSize IntN n
_ = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
instance FiniteBits SomeIntN where
finiteBitSize :: SomeIntN -> Int
finiteBitSize (SomeIntN (IntN n
n :: IntN n)) = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ IntN n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal IntN n
n
countLeadingZeros :: SomeIntN -> Int
countLeadingZeros = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> Int)
-> SomeIntN -> Int
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN IntN n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> Int
forall b. FiniteBits b => b -> Int
countLeadingZeros
countTrailingZeros :: SomeIntN -> Int
countTrailingZeros = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> Int)
-> SomeIntN -> Int
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN IntN n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> Int
forall b. FiniteBits b => b -> Int
countTrailingZeros
instance (KnownNat n, 1 <= n) => Bounded (IntN n) where
maxBound :: IntN n
maxBound = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
minBound :: IntN n
minBound = IntN n
forall a. Bounded a => a
maxBound IntN n -> IntN n -> IntN n
forall a. Num a => a -> a -> a
+ IntN n
1
instance (KnownNat n, 1 <= n) => Enum (IntN n) where
succ :: IntN n -> IntN n
succ IntN n
x
| IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
/= IntN n
forall a. Bounded a => a
maxBound = IntN n
x IntN n -> IntN n -> IntN n
forall a. Num a => a -> a -> a
+ IntN n
1
| Bool
otherwise = String -> IntN n
forall a. String -> a
succError (String -> IntN n) -> String -> IntN n
forall a b. (a -> b) -> a -> b
$ String
"IntN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
pred :: IntN n -> IntN n
pred IntN n
x
| IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
/= IntN n
forall a. Bounded a => a
minBound = IntN n
x IntN n -> IntN n -> IntN n
forall a. Num a => a -> a -> a
- IntN n
1
| Bool
otherwise = String -> IntN n
forall a. String -> a
predError (String -> IntN n) -> String -> IntN n
forall a b. (a -> b) -> a -> b
$ String
"IntN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
toEnum :: Int -> IntN n
toEnum Int
i
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= IntN n -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (IntN n
forall a. Bounded a => a
minBound :: IntN n) Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= IntN n -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (IntN n
forall a. Bounded a => a
maxBound :: IntN n) = Int -> IntN n
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i
| Bool
otherwise = String -> Int -> (WordN n, WordN n) -> IntN n
forall a b. Show a => String -> Int -> (a, a) -> b
toEnumError (String
"IntN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Nat -> String
forall a. Show a => a -> String
show (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))) Int
i (WordN n
forall a. Bounded a => a
minBound :: WordN n, WordN n
forall a. Bounded a => a
maxBound :: WordN n)
fromEnum :: IntN n -> Int
fromEnum = Integer -> Int
forall a. Enum a => a -> Int
fromEnum (Integer -> Int) -> (IntN n -> Integer) -> IntN n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger
enumFrom :: IntN n -> [IntN n]
enumFrom = IntN n -> [IntN n]
forall a. (Enum a, Bounded a) => a -> [a]
boundedEnumFrom
{-# INLINE enumFrom #-}
enumFromThen :: IntN n -> IntN n -> [IntN n]
enumFromThen = IntN n -> IntN n -> [IntN n]
forall a. (Enum a, Bounded a) => a -> a -> [a]
boundedEnumFromThen
{-# INLINE enumFromThen #-}
instance Enum SomeIntN where
toEnum :: Int -> SomeIntN
toEnum = String -> Int -> SomeIntN
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 = String -> SomeIntN -> Int
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 = IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
i Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1
instance Real SomeIntN where
toRational :: SomeIntN -> Rational
toRational = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> Rational)
-> SomeIntN -> Rational
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN IntN n -> Rational
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> Rational
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 IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& IntN n
y IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== -IntN n
1
then ArithException -> IntN n
forall a e. Exception e => e -> a
throw ArithException
Overflow
else Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
y)
rem :: IntN n -> IntN n -> IntN n
rem IntN n
x IntN n
y = Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
y)
quotRem :: IntN n -> IntN n -> (IntN n, IntN n)
quotRem IntN n
x IntN n
y =
if IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& IntN n
y IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== -IntN n
1
then ArithException -> (IntN n, IntN n)
forall a e. Exception e => e -> a
throw ArithException
Overflow
else case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
quotRem (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x) (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
y) of
(Integer
q, Integer
r) -> (Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger Integer
q, Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger Integer
r)
div :: IntN n -> IntN n -> IntN n
div IntN n
x IntN n
y =
if IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& IntN n
y IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== -IntN n
1
then ArithException -> IntN n
forall a e. Exception e => e -> a
throw ArithException
Overflow
else Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
y)
mod :: IntN n -> IntN n -> IntN n
mod IntN n
x IntN n
y = Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
y)
divMod :: IntN n -> IntN n -> (IntN n, IntN n)
divMod IntN n
x IntN n
y =
if IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& IntN n
y IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== -IntN n
1
then ArithException -> (IntN n, IntN n)
forall a e. Exception e => e -> a
throw ArithException
Overflow
else case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x) (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
y) of
(Integer
q, Integer
r) -> (Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger Integer
q, Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger Integer
r)
toInteger :: IntN n -> Integer
toInteger i :: IntN n
i@(IntN Integer
n) = case IntN n -> IntN n
forall a. Num a => a -> a
signum IntN n
i of
IntN n
0 -> Integer
0
-1 ->
let x :: IntN n
x = IntN n -> IntN n
forall a. Num a => a -> a
negate IntN n
i
in if IntN n -> IntN n
forall a. Num a => a -> a
signum IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== -IntN n
1 then -Integer
n else Integer -> Integer
forall a. Num a => a -> a
negate (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x)
IntN n
1 -> Integer
n
IntN n
_ -> Integer
forall a. HasCallStack => a
undefined
instance Integral SomeIntN where
quot :: SomeIntN -> SomeIntN -> SomeIntN
quot = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Integral a => a -> a -> a
quot
rem :: SomeIntN -> SomeIntN -> SomeIntN
rem = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Integral a => a -> a -> a
rem
quotRem :: SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
quotRem = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> (IntN n, IntN n))
-> SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
binSomeIntNR2 IntN n -> IntN n -> (IntN n, IntN n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> (IntN n, IntN n)
forall a. Integral a => a -> a -> (a, a)
quotRem
div :: SomeIntN -> SomeIntN -> SomeIntN
div = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Integral a => a -> a -> a
div
mod :: SomeIntN -> SomeIntN -> SomeIntN
mod = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Integral a => a -> a -> a
mod
divMod :: SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
divMod = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> (IntN n, IntN n))
-> SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
binSomeIntNR2 IntN n -> IntN n -> (IntN n, IntN n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> (IntN n, IntN n)
forall a. Integral a => a -> a -> (a, a)
divMod
toInteger :: SomeIntN -> Integer
toInteger = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> Integer)
-> SomeIntN -> Integer
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN IntN n -> Integer
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> Integer
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 = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y) IntN n -> IntN n -> IntN n
forall a. Bits a => a -> a -> a
.&. Proxy n -> IntN n
forall (proxy :: Nat -> *) (n :: Nat).
KnownNat n =>
proxy n -> IntN n
minusOneIntN (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
IntN Integer
x * :: IntN n -> IntN n -> IntN n
* IntN Integer
y = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y) IntN n -> IntN n -> IntN n
forall a. Bits a => a -> a -> a
.&. Proxy n -> IntN n
forall (proxy :: Nat -> *) (n :: Nat).
KnownNat n =>
proxy n -> IntN n
minusOneIntN (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
IntN Integer
x - :: IntN n -> IntN n -> IntN n
- IntN Integer
y
| Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
y = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)
| Bool
otherwise = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN ((Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)
negate :: IntN n -> IntN n
negate (IntN Integer
0) = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
0
negate IntN n
a = IntN n -> IntN n
forall a. Bits a => a -> a
complement IntN n
a IntN n -> IntN n -> IntN n
forall a. Num a => a -> a -> a
+ Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
1
abs :: IntN n -> IntN n
abs IntN n
x = if IntN n -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit IntN n
x (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) then IntN n -> IntN n
forall a. Num a => a -> a
negate IntN n
x else IntN n
x
signum :: IntN n -> IntN n
signum (IntN Integer
0) = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
0
signum IntN n
i = if IntN n -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit IntN n
i (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) then -IntN n
1 else IntN n
1
fromInteger :: Integer -> IntN n
fromInteger !Integer
x = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> Integer -> IntN n
forall a b. (a -> b) -> a -> b
$ if Integer
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 then Integer
v else (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
n) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
v
where
v :: Integer
v = WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (Integer -> WordN n
forall a. Num a => Integer -> a
fromInteger (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
maxn) :: WordN n) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
maxn
n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
maxn :: Integer
maxn = Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
instance Num SomeIntN where
+ :: SomeIntN -> SomeIntN -> SomeIntN
(+) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Num a => a -> a -> a
(+)
(-) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 (-)
* :: SomeIntN -> SomeIntN -> SomeIntN
(*) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Num a => a -> a -> a
(*)
negate :: SomeIntN -> SomeIntN
negate = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 IntN n -> IntN n
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n
forall a. Num a => a -> a
negate
abs :: SomeIntN -> SomeIntN
abs = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 IntN n -> IntN n
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n
forall a. Num a => a -> a
abs
signum :: SomeIntN -> SomeIntN
signum = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 IntN n -> IntN n
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n
forall a. Num a => a -> a
signum
fromInteger :: Integer -> SomeIntN
fromInteger = String -> Integer -> SomeIntN
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
b
where
n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
as :: Bool
as = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
bs :: Bool
bs = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
b (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
instance (KnownNat n, 1 <= n) => QC.Arbitrary (IntN n) where
arbitrary :: Gen (IntN n)
arbitrary = Gen (IntN n)
forall a. (Bounded a, Integral a) => Gen a
QC.arbitrarySizedBoundedIntegral
shrink :: IntN n -> [IntN n]
shrink IntN n
i
| IntN n
i IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
0 = []
| IntN n
i IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
1 = [IntN n
0]
| Bool
otherwise = IntN n -> [IntN n]
forall a. Integral a => a -> [a]
QC.shrinkIntegral IntN n
i
instance SizedBV WordN where
sizedBVConcat :: forall l r. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => WordN l -> WordN r -> WordN (l + r)
sizedBVConcat :: forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
WordN l -> WordN r -> WordN (l + r)
sizedBVConcat (WordN Integer
a) (WordN Integer
b) = Integer -> WordN (l + r)
forall (n :: Nat). Integer -> WordN n
WordN ((Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy r -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy r
forall {k} (t :: k). Proxy t
Proxy :: Proxy r))) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
b)
sizedBVZext :: forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
sizedBVZext proxy r
_ (WordN Integer
v) = Integer -> WordN r
forall (n :: Nat). Integer -> WordN n
WordN Integer
v
sizedBVSext :: forall l r proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r
sizedBVSext :: forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
sizedBVSext proxy r
pr (WordN Integer
v) = if Bool
s then Integer -> WordN r
forall (n :: Nat). Integer -> WordN n
WordN (Integer
maxi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
noi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
v) else Integer -> WordN r
forall (n :: Nat). Integer -> WordN n
WordN Integer
v
where
r :: Int
r = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ proxy r -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal proxy r
pr
l :: Int
l = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy l -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy l
forall {k} (t :: k). Proxy t
Proxy :: Proxy l)
s :: Bool
s = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
v (Int
l Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
maxi :: Integer
maxi = (Integer
1 :: Integer) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
r
noi :: Integer
noi = (Integer
1 :: Integer) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
l
sizedBVExt :: forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
sizedBVExt = proxy r -> WordN l -> WordN r
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVZext
sizedBVSelect ::
forall n ix w p q.
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) =>
p ix ->
q w ->
WordN n ->
WordN w
sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) (p :: Nat -> *)
(q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n) =>
p ix -> q w -> WordN n -> WordN w
sizedBVSelect p ix
pix q w
pw (WordN Integer
v) = Integer -> WordN w
forall (n :: Nat). Integer -> WordN n
WordN ((Integer
v Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
ix) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask)
where
ix :: Int
ix = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ p ix -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal p ix
pix
w :: Int
w = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ q w -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal q w
pw
mask :: Integer
mask = (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
w) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
instance SizedBV IntN where
sizedBVConcat :: forall l r. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => IntN l -> IntN r -> IntN (l + r)
sizedBVConcat :: forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
IntN l -> IntN r -> IntN (l + r)
sizedBVConcat (IntN Integer
a) (IntN Integer
b) = Integer -> IntN (l + r)
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN (l + r)) -> Integer -> IntN (l + r)
forall a b. (a -> b) -> a -> b
$ WordN (l + r) -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN (l + r) -> Integer) -> WordN (l + r) -> Integer
forall a b. (a -> b) -> a -> b
$ WordN l -> WordN r -> WordN (l + r)
forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
WordN l -> WordN r -> WordN (l + r)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat (Integer -> WordN l
forall (n :: Nat). Integer -> WordN n
WordN Integer
a :: WordN l) (Integer -> WordN r
forall (n :: Nat). Integer -> WordN n
WordN Integer
b :: WordN r)
sizedBVZext :: forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> IntN l -> IntN r
sizedBVZext proxy r
_ (IntN Integer
v) = Integer -> IntN r
forall (n :: Nat). Integer -> IntN n
IntN Integer
v
sizedBVSext :: forall l r proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r
sizedBVSext :: forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> IntN l -> IntN r
sizedBVSext proxy r
pr (IntN Integer
v) = Integer -> IntN r
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN r) -> Integer -> IntN r
forall a b. (a -> b) -> a -> b
$ WordN r -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN r -> Integer) -> WordN r -> Integer
forall a b. (a -> b) -> a -> b
$ proxy r -> WordN l -> WordN r
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVSext proxy r
pr (Integer -> WordN l
forall (n :: Nat). Integer -> WordN n
WordN Integer
v :: WordN l)
sizedBVExt :: forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> IntN l -> IntN r
sizedBVExt = proxy r -> IntN l -> IntN r
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> IntN l -> IntN r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVSext
sizedBVSelect ::
forall n ix w p q.
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) =>
p ix ->
q w ->
IntN n ->
IntN w
sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) (p :: Nat -> *)
(q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n) =>
p ix -> q w -> IntN n -> IntN w
sizedBVSelect p ix
pix q w
pw (IntN Integer
v) = Integer -> IntN w
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN w) -> Integer -> IntN w
forall a b. (a -> b) -> a -> b
$ WordN w -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN w -> Integer) -> WordN w -> Integer
forall a b. (a -> b) -> a -> b
$ p ix -> q w -> WordN n -> WordN w
forall (n :: Nat) (ix :: Nat) (w :: Nat) (p :: Nat -> *)
(q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n) =>
p ix -> q w -> WordN n -> WordN w
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
(p :: Nat -> *) (q :: Nat -> *).
(SizedBV bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n) =>
p ix -> q w -> bv n -> bv w
sizedBVSelect p ix
pix q w
pw (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
v :: WordN n)
instance BV SomeWordN where
bvConcat :: SomeWordN -> SomeWordN -> SomeWordN
bvConcat (SomeWordN (WordN n
a :: WordN l)) (SomeWordN (WordN n
b :: WordN r)) =
case (Proxy n -> Proxy n -> LeqProof 1 (n + n)
forall (m :: Nat) (n :: Nat) (p :: Nat -> *) (q :: Nat -> *).
(1 <= m, 1 <= n) =>
p m -> q n -> LeqProof 1 (m + n)
leqAddPos (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r), forall (m :: Nat) (n :: Nat).
KnownProof m -> KnownProof n -> KnownProof (m + n)
knownAdd @l @r KnownProof n
forall (n :: Nat). KnownNat n => KnownProof n
KnownProof KnownProof n
forall (n :: Nat). KnownNat n => KnownProof n
KnownProof) of
(LeqProof 1 (n + n)
LeqProof, KnownProof (n + n)
KnownProof) ->
WordN (n + n) -> SomeWordN
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN (WordN (n + n) -> SomeWordN) -> WordN (n + n) -> SomeWordN
forall a b. (a -> b) -> a -> b
$ WordN n -> WordN n -> WordN (n + n)
forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
WordN l -> WordN r -> WordN (l + r)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat WordN n
a WordN n
b
{-# INLINE bvConcat #-}
bvZext :: Int -> SomeWordN -> SomeWordN
bvZext Int
l (SomeWordN (WordN n
a :: WordN n))
| Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n = String -> SomeWordN
forall a. HasCallStack => String -> a
error String
"bvZext: trying to zero extend a value to a smaller size"
| Bool
otherwise = Proxy n -> SomeWordN
forall (l :: Nat). Proxy l -> SomeWordN
res (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
where
n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
res :: forall (l :: Nat). Proxy l -> SomeWordN
res :: forall (l :: Nat). Proxy l -> SomeWordN
res Proxy l
p =
case (forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @l (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l), forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @l, forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @n @l) of
(KnownProof l
KnownProof, LeqProof 1 l
LeqProof, LeqProof n l
LeqProof) -> WordN l -> SomeWordN
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN (WordN l -> SomeWordN) -> WordN l -> SomeWordN
forall a b. (a -> b) -> a -> b
$ Proxy l -> WordN n -> WordN l
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVZext Proxy l
p WordN n
a
bvSext :: Int -> SomeWordN -> SomeWordN
bvSext Int
l (SomeWordN (WordN n
a :: WordN n))
| Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n = String -> SomeWordN
forall a. HasCallStack => String -> a
error String
"bvSext: trying to zero extend a value to a smaller size"
| Bool
otherwise = Proxy n -> SomeWordN
forall (l :: Nat). Proxy l -> SomeWordN
res (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
where
n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
res :: forall (l :: Nat). Proxy l -> SomeWordN
res :: forall (l :: Nat). Proxy l -> SomeWordN
res Proxy l
p =
case (forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @l (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l), forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @l, forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @n @l) of
(KnownProof l
KnownProof, LeqProof 1 l
LeqProof, LeqProof n l
LeqProof) -> WordN l -> SomeWordN
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN (WordN l -> SomeWordN) -> WordN l -> SomeWordN
forall a b. (a -> b) -> a -> b
$ Proxy l -> WordN n -> WordN l
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVSext Proxy l
p WordN n
a
bvExt :: Int -> SomeWordN -> SomeWordN
bvExt = Int -> SomeWordN -> SomeWordN
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
w Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n = String -> SomeWordN
forall a. HasCallStack => String -> a
error String
"bvSelect: trying to select a bitvector outside the bounds of the input"
| Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = String -> SomeWordN
forall a. HasCallStack => String -> a
error String
"bvSelect: trying to select a bitvector of size 0"
| Bool
otherwise = Proxy n -> Proxy n -> SomeWordN
forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> SomeWordN
res (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
where
n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> SomeWordN
res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> SomeWordN
res Proxy w
_ Proxy ix
_ =
case ( forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @ix (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
ix),
forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @w (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
w),
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @w,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @(ix + w) @n
) of
(KnownProof ix
KnownProof, KnownProof w
KnownProof, LeqProof 1 w
LeqProof, LeqProof (ix + w) n
LeqProof) ->
WordN w -> SomeWordN
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN (WordN w -> SomeWordN) -> WordN w -> SomeWordN
forall a b. (a -> b) -> a -> b
$ Proxy ix -> Proxy w -> WordN n -> WordN w
forall (n :: Nat) (ix :: Nat) (w :: Nat) (p :: Nat -> *)
(q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n) =>
p ix -> q w -> WordN n -> WordN w
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
(p :: Nat -> *) (q :: Nat -> *).
(SizedBV bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n) =>
p ix -> q w -> bv n -> bv w
sizedBVSelect (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @ix) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) WordN n
a
instance BV SomeIntN where
bvConcat :: SomeIntN -> SomeIntN -> SomeIntN
bvConcat SomeIntN
l SomeIntN
r = SomeWordN -> SomeIntN
forall ubv sbv. SignConversion ubv sbv => ubv -> sbv
toSigned (SomeWordN -> SomeIntN) -> SomeWordN -> SomeIntN
forall a b. (a -> b) -> a -> b
$ SomeWordN -> SomeWordN -> SomeWordN
forall bv. BV bv => bv -> bv -> bv
bvConcat (SomeIntN -> SomeWordN
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned SomeIntN
l) (SomeIntN -> SomeWordN
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned SomeIntN
r)
{-# INLINE bvConcat #-}
bvZext :: Int -> SomeIntN -> SomeIntN
bvZext Int
l = SomeWordN -> SomeIntN
forall ubv sbv. SignConversion ubv sbv => ubv -> sbv
toSigned (SomeWordN -> SomeIntN)
-> (SomeIntN -> SomeWordN) -> SomeIntN -> SomeIntN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SomeWordN -> SomeWordN
forall bv. BV bv => Int -> bv -> bv
bvZext Int
l (SomeWordN -> SomeWordN)
-> (SomeIntN -> SomeWordN) -> SomeIntN -> SomeWordN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeIntN -> SomeWordN
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned
{-# INLINE bvZext #-}
bvSext :: Int -> SomeIntN -> SomeIntN
bvSext Int
l = SomeWordN -> SomeIntN
forall ubv sbv. SignConversion ubv sbv => ubv -> sbv
toSigned (SomeWordN -> SomeIntN)
-> (SomeIntN -> SomeWordN) -> SomeIntN -> SomeIntN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SomeWordN -> SomeWordN
forall bv. BV bv => Int -> bv -> bv
bvSext Int
l (SomeWordN -> SomeWordN)
-> (SomeIntN -> SomeWordN) -> SomeIntN -> SomeWordN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeIntN -> SomeWordN
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned
{-# INLINE bvSext #-}
bvExt :: Int -> SomeIntN -> SomeIntN
bvExt Int
l = SomeWordN -> SomeIntN
forall ubv sbv. SignConversion ubv sbv => ubv -> sbv
toSigned (SomeWordN -> SomeIntN)
-> (SomeIntN -> SomeWordN) -> SomeIntN -> SomeIntN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SomeWordN -> SomeWordN
forall bv. BV bv => Int -> bv -> bv
bvExt Int
l (SomeWordN -> SomeWordN)
-> (SomeIntN -> SomeWordN) -> SomeIntN -> SomeWordN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeIntN -> SomeWordN
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned
{-# INLINE bvExt #-}
bvSelect :: Int -> Int -> SomeIntN -> SomeIntN
bvSelect Int
ix Int
w = SomeWordN -> SomeIntN
forall ubv sbv. SignConversion ubv sbv => ubv -> sbv
toSigned (SomeWordN -> SomeIntN)
-> (SomeIntN -> SomeWordN) -> SomeIntN -> SomeIntN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> SomeWordN -> SomeWordN
forall bv. BV bv => Int -> Int -> bv -> bv
bvSelect Int
ix Int
w (SomeWordN -> SomeWordN)
-> (SomeIntN -> SomeWordN) -> SomeIntN -> SomeWordN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeIntN -> SomeWordN
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned
{-# INLINE bvSelect #-}
instance (KnownNat n, 1 <= n) => SignConversion (WordN n) (IntN n) where
toSigned :: WordN n -> IntN n
toSigned (WordN Integer
i) = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
i
toUnsigned :: IntN n -> WordN n
toUnsigned (IntN Integer
i) = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
i
instance SignConversion SomeWordN SomeIntN where
toSigned :: SomeWordN -> SomeIntN
toSigned (SomeWordN WordN n
i) = IntN n -> SomeIntN
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN (IntN n -> SomeIntN) -> IntN n -> SomeIntN
forall a b. (a -> b) -> a -> b
$ WordN n -> IntN n
forall ubv sbv. SignConversion ubv sbv => ubv -> sbv
toSigned WordN n
i
toUnsigned :: SomeIntN -> SomeWordN
toUnsigned (SomeIntN IntN n
i) = WordN n -> SomeWordN
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN (WordN n -> SomeWordN) -> WordN n -> SomeWordN
forall a b. (a -> b) -> a -> b
$ IntN n -> WordN n
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned IntN n
i
deriving via
(DefaultFiniteBitsSymShift (IntN n))
instance
(KnownNat n, 1 <= n) => SymShift (IntN n)
deriving via
(DefaultFiniteBitsSymShift (WordN n))
instance
(KnownNat n, 1 <= n) => SymShift (WordN n)
deriving via
(DefaultFiniteBitsSymRotate (IntN n))
instance
(KnownNat n, 1 <= n) => SymRotate (IntN n)
deriving via
(DefaultFiniteBitsSymRotate (WordN n))
instance
(KnownNat n, 1 <= n) => SymRotate (WordN n)