    {-# LANGUAGE BangPatterns #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE DeriveAnyClass #-}
    {-# LANGUAGE DeriveGeneric #-}
    {-# LANGUAGE DeriveLift #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE MultiWayIf #-}
    {-# LANGUAGE PatternSynonyms #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TemplateHaskell #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE TypeOperators #-}

    {-|
    Module      : Data.BitVector.Sized.Internal
    Copyright   : (c) Galois Inc. 2018
    License     : BSD-3
    Maintainer  : benselfridge@galois.com
    Stability   : experimental
    Portability : portable

    Internal hidden module containing all definitions for the 'BV' type.
    -}

    module Data.BitVector.Sized.Internal where

    import Data.BitVector.Sized.Panic (panic)

    -- Qualified imports
    import qualified Data.Bits                  as B
    import qualified Data.Bits.Bitwise          as B
    import qualified Data.ByteString            as BS
    import qualified Numeric                    as N
    import qualified Data.Parameterized.NatRepr as P
    import qualified Prelude

    -- Unqualified imports
    import Control.DeepSeq (NFData)
    import Data.Char (intToDigit)
    import Data.List (genericLength)
    import Data.Int (Int8, Int16, Int32, Int64)
    import Data.Kind (Type)
    import Data.Maybe (fromJust)
    import Data.Word (Word8, Word16, Word32, Word64)
    import Data.Parameterized ( NatRepr
                              , mkNatRepr
                              , natValue
                              , intValue
                              , addNat
                              , ShowF
                              , EqF(..)
                              , Hashable(..)
                              , Some(..)
                              , Pair(..)
                              )
    import GHC.Generics (Generic)
    import GHC.TypeLits (Nat, type(+), type(<=))
    import Language.Haskell.TH.Lift (Lift)
    import Numeric.Natural (Natural)
    import Prelude hiding (abs, or, and, negate, concat, signum)
    import System.Random.Stateful

    ----------------------------------------
    -- Utility functions

    -- | Check that a 'NatRepr' is representable as an 'Int'.
    checkNatRepr :: NatRepr w -> a -> a
    checkNatRepr :: forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr = Natural -> a -> a
    forall a. Natural -> a -> a
    checkNatural (Natural -> a -> a)
    -> (NatRepr w -> Natural) -> NatRepr w -> a -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue

    -- | Check that a 'Natural' is representable as an 'Int'.
    checkNatural :: Natural -> a -> a
    checkNatural :: forall a. Natural -> a -> a
    checkNatural Natural
    n a
    a = if Natural
    n Natural -> Natural -> Bool
    forall a. Ord a => a -> a -> Bool
    > (Int -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int
    forall a. Bounded a => a
    maxBound :: Int) :: Natural)
      then String -> [String] -> a
    forall a. String -> [String] -> a
    panic String
    "Data.BitVector.Sized.Internal.checkNatural"
           [Natural -> String
    forall a. Show a => a -> String
    show Natural
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " not representable as Int"]
      else a
    a

    -- | Unsafe coercion from @Natural@ to @Int@.  We mostly use this to
    --   interact with operations from "Data.Bits".  This should only be
    --   called when we already know the input @Natural@ is small enough,
    --   e.g., because we previously called @checkNatural@.
    fromNatural :: Natural -> Int
    fromNatural :: Natural -> Int
    fromNatural = Natural -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral

    ----------------------------------------
    -- BitVector data type definitions

    -- | Bitvector datatype, parameterized by width.
    newtype BV (w :: Nat) :: Type where
      -- | We store the value as an 'Integer' rather than a 'Natural',
      -- since many of the operations on bitvectors rely on a two's
      -- complement representation. However, an invariant on the value is
      -- that it must always be positive.
      --
      -- Secondly, we maintain the invariant that any constructed BV value
      -- has a width whose value is representable in a Haskell @Int@.
      BV :: Integer -> BV w

      deriving ( (forall x. BV w -> Rep (BV w) x)
    -> (forall x. Rep (BV w) x -> BV w) -> Generic (BV w)
    forall (w :: Natural) x. Rep (BV w) x -> BV w
    forall (w :: Natural) x. BV w -> Rep (BV w) x
    forall x. Rep (BV w) x -> BV w
    forall x. BV w -> Rep (BV w) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall (w :: Natural) x. BV w -> Rep (BV w) x
    from :: forall x. BV w -> Rep (BV w) x
    $cto :: forall (w :: Natural) x. Rep (BV w) x -> BV w
    to :: forall x. Rep (BV w) x -> BV w
    Generic
               , BV w -> ()
    (BV w -> ()) -> NFData (BV w)
    forall (w :: Natural). BV w -> ()
    forall a. (a -> ()) -> NFData a
    $crnf :: forall (w :: Natural). BV w -> ()
    rnf :: BV w -> ()
    NFData
               , Int -> BV w -> String -> String
    [BV w] -> String -> String
    BV w -> String
    (Int -> BV w -> String -> String)
    -> (BV w -> String) -> ([BV w] -> String -> String) -> Show (BV w)
    forall (w :: Natural). Int -> BV w -> String -> String
    forall (w :: Natural). [BV w] -> String -> String
    forall (w :: Natural). BV w -> String
    forall a.
    (Int -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    $cshowsPrec :: forall (w :: Natural). Int -> BV w -> String -> String
    showsPrec :: Int -> BV w -> String -> String
    $cshow :: forall (w :: Natural). BV w -> String
    show :: BV w -> String
    $cshowList :: forall (w :: Natural). [BV w] -> String -> String
    showList :: [BV w] -> String -> String
    Show
               , ReadPrec [BV w]
    ReadPrec (BV w)
    Int -> ReadS (BV w)
    ReadS [BV w]
    (Int -> ReadS (BV w))
    -> ReadS [BV w]
    -> ReadPrec (BV w)
    -> ReadPrec [BV w]
    -> Read (BV w)
    forall (w :: Natural). ReadPrec [BV w]
    forall (w :: Natural). ReadPrec (BV w)
    forall (w :: Natural). Int -> ReadS (BV w)
    forall (w :: Natural). ReadS [BV w]
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    $creadsPrec :: forall (w :: Natural). Int -> ReadS (BV w)
    readsPrec :: Int -> ReadS (BV w)
    $creadList :: forall (w :: Natural). ReadS [BV w]
    readList :: ReadS [BV w]
    $creadPrec :: forall (w :: Natural). ReadPrec (BV w)
    readPrec :: ReadPrec (BV w)
    $creadListPrec :: forall (w :: Natural). ReadPrec [BV w]
    readListPrec :: ReadPrec [BV w]
    Read
               , BV w -> BV w -> Bool
    (BV w -> BV w -> Bool) -> (BV w -> BV w -> Bool) -> Eq (BV w)
    forall (w :: Natural). BV w -> BV w -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall (w :: Natural). BV w -> BV w -> Bool
    == :: BV w -> BV w -> Bool
    $c/= :: forall (w :: Natural). BV w -> BV w -> Bool
    /= :: BV w -> BV w -> Bool
    Eq
               , Eq (BV w)
    Eq (BV w)
    -> (BV w -> BV w -> Ordering)
    -> (BV w -> BV w -> Bool)
    -> (BV w -> BV w -> Bool)
    -> (BV w -> BV w -> Bool)
    -> (BV w -> BV w -> Bool)
    -> (BV w -> BV w -> BV w)
    -> (BV w -> BV w -> BV w)
    -> Ord (BV w)
    BV w -> BV w -> Bool
    BV w -> BV w -> Ordering
    BV w -> BV w -> BV w
    forall (w :: Natural). Eq (BV w)
    forall (w :: Natural). BV w -> BV w -> Bool
    forall (w :: Natural). BV w -> BV w -> Ordering
    forall (w :: Natural). BV w -> BV w -> BV w
    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 (w :: Natural). BV w -> BV w -> Ordering
    compare :: BV w -> BV w -> Ordering
    $c< :: forall (w :: Natural). BV w -> BV w -> Bool
    < :: BV w -> BV w -> Bool
    $c<= :: forall (w :: Natural). BV w -> BV w -> Bool
    <= :: BV w -> BV w -> Bool
    $c> :: forall (w :: Natural). BV w -> BV w -> Bool
    > :: BV w -> BV w -> Bool
    $c>= :: forall (w :: Natural). BV w -> BV w -> Bool
    >= :: BV w -> BV w -> Bool
    $cmax :: forall (w :: Natural). BV w -> BV w -> BV w
    max :: BV w -> BV w -> BV w
    $cmin :: forall (w :: Natural). BV w -> BV w -> BV w
    min :: BV w -> BV w -> BV w
    Ord -- ^ Uses an unsigned ordering, but 'ule' and 'ult' are
                     -- preferred. We provide this instance to allow the use of 'BV'
                     -- in situations where an arbitrary ordering is required (e.g.,
                     -- as the keys in a map)
               , (forall (m :: * -> *). Quote m => BV w -> m Exp)
    -> (forall (m :: * -> *). Quote m => BV w -> Code m (BV w))
    -> Lift (BV w)
    forall (w :: Natural) (m :: * -> *). Quote m => BV w -> m Exp
    forall (w :: Natural) (m :: * -> *).
    Quote m =>
    BV w -> Code m (BV w)
    forall t.
    (forall (m :: * -> *). Quote m => t -> m Exp)
    -> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
    forall (m :: * -> *). Quote m => BV w -> m Exp
    forall (m :: * -> *). Quote m => BV w -> Code m (BV w)
    $clift :: forall (w :: Natural) (m :: * -> *). Quote m => BV w -> m Exp
    lift :: forall (m :: * -> *). Quote m => BV w -> m Exp
    $cliftTyped :: forall (w :: Natural) (m :: * -> *).
    Quote m =>
    BV w -> Code m (BV w)
    liftTyped :: forall (m :: * -> *). Quote m => BV w -> Code m (BV w)
    Lift)

    instance ShowF BV

    instance EqF BV where
      BV Integer
    bv eqF :: forall (w :: Natural). BV w -> BV w -> Bool
    `eqF` BV Integer
    bv' = Integer
    bv Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    bv'

    instance Hashable (BV w) where
      hashWithSalt :: Int -> BV w -> Int
    hashWithSalt Int
    salt (BV Integer
    i) = Int -> Integer -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt Int
    salt Integer
    i

    ----------------------------------------
    -- BV construction
    -- | Internal function for masking the input integer *without*
    -- checking that the width is representable as an 'Int'. We use this
    -- instead of 'mkBV' whenever we already have some guarantee that the
    -- width is legal.
    mkBV' :: NatRepr w -> Integer -> BV w
    mkBV' :: forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w Integer
    x = Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (NatRepr w -> Integer -> Integer
    forall (w :: Natural). NatRepr w -> Integer -> Integer
    P.toUnsigned NatRepr w
    w Integer
    x)

    -- | Construct a bitvector with a particular width, where the width is
    -- provided as an explicit `NatRepr` argument. The input 'Integer',
    -- whether positive or negative, is silently truncated to fit into the
    -- number of bits demanded by the return type. The width cannot be
    -- arbitrarily large; it must be representable as an 'Int'.
    --
    -- >>> mkBV (knownNat @4) 10
    -- BV 10
    -- >>> mkBV (knownNat @2) 10
    -- BV 2
    -- >>> mkBV (knownNat @4) (-2)
    -- BV 14
    mkBV :: NatRepr w
         -- ^ Desired bitvector width
         -> Integer
         -- ^ Integer value to truncate to bitvector width
         -> BV w
    mkBV :: forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV NatRepr w
    w Integer
    x = NatRepr w -> BV w -> BV w
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr NatRepr w
    w (BV w -> BV w) -> BV w -> BV w
    forall a b. (a -> b) -> a -> b
    $ NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w Integer
    x

    -- | Return 'Nothing' if the unsigned 'Integer' does not fit in the
    -- required number of bits, otherwise return the input.
    checkUnsigned :: NatRepr w
                  -> Integer
                  -> Maybe Integer
    checkUnsigned :: forall (w :: Natural). NatRepr w -> Integer -> Maybe Integer
    checkUnsigned NatRepr w
    w Integer
    i = if Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    0 Bool -> Bool -> Bool
    || Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > NatRepr w -> Integer
    forall (w :: Natural). NatRepr w -> Integer
    P.maxUnsigned NatRepr w
    w
      then Maybe Integer
    forall a. Maybe a
    Nothing
      else Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    i

    -- | Like 'mkBV', but returns 'Nothing' if unsigned input integer cannot be
    -- represented in @w@ bits.
    mkBVUnsigned :: NatRepr w
                 -- ^ Desired bitvector width
                 -> Integer
                 -- ^ Integer value
                 -> Maybe (BV w)
    mkBVUnsigned :: forall (w :: Natural). NatRepr w -> Integer -> Maybe (BV w)
    mkBVUnsigned NatRepr w
    w Integer
    x = NatRepr w -> Maybe (BV w) -> Maybe (BV w)
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr NatRepr w
    w (Maybe (BV w) -> Maybe (BV w)) -> Maybe (BV w) -> Maybe (BV w)
    forall a b. (a -> b) -> a -> b
    $ Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Integer -> BV w) -> Maybe Integer -> Maybe (BV w)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NatRepr w -> Integer -> Maybe Integer
    forall (w :: Natural). NatRepr w -> Integer -> Maybe Integer
    checkUnsigned NatRepr w
    w Integer
    x

    -- | Return 'Nothing if the signed 'Integer' does not fit in the
    -- required number of bits, otherwise return an unsigned positive
    -- integer that fits in @w@ bits.
    signedToUnsigned :: 1 <= w => NatRepr w
                     -- ^ Width of output
                     -> Integer
                     -> Maybe Integer
    signedToUnsigned :: forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> Integer -> Maybe Integer
    signedToUnsigned NatRepr w
    w Integer
    i = if Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < NatRepr w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
    P.minSigned NatRepr w
    w Bool -> Bool -> Bool
    || Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > NatRepr w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
    P.maxSigned NatRepr w
    w
      then Maybe Integer
    forall a. Maybe a
    Nothing
      else Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
    forall a b. (a -> b) -> a -> b
    $ if Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    0 then Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + NatRepr w -> Integer
    forall (w :: Natural). NatRepr w -> Integer
    P.maxUnsigned NatRepr w
    w Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1 else Integer
    i

    -- | Like 'mkBV', but returns 'Nothing' if signed input integer cannot
    -- be represented in @w@ bits.
    mkBVSigned :: 1 <= w => NatRepr w
                  -- ^ Desired bitvector width
               -> Integer
               -- ^ Integer value
               -> Maybe (BV w)
    mkBVSigned :: forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> Integer -> Maybe (BV w)
    mkBVSigned NatRepr w
    w Integer
    x = NatRepr w -> Maybe (BV w) -> Maybe (BV w)
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr NatRepr w
    w (Maybe (BV w) -> Maybe (BV w)) -> Maybe (BV w) -> Maybe (BV w)
    forall a b. (a -> b) -> a -> b
    $ Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Integer -> BV w) -> Maybe Integer -> Maybe (BV w)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NatRepr w -> Integer -> Maybe Integer
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> Integer -> Maybe Integer
    signedToUnsigned NatRepr w
    w Integer
    x

    -- | The zero bitvector of any width.
    zero :: NatRepr w -> BV w
    zero :: forall (w :: Natural). NatRepr w -> BV w
    zero NatRepr w
    w = NatRepr w -> BV w -> BV w
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr NatRepr w
    w (BV w -> BV w) -> BV w -> BV w
    forall a b. (a -> b) -> a -> b
    $ Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV Integer
    0

    -- | The bitvector with value 1, of any positive width.
    one :: 1 <= w => NatRepr w -> BV w
    one :: forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
    one NatRepr w
    w = NatRepr w -> BV w -> BV w
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr NatRepr w
    w (BV w -> BV w) -> BV w -> BV w
    forall a b. (a -> b) -> a -> b
    $ Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV Integer
    1

    -- | The bitvector whose value is its own width, of any width.
    width :: NatRepr w -> BV w
    width :: forall (w :: Natural). NatRepr w -> BV w
    width NatRepr w
    w = NatRepr w -> BV w -> BV w
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr NatRepr w
    w (BV w -> BV w) -> BV w -> BV w
    forall a b. (a -> b) -> a -> b
    $ Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (NatRepr w -> Integer
    forall (w :: Natural). NatRepr w -> Integer
    intValue NatRepr w
    w)

    -- | The minimum unsigned value for bitvector with given width (always 0).
    minUnsigned :: NatRepr w -> BV w
    minUnsigned :: forall (w :: Natural). NatRepr w -> BV w
    minUnsigned NatRepr w
    w = NatRepr w -> BV w -> BV w
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr NatRepr w
    w (BV w -> BV w) -> BV w -> BV w
    forall a b. (a -> b) -> a -> b
    $ Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV Integer
    0

    -- | The maximum unsigned value for bitvector with given width.
    maxUnsigned :: NatRepr w -> BV w
    maxUnsigned :: forall (w :: Natural). NatRepr w -> BV w
    maxUnsigned NatRepr w
    w = NatRepr w -> BV w -> BV w
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr NatRepr w
    w (BV w -> BV w) -> BV w -> BV w
    forall a b. (a -> b) -> a -> b
    $ Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (NatRepr w -> Integer
    forall (w :: Natural). NatRepr w -> Integer
    P.maxUnsigned NatRepr w
    w)

    -- | The minimum value for bitvector in two's complement with given width.
    minSigned :: 1 <= w => NatRepr w -> BV w
    minSigned :: forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
    minSigned NatRepr w
    w = NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV NatRepr w
    w (NatRepr w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
    P.minSigned NatRepr w
    w)

    -- | The maximum value for bitvector in two's complement with given width.
    maxSigned :: 1 <= w => NatRepr w -> BV w
    maxSigned :: forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
    maxSigned NatRepr w
    w = NatRepr w -> BV w -> BV w
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr NatRepr w
    w (BV w -> BV w) -> BV w -> BV w
    forall a b. (a -> b) -> a -> b
    $ Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (NatRepr w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
    P.maxSigned NatRepr w
    w)

    -- | @unsignedClamp w i@ rounds @i@ to the nearest value between @0@
    -- and @2^w - 1@ (inclusive).
    unsignedClamp :: NatRepr w -> Integer -> BV w
    unsignedClamp :: forall (w :: Natural). NatRepr w -> Integer -> BV w
    unsignedClamp NatRepr w
    w Integer
    x = NatRepr w -> BV w -> BV w
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr NatRepr w
    w (BV w -> BV w) -> BV w -> BV w
    forall a b. (a -> b) -> a -> b
    $
      if | Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < NatRepr w -> Integer
    forall (w :: Natural). NatRepr w -> Integer
    P.minUnsigned NatRepr w
    w -> Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (NatRepr w -> Integer
    forall (w :: Natural). NatRepr w -> Integer
    P.minUnsigned NatRepr w
    w)
         | Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > NatRepr w -> Integer
    forall (w :: Natural). NatRepr w -> Integer
    P.maxUnsigned NatRepr w
    w -> Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (NatRepr w -> Integer
    forall (w :: Natural). NatRepr w -> Integer
    P.maxUnsigned NatRepr w
    w)
         | Bool
    otherwise -> Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV Integer
    x

    -- | @signedClamp w i@ rounds @i@ to the nearest value between
    -- @-2^(w-1)@ and @2^(w-1) - 1@ (inclusive).
    signedClamp :: 1 <= w => NatRepr w -> Integer -> BV w
    signedClamp :: forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> BV w
    signedClamp NatRepr w
    w Integer
    x = NatRepr w -> BV w -> BV w
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr NatRepr w
    w (BV w -> BV w) -> BV w -> BV w
    forall a b. (a -> b) -> a -> b
    $
      if | Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < NatRepr w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
    P.minSigned NatRepr w
    w -> NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w (NatRepr w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
    P.minSigned NatRepr w
    w)
         | Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > NatRepr w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
    P.maxSigned NatRepr w
    w -> Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (NatRepr w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
    P.maxSigned NatRepr w
    w)
         | Bool
    otherwise -> NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w Integer
    x

    ----------------------------------------
    -- Construction from fixed-width data types

    -- | Construct a 'BV' from a 'Bool'.
    bool :: Bool -> BV 1
    bool :: Bool -> BV 1
    bool Bool
    True = Integer -> BV 1
    forall (w :: Natural). Integer -> BV w
    BV Integer
    1
    bool Bool
    False = Integer -> BV 1
    forall (w :: Natural). Integer -> BV w
    BV Integer
    0

    -- | Construct a 'BV' from a 'Word8'.
    word8 :: Word8 -> BV 8
    word8 :: Word8 -> BV 8
    word8 = Integer -> BV 8
    forall (w :: Natural). Integer -> BV w
    BV (Integer -> BV 8) -> (Word8 -> Integer) -> Word8 -> BV 8
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word8 -> Integer
    forall a. Integral a => a -> Integer
    toInteger

    -- | Construct a 'BV' from a 'Word16'.
    word16 :: Word16 -> BV 16
    word16 :: Word16 -> BV 16
    word16 = Integer -> BV 16
    forall (w :: Natural). Integer -> BV w
    BV (Integer -> BV 16) -> (Word16 -> Integer) -> Word16 -> BV 16
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word16 -> Integer
    forall a. Integral a => a -> Integer
    toInteger

    -- | Construct a 'BV' from a 'Word32'.
    word32 :: Word32 -> BV 32
    word32 :: Word32 -> BV 32
    word32 = Integer -> BV 32
    forall (w :: Natural). Integer -> BV w
    BV (Integer -> BV 32) -> (Word32 -> Integer) -> Word32 -> BV 32
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word32 -> Integer
    forall a. Integral a => a -> Integer
    toInteger

    -- | Construct a 'BV' from a 'Word64'.
    word64 :: Word64 -> BV 64
    word64 :: Word64 -> BV 64
    word64 = Integer -> BV 64
    forall (w :: Natural). Integer -> BV w
    BV (Integer -> BV 64) -> (Word64 -> Integer) -> Word64 -> BV 64
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word64 -> Integer
    forall a. Integral a => a -> Integer
    toInteger

    -- | Construct a 'BV' from an 'Int8'.
    int8 :: Int8 -> BV 8
    int8 :: Int8 -> BV 8
    int8 = Word8 -> BV 8
    word8 (Word8 -> BV 8) -> (Int8 -> Word8) -> Int8 -> BV 8
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int8 -> Word8
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral :: Int8 -> Word8)

    -- | Construct a 'BV' from an 'Int16'.
    int16 :: Int16 -> BV 16
    int16 :: Int16 -> BV 16
    int16 = Word16 -> BV 16
    word16 (Word16 -> BV 16) -> (Int16 -> Word16) -> Int16 -> BV 16
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int16 -> Word16
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral :: Int16 -> Word16)

    -- | Construct a 'BV' from an 'Int32'.
    int32 :: Int32 -> BV 32
    int32 :: Int32 -> BV 32
    int32 = Word32 -> BV 32
    word32 (Word32 -> BV 32) -> (Int32 -> Word32) -> Int32 -> BV 32
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int32 -> Word32
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral :: Int32 -> Word32)

    -- | Construct a 'BV' from an 'Int64'.
    int64 :: Int64 -> BV 64
    int64 :: Int64 -> BV 64
    int64 = Word64 -> BV 64
    word64 (Word64 -> BV 64) -> (Int64 -> Word64) -> Int64 -> BV 64
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int64 -> Word64
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral :: Int64 -> Word64)

    -- | Construct a 'BV' from a list of bits, in big endian order (bits
    -- with lower value index in the list are mapped to higher order bits
    -- in the output bitvector). Return the resulting 'BV' along with its
    -- width.
    --
    -- >>> case bitsBE [True, False] of p -> (fstPair p, sndPair p)
    -- (2,BV 2)
    bitsBE :: [Bool] -> Pair NatRepr BV
    bitsBE :: [Bool] -> Pair NatRepr BV
    bitsBE [Bool]
    bs = case Natural -> Some NatRepr
    mkNatRepr (Integer -> Natural
    forall a. Num a => Integer -> a
    fromInteger ([Bool] -> Integer
    forall i a. Num i => [a] -> i
    genericLength [Bool]
    bs)) of
      Some NatRepr x
    w -> NatRepr x -> Pair NatRepr BV -> Pair NatRepr BV
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr NatRepr x
    w (Pair NatRepr BV -> Pair NatRepr BV)
    -> Pair NatRepr BV -> Pair NatRepr BV
    forall a b. (a -> b) -> a -> b
    $ NatRepr x -> BV x -> Pair NatRepr BV
    forall {k} (a :: k -> *) (tp :: k) (b :: k -> *).
    a tp -> b tp -> Pair a b
    Pair NatRepr x
    w (Integer -> BV x
    forall (w :: Natural). Integer -> BV w
    BV ([Bool] -> Integer
    forall b. Bits b => [Bool] -> b
    B.fromListBE [Bool]
    bs))

    -- | Construct a 'BV' from a list of bits, in little endian order
    -- (bits with lower value index in the list are mapped to lower order
    -- bits in the output bitvector). Return the resulting 'BV' along
    -- with its width.
    --
    -- >>> case bitsLE [True, False] of p -> (fstPair p, sndPair p)
    -- (2,BV 1)
    bitsLE :: [Bool] -> Pair NatRepr BV
    bitsLE :: [Bool] -> Pair NatRepr BV
    bitsLE [Bool]
    bs = case Natural -> Some NatRepr
    mkNatRepr (Integer -> Natural
    forall a. Num a => Integer -> a
    fromInteger ([Bool] -> Integer
    forall i a. Num i => [a] -> i
    genericLength [Bool]
    bs)) of
      Some NatRepr x
    w -> NatRepr x -> Pair NatRepr BV -> Pair NatRepr BV
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr NatRepr x
    w (Pair NatRepr BV -> Pair NatRepr BV)
    -> Pair NatRepr BV -> Pair NatRepr BV
    forall a b. (a -> b) -> a -> b
    $ NatRepr x -> BV x -> Pair NatRepr BV
    forall {k} (a :: k -> *) (tp :: k) (b :: k -> *).
    a tp -> b tp -> Pair a b
    Pair NatRepr x
    w (Integer -> BV x
    forall (w :: Natural). Integer -> BV w
    BV ([Bool] -> Integer
    forall b. Bits b => [Bool] -> b
    B.fromListLE [Bool]
    bs))

    -- | Convert a 'ByteString' (big-endian) of length @n@ to an 'Integer'
    -- with @8*n@ bits. This function uses a balanced binary fold to
    -- achieve /O(n log n)/ total memory allocation and run-time, in
    -- contrast to the /O(n^2)/ that would be required by a naive
    -- left-fold.
    bytestringToIntegerBE :: BS.ByteString -> Integer
    bytestringToIntegerBE :: ByteString -> Integer
    bytestringToIntegerBE ByteString
    bs
      | Int
    l Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 = Integer
    0
      | Int
    l Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1 = Word8 -> Integer
    forall a. Integral a => a -> Integer
    toInteger (HasCallStack => ByteString -> Word8
    ByteString -> Word8
    BS.head ByteString
    bs)
      | Bool
    otherwise = Integer
    x1 Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `B.shiftL` (Int
    l2 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    * Int
    8) Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    B..|. Integer
    x2
      where
        l :: Int
    l = ByteString -> Int
    BS.length ByteString
    bs
        l1 :: Int
    l1 = Int
    l Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `div` Int
    2
        l2 :: Int
    l2 = Int
    l Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    l1
        (ByteString
    bs1, ByteString
    bs2) = Int -> ByteString -> (ByteString, ByteString)
    BS.splitAt Int
    l1 ByteString
    bs
        x1 :: Integer
    x1 = ByteString -> Integer
    bytestringToIntegerBE ByteString
    bs1
        x2 :: Integer
    x2 = ByteString -> Integer
    bytestringToIntegerBE ByteString
    bs2

    bytestringToIntegerLE :: BS.ByteString -> Integer
    bytestringToIntegerLE :: ByteString -> Integer
    bytestringToIntegerLE ByteString
    bs
      | Int
    l Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 = Integer
    0
      | Int
    l Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1 = Word8 -> Integer
    forall a. Integral a => a -> Integer
    toInteger (HasCallStack => ByteString -> Word8
    ByteString -> Word8
    BS.head ByteString
    bs)
      | Bool
    otherwise = Integer
    x2 Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `B.shiftL` (Int
    l1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    * Int
    8) Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    B..|. Integer
    x1
      where
        l :: Int
    l = ByteString -> Int
    BS.length ByteString
    bs
        l1 :: Int
    l1 = Int
    l Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `div` Int
    2
        (ByteString
    bs1, ByteString
    bs2) = Int -> ByteString -> (ByteString, ByteString)
    BS.splitAt Int
    l1 ByteString
    bs
        x1 :: Integer
    x1 = ByteString -> Integer
    bytestringToIntegerLE ByteString
    bs1
        x2 :: Integer
    x2 = ByteString -> Integer
    bytestringToIntegerLE ByteString
    bs2

    -- | Construct a 'BV' from a big-endian bytestring.
    --
    -- >>> case bytestringBE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p)
    -- (24,BV 257)
    bytestringBE :: BS.ByteString -> Pair NatRepr BV
    bytestringBE :: ByteString -> Pair NatRepr BV
    bytestringBE ByteString
    bs = case Natural -> Some NatRepr
    mkNatRepr (Natural
    8Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    *Int -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (ByteString -> Int
    BS.length ByteString
    bs)) of
      Some NatRepr x
    w -> NatRepr x -> Pair NatRepr BV -> Pair NatRepr BV
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr NatRepr x
    w (Pair NatRepr BV -> Pair NatRepr BV)
    -> Pair NatRepr BV -> Pair NatRepr BV
    forall a b. (a -> b) -> a -> b
    $ NatRepr x -> BV x -> Pair NatRepr BV
    forall {k} (a :: k -> *) (tp :: k) (b :: k -> *).
    a tp -> b tp -> Pair a b
    Pair NatRepr x
    w (Integer -> BV x
    forall (w :: Natural). Integer -> BV w
    BV (ByteString -> Integer
    bytestringToIntegerBE ByteString
    bs))

    -- | Construct a 'BV' from a little-endian bytestring.
    --
    -- >>> case bytestringLE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p)
    -- (24,BV 65792)
    bytestringLE :: BS.ByteString -> Pair NatRepr BV
    bytestringLE :: ByteString -> Pair NatRepr BV
    bytestringLE ByteString
    bs = case Natural -> Some NatRepr
    mkNatRepr (Natural
    8Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    *Int -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (ByteString -> Int
    BS.length ByteString
    bs)) of
      Some NatRepr x
    w -> NatRepr x -> Pair NatRepr BV -> Pair NatRepr BV
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr NatRepr x
    w (Pair NatRepr BV -> Pair NatRepr BV)
    -> Pair NatRepr BV -> Pair NatRepr BV
    forall a b. (a -> b) -> a -> b
    $ NatRepr x -> BV x -> Pair NatRepr BV
    forall {k} (a :: k -> *) (tp :: k) (b :: k -> *).
    a tp -> b tp -> Pair a b
    Pair NatRepr x
    w (Integer -> BV x
    forall (w :: Natural). Integer -> BV w
    BV (ByteString -> Integer
    bytestringToIntegerLE ByteString
    bs))

    -- | Construct a 'BV' from a list of bytes, in big endian order (bytes
    -- with lower value index in the list are mapped to higher order bytes
    -- in the output bitvector).
    --
    -- >>> case bytesBE [0, 1, 1] of p -> (fstPair p, sndPair p)
    -- (24,BV 257)
    bytesBE :: [Word8] -> Pair NatRepr BV
    bytesBE :: [Word8] -> Pair NatRepr BV
    bytesBE = ByteString -> Pair NatRepr BV
    bytestringBE (ByteString -> Pair NatRepr BV)
    -> ([Word8] -> ByteString) -> [Word8] -> Pair NatRepr BV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Word8] -> ByteString
    BS.pack

    -- | Construct a 'BV' from a list of bytes, in little endian order
    -- (bytes with lower value index in the list are mapped to lower
    -- order bytes in the output bitvector).
    --
    -- >>> case bytesLE [0, 1, 1] of p -> (fstPair p, sndPair p)
    -- (24,BV 65792)
    bytesLE :: [Word8] -> Pair NatRepr BV
    bytesLE :: [Word8] -> Pair NatRepr BV
    bytesLE = ByteString -> Pair NatRepr BV
    bytestringLE (ByteString -> Pair NatRepr BV)
    -> ([Word8] -> ByteString) -> [Word8] -> Pair NatRepr BV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Word8] -> ByteString
    BS.pack

    ----------------------------------------
    -- BitVector -> Integer functions

    -- | Unsigned interpretation of a bitvector as a positive Integer.
    asUnsigned :: BV w -> Integer
    asUnsigned :: forall (w :: Natural). BV w -> Integer
    asUnsigned (BV Integer
    x) = Integer
    x

    -- | Signed interpretation of a bitvector as an Integer.
    asSigned :: (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned :: forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w (BV Integer
    x) =
      -- NB, fromNatural is OK here because we maintain the invariant that
      --  any existing BV value has a representable width
      let wInt :: Int
    wInt = Natural -> Int
    fromNatural (NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w) in
      if Integer -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    B.testBit Integer
    x (Int
    wInt Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1)
      then Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Int -> Integer
    forall a. Bits a => Int -> a
    B.bit Int
    wInt
      else Integer
    x

    -- | Unsigned interpretation of a bitvector as a Natural.
    asNatural :: BV w -> Natural
    asNatural :: forall (w :: Natural). BV w -> Natural
    asNatural = (Integer -> Natural
    forall a. Num a => Integer -> a
    fromInteger :: Integer -> Natural) (Integer -> Natural) -> (BV w -> Integer) -> BV w -> Natural
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    asUnsigned

    -- | Convert a bitvector to a list of bits, in big endian order
    -- (higher order bits in the bitvector are mapped to lower indices in
    -- the output list).
    --
    -- >>> asBitsBE (knownNat @5) (mkBV knownNat 0b1101)
    -- [False,True,True,False,True]
    asBitsBE :: NatRepr w -> BV w -> [Bool]
    asBitsBE :: forall (w :: Natural). NatRepr w -> BV w -> [Bool]
    asBitsBE NatRepr w
    w BV w
    bv = [ Natural -> BV w -> Bool
    forall (w :: Natural). Natural -> BV w -> Bool
    testBit' Natural
    i BV w
    bv | Natural
    i <- Integer -> Natural
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Natural) -> [Integer] -> [Natural]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Integer
    wi Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1, Integer
    wi Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    2 .. Integer
    0] ]
      where wi :: Integer
    wi = NatRepr w -> Integer
    forall (w :: Natural). NatRepr w -> Integer
    intValue NatRepr w
    w

    -- | Convert a bitvector to a list of bits, in little endian order
    -- (lower order bits in the bitvector are mapped to lower indices in
    -- the output list).
    --
    -- >>> asBitsLE (knownNat @5) (mkBV knownNat 0b1101)
    -- [True,False,True,True,False]
    asBitsLE :: NatRepr w -> BV w -> [Bool]
    asBitsLE :: forall (w :: Natural). NatRepr w -> BV w -> [Bool]
    asBitsLE NatRepr w
    w BV w
    bv = [ Natural -> BV w -> Bool
    forall (w :: Natural). Natural -> BV w -> Bool
    testBit' Natural
    i BV w
    bv | Natural
    i <- Integer -> Natural
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Natural) -> [Integer] -> [Natural]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Integer
    0 .. Integer
    wi Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1] ]
      where wi :: Integer
    wi = NatRepr w -> Integer
    forall (w :: Natural). NatRepr w -> Integer
    intValue NatRepr w
    w

    integerToBytesBE :: Natural
                     -- ^ number of bytes
                     -> Integer
                     -> [Word8]
    integerToBytesBE :: Natural -> Integer -> [Word8]
    integerToBytesBE Natural
    n Integer
    x =
      [ Integer -> Word8
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Integer
    x Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `B.shiftR` (Int
    8Int -> Int -> Int
    forall a. Num a => a -> a -> a
    *Int
    ix)) | Int
    ix <- [Int
    niInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1, Int
    niInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    2 .. Int
    0] ]
      where ni :: Int
    ni = Natural -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Natural
    n

    integerToBytesLE :: Natural
                     -- ^ number of bytes
                     -> Integer
                     -> [Word8]
    integerToBytesLE :: Natural -> Integer -> [Word8]
    integerToBytesLE Natural
    n Integer
    x =
      [ Integer -> Word8
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Integer
    x Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `B.shiftR` (Int
    8Int -> Int -> Int
    forall a. Num a => a -> a -> a
    *Int
    ix)) | Int
    ix <- [Int
    0 .. Int
    niInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1] ]
      where ni :: Int
    ni = Natural -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Natural
    n

    -- | Convert a bitvector to a list of bytes, in big endian order
    -- (higher order bytes in the bitvector are mapped to lower indices in
    -- the output list). Return 'Nothing' if the width is not a multiple
    -- of 8.
    --
    -- >>> asBytesBE (knownNat @32) (mkBV knownNat 0xaabbccdd)
    -- Just [170,187,204,221]
    asBytesBE :: NatRepr w -> BV w -> Maybe [Word8]
    asBytesBE :: forall (w :: Natural). NatRepr w -> BV w -> Maybe [Word8]
    asBytesBE NatRepr w
    w (BV Integer
    x)
      | NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w Natural -> Natural -> Natural
    forall a. Integral a => a -> a -> a
    `mod` Natural
    8 Natural -> Natural -> Bool
    forall a. Eq a => a -> a -> Bool
    == Natural
    0 = [Word8] -> Maybe [Word8]
    forall a. a -> Maybe a
    Just ([Word8] -> Maybe [Word8]) -> [Word8] -> Maybe [Word8]
    forall a b. (a -> b) -> a -> b
    $ Natural -> Integer -> [Word8]
    integerToBytesBE (NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w Natural -> Natural -> Natural
    forall a. Integral a => a -> a -> a
    `div` Natural
    8) Integer
    x
      | Bool
    otherwise = Maybe [Word8]
    forall a. Maybe a
    Nothing

    -- | Convert a bitvector to a list of bytes, in little endian order
    -- (lower order bytes in the bitvector are mapped to lower indices in
    -- the output list). Return 'Nothing' if the width is not a multiple
    -- of 8.
    --
    -- >>> asBytesLE (knownNat @32) (mkBV knownNat 0xaabbccdd)
    -- Just [221,204,187,170]
    asBytesLE :: NatRepr w -> BV w -> Maybe [Word8]
    asBytesLE :: forall (w :: Natural). NatRepr w -> BV w -> Maybe [Word8]
    asBytesLE NatRepr w
    w (BV Integer
    x)
      | NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w Natural -> Natural -> Natural
    forall a. Integral a => a -> a -> a
    `mod` Natural
    8 Natural -> Natural -> Bool
    forall a. Eq a => a -> a -> Bool
    == Natural
    0 = [Word8] -> Maybe [Word8]
    forall a. a -> Maybe a
    Just ([Word8] -> Maybe [Word8]) -> [Word8] -> Maybe [Word8]
    forall a b. (a -> b) -> a -> b
    $ Natural -> Integer -> [Word8]
    integerToBytesLE (NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w Natural -> Natural -> Natural
    forall a. Integral a => a -> a -> a
    `div` Natural
    8) Integer
    x
      | Bool
    otherwise = Maybe [Word8]
    forall a. Maybe a
    Nothing

    -- | 'asBytesBE', but for bytestrings.
    asBytestringBE :: NatRepr w -> BV w -> Maybe BS.ByteString
    asBytestringBE :: forall (w :: Natural). NatRepr w -> BV w -> Maybe ByteString
    asBytestringBE NatRepr w
    w BV w
    bv = [Word8] -> ByteString
    BS.pack ([Word8] -> ByteString) -> Maybe [Word8] -> Maybe ByteString
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NatRepr w -> BV w -> Maybe [Word8]
    forall (w :: Natural). NatRepr w -> BV w -> Maybe [Word8]
    asBytesBE NatRepr w
    w BV w
    bv

    -- | 'asBytesLE', but for bytestrings.
    asBytestringLE :: NatRepr w -> BV w -> Maybe BS.ByteString
    asBytestringLE :: forall (w :: Natural). NatRepr w -> BV w -> Maybe ByteString
    asBytestringLE NatRepr w
    w BV w
    bv = [Word8] -> ByteString
    BS.pack ([Word8] -> ByteString) -> Maybe [Word8] -> Maybe ByteString
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NatRepr w -> BV w -> Maybe [Word8]
    forall (w :: Natural). NatRepr w -> BV w -> Maybe [Word8]
    asBytesLE NatRepr w
    w BV w
    bv

    ----------------------------------------
    -- BV w operations (fixed width)

    -- | Bitwise and.
    and :: BV w -> BV w -> BV w
    and :: forall (w :: Natural). BV w -> BV w -> BV w
    and (BV Integer
    x) (BV Integer
    y) = Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Integer
    x Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    B..&. Integer
    y)

    -- | Bitwise or.
    or :: BV w -> BV w -> BV w
    or :: forall (w :: Natural). BV w -> BV w -> BV w
    or (BV Integer
    x) (BV Integer
    y) = Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Integer
    x Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    B..|. Integer
    y)

    -- | Bitwise xor.
    xor :: BV w -> BV w -> BV w
    xor :: forall (w :: Natural). BV w -> BV w -> BV w
    xor (BV Integer
    x) (BV Integer
    y) = Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Integer
    x Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    `B.xor` Integer
    y)

    -- | Bitwise complement (flip every bit).
    complement :: NatRepr w -> BV w -> BV w
    complement :: forall (w :: Natural). NatRepr w -> BV w -> BV w
    complement NatRepr w
    w (BV Integer
    x) = NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w (Integer -> Integer
    forall a. Bits a => a -> a
    B.complement Integer
    x)

    -- | Clamp shift amounts to the word width and
    --   coerce to an @Int@
    shiftAmount :: NatRepr w -> Natural -> Int
    shiftAmount :: forall (w :: Natural). NatRepr w -> Natural -> Int
    shiftAmount NatRepr w
    w Natural
    shf = Natural -> Int
    fromNatural (Natural -> Natural -> Natural
    forall a. Ord a => a -> a -> a
    min (NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w) Natural
    shf)

    -- | Left shift by positive 'Natural'.
    shl :: NatRepr w -> BV w -> Natural -> BV w
    shl :: forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
    shl NatRepr w
    w (BV Integer
    x) Natural
    shf = NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w (Integer
    x Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `B.shiftL` NatRepr w -> Natural -> Int
    forall (w :: Natural). NatRepr w -> Natural -> Int
    shiftAmount NatRepr w
    w Natural
    shf)

    -- | Right arithmetic shift by positive 'Natural'.
    ashr :: (1 <= w) => NatRepr w -> BV w -> Natural -> BV w
    ashr :: forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> Natural -> BV w
    ashr NatRepr w
    w BV w
    bv Natural
    shf = NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w (NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `B.shiftR` NatRepr w -> Natural -> Int
    forall (w :: Natural). NatRepr w -> Natural -> Int
    shiftAmount NatRepr w
    w Natural
    shf)

    -- | Right logical shift by positive 'Natural'.
    lshr :: NatRepr w -> BV w -> Natural -> BV w
    lshr :: forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
    lshr NatRepr w
    w (BV Integer
    x) Natural
    shf =
      -- Shift right (logical by default since the value is positive). No
      -- need to truncate bits, since the result is guaranteed to occupy
      -- no more bits than the input.
      Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Integer
    x Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `B.shiftR` NatRepr w -> Natural -> Int
    forall (w :: Natural). NatRepr w -> Natural -> Int
    shiftAmount NatRepr w
    w Natural
    shf)

    -- | Bitwise rotate left.
    rotateL :: NatRepr w -> BV w -> Natural -> BV w
    rotateL :: forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
    rotateL NatRepr w
    w BV w
    bv Natural
    rot' = BV w
    leftChunk BV w -> BV w -> BV w
    forall (w :: Natural). BV w -> BV w -> BV w
    `or` BV w
    rightChunk
      where rot :: Natural
    rot = if Natural
    wNatural Natural -> Natural -> Bool
    forall a. Eq a => a -> a -> Bool
    == Natural
    0 then Natural
    0 else Natural
    rot' Natural -> Natural -> Natural
    forall a. Integral a => a -> a -> a
    `mod` Natural
    wNatural
            leftChunk :: BV w
    leftChunk = NatRepr w -> BV w -> Natural -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
    shl NatRepr w
    w BV w
    bv Natural
    rot
            rightChunk :: BV w
    rightChunk = NatRepr w -> BV w -> Natural -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
    lshr NatRepr w
    w BV w
    bv (Natural
    wNatural Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    - Natural
    rot)
            wNatural :: Natural
    wNatural = NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w

    -- | Bitwise rotate right.
    rotateR :: NatRepr w -> BV w -> Natural -> BV w
    rotateR :: forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
    rotateR NatRepr w
    w BV w
    bv Natural
    rot' = BV w
    leftChunk BV w -> BV w -> BV w
    forall (w :: Natural). BV w -> BV w -> BV w
    `or` BV w
    rightChunk
      where rot :: Natural
    rot = if Natural
    wNatural Natural -> Natural -> Bool
    forall a. Eq a => a -> a -> Bool
    == Natural
    0 then Natural
    0 else Natural
    rot' Natural -> Natural -> Natural
    forall a. Integral a => a -> a -> a
    `mod` Natural
    wNatural
            rightChunk :: BV w
    rightChunk = NatRepr w -> BV w -> Natural -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
    lshr NatRepr w
    w BV w
    bv Natural
    rot
            leftChunk :: BV w
    leftChunk = NatRepr w -> BV w -> Natural -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
    shl NatRepr w
    w BV w
    bv (Natural
    wNatural Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    - Natural
    rot)
            wNatural :: Natural
    wNatural = NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w

    -- | The 'BV' that has a particular bit set, and is 0 everywhere
    -- else.
    bit :: ix+1 <= w
        => NatRepr w
        -- ^ Desired output width
        -> NatRepr ix
        -- ^ Index of bit to set
        -> BV w
    bit :: forall (ix :: Natural) (w :: Natural).
    ((ix + 1) <= w) =>
    NatRepr w -> NatRepr ix -> BV w
    bit NatRepr w
    w NatRepr ix
    ix =
      NatRepr w -> BV w -> BV w
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr NatRepr w
    w (BV w -> BV w) -> BV w -> BV w
    forall a b. (a -> b) -> a -> b
    $
        -- NB fromNatural is OK here because of the (ix+1<w) constraint
        Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Int -> Integer
    forall a. Bits a => Int -> a
    B.bit (Natural -> Int
    fromNatural (NatRepr ix -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr ix
    ix)))

    -- | Like 'bit', but without the requirement that the index bit refers
    -- to an actual bit in the output 'BV'. If it is out of range, just
    -- silently return the zero bitvector.
    bit' :: NatRepr w
         -- ^ Desired output width
         -> Natural
         -- ^ Index of bit to set
         -> BV w
    bit' :: forall (w :: Natural). NatRepr w -> Natural -> BV w
    bit' NatRepr w
    w Natural
    ix
      | Natural
    ix Natural -> Natural -> Bool
    forall a. Ord a => a -> a -> Bool
    < NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w = NatRepr w -> BV w -> BV w
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr NatRepr w
    w (BV w -> BV w) -> BV w -> BV w
    forall a b. (a -> b) -> a -> b
    $ NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w (Int -> Integer
    forall a. Bits a => Int -> a
    B.bit (Natural -> Int
    fromNatural Natural
    ix))
      | Bool
    otherwise = NatRepr w -> BV w
    forall (w :: Natural). NatRepr w -> BV w
    zero NatRepr w
    w

    -- | @setBit bv ix@ is the same as @or bv (bit knownNat ix)@.
    setBit :: ix+1 <= w
           => NatRepr ix
           -- ^ Index of bit to set
           -> BV w
           -- ^ Original bitvector
           -> BV w
    setBit :: forall (ix :: Natural) (w :: Natural).
    ((ix + 1) <= w) =>
    NatRepr ix -> BV w -> BV w
    setBit NatRepr ix
    ix BV w
    bv =
      -- NB, fromNatural is OK because of the (ix+1 <= w) constraint
      BV w -> BV w -> BV w
    forall (w :: Natural). BV w -> BV w -> BV w
    or BV w
    bv (Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Int -> Integer
    forall a. Bits a => Int -> a
    B.bit (Natural -> Int
    fromNatural (NatRepr ix -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr ix
    ix))))

    -- | Like 'setBit', but without the requirement that the index bit
    -- refers to an actual bit in the input 'BV'. If it is out of range,
    -- just silently return the original input.
    setBit' :: NatRepr w
            -- ^ Desired output width
            -> Natural
            -- ^ Index of bit to set
            -> BV w
            -- ^ Original bitvector
            -> BV w
    setBit' :: forall (w :: Natural). NatRepr w -> Natural -> BV w -> BV w
    setBit' NatRepr w
    w Natural
    ix BV w
    bv
      | Natural
    ix Natural -> Natural -> Bool
    forall a. Ord a => a -> a -> Bool
    < NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w = BV w -> BV w -> BV w
    forall (w :: Natural). BV w -> BV w -> BV w
    or BV w
    bv (Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Int -> Integer
    forall a. Bits a => Int -> a
    B.bit (Natural -> Int
    fromNatural Natural
    ix)))
      | Bool
    otherwise = BV w
    bv

    -- | @clearBit w bv ix@ is the same as @and bv (complement (bit w ix))@.
    clearBit :: ix+1 <= w
             => NatRepr w
             -- ^ Desired output width
             -> NatRepr ix
             -- ^ Index of bit to clear
             -> BV w
             -- ^ Original bitvector
             -> BV w
    clearBit :: forall (ix :: Natural) (w :: Natural).
    ((ix + 1) <= w) =>
    NatRepr w -> NatRepr ix -> BV w -> BV w
    clearBit NatRepr w
    w NatRepr ix
    ix BV w
    bv =
      -- NB, fromNatural is OK because of the (ix+1<=w) constraint
      BV w -> BV w -> BV w
    forall (w :: Natural). BV w -> BV w -> BV w
    and BV w
    bv (NatRepr w -> BV w -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> BV w
    complement NatRepr w
    w (Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Int -> Integer
    forall a. Bits a => Int -> a
    B.bit (Natural -> Int
    fromNatural (NatRepr ix -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr ix
    ix)))))

    -- | Like 'clearBit', but without the requirement that the index bit
    -- refers to an actual bit in the input 'BV'. If it is out of range,
    -- just silently return the original input.
    clearBit' :: NatRepr w
              -- ^ Desired output width
              -> Natural
              -- ^ Index of bit to clear
              -> BV w
              -- ^ Original bitvector
              -> BV w
    clearBit' :: forall (w :: Natural). NatRepr w -> Natural -> BV w -> BV w
    clearBit' NatRepr w
    w Natural
    ix BV w
    bv
      | Natural
    ix Natural -> Natural -> Bool
    forall a. Ord a => a -> a -> Bool
    < NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w = BV w -> BV w -> BV w
    forall (w :: Natural). BV w -> BV w -> BV w
    and BV w
    bv (NatRepr w -> BV w -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> BV w
    complement NatRepr w
    w (Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Int -> Integer
    forall a. Bits a => Int -> a
    B.bit (Natural -> Int
    fromNatural Natural
    ix))))
      | Bool
    otherwise = BV w
    bv

    -- | @complementBit bv ix@ is the same as @xor bv (bit knownNat ix)@.
    complementBit :: ix+1 <= w
                  => NatRepr ix
                  -- ^ Index of bit to flip
                  -> BV w
                  -- ^ Original bitvector
                  -> BV w
    complementBit :: forall (ix :: Natural) (w :: Natural).
    ((ix + 1) <= w) =>
    NatRepr ix -> BV w -> BV w
    complementBit NatRepr ix
    ix BV w
    bv =
      -- NB, fromNatural is OK because of (ix+1 <= w) constraint
      BV w -> BV w -> BV w
    forall (w :: Natural). BV w -> BV w -> BV w
    xor BV w
    bv (Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Int -> Integer
    forall a. Bits a => Int -> a
    B.bit (Natural -> Int
    fromNatural (NatRepr ix -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr ix
    ix))))

    -- | Like 'complementBit', but without the requirement that the index
    -- bit refers to an actual bit in the input 'BV'. If it is out of
    -- range, just silently return the original input.
    complementBit' :: NatRepr w
                   -- ^ Desired output width
                   -> Natural
                   -- ^ Index of bit to flip
                   -> BV w
                   -- ^ Original bitvector
                   -> BV w
    complementBit' :: forall (w :: Natural). NatRepr w -> Natural -> BV w -> BV w
    complementBit' NatRepr w
    w Natural
    ix BV w
    bv
      | Natural
    ix Natural -> Natural -> Bool
    forall a. Ord a => a -> a -> Bool
    < NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w = BV w -> BV w -> BV w
    forall (w :: Natural). BV w -> BV w -> BV w
    xor BV w
    bv (Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Int -> Integer
    forall a. Bits a => Int -> a
    B.bit (Natural -> Int
    fromNatural Natural
    ix)))
      | Bool
    otherwise = BV w
    bv

    -- | Test if a particular bit is set.
    testBit :: ix+1 <= w => NatRepr ix -> BV w -> Bool
    testBit :: forall (ix :: Natural) (w :: Natural).
    ((ix + 1) <= w) =>
    NatRepr ix -> BV w -> Bool
    testBit NatRepr ix
    ix (BV Integer
    x) = Integer -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    B.testBit Integer
    x (Natural -> Int
    fromNatural (NatRepr ix -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr ix
    ix))

    -- | Like 'testBit', but takes a 'Natural' for the bit index. If the
    -- index is out of bounds, return 'False'.
    testBit' :: Natural -> BV w -> Bool
    testBit' :: forall (w :: Natural). Natural -> BV w -> Bool
    testBit' Natural
    ix (BV Integer
    x)
      -- NB, If the index is larger than the maximum representable 'Int',
      -- this function should be 'False' by construction of 'BV'.
      | Natural
    ix Natural -> Natural -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int
    forall a. Bounded a => a
    maxBound :: Int) = Bool
    False
      | Bool
    otherwise = Integer -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    B.testBit Integer
    x (Natural -> Int
    fromNatural Natural
    ix)

    -- | Get the number of 1 bits in a 'BV'.
    popCount :: BV w -> BV w
    popCount :: forall (w :: Natural). BV w -> BV w
    popCount (BV Integer
    x) = Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Integer -> Int
    forall a. Bits a => a -> Int
    B.popCount Integer
    x))

    -- | Count trailing zeros in a 'BV'.
    ctz :: NatRepr w -> BV w -> BV w
    ctz :: forall (w :: Natural). NatRepr w -> BV w -> BV w
    ctz NatRepr w
    w (BV Integer
    x) = Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Integer -> Integer
    go Integer
    0)
      where go :: Integer -> Integer
    go !Integer
    i | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < NatRepr w -> Integer
    forall (w :: Natural). NatRepr w -> Integer
    intValue NatRepr w
    w Bool -> Bool -> Bool
    &&
                    Bool -> Bool
    not (Integer -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    B.testBit Integer
    x (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    i)) = Integer -> Integer
    go (Integer
    iInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    1)
                  | Bool
    otherwise = Integer
    i

    -- | Count leading zeros in a 'BV'.
    clz :: NatRepr w -> BV w -> BV w
    clz :: forall (w :: Natural). NatRepr w -> BV w -> BV w
    clz NatRepr w
    w (BV Integer
    x) = Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Integer -> Integer
    go Integer
    0)
     where go :: Integer -> Integer
    go !Integer
    i | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < NatRepr w -> Integer
    forall (w :: Natural). NatRepr w -> Integer
    intValue NatRepr w
    w Bool -> Bool -> Bool
    &&
                   Bool -> Bool
    not (Integer -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    B.testBit Integer
    x (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (NatRepr w -> Integer
    forall (w :: Natural). NatRepr w -> Integer
    intValue NatRepr w
    w Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1))) =
                     Integer -> Integer
    go (Integer
    iInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    1)
                 | Bool
    otherwise = Integer
    i

    -- | Truncate a bitvector to a particular width given at runtime,
    -- while keeping the type-level width constant.
    truncBits :: Natural -> BV w -> BV w
    truncBits :: forall (w :: Natural). Natural -> BV w -> BV w
    truncBits Natural
    b (BV Integer
    x) = Natural -> BV w -> BV w
    forall a. Natural -> a -> a
    checkNatural Natural
    b (BV w -> BV w) -> BV w -> BV w
    forall a b. (a -> b) -> a -> b
    $ Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Integer
    x Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    B..&. (Int -> Integer
    forall a. Bits a => Int -> a
    B.bit (Natural -> Int
    fromNatural Natural
    b) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1))

    ----------------------------------------
    -- BV w arithmetic operations (fixed width)

    -- | Bitvector add.
    add :: NatRepr w -> BV w -> BV w -> BV w
    add :: forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
    add NatRepr w
    w (BV Integer
    x) (BV Integer
    y) = NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w (Integer
    xInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    y)

    -- | Bitvector subtract.
    sub :: NatRepr w -> BV w -> BV w -> BV w
    sub :: forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
    sub NatRepr w
    w (BV Integer
    x) (BV Integer
    y) = NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w (Integer
    xInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    y)

    -- | Bitvector multiply.
    mul :: NatRepr w -> BV w -> BV w -> BV w
    mul :: forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
    mul NatRepr w
    w (BV Integer
    x) (BV Integer
    y) = NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w (Integer
    xInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *Integer
    y)

    -- | Bitvector division (unsigned). Rounds to zero. Division by zero
    -- yields a runtime error.
    uquot :: BV w -> BV w -> BV w
    uquot :: forall (w :: Natural). BV w -> BV w -> BV w
    uquot (BV Integer
    x) (BV Integer
    y) = Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `quot` Integer
    y)

    -- | Bitvector remainder after division (unsigned), when rounded to
    -- zero. Division by zero yields a runtime error.
    urem :: BV w -> BV w -> BV w
    urem :: forall (w :: Natural). BV w -> BV w -> BV w
    urem (BV Integer
    x) (BV Integer
    y) = Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `rem` Integer
    y)

    -- | 'uquot' and 'urem' returned as a pair.
    uquotRem :: BV w -> BV w -> (BV w, BV w)
    uquotRem :: forall (w :: Natural). BV w -> BV w -> (BV w, BV w)
    uquotRem BV w
    bv1 BV w
    bv2 = (BV w -> BV w -> BV w
    forall (w :: Natural). BV w -> BV w -> BV w
    uquot BV w
    bv1 BV w
    bv2, BV w -> BV w -> BV w
    forall (w :: Natural). BV w -> BV w -> BV w
    urem BV w
    bv1 BV w
    bv2)

    -- | Bitvector division (signed). Rounds to zero. Division by zero
    -- yields a runtime error.
    squot :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
    squot :: forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> BV w -> BV w
    squot NatRepr w
    w BV w
    bv1 BV w
    bv2 = NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w (Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `quot` Integer
    y)
      where x :: Integer
    x = NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv1
            y :: Integer
    y = NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv2

    -- | Bitvector remainder after division (signed), when rounded to
    -- zero. Division by zero yields a runtime error.
    srem :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
    srem :: forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> BV w -> BV w
    srem NatRepr w
    w BV w
    bv1 BV w
    bv2 = NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w (Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `rem` Integer
    y)
      where x :: Integer
    x = NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv1
            y :: Integer
    y = NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv2

    -- | 'squot' and 'srem' returned as a pair.
    squotRem :: (1 <= w) => NatRepr w -> BV w -> BV w -> (BV w, BV w)
    squotRem :: forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> BV w -> (BV w, BV w)
    squotRem NatRepr w
    w BV w
    bv1 BV w
    bv2 = (NatRepr w -> BV w -> BV w -> BV w
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> BV w -> BV w
    squot NatRepr w
    w BV w
    bv1 BV w
    bv2, NatRepr w -> BV w -> BV w -> BV w
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> BV w -> BV w
    srem NatRepr w
    w BV w
    bv1 BV w
    bv2)

    -- | Bitvector division (signed). Rounds to negative infinity. Division
    -- by zero yields a runtime error.
    sdiv :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
    sdiv :: forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> BV w -> BV w
    sdiv NatRepr w
    w BV w
    bv1 BV w
    bv2 = NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w (Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    y)
      where x :: Integer
    x = NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv1
            y :: Integer
    y = NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv2

    -- | Bitvector remainder after division (signed), when rounded to
    -- negative infinity. Division by zero yields a runtime error.
    smod :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
    smod :: forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> BV w -> BV w
    smod NatRepr w
    w BV w
    bv1 BV w
    bv2 = NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w (Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    y)
      where x :: Integer
    x = NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv1
            y :: Integer
    y = NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv2

    -- | 'sdiv' and 'smod' returned as a pair.
    sdivMod :: (1 <= w) => NatRepr w -> BV w -> BV w -> (BV w, BV w)
    sdivMod :: forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> BV w -> (BV w, BV w)
    sdivMod NatRepr w
    w BV w
    bv1 BV w
    bv2 = (NatRepr w -> BV w -> BV w -> BV w
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> BV w -> BV w
    sdiv NatRepr w
    w BV w
    bv1 BV w
    bv2, NatRepr w -> BV w -> BV w -> BV w
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> BV w -> BV w
    smod NatRepr w
    w BV w
    bv1 BV w
    bv2)

    -- | Bitvector absolute value.  Returns the 2's complement
    --   magnitude of the bitvector.
    abs :: (1 <= w) => NatRepr w -> BV w -> BV w
    abs :: forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> BV w
    abs NatRepr w
    w BV w
    bv = NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w (Integer -> Integer
    forall a. Num a => a -> a
    Prelude.abs (NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv))

    -- | 2's complement bitvector negation.
    negate :: NatRepr w -> BV w -> BV w
    negate :: forall (w :: Natural). NatRepr w -> BV w -> BV w
    negate NatRepr w
    w (BV Integer
    x) = NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w (-Integer
    x)

    -- | Get the sign bit as a 'BV'.
    signBit :: 1 <= w => NatRepr w -> BV w -> BV w
    signBit :: forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> BV w
    signBit NatRepr w
    w bv :: BV w
    bv@(BV Integer
    _) = NatRepr w -> BV w -> Natural -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
    lshr NatRepr w
    w BV w
    bv (NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    - Natural
    1) BV w -> BV w -> BV w
    forall (w :: Natural). BV w -> BV w -> BV w
    `and` Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV Integer
    1

    -- | Return 1 if positive, -1 if negative, and 0 if 0.
    signum :: 1 <= w => NatRepr w -> BV w -> BV w
    signum :: forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> BV w
    signum NatRepr w
    w BV w
    bv = NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w (Integer -> Integer
    forall a. Num a => a -> a
    Prelude.signum (NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv))

    -- | Signed less than.
    slt :: (1 <= w) => NatRepr w -> BV w -> BV w -> Bool
    slt :: forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> BV w -> Bool
    slt NatRepr w
    w BV w
    bv1 BV w
    bv2 = NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv1 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv2

    -- | Signed less than or equal.
    sle :: (1 <= w) => NatRepr w -> BV w -> BV w -> Bool
    sle :: forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> BV w -> Bool
    sle NatRepr w
    w BV w
    bv1 BV w
    bv2 = NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv1 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv2

    -- | Unsigned less than.
    ult :: BV w -> BV w -> Bool
    ult :: forall (w :: Natural). BV w -> BV w -> Bool
    ult BV w
    bv1 BV w
    bv2 = BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    asUnsigned BV w
    bv1 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    asUnsigned BV w
    bv2

    -- | Unsigned less than or equal.
    ule :: BV w -> BV w -> Bool
    ule :: forall (w :: Natural). BV w -> BV w -> Bool
    ule BV w
    bv1 BV w
    bv2 = BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    asUnsigned BV w
    bv1 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    asUnsigned BV w
    bv2

    -- | Unsigned minimum of two bitvectors.
    umin :: BV w -> BV w -> BV w
    umin :: forall (w :: Natural). BV w -> BV w -> BV w
    umin (BV Integer
    x) (BV Integer
    y) = if Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    y then Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV Integer
    x else Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV Integer
    y

    -- | Unsigned maximum of two bitvectors.
    umax :: BV w -> BV w -> BV w
    umax :: forall (w :: Natural). BV w -> BV w -> BV w
    umax (BV Integer
    x) (BV Integer
    y) = if Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    y then Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV Integer
    y else Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV Integer
    x

    -- | Signed minimum of two bitvectors.
    smin :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
    smin :: forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> BV w -> BV w
    smin NatRepr w
    w BV w
    bv1 BV w
    bv2 = if NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv1 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv2 then BV w
    bv1 else BV w
    bv2

    -- | Signed maximum of two bitvectors.
    smax :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
    smax :: forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> BV w -> BV w
    smax NatRepr w
    w BV w
    bv1 BV w
    bv2 = if NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv1 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv2 then BV w
    bv2 else BV w
    bv1

    ----------------------------------------
    -- Width-changing operations

    -- | Concatenate two bitvectors. The first argument gets placed in the
    -- higher order bits.
    --
    -- >>> concat knownNat (mkBV (knownNat @3) 0b001) (mkBV (knownNat @2) 0b10)
    -- BV 6
    -- >>> :type it
    -- it :: BV 5
    concat :: NatRepr w
           -- ^ Width of higher-order bits
           -> NatRepr w'
           -- ^ Width of lower-order bits
           -> BV w
           -- ^ Higher-order bits
           -> BV w'
           -- ^ Lower-order bits
           -> BV (w+w')
    concat :: forall (w :: Natural) (w' :: Natural).
    NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')
    concat NatRepr w
    w NatRepr w'
    w' (BV Integer
    hi) (BV Integer
    lo) = NatRepr (w + w') -> BV (w + w') -> BV (w + w')
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr (NatRepr w
    w NatRepr w -> NatRepr w' -> NatRepr (w + w')
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> NatRepr (m + n)
    `addNat` NatRepr w'
    w') (BV (w + w') -> BV (w + w')) -> BV (w + w') -> BV (w + w')
    forall a b. (a -> b) -> a -> b
    $
      Integer -> BV (w + w')
    forall (w :: Natural). Integer -> BV w
    BV ((Integer
    hi Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `B.shiftL` Natural -> Int
    fromNatural (NatRepr w' -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w'
    w')) Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    B..|. Integer
    lo)

    -- | Slice out a smaller bitvector from a larger one.
    --
    -- >>> select (knownNat @4) (knownNat @1) (mkBV (knownNat @12) 0b110010100110)
    -- BV 3
    -- >>> :type it
    -- it :: BV 4
    select :: ix + w' <= w
           => NatRepr ix
           -- ^ Index to start selecting from
           -> NatRepr w'
           -- ^ Desired output width
           -> BV w
           -- ^ Bitvector to select from
           -> BV w'
    select :: forall (ix :: Natural) (w' :: Natural) (w :: Natural).
    ((ix + w') <= w) =>
    NatRepr ix -> NatRepr w' -> BV w -> BV w'
    select NatRepr ix
    ix NatRepr w'
    w' (BV Integer
    x) = NatRepr w' -> Integer -> BV w'
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w'
    w' Integer
    xShf
      -- NB fromNatural is OK because of (ix + w' <= w) constraint
      where xShf :: Integer
    xShf = Integer
    x Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `B.shiftR` Natural -> Int
    fromNatural (NatRepr ix -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr ix
    ix)

    -- | Like 'select', but takes a 'Natural' as the index to start
    -- selecting from. Neither the index nor the output width is checked
    -- to ensure the resulting 'BV' lies entirely within the bounds of the
    -- original bitvector. Any bits "selected" from beyond the bounds of
    -- the input bitvector will be 0.
    --
    -- >>> select' (knownNat @4) 9 (mkBV (knownNat @12) 0b110010100110)
    -- BV 6
    -- >>> :type it
    -- it :: BV 4
    select' :: Natural
            -- ^ Index to start selecting from
            -> NatRepr w'
            -- ^ Desired output width
            -> BV w
            -- ^ Bitvector to select from
            -> BV w'
    select' :: forall (w' :: Natural) (w :: Natural).
    Natural -> NatRepr w' -> BV w -> BV w'
    select' Natural
    ix NatRepr w'
    w' (BV Integer
    x)
      | Natural -> Integer
    forall a. Integral a => a -> Integer
    toInteger Natural
    ix Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Int
    forall a. Bounded a => a
    maxBound :: Int) = NatRepr w' -> Integer -> BV w'
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV NatRepr w'
    w' (Integer
    x Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `B.shiftR` Natural -> Int
    fromNatural Natural
    ix)
      | Bool
    otherwise = NatRepr w' -> BV w'
    forall (w :: Natural). NatRepr w -> BV w
    zero NatRepr w'
    w'

    -- | Zero-extend a bitvector to one of strictly greater width.
    --
    -- >>> zext (knownNat @8) (mkBV (knownNat @4) 0b1101)
    -- BV 13
    -- >>> :type it
    -- it :: BV 8
    zext :: w + 1 <= w'
         => NatRepr w'
         -- ^ Desired output width
         -> BV w
         -- ^ Bitvector to extend
         -> BV w'
    zext :: forall (w :: Natural) (w' :: Natural).
    ((w + 1) <= w') =>
    NatRepr w' -> BV w -> BV w'
    zext NatRepr w'
    w (BV Integer
    x) = NatRepr w' -> BV w' -> BV w'
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr NatRepr w'
    w (BV w' -> BV w') -> BV w' -> BV w'
    forall a b. (a -> b) -> a -> b
    $ Integer -> BV w'
    forall (w :: Natural). Integer -> BV w
    BV Integer
    x

    -- | Sign-extend a bitvector to one of strictly greater width.
    sext :: (1 <= w, w + 1 <= w')
         => NatRepr w
         -- ^ Width of input bitvector
         -> NatRepr w'
         -- ^ Desired output width
         -> BV w
         -- ^ Bitvector to extend
         -> BV w'
    sext :: forall (w :: Natural) (w' :: Natural).
    (1 <= w, (w + 1) <= w') =>
    NatRepr w -> NatRepr w' -> BV w -> BV w'
    sext NatRepr w
    w NatRepr w'
    w' BV w
    bv = NatRepr w' -> Integer -> BV w'
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV NatRepr w'
    w' (NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv)

    -- | Truncate a bitvector to one of strictly smaller width.
    trunc :: w' + 1 <= w
          => NatRepr w'
          -- ^ Desired output width
          -> BV w
          -- ^ Bitvector to truncate
          -> BV w'
    trunc :: forall (w' :: Natural) (w :: Natural).
    ((w' + 1) <= w) =>
    NatRepr w' -> BV w -> BV w'
    trunc NatRepr w'
    w' (BV Integer
    x) = NatRepr w' -> Integer -> BV w'
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w'
    w' Integer
    x

    -- | Like 'trunc', but allows the input width to be greater than or
    -- equal to the output width, in which case it just performs a zero
    -- extension.
    trunc' :: NatRepr w'
           -- ^ Desired output width
           -> BV w
           -- ^ Bitvector to truncate
           -> BV w'
    trunc' :: forall (w' :: Natural) (w :: Natural). NatRepr w' -> BV w -> BV w'
    trunc' NatRepr w'
    w' (BV Integer
    x) = NatRepr w' -> Integer -> BV w'
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV NatRepr w'
    w' Integer
    x
    {-# DEPRECATED trunc' "Use zresize instead" #-}

    -- | Resizes a bitvector. If @w' > w@, perform a zero extension.
    zresize :: NatRepr w'
            -- ^ Desired output width
            -> BV w
            -- ^ Bitvector to resize
            -> BV w'
    zresize :: forall (w' :: Natural) (w :: Natural). NatRepr w' -> BV w -> BV w'
    zresize NatRepr w'
    w' (BV Integer
    x) = NatRepr w' -> Integer -> BV w'
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV NatRepr w'
    w' Integer
    x

    -- | Resizes a bitvector. If @w' > w@, perform a signed extension.
    sresize :: 1 <= w
            => NatRepr w
            -- ^ Width of input vector
            -> NatRepr w'
            -- ^ Desired output width
            -> BV w
            -- ^ Bitvector to resize
            -> BV w'
    sresize :: forall (w :: Natural) (w' :: Natural).
    (1 <= w) =>
    NatRepr w -> NatRepr w' -> BV w -> BV w'
    sresize NatRepr w
    w NatRepr w'
    w' BV w
    bv = NatRepr w' -> Integer -> BV w'
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV NatRepr w'
    w' (NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv)

    -- | Wide multiply of two bitvectors.
    mulWide :: NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w+w')
    mulWide :: forall (w :: Natural) (w' :: Natural).
    NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')
    mulWide NatRepr w
    w NatRepr w'
    w' (BV Integer
    x) (BV Integer
    y) = NatRepr (w + w') -> BV (w + w') -> BV (w + w')
    forall (w :: Natural) a. NatRepr w -> a -> a
    checkNatRepr (NatRepr w
    w NatRepr w -> NatRepr w' -> NatRepr (w + w')
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> NatRepr (m + n)
    `addNat` NatRepr w'
    w') (BV (w + w') -> BV (w + w')) -> BV (w + w') -> BV (w + w')
    forall a b. (a -> b) -> a -> b
    $ Integer -> BV (w + w')
    forall (w :: Natural). Integer -> BV w
    BV (Integer
    xInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *Integer
    y)

    ----------------------------------------
    -- Enum functions

    -- | Unsigned successor. @succUnsigned w (maxUnsigned w)@ returns 'Nothing'.
    succUnsigned :: NatRepr w -> BV w -> Maybe (BV w)
    succUnsigned :: forall (w :: Natural). NatRepr w -> BV w -> Maybe (BV w)
    succUnsigned NatRepr w
    w (BV Integer
    x) =
      if Integer
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == NatRepr w -> Integer
    forall (w :: Natural). NatRepr w -> Integer
    P.maxUnsigned NatRepr w
    w
      then Maybe (BV w)
    forall a. Maybe a
    Nothing
      else BV w -> Maybe (BV w)
    forall a. a -> Maybe a
    Just (Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Integer
    xInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    1))

    -- | Signed successor. @succSigned w (maxSigned w)@ returns 'Nothing'.
    succSigned :: 1 <= w => NatRepr w -> BV w -> Maybe (BV w)
    succSigned :: forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> Maybe (BV w)
    succSigned NatRepr w
    w (BV Integer
    x) =
      if Integer
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == NatRepr w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
    P.maxSigned NatRepr w
    w
      then Maybe (BV w)
    forall a. Maybe a
    Nothing
      else BV w -> Maybe (BV w)
    forall a. a -> Maybe a
    Just (NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w (Integer
    xInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    1))

    -- | Unsigned predecessor. @predUnsigned w zero@ returns 'Nothing'.
    predUnsigned :: NatRepr w -> BV w -> Maybe (BV w)
    predUnsigned :: forall (w :: Natural). NatRepr w -> BV w -> Maybe (BV w)
    predUnsigned NatRepr w
    w (BV Integer
    x) =
      if Integer
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == NatRepr w -> Integer
    forall (w :: Natural). NatRepr w -> Integer
    P.minUnsigned NatRepr w
    w
      then Maybe (BV w)
    forall a. Maybe a
    Nothing
      else BV w -> Maybe (BV w)
    forall a. a -> Maybe a
    Just (Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Integer
    xInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1))

    -- | Signed predecessor. @predSigned w (minSigned w)@ returns 'Nothing'.
    predSigned :: 1 <= w => NatRepr w -> BV w -> Maybe (BV w)
    predSigned :: forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> Maybe (BV w)
    predSigned NatRepr w
    w bv :: BV w
    bv@(BV Integer
    x) =
      if BV w
    bv BV w -> BV w -> Bool
    forall a. Eq a => a -> a -> Bool
    == NatRepr w -> BV w
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
    minSigned NatRepr w
    w
      then Maybe (BV w)
    forall a. Maybe a
    Nothing
      else BV w -> Maybe (BV w)
    forall a. a -> Maybe a
    Just (NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV' NatRepr w
    w (Integer
    xInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1))

    -- | List of all unsigned bitvectors from a lower to an upper bound,
    -- inclusive.
    enumFromToUnsigned :: BV w
                       -- ^ Lower bound
                       -> BV w
                       -- ^ Upper bound
                       -> [BV w]
    enumFromToUnsigned :: forall (w :: Natural). BV w -> BV w -> [BV w]
    enumFromToUnsigned BV w
    bv1 BV w
    bv2 = Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Integer -> BV w) -> [Integer] -> [BV w]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    asUnsigned BV w
    bv1 .. BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    asUnsigned BV w
    bv2]

    -- | List of all signed bitvectors from a lower to an upper bound,
    -- inclusive.
    enumFromToSigned :: 1 <= w => NatRepr w
                     -> BV w
                     -- ^ Lower bound
                     -> BV w
                     -- ^ Upper bound
                     -> [BV w]
    enumFromToSigned :: forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> BV w -> [BV w]
    enumFromToSigned NatRepr w
    w BV w
    bv1 BV w
    bv2 =
      Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Integer -> BV w) -> (Integer -> Integer) -> Integer -> BV w
    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
    . NatRepr w -> Integer -> Maybe Integer
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> Integer -> Maybe Integer
    signedToUnsigned NatRepr w
    w (Integer -> BV w) -> [Integer] -> [BV w]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv1 .. NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    bv2]

    ----------------------------------------
    -- Generating random bitvectors

    -- | Generates a bitvector uniformly distributed over all possible values for a
    -- given width. (See 'System.Random.Stateful.uniformM').
    uniformM :: StatefulGen g m => NatRepr w -> g -> m (BV w)
    uniformM :: forall g (m :: * -> *) (w :: Natural).
    StatefulGen g m =>
    NatRepr w -> g -> m (BV w)
    uniformM NatRepr w
    w g
    g = Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Integer -> BV w) -> m Integer -> m (BV w)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer, Integer) -> g -> m Integer
    forall a g (m :: * -> *).
    (UniformRange a, StatefulGen g m) =>
    (a, a) -> g -> m a
    forall g (m :: * -> *).
    StatefulGen g m =>
    (Integer, Integer) -> g -> m Integer
    uniformRM (NatRepr w -> Integer
    forall (w :: Natural). NatRepr w -> Integer
    P.minUnsigned NatRepr w
    w, NatRepr w -> Integer
    forall (w :: Natural). NatRepr w -> Integer
    P.maxUnsigned NatRepr w
    w) g
    g

    -- | Generates a bitvector uniformly distributed over the provided range
    -- (interpreted as a range of /unsigned/ bitvectors), which is interpreted as
    -- inclusive in the lower and upper bound. (See
    -- 'System.Random.Stateful.uniformRM').
    uUniformRM :: StatefulGen g m => (BV w, BV w) -> g -> m (BV w)
    uUniformRM :: forall g (m :: * -> *) (w :: Natural).
    StatefulGen g m =>
    (BV w, BV w) -> g -> m (BV w)
    uUniformRM (BV w
    lo, BV w
    hi) g
    g =
      let loI :: Integer
    loI = BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    asUnsigned BV w
    lo
          hiI :: Integer
    hiI = BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    asUnsigned BV w
    hi
      in Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV (Integer -> BV w) -> m Integer -> m (BV w)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer, Integer) -> g -> m Integer
    forall a g (m :: * -> *).
    (UniformRange a, StatefulGen g m) =>
    (a, a) -> g -> m a
    forall g (m :: * -> *).
    StatefulGen g m =>
    (Integer, Integer) -> g -> m Integer
    uniformRM (Integer
    loI, Integer
    hiI) g
    g

    -- | Generates a bitvector uniformly distributed over the provided range
    -- (interpreted as a range of /signed/ bitvectors), which is interpreted as
    -- inclusive in the lower and upper bound. (See
    -- 'System.Random.Stateful.uniformRM').
    sUniformRM :: (StatefulGen g m, 1 <= w) => NatRepr w -> (BV w, BV w) -> g -> m (BV w)
    sUniformRM :: forall g (m :: * -> *) (w :: Natural).
    (StatefulGen g m, 1 <= w) =>
    NatRepr w -> (BV w, BV w) -> g -> m (BV w)
    sUniformRM NatRepr w
    w (BV w
    lo, BV w
    hi) g
    g =
      let loI :: Integer
    loI = NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    lo
          hiI :: Integer
    hiI = NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    asSigned NatRepr w
    w BV w
    hi
      in NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV NatRepr w
    w (Integer -> BV w) -> m Integer -> m (BV w)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer, Integer) -> g -> m Integer
    forall a g (m :: * -> *).
    (UniformRange a, StatefulGen g m) =>
    (a, a) -> g -> m a
    forall g (m :: * -> *).
    StatefulGen g m =>
    (Integer, Integer) -> g -> m Integer
    uniformRM (Integer
    loI, Integer
    hiI) g
    g

    ----------------------------------------
    -- Pretty printing

    -- | Pretty print in hex
    ppHex :: NatRepr w -> BV w -> String
    ppHex :: forall (w :: Natural). NatRepr w -> BV w -> String
    ppHex NatRepr w
    w (BV Integer
    x) = String
    "0x" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String -> String
    forall a. Integral a => a -> String -> String
    N.showHex Integer
    x String
    "" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ":" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ NatRepr w -> String
    forall (w :: Natural). NatRepr w -> String
    ppWidth NatRepr w
    w

    -- | Pretty print in binary
    ppBin :: NatRepr w -> BV w -> String
    ppBin :: forall (w :: Natural). NatRepr w -> BV w -> String
    ppBin NatRepr w
    w (BV Integer
    x) = String
    "0b" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Integer -> (Int -> Char) -> Integer -> String -> String
    forall a. Integral a => a -> (Int -> Char) -> a -> String -> String
    N.showIntAtBase Integer
    2 Int -> Char
    intToDigit Integer
    x String
    "" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ":" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ NatRepr w -> String
    forall (w :: Natural). NatRepr w -> String
    ppWidth NatRepr w
    w

    -- | Pretty print in octal
    ppOct :: NatRepr w -> BV w -> String
    ppOct :: forall (w :: Natural). NatRepr w -> BV w -> String
    ppOct NatRepr w
    w (BV Integer
    x) = String
    "0o" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String -> String
    forall a. Integral a => a -> String -> String
    N.showOct Integer
    x String
    "" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ":" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ NatRepr w -> String
    forall (w :: Natural). NatRepr w -> String
    ppWidth NatRepr w
    w

    -- | Pretty print in decimal
    ppDec :: NatRepr w -> BV w -> String
    ppDec :: forall (w :: Natural). NatRepr w -> BV w -> String
    ppDec NatRepr w
    w (BV Integer
    x) = Integer -> String
    forall a. Show a => a -> String
    show Integer
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ":" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ NatRepr w -> String
    forall (w :: Natural). NatRepr w -> String
    ppWidth NatRepr w
    w

    ppWidth :: NatRepr w -> String
    ppWidth :: forall (w :: Natural). NatRepr w -> String
    ppWidth NatRepr w
    w = String
    "[" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Natural -> String
    forall a. Show a => a -> String
    show (NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "]"