{-|
Copyright  :  (C) 2013-2016, University of Twente,
                  2016     , Myrtle Software Ltd,
                  2021-2022, QBayLogic B.V.
License    :  BSD2 (see the file LICENSE)
Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>
-}

{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE MultiWayIf #-}
{-# 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
  , toEnum#
  , fromEnum#
    -- ** 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
import GHC.Natural                    (naturalToInteger)
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.Annotations.Primitive (hasBlackBox)
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.Class.BitPack.BitIndex   ((!), msb, replaceBit, split)
import Clash.Class.BitPack.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)

{- $setup
>>> :m -Prelude
>>> import Clash.Prelude
-}

#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/exts/roles.html 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, 'unsafeToNatural', 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)

{-# ANN U hasBlackBox #-}

{-# NOINLINE size# #-}
{-# ANN size# hasBlackBox #-}
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# #-}
{-# ANN pack# hasBlackBox #-}
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# #-}
{-# ANN unpack# hasBlackBox #-}
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# #-}
{-# ANN eq# hasBlackBox #-}
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# #-}
{-# ANN neq# hasBlackBox #-}
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# #-}
{-# ANN lt# hasBlackBox #-}
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# #-}
{-# ANN ge# hasBlackBox #-}
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# #-}
{-# ANN gt# hasBlackBox #-}
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# #-}
{-# ANN le# hasBlackBox #-}
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         = Int -> Unsigned n
forall (n :: Nat). KnownNat n => Int -> Unsigned n
toEnum#
  fromEnum :: Unsigned n -> Int
fromEnum       = Unsigned n -> Int
forall (n :: Nat). KnownNat n => Unsigned n -> Int
fromEnum#
  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#

toEnum# :: forall n. KnownNat n => Int -> Unsigned n
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
{-# NOINLINE toEnum# #-}
{-# ANN toEnum# hasBlackBox #-}

fromEnum# :: forall n. KnownNat n => Unsigned n -> Int
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#
{-# NOINLINE fromEnum# #-}
{-# ANN fromEnum# hasBlackBox #-}

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# #-}
{-# ANN minBound# hasBlackBox #-}

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# #-}
{-# ANN maxBound# hasBlackBox #-}

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 (+#) #-}
{-# ANN (+#) hasBlackBox #-}
+# :: 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 (-#) #-}
{-# ANN (-#) hasBlackBox #-}
-# :: 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 (*#) #-}
{-# ANN (*#) hasBlackBox #-}
*# :: 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# #-}
{-# ANN negate# hasBlackBox #-}
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# #-}
{-# ANN fromInteger# hasBlackBox #-}
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# #-}
{-# ANN plus# hasBlackBox #-}
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# #-}
{-# ANN minus# hasBlackBox #-}
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# #-}
{-# ANN times# hasBlackBox #-}
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# #-}
{-# ANN quot# hasBlackBox #-}
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# #-}
{-# ANN rem# hasBlackBox #-}
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# #-}
{-# ANN toInteger# hasBlackBox #-}
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# #-}
{-# ANN and# hasBlackBox #-}
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# #-}
{-# ANN or# hasBlackBox #-}
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# #-}
{-# ANN xor# hasBlackBox #-}
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# #-}
{-# ANN complement# hasBlackBox #-}
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# #-}
{-# ANN shiftL# hasBlackBox #-}
shiftL# :: Unsigned n -> Int -> Unsigned n
shiftL# = \(U Natural
v) Int
i ->
#if MIN_VERSION_base(4,15,0)
  let i' = fromIntegral i in
  if | i < 0     -> error $ "'shiftL' undefined for negative number: " ++ show i
     | i' >= sz  -> U 0
     | otherwise -> U ((naturalShiftL v i') `mod` m)
 where
  sz = naturalToWord (natVal (Proxy @n))
  m  = 1 `naturalShiftL` sz
#else
  if | 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
"'shiftL' undefined for negative number: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
     | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
sz   -> Natural -> Unsigned n
forall (n :: Nat). Natural -> Unsigned n
U Natural
0
     | Bool
otherwise -> 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)
 where
  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))
  m :: Natural
m  = Natural
1 Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftL` Int
sz
#endif

{-# NOINLINE shiftR# #-}
{-# ANN shiftR# hasBlackBox #-}
-- 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# #-}
{-# ANN rotateL# hasBlackBox #-}
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 -> Unsigned n) -> String -> Unsigned n
forall a b. (a -> b) -> a -> b
$ String
"'rotateL' undefined for negative number: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  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# #-}
{-# ANN rotateR# hasBlackBox #-}
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 -> Unsigned n) -> String -> Unsigned n
forall a b. (a -> b) -> a -> b
$ String
"'rotateR' undefined for negative number: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
  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# #-}
{-# ANN resize# hasBlackBox #-}
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
SatError 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
_ -> String -> Unsigned n
forall a. HasCallStack => String -> a
errorX String
"Unsigned.satAdd: overflow"
  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
SatError 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
_ -> String -> Unsigned n
forall a. HasCallStack => String -> a
errorX String
"Unsigned.satSub: underflow"
  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
SatError 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
_ -> String -> Unsigned n
forall a. HasCallStack => String -> a
errorX String
"Unsigned.satMul: overflow"
  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#

  -- Implementations for satSucc and satPred are needed because 1 :: Unsigned 0
  -- overflows to 0, meaning without the first check SatError would return 0.

  satSucc :: SaturationMode -> Unsigned n -> Unsigned n
satSucc SaturationMode
SatError Unsigned n
a
    | Unsigned n
a 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
errorX String
"Unsigned.satSucc: overflow"
  satSucc SaturationMode
satMode Unsigned n
a = SaturationMode -> Unsigned n -> Unsigned n -> Unsigned n
forall a. SaturatingNum a => SaturationMode -> a -> a -> a
satAdd SaturationMode
satMode Unsigned n
a Unsigned n
1
  {-# INLINE satSucc #-}

  satPred :: SaturationMode -> Unsigned n -> Unsigned n
satPred SaturationMode
SatError Unsigned n
a
    | Unsigned n
a 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
errorX String
"Unsigned.satPred: underflow"
  satPred SaturationMode
satMode Unsigned n
a = SaturationMode -> Unsigned n -> Unsigned n -> Unsigned n
forall a. SaturatingNum a => SaturationMode -> a -> a -> a
satSub SaturationMode
satMode Unsigned n
a Unsigned n
1
  {-# INLINE satPred #-}

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 #-}
{-# ANN unsignedToWord hasBlackBox #-}

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 #-}
{-# ANN unsigned8toWord8 hasBlackBox #-}

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 #-}
{-# ANN unsigned16toWord16 hasBlackBox #-}

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 #-}
{-# ANN unsigned32toWord32 hasBlackBox #-}

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