    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Core.Sized
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Type-level sized bit-vectors. Thanks to Ben Blaxill for providing an
    -- initial implementation of this idea.
    -----------------------------------------------------------------------------

    {-# LANGUAGE DataKinds            #-}
    {-# LANGUAGE FlexibleInstances    #-}
    {-# LANGUAGE ScopedTypeVariables  #-}
    {-# LANGUAGE TypeApplications     #-}
    {-# LANGUAGE TypeFamilies         #-}
    {-# LANGUAGE TypeOperators        #-}
    {-# LANGUAGE UndecidableInstances #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Core.Sized (
            -- * Type-sized unsigned bit-vectors
              SWord, WordN, sWord, sWord_, sWords
            -- * Type-sized signed bit-vectors
            , SInt, IntN, sInt, sInt_, sInts
            -- * Bit-vector operations
            , bvExtract, (#), zeroExtend, signExtend, bvDrop, bvTake
           ) where

    import Data.Bits
    import Data.Maybe (fromJust)
    import Data.Proxy (Proxy(..))

    import GHC.TypeLits

    import Data.SBV.Core.Data
    import Data.SBV.Core.Kind
    import Data.SBV.Core.Model
    import Data.SBV.Core.Operations
    import Data.SBV.Core.Symbolic

    import Data.SBV.SMT.SMT

    import Test.QuickCheck(Arbitrary(..))

    -- | An unsigned bit-vector carrying its size info
    newtype WordN (n :: Nat) = WordN Integer deriving (WordN n -> WordN n -> Bool
    (WordN n -> WordN n -> Bool)
    -> (WordN n -> WordN n -> Bool) -> Eq (WordN n)
    forall (n :: Nat). WordN n -> WordN n -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall (n :: Nat). WordN n -> WordN n -> Bool
    == :: WordN n -> WordN n -> Bool
    $c/= :: forall (n :: Nat). WordN n -> WordN n -> Bool
    /= :: WordN n -> WordN n -> Bool
    Eq, Eq (WordN n)
    Eq (WordN n) =>
    (WordN n -> WordN n -> Ordering)
    -> (WordN n -> WordN n -> Bool)
    -> (WordN n -> WordN n -> Bool)
    -> (WordN n -> WordN n -> Bool)
    -> (WordN n -> WordN n -> Bool)
    -> (WordN n -> WordN n -> WordN n)
    -> (WordN n -> WordN n -> WordN n)
    -> Ord (WordN n)
    WordN n -> WordN n -> Bool
    WordN n -> WordN n -> Ordering
    WordN n -> WordN n -> WordN n
    forall (n :: Nat). Eq (WordN n)
    forall (n :: Nat). WordN n -> WordN n -> Bool
    forall (n :: Nat). WordN n -> WordN n -> Ordering
    forall (n :: Nat). WordN n -> WordN n -> WordN n
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: forall (n :: Nat). WordN n -> WordN n -> Ordering
    compare :: WordN n -> WordN n -> Ordering
    $c< :: forall (n :: Nat). WordN n -> WordN n -> Bool
    < :: WordN n -> WordN n -> Bool
    $c<= :: forall (n :: Nat). WordN n -> WordN n -> Bool
    <= :: WordN n -> WordN n -> Bool
    $c> :: forall (n :: Nat). WordN n -> WordN n -> Bool
    > :: WordN n -> WordN n -> Bool
    $c>= :: forall (n :: Nat). WordN n -> WordN n -> Bool
    >= :: WordN n -> WordN n -> Bool
    $cmax :: forall (n :: Nat). WordN n -> WordN n -> WordN n
    max :: WordN n -> WordN n -> WordN n
    $cmin :: forall (n :: Nat). WordN n -> WordN n -> WordN n
    min :: WordN n -> WordN n -> WordN n
    Ord)

    -- | A symbolic unsigned bit-vector carrying its size info
    type SWord (n :: Nat) = SBV (WordN n)

    -- | Show instance for 'WordN'
    instance Show (WordN n) where
      show :: WordN n -> String
    show (WordN Integer
    v) = Integer -> String
    forall a. Show a => a -> String
    show Integer
    v

    -- | 'WordN' has a kind
    instance (KnownNat n, BVIsNonZero n) => HasKind (WordN n) where
      kindOf :: WordN n -> Kind
    kindOf WordN n
    _ = Bool -> Int -> Kind
    KBounded Bool
    False (Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n))

    -- | 'SymVal' instance for 'WordN'
    instance (KnownNat n, BVIsNonZero n) => SymVal (WordN n) where
       literal :: WordN n -> SBV (WordN n)
    literal  WordN n
    x = Kind -> WordN n -> SBV (WordN n)
    forall a b. Integral a => Kind -> a -> SBV b
    genLiteral  (WordN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf WordN n
    x) WordN n
    x
       mkSymVal :: forall (m :: * -> *).
    MonadSymbolic m =>
    VarContext -> Maybe String -> m (SBV (WordN n))
    mkSymVal   = Kind -> VarContext -> Maybe String -> m (SBV (WordN n))
    forall (m :: * -> *) a.
    MonadSymbolic m =>
    Kind -> VarContext -> Maybe String -> m (SBV a)
    genMkSymVar (WordN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (WordN n
    forall a. HasCallStack => a
    undefined :: WordN n))
       fromCV :: CV -> WordN n
    fromCV     = CV -> WordN n
    forall a. Integral a => CV -> a
    genFromCV

    -- | A signed bit-vector carrying its size info
    newtype IntN (n :: Nat) = IntN Integer deriving (IntN n -> IntN n -> Bool
    (IntN n -> IntN n -> Bool)
    -> (IntN n -> IntN n -> Bool) -> Eq (IntN n)
    forall (n :: Nat). IntN n -> IntN n -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall (n :: Nat). IntN n -> IntN n -> Bool
    == :: IntN n -> IntN n -> Bool
    $c/= :: forall (n :: Nat). IntN n -> IntN n -> Bool
    /= :: IntN n -> IntN n -> Bool
    Eq, Eq (IntN n)
    Eq (IntN n) =>
    (IntN n -> IntN n -> Ordering)
    -> (IntN n -> IntN n -> Bool)
    -> (IntN n -> IntN n -> Bool)
    -> (IntN n -> IntN n -> Bool)
    -> (IntN n -> IntN n -> Bool)
    -> (IntN n -> IntN n -> IntN n)
    -> (IntN n -> IntN n -> IntN n)
    -> Ord (IntN n)
    IntN n -> IntN n -> Bool
    IntN n -> IntN n -> Ordering
    IntN n -> IntN n -> IntN n
    forall (n :: Nat). Eq (IntN n)
    forall (n :: Nat). IntN n -> IntN n -> Bool
    forall (n :: Nat). IntN n -> IntN n -> Ordering
    forall (n :: Nat). IntN n -> IntN n -> IntN n
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: forall (n :: Nat). IntN n -> IntN n -> Ordering
    compare :: IntN n -> IntN n -> Ordering
    $c< :: forall (n :: Nat). IntN n -> IntN n -> Bool
    < :: IntN n -> IntN n -> Bool
    $c<= :: forall (n :: Nat). IntN n -> IntN n -> Bool
    <= :: IntN n -> IntN n -> Bool
    $c> :: forall (n :: Nat). IntN n -> IntN n -> Bool
    > :: IntN n -> IntN n -> Bool
    $c>= :: forall (n :: Nat). IntN n -> IntN n -> Bool
    >= :: IntN n -> IntN n -> Bool
    $cmax :: forall (n :: Nat). IntN n -> IntN n -> IntN n
    max :: IntN n -> IntN n -> IntN n
    $cmin :: forall (n :: Nat). IntN n -> IntN n -> IntN n
    min :: IntN n -> IntN n -> IntN n
    Ord)

    -- | A symbolic signed bit-vector carrying its size info
    type SInt (n :: Nat) = SBV (IntN n)

    -- | Show instance for 'IntN'
    instance Show (IntN n) where
      show :: IntN n -> String
    show (IntN Integer
    v) = Integer -> String
    forall a. Show a => a -> String
    show Integer
    v

    -- | 'IntN' has a kind
    instance (KnownNat n, BVIsNonZero n) => HasKind (IntN n) where
      kindOf :: IntN n -> Kind
    kindOf IntN n
    _ = Bool -> Int -> Kind
    KBounded Bool
    True (Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n))

    -- | 'SymVal' instance for 'IntN'
    instance (KnownNat n, BVIsNonZero n) => SymVal (IntN n) where
       literal :: IntN n -> SBV (IntN n)
    literal  IntN n
    x = Kind -> IntN n -> SBV (IntN n)
    forall a b. Integral a => Kind -> a -> SBV b
    genLiteral  (IntN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf IntN n
    x) IntN n
    x
       mkSymVal :: forall (m :: * -> *).
    MonadSymbolic m =>
    VarContext -> Maybe String -> m (SBV (IntN n))
    mkSymVal   = Kind -> VarContext -> Maybe String -> m (SBV (IntN n))
    forall (m :: * -> *) a.
    MonadSymbolic m =>
    Kind -> VarContext -> Maybe String -> m (SBV a)
    genMkSymVar (IntN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (IntN n
    forall a. HasCallStack => a
    undefined :: IntN n))
       fromCV :: CV -> IntN n
    fromCV     = CV -> IntN n
    forall a. Integral a => CV -> a
    genFromCV

    -- Lift a unary operation via SVal
    lift1 :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> SVal) -> bv n -> bv n
    lift1 :: forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal) -> bv n -> bv n
    lift1 String
    nm SVal -> SVal
    op bv n
    x = SVal -> bv n
    uc (SVal -> bv n) -> SVal -> bv n
    forall a b. (a -> b) -> a -> b
    $ SVal -> SVal
    op (bv n -> SVal
    c bv n
    x)
      where k :: Kind
    k = bv n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf bv n
    x
            c :: bv n -> SVal
    c = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal)
    -> (bv n -> Either CV (Cached SV)) -> bv n -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV))
    -> (bv n -> CV) -> bv n -> Either CV (Cached SV)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CV -> CV
    normCV (CV -> CV) -> (bv n -> CV) -> bv n -> CV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> (bv n -> CVal) -> bv n -> CV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> CVal
    CInteger (Integer -> CVal) -> (bv n -> Integer) -> bv n -> CVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . bv n -> Integer
    forall a. Integral a => a -> Integer
    toInteger
            uc :: SVal -> bv n
    uc (SVal Kind
    _ (Left (CV Kind
    _ (CInteger Integer
    v)))) = Integer -> bv n
    forall a. Num a => Integer -> a
    fromInteger Integer
    v
            uc SVal
    r                                   = String -> bv n
    forall a. HasCallStack => String -> a
    error (String -> bv n) -> String -> bv n
    forall a b. (a -> b) -> a -> b
    $ String
    "Impossible happened while lifting " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " over " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Kind, bv n, SVal) -> String
    forall a. Show a => a -> String
    show (Kind
    k, bv n
    x, SVal
    r)

    -- Lift a binary operation via SVal
    lift2 :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2 :: forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2 String
    nm SVal -> SVal -> SVal
    op bv n
    x bv n
    y = SVal -> bv n
    uc (SVal -> bv n) -> SVal -> bv n
    forall a b. (a -> b) -> a -> b
    $ bv n -> SVal
    c bv n
    x SVal -> SVal -> SVal
    `op` bv n -> SVal
    c bv n
    y
      where k :: Kind
    k = bv n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf bv n
    x
            c :: bv n -> SVal
    c = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal)
    -> (bv n -> Either CV (Cached SV)) -> bv n -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV))
    -> (bv n -> CV) -> bv n -> Either CV (Cached SV)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CV -> CV
    normCV (CV -> CV) -> (bv n -> CV) -> bv n -> CV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> (bv n -> CVal) -> bv n -> CV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> CVal
    CInteger (Integer -> CVal) -> (bv n -> Integer) -> bv n -> CVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . bv n -> Integer
    forall a. Integral a => a -> Integer
    toInteger
            uc :: SVal -> bv n
    uc (SVal Kind
    _ (Left (CV Kind
    _ (CInteger Integer
    v)))) = Integer -> bv n
    forall a. Num a => Integer -> a
    fromInteger Integer
    v
            uc SVal
    r                                   = String -> bv n
    forall a. HasCallStack => String -> a
    error (String -> bv n) -> String -> bv n
    forall a b. (a -> b) -> a -> b
    $ String
    "Impossible happened while lifting " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " over " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Kind, bv n, bv n, SVal) -> String
    forall a. Show a => a -> String
    show (Kind
    k, bv n
    x, bv n
    y, SVal
    r)

    -- Lift a binary operation via SVal where second argument is an Int
    lift2I :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I :: forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I String
    nm SVal -> Int -> SVal
    op bv n
    x Int
    i = SVal -> bv n
    uc (SVal -> bv n) -> SVal -> bv n
    forall a b. (a -> b) -> a -> b
    $ bv n -> SVal
    c bv n
    x SVal -> Int -> SVal
    `op` Int
    i
      where k :: Kind
    k = bv n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf bv n
    x
            c :: bv n -> SVal
    c = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal)
    -> (bv n -> Either CV (Cached SV)) -> bv n -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV))
    -> (bv n -> CV) -> bv n -> Either CV (Cached SV)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CV -> CV
    normCV (CV -> CV) -> (bv n -> CV) -> bv n -> CV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> (bv n -> CVal) -> bv n -> CV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> CVal
    CInteger (Integer -> CVal) -> (bv n -> Integer) -> bv n -> CVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . bv n -> Integer
    forall a. Integral a => a -> Integer
    toInteger
            uc :: SVal -> bv n
    uc (SVal Kind
    _ (Left (CV Kind
    _ (CInteger Integer
    v)))) = Integer -> bv n
    forall a. Num a => Integer -> a
    fromInteger Integer
    v
            uc SVal
    r                                   = String -> bv n
    forall a. HasCallStack => String -> a
    error (String -> bv n) -> String -> bv n
    forall a b. (a -> b) -> a -> b
    $ String
    "Impossible happened while lifting " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " over " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Kind, bv n, Int, SVal) -> String
    forall a. Show a => a -> String
    show (Kind
    k, bv n
    x, Int
    i, SVal
    r)

    -- Lift a binary operation via SVal where second argument is an Int and returning a Bool
    lift2IB :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool
    lift2IB :: forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool
    lift2IB String
    nm SVal -> Int -> SVal
    op bv n
    x Int
    i = SVal -> Bool
    uc (SVal -> Bool) -> SVal -> Bool
    forall a b. (a -> b) -> a -> b
    $ bv n -> SVal
    c bv n
    x SVal -> Int -> SVal
    `op` Int
    i
      where k :: Kind
    k = bv n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf bv n
    x
            c :: bv n -> SVal
    c = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal)
    -> (bv n -> Either CV (Cached SV)) -> bv n -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV))
    -> (bv n -> CV) -> bv n -> Either CV (Cached SV)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CV -> CV
    normCV (CV -> CV) -> (bv n -> CV) -> bv n -> CV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> (bv n -> CVal) -> bv n -> CV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> CVal
    CInteger (Integer -> CVal) -> (bv n -> Integer) -> bv n -> CVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . bv n -> Integer
    forall a. Integral a => a -> Integer
    toInteger
            uc :: SVal -> Bool
    uc (SVal Kind
    _ (Left CV
    v)) = CV -> Bool
    cvToBool CV
    v
            uc SVal
    r                 = String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ String
    "Impossible happened while lifting " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " over " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Kind, bv n, Int, SVal) -> String
    forall a. Show a => a -> String
    show (Kind
    k, bv n
    x, Int
    i, SVal
    r)

    -- | 'Bounded' instance for 'WordN'
    instance (KnownNat n, BVIsNonZero n) => Bounded (WordN n) where
       minBound :: WordN n
    minBound = Integer -> WordN n
    forall (n :: Nat). Integer -> WordN n
    WordN Integer
    0
       maxBound :: WordN n
    maxBound = let sz :: Int
    sz = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n) in Integer -> WordN n
    forall (n :: Nat). Integer -> WordN n
    WordN (Integer -> WordN n) -> Integer -> WordN n
    forall a b. (a -> b) -> a -> b
    $ Integer
    2 Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Int
    sz Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1

    -- | 'Bounded' instance for 'IntN'
    instance (KnownNat n, BVIsNonZero n) => Bounded (IntN n) where
       minBound :: IntN n
    minBound = let sz1 :: Int
    sz1 = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 in Integer -> IntN n
    forall (n :: Nat). Integer -> IntN n
    IntN (Integer -> IntN n) -> Integer -> IntN n
    forall a b. (a -> b) -> a -> b
    $ - (Integer
    2 Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Int
    sz1)
       maxBound :: IntN n
    maxBound = let sz1 :: Int
    sz1 = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 in Integer -> IntN n
    forall (n :: Nat). Integer -> IntN n
    IntN (Integer -> IntN n) -> Integer -> IntN n
    forall a b. (a -> b) -> a -> b
    $ Integer
    2 Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Int
    sz1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1

    -- | 'Num' instance for 'WordN'
    instance (KnownNat n, BVIsNonZero n) => Num (WordN n) where
       + :: WordN n -> WordN n -> WordN n
    (+)         = String -> (SVal -> SVal -> SVal) -> WordN n -> WordN n -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2 String
    "(+)"    SVal -> SVal -> SVal
    svPlus
       (-)         = String -> (SVal -> SVal -> SVal) -> WordN n -> WordN n -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2 String
    "(*)"    SVal -> SVal -> SVal
    svMinus
       * :: WordN n -> WordN n -> WordN n
    (*)         = String -> (SVal -> SVal -> SVal) -> WordN n -> WordN n -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2 String
    "(*)"    SVal -> SVal -> SVal
    svTimes
       negate :: WordN n -> WordN n
    negate      = String -> (SVal -> SVal) -> WordN n -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal) -> bv n -> bv n
    lift1 String
    "signum" SVal -> SVal
    svUNeg
       abs :: WordN n -> WordN n
    abs         = String -> (SVal -> SVal) -> WordN n -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal) -> bv n -> bv n
    lift1 String
    "abs"    SVal -> SVal
    svAbs
       signum :: WordN n -> WordN n
    signum      = Integer -> WordN n
    forall (n :: Nat). Integer -> WordN n
    WordN (Integer -> WordN n) -> (WordN n -> Integer) -> WordN n -> WordN n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer
    forall a. Num a => a -> a
    signum   (Integer -> Integer) -> (WordN n -> Integer) -> WordN n -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WordN n -> Integer
    forall a. Integral a => a -> Integer
    toInteger
       fromInteger :: Integer -> WordN n
    fromInteger = Integer -> WordN n
    forall (n :: Nat). Integer -> WordN n
    WordN (Integer -> WordN n) -> (Integer -> Integer) -> Integer -> WordN n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Integer -> Integer
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe Integer -> Integer)
    -> (Integer -> Maybe Integer) -> Integer -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SVal -> Maybe Integer
    svAsInteger (SVal -> Maybe Integer)
    -> (Integer -> SVal) -> Integer -> Maybe Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Kind -> Integer -> SVal
    svInteger (WordN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (WordN n
    forall a. HasCallStack => a
    undefined :: WordN n))

    -- | 'Num' instance for 'IntN'
    instance (KnownNat n, BVIsNonZero n) => Num (IntN n) where
       + :: IntN n -> IntN n -> IntN n
    (+)         = String -> (SVal -> SVal -> SVal) -> IntN n -> IntN n -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2 String
    "(+)"    SVal -> SVal -> SVal
    svPlus
       (-)         = String -> (SVal -> SVal -> SVal) -> IntN n -> IntN n -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2 String
    "(*)"    SVal -> SVal -> SVal
    svMinus
       * :: IntN n -> IntN n -> IntN n
    (*)         = String -> (SVal -> SVal -> SVal) -> IntN n -> IntN n -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2 String
    "(*)"    SVal -> SVal -> SVal
    svTimes
       negate :: IntN n -> IntN n
    negate      = String -> (SVal -> SVal) -> IntN n -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal) -> bv n -> bv n
    lift1 String
    "signum" SVal -> SVal
    svUNeg
       abs :: IntN n -> IntN n
    abs         = String -> (SVal -> SVal) -> IntN n -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal) -> bv n -> bv n
    lift1 String
    "abs"    SVal -> SVal
    svAbs
       signum :: IntN n -> IntN n
    signum      = Integer -> IntN n
    forall (n :: Nat). Integer -> IntN n
    IntN (Integer -> IntN n) -> (IntN n -> Integer) -> IntN n -> IntN n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer
    forall a. Num a => a -> a
    signum   (Integer -> Integer) -> (IntN n -> Integer) -> IntN n -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IntN n -> Integer
    forall a. Integral a => a -> Integer
    toInteger
       fromInteger :: Integer -> IntN n
    fromInteger = Integer -> IntN n
    forall (n :: Nat). Integer -> IntN n
    IntN (Integer -> IntN n) -> (Integer -> Integer) -> Integer -> IntN n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Integer -> Integer
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe Integer -> Integer)
    -> (Integer -> Maybe Integer) -> Integer -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SVal -> Maybe Integer
    svAsInteger (SVal -> Maybe Integer)
    -> (Integer -> SVal) -> Integer -> Maybe Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Kind -> Integer -> SVal
    svInteger (IntN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (IntN n
    forall a. HasCallStack => a
    undefined :: IntN n))

    -- | 'Enum' instance for 'WordN'
    instance (KnownNat n, BVIsNonZero n) => Enum (WordN n) where
       toEnum :: Int -> WordN n
    toEnum   = Integer -> WordN n
    forall a. Num a => Integer -> a
    fromInteger  (Integer -> WordN n) -> (Int -> Integer) -> Int -> WordN n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger
       fromEnum :: WordN n -> Int
    fromEnum = Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Integer -> Int) -> (WordN n -> Integer) -> WordN n -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WordN n -> Integer
    forall a. Integral a => a -> Integer
    toInteger

    -- | 'Enum' instance for 'IntN'
    instance (KnownNat n, BVIsNonZero n) => Enum (IntN n) where
       toEnum :: Int -> IntN n
    toEnum   = Integer -> IntN n
    forall a. Num a => Integer -> a
    fromInteger  (Integer -> IntN n) -> (Int -> Integer) -> Int -> IntN n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger
       fromEnum :: IntN n -> Int
    fromEnum = Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Integer -> Int) -> (IntN n -> Integer) -> IntN n -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IntN n -> Integer
    forall a. Integral a => a -> Integer
    toInteger

    -- | 'Real' instance for 'WordN'
    instance (KnownNat n, BVIsNonZero n) => Real (WordN n) where
       toRational :: WordN n -> Rational
    toRational (WordN Integer
    x) = Integer -> Rational
    forall a. Real a => a -> Rational
    toRational Integer
    x

    -- | 'Real' instance for 'IntN'
    instance (KnownNat n, BVIsNonZero n) => Real (IntN n) where
       toRational :: IntN n -> Rational
    toRational (IntN Integer
    x) = Integer -> Rational
    forall a. Real a => a -> Rational
    toRational Integer
    x

    -- | 'Integral' instance for 'WordN'
    instance (KnownNat n, BVIsNonZero n) => Integral (WordN n) where
       toInteger :: WordN n -> Integer
    toInteger (WordN Integer
    x)           = Integer
    x
       quotRem :: WordN n -> WordN n -> (WordN n, WordN n)
    quotRem   (WordN Integer
    x) (WordN Integer
    y) = let (Integer
    q, Integer
    r) = Integer -> Integer -> (Integer, Integer)
    forall a. Integral a => a -> a -> (a, a)
    quotRem Integer
    x Integer
    y in (Integer -> WordN n
    forall (n :: Nat). Integer -> WordN n
    WordN Integer
    q, Integer -> WordN n
    forall (n :: Nat). Integer -> WordN n
    WordN Integer
    r)

    -- | 'Integral' instance for 'IntN'
    instance (KnownNat n, BVIsNonZero n) => Integral (IntN n) where
       toInteger :: IntN n -> Integer
    toInteger (IntN Integer
    x)          = Integer
    x
       quotRem :: IntN n -> IntN n -> (IntN n, IntN n)
    quotRem   (IntN Integer
    x) (IntN Integer
    y) = let (Integer
    q, Integer
    r) = Integer -> Integer -> (Integer, Integer)
    forall a. Integral a => a -> a -> (a, a)
    quotRem Integer
    x Integer
    y in (Integer -> IntN n
    forall (n :: Nat). Integer -> IntN n
    IntN Integer
    q, Integer -> IntN n
    forall (n :: Nat). Integer -> IntN n
    IntN Integer
    r)

    --  'Bits' instance for 'WordN'
    instance (KnownNat n, BVIsNonZero n) => Bits (WordN n) where
       .&. :: WordN n -> WordN n -> WordN n
    (.&.)        = String -> (SVal -> SVal -> SVal) -> WordN n -> WordN n -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2   String
    "(.&.)"      SVal -> SVal -> SVal
    svAnd
       .|. :: WordN n -> WordN n -> WordN n
    (.|.)        = String -> (SVal -> SVal -> SVal) -> WordN n -> WordN n -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2   String
    "(.|.)"      SVal -> SVal -> SVal
    svOr
       xor :: WordN n -> WordN n -> WordN n
    xor          = String -> (SVal -> SVal -> SVal) -> WordN n -> WordN n -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2   String
    "xor"        SVal -> SVal -> SVal
    svXOr
       complement :: WordN n -> WordN n
    complement   = String -> (SVal -> SVal) -> WordN n -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal) -> bv n -> bv n
    lift1   String
    "complement" SVal -> SVal
    svNot
       shiftL :: WordN n -> Int -> WordN n
    shiftL       = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I  String
    "shiftL"     SVal -> Int -> SVal
    svShl
       shiftR :: WordN n -> Int -> WordN n
    shiftR       = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I  String
    "shiftR"     SVal -> Int -> SVal
    svShr
       rotateL :: WordN n -> Int -> WordN n
    rotateL      = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I  String
    "rotateL"    SVal -> Int -> SVal
    svRol
       rotateR :: WordN n -> Int -> WordN n
    rotateR      = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I  String
    "rotateR"    SVal -> Int -> SVal
    svRor
       testBit :: WordN n -> Int -> Bool
    testBit      = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> Bool
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool
    lift2IB String
    "svTestBit"  SVal -> Int -> SVal
    svTestBit
       bitSizeMaybe :: WordN n -> Maybe Int
    bitSizeMaybe = Int -> Maybe Int
    forall a. a -> Maybe a
    Just (Int -> Maybe Int) -> (WordN n -> Int) -> WordN n -> Maybe Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> WordN n -> Int
    forall a b. a -> b -> a
    const (Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n))
       bitSize :: WordN n -> Int
    bitSize WordN n
    _    = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n)
       isSigned :: WordN n -> Bool
    isSigned     = Kind -> Bool
    forall a. HasKind a => a -> Bool
    hasSign (Kind -> Bool) -> (WordN n -> Kind) -> WordN n -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WordN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf
       bit :: Int -> WordN n
    bit Int
    i        = WordN n
    1 WordN n -> Int -> WordN n
    forall a. Bits a => a -> Int -> a
    `shiftL` Int
    i
       popCount :: WordN n -> Int
    popCount     = Int -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Int) -> (WordN n -> Int) -> WordN n -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Int
    forall a. Bits a => a -> Int
    popCount (Integer -> Int) -> (WordN n -> Integer) -> WordN n -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WordN n -> Integer
    forall a. Integral a => a -> Integer
    toInteger

    --  'Bits' instance for 'IntN'
    instance (KnownNat n, BVIsNonZero n) => Bits (IntN n) where
       .&. :: IntN n -> IntN n -> IntN n
    (.&.)        = String -> (SVal -> SVal -> SVal) -> IntN n -> IntN n -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2   String
    "(.&.)"      SVal -> SVal -> SVal
    svAnd
       .|. :: IntN n -> IntN n -> IntN n
    (.|.)        = String -> (SVal -> SVal -> SVal) -> IntN n -> IntN n -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2   String
    "(.|.)"      SVal -> SVal -> SVal
    svOr
       xor :: IntN n -> IntN n -> IntN n
    xor          = String -> (SVal -> SVal -> SVal) -> IntN n -> IntN n -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2   String
    "xor"        SVal -> SVal -> SVal
    svXOr
       complement :: IntN n -> IntN n
    complement   = String -> (SVal -> SVal) -> IntN n -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal) -> bv n -> bv n
    lift1   String
    "complement" SVal -> SVal
    svNot
       shiftL :: IntN n -> Int -> IntN n
    shiftL       = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I  String
    "shiftL"     SVal -> Int -> SVal
    svShl
       shiftR :: IntN n -> Int -> IntN n
    shiftR       = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I  String
    "shiftR"     SVal -> Int -> SVal
    svShr
       rotateL :: IntN n -> Int -> IntN n
    rotateL      = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I  String
    "rotateL"    SVal -> Int -> SVal
    svRol
       rotateR :: IntN n -> Int -> IntN n
    rotateR      = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I  String
    "rotateR"    SVal -> Int -> SVal
    svRor
       testBit :: IntN n -> Int -> Bool
    testBit      = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> Bool
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool
    lift2IB String
    "svTestBit"  SVal -> Int -> SVal
    svTestBit
       bitSizeMaybe :: IntN n -> Maybe Int
    bitSizeMaybe = Int -> Maybe Int
    forall a. a -> Maybe a
    Just (Int -> Maybe Int) -> (IntN n -> Int) -> IntN n -> Maybe Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> IntN n -> Int
    forall a b. a -> b -> a
    const (Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n))
       bitSize :: IntN n -> Int
    bitSize IntN n
    _    = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n)
       isSigned :: IntN n -> Bool
    isSigned     = Kind -> Bool
    forall a. HasKind a => a -> Bool
    hasSign (Kind -> Bool) -> (IntN n -> Kind) -> IntN n -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IntN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf
       bit :: Int -> IntN n
    bit Int
    i        = IntN n
    1 IntN n -> Int -> IntN n
    forall a. Bits a => a -> Int -> a
    `shiftL` Int
    i
       popCount :: IntN n -> Int
    popCount     = Int -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Int) -> (IntN n -> Int) -> IntN n -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Int
    forall a. Bits a => a -> Int
    popCount (Integer -> Int) -> (IntN n -> Integer) -> IntN n -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IntN n -> Integer
    forall a. Integral a => a -> Integer
    toInteger

    -- | 'SIntegral' instance for 'WordN'
    instance (KnownNat n, BVIsNonZero n) => SIntegral (WordN n)

    -- | 'SIntegral' instance for 'IntN'
    instance (KnownNat n, BVIsNonZero n) => SIntegral (IntN n)

    -- | 'SDivisible' instance for 'WordN'
    instance (KnownNat n, BVIsNonZero n) => SDivisible (WordN n) where
      sQuotRem :: WordN n -> WordN n -> (WordN n, WordN n)
    sQuotRem WordN n
    x WordN n
    0 = (WordN n
    0, WordN n
    x)
      sQuotRem WordN n
    x WordN n
    y = WordN n
    x WordN n -> WordN n -> (WordN n, WordN n)
    forall a. Integral a => a -> a -> (a, a)
    `quotRem` WordN n
    y
      sDivMod :: WordN n -> WordN n -> (WordN n, WordN n)
    sDivMod  WordN n
    x WordN n
    0 = (WordN n
    0, WordN n
    x)
      sDivMod  WordN n
    x WordN n
    y = WordN n
    x WordN n -> WordN n -> (WordN n, WordN n)
    forall a. Integral a => a -> a -> (a, a)
    `divMod` WordN n
    y

    -- | 'SDivisible' instance for 'IntN'
    instance (KnownNat n, BVIsNonZero n) => SDivisible (IntN n) where
      sQuotRem :: IntN n -> IntN n -> (IntN n, IntN n)
    sQuotRem IntN n
    x IntN n
    0 = (IntN n
    0, IntN n
    x)
      sQuotRem IntN n
    x IntN n
    y = IntN n
    x IntN n -> IntN n -> (IntN n, IntN n)
    forall a. Integral a => a -> a -> (a, a)
    `quotRem` IntN n
    y
      sDivMod :: IntN n -> IntN n -> (IntN n, IntN n)
    sDivMod  IntN n
    x IntN n
    0 = (IntN n
    0, IntN n
    x)
      sDivMod  IntN n
    x IntN n
    y = IntN n
    x IntN n -> IntN n -> (IntN n, IntN n)
    forall a. Integral a => a -> a -> (a, a)
    `divMod` IntN n
    y

    -- | 'SDivisible' instance for 'SWord'
    instance (KnownNat n, BVIsNonZero n) => SDivisible (SWord n) where
      sQuotRem :: SWord n -> SWord n -> (SWord n, SWord n)
    sQuotRem = SWord n -> SWord n -> (SWord n, SWord n)
    forall a. (Eq a, SymVal a) => SBV a -> SBV a -> (SBV a, SBV a)
    liftQRem
      sDivMod :: SWord n -> SWord n -> (SWord n, SWord n)
    sDivMod  = SWord n -> SWord n -> (SWord n, SWord n)
    forall a.
    (Ord a, SymVal a, Num a, SDivisible (SBV a)) =>
    SBV a -> SBV a -> (SBV a, SBV a)
    liftDMod

    -- | 'SDivisible' instance for 'SInt'
    instance (KnownNat n, BVIsNonZero n) => SDivisible (SInt n) where
      sQuotRem :: SInt n -> SInt n -> (SInt n, SInt n)
    sQuotRem = SInt n -> SInt n -> (SInt n, SInt n)
    forall a. (Eq a, SymVal a) => SBV a -> SBV a -> (SBV a, SBV a)
    liftQRem
      sDivMod :: SInt n -> SInt n -> (SInt n, SInt n)
    sDivMod  = SInt n -> SInt n -> (SInt n, SInt n)
    forall a.
    (Ord a, SymVal a, Num a, SDivisible (SBV a)) =>
    SBV a -> SBV a -> (SBV a, SBV a)
    liftDMod

    -- | 'SFiniteBits' instance for 'WordN'
    instance (KnownNat n, BVIsNonZero n) => SFiniteBits (WordN n) where
       sFiniteBitSize :: SBV (WordN n) -> Int
    sFiniteBitSize SBV (WordN n)
    _ = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n)

    -- | 'SFiniteBits' instance for 'IntN'
    instance (KnownNat n, BVIsNonZero n) => SFiniteBits (IntN n) where
       sFiniteBitSize :: SBV (IntN n) -> Int
    sFiniteBitSize SBV (IntN n)
    _ = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n)

    -- | Constructing models for 'WordN'
    instance (KnownNat n, BVIsNonZero n) => SatModel (WordN n) where
      parseCVs :: [CV] -> Maybe (WordN n, [CV])
    parseCVs = Kind -> [CV] -> Maybe (WordN n, [CV])
    forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
    genParse (WordN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (WordN n
    forall a. HasCallStack => a
    undefined :: WordN n))

    -- | Constructing models for 'IntN'
    instance (KnownNat n, BVIsNonZero n) => SatModel (IntN n) where
      parseCVs :: [CV] -> Maybe (IntN n, [CV])
    parseCVs = Kind -> [CV] -> Maybe (IntN n, [CV])
    forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
    genParse (IntN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (IntN n
    forall a. HasCallStack => a
    undefined :: IntN n))

    -- | Optimizing 'WordN'
    instance (KnownNat n, BVIsNonZero n) => Metric (WordN n)

    -- | Optimizing 'IntN'
    instance (KnownNat n, BVIsNonZero n) => Metric (IntN n) where
      type MetricSpace (IntN n) = WordN n
      toMetricSpace :: SBV (IntN n) -> SBV (MetricSpace (IntN n))
    toMetricSpace    SBV (IntN n)
    x        = SBV (IntN n) -> SBV (WordN n)
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    sFromIntegral SBV (IntN n)
    x SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
    forall a. Num a => a -> a -> a
    + SBV (WordN n)
    2 SBV (WordN n) -> Int -> SBV (WordN n)
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ (Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1)
      fromMetricSpace :: SBV (MetricSpace (IntN n)) -> SBV (IntN n)
    fromMetricSpace  SBV (MetricSpace (IntN n))
    x        = SBV (WordN n) -> SBV (IntN n)
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    sFromIntegral SBV (MetricSpace (IntN n))
    SBV (WordN n)
    x SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)
    forall a. Num a => a -> a -> a
    - SBV (IntN n)
    2 SBV (IntN n) -> Int -> SBV (IntN n)
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ (Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1)

    -- | Generalization of 'Data.SBV.sWord'
    sWord :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => String -> m (SWord n)
    sWord :: forall (n :: Nat) (m :: * -> *).
    (KnownNat n, BVIsNonZero n, MonadSymbolic m) =>
    String -> m (SWord n)
    sWord = String -> m (SBV (WordN n))
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    forall (m :: * -> *).
    MonadSymbolic m =>
    String -> m (SBV (WordN n))
    symbolic

    -- | Generalization of 'Data.SBV.sWord_'
    sWord_ :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => m (SWord n)
    sWord_ :: forall (n :: Nat) (m :: * -> *).
    (KnownNat n, BVIsNonZero n, MonadSymbolic m) =>
    m (SWord n)
    sWord_ = m (SBV (WordN n))
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    forall (m :: * -> *). MonadSymbolic m => m (SBV (WordN n))
    free_

    -- | Generalization of 'Data.SBV.sWord64s'
    sWords :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => [String] -> m [SWord n]
    sWords :: forall (n :: Nat) (m :: * -> *).
    (KnownNat n, BVIsNonZero n, MonadSymbolic m) =>
    [String] -> m [SWord n]
    sWords = [String] -> m [SBV (WordN n)]
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    [String] -> m [SBV a]
    forall (m :: * -> *).
    MonadSymbolic m =>
    [String] -> m [SBV (WordN n)]
    symbolics

    -- | Generalization of 'Data.SBV.sInt'
    sInt :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => String -> m (SInt n)
    sInt :: forall (n :: Nat) (m :: * -> *).
    (KnownNat n, BVIsNonZero n, MonadSymbolic m) =>
    String -> m (SInt n)
    sInt = String -> m (SBV (IntN n))
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    forall (m :: * -> *). MonadSymbolic m => String -> m (SBV (IntN n))
    symbolic

    -- | Generalization of 'Data.SBV.sInt_'
    sInt_ :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => m (SInt n)
    sInt_ :: forall (n :: Nat) (m :: * -> *).
    (KnownNat n, BVIsNonZero n, MonadSymbolic m) =>
    m (SInt n)
    sInt_ = m (SBV (IntN n))
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    forall (m :: * -> *). MonadSymbolic m => m (SBV (IntN n))
    free_

    -- | Generalization of 'Data.SBV.sInts'
    sInts :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => [String] -> m [SInt n]
    sInts :: forall (n :: Nat) (m :: * -> *).
    (KnownNat n, BVIsNonZero n, MonadSymbolic m) =>
    [String] -> m [SInt n]
    sInts = [String] -> m [SBV (IntN n)]
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    [String] -> m [SBV a]
    forall (m :: * -> *).
    MonadSymbolic m =>
    [String] -> m [SBV (IntN n)]
    symbolics

    -- | Extract a portion of bits to form a smaller bit-vector.
    bvExtract :: forall i j n bv proxy. ( KnownNat n, BVIsNonZero n, SymVal (bv n)
                                        , KnownNat i
                                        , KnownNat j
                                        , i + 1 <= n
                                        , j <= i
                                        , BVIsNonZero (i - j + 1)
                                        ) => proxy i                -- ^ @i@: Start position, numbered from @n-1@ to @0@
                                          -> proxy j                -- ^ @j@: End position, numbered from @n-1@ to @0@, @j <= i@ must hold
                                          -> SBV (bv n)             -- ^ Input bit vector of size @n@
                                          -> SBV (bv (i - j + 1))   -- ^ Output is of size @i - j + 1@
    bvExtract :: forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract proxy i
    start proxy j
    end = SVal -> SBV (bv ((i - j) + 1))
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (bv ((i - j) + 1)))
    -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Int -> SVal -> SVal
    svExtract Int
    i Int
    j (SVal -> SVal) -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBV (bv n) -> SVal
    forall a. SBV a -> SVal
    unSBV
       where i :: Int
    i  = Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (proxy i -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy i
    start)
             j :: Int
    j  = Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (proxy j -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy j
    end)

    -- | Join two bitvectors.
    (#) :: ( KnownNat n, BVIsNonZero n, SymVal (bv n)
           , KnownNat m, BVIsNonZero m, SymVal (bv m)
           ) => SBV (bv n)                     -- ^ First input, of size @n@, becomes the left side
             -> SBV (bv m)                     -- ^ Second input, of size @m@, becomes the right side
             -> SBV (bv (n + m))               -- ^ Concatenation, of size @n+m@
    SBV (bv n)
    n # :: forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
    (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
     BVIsNonZero m, SymVal (bv m)) =>
    SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
    # SBV (bv m)
    m = SVal -> SBV (bv (n + m))
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (bv (n + m))) -> SVal -> SBV (bv (n + m))
    forall a b. (a -> b) -> a -> b
    $ SVal -> SVal -> SVal
    svJoin (SBV (bv n) -> SVal
    forall a. SBV a -> SVal
    unSBV SBV (bv n)
    n) (SBV (bv m) -> SVal
    forall a. SBV a -> SVal
    unSBV SBV (bv m)
    m)
    infixr 5 #

    -- | Zero extend a bit-vector.
    zeroExtend :: forall n m bv. ( KnownNat n, BVIsNonZero n, SymVal (bv n)
                                 , KnownNat m, BVIsNonZero m, SymVal (bv m)
                                 , n + 1 <= m
                                 , SIntegral   (bv (m - n))
                                 , BVIsNonZero (m - n)
                                 ) => SBV (bv n)    -- ^ Input, of size @n@
                                   -> SBV (bv m)    -- ^ Output, of size @m@. @n < m@ must hold
    zeroExtend :: forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
     BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m - n)),
     BVIsNonZero (m - n)) =>
    SBV (bv n) -> SBV (bv m)
    zeroExtend SBV (bv n)
    n = SVal -> SBV (bv m)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (bv m)) -> SVal -> SBV (bv m)
    forall a b. (a -> b) -> a -> b
    $ Int -> SVal -> SVal
    svZeroExtend Int
    i (SBV (bv n) -> SVal
    forall a. SBV a -> SVal
    unSBV SBV (bv n)
    n)
      where nv :: Int
    nv = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n)
            mv :: Int
    mv = Proxy m -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @m)
            i :: Int
    i  = Int -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int
    mv Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    nv)

    -- | Sign extend a bit-vector.
    signExtend :: forall n m bv. ( KnownNat n, BVIsNonZero n, SymVal (bv n)
                                 , KnownNat m, BVIsNonZero m, SymVal (bv m)
                                 , n + 1 <= m
                                 , SFiniteBits (bv n)
                                 , SIntegral   (bv (m - n))
                                 , BVIsNonZero (m - n)
                                 ) => SBV (bv n)  -- ^ Input, of size @n@
                                   -> SBV (bv m)  -- ^ Output, of size @m@. @n < m@ must hold
    signExtend :: forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
    (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
     BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n),
     SIntegral (bv (m - n)), BVIsNonZero (m - n)) =>
    SBV (bv n) -> SBV (bv m)
    signExtend SBV (bv n)
    n = SVal -> SBV (bv m)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (bv m)) -> SVal -> SBV (bv m)
    forall a b. (a -> b) -> a -> b
    $ Int -> SVal -> SVal
    svSignExtend Int
    i (SBV (bv n) -> SVal
    forall a. SBV a -> SVal
    unSBV SBV (bv n)
    n)
      where nv :: Int
    nv = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n)
            mv :: Int
    mv = Proxy m -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @m)
            i :: Int
    i  = Int -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int
    mv Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    nv)

    -- | Drop bits from the top of a bit-vector.
    bvDrop :: forall i n m bv proxy. ( KnownNat n, BVIsNonZero n
                                     , KnownNat i
                                     , i + 1 <= n
                                     , i + m - n <= 0
                                     , BVIsNonZero (n - i)
                                     ) => proxy i                    -- ^ @i@: Number of bits to drop. @i < n@ must hold.
                                       -> SBV (bv n)                 -- ^ Input, of size @n@
                                       -> SBV (bv m)                 -- ^ Output, of size @m@. @m = n - i@ holds.
    bvDrop :: forall (i :: Nat) (n :: Nat) (m :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, BVIsNonZero n, KnownNat i, (i + 1) <= n,
     ((i + m) - n) <= 0, BVIsNonZero (n - i)) =>
    proxy i -> SBV (bv n) -> SBV (bv m)
    bvDrop proxy i
    i = SVal -> SBV (bv m)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (bv m))
    -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SBV (bv m)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Int -> SVal -> SVal
    svExtract Int
    start Int
    0 (SVal -> SVal) -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBV (bv n) -> SVal
    forall a. SBV a -> SVal
    unSBV
      where nv :: Int
    nv    = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n)
            start :: Int
    start = Int
    nv Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (proxy i -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy i
    i) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1

    -- | Take bits from the top of a bit-vector.
    bvTake :: forall i n bv proxy. ( KnownNat n, BVIsNonZero n
                                   , KnownNat i, BVIsNonZero i
                                   , i <= n
                                   ) => proxy i                  -- ^ @i@: Number of bits to take. @0 < i <= n@ must hold.
                                     -> SBV (bv n)               -- ^ Input, of size @n@
                                     -> SBV (bv i)               -- ^ Output, of size @i@
    bvTake :: forall (i :: Nat) (n :: Nat) (bv :: Nat -> *) (proxy :: Nat -> *).
    (KnownNat n, BVIsNonZero n, KnownNat i, BVIsNonZero i, i <= n) =>
    proxy i -> SBV (bv n) -> SBV (bv i)
    bvTake proxy i
    i = SVal -> SBV (bv i)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (bv i))
    -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SBV (bv i)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Int -> SVal -> SVal
    svExtract Int
    start Int
    end (SVal -> SVal) -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBV (bv n) -> SVal
    forall a. SBV a -> SVal
    unSBV
      where nv :: Int
    nv    = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n)
            start :: Int
    start = Int
    nv Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1
            end :: Int
    end   = Int
    start Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (proxy i -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy i
    i) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1

    -- | Quickcheck instance for WordN
    instance KnownNat n => Arbitrary (WordN n) where
      arbitrary :: Gen (WordN n)
    arbitrary = (Integer -> WordN n
    forall (n :: Nat). Integer -> WordN n
    WordN (Integer -> WordN n) -> (Integer -> Integer) -> Integer -> WordN n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer
    norm (Integer -> Integer) -> (Integer -> Integer) -> Integer -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer
    forall a. Num a => a -> a
    abs) (Integer -> WordN n) -> Gen Integer -> Gen (WordN n)
    forall a b. (a -> b) -> Gen a -> Gen b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` Gen Integer
    forall a. Arbitrary a => Gen a
    arbitrary
        where sz :: Int
    sz = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n)

              norm :: Integer -> Integer
    norm Integer
    v | Int
    sz Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 = Integer
    0
                     | Bool
    True    = Integer
    v Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. (((Integer
    1 :: Integer) Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftL` Int
    sz) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1)

    -- | Quickcheck instance for IntN
    instance KnownNat n => Arbitrary (IntN n) where
      arbitrary :: Gen (IntN n)
    arbitrary = (Integer -> IntN n
    forall (n :: Nat). Integer -> IntN n
    IntN (Integer -> IntN n) -> (Integer -> Integer) -> Integer -> IntN n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer
    norm) (Integer -> IntN n) -> Gen Integer -> Gen (IntN n)
    forall a b. (a -> b) -> Gen a -> Gen b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` Gen Integer
    forall a. Arbitrary a => Gen a
    arbitrary
        where sz :: Int
    sz = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n)

              norm :: Integer -> Integer
    norm Integer
    v | Int
    sz Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 = Integer
    0
                     | Bool
    True  = let rg :: Integer
    rg = Integer
    2 Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ (Int
    sz Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1)
                               in case Integer -> Integer -> (Integer, Integer)
    forall a. Integral a => a -> a -> (a, a)
    divMod Integer
    v Integer
    rg of
                                         (Integer
    a, Integer
    b) | Integer -> Bool
    forall a. Integral a => a -> Bool
    even Integer
    a -> Integer
    b
                                         (Integer
    _, Integer
    b)          -> Integer
    b Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    rg