{-|
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 BangPatterns          #-}
{-# LANGUAGE CPP                   #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveDataTypeable    #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MagicHash             #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}
#if __GLASGOW_HASKELL__ >= 806
{-# LANGUAGE NoStarIsType #-}
#endif

{-# 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 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(..))
import Numeric.Natural            (Natural)
import GHC.Generics               (Generic)
import GHC.Stack                  (HasCallStack)
import GHC.TypeLits               (CmpNat, 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.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, leToPlusKN)
import Clash.XException
  (ShowX (..), NFDataX (..), errorX, showsPrecXWith, rwhnfX)

-- | 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 i :: Integer
i) = Integer -> ()
forall a. NFData a => a -> ()
rnf Integer
i () -> () -> ()
forall a b. a -> b -> b
`seq` ()
  {-# NOINLINE rnf #-}
  -- NOINLINE is needed so that Clash doesn't trip on the "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, CmpNat n m ~ 'LT) => 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 i :: Integer
i) = Integer -> Integer -> BitVector (CLog 2 n)
forall (n :: Nat). Integer -> Integer -> BitVector n
BV 0 Integer
i

{-# NOINLINE unpack# #-}
unpack# :: (KnownNat n, 1 <= n) => BitVector (CLog 2 n) -> Index n
unpack# :: BitVector (CLog 2 n) -> Index n
unpack# (BV 0 i :: Integer
i) = Integer -> Index n
forall (n :: Nat). (HasCallStack, KnownNat n) => Integer -> Index n
fromInteger_INLINE Integer
i
unpack# bv :: BitVector (CLog 2 n)
bv = String -> [BitVector (CLog 2 n)] -> Index n
forall (n :: Nat) a.
(HasCallStack, KnownNat n) =>
String -> [BitVector n] -> a
undefError "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 n :: Integer
n) eq# :: Index n -> Index n -> Bool
`eq#` (I m :: 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 n :: Integer
n) neq# :: Index n -> Index n -> Bool
`neq#` (I m :: 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 n :: Integer
n) (I m :: 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 n :: Integer
n) (I m :: 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 n :: Integer
n) (I m :: 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 n :: Integer
n) (I m :: Integer
m) = Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
m

-- | The functions: 'enumFrom', 'enumFromThen', 'enumFromTo', and
-- 'enumFromThenTo', are not synthesizable.
instance KnownNat n => Enum (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# 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# 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#

{-# NOINLINE enumFrom# #-}
{-# NOINLINE enumFromThen# #-}
{-# NOINLINE enumFromTo# #-}
{-# NOINLINE enumFromThenTo# #-}
enumFrom#       :: KnownNat n => Index n -> [Index n]
enumFromThen#   :: KnownNat n => Index n -> Index n -> [Index n]
enumFromTo#     :: Index n -> Index n -> [Index n]
enumFromThenTo# :: Index n -> Index n -> Index n -> [Index n]
enumFrom# :: Index n -> [Index n]
enumFrom# x :: Index n
x             = (Integer -> Index n) -> [Integer] -> [Index n]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> Index n
forall (n :: Nat). (HasCallStack, KnownNat n) => Integer -> Index n
fromInteger_INLINE [Index n -> Integer
forall (n :: Nat). Index n -> Integer
unsafeToInteger Index n
x ..]
enumFromThen# :: Index n -> Index n -> [Index n]
enumFromThen# x :: Index n
x y :: Index n
y       = (Integer -> Index n) -> [Integer] -> [Index n]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> Index n
forall (n :: Nat). (HasCallStack, KnownNat n) => Integer -> Index n
fromInteger_INLINE [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 ..]
enumFromTo# :: Index n -> Index n -> [Index n]
enumFromTo# x :: Index n
x y :: 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]
enumFromThenTo# :: Index n -> Index n -> Index n -> [Index n]
enumFromThenTo# x1 :: Index n
x1 x2 :: Index n
x2 y :: 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]

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

{-# NOINLINE maxBound# #-}
maxBound# :: KnownNat n => Index n
maxBound# :: Index n
maxBound# = let res :: Index n
res = Integer -> Index n
forall (n :: Nat). (HasCallStack, KnownNat n) => Integer -> Index n
fromInteger_INLINE (Index n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal Index n
res Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1) in Index n
res

-- | 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 i :: Index n
i    = if Index n
i Index n -> Index n -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then 0 else 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 a :: Integer
a) (I b :: 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 a :: Integer
a) (I b :: 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 a :: Integer
a) (I b :: 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 i :: Integer
i = Integer
bound Integer -> Index n -> Index n
forall a b. a -> b -> b
`seq` if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> (-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 ("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]
++
                   " 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
- 1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "]")

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 a :: Integer
a) (I b :: 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 a :: Integer
a) (I b :: 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 ("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]
++
                   " is smaller than 0")
      res :: Index ((m + n) - 1)
res = if Integer
z Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 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 a :: Integer
a) (I b :: 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 SatWrap !Index n
a !Index n
b =
    case SNat n -> Int
forall a (n :: Nat). Num a => SNat n -> a
snatToNum @Int (KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat @n) of
      1 -> Integer -> Index n
forall (n :: Nat). KnownNat n => Integer -> Index n
fromInteger# 0
      _ -> 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
          z :: 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)
          z :: 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 SatZero a :: Index n
a b :: 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
        z :: 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# 0
        z :: 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 _ a :: Index n
a b :: 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
        z :: 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#
        z :: 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 SatWrap a :: Index n
a b :: 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
+# 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 _ a :: Index n
a b :: 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# 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 SatWrap !Index n
a !Index n
b =
    case SNat n -> Int
forall a (n :: Nat). Num a => SNat n -> a
snatToNum @Int (KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat @n) of
      1 -> Integer -> Index n
forall (n :: Nat). KnownNat n => Integer -> Index n
fromInteger# 0
      _ -> 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
          z :: 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 SatZero a :: Index n
a b :: 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
        z :: 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# 0
        z :: 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 _ a :: Index n
a b :: 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
        z :: 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#
        z :: 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 n :: Index n
n d :: 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  n :: Index n
n d :: 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 a :: Integer
a) quot# :: Index n -> Index n -> Index n
`quot#` (I b :: 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 a :: Integer
a) rem# :: Index n -> Index n -> Index n
`rem#` (I b :: 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 n :: Integer
n) = Integer
n

instance (KnownNat n, 1 <= n) => Bits (Index n) where
  a :: Index n
a .&. :: Index n -> Index n -> Index n
.&. b :: 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). 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)
  a :: Index n
a .|. :: Index n -> Index n -> Index n
.|. b :: 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). 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 a :: Index n
a b :: 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). 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 i :: 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 v :: Index n
v i :: 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, KnownNat (BitSize 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 v :: Index n
v i :: 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, KnownNat (BitSize 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 v :: Index n
v i :: 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 v :: Index n
v i :: 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 v :: 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 _        = Bool
False
  shiftL :: Index n -> Int -> Index n
shiftL v :: Index n
v i :: 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 v :: Index n
v i :: 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 v :: Index n
v i :: 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 v :: Index n
v i :: 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 i :: 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  i :: 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 i :: 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 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 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 #-}

decIndex :: Integer -> TypeQ
decIndex :: Integer -> TypeQ
decIndex n :: 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 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# 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 x :: 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
< 3 = case Index n -> Integer
forall a. Integral a => a -> Integer
toInteger Index n
x of
                                 1 -> [0]
                                 _ -> []
              -- '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