{-|
Copyright  :  (C) 2013-2016, University of Twente,
                  2016     , Myrtle Software Ltd
License    :  BSD2 (see the file LICENSE)
Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
-}

{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DeriveAnyClass             #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE MagicHash                  #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE UndecidableInstances       #-}

{-# LANGUAGE Unsafe #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_HADDOCK show-extensions not-home #-}

module Clash.Sized.Internal.Unsigned
  ( -- * Datatypes
    Unsigned (..)
    -- * Accessors
    -- ** Length information
  , size#
    -- * Type classes
    -- ** BitPack
  , pack#
  , unpack#
    -- ** Eq
  , eq#
  , neq#
    -- ** Ord
  , lt#
  , ge#
  , gt#
  , le#
    -- ** Enum (not synthesizable)
  , enumFrom#
  , enumFromThen#
  , enumFromTo#
  , enumFromThenTo#
    -- ** Bounded
  , minBound#
  , maxBound#
    -- ** Num
  , (+#)
  , (-#)
  , (*#)
  , negate#
  , fromInteger#
    -- ** ExtendingNum
  , plus#
  , minus#
  , times#
    -- ** Integral
  , quot#
  , rem#
  , toInteger#
    -- ** Bits
  , and#
  , or#
  , xor#
  , complement#
  , shiftL#
  , shiftR#
  , rotateL#
  , rotateR#
    -- ** Resize
  , resize#
  )
where

import Control.DeepSeq                (NFData (..))
import Control.Lens                   (Index, Ixed (..), IxValue)
import Data.Bits                      (Bits (..), FiniteBits (..))
import Data.Data                      (Data)
import Data.Default.Class             (Default (..))
import Data.Proxy                     (Proxy (..))
import Text.Read                      (Read (..), ReadPrec)
import GHC.Generics                   (Generic)
import GHC.TypeLits                   (KnownNat, Nat, type (+), natVal)
import GHC.TypeLits.Extra             (Max)
import Language.Haskell.TH            (TypeQ, appT, conT, litT, numTyLit, sigE)
import Language.Haskell.TH.Syntax     (Lift(..))
import Numeric.Natural                (Natural)
import Test.QuickCheck.Arbitrary      (Arbitrary (..), CoArbitrary (..),
                                       arbitraryBoundedIntegral,
                                       coarbitraryIntegral)

import Clash.Class.BitPack            (BitPack (..), packXWith)
import Clash.Class.Num                (ExtendingNum (..), SaturatingNum (..),
                                       SaturationMode (..))
import Clash.Class.Resize             (Resize (..))
import Clash.Prelude.BitIndex         ((!), msb, replaceBit, split)
import Clash.Prelude.BitReduction     (reduceOr)
import Clash.Sized.Internal.BitVector (BitVector (BV), Bit, high, low, undefError)
import qualified Clash.Sized.Internal.BitVector as BV
import Clash.XException
  (ShowX (..), NFDataX (..), errorX, showsPrecXWith, rwhnfX)

-- | Arbitrary-width unsigned integer represented by @n@ bits
--
-- Given @n@ bits, an 'Unsigned' @n@ number has a range of: [0 .. 2^@n@-1]
--
-- __NB__: The 'Num' operators perform @wrap-around@ on overflow. If you want
-- saturation on overflow, check out the 'SaturatingNum' class.
--
-- >>> maxBound :: Unsigned 3
-- 7
-- >>> minBound :: Unsigned 3
-- 0
-- >>> read (show (maxBound :: Unsigned 3)) :: Unsigned 3
-- 7
-- >>> 1 + 2 :: Unsigned 3
-- 3
-- >>> 2 + 6 :: Unsigned 3
-- 0
-- >>> 1 - 3 :: Unsigned 3
-- 6
-- >>> 2 * 3 :: Unsigned 3
-- 6
-- >>> 2 * 4 :: Unsigned 3
-- 0
-- >>> (2 :: Unsigned 3) `mul` (4 :: Unsigned 3) :: Unsigned 6
-- 8
-- >>> (2 :: Unsigned 3) `add` (6 :: Unsigned 3) :: Unsigned 4
-- 8
-- >>> satAdd SatSymmetric 2 6 :: Unsigned 3
-- 7
-- >>> satSub SatSymmetric 2 3 :: Unsigned 3
-- 0
newtype Unsigned (n :: Nat) =
    -- | The constructor, 'U', and the field, 'unsafeToInteger', are not
    -- synthesizable.
    U { Unsigned n -> Integer
unsafeToInteger :: Integer }
  deriving (Typeable (Unsigned n)
DataType
Constr
Typeable (Unsigned n) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Unsigned n -> c (Unsigned n))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Unsigned n))
-> (Unsigned n -> Constr)
-> (Unsigned n -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Unsigned n)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Unsigned n)))
-> ((forall b. Data b => b -> b) -> Unsigned n -> Unsigned n)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Unsigned n -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Unsigned n -> r)
-> (forall u. (forall d. Data d => d -> u) -> Unsigned n -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Unsigned n -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n))
-> Data (Unsigned n)
Unsigned n -> DataType
Unsigned n -> Constr
(forall b. Data b => b -> b) -> Unsigned n -> Unsigned n
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Unsigned n -> c (Unsigned n)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Unsigned n)
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Unsigned n -> u
forall u. (forall d. Data d => d -> u) -> Unsigned n -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Unsigned n -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Unsigned n -> r
forall (n :: Nat). KnownNat n => Typeable (Unsigned n)
forall (n :: Nat). KnownNat n => Unsigned n -> DataType
forall (n :: Nat). KnownNat n => Unsigned n -> Constr
forall (n :: Nat).
KnownNat n =>
(forall b. Data b => b -> b) -> Unsigned n -> Unsigned n
forall (n :: Nat) u.
KnownNat n =>
Int -> (forall d. Data d => d -> u) -> Unsigned n -> u
forall (n :: Nat) u.
KnownNat n =>
(forall d. Data d => d -> u) -> Unsigned n -> [u]
forall (n :: Nat) r r'.
KnownNat n =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Unsigned n -> r
forall (n :: Nat) r r'.
KnownNat n =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Unsigned n -> r
forall (n :: Nat) (m :: * -> *).
(KnownNat n, Monad m) =>
(forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n)
forall (n :: Nat) (m :: * -> *).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n)
forall (n :: Nat) (c :: * -> *).
KnownNat n =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Unsigned n)
forall (n :: Nat) (c :: * -> *).
KnownNat n =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Unsigned n -> c (Unsigned n)
forall (n :: Nat) (t :: * -> *) (c :: * -> *).
(KnownNat n, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Unsigned n))
forall (n :: Nat) (t :: * -> * -> *) (c :: * -> *).
(KnownNat n, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Unsigned n))
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Unsigned n)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Unsigned n -> c (Unsigned n)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Unsigned n))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Unsigned n))
$cU :: Constr
$tUnsigned :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n)
$cgmapMo :: forall (n :: Nat) (m :: * -> *).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n)
gmapMp :: (forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n)
$cgmapMp :: forall (n :: Nat) (m :: * -> *).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n)
gmapM :: (forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n)
$cgmapM :: forall (n :: Nat) (m :: * -> *).
(KnownNat n, Monad m) =>
(forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Unsigned n -> u
$cgmapQi :: forall (n :: Nat) u.
KnownNat n =>
Int -> (forall d. Data d => d -> u) -> Unsigned n -> u
gmapQ :: (forall d. Data d => d -> u) -> Unsigned n -> [u]
$cgmapQ :: forall (n :: Nat) u.
KnownNat n =>
(forall d. Data d => d -> u) -> Unsigned n -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Unsigned n -> r
$cgmapQr :: forall (n :: Nat) r r'.
KnownNat n =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Unsigned n -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Unsigned n -> r
$cgmapQl :: forall (n :: Nat) r r'.
KnownNat n =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Unsigned n -> r
gmapT :: (forall b. Data b => b -> b) -> Unsigned n -> Unsigned n
$cgmapT :: forall (n :: Nat).
KnownNat n =>
(forall b. Data b => b -> b) -> Unsigned n -> Unsigned n
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Unsigned n))
$cdataCast2 :: forall (n :: Nat) (t :: * -> * -> *) (c :: * -> *).
(KnownNat n, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Unsigned n))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Unsigned n))
$cdataCast1 :: forall (n :: Nat) (t :: * -> *) (c :: * -> *).
(KnownNat n, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Unsigned n))
dataTypeOf :: Unsigned n -> DataType
$cdataTypeOf :: forall (n :: Nat). KnownNat n => Unsigned n -> DataType
toConstr :: Unsigned n -> Constr
$ctoConstr :: forall (n :: Nat). KnownNat n => Unsigned n -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Unsigned n)
$cgunfold :: forall (n :: Nat) (c :: * -> *).
KnownNat n =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Unsigned n)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Unsigned n -> c (Unsigned n)
$cgfoldl :: forall (n :: Nat) (c :: * -> *).
KnownNat n =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Unsigned n -> c (Unsigned n)
$cp1Data :: forall (n :: Nat). KnownNat n => Typeable (Unsigned n)
Data, (forall x. Unsigned n -> Rep (Unsigned n) x)
-> (forall x. Rep (Unsigned n) x -> Unsigned n)
-> Generic (Unsigned n)
forall x. Rep (Unsigned n) x -> Unsigned n
forall x. Unsigned n -> Rep (Unsigned n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (n :: Nat) x. Rep (Unsigned n) x -> Unsigned n
forall (n :: Nat) x. Unsigned n -> Rep (Unsigned n) x
$cto :: forall (n :: Nat) x. Rep (Unsigned n) x -> Unsigned n
$cfrom :: forall (n :: Nat) x. Unsigned n -> Rep (Unsigned n) x
Generic)

{-# NOINLINE size# #-}
size# :: KnownNat n => Unsigned n -> Int
size# :: Unsigned n -> Int
size# u :: Unsigned n
u = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Unsigned n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Unsigned n
u)

instance NFData (Unsigned n) where
  rnf :: Unsigned n -> ()
rnf (U i :: Integer
i) = Integer -> ()
forall a. NFData a => a -> ()
rnf Integer
i () -> () -> ()
forall a b. a -> b -> b
`seq` ()
  {-# NOINLINE rnf #-}
  -- NOINLINE is needed so that Clash doesn't trip on the "Unsigned ~# Integer"
  -- coercion

instance Show (Unsigned n) where
  show :: Unsigned n -> String
show (U i :: Integer
i) = Integer -> String
forall a. Show a => a -> String
show Integer
i
  {-# NOINLINE show #-}

instance ShowX (Unsigned n) where
  showsPrecX :: Int -> Unsigned n -> ShowS
showsPrecX = (Int -> Unsigned n -> ShowS) -> Int -> Unsigned n -> ShowS
forall a. (Int -> a -> ShowS) -> Int -> a -> ShowS
showsPrecXWith Int -> Unsigned n -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

instance NFDataX (Unsigned n) where
  deepErrorX :: String -> Unsigned n
deepErrorX = String -> Unsigned n
forall a. HasCallStack => String -> a
errorX
  rnfX :: Unsigned n -> ()
rnfX = Unsigned n -> ()
forall a. a -> ()
rwhnfX

-- | None of the 'Read' class' methods are synthesizable.
instance KnownNat n => Read (Unsigned n) where
  readPrec :: ReadPrec (Unsigned n)
readPrec = Natural -> Unsigned n
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Unsigned n)
-> ReadPrec Natural -> ReadPrec (Unsigned n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ReadPrec Natural
forall a. Read a => ReadPrec a
readPrec :: ReadPrec Natural)

instance KnownNat n => BitPack (Unsigned n) where
  type BitSize (Unsigned n) = n
  pack :: Unsigned n -> BitVector (BitSize (Unsigned n))
pack   = (Unsigned n -> BitVector n) -> Unsigned n -> BitVector n
forall (n :: Nat) a.
KnownNat n =>
(a -> BitVector n) -> a -> BitVector n
packXWith Unsigned n -> BitVector n
forall (n :: Nat). Unsigned n -> BitVector n
pack#
  unpack :: BitVector (BitSize (Unsigned n)) -> Unsigned n
unpack = BitVector (BitSize (Unsigned n)) -> Unsigned n
forall (n :: Nat). KnownNat n => BitVector n -> Unsigned n
unpack#

{-# NOINLINE pack# #-}
pack# :: Unsigned n -> BitVector n
pack# :: Unsigned n -> BitVector n
pack# (U i :: Integer
i) = Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV 0 Integer
i

{-# NOINLINE unpack# #-}
unpack# :: KnownNat n => BitVector n -> Unsigned n
unpack# :: BitVector n -> Unsigned n
unpack# (BV 0 i :: Integer
i) = Integer -> Unsigned n
forall (n :: Nat). Integer -> Unsigned n
U Integer
i
unpack# bv :: BitVector n
bv = String -> [BitVector n] -> Unsigned n
forall (n :: Nat) a.
(HasCallStack, KnownNat n) =>
String -> [BitVector n] -> a
undefError "Unsigned.unpack" [BitVector n
bv]

instance Eq (Unsigned n) where
  == :: Unsigned n -> Unsigned n -> Bool
(==) = Unsigned n -> Unsigned n -> Bool
forall (n :: Nat). Unsigned n -> Unsigned n -> Bool
eq#
  /= :: Unsigned n -> Unsigned n -> Bool
(/=) = Unsigned n -> Unsigned n -> Bool
forall (n :: Nat). Unsigned n -> Unsigned n -> Bool
neq#

{-# NOINLINE eq# #-}
eq# :: Unsigned n -> Unsigned n -> Bool
eq# :: Unsigned n -> Unsigned n -> Bool
eq# (U v1 :: Integer
v1) (U v2 :: Integer
v2) = Integer
v1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
v2

{-# NOINLINE neq# #-}
neq# :: Unsigned n -> Unsigned n -> Bool
neq# :: Unsigned n -> Unsigned n -> Bool
neq# (U v1 :: Integer
v1) (U v2 :: Integer
v2) = Integer
v1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
v2

instance Ord (Unsigned n) where
  < :: Unsigned n -> Unsigned n -> Bool
(<)  = Unsigned n -> Unsigned n -> Bool
forall (n :: Nat). Unsigned n -> Unsigned n -> Bool
lt#
  >= :: Unsigned n -> Unsigned n -> Bool
(>=) = Unsigned n -> Unsigned n -> Bool
forall (n :: Nat). Unsigned n -> Unsigned n -> Bool
ge#
  > :: Unsigned n -> Unsigned n -> Bool
(>)  = Unsigned n -> Unsigned n -> Bool
forall (n :: Nat). Unsigned n -> Unsigned n -> Bool
gt#
  <= :: Unsigned n -> Unsigned n -> Bool
(<=) = Unsigned n -> Unsigned n -> Bool
forall (n :: Nat). Unsigned n -> Unsigned n -> Bool
le#

lt#,ge#,gt#,le# :: Unsigned n -> Unsigned n -> Bool
{-# NOINLINE lt# #-}
lt# :: Unsigned n -> Unsigned n -> Bool
lt# (U n :: Integer
n) (U m :: Integer
m) = Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
m
{-# NOINLINE ge# #-}
ge# :: Unsigned n -> Unsigned n -> Bool
ge# (U n :: Integer
n) (U m :: Integer
m) = Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
m
{-# NOINLINE gt# #-}
gt# :: Unsigned n -> Unsigned n -> Bool
gt# (U n :: Integer
n) (U m :: Integer
m) = Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
m
{-# NOINLINE le# #-}
le# :: Unsigned n -> Unsigned n -> Bool
le# (U n :: Integer
n) (U m :: Integer
m) = Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
m

-- | The functions: 'enumFrom', 'enumFromThen', 'enumFromTo', and
-- 'enumFromThenTo', are not synthesizable.
instance KnownNat n => Enum (Unsigned n) where
  succ :: Unsigned n -> Unsigned n
succ           = (Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat).
KnownNat n =>
Unsigned n -> Unsigned n -> Unsigned n
+# Integer -> Unsigned n
forall (n :: Nat). KnownNat n => Integer -> Unsigned n
fromInteger# 1)
  pred :: Unsigned n -> Unsigned n
pred           = (Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat).
KnownNat n =>
Unsigned n -> Unsigned n -> Unsigned n
-# Integer -> Unsigned n
forall (n :: Nat). KnownNat n => Integer -> Unsigned n
fromInteger# 1)
  toEnum :: Int -> Unsigned n
toEnum         = Integer -> Unsigned n
forall (n :: Nat). KnownNat n => Integer -> Unsigned n
fromInteger# (Integer -> Unsigned n) -> (Int -> Integer) -> Int -> Unsigned n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger
  fromEnum :: Unsigned n -> Int
fromEnum       = Integer -> Int
forall a. Enum a => a -> Int
fromEnum (Integer -> Int) -> (Unsigned n -> Integer) -> Unsigned n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unsigned n -> Integer
forall (n :: Nat). Unsigned n -> Integer
toInteger#
  enumFrom :: Unsigned n -> [Unsigned n]
enumFrom       = Unsigned n -> [Unsigned n]
forall (n :: Nat). KnownNat n => Unsigned n -> [Unsigned n]
enumFrom#
  enumFromThen :: Unsigned n -> Unsigned n -> [Unsigned n]
enumFromThen   = Unsigned n -> Unsigned n -> [Unsigned n]
forall (n :: Nat).
KnownNat n =>
Unsigned n -> Unsigned n -> [Unsigned n]
enumFromThen#
  enumFromTo :: Unsigned n -> Unsigned n -> [Unsigned n]
enumFromTo     = Unsigned n -> Unsigned n -> [Unsigned n]
forall (n :: Nat). Unsigned n -> Unsigned n -> [Unsigned n]
enumFromTo#
  enumFromThenTo :: Unsigned n -> Unsigned n -> Unsigned n -> [Unsigned n]
enumFromThenTo = Unsigned n -> Unsigned n -> Unsigned n -> [Unsigned n]
forall (n :: Nat).
Unsigned n -> Unsigned n -> Unsigned n -> [Unsigned n]
enumFromThenTo#

{-# NOINLINE enumFrom# #-}
{-# NOINLINE enumFromThen# #-}
{-# NOINLINE enumFromTo# #-}
{-# NOINLINE enumFromThenTo# #-}
enumFrom#       :: KnownNat n => Unsigned n -> [Unsigned n]
enumFromThen#   :: KnownNat n => Unsigned n -> Unsigned n -> [Unsigned n]
enumFromTo#     :: Unsigned n -> Unsigned n -> [Unsigned n]
enumFromThenTo# :: Unsigned n -> Unsigned n -> Unsigned n -> [Unsigned n]
enumFrom# :: Unsigned n -> [Unsigned n]
enumFrom# x :: Unsigned n
x             = (Integer -> Unsigned n) -> [Integer] -> [Unsigned n]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> Unsigned n
forall (n :: Nat). KnownNat n => Integer -> Unsigned n
fromInteger_INLINE [Unsigned n -> Integer
forall (n :: Nat). Unsigned n -> Integer
unsafeToInteger Unsigned n
x ..]
enumFromThen# :: Unsigned n -> Unsigned n -> [Unsigned n]
enumFromThen# x :: Unsigned n
x y :: Unsigned n
y       = (Integer -> Unsigned n) -> [Integer] -> [Unsigned n]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> Unsigned n
forall (n :: Nat). KnownNat n => Integer -> Unsigned n
fromInteger_INLINE [Unsigned n -> Integer
forall (n :: Nat). Unsigned n -> Integer
unsafeToInteger Unsigned n
x, Unsigned n -> Integer
forall (n :: Nat). Unsigned n -> Integer
unsafeToInteger Unsigned n
y ..]
enumFromTo# :: Unsigned n -> Unsigned n -> [Unsigned n]
enumFromTo# x :: Unsigned n
x y :: Unsigned n
y         = (Integer -> Unsigned n) -> [Integer] -> [Unsigned n]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> Unsigned n
forall (n :: Nat). Integer -> Unsigned n
U [Unsigned n -> Integer
forall (n :: Nat). Unsigned n -> Integer
unsafeToInteger Unsigned n
x .. Unsigned n -> Integer
forall (n :: Nat). Unsigned n -> Integer
unsafeToInteger Unsigned n
y]
enumFromThenTo# :: Unsigned n -> Unsigned n -> Unsigned n -> [Unsigned n]
enumFromThenTo# x1 :: Unsigned n
x1 x2 :: Unsigned n
x2 y :: Unsigned n
y = (Integer -> Unsigned n) -> [Integer] -> [Unsigned n]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> Unsigned n
forall (n :: Nat). Integer -> Unsigned n
U [Unsigned n -> Integer
forall (n :: Nat). Unsigned n -> Integer
unsafeToInteger Unsigned n
x1, Unsigned n -> Integer
forall (n :: Nat). Unsigned n -> Integer
unsafeToInteger Unsigned n
x2 .. Unsigned n -> Integer
forall (n :: Nat). Unsigned n -> Integer
unsafeToInteger Unsigned n
y]

instance KnownNat n => Bounded (Unsigned n) where
  minBound :: Unsigned n
minBound = Unsigned n
forall (n :: Nat). Unsigned n
minBound#
  maxBound :: Unsigned n
maxBound = Unsigned n
forall (n :: Nat). KnownNat n => Unsigned n
maxBound#

{-# NOINLINE minBound# #-}
minBound# :: Unsigned n
minBound# :: Unsigned n
minBound# = Integer -> Unsigned n
forall (n :: Nat). Integer -> Unsigned n
U 0

{-# NOINLINE maxBound# #-}
maxBound# :: forall n .KnownNat n => Unsigned n
maxBound# :: Unsigned n
maxBound# = let m :: Integer
m = 1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
            in  Integer -> Unsigned n
forall (n :: Nat). Integer -> Unsigned n
U (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1)

instance KnownNat n => Num (Unsigned n) where
  + :: Unsigned n -> Unsigned n -> Unsigned n
(+)         = Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat).
KnownNat n =>
Unsigned n -> Unsigned n -> Unsigned n
(+#)
  (-)         = Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat).
KnownNat n =>
Unsigned n -> Unsigned n -> Unsigned n
(-#)
  * :: Unsigned n -> Unsigned n -> Unsigned n
(*)         = Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat).
KnownNat n =>
Unsigned n -> Unsigned n -> Unsigned n
(*#)
  negate :: Unsigned n -> Unsigned n
negate      = Unsigned n -> Unsigned n
forall (n :: Nat). KnownNat n => Unsigned n -> Unsigned n
negate#
  abs :: Unsigned n -> Unsigned n
abs         = Unsigned n -> Unsigned n
forall a. a -> a
id
  signum :: Unsigned n -> Unsigned n
signum bv :: Unsigned n
bv   = Unsigned 1 -> Unsigned n
forall (n :: Nat) (m :: Nat).
KnownNat m =>
Unsigned n -> Unsigned m
resize# (BitVector 1 -> Unsigned 1
forall (n :: Nat). KnownNat n => BitVector n -> Unsigned n
unpack# (Bit -> BitVector 1
BV.pack# (Unsigned n -> Bit
forall a. (BitPack a, KnownNat (BitSize a)) => a -> Bit
reduceOr Unsigned n
bv)))
  fromInteger :: Integer -> Unsigned n
fromInteger = Integer -> Unsigned n
forall (n :: Nat). KnownNat n => Integer -> Unsigned n
fromInteger#

(+#),(-#),(*#) :: forall n . KnownNat n => Unsigned n -> Unsigned n -> Unsigned n
{-# NOINLINE (+#) #-}
+# :: Unsigned n -> Unsigned n -> Unsigned n
(+#) (U i :: Integer
i) (U j :: Integer
j) = let m :: Integer
m = 1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
                       z :: Integer
z = Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j
                   in  if Integer
z Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
m then Integer -> Unsigned n
forall (n :: Nat). Integer -> Unsigned n
U (Integer
z Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
m) else Integer -> Unsigned n
forall (n :: Nat). Integer -> Unsigned n
U Integer
z

{-# NOINLINE (-#) #-}
-# :: Unsigned n -> Unsigned n -> Unsigned n
(-#) (U i :: Integer
i) (U j :: Integer
j) = let m :: Integer
m = 1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
                       z :: Integer
z = Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j
                   in  if Integer
z Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0 then Integer -> Unsigned n
forall (n :: Nat). Integer -> Unsigned n
U (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
z) else Integer -> Unsigned n
forall (n :: Nat). Integer -> Unsigned n
U Integer
z

{-# NOINLINE (*#) #-}
*# :: Unsigned n -> Unsigned n -> Unsigned n
(*#) (U i :: Integer
i) (U j :: Integer
j) = Integer -> Unsigned n
forall (n :: Nat). KnownNat n => Integer -> Unsigned n
fromInteger_INLINE (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
j)

{-# NOINLINE negate# #-}
negate# :: forall n . KnownNat n => Unsigned n -> Unsigned n
negate# :: Unsigned n -> Unsigned n
negate# (U 0) = Integer -> Unsigned n
forall (n :: Nat). Integer -> Unsigned n
U 0
negate# (U i :: Integer
i) = Integer
sz Integer -> Unsigned n -> Unsigned n
forall a b. a -> b -> b
`seq` Integer -> Unsigned n
forall (n :: Nat). Integer -> Unsigned n
U (Integer
sz Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
i)
  where
    sz :: Integer
sz = 1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))

{-# NOINLINE fromInteger# #-}
fromInteger# :: KnownNat n => Integer -> Unsigned n
fromInteger# :: Integer -> Unsigned n
fromInteger# = Integer -> Unsigned n
forall (n :: Nat). KnownNat n => Integer -> Unsigned n
fromInteger_INLINE

{-# INLINE fromInteger_INLINE #-}
fromInteger_INLINE :: forall n . KnownNat n => Integer -> Unsigned n
fromInteger_INLINE :: Integer -> Unsigned n
fromInteger_INLINE i :: Integer
i = Integer -> Unsigned n
forall (n :: Nat). Integer -> Unsigned n
U (Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
sz)
  where
    sz :: Integer
sz = 1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))

instance (KnownNat m, KnownNat n) => ExtendingNum (Unsigned m) (Unsigned n) where
  type AResult (Unsigned m) (Unsigned n) = Unsigned (Max m n + 1)
  add :: Unsigned m -> Unsigned n -> AResult (Unsigned m) (Unsigned n)
add  = Unsigned m -> Unsigned n -> AResult (Unsigned m) (Unsigned n)
forall (m :: Nat) (n :: Nat).
Unsigned m -> Unsigned n -> Unsigned (Max m n + 1)
plus#
  sub :: Unsigned m -> Unsigned n -> AResult (Unsigned m) (Unsigned n)
sub = Unsigned m -> Unsigned n -> AResult (Unsigned m) (Unsigned n)
forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
Unsigned m -> Unsigned n -> Unsigned (Max m n + 1)
minus#
  type MResult (Unsigned m) (Unsigned n) = Unsigned (m + n)
  mul :: Unsigned m -> Unsigned n -> MResult (Unsigned m) (Unsigned n)
mul = Unsigned m -> Unsigned n -> MResult (Unsigned m) (Unsigned n)
forall (m :: Nat) (n :: Nat).
Unsigned m -> Unsigned n -> Unsigned (m + n)
times#

{-# NOINLINE plus# #-}
plus# :: Unsigned m -> Unsigned n -> Unsigned (Max m n + 1)
plus# :: Unsigned m -> Unsigned n -> Unsigned (Max m n + 1)
plus# (U a :: Integer
a) (U b :: Integer
b) = Integer -> Unsigned (Max m n + 1)
forall (n :: Nat). Integer -> Unsigned n
U (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
b)

{-# NOINLINE minus# #-}
minus# :: forall m n . (KnownNat m, KnownNat n) => Unsigned m -> Unsigned n
                                                -> Unsigned (Max m n + 1)
minus# :: Unsigned m -> Unsigned n -> Unsigned (Max m n + 1)
minus# (U a :: Integer
a) (U b :: Integer
b) =
  let sz :: Int
sz   = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy (Max m n + 1) -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Max m n + 1)
forall k (t :: k). Proxy t
Proxy @(Max m n + 1)))
      mask :: Integer
mask = 1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
sz
      z :: Integer
z    = Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b
  in  if Integer
z Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0 then Integer -> Unsigned (Max m n + 1)
forall (n :: Nat). Integer -> Unsigned n
U (Integer
mask Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
z) else Integer -> Unsigned (Max m n + 1)
forall (n :: Nat). Integer -> Unsigned n
U Integer
z

{-# NOINLINE times# #-}
times# :: Unsigned m -> Unsigned n -> Unsigned (m + n)
times# :: Unsigned m -> Unsigned n -> Unsigned (m + n)
times# (U a :: Integer
a) (U b :: Integer
b) = Integer -> Unsigned (m + n)
forall (n :: Nat). Integer -> Unsigned n
U (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
b)

instance KnownNat n => Real (Unsigned n) where
  toRational :: Unsigned n -> Rational
toRational = Integer -> Rational
forall a. Real a => a -> Rational
toRational (Integer -> Rational)
-> (Unsigned n -> Integer) -> Unsigned n -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unsigned n -> Integer
forall (n :: Nat). Unsigned n -> Integer
toInteger#

instance KnownNat n => Integral (Unsigned n) where
  quot :: Unsigned n -> Unsigned n -> Unsigned n
quot        = Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat). Unsigned n -> Unsigned n -> Unsigned n
quot#
  rem :: Unsigned n -> Unsigned n -> Unsigned n
rem         = Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat). Unsigned n -> Unsigned n -> Unsigned n
rem#
  div :: Unsigned n -> Unsigned n -> Unsigned n
div         = Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat). Unsigned n -> Unsigned n -> Unsigned n
quot#
  mod :: Unsigned n -> Unsigned n -> Unsigned n
mod         = Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat). Unsigned n -> Unsigned n -> Unsigned n
rem#
  quotRem :: Unsigned n -> Unsigned n -> (Unsigned n, Unsigned n)
quotRem n :: Unsigned n
n d :: Unsigned n
d = (Unsigned n
n Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat). Unsigned n -> Unsigned n -> Unsigned n
`quot#` Unsigned n
d,Unsigned n
n Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat). Unsigned n -> Unsigned n -> Unsigned n
`rem#` Unsigned n
d)
  divMod :: Unsigned n -> Unsigned n -> (Unsigned n, Unsigned n)
divMod  n :: Unsigned n
n d :: Unsigned n
d = (Unsigned n
n Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat). Unsigned n -> Unsigned n -> Unsigned n
`quot#` Unsigned n
d,Unsigned n
n Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat). Unsigned n -> Unsigned n -> Unsigned n
`rem#` Unsigned n
d)
  toInteger :: Unsigned n -> Integer
toInteger   = Unsigned n -> Integer
forall (n :: Nat). Unsigned n -> Integer
toInteger#

quot#,rem# :: Unsigned n -> Unsigned n -> Unsigned n
{-# NOINLINE quot# #-}
quot# :: Unsigned n -> Unsigned n -> Unsigned n
quot# (U i :: Integer
i) (U j :: Integer
j) = Integer -> Unsigned n
forall (n :: Nat). Integer -> Unsigned n
U (Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
j)
{-# NOINLINE rem# #-}
rem# :: Unsigned n -> Unsigned n -> Unsigned n
rem# (U i :: Integer
i) (U j :: Integer
j) = Integer -> Unsigned n
forall (n :: Nat). Integer -> Unsigned n
U (Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` Integer
j)

{-# NOINLINE toInteger# #-}
toInteger# :: Unsigned n -> Integer
toInteger# :: Unsigned n -> Integer
toInteger# (U i :: Integer
i) = Integer
i

instance KnownNat n => Bits (Unsigned n) where
  .&. :: Unsigned n -> Unsigned n -> Unsigned n
(.&.)             = Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat). Unsigned n -> Unsigned n -> Unsigned n
and#
  .|. :: Unsigned n -> Unsigned n -> Unsigned n
(.|.)             = Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat). Unsigned n -> Unsigned n -> Unsigned n
or#
  xor :: Unsigned n -> Unsigned n -> Unsigned n
xor               = Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat). Unsigned n -> Unsigned n -> Unsigned n
xor#
  complement :: Unsigned n -> Unsigned n
complement        = Unsigned n -> Unsigned n
forall (n :: Nat). KnownNat n => Unsigned n -> Unsigned n
complement#
  zeroBits :: Unsigned n
zeroBits          = 0
  bit :: Int -> Unsigned n
bit i :: Int
i             = Int -> Bit -> Unsigned n -> Unsigned n
forall a i.
(BitPack a, KnownNat (BitSize a), Enum i) =>
i -> Bit -> a -> a
replaceBit Int
i Bit
high 0
  setBit :: Unsigned n -> Int -> Unsigned n
setBit v :: Unsigned n
v i :: Int
i        = Int -> Bit -> Unsigned n -> Unsigned n
forall a i.
(BitPack a, KnownNat (BitSize a), Enum i) =>
i -> Bit -> a -> a
replaceBit Int
i Bit
high Unsigned n
v
  clearBit :: Unsigned n -> Int -> Unsigned n
clearBit v :: Unsigned n
v i :: Int
i      = Int -> Bit -> Unsigned n -> Unsigned n
forall a i.
(BitPack a, KnownNat (BitSize a), Enum i) =>
i -> Bit -> a -> a
replaceBit Int
i Bit
low  Unsigned n
v
  complementBit :: Unsigned n -> Int -> Unsigned n
complementBit v :: Unsigned n
v i :: Int
i = Int -> Bit -> Unsigned n -> Unsigned n
forall a i.
(BitPack a, KnownNat (BitSize a), Enum i) =>
i -> Bit -> a -> a
replaceBit Int
i (Bit -> Bit
BV.complement## (Unsigned n
v Unsigned n -> Int -> Bit
forall a i.
(BitPack a, KnownNat (BitSize a), Enum i) =>
a -> i -> Bit
! Int
i)) Unsigned n
v
  testBit :: Unsigned n -> Int -> Bool
testBit v :: Unsigned n
v i :: Int
i       = Unsigned n
v Unsigned n -> Int -> Bit
forall a i.
(BitPack a, KnownNat (BitSize a), Enum i) =>
a -> i -> Bit
! Int
i Bit -> Bit -> Bool
forall a. Eq a => a -> a -> Bool
== Bit
high
  bitSizeMaybe :: Unsigned n -> Maybe Int
bitSizeMaybe v :: Unsigned n
v    = Int -> Maybe Int
forall a. a -> Maybe a
Just (Unsigned n -> Int
forall (n :: Nat). KnownNat n => Unsigned n -> Int
size# Unsigned n
v)
  bitSize :: Unsigned n -> Int
bitSize           = Unsigned n -> Int
forall (n :: Nat). KnownNat n => Unsigned n -> Int
size#
  isSigned :: Unsigned n -> Bool
isSigned _        = Bool
False
  shiftL :: Unsigned n -> Int -> Unsigned n
shiftL v :: Unsigned n
v i :: Int
i        = Unsigned n -> Int -> Unsigned n
forall (n :: Nat). KnownNat n => Unsigned n -> Int -> Unsigned n
shiftL# Unsigned n
v Int
i
  shiftR :: Unsigned n -> Int -> Unsigned n
shiftR v :: Unsigned n
v i :: Int
i        = Unsigned n -> Int -> Unsigned n
forall (n :: Nat). KnownNat n => Unsigned n -> Int -> Unsigned n
shiftR# Unsigned n
v Int
i
  rotateL :: Unsigned n -> Int -> Unsigned n
rotateL v :: Unsigned n
v i :: Int
i       = Unsigned n -> Int -> Unsigned n
forall (n :: Nat). KnownNat n => Unsigned n -> Int -> Unsigned n
rotateL# Unsigned n
v Int
i
  rotateR :: Unsigned n -> Int -> Unsigned n
rotateR v :: Unsigned n
v i :: Int
i       = Unsigned n -> Int -> Unsigned n
forall (n :: Nat). KnownNat n => Unsigned n -> Int -> Unsigned n
rotateR# Unsigned n
v Int
i
  popCount :: Unsigned n -> Int
popCount u :: Unsigned n
u        = BitVector n -> Int
forall a. Bits a => a -> Int
popCount (Unsigned n -> BitVector n
forall (n :: Nat). Unsigned n -> BitVector n
pack# Unsigned n
u)

{-# NOINLINE and# #-}
and# :: Unsigned n -> Unsigned n -> Unsigned n
and# :: Unsigned n -> Unsigned n -> Unsigned n
and# (U v1 :: Integer
v1) (U v2 :: Integer
v2) = Integer -> Unsigned n
forall (n :: Nat). Integer -> Unsigned n
U (Integer
v1 Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
v2)

{-# NOINLINE or# #-}
or# :: Unsigned n -> Unsigned n -> Unsigned n
or# :: Unsigned n -> Unsigned n -> Unsigned n
or# (U v1 :: Integer
v1) (U v2 :: Integer
v2) = Integer -> Unsigned n
forall (n :: Nat). Integer -> Unsigned n
U (Integer
v1 Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
v2)

{-# NOINLINE xor# #-}
xor# :: Unsigned n -> Unsigned n -> Unsigned n
xor# :: Unsigned n -> Unsigned n -> Unsigned n
xor# (U v1 :: Integer
v1) (U v2 :: Integer
v2) = Integer -> Unsigned n
forall (n :: Nat). Integer -> Unsigned n
U (Integer
v1 Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer
v2)

{-# NOINLINE complement# #-}
complement# :: KnownNat n => Unsigned n -> Unsigned n
complement# :: Unsigned n -> Unsigned n
complement# (U i :: Integer
i) = Integer -> Unsigned n
forall (n :: Nat). KnownNat n => Integer -> Unsigned n
fromInteger_INLINE (Integer -> Integer
forall a. Bits a => a -> a
complement Integer
i)

shiftL#, shiftR#, rotateL#, rotateR# :: KnownNat n => Unsigned n -> Int -> Unsigned n
{-# NOINLINE shiftL# #-}
shiftL# :: Unsigned n -> Int -> Unsigned n
shiftL# (U v :: Integer
v) i :: Int
i
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0     = String -> Unsigned n
forall a. HasCallStack => String -> a
error
              (String -> Unsigned n) -> String -> Unsigned n
forall a b. (a -> b) -> a -> b
$ "'shiftL undefined for negative number: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
  | Bool
otherwise = Integer -> Unsigned n
forall (n :: Nat). KnownNat n => Integer -> Unsigned n
fromInteger_INLINE (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
v Int
i)

{-# NOINLINE shiftR# #-}
-- shiftR# doesn't need the KnownNat constraint
-- But having the same type signature for all shift and rotate functions
-- makes implementing the Evaluator easier.
shiftR# :: Unsigned n -> Int -> Unsigned n
shiftR# (U v :: Integer
v) i :: Int
i
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0     = String -> Unsigned n
forall a. HasCallStack => String -> a
error
              (String -> Unsigned n) -> String -> Unsigned n
forall a b. (a -> b) -> a -> b
$ "'shiftR undefined for negative number: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
  | Bool
otherwise = Integer -> Unsigned n
forall (n :: Nat). Integer -> Unsigned n
U (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftR Integer
v Int
i)

{-# NOINLINE rotateL# #-}
rotateL# :: Unsigned n -> Int -> Unsigned n
rotateL# _ b :: Int
b | Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = String -> Unsigned n
forall a. HasCallStack => String -> a
error "'shiftL undefined for negative numbers"
rotateL# bv :: Unsigned n
bv@(U n :: Integer
n) b :: Int
b   = Integer -> Unsigned n
forall (n :: Nat). KnownNat n => Integer -> Unsigned n
fromInteger_INLINE (Integer
l Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
r)
  where
    l :: Integer
l    = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
n Int
b'
    r :: Integer
r    = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftR Integer
n Int
b''

    b' :: Int
b'   = Int
b Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
sz
    b'' :: Int
b''  = Int
sz Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
b'
    sz :: Int
sz   = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Unsigned n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Unsigned n
bv)

{-# NOINLINE rotateR# #-}
rotateR# :: Unsigned n -> Int -> Unsigned n
rotateR# _ b :: Int
b | Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = String -> Unsigned n
forall a. HasCallStack => String -> a
error "'shiftR undefined for negative numbers"
rotateR# bv :: Unsigned n
bv@(U n :: Integer
n) b :: Int
b   = Integer -> Unsigned n
forall (n :: Nat). KnownNat n => Integer -> Unsigned n
fromInteger_INLINE (Integer
l Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
r)
  where
    l :: Integer
l   = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftR Integer
n Int
b'
    r :: Integer
r   = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
n Int
b''

    b' :: Int
b'  = Int
b Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
sz
    b'' :: Int
b'' = Int
sz Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
b'
    sz :: Int
sz  = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Unsigned n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Unsigned n
bv)

instance KnownNat n => FiniteBits (Unsigned n) where
  finiteBitSize :: Unsigned n -> Int
finiteBitSize        = Unsigned n -> Int
forall (n :: Nat). KnownNat n => Unsigned n -> Int
size#
  countLeadingZeros :: Unsigned n -> Int
countLeadingZeros  u :: Unsigned n
u = BitVector n -> Int
forall b. FiniteBits b => b -> Int
countLeadingZeros  (Unsigned n -> BitVector n
forall (n :: Nat). Unsigned n -> BitVector n
pack# Unsigned n
u)
  countTrailingZeros :: Unsigned n -> Int
countTrailingZeros u :: Unsigned n
u = BitVector n -> Int
forall b. FiniteBits b => b -> Int
countTrailingZeros (Unsigned n -> BitVector n
forall (n :: Nat). Unsigned n -> BitVector n
pack# Unsigned n
u)

instance Resize Unsigned where
  resize :: Unsigned a -> Unsigned b
resize     = Unsigned a -> Unsigned b
forall (n :: Nat) (m :: Nat).
KnownNat m =>
Unsigned n -> Unsigned m
resize#
  zeroExtend :: Unsigned a -> Unsigned (b + a)
zeroExtend = Unsigned a -> Unsigned (b + a)
forall (f :: Nat -> *) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a, KnownNat b) =>
f a -> f (b + a)
extend
  truncateB :: Unsigned (a + b) -> Unsigned a
truncateB  = Unsigned (a + b) -> Unsigned a
forall (n :: Nat) (m :: Nat).
KnownNat m =>
Unsigned n -> Unsigned m
resize#

{-# NOINLINE resize# #-}
resize# :: forall n m . KnownNat m => Unsigned n -> Unsigned m
resize# :: Unsigned n -> Unsigned m
resize# (U i :: Integer
i) = let m :: Integer
m = 1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy m -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy m
forall k (t :: k). Proxy t
Proxy @m))
                in  if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
m then Integer -> Unsigned m
forall (n :: Nat). KnownNat n => Integer -> Unsigned n
fromInteger_INLINE Integer
i else Integer -> Unsigned m
forall (n :: Nat). Integer -> Unsigned n
U Integer
i

instance Default (Unsigned n) where
  def :: Unsigned n
def = Unsigned n
forall (n :: Nat). Unsigned n
minBound#

instance KnownNat n => Lift (Unsigned n) where
  lift :: Unsigned n -> Q Exp
lift u :: Unsigned n
u@(U i :: Integer
i) = Q Exp -> TypeQ -> Q Exp
sigE [| fromInteger# i |] (Integer -> TypeQ
decUnsigned (Unsigned n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Unsigned n
u))
  {-# NOINLINE lift #-}

decUnsigned :: Integer -> TypeQ
decUnsigned :: Integer -> TypeQ
decUnsigned n :: Integer
n = TypeQ -> TypeQ -> TypeQ
appT (Name -> TypeQ
conT ''Unsigned) (TyLitQ -> TypeQ
litT (TyLitQ -> TypeQ) -> TyLitQ -> TypeQ
forall a b. (a -> b) -> a -> b
$ Integer -> TyLitQ
numTyLit Integer
n)

instance KnownNat n => SaturatingNum (Unsigned n) where
  satAdd :: SaturationMode -> Unsigned n -> Unsigned n -> Unsigned n
satAdd SatWrap a :: Unsigned n
a b :: Unsigned n
b = Unsigned n
a Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat).
KnownNat n =>
Unsigned n -> Unsigned n -> Unsigned n
+# Unsigned n
b
  satAdd SatZero a :: Unsigned n
a b :: Unsigned n
b =
    let r :: Unsigned (Max n n + 1)
r = Unsigned n -> Unsigned n -> Unsigned (Max n n + 1)
forall (m :: Nat) (n :: Nat).
Unsigned m -> Unsigned n -> Unsigned (Max m n + 1)
plus# Unsigned n
a Unsigned n
b
    in  case Unsigned (n + 1) -> Bit
forall a. (BitPack a, KnownNat (BitSize a)) => a -> Bit
msb Unsigned (n + 1)
Unsigned (Max n n + 1)
r of
          0 -> Unsigned (n + 1) -> Unsigned n
forall (n :: Nat) (m :: Nat).
KnownNat m =>
Unsigned n -> Unsigned m
resize# Unsigned (n + 1)
Unsigned (Max n n + 1)
r
          _ -> Unsigned n
forall (n :: Nat). Unsigned n
minBound#
  satAdd _ a :: Unsigned n
a b :: Unsigned n
b =
    let r :: Unsigned (Max n n + 1)
r  = Unsigned n -> Unsigned n -> Unsigned (Max n n + 1)
forall (m :: Nat) (n :: Nat).
Unsigned m -> Unsigned n -> Unsigned (Max m n + 1)
plus# Unsigned n
a Unsigned n
b
    in  case Unsigned (n + 1) -> Bit
forall a. (BitPack a, KnownNat (BitSize a)) => a -> Bit
msb Unsigned (n + 1)
Unsigned (Max n n + 1)
r of
          0 -> Unsigned (n + 1) -> Unsigned n
forall (n :: Nat) (m :: Nat).
KnownNat m =>
Unsigned n -> Unsigned m
resize# Unsigned (n + 1)
Unsigned (Max n n + 1)
r
          _ -> Unsigned n
forall (n :: Nat). KnownNat n => Unsigned n
maxBound#

  satSub :: SaturationMode -> Unsigned n -> Unsigned n -> Unsigned n
satSub SatWrap a :: Unsigned n
a b :: Unsigned n
b = Unsigned n
a Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat).
KnownNat n =>
Unsigned n -> Unsigned n -> Unsigned n
-# Unsigned n
b
  satSub _ a :: Unsigned n
a b :: Unsigned n
b =
    let r :: Unsigned (Max n n + 1)
r = Unsigned n -> Unsigned n -> Unsigned (Max n n + 1)
forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
Unsigned m -> Unsigned n -> Unsigned (Max m n + 1)
minus# Unsigned n
a Unsigned n
b
    in  case Unsigned (n + 1) -> Bit
forall a. (BitPack a, KnownNat (BitSize a)) => a -> Bit
msb Unsigned (n + 1)
Unsigned (Max n n + 1)
r of
          0 -> Unsigned (n + 1) -> Unsigned n
forall (n :: Nat) (m :: Nat).
KnownNat m =>
Unsigned n -> Unsigned m
resize# Unsigned (n + 1)
Unsigned (Max n n + 1)
r
          _ -> Unsigned n
forall (n :: Nat). Unsigned n
minBound#

  satMul :: SaturationMode -> Unsigned n -> Unsigned n -> Unsigned n
satMul SatWrap a :: Unsigned n
a b :: Unsigned n
b = Unsigned n
a Unsigned n -> Unsigned n -> Unsigned n
forall (n :: Nat).
KnownNat n =>
Unsigned n -> Unsigned n -> Unsigned n
*# Unsigned n
b
  satMul SatZero a :: Unsigned n
a b :: Unsigned n
b =
    let r :: Unsigned (n + n)
r       = Unsigned n -> Unsigned n -> Unsigned (n + n)
forall (m :: Nat) (n :: Nat).
Unsigned m -> Unsigned n -> Unsigned (m + n)
times# Unsigned n
a Unsigned n
b
        (rL :: BitVector n
rL,rR :: BitVector n
rR) = Unsigned (n + n) -> (BitVector n, BitVector n)
forall a (m :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ (m + n), KnownNat n) =>
a -> (BitVector m, BitVector n)
split Unsigned (n + n)
r
    in  case BitVector n
rL of
          0 -> BitVector n -> Unsigned n
forall (n :: Nat). KnownNat n => BitVector n -> Unsigned n
unpack# BitVector n
rR
          _ -> Unsigned n
forall (n :: Nat). Unsigned n
minBound#
  satMul _ a :: Unsigned n
a b :: Unsigned n
b =
    let r :: Unsigned (n + n)
r       = Unsigned n -> Unsigned n -> Unsigned (n + n)
forall (m :: Nat) (n :: Nat).
Unsigned m -> Unsigned n -> Unsigned (m + n)
times# Unsigned n
a Unsigned n
b
        (rL :: BitVector n
rL,rR :: BitVector n
rR) = Unsigned (n + n) -> (BitVector n, BitVector n)
forall a (m :: Nat) (n :: Nat).
(BitPack a, BitSize a ~ (m + n), KnownNat n) =>
a -> (BitVector m, BitVector n)
split Unsigned (n + n)
r
    in  case BitVector n
rL of
          0 -> BitVector n -> Unsigned n
forall (n :: Nat). KnownNat n => BitVector n -> Unsigned n
unpack# BitVector n
rR
          _ -> Unsigned n
forall (n :: Nat). KnownNat n => Unsigned n
maxBound#

instance KnownNat n => Arbitrary (Unsigned n) where
  arbitrary :: Gen (Unsigned n)
arbitrary = Gen (Unsigned n)
forall a. (Bounded a, Integral a) => Gen a
arbitraryBoundedIntegral
  shrink :: Unsigned n -> [Unsigned n]
shrink    = Unsigned n -> [Unsigned n]
forall (n :: Nat) (p :: Nat -> *).
(KnownNat n, Integral (p n)) =>
p n -> [p n]
BV.shrinkSizedUnsigned

instance KnownNat n => CoArbitrary (Unsigned n) where
  coarbitrary :: Unsigned n -> Gen b -> Gen b
coarbitrary = Unsigned n -> Gen b -> Gen b
forall a b. Integral a => a -> Gen b -> Gen b
coarbitraryIntegral

type instance Index   (Unsigned n) = Int
type instance IxValue (Unsigned n) = Bit
instance KnownNat n => Ixed (Unsigned n) where
  ix :: Index (Unsigned n)
-> Traversal' (Unsigned n) (IxValue (Unsigned n))
ix i :: Index (Unsigned n)
i f :: IxValue (Unsigned n) -> f (IxValue (Unsigned n))
f s :: Unsigned n
s = BitVector n -> Unsigned n
forall (n :: Nat). KnownNat n => BitVector n -> Unsigned n
unpack# (BitVector n -> Unsigned n)
-> (Bit -> BitVector n) -> Bit -> Unsigned n
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BitVector n -> Int -> Bit -> BitVector n
forall (n :: Nat).
KnownNat n =>
BitVector n -> Int -> Bit -> BitVector n
BV.replaceBit# (Unsigned n -> BitVector n
forall (n :: Nat). Unsigned n -> BitVector n
pack# Unsigned n
s) Int
Index (Unsigned n)
i
                     (Bit -> Unsigned n) -> f Bit -> f (Unsigned n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IxValue (Unsigned n) -> f (IxValue (Unsigned n))
f (BitVector n -> Int -> Bit
forall (n :: Nat). KnownNat n => BitVector n -> Int -> Bit
BV.index# (Unsigned n -> BitVector n
forall (n :: Nat). Unsigned n -> BitVector n
pack# Unsigned n
s) Int
Index (Unsigned n)
i)