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

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DeriveAnyClass #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE RoleAnnotations #-}
    {-# 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
      , toEnum#
      , fromEnum#
        -- ** Enum (not synthesizable)
      , enumFrom#
      , enumFromThen#
      , enumFromTo#
      , enumFromThenTo#
        -- ** Bounded
      , maxBound#
        -- ** Num
      , (+#)
      , (-#)
      , (*#)
      , negate#
      , 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 Text.Read                  (Read (..), ReadPrec)
    import Text.Printf                (PrintfArg (..), printf)
    import Data.Ix                    (Ix(..))
    import Language.Haskell.TH        (appT, conT, litT, numTyLit, sigE)
    import Language.Haskell.TH.Syntax (Lift(..))
    #if MIN_VERSION_template_haskell(2,16,0)
    import Language.Haskell.TH.Compat
    #endif
    #if MIN_VERSION_template_haskell(2,17,0)
    import Language.Haskell.TH        (Quote, Type)
    #else
    import Language.Haskell.TH        (TypeQ)
    #endif
    import GHC.Generics               (Generic)
    import GHC.Natural                (Natural, naturalFromInteger)
    import GHC.Natural                (naturalToInteger)
    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.Annotations.Primitive (hasBlackBox)
    import Clash.Class.BitPack.Internal (BitPack (..), packXWith)
    import Clash.Class.Num            (ExtendingNum (..), SaturatingNum (..),
                                       SaturationMode (..))
    import Clash.Class.Parity         (Parity (..))
    import Clash.Class.Resize         (Resize (..))
    import Clash.Class.BitPack.BitIndex (replaceBit)
    import Clash.Sized.Internal       (formatRange)
    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, seqX)

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

    type role Index nominal

    -- | Arbitrarily-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]
    -- ...
    --
    -- __NB__: The usual Haskell method of converting an integral numeric type to
    -- another, 'fromIntegral', is not well suited for Clash as it will go through
    -- 'Integer' which is arbitrarily bounded in HDL. Instead use
    -- 'Clash.Class.BitPack.bitCoerce' and the 'Resize' class.
    --
    -- Index has the <https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/roles.html type role>
    --
    -- >>> :i Index
    -- type role Index nominal
    -- ...
    --
    -- as it is not safe to coerce between 'Index'es with different ranges. To
    -- change the size, use the functions in the 'Resize' class.
    data Index (n :: Nat) =
        -- | The constructor, 'I', and the field, 'unsafeToInteger', are not
        -- synthesizable.
        I { forall (n :: Nat). Index n -> Integer
    unsafeToInteger :: !Integer }
      deriving (Typeable (Index n)
    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 -> Constr
    Index n -> DataType
    (forall b. Data b => b -> b) -> Index n -> Index n
    forall (n :: Nat). KnownNat n => Typeable (Index n)
    forall (n :: Nat). KnownNat n => Index n -> Constr
    forall (n :: Nat). KnownNat n => Index n -> DataType
    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 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 (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))
    $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)
    gfoldl :: 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)
    $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)
    gunfold :: forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Index n)
    $ctoConstr :: forall (n :: Nat). KnownNat n => Index n -> Constr
    toConstr :: Index n -> Constr
    $cdataTypeOf :: forall (n :: Nat). KnownNat n => Index n -> DataType
    dataTypeOf :: Index n -> DataType
    $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))
    dataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> 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))
    dataCast2 :: 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))
    $cgmapT :: forall (n :: Nat).
    KnownNat n =>
    (forall b. Data b => b -> b) -> Index n -> Index n
    gmapT :: (forall b. Data b => b -> b) -> Index n -> Index n
    $cgmapQl :: forall (n :: Nat) r r'.
    KnownNat n =>
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Index n -> r
    gmapQl :: forall r r'.
    (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
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Index n -> r
    $cgmapQ :: forall (n :: Nat) u.
    KnownNat n =>
    (forall d. Data d => d -> u) -> Index n -> [u]
    gmapQ :: forall u. (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
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Index n -> u
    $cgmapM :: forall (n :: Nat) (m :: Type -> Type).
    (KnownNat n, Monad m) =>
    (forall d. Data d => d -> m d) -> Index n -> m (Index n)
    gmapM :: forall (m :: Type -> Type).
    Monad m =>
    (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)
    gmapMp :: forall (m :: Type -> Type).
    MonadPlus m =>
    (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)
    gmapMo :: forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Index n -> m (Index n)
    Data, (forall x. Index n -> Rep (Index n) x)
    -> (forall x. Rep (Index n) x -> Index n) -> Generic (Index n)
    forall (n :: Nat) x. Rep (Index n) x -> Index n
    forall (n :: Nat) x. Index n -> Rep (Index n) x
    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
    $cfrom :: forall (n :: Nat) x. Index n -> Rep (Index n) x
    from :: forall x. Index n -> Rep (Index n) x
    $cto :: forall (n :: Nat) x. Rep (Index n) x -> Index n
    to :: forall x. Rep (Index n) x -> Index n
    Generic)

    {-# ANN I hasBlackBox #-}

    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE size# #-}
    size# :: (KnownNat n, 1 <= n) => Index n -> Int
    size# :: forall (n :: Nat). (KnownNat n, 1 <= n) => 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 () -> () -> ()
    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 (CLog 2 n) -> Index n
    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 + 1 <= m) => SNat n -> Index m
    fromSNat :: forall (m :: Nat) (n :: Nat).
    (KnownNat m, (n + 1) <= m) =>
    SNat n -> Index m
    fromSNat = SNat n -> Index m
    forall a (n :: Nat). Num a => SNat n -> a
    snatToNum

    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE pack# #-}
    {-# ANN pack# hasBlackBox #-}
    pack# :: Index n -> BitVector (CLog 2 n)
    pack# :: forall (n :: Nat). Index n -> BitVector (CLog 2 n)
    pack# (I Integer
    i) = Nat -> Nat -> BitVector (CLog 2 n)
    forall (n :: Nat). Nat -> Nat -> BitVector n
    BV Nat
    0 (Integer -> Nat
    naturalFromInteger Integer
    i)

    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE unpack# #-}
    {-# ANN unpack# hasBlackBox #-}
    unpack# :: (KnownNat n, 1 <= n) => BitVector (CLog 2 n) -> Index n
    unpack# :: forall (n :: Nat).
    (KnownNat n, 1 <= n) =>
    BitVector (CLog 2 n) -> Index n
    unpack# (BV Nat
    0 Nat
    i) = Integer -> Index n
    forall (n :: Nat). (HasCallStack, KnownNat n) => Integer -> Index n
    fromInteger_INLINE (Nat -> Integer
    naturalToInteger Nat
    i)
    unpack# BitVector (CLog 2 n)
    bv = String -> [BitVector (CLog 2 n)] -> Index n
    forall (n :: Nat) a. 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#

    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE eq# #-}
    {-# ANN eq# hasBlackBox #-}
    eq# :: (Index n) -> (Index n) -> Bool
    (I Integer
    n) eq# :: forall (n :: Nat). Index n -> Index n -> Bool
    `eq#` (I Integer
    m) = Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    m

    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE neq# #-}
    {-# ANN neq# hasBlackBox #-}
    neq# :: (Index n) -> (Index n) -> Bool
    (I Integer
    n) neq# :: forall (n :: Nat). 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
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE lt# #-}
    {-# ANN lt# hasBlackBox #-}
    lt# :: forall (n :: Nat). 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
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE ge# #-}
    {-# ANN ge# hasBlackBox #-}
    ge# :: forall (n :: Nat). 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
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE gt# #-}
    {-# ANN gt# hasBlackBox #-}
    gt# :: forall (n :: Nat). 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
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE le# #-}
    {-# ANN le# hasBlackBox #-}
    le# :: forall (n :: Nat). 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         = Int -> Index n
    forall (n :: Nat). KnownNat n => Int -> Index n
    toEnum#
      fromEnum :: Index n -> Int
    fromEnum       = Index n -> Int
    forall (n :: Nat). KnownNat n => Index n -> Int
    fromEnum#
      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#

    toEnum# :: forall n. KnownNat n => Int -> Index n
    toEnum# :: forall (n :: Nat). KnownNat n => 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
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE toEnum# #-}
    {-# ANN toEnum# hasBlackBox #-}

    fromEnum# :: forall n. KnownNat n => Index n -> Int
    fromEnum# :: forall (n :: Nat). KnownNat n => 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#
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE fromEnum# #-}
    {-# ANN fromEnum# hasBlackBox #-}

    enumFrom# :: forall n. KnownNat n => Index n -> [Index n]
    enumFrom# :: forall (n :: Nat). KnownNat n => Index n -> [Index n]
    enumFrom# Index n
    x = [Index n
    x .. Index n
    forall a. Bounded a => a
    maxBound]
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE enumFrom# #-}

    enumFromThen# :: forall n. KnownNat n => Index n -> Index n -> [Index n]
    enumFromThen# :: forall (n :: Nat). KnownNat n => 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]
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE enumFromThen# #-}

    enumFromTo# :: Index n -> Index n -> [Index n]
    enumFromTo# :: forall (n :: Nat). 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]
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE enumFromTo# #-}

    enumFromThenTo# :: Index n -> Index n -> Index n -> [Index n]
    enumFromThenTo# :: forall (n :: Nat). 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]
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE 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# :: forall (n :: Nat). KnownNat n => Index n
    maxBound# =
      case 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)
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE maxBound# #-}
    {-# ANN maxBound# hasBlackBox #-}

    -- | Operators report an error on overflow and underflow
    --
    -- __NB__: 'fromInteger'/'fromIntegral' can cause unexpected truncation, as
    -- 'Integer' is arbitrarily bounded during synthesis.  Prefer
    -- 'Clash.Class.BitPack.bitCoerce' and the 'Resize' class.
    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 -> Index n
    forall (n :: Nat). KnownNat n => Index n -> Index n
    negate#
      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
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE (+#) #-}
    {-# ANN (+#) hasBlackBox #-}
    +# :: forall (n :: Nat). KnownNat n => 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

    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE (-#) #-}
    {-# ANN (-#) hasBlackBox #-}
    -# :: forall (n :: Nat). KnownNat n => 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

    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE (*#) #-}
    {-# ANN (*#) hasBlackBox #-}
    *# :: forall (n :: Nat). KnownNat n => 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

    negate# :: KnownNat n => Index n -> Index n
    negate# :: forall (n :: Nat). KnownNat n => Index n -> Index n
    negate# Index n
    0 = Index n
    0
    negate# Index n
    i = 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
    i Index n -> Index n -> Index n
    forall (n :: Nat). KnownNat n => Index n -> Index n -> Index n
    +# Index n
    1

    fromInteger# :: KnownNat n => Integer -> Index n
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE fromInteger# #-}
    {-# ANN fromInteger# hasBlackBox #-}
    fromInteger# :: forall (n :: Nat). KnownNat n => 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 :: forall (n :: Nat). (HasCallStack, KnownNat n) => Integer -> Index n
    fromInteger_INLINE 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
    > (-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 = forall (n :: Nat). KnownNat n => Integer
    natToInteger @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: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Integer -> Integer -> String
    forall a. (Ord a, Show a) => a -> a -> String
    formatRange Integer
    0 (Integer
    bound Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1))

    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)
    Index m -> Index n -> Index ((m + n) - 1)
    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)
    Index m -> Index n -> Index ((m + n) - 1)
    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)
    Index m -> Index n -> Index (((m - 1) * (n - 1)) + 1)
    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)
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE plus# #-}
    {-# ANN plus# hasBlackBox #-}
    plus# :: forall (m :: Nat) (n :: Nat).
    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)

    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE minus# #-}
    {-# ANN minus# hasBlackBox #-}
    minus# :: forall (m :: Nat) (n :: Nat).
    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

    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE times# #-}
    {-# ANN times# hasBlackBox #-}
    times# :: Index m -> Index n -> Index (((m - 1) * (n - 1)) + 1)
    times# :: forall (m :: Nat) (n :: Nat).
    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 forall (n :: Nat). KnownNat n => Integer
    natToInteger @n of
          Integer
    1 -> Index n
    a Index n -> Index n -> Index n
    forall (n :: Nat). KnownNat n => Index n -> Index n -> Index n
    +# Index n
    b
          Integer
    _ -> 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# (forall (n :: Nat). KnownNat n => Integer
    natToInteger @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 (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# (forall (n :: Nat). KnownNat n => Integer
    natToInteger @(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
    SatError Index n
    a Index n
    b =
        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# (forall (n :: Nat). KnownNat n => Integer
    natToInteger @(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 -> String -> Index n
    forall a. HasCallStack => String -> a
    errorX String
    "Index.satAdd: overflow"
            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 (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# (forall (n :: Nat). KnownNat n => Integer
    natToInteger @(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
    SatError 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 String -> Index n
    forall a. HasCallStack => String -> a
    errorX String
    "Index.satSub: underflow"
           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 forall (n :: Nat). KnownNat n => Integer
    natToInteger @n of
          Integer
    1 -> Index n
    a Index n -> Index n -> Index n
    forall (n :: Nat). KnownNat n => Index n -> Index n -> Index n
    *# Index n
    b
          Integer
    2 -> case Index n
    a of {Index n
    0 -> Index n
    0; Index n
    _ -> Index n
    b}
          Integer
    _ -> 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# (forall (n :: Nat). KnownNat n => Integer
    natToInteger @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 (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# (forall (n :: Nat). KnownNat n => Integer
    natToInteger @(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
    SatError Index n
    a Index n
    b =
        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# (forall (n :: Nat). KnownNat n => Integer
    natToInteger @(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 -> String -> Index n
    forall a. HasCallStack => String -> a
    errorX String
    "Index.satMul: overflow"
            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 (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# (forall (n :: Nat). KnownNat n => Integer
    natToInteger @(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

      satSucc :: SaturationMode -> Index n -> Index n
    satSucc SaturationMode
    SatError Index n
    a =
        case forall (n :: Nat). KnownNat n => Integer
    natToInteger @n of
          Integer
    1 -> Index n
    a Index n -> Index n -> Index n
    forall a b. a -> b -> b
    `seqX` String -> Index n
    forall a. HasCallStack => String -> a
    errorX String
    "Index.satSucc: overflow"
          Integer
    _ -> SaturationMode -> Index n -> Index n -> Index n
    forall a. SaturatingNum a => SaturationMode -> a -> a -> a
    satAdd SaturationMode
    SatError Index n
    a (Index n -> Index n) -> Index n -> Index n
    forall a b. (a -> b) -> a -> b
    $ Integer -> Index n
    forall (n :: Nat). KnownNat n => Integer -> Index n
    fromInteger# Integer
    1
      satSucc SaturationMode
    satMode !Index n
    a =
        case forall (n :: Nat). KnownNat n => Integer
    natToInteger @n of
          Integer
    1 -> Integer -> Index n
    forall (n :: Nat). KnownNat n => Integer -> Index n
    fromInteger# Integer
    0
          Integer
    _ -> SaturationMode -> Index n -> Index n -> Index n
    forall a. SaturatingNum a => SaturationMode -> a -> a -> a
    satAdd SaturationMode
    satMode Index n
    a (Index n -> Index n) -> Index n -> Index n
    forall a b. (a -> b) -> a -> b
    $ Integer -> Index n
    forall (n :: Nat). KnownNat n => Integer -> Index n
    fromInteger# Integer
    1
      {-# INLINE satSucc #-}

      satPred :: SaturationMode -> Index n -> Index n
    satPred SaturationMode
    SatError Index n
    a =
        case forall (n :: Nat). KnownNat n => Integer
    natToInteger @n of
          Integer
    1 -> Index n
    a Index n -> Index n -> Index n
    forall a b. a -> b -> b
    `seqX` String -> Index n
    forall a. HasCallStack => String -> a
    errorX String
    "Index.satPred: underflow"
          Integer
    _ -> SaturationMode -> Index n -> Index n -> Index n
    forall a. SaturatingNum a => SaturationMode -> a -> a -> a
    satSub SaturationMode
    SatError Index n
    a (Index n -> Index n) -> Index n -> Index n
    forall a b. (a -> b) -> a -> b
    $ Integer -> Index n
    forall (n :: Nat). KnownNat n => Integer -> Index n
    fromInteger# Integer
    1
      satPred SaturationMode
    satMode !Index n
    a =
        case forall (n :: Nat). KnownNat n => Integer
    natToInteger @n of
          Integer
    1 -> Integer -> Index n
    forall (n :: Nat). KnownNat n => Integer -> Index n
    fromInteger# Integer
    0
          Integer
    _ -> SaturationMode -> Index n -> Index n -> Index n
    forall a. SaturatingNum a => SaturationMode -> a -> a -> a
    satSub SaturationMode
    satMode Index n
    a (Index n -> Index n) -> Index n -> Index n
    forall a b. (a -> b) -> a -> b
    $ Integer -> Index n
    forall (n :: Nat). KnownNat n => Integer -> Index n
    fromInteger# Integer
    1
      {-# INLINE satPred #-}

    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#

    -- | __NB__: 'toInteger'/'fromIntegral' can cause unexpected truncation, as
    -- 'Integer' is arbitrarily bounded during synthesis.  Prefer
    -- 'Clash.Class.BitPack.bitCoerce' and the 'Resize' class.
    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
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE quot# #-}
    {-# ANN quot# hasBlackBox #-}
    (I Integer
    a) quot# :: forall (n :: Nat). 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)
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE rem# #-}
    {-# ANN rem# hasBlackBox #-}
    (I Integer
    a) rem# :: forall (n :: Nat). 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)

    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE toInteger# #-}
    {-# ANN toInteger# hasBlackBox #-}
    toInteger# :: Index n -> Integer
    toInteger# :: forall (n :: Nat). Index n -> Integer
    toInteger# (I Integer
    n) = Integer
    n

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

    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)
    Index n -> BitVector (BitSize (Index 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)
    Index n -> BitVector (BitSize (Index 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 :: forall (a :: Nat) (b :: Nat).
    (KnownNat a, KnownNat b) =>
    Index a -> Index b
    resize     = Index a -> Index b
    forall (m :: Nat) (n :: Nat). KnownNat m => Index n -> Index m
    resize#
      zeroExtend :: forall (a :: Nat) (b :: Nat).
    (KnownNat a, KnownNat b) =>
    Index a -> Index (b + a)
    zeroExtend = Index a -> Index (b + a)
    forall (a :: Nat) (b :: Nat).
    (KnownNat a, KnownNat b) =>
    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 :: forall (a :: Nat) (b :: Nat).
    KnownNat a =>
    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# :: forall (m :: Nat) (n :: Nat). KnownNat m => Index n -> Index m
    resize# (I Integer
    i) = Integer -> Index m
    forall (n :: Nat). (HasCallStack, KnownNat n) => Integer -> Index n
    fromInteger_INLINE Integer
    i
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE resize# #-}
    {-# ANN resize# hasBlackBox #-}

    instance KnownNat n => Lift (Index n) where
      lift :: forall (m :: Type -> Type). Quote m => Index n -> m Exp
    lift u :: Index n
    u@(I Integer
    i) = m Exp -> m Type -> m Exp
    forall (m :: Type -> Type). Quote m => m Exp -> m Type -> m Exp
    sigE [| fromInteger# i |] (Integer -> m Type
    forall (m :: Type -> Type). Quote m => Integer -> m Type
    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 :: forall (m :: Type -> Type). Quote m => Index n -> Code m (Index n)
    liftTyped = Index n -> Code m (Index n)
    forall a (m :: Type -> Type). (Lift a, Quote m) => a -> Code m a
    liftTypedFromUntyped
    #endif

    #if MIN_VERSION_template_haskell(2,17,0)
    decIndex :: Quote m => Integer -> m Type
    #else
    decIndex :: Integer -> TypeQ
    #endif
    decIndex :: forall (m :: Type -> Type). Quote m => Integer -> m Type
    decIndex Integer
    n = m Type -> m Type -> m Type
    forall (m :: Type -> Type). Quote m => m Type -> m Type -> m Type
    appT (Name -> m Type
    forall (m :: Type -> Type). Quote m => Name -> m Type
    conT ''Index) (m TyLit -> m Type
    forall (m :: Type -> Type). Quote m => m TyLit -> m Type
    litT (m TyLit -> m Type) -> m TyLit -> m Type
    forall a b. (a -> b) -> a -> b
    $ Integer -> m TyLit
    forall (m :: Type -> Type). Quote m => Integer -> m TyLit
    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 :: HasCallStack => String -> Index n
    deepErrorX = String -> Index n
    forall a. HasCallStack => String -> a
    errorX
      ensureSpine :: Index n -> Index n
    ensureSpine = Index n -> Index n
    forall a. a -> a
    id
      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 = Nat -> Index n
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Nat -> Index n) -> ReadPrec Nat -> ReadPrec (Index n)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> (ReadPrec Nat
    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 :: forall (n :: Nat). KnownNat n => 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 :: forall b. Index n -> Gen b -> Gen b
    coarbitrary = Index n -> Gen b -> Gen b
    forall a b. Integral a => a -> Gen b -> Gen b
    coarbitraryIntegral

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