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

{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

{-# LANGUAGE Unsafe #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise       #-}

{-# OPTIONS_HADDOCK show-extensions not-home #-}

module Clash.Sized.Internal.Index
  ( -- * Datatypes
    Index (..)
    -- * Construction
  , fromSNat
  -- * 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
  , maxBound#
    -- ** Num
  , (+#)
  , (-#)
  , (*#)
  , fromInteger#
    -- ** ExtendingNum
  , plus#
  , minus#
  , times#
    -- ** Integral
  , quot#
  , rem#
  , toInteger#
    -- ** Resize
  , resize#
  )
where

import Prelude hiding             (even, odd)

import Control.DeepSeq            (NFData (..))
import Data.Bits                  (Bits (..), FiniteBits (..))
import Data.Data                  (Data)
import Data.Default.Class         (Default (..))
import Data.Proxy                 (Proxy (..))
import Text.Read                  (Read (..), ReadPrec)
import Language.Haskell.TH        (TypeQ, 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
import GHC.Generics               (Generic)
import GHC.Natural                (Natural, naturalFromInteger)
#if MIN_VERSION_base(4,12,0)
import GHC.Natural                (naturalToInteger)
#else
import Clash.Sized.Internal.Mod   (naturalToInteger)
#endif
import GHC.Stack                  (HasCallStack)
import GHC.TypeLits               (KnownNat, Nat, type (+), type (-),
                                   type (*), type (<=), natVal)
import GHC.TypeLits.Extra         (CLog)
import Test.QuickCheck.Arbitrary  (Arbitrary (..), CoArbitrary (..),
                                   arbitraryBoundedIntegral,
                                   coarbitraryIntegral, shrinkIntegral)

import Clash.Class.BitPack        (BitPack (..), packXWith)
import Clash.Class.Num            (ExtendingNum (..), SaturatingNum (..),
                                   SaturationMode (..))
import Clash.Class.Parity         (Parity (..))
import Clash.Class.Resize         (Resize (..))
import Clash.Prelude.BitIndex     (replaceBit)
import {-# SOURCE #-} Clash.Sized.Internal.BitVector (BitVector (BV), high, low, undefError)
import qualified Clash.Sized.Internal.BitVector as BV
import Clash.Promoted.Nat         (SNat(..), snatToNum, natToInteger, leToPlusKN)
import Clash.XException
  (ShowX (..), NFDataX (..), errorX, showsPrecXWith, rwhnfX)

{- $setup
>>> import Clash.Sized.Internal.Index
-}

-- | Arbitrary-bounded unsigned integer represented by @ceil(log_2(n))@ bits.
--
-- Given an upper bound @n@, an 'Index' @n@ number has a range of: [0 .. @n@-1]
--
-- >>> maxBound :: Index 8
-- 7
-- >>> minBound :: Index 8
-- 0
-- >>> read (show (maxBound :: Index 8)) :: Index 8
-- 7
-- >>> 1 + 2 :: Index 8
-- 3
-- >>> 2 + 6 :: Index 8
-- *** Exception: X: Clash.Sized.Index: result 8 is out of bounds: [0..7]
-- ...
-- >>> 1 - 3 :: Index 8
-- *** Exception: X: Clash.Sized.Index: result -2 is out of bounds: [0..7]
-- ...
-- >>> 2 * 3 :: Index 8
-- 6
-- >>> 2 * 4 :: Index 8
-- *** Exception: X: Clash.Sized.Index: result 8 is out of bounds: [0..7]
-- ...
newtype Index (n :: Nat) =
    -- | The constructor, 'I', and the field, 'unsafeToInteger', are not
    -- synthesizable.
    I { Index n -> Integer
unsafeToInteger :: Integer }
  deriving (Typeable (Index n)
DataType
Constr
Typeable (Index n)
-> (forall (c :: Type -> Type).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Index n -> c (Index n))
-> (forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Index n))
-> (Index n -> Constr)
-> (Index n -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Index n)))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Index n)))
-> ((forall b. Data b => b -> b) -> Index n -> Index n)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Index n -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Index n -> r)
-> (forall u. (forall d. Data d => d -> u) -> Index n -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Index n -> u)
-> (forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d) -> Index n -> m (Index n))
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Index n -> m (Index n))
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Index n -> m (Index n))
-> Data (Index n)
Index n -> DataType
Index n -> Constr
(forall b. Data b => b -> b) -> Index n -> Index n
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Index n -> c (Index n)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Index 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) -> Index n -> u
forall u. (forall d. Data d => d -> u) -> Index n -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Index n -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Index n -> r
forall (n :: Nat). KnownNat n => Typeable (Index n)
forall (n :: Nat). KnownNat n => Index n -> DataType
forall (n :: Nat). KnownNat n => Index n -> Constr
forall (n :: Nat).
KnownNat n =>
(forall b. Data b => b -> b) -> Index n -> Index n
forall (n :: Nat) u.
KnownNat n =>
Int -> (forall d. Data d => d -> u) -> Index n -> u
forall (n :: Nat) u.
KnownNat n =>
(forall d. Data d => d -> u) -> Index n -> [u]
forall (n :: Nat) r r'.
KnownNat n =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Index n -> r
forall (n :: Nat) r r'.
KnownNat n =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Index n -> r
forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, Monad m) =>
(forall d. Data d => d -> m d) -> Index n -> m (Index n)
forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Index n -> m (Index 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 (Index 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) -> Index n -> c (Index n)
forall (n :: Nat) (t :: Type -> Type) (c :: Type -> Type).
(KnownNat n, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Index 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 (Index n))
forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> Index n -> m (Index n)
forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Index n -> m (Index n)
forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Index n)
forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Index n -> c (Index n)
forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Index n))
forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Index n))
$cI :: Constr
$tIndex :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Index n -> m (Index n)
$cgmapMo :: forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Index n -> m (Index n)
gmapMp :: (forall d. Data d => d -> m d) -> Index n -> m (Index n)
$cgmapMp :: forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Index n -> m (Index n)
gmapM :: (forall d. Data d => d -> m d) -> Index n -> m (Index n)
$cgmapM :: forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, Monad m) =>
(forall d. Data d => d -> m d) -> Index n -> m (Index n)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Index n -> u
$cgmapQi :: forall (n :: Nat) u.
KnownNat n =>
Int -> (forall d. Data d => d -> u) -> Index n -> u
gmapQ :: (forall d. Data d => d -> u) -> Index n -> [u]
$cgmapQ :: forall (n :: Nat) u.
KnownNat n =>
(forall d. Data d => d -> u) -> Index n -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Index n -> r
$cgmapQr :: forall (n :: Nat) r r'.
KnownNat n =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Index n -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Index n -> r
$cgmapQl :: forall (n :: Nat) r r'.
KnownNat n =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Index n -> r
gmapT :: (forall b. Data b => b -> b) -> Index n -> Index n
$cgmapT :: forall (n :: Nat).
KnownNat n =>
(forall b. Data b => b -> b) -> Index n -> Index n
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Index 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 (Index n))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Index n))
$cdataCast1 :: forall (n :: Nat) (t :: Type -> Type) (c :: Type -> Type).
(KnownNat n, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Index n))
dataTypeOf :: Index n -> DataType
$cdataTypeOf :: forall (n :: Nat). KnownNat n => Index n -> DataType
toConstr :: Index n -> Constr
$ctoConstr :: forall (n :: Nat). KnownNat n => Index n -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Index 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 (Index n)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Index n -> c (Index 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) -> Index n -> c (Index n)
$cp1Data :: forall (n :: Nat). KnownNat n => Typeable (Index n)
Data, (forall x. Index n -> Rep (Index n) x)
-> (forall x. Rep (Index n) x -> Index n) -> Generic (Index n)
forall x. Rep (Index n) x -> Index n
forall x. Index n -> Rep (Index n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (n :: Nat) x. Rep (Index n) x -> Index n
forall (n :: Nat) x. Index n -> Rep (Index n) x
$cto :: forall (n :: Nat) x. Rep (Index n) x -> Index n
$cfrom :: forall (n :: Nat) x. Index n -> Rep (Index n) x
Generic)

{-# NOINLINE size# #-}
size# :: (KnownNat n, 1 <= n) => Index n -> Int
size# :: Index n -> Int
size# = BitVector (CLog 2 n) -> Int
forall (n :: Nat). KnownNat n => BitVector n -> Int
BV.size# (BitVector (CLog 2 n) -> Int)
-> (Index n -> BitVector (CLog 2 n)) -> Index n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack#

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

instance (KnownNat n, 1 <= n) => BitPack (Index n) where
  type BitSize (Index n) = CLog 2 n
  pack :: Index n -> BitVector (BitSize (Index n))
pack   = (Index n -> BitVector (CLog 2 n))
-> Index n -> BitVector (CLog 2 n)
forall (n :: Nat) a.
KnownNat n =>
(a -> BitVector n) -> a -> BitVector n
packXWith Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack#
  unpack :: BitVector (BitSize (Index n)) -> Index n
unpack = BitVector (BitSize (Index n)) -> Index n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
BitVector (CLog 2 n) -> Index n
unpack#

-- | Safely convert an `SNat` value to an `Index`
fromSNat :: (KnownNat m, n <= m + 1) => SNat n -> Index m
fromSNat :: SNat n -> Index m
fromSNat = SNat n -> Index m
forall a (n :: Nat). Num a => SNat n -> a
snatToNum

{-# NOINLINE pack# #-}
pack# :: Index n -> BitVector (CLog 2 n)
pack# :: Index n -> BitVector (CLog 2 n)
pack# (I Integer
i) = Natural -> Natural -> BitVector (CLog 2 n)
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
0 (Integer -> Natural
naturalFromInteger Integer
i)

{-# NOINLINE unpack# #-}
unpack# :: (KnownNat n, 1 <= n) => BitVector (CLog 2 n) -> Index n
unpack# :: BitVector (CLog 2 n) -> Index n
unpack# (BV Natural
0 Natural
i) = Integer -> Index n
forall (n :: Nat). (HasCallStack, KnownNat n) => Integer -> Index n
fromInteger_INLINE (Natural -> Integer
naturalToInteger Natural
i)
unpack# BitVector (CLog 2 n)
bv = String -> [BitVector (CLog 2 n)] -> Index n
forall (n :: Nat) a.
(HasCallStack, KnownNat n) =>
String -> [BitVector n] -> a
undefError String
"Index.unpack" [BitVector (CLog 2 n)
bv]

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

{-# NOINLINE eq# #-}
eq# :: (Index n) -> (Index n) -> Bool
(I Integer
n) eq# :: Index n -> Index n -> Bool
`eq#` (I Integer
m) = Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
m

{-# NOINLINE neq# #-}
neq# :: (Index n) -> (Index n) -> Bool
(I Integer
n) neq# :: Index n -> Index n -> Bool
`neq#` (I Integer
m) = Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
m

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

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

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

enumFrom# :: forall n. KnownNat n => Index n -> [Index n]
enumFrom# :: Index n -> [Index n]
enumFrom# Index n
x = [Index n
x .. Index n
forall a. Bounded a => a
maxBound]
{-# NOINLINE enumFrom# #-}

enumFromThen# :: forall n. KnownNat n => Index n -> Index n -> [Index n]
enumFromThen# :: Index n -> Index n -> [Index n]
enumFromThen# Index n
x Index n
y = if Index n
x Index n -> Index n -> Bool
forall a. Ord a => a -> a -> Bool
<= Index n
y then [Index n
x, Index n
y .. Index n
forall a. Bounded a => a
maxBound] else [Index n
x, Index n
y .. Index n
forall a. Bounded a => a
minBound]
{-# NOINLINE enumFromThen# #-}

enumFromTo# :: Index n -> Index n -> [Index n]
enumFromTo# :: Index n -> Index n -> [Index n]
enumFromTo# Index n
x Index n
y = (Integer -> Index n) -> [Integer] -> [Index n]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> Index n
forall (n :: Nat). Integer -> Index n
I [Index n -> Integer
forall (n :: Nat). Index n -> Integer
unsafeToInteger Index n
x .. Index n -> Integer
forall (n :: Nat). Index n -> Integer
unsafeToInteger Index n
y]
{-# NOINLINE enumFromTo# #-}

enumFromThenTo# :: Index n -> Index n -> Index n -> [Index n]
enumFromThenTo# :: Index n -> Index n -> Index n -> [Index n]
enumFromThenTo# Index n
x1 Index n
x2 Index n
y = (Integer -> Index n) -> [Integer] -> [Index n]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> Index n
forall (n :: Nat). Integer -> Index n
I [Index n -> Integer
forall (n :: Nat). Index n -> Integer
unsafeToInteger Index n
x1, Index n -> Integer
forall (n :: Nat). Index n -> Integer
unsafeToInteger Index n
x2 .. Index n -> Integer
forall (n :: Nat). Index n -> Integer
unsafeToInteger Index n
y]
{-# NOINLINE enumFromThenTo# #-}

instance KnownNat n => Bounded (Index n) where
  minBound :: Index n
minBound = Integer -> Index n
forall (n :: Nat). KnownNat n => Integer -> Index n
fromInteger# Integer
0
  maxBound :: Index n
maxBound = Index n
forall (n :: Nat). KnownNat n => Index n
maxBound#

maxBound# :: forall n. KnownNat n => Index n
maxBound# :: Index n
maxBound# =
  case KnownNat n => Integer
forall (n :: Nat). KnownNat n => Integer
natToInteger @n of
    Integer
0 -> String -> Index n
forall a. HasCallStack => String -> a
errorX String
"maxBound of 'Index 0' is undefined"
    Integer
n -> Integer -> Index n
forall (n :: Nat). (HasCallStack, KnownNat n) => Integer -> Index n
fromInteger_INLINE (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
{-# NOINLINE maxBound# #-}

-- | Operators report an error on overflow and underflow
instance KnownNat n => Num (Index n) where
  + :: Index n -> Index n -> Index n
(+)         = Index n -> Index n -> Index n
forall (n :: Nat). KnownNat n => Index n -> Index n -> Index n
(+#)
  (-)         = Index n -> Index n -> Index n
forall (n :: Nat). KnownNat n => Index n -> Index n -> Index n
(-#)
  * :: Index n -> Index n -> Index n
(*)         = Index n -> Index n -> Index n
forall (n :: Nat). KnownNat n => Index n -> Index n -> Index n
(*#)
  negate :: Index n -> Index n
negate      = (Index n
forall (n :: Nat). KnownNat n => Index n
maxBound# Index n -> Index n -> Index n
forall (n :: Nat). KnownNat n => Index n -> Index n -> Index n
-#)
  abs :: Index n -> Index n
abs         = Index n -> Index n
forall a. a -> a
id
  signum :: Index n -> Index n
signum Index n
i    = if Index n
i Index n -> Index n -> Bool
forall a. Eq a => a -> a -> Bool
== Index n
0 then Index n
0 else Index n
1
  fromInteger :: Integer -> Index n
fromInteger = Integer -> Index n
forall (n :: Nat). KnownNat n => Integer -> Index n
fromInteger#

(+#),(-#),(*#) :: KnownNat n => Index n -> Index n -> Index n
{-# NOINLINE (+#) #-}
+# :: Index n -> Index n -> Index n
(+#) (I Integer
a) (I Integer
b) = Integer -> Index n
forall (n :: Nat). (HasCallStack, KnownNat n) => Integer -> Index n
fromInteger_INLINE (Integer -> Index n) -> Integer -> Index n
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
b

{-# NOINLINE (-#) #-}
-# :: Index n -> Index n -> Index n
(-#) (I Integer
a) (I Integer
b) = Integer -> Index n
forall (n :: Nat). (HasCallStack, KnownNat n) => Integer -> Index n
fromInteger_INLINE (Integer -> Index n) -> Integer -> Index n
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b

{-# NOINLINE (*#) #-}
*# :: Index n -> Index n -> Index n
(*#) (I Integer
a) (I Integer
b) = Integer -> Index n
forall (n :: Nat). (HasCallStack, KnownNat n) => Integer -> Index n
fromInteger_INLINE (Integer -> Index n) -> Integer -> Index n
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
b

fromInteger# :: KnownNat n => Integer -> Index n
{-# NOINLINE fromInteger# #-}
fromInteger# :: Integer -> Index n
fromInteger# = Integer -> Index n
forall (n :: Nat). (HasCallStack, KnownNat n) => Integer -> Index n
fromInteger_INLINE
{-# INLINE fromInteger_INLINE #-}
fromInteger_INLINE :: forall n . (HasCallStack, KnownNat n) => Integer -> Index n
fromInteger_INLINE :: Integer -> Index n
fromInteger_INLINE Integer
i = Integer
bound Integer -> Index n -> Index n
`seq` if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> (-Integer
1) Bool -> Bool -> Bool
&& Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
bound then Integer -> Index n
forall (n :: Nat). Integer -> Index n
I Integer
i else Index n
err
  where
    bound :: Integer
bound = 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)
    err :: Index n
err   = String -> Index n
forall a. HasCallStack => String -> a
errorX (String
"Clash.Sized.Index: result " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i String -> String -> String
forall a. [a] -> [a] -> [a]
++
                   String
" is out of bounds: [0.." String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Integer
bound Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]")

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

plus#, minus# :: Index m -> Index n -> Index (m + n - 1)
{-# NOINLINE plus# #-}
plus# :: Index m -> Index n -> Index ((m + n) - 1)
plus# (I Integer
a) (I Integer
b) = Integer -> Index ((m + n) - 1)
forall (n :: Nat). Integer -> Index n
I (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
b)

{-# NOINLINE minus# #-}
minus# :: Index m -> Index n -> Index ((m + n) - 1)
minus# (I Integer
a) (I Integer
b) =
  let z :: Integer
z   = Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b
      err :: Index ((m + n) - 1)
err = String -> Index ((m + n) - 1)
forall a. HasCallStack => String -> a
error (String
"Clash.Sized.Index.minus: result " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
z String -> String -> String
forall a. [a] -> [a] -> [a]
++
                   String
" is smaller than 0")
      res :: Index ((m + n) - 1)
res = if Integer
z Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 then Index ((m + n) - 1)
err else Integer -> Index ((m + n) - 1)
forall (n :: Nat). Integer -> Index n
I Integer
z
  in  Index ((m + n) - 1)
res

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

instance (KnownNat n, 1 <= n) => SaturatingNum (Index n) where
  satAdd :: SaturationMode -> Index n -> Index n -> Index n
satAdd SaturationMode
SatWrap !Index n
a !Index n
b =
    case SNat n -> Integer
forall a (n :: Nat). Num a => SNat n -> a
snatToNum @Integer (KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat @n) of
      Integer
1 -> Integer -> Index n
forall (n :: Nat). KnownNat n => Integer -> Index n
fromInteger# Integer
0
      Integer
_ -> forall r.
(1 <= n, KnownNat 1, KnownNat n) =>
(forall (m :: Nat). (n ~ (1 + m), KnownNat m) => r) -> r
forall (k :: Nat) (n :: Nat) r.
(k <= n, KnownNat k, KnownNat n) =>
(forall (m :: Nat). (n ~ (k + m), KnownNat m) => r) -> r
leToPlusKN @1 @n ((forall (m :: Nat). (n ~ (1 + m), KnownNat m) => Index n)
 -> Index n)
-> (forall (m :: Nat). (n ~ (1 + m), KnownNat m) => Index n)
-> Index n
forall a b. (a -> b) -> a -> b
$
        case Index n -> Index n -> Index ((n + n) - 1)
forall (m :: Nat) (n :: Nat).
Index m -> Index n -> Index ((m + n) - 1)
plus# Index n
a Index n
b of
          Index ((n + n) - 1)
z | let m :: Index ((n + n) - 1)
m = Integer -> Index ((n + n) - 1)
forall (n :: Nat). KnownNat n => Integer -> Index n
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))
            , Index ((n + n) - 1)
z Index ((n + n) - 1) -> Index ((n + n) - 1) -> Bool
forall a. Ord a => a -> a -> Bool
>= Index ((n + n) - 1)
m -> Index ((n + n) - 1) -> Index n
forall (m :: Nat) (n :: Nat). KnownNat m => Index n -> Index m
resize# (Index ((n + n) - 1)
z Index ((n + n) - 1) -> Index ((n + n) - 1) -> Index ((n + n) - 1)
forall a. Num a => a -> a -> a
- Index ((n + n) - 1)
m)
          Index ((n + n) - 1)
z -> Index ((n + n) - 1) -> Index n
forall (m :: Nat) (n :: Nat). KnownNat m => Index n -> Index m
resize# Index ((n + n) - 1)
z
  satAdd SaturationMode
SatZero Index n
a Index n
b =
    forall r.
(1 <= n, KnownNat 1, KnownNat n) =>
(forall (m :: Nat). (n ~ (1 + m), KnownNat m) => r) -> r
forall (k :: Nat) (n :: Nat) r.
(k <= n, KnownNat k, KnownNat n) =>
(forall (m :: Nat). (n ~ (k + m), KnownNat m) => r) -> r
leToPlusKN @1 @n ((forall (m :: Nat). (n ~ (1 + m), KnownNat m) => Index n)
 -> Index n)
-> (forall (m :: Nat). (n ~ (1 + m), KnownNat m) => Index n)
-> Index n
forall a b. (a -> b) -> a -> b
$
      case Index n -> Index n -> Index ((n + n) - 1)
forall (m :: Nat) (n :: Nat).
Index m -> Index n -> Index ((m + n) - 1)
plus# Index n
a Index n
b of
        Index ((n + n) - 1)
z | let m :: Index ((n + n) - 1)
m = Integer -> Index ((n + n) - 1)
forall (n :: Nat). KnownNat n => Integer -> Index n
fromInteger# (Proxy (n - 1) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (n - 1)
forall k (t :: k). Proxy t
Proxy @ (n - 1)))
          , Index ((n + n) - 1)
z Index ((n + n) - 1) -> Index ((n + n) - 1) -> Bool
forall a. Ord a => a -> a -> Bool
> Index ((n + n) - 1)
m -> Integer -> Index n
forall (n :: Nat). KnownNat n => Integer -> Index n
fromInteger# Integer
0
        Index ((n + n) - 1)
z -> Index ((n + n) - 1) -> Index n
forall (m :: Nat) (n :: Nat). KnownNat m => Index n -> Index m
resize# Index ((n + n) - 1)
z
  satAdd SaturationMode
_ Index n
a Index n
b =
    forall r.
(1 <= n, KnownNat 1, KnownNat n) =>
(forall (m :: Nat). (n ~ (1 + m), KnownNat m) => r) -> r
forall (k :: Nat) (n :: Nat) r.
(k <= n, KnownNat k, KnownNat n) =>
(forall (m :: Nat). (n ~ (k + m), KnownNat m) => r) -> r
leToPlusKN @1 @n ((forall (m :: Nat). (n ~ (1 + m), KnownNat m) => Index n)
 -> Index n)
-> (forall (m :: Nat). (n ~ (1 + m), KnownNat m) => Index n)
-> Index n
forall a b. (a -> b) -> a -> b
$
      case Index n -> Index n -> Index ((n + n) - 1)
forall (m :: Nat) (n :: Nat).
Index m -> Index n -> Index ((m + n) - 1)
plus# Index n
a Index n
b of
        Index ((n + n) - 1)
z | let m :: Index ((n + n) - 1)
m = Integer -> Index ((n + n) - 1)
forall (n :: Nat). KnownNat n => Integer -> Index n
fromInteger# (Proxy (n - 1) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (n - 1)
forall k (t :: k). Proxy t
Proxy @ (n - 1)))
          , Index ((n + n) - 1)
z Index ((n + n) - 1) -> Index ((n + n) - 1) -> Bool
forall a. Ord a => a -> a -> Bool
> Index ((n + n) - 1)
m -> Index n
forall (n :: Nat). KnownNat n => Index n
maxBound#
        Index ((n + n) - 1)
z -> Index ((n + n) - 1) -> Index n
forall (m :: Nat) (n :: Nat). KnownNat m => Index n -> Index m
resize# Index ((n + n) - 1)
z

  satSub :: SaturationMode -> Index n -> Index n -> Index n
satSub SaturationMode
SatWrap Index n
a Index n
b =
    if Index n -> Index n -> Bool
forall (n :: Nat). Index n -> Index n -> Bool
lt# Index n
a Index n
b
       then Index n
forall a. Bounded a => a
maxBound Index n -> Index n -> Index n
forall (n :: Nat). KnownNat n => Index n -> Index n -> Index n
-# (Index n
b Index n -> Index n -> Index n
forall (n :: Nat). KnownNat n => Index n -> Index n -> Index n
-# Index n
a) Index n -> Index n -> Index n
forall (n :: Nat). KnownNat n => Index n -> Index n -> Index n
+# Index n
1
       else Index n
a Index n -> Index n -> Index n
forall (n :: Nat). KnownNat n => Index n -> Index n -> Index n
-# Index n
b

  satSub SaturationMode
_ Index n
a Index n
b =
    if Index n -> Index n -> Bool
forall (n :: Nat). Index n -> Index n -> Bool
lt# Index n
a Index n
b
       then Integer -> Index n
forall (n :: Nat). KnownNat n => Integer -> Index n
fromInteger# Integer
0
       else Index n
a Index n -> Index n -> Index n
forall (n :: Nat). KnownNat n => Index n -> Index n -> Index n
-# Index n
b

  satMul :: SaturationMode -> Index n -> Index n -> Index n
satMul SaturationMode
SatWrap !Index n
a !Index n
b =
    case SNat n -> Integer
forall a (n :: Nat). Num a => SNat n -> a
snatToNum @Integer (KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat @n) of
      Integer
1 -> Integer -> Index n
forall (n :: Nat). KnownNat n => Integer -> Index n
fromInteger# Integer
0
      Integer
_ -> forall r.
(1 <= n, KnownNat 1, KnownNat n) =>
(forall (m :: Nat). (n ~ (1 + m), KnownNat m) => r) -> r
forall (k :: Nat) (n :: Nat) r.
(k <= n, KnownNat k, KnownNat n) =>
(forall (m :: Nat). (n ~ (k + m), KnownNat m) => r) -> r
leToPlusKN @1 @n ((forall (m :: Nat). (n ~ (1 + m), KnownNat m) => Index n)
 -> Index n)
-> (forall (m :: Nat). (n ~ (1 + m), KnownNat m) => Index n)
-> Index n
forall a b. (a -> b) -> a -> b
$
        case Index n -> Index n -> Index (((n - 1) * (n - 1)) + 1)
forall (m :: Nat) (n :: Nat).
Index m -> Index n -> Index (((m - 1) * (n - 1)) + 1)
times# Index n
a Index n
b of
          Index (((n - 1) * (n - 1)) + 1)
z -> let m :: Index (((n - 1) * (n - 1)) + 1)
m = Integer -> Index (((n - 1) * (n - 1)) + 1)
forall (n :: Nat). KnownNat n => Integer -> Index n
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))
               in Index (((n - 1) * (n - 1)) + 1) -> Index n
forall (m :: Nat) (n :: Nat). KnownNat m => Index n -> Index m
resize# (Index (((n - 1) * (n - 1)) + 1)
z Index (((n - 1) * (n - 1)) + 1)
-> Index (((n - 1) * (n - 1)) + 1)
-> Index (((n - 1) * (n - 1)) + 1)
forall a. Integral a => a -> a -> a
`mod` Index (((n - 1) * (n - 1)) + 1)
m)
  satMul SaturationMode
SatZero Index n
a Index n
b =
    forall r.
(1 <= n, KnownNat 1, KnownNat n) =>
(forall (m :: Nat). (n ~ (1 + m), KnownNat m) => r) -> r
forall (k :: Nat) (n :: Nat) r.
(k <= n, KnownNat k, KnownNat n) =>
(forall (m :: Nat). (n ~ (k + m), KnownNat m) => r) -> r
leToPlusKN @1 @n ((forall (m :: Nat). (n ~ (1 + m), KnownNat m) => Index n)
 -> Index n)
-> (forall (m :: Nat). (n ~ (1 + m), KnownNat m) => Index n)
-> Index n
forall a b. (a -> b) -> a -> b
$
      case Index n -> Index n -> Index (((n - 1) * (n - 1)) + 1)
forall (m :: Nat) (n :: Nat).
Index m -> Index n -> Index (((m - 1) * (n - 1)) + 1)
times# Index n
a Index n
b of
        Index (((n - 1) * (n - 1)) + 1)
z | let m :: Index (((n - 1) * (n - 1)) + 1)
m = Integer -> Index (((n - 1) * (n - 1)) + 1)
forall (n :: Nat). KnownNat n => Integer -> Index n
fromInteger# (Proxy (n - 1) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (n - 1)
forall k (t :: k). Proxy t
Proxy @ (n - 1)))
          , Index (((n - 1) * (n - 1)) + 1)
z Index (((n - 1) * (n - 1)) + 1)
-> Index (((n - 1) * (n - 1)) + 1) -> Bool
forall a. Ord a => a -> a -> Bool
> Index (((n - 1) * (n - 1)) + 1)
m -> Integer -> Index n
forall (n :: Nat). KnownNat n => Integer -> Index n
fromInteger# Integer
0
        Index (((n - 1) * (n - 1)) + 1)
z -> Index (((n - 1) * (n - 1)) + 1) -> Index n
forall (m :: Nat) (n :: Nat). KnownNat m => Index n -> Index m
resize# Index (((n - 1) * (n - 1)) + 1)
z
  satMul SaturationMode
_ Index n
a Index n
b =
    forall r.
(1 <= n, KnownNat 1, KnownNat n) =>
(forall (m :: Nat). (n ~ (1 + m), KnownNat m) => r) -> r
forall (k :: Nat) (n :: Nat) r.
(k <= n, KnownNat k, KnownNat n) =>
(forall (m :: Nat). (n ~ (k + m), KnownNat m) => r) -> r
leToPlusKN @1 @n ((forall (m :: Nat). (n ~ (1 + m), KnownNat m) => Index n)
 -> Index n)
-> (forall (m :: Nat). (n ~ (1 + m), KnownNat m) => Index n)
-> Index n
forall a b. (a -> b) -> a -> b
$
      case Index n -> Index n -> Index (((n - 1) * (n - 1)) + 1)
forall (m :: Nat) (n :: Nat).
Index m -> Index n -> Index (((m - 1) * (n - 1)) + 1)
times# Index n
a Index n
b of
        Index (((n - 1) * (n - 1)) + 1)
z | let m :: Index (((n - 1) * (n - 1)) + 1)
m = Integer -> Index (((n - 1) * (n - 1)) + 1)
forall (n :: Nat). KnownNat n => Integer -> Index n
fromInteger# (Proxy (n - 1) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (n - 1)
forall k (t :: k). Proxy t
Proxy @ (n - 1)))
          , Index (((n - 1) * (n - 1)) + 1)
z Index (((n - 1) * (n - 1)) + 1)
-> Index (((n - 1) * (n - 1)) + 1) -> Bool
forall a. Ord a => a -> a -> Bool
> Index (((n - 1) * (n - 1)) + 1)
m -> Index n
forall (n :: Nat). KnownNat n => Index n
maxBound#
        Index (((n - 1) * (n - 1)) + 1)
z -> Index (((n - 1) * (n - 1)) + 1) -> Index n
forall (m :: Nat) (n :: Nat). KnownNat m => Index n -> Index m
resize# Index (((n - 1) * (n - 1)) + 1)
z

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

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

quot#,rem# :: Index n -> Index n -> Index n
{-# NOINLINE quot# #-}
(I Integer
a) quot# :: Index n -> Index n -> Index n
`quot#` (I Integer
b) = Integer -> Index n
forall (n :: Nat). Integer -> Index n
I (Integer
a Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
b)
{-# NOINLINE rem# #-}
(I Integer
a) rem# :: Index n -> Index n -> Index n
`rem#` (I Integer
b) = Integer -> Index n
forall (n :: Nat). Integer -> Index n
I (Integer
a Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` Integer
b)

{-# NOINLINE toInteger# #-}
toInteger# :: Index n -> Integer
toInteger# :: Index n -> Integer
toInteger# (I Integer
n) = Integer
n

instance (KnownNat n, 1 <= n) => Parity (Index n) where
  even :: Index n -> Bool
even = BitVector (CLog 2 n) -> Bool
forall a. Parity a => a -> Bool
even (BitVector (CLog 2 n) -> Bool)
-> (Index n -> BitVector (CLog 2 n)) -> Index n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n -> BitVector (CLog 2 n)
forall a. BitPack a => a -> BitVector (BitSize a)
pack
  odd :: Index n -> Bool
odd = BitVector (CLog 2 n) -> Bool
forall a. Parity a => a -> Bool
odd (BitVector (CLog 2 n) -> Bool)
-> (Index n -> BitVector (CLog 2 n)) -> Index n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n -> BitVector (CLog 2 n)
forall a. BitPack a => a -> BitVector (BitSize a)
pack

instance (KnownNat n, 1 <= n) => Bits (Index n) where
  Index n
a .&. :: Index n -> Index n -> Index n
.&. Index n
b           = BitVector (CLog 2 n) -> Index n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
BitVector (CLog 2 n) -> Index n
unpack# (BitVector (CLog 2 n) -> Index n)
-> BitVector (CLog 2 n) -> Index n
forall a b. (a -> b) -> a -> b
$ BitVector (CLog 2 n)
-> BitVector (CLog 2 n) -> BitVector (CLog 2 n)
forall (n :: Nat).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
BV.and# (Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack# Index n
a) (Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack# Index n
b)
  Index n
a .|. :: Index n -> Index n -> Index n
.|. Index n
b           = BitVector (CLog 2 n) -> Index n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
BitVector (CLog 2 n) -> Index n
unpack# (BitVector (CLog 2 n) -> Index n)
-> BitVector (CLog 2 n) -> Index n
forall a b. (a -> b) -> a -> b
$ BitVector (CLog 2 n)
-> BitVector (CLog 2 n) -> BitVector (CLog 2 n)
forall (n :: Nat).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
BV.or# (Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack# Index n
a) (Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack# Index n
b)
  xor :: Index n -> Index n -> Index n
xor Index n
a Index n
b           = BitVector (CLog 2 n) -> Index n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
BitVector (CLog 2 n) -> Index n
unpack# (BitVector (CLog 2 n) -> Index n)
-> BitVector (CLog 2 n) -> Index n
forall a b. (a -> b) -> a -> b
$ BitVector (CLog 2 n)
-> BitVector (CLog 2 n) -> BitVector (CLog 2 n)
forall (n :: Nat).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
BV.xor# (Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack# Index n
a) (Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack# Index n
b)
  complement :: Index n -> Index n
complement        = BitVector (CLog 2 n) -> Index n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
BitVector (CLog 2 n) -> Index n
unpack# (BitVector (CLog 2 n) -> Index n)
-> (Index n -> BitVector (CLog 2 n)) -> Index n -> Index n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector (CLog 2 n) -> BitVector (CLog 2 n)
forall (n :: Nat). KnownNat n => BitVector n -> BitVector n
BV.complement# (BitVector (CLog 2 n) -> BitVector (CLog 2 n))
-> (Index n -> BitVector (CLog 2 n))
-> Index n
-> BitVector (CLog 2 n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack#
  zeroBits :: Index n
zeroBits          = BitVector (CLog 2 n) -> Index n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
BitVector (CLog 2 n) -> Index n
unpack# BitVector (CLog 2 n)
forall a. Bits a => a
zeroBits
  bit :: Int -> Index n
bit Int
i             = BitVector (CLog 2 n) -> Index n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
BitVector (CLog 2 n) -> Index n
unpack# (BitVector (CLog 2 n) -> Index n)
-> BitVector (CLog 2 n) -> Index n
forall a b. (a -> b) -> a -> b
$ Int -> BitVector (CLog 2 n)
forall a. Bits a => Int -> a
bit Int
i
  setBit :: Index n -> Int -> Index n
setBit Index n
v Int
i        = BitVector (CLog 2 n) -> Index n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
BitVector (CLog 2 n) -> Index n
unpack# (BitVector (CLog 2 n) -> Index n)
-> BitVector (CLog 2 n) -> Index n
forall a b. (a -> b) -> a -> b
$ Int -> Bit -> BitVector (CLog 2 n) -> BitVector (CLog 2 n)
forall a i. (BitPack a, Enum i) => i -> Bit -> a -> a
replaceBit Int
i Bit
high (Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack# Index n
v)
  clearBit :: Index n -> Int -> Index n
clearBit Index n
v Int
i      = BitVector (CLog 2 n) -> Index n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
BitVector (CLog 2 n) -> Index n
unpack# (BitVector (CLog 2 n) -> Index n)
-> BitVector (CLog 2 n) -> Index n
forall a b. (a -> b) -> a -> b
$ Int -> Bit -> BitVector (CLog 2 n) -> BitVector (CLog 2 n)
forall a i. (BitPack a, Enum i) => i -> Bit -> a -> a
replaceBit Int
i Bit
low  (Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack# Index n
v)
  complementBit :: Index n -> Int -> Index n
complementBit Index n
v Int
i = BitVector (CLog 2 n) -> Index n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
BitVector (CLog 2 n) -> Index n
unpack# (BitVector (CLog 2 n) -> Index n)
-> BitVector (CLog 2 n) -> Index n
forall a b. (a -> b) -> a -> b
$ BitVector (CLog 2 n) -> Int -> BitVector (CLog 2 n)
forall a. Bits a => a -> Int -> a
complementBit (Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack# Index n
v) Int
i
  testBit :: Index n -> Int -> Bool
testBit Index n
v Int
i       = BitVector (CLog 2 n) -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit (Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack# Index n
v) Int
i
  bitSizeMaybe :: Index n -> Maybe Int
bitSizeMaybe Index n
v    = Int -> Maybe Int
forall a. a -> Maybe a
Just (Index n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => Index n -> Int
size# Index n
v)
  bitSize :: Index n -> Int
bitSize           = Index n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => Index n -> Int
size#
  isSigned :: Index n -> Bool
isSigned Index n
_        = Bool
False
  shiftL :: Index n -> Int -> Index n
shiftL Index n
v Int
i        = BitVector (CLog 2 n) -> Index n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
BitVector (CLog 2 n) -> Index n
unpack# (BitVector (CLog 2 n) -> Index n)
-> BitVector (CLog 2 n) -> Index n
forall a b. (a -> b) -> a -> b
$ BitVector (CLog 2 n) -> Int -> BitVector (CLog 2 n)
forall a. Bits a => a -> Int -> a
shiftL (Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack# Index n
v) Int
i
  shiftR :: Index n -> Int -> Index n
shiftR Index n
v Int
i        = BitVector (CLog 2 n) -> Index n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
BitVector (CLog 2 n) -> Index n
unpack# (BitVector (CLog 2 n) -> Index n)
-> BitVector (CLog 2 n) -> Index n
forall a b. (a -> b) -> a -> b
$ BitVector (CLog 2 n) -> Int -> BitVector (CLog 2 n)
forall a. Bits a => a -> Int -> a
shiftR (Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack# Index n
v) Int
i
  rotateL :: Index n -> Int -> Index n
rotateL Index n
v Int
i       = BitVector (CLog 2 n) -> Index n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
BitVector (CLog 2 n) -> Index n
unpack# (BitVector (CLog 2 n) -> Index n)
-> BitVector (CLog 2 n) -> Index n
forall a b. (a -> b) -> a -> b
$ BitVector (CLog 2 n) -> Int -> BitVector (CLog 2 n)
forall a. Bits a => a -> Int -> a
rotateL (Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack# Index n
v) Int
i
  rotateR :: Index n -> Int -> Index n
rotateR Index n
v Int
i       = BitVector (CLog 2 n) -> Index n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
BitVector (CLog 2 n) -> Index n
unpack# (BitVector (CLog 2 n) -> Index n)
-> BitVector (CLog 2 n) -> Index n
forall a b. (a -> b) -> a -> b
$ BitVector (CLog 2 n) -> Int -> BitVector (CLog 2 n)
forall a. Bits a => a -> Int -> a
rotateR (Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack# Index n
v) Int
i
  popCount :: Index n -> Int
popCount Index n
i        = BitVector (CLog 2 n) -> Int
forall a. Bits a => a -> Int
popCount (Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack# Index n
i)

instance (KnownNat n, 1 <= n) => FiniteBits (Index n) where
  finiteBitSize :: Index n -> Int
finiteBitSize        = Index n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => Index n -> Int
size#
  countLeadingZeros :: Index n -> Int
countLeadingZeros  Index n
i = BitVector (CLog 2 n) -> Int
forall b. FiniteBits b => b -> Int
countLeadingZeros  (Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack# Index n
i)
  countTrailingZeros :: Index n -> Int
countTrailingZeros Index n
i = BitVector (CLog 2 n) -> Int
forall b. FiniteBits b => b -> Int
countTrailingZeros (Index n -> BitVector (CLog 2 n)
forall (n :: Nat). Index n -> BitVector (CLog 2 n)
pack# Index n
i)

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

resize# :: KnownNat m => Index n -> Index m
resize# :: Index n -> Index m
resize# (I Integer
i) = Integer -> Index m
forall (n :: Nat). (HasCallStack, KnownNat n) => Integer -> Index n
fromInteger_INLINE Integer
i
{-# NOINLINE resize# #-}

instance KnownNat n => Lift (Index n) where
  lift :: Index n -> Q Exp
lift u :: Index n
u@(I Integer
i) = Q Exp -> TypeQ -> Q Exp
sigE [| fromInteger# i |] (Integer -> TypeQ
decIndex (Index n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal Index n
u))
  {-# NOINLINE lift #-}
#if MIN_VERSION_template_haskell(2,16,0)
  liftTyped :: Index n -> Q (TExp (Index n))
liftTyped = Index n -> Q (TExp (Index n))
forall a. Lift a => a -> Q (TExp a)
liftTypedFromUntyped
#endif

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

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

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

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

-- | None of the 'Read' class' methods are synthesizable.
instance KnownNat n => Read (Index n) where
  readPrec :: ReadPrec (Index n)
readPrec = Natural -> Index n
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Index n) -> ReadPrec Natural -> ReadPrec (Index 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 => Default (Index n) where
  def :: Index n
def = Integer -> Index n
forall (n :: Nat). KnownNat n => Integer -> Index n
fromInteger# Integer
0

instance KnownNat n => Arbitrary (Index n) where
  arbitrary :: Gen (Index n)
arbitrary = Gen (Index n)
forall a. (Bounded a, Integral a) => Gen a
arbitraryBoundedIntegral
  shrink :: Index n -> [Index n]
shrink    = Index n -> [Index n]
forall (n :: Nat). KnownNat n => Index n -> [Index n]
shrinkIndex

shrinkIndex :: KnownNat n => Index n -> [Index n]
shrinkIndex :: Index n -> [Index n]
shrinkIndex Index n
x | Index n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal Index n
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
3 = case Index n -> Integer
forall a. Integral a => a -> Integer
toInteger Index n
x of
                                 Integer
1 -> [Index n
0]
                                 Integer
_ -> []
              -- 'shrinkIntegral' uses "`quot` 2", which for 'Index' types with
              -- an upper bound less than 2 results in an error.
              | Bool
otherwise    = Index n -> [Index n]
forall a. Integral a => a -> [a]
shrinkIntegral Index n
x

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