{-|
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 CPP #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# 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#
    -- ** Conversions
  , unsignedToWord
  , unsigned8toWord8
  , unsigned16toWord16
  , unsigned32toWord32
  )
where

import Prelude hiding                 (even, odd)

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 Text.Printf                    (PrintfArg (..), printf)
import GHC.Exts                       (narrow8Word#, narrow16Word#, narrow32Word#)
import GHC.Generics                   (Generic)
#if MIN_VERSION_base(4,15,0)
import GHC.Num.BigNat                 (bigNatToWord, bigNatToWord#)
import GHC.Num.Integer
  (integerFromNatural, integerShiftL, integerToNatural)
import GHC.Num.Natural
  (Natural (..), naturalShiftL, naturalShiftR, naturalToWord)
#else
import GHC.Integer.GMP.Internals      (bigNatToWord)
import GHC.Natural                    (Natural (..), naturalFromInteger)
#endif
#if MIN_VERSION_base(4,12,0)
import GHC.Natural                    (naturalToInteger)
#endif
import GHC.TypeLits                   (KnownNat, Nat, type (+))
#if MIN_VERSION_base(4,15,0)
import GHC.TypeNats                   (natVal)
#else
import GHC.TypeLits                   (natVal)
#endif
import GHC.TypeLits.Extra             (Max)
import GHC.Word                       (Word (..), Word8 (..), Word16 (..), Word32 (..))
import Data.Ix                        (Ix(..))
import Language.Haskell.TH            (appT, conT, litT, numTyLit, sigE)
import Language.Haskell.TH.Syntax     (Lift(..))
#if MIN_VERSION_template_haskell(2,16,0)
import Language.Haskell.TH.Compat
#endif
#if MIN_VERSION_template_haskell(2,17,0)
import Language.Haskell.TH            (Quote, Type)
#else
import Language.Haskell.TH            (TypeQ)
#endif
import Test.QuickCheck.Arbitrary      (Arbitrary (..), CoArbitrary (..),
                                       arbitraryBoundedIntegral,
                                       coarbitraryIntegral)

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

#include "MachDeps.h"

type role Unsigned nominal

-- | 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
--
-- Unsigned has the <https://downloads.haskell.org/ghc/latest/docs/html/users_guide/glasgow_exts.html#roles type role>
--
-- >>> :i Unsigned
-- type role Unsigned nominal
-- ...
--
-- as it is not safe to coerce between different width Unsigned. To change the
-- width, use the functions in the 'Clash.Class.Resize.Resize' class.
#if MIN_VERSION_base(4,15,0)
data Unsigned (n :: Nat) =
    -- | The constructor, 'U', and the field, 'unsafeToInteger', are not
    -- synthesizable.
    U { unsafeToNatural :: !Natural }
#else
newtype Unsigned (n :: Nat) =
    -- | The constructor, 'U', and the field, 'unsafeToNatural', are not
    -- synthesizable.
    U { Unsigned n -> Natural
unsafeToNatural :: Natural }
#endif
  deriving (Typeable (Unsigned n)
DataType
Constr
Typeable (Unsigned n)
-> (forall (c :: Type -> Type).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Unsigned n -> c (Unsigned n))
-> (forall (c :: Type -> Type).
    (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 :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Unsigned n)))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    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 :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n))
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n))
-> (forall (m :: Type -> Type).
    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 :: Type -> Type).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    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 :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
    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 :: Type -> Type).
(KnownNat n, Monad m) =>
(forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n)
forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n)
forall (n :: Nat) (c :: Type -> Type).
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 :: Type -> Type).
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 :: Type -> Type) (c :: Type -> Type).
(KnownNat n, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Unsigned n))
forall (n :: Nat) (t :: Type -> Type -> Type) (c :: Type -> Type).
(KnownNat n, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Unsigned n))
forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n)
forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Unsigned n -> m (Unsigned n)
forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Unsigned n)
forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Unsigned n -> c (Unsigned n)
forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Unsigned n))
forall (t :: Type -> Type -> Type) (c :: Type -> Type).
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 :: Type -> Type).
(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 :: Type -> Type).
(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 :: Type -> Type).
(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 :: Type -> Type -> Type) (c :: Type -> Type).
(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 :: Type -> Type) (c :: Type -> Type).
(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 :: Type -> Type).
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 :: Type -> Type).
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
#if MIN_VERSION_base(4,15,0)
size# u = fromIntegral (natVal u)
#else
size# :: Unsigned n -> Int
size# Unsigned n
u = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Unsigned n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal Unsigned n
u)
#endif

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

instance Show (Unsigned n) where
  show :: Unsigned n -> String
show (U Natural
i) = Natural -> String
forall a. Show a => a -> String
show Natural
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 :: Type -> Type) 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 Natural
i) = Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
0 Natural
i

{-# NOINLINE unpack# #-}
unpack# :: KnownNat n => BitVector n -> Unsigned n
unpack# :: BitVector n -> Unsigned n
unpack# (BV Natural
0 Natural
i) = Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U Natural
i
unpack# BitVector n
bv = String -> [BitVector n] -> Unsigned n
forall (n :: Nat) a. KnownNat n => String -> [BitVector n] -> a
undefError String
"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 Natural
v1) (U Natural
v2) = Natural
v1 Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
v2

{-# NOINLINE neq# #-}
neq# :: Unsigned n -> Unsigned n -> Bool
neq# :: Unsigned n -> Unsigned n -> Bool
neq# (U Natural
v1) (U Natural
v2) = Natural
v1 Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
/= Natural
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 Natural
n) (U Natural
m) = Natural
n Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
m
{-# NOINLINE ge# #-}
ge# :: Unsigned n -> Unsigned n -> Bool
ge# (U Natural
n) (U Natural
m) = Natural
n Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= Natural
m
{-# NOINLINE gt# #-}
gt# :: Unsigned n -> Unsigned n -> Bool
gt# (U Natural
n) (U Natural
m) = Natural
n Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
m
{-# NOINLINE le# #-}
le# :: Unsigned n -> Unsigned n -> Bool
le# (U Natural
n) (U Natural
m) = Natural
n Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
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
n
    | Unsigned n
n Unsigned n -> Unsigned n -> Bool
forall a. Eq a => a -> a -> Bool
== Unsigned n
forall a. Bounded a => a
maxBound =
        String -> Unsigned n
forall a. HasCallStack => String -> a
error (String -> Unsigned n) -> String -> Unsigned n
forall a b. (a -> b) -> a -> b
$ String
"'succ' was called on (" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Unsigned n -> String
forall a. Show a => a -> String
show @(Unsigned n) Unsigned n
forall a. Bounded a => a
maxBound String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" :: "
             String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"Unsigned " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Natural -> String
forall a. Show a => a -> String
show (KnownNat n => Natural
forall (n :: Nat). KnownNat n => Natural
natToNatural @n) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
") and caused an "
             String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"overflow. Use 'satSucc' and specify a SaturationMode if you "
             String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"need other behavior."
    | Bool
otherwise = Unsigned n
n 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# Integer
1

  pred :: Unsigned n -> Unsigned n
pred Unsigned n
n
    | Unsigned n
n Unsigned n -> Unsigned n -> Bool
forall a. Eq a => a -> a -> Bool
== Unsigned n
forall a. Bounded a => a
minBound =
        String -> Unsigned n
forall a. HasCallStack => String -> a
error (String -> Unsigned n) -> String -> Unsigned n
forall a b. (a -> b) -> a -> b
$ String
"'pred' was called on (" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Unsigned n -> String
forall a. Show a => a -> String
show @(Unsigned n) Unsigned n
forall a. Bounded a => a
maxBound String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" :: "
             String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"Unsigned " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Natural -> String
forall a. Show a => a -> String
show (KnownNat n => Natural
forall (n :: Nat). KnownNat n => Natural
natToNatural @n) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
") and caused an "
             String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"underflow. Use 'satPred' and specify a SaturationMode if you "
             String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"need other behavior."
    | Bool
otherwise = Unsigned n
n 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# Integer
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).
KnownNat n =>
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).
KnownNat n =>
Unsigned n -> Unsigned n -> Unsigned n -> [Unsigned n]
enumFromThenTo#

enumFrom# :: forall n. KnownNat n => Unsigned n -> [Unsigned n]
enumFrom# :: Unsigned n -> [Unsigned n]
enumFrom# = \Unsigned n
x -> (Natural -> Unsigned n) -> [Natural] -> [Unsigned n]
forall a b. (a -> b) -> [a] -> [b]
map (Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U (Natural -> Unsigned n)
-> (Natural -> Natural) -> Natural -> Unsigned n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m)) [Unsigned n -> Natural
forall (n :: Nat). Unsigned n -> Natural
unsafeToNatural Unsigned n
x .. Unsigned n -> Natural
forall (n :: Nat). Unsigned n -> Natural
unsafeToNatural (Unsigned n
forall a. Bounded a => a
maxBound :: Unsigned n)]
#if MIN_VERSION_base(4,15,0)
  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
#else
  where m :: Natural
m = Natural
1 Natural -> Int -> Natural
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 -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
#endif
{-# NOINLINE enumFrom# #-}

enumFromThen# :: forall n. KnownNat n => Unsigned n -> Unsigned n -> [Unsigned n]
enumFromThen# :: Unsigned n -> Unsigned n -> [Unsigned n]
enumFromThen# = \Unsigned n
x Unsigned n
y -> [Natural] -> [Unsigned n]
toUnsigneds [Unsigned n -> Natural
forall (n :: Nat). Unsigned n -> Natural
unsafeToNatural Unsigned n
x, Unsigned n -> Natural
forall (n :: Nat). Unsigned n -> Natural
unsafeToNatural Unsigned n
y .. Unsigned n -> Unsigned n -> Natural
bound Unsigned n
x Unsigned n
y]
 where
  toUnsigneds :: [Natural] -> [Unsigned n]
toUnsigneds = (Natural -> Unsigned n) -> [Natural] -> [Unsigned n]
forall a b. (a -> b) -> [a] -> [b]
map (Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U (Natural -> Unsigned n)
-> (Natural -> Natural) -> Natural -> Unsigned n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m))
  bound :: Unsigned n -> Unsigned n -> Natural
bound Unsigned n
x Unsigned n
y = Unsigned n -> Natural
forall (n :: Nat). Unsigned n -> Natural
unsafeToNatural (if Unsigned n
x Unsigned n -> Unsigned n -> Bool
forall a. Ord a => a -> a -> Bool
<= Unsigned n
y then Unsigned n
forall a. Bounded a => a
maxBound else Unsigned n
forall a. Bounded a => a
minBound :: Unsigned n)
#if MIN_VERSION_base(4,15,0)
  m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
#else
  m :: Natural
m = Natural
1 Natural -> Int -> Natural
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 -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
#endif
{-# NOINLINE enumFromThen# #-}

enumFromTo# :: forall n. KnownNat n => Unsigned n -> Unsigned n -> [Unsigned n]
enumFromTo# :: Unsigned n -> Unsigned n -> [Unsigned n]
enumFromTo# = \Unsigned n
x Unsigned n
y -> (Natural -> Unsigned n) -> [Natural] -> [Unsigned n]
forall a b. (a -> b) -> [a] -> [b]
map (Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U (Natural -> Unsigned n)
-> (Natural -> Natural) -> Natural -> Unsigned n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m)) [Unsigned n -> Natural
forall (n :: Nat). Unsigned n -> Natural
unsafeToNatural Unsigned n
x .. Unsigned n -> Natural
forall (n :: Nat). Unsigned n -> Natural
unsafeToNatural Unsigned n
y]
#if MIN_VERSION_base(4,15,0)
  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
#else
  where m :: Natural
m = Natural
1 Natural -> Int -> Natural
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 -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
#endif
{-# NOINLINE enumFromTo# #-}

enumFromThenTo# :: forall n. KnownNat n => Unsigned n -> Unsigned n -> Unsigned n -> [Unsigned n]
enumFromThenTo# :: Unsigned n -> Unsigned n -> Unsigned n -> [Unsigned n]
enumFromThenTo# = \Unsigned n
x1 Unsigned n
x2 Unsigned n
y -> (Natural -> Unsigned n) -> [Natural] -> [Unsigned n]
forall a b. (a -> b) -> [a] -> [b]
map (Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U (Natural -> Unsigned n)
-> (Natural -> Natural) -> Natural -> Unsigned n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m)) [Unsigned n -> Natural
forall (n :: Nat). Unsigned n -> Natural
unsafeToNatural Unsigned n
x1, Unsigned n -> Natural
forall (n :: Nat). Unsigned n -> Natural
unsafeToNatural Unsigned n
x2 .. Unsigned n -> Natural
forall (n :: Nat). Unsigned n -> Natural
unsafeToNatural Unsigned n
y]
#if MIN_VERSION_base(4,15,0)
  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
#else
  where m :: Natural
m = Natural
1 Natural -> Int -> Natural
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 -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
#endif
{-# NOINLINE enumFromThenTo# #-}

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#

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

maxBound# :: forall n. KnownNat n => Unsigned n
maxBound# :: Unsigned n
maxBound# = let m :: Natural
m = Natural
1 Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftL` (forall a. (Num a, KnownNat n) => a
forall (n :: Nat) a. (Num a, KnownNat n) => a
natToNum @n) in  Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U (Natural
m Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)
{-# NOINLINE maxBound# #-}

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 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 => 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 Natural
i) (U Natural
j) -> Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U (Natural -> Natural -> Natural -> Natural
addMod Natural
m Natural
i Natural
j)
#if MIN_VERSION_base(4,15,0)
  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
#else
  where m :: Natural
m = Natural
1 Natural -> Int -> Natural
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 -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
#endif

{-# NOINLINE (-#) #-}
-# :: Unsigned n -> Unsigned n -> Unsigned n
(-#) = \(U Natural
i) (U Natural
j) -> Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U (Natural -> Natural -> Natural -> Natural
subMod Natural
m Natural
i Natural
j)
#if MIN_VERSION_base(4,15,0)
  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
#else
  where m :: Natural
m = Natural
1 Natural -> Int -> Natural
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 -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
#endif

{-# NOINLINE (*#) #-}
*# :: Unsigned n -> Unsigned n -> Unsigned n
(*#) = \(U Natural
i) (U Natural
j) -> Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U (Natural -> Natural -> Natural -> Natural
mulMod2 Natural
m Natural
i Natural
j)
#if MIN_VERSION_base(4,15,0)
  where m = (1 `naturalShiftL` naturalToWord (natVal (Proxy @n))) - 1
#else
  where m :: Natural
m = (Natural
1 Natural -> Int -> Natural
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 -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1
#endif

{-# NOINLINE negate# #-}
negate# :: forall n . KnownNat n => Unsigned n -> Unsigned n
negate# :: Unsigned n -> Unsigned n
negate# = \(U Natural
i) -> Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U (Natural -> Natural -> Natural
negateMod Natural
m Natural
i)
#if MIN_VERSION_base(4,15,0)
  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
#else
  where m :: Natural
m = Natural
1 Natural -> Int -> Natural
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 -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
#endif

{-# NOINLINE fromInteger# #-}
fromInteger# :: forall n . KnownNat n => Integer -> Unsigned n
#if MIN_VERSION_base(4,15,0)
fromInteger# = \x -> U (integerToNatural (x `mod` m))
 where
  m = 1 `integerShiftL` naturalToWord (natVal (Proxy @n))
#else
fromInteger# :: Integer -> Unsigned n
fromInteger# = \Integer
x -> Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U (Integer -> Natural
naturalFromInteger (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
m))
 where
  m :: Integer
m = Integer
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 -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
#endif

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 Natural
a) (U Natural
b) = Natural -> Unsigned (Max m n + 1)
forall (n :: Nat). Natural -> Unsigned n
U (Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
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 Natural
a) (U Natural
b) -> Natural -> Unsigned (Max m n + 1)
forall (n :: Nat). Natural -> Unsigned n
U (Natural -> Natural -> Natural -> Natural
subMod Natural
mask Natural
a Natural
b)
 where
#if MIN_VERSION_base(4,15,0)
  sz   = naturalToWord (natVal (Proxy @(Max m n + 1)))
  mask = 1 `naturalShiftL` sz
#else
  sz :: Int
sz   = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy (Max m n + 1) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Max m n + 1)
forall k (t :: k). Proxy t
Proxy @(Max m n + 1)))
  mask :: Natural
mask = Natural
1 Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftL` Int
sz
#endif

{-# NOINLINE times# #-}
times# :: Unsigned m -> Unsigned n -> Unsigned (m + n)
times# :: Unsigned m -> Unsigned n -> Unsigned (m + n)
times# (U Natural
a) (U Natural
b) = Natural -> Unsigned (m + n)
forall (n :: Nat). Natural -> Unsigned n
U (Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
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 Unsigned n
n 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  Unsigned n
n 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 Natural
i) (U Natural
j) = Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U (Natural
i Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`quot` Natural
j)
{-# NOINLINE rem# #-}
rem# :: Unsigned n -> Unsigned n -> Unsigned n
rem# (U Natural
i) (U Natural
j) = Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U (Natural
i Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`rem` Natural
j)

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

instance KnownNat n => PrintfArg (Unsigned n) where
  formatArg :: Unsigned n -> FieldFormatter
formatArg = Integer -> FieldFormatter
forall a. PrintfArg a => a -> FieldFormatter
formatArg (Integer -> FieldFormatter)
-> (Unsigned n -> Integer) -> Unsigned n -> FieldFormatter
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unsigned n -> Integer
forall a. Integral a => a -> Integer
toInteger

instance KnownNat n => Parity (Unsigned n) where
  even :: Unsigned n -> Bool
even = BitVector n -> Bool
forall a. Parity a => a -> Bool
even (BitVector n -> Bool)
-> (Unsigned n -> BitVector n) -> Unsigned n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unsigned n -> BitVector n
forall a. BitPack a => a -> BitVector (BitSize a)
pack
  odd :: Unsigned n -> Bool
odd = BitVector n -> Bool
forall a. Parity a => a -> Bool
odd (BitVector n -> Bool)
-> (Unsigned n -> BitVector n) -> Unsigned n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unsigned n -> BitVector n
forall a. BitPack a => a -> BitVector (BitSize a)
pack

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          = Unsigned n
0
  bit :: Int -> Unsigned n
bit Int
i             = Int -> Bit -> Unsigned n -> Unsigned n
forall a i. (BitPack a, Enum i) => i -> Bit -> a -> a
replaceBit Int
i Bit
high Unsigned n
0
  setBit :: Unsigned n -> Int -> Unsigned n
setBit Unsigned n
v Int
i        = Int -> Bit -> Unsigned n -> Unsigned n
forall a i. (BitPack a, Enum i) => i -> Bit -> a -> a
replaceBit Int
i Bit
high Unsigned n
v
  clearBit :: Unsigned n -> Int -> Unsigned n
clearBit Unsigned n
v Int
i      = Int -> Bit -> Unsigned n -> Unsigned n
forall a i. (BitPack a, Enum i) => i -> Bit -> a -> a
replaceBit Int
i Bit
low  Unsigned n
v
  complementBit :: Unsigned n -> Int -> Unsigned n
complementBit Unsigned n
v Int
i = Int -> Bit -> Unsigned n -> Unsigned n
forall a i. (BitPack 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, Enum i) => a -> i -> Bit
! Int
i)) Unsigned n
v
  testBit :: Unsigned n -> Int -> Bool
testBit Unsigned n
v Int
i       = Unsigned n
v Unsigned n -> Int -> Bit
forall a i. (BitPack 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 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 Unsigned n
_        = Bool
False
  shiftL :: Unsigned n -> Int -> Unsigned n
shiftL Unsigned n
v 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 Unsigned n
v 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 Unsigned n
v 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 Unsigned n
v 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 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 Natural
v1) (U Natural
v2) = Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U (Natural
v1 Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. Natural
v2)

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

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

{-# NOINLINE complement# #-}
complement# :: forall n . KnownNat n => Unsigned n -> Unsigned n
complement# :: Unsigned n -> Unsigned n
complement# = \(U Natural
i) -> Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U (Natural -> Natural
complementN Natural
i)
  where complementN :: Natural -> Natural
complementN = Integer -> Natural -> Natural
complementMod (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))

shiftL#, shiftR#, rotateL#, rotateR# :: forall n .KnownNat n => Unsigned n -> Int -> Unsigned n
{-# NOINLINE shiftL# #-}
shiftL# :: Unsigned n -> Int -> Unsigned n
shiftL# =
  \(U Natural
v) Int
i ->
    if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 then
#if MIN_VERSION_base
      U ((naturalShiftL v i) `mod` m)
#else
      Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U ((Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftL Natural
v Int
i) Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m)
#endif
    else
      String -> Unsigned n
forall a. HasCallStack => String -> a
error (String
"'shiftL undefined for negative number: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)
 where
#if MIN_VERSION_base(4,15,0)
  m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
#else
  m :: Natural
m = Natural
1 Natural -> Int -> Natural
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 -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
#endif

{-# 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 Natural
v) Int
i
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0     = String -> Unsigned n
forall a. HasCallStack => String -> a
error
              (String -> Unsigned n) -> String -> Unsigned n
forall a b. (a -> b) -> a -> b
$ String
"'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 = Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U (Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftR Natural
v Int
i)

{-# NOINLINE rotateL# #-}
rotateL# :: Unsigned n -> Int -> Unsigned n
rotateL# =
  \(U Natural
n) Int
b ->
    if Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 then
#if MIN_VERSION_base(4,15,0)
      let l   = naturalShiftL n b'
          r   = naturalShiftR n b''
          b'  = fromIntegral b `mod` sz
#else
      let l :: Natural
l   = Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftL Natural
n Int
b'
          r :: Natural
r   = Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftR Natural
n Int
b''
          b' :: Int
b'  = Int
b Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
sz
#endif
          b'' :: Int
b'' = Int
sz Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
b'
      in  Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U ((Natural
l Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|. Natural
r) Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m)
    else
      String -> Unsigned n
forall a. HasCallStack => String -> a
error String
"'rotateL undefined for negative numbers"
  where
#if MIN_VERSION_base(4,15,0)
    sz = naturalToWord (natVal (Proxy @n))
    m  = 1 `naturalShiftL` sz
#else
    sz :: Int
sz = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n)) :: Int
    m :: Natural
m  = Natural
1 Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftL` Int
sz
#endif

{-# NOINLINE rotateR# #-}
rotateR# :: Unsigned n -> Int -> Unsigned n
rotateR# =
  \(U Natural
n) Int
b ->
    if Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 then
#if MIN_VERSION_base(4,15,0)
      let l   = naturalShiftR n b'
          r   = naturalShiftL n b''
          b'  = fromIntegral b `mod` sz
#else
      let l :: Natural
l   = Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftR Natural
n Int
b'
          r :: Natural
r   = Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftL Natural
n Int
b''
          b' :: Int
b'  = Int
b Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
sz
#endif
          b'' :: Int
b'' = Int
sz Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
b'
      in  Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U ((Natural
l Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|. Natural
r) Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m)
    else
      String -> Unsigned n
forall a. HasCallStack => String -> a
error String
"'rotateR undefined for negative numbers"
  where
#if MIN_VERSION_base(4,15,0)
    sz = naturalToWord (natVal (Proxy @n))
    m  = 1 `naturalShiftL` sz
#else
    sz :: Int
sz = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n)) :: Int
    m :: Natural
m  = Natural
1 Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftL` Int
sz
#endif


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  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 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 -> Type) (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 Natural
i) -> if Natural
i Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= Natural
m then Natural -> Unsigned m
forall (n :: Nat). Natural -> Unsigned n
U (Natural
i Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m) else Natural -> Unsigned m
forall (n :: Nat). Natural -> Unsigned n
U Natural
i
#if MIN_VERSION_base(4,15,0)
  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @m))
#else
  where m :: Natural
m = Natural
1 Natural -> Int -> Natural
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 -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy m
forall k (t :: k). Proxy t
Proxy @m))
#endif

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 Natural
i) = Q Exp -> TypeQ -> Q Exp
sigE [| fromInteger# i |] (Integer -> TypeQ
decUnsigned (Unsigned n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal Unsigned n
u))
  {-# NOINLINE lift #-}
#if MIN_VERSION_template_haskell(2,16,0)
  liftTyped :: Unsigned n -> Q (TExp (Unsigned n))
liftTyped = Unsigned n -> Q (TExp (Unsigned n))
forall a. Lift a => a -> Q (TExp a)
liftTypedFromUntyped
#endif

#if MIN_VERSION_template_haskell(2,17,0)
decUnsigned :: Quote m => Natural -> m Type
decUnsigned n = appT (conT ''Unsigned) (litT $ numTyLit (integerFromNatural n))
#else
decUnsigned :: Integer -> TypeQ
decUnsigned :: Integer -> TypeQ
decUnsigned 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)
#endif

instance KnownNat n => SaturatingNum (Unsigned n) where
  satAdd :: SaturationMode -> Unsigned n -> Unsigned n -> Unsigned n
satAdd SaturationMode
SatWrap Unsigned n
a 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 SaturationMode
SatZero Unsigned n
a 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 => a -> Bit
msb Unsigned (n + 1)
Unsigned (Max n n + 1)
r of
          Bit
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
          Bit
_ -> Unsigned n
forall (n :: Nat). Unsigned n
minBound#
  satAdd SaturationMode
_ Unsigned n
a 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 => a -> Bit
msb Unsigned (n + 1)
Unsigned (Max n n + 1)
r of
          Bit
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
          Bit
_ -> Unsigned n
forall (n :: Nat). KnownNat n => Unsigned n
maxBound#

  satSub :: SaturationMode -> Unsigned n -> Unsigned n -> Unsigned n
satSub SaturationMode
SatWrap Unsigned n
a 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 SaturationMode
_ Unsigned n
a 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 => a -> Bit
msb Unsigned (n + 1)
Unsigned (Max n n + 1)
r of
          Bit
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
          Bit
_ -> Unsigned n
forall (n :: Nat). Unsigned n
minBound#

  satMul :: SaturationMode -> Unsigned n -> Unsigned n -> Unsigned n
satMul SaturationMode
SatWrap Unsigned n
a 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 SaturationMode
SatZero Unsigned n
a 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
        (BitVector n
rL,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
          BitVector n
0 -> BitVector n -> Unsigned n
forall (n :: Nat). KnownNat n => BitVector n -> Unsigned n
unpack# BitVector n
rR
          BitVector n
_ -> Unsigned n
forall (n :: Nat). Unsigned n
minBound#
  satMul SaturationMode
_ Unsigned n
a 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
        (BitVector n
rL,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
          BitVector n
0 -> BitVector n -> Unsigned n
forall (n :: Nat). KnownNat n => BitVector n -> Unsigned n
unpack# BitVector n
rR
          BitVector n
_ -> 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 -> Type).
(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 Index (Unsigned n)
i IxValue (Unsigned n) -> f (IxValue (Unsigned n))
f 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 :: Type -> Type) 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 :: Type -> Type) 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)

instance (KnownNat n) => Ix (Unsigned n) where
  range :: (Unsigned n, Unsigned n) -> [Unsigned n]
range (Unsigned n
a, Unsigned n
b) = [Unsigned n
a..Unsigned n
b]
  index :: (Unsigned n, Unsigned n) -> Unsigned n -> Int
index ab :: (Unsigned n, Unsigned n)
ab@(Unsigned n
a, Unsigned n
b) Unsigned n
x
    | (Unsigned n, Unsigned n) -> Unsigned n -> Bool
forall a. Ix a => (a, a) -> a -> Bool
inRange (Unsigned n, Unsigned n)
ab Unsigned n
x = Unsigned n -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Unsigned n -> Int) -> Unsigned n -> Int
forall a b. (a -> b) -> a -> b
$ Unsigned n
x Unsigned n -> Unsigned n -> Unsigned n
forall a. Num a => a -> a -> a
- Unsigned n
a
    | Bool
otherwise = String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ String -> Unsigned n -> Unsigned n -> Unsigned n -> String
forall r. PrintfType r => String -> r
printf String
"Index %d out of bounds (%d, %d) ab" Unsigned n
x Unsigned n
a Unsigned n
b
  inRange :: (Unsigned n, Unsigned n) -> Unsigned n -> Bool
inRange (Unsigned n
a, Unsigned n
b) Unsigned n
x = Unsigned n
a Unsigned n -> Unsigned n -> Bool
forall a. Ord a => a -> a -> Bool
<= Unsigned n
x Bool -> Bool -> Bool
&& Unsigned n
x Unsigned n -> Unsigned n -> Bool
forall a. Ord a => a -> a -> Bool
<= Unsigned n
b

unsignedToWord :: Unsigned WORD_SIZE_IN_BITS -> Word
#if MIN_VERSION_base(4,15,0)
unsignedToWord (U (NS u#)) = W# u#
unsignedToWord (U (NB u#)) = bigNatToWord u#
#else
unsignedToWord :: Unsigned 64 -> Word
unsignedToWord (U (NatS# GmpLimb#
u#)) = GmpLimb# -> Word
W# GmpLimb#
u#
unsignedToWord (U (NatJ# BigNat
u#)) = GmpLimb# -> Word
W# (BigNat -> GmpLimb#
bigNatToWord BigNat
u#)
#endif
{-# NOINLINE unsignedToWord #-}

unsigned8toWord8 :: Unsigned 8 -> Word8
#if MIN_VERSION_base(4,15,0)
unsigned8toWord8 (U (NS u#)) = W8# (narrow8Word# u#)
unsigned8toWord8 (U (NB u#)) = W8# (narrow8Word# (bigNatToWord# u#))
#else
unsigned8toWord8 :: Unsigned 8 -> Word8
unsigned8toWord8 (U (NatS# GmpLimb#
u#)) = GmpLimb# -> Word8
W8# (GmpLimb# -> GmpLimb#
narrow8Word# GmpLimb#
u#)
unsigned8toWord8 (U (NatJ# BigNat
u#)) = GmpLimb# -> Word8
W8# (GmpLimb# -> GmpLimb#
narrow8Word# (BigNat -> GmpLimb#
bigNatToWord BigNat
u#))
#endif
{-# NOINLINE unsigned8toWord8 #-}

unsigned16toWord16 :: Unsigned 16 -> Word16
#if MIN_VERSION_base(4,15,0)
unsigned16toWord16 (U (NS u#)) = W16# (narrow16Word# u#)
unsigned16toWord16 (U (NB u#)) = W16# (narrow16Word# (bigNatToWord# u#))
#else
unsigned16toWord16 :: Unsigned 16 -> Word16
unsigned16toWord16 (U (NatS# GmpLimb#
u#)) = GmpLimb# -> Word16
W16# (GmpLimb# -> GmpLimb#
narrow16Word# GmpLimb#
u#)
unsigned16toWord16 (U (NatJ# BigNat
u#)) = GmpLimb# -> Word16
W16# (GmpLimb# -> GmpLimb#
narrow16Word# (BigNat -> GmpLimb#
bigNatToWord BigNat
u#))
#endif
{-# NOINLINE unsigned16toWord16 #-}

unsigned32toWord32 :: Unsigned 32 -> Word32
#if MIN_VERSION_base(4,15,0)
unsigned32toWord32 (U (NS u#)) = W32# (narrow32Word# u#)
unsigned32toWord32 (U (NB u#)) = W32# (narrow32Word# (bigNatToWord# u#))
#else
unsigned32toWord32 :: Unsigned 32 -> Word32
unsigned32toWord32 (U (NatS# GmpLimb#
u#)) = GmpLimb# -> Word32
W32# (GmpLimb# -> GmpLimb#
narrow32Word# GmpLimb#
u#)
unsigned32toWord32 (U (NatJ# BigNat
u#)) = GmpLimb# -> Word32
W32# (GmpLimb# -> GmpLimb#
narrow32Word# (BigNat -> GmpLimb#
bigNatToWord BigNat
u#))
#endif
{-# NOINLINE unsigned32toWord32 #-}

{-# RULES
"bitCoerce/Unsigned WORD_SIZE_IN_BITS -> Word" bitCoerce = unsignedToWord
"bitCoerce/Unsigned 8 -> Word8" bitCoerce = unsigned8toWord8
"bitCoerce/Unsigned 16 -> Word16" bitCoerce = unsigned16toWord16
"bitCoerce/Unsigned 32 -> Word32" bitCoerce = unsigned32toWord32
 #-}