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

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

{-# LANGUAGE Unsafe #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise       #-}
{-# OPTIONS_HADDOCK show-extensions not-home #-}

module Clash.Sized.Internal.BitVector
  ( -- * Bit
    Bit (..)
    -- ** Construction
  , high
  , low
    -- ** Type classes
    -- *** Eq
  , eq##
  , neq##
    -- *** Ord
  , lt##
  , ge##
  , gt##
  , le##
    -- *** Num
  , fromInteger##
    -- *** Bits
  , and##
  , or##
  , xor##
  , complement##
    -- *** BitPack
  , pack#
  , unpack#
    -- * BitVector
  , BitVector (..)
    -- ** Accessors
  , size#
  , maxIndex#
    -- ** Construction
  , bLit
  , undefined#
    -- ** Concatenation
  , (++#)
    -- ** Reduction
  , reduceAnd#
  , reduceOr#
  , reduceXor#
    -- ** Indexing
  , index#
  , replaceBit#
  , setSlice#
  , slice#
  , split#
  , msb#
  , lsb#
    -- ** Type classes
    -- **** Eq
  , eq#
  , neq#
  , isLike
    -- *** Ord
  , lt#
  , ge#
  , gt#
  , le#
    -- *** Enum (not synthesizable)
  , enumFrom#
  , enumFromThen#
  , enumFromTo#
  , enumFromThenTo#
    -- *** Bounded
  , minBound#
  , maxBound#
    -- *** Num
  , (+#)
  , (-#)
  , (*#)
  , negate#
  , fromInteger#
    -- *** ExtendingNum
  , plus#
  , minus#
  , times#
    -- *** Integral
  , quot#
  , rem#
  , toInteger#
    -- *** Bits
  , and#
  , or#
  , xor#
  , complement#
  , shiftL#
  , shiftR#
  , rotateL#
  , rotateR#
  , popCountBV
    -- *** FiniteBits
  , countLeadingZerosBV
  , countTrailingZerosBV
    -- *** Resize
  , truncateB#
    -- *** QuickCheck
  , shrinkSizedUnsigned
  -- ** Other
  , undefError
  , checkUnpackUndef
  , bitPattern
  )
where

import Control.DeepSeq            (NFData (..))
import Control.Lens               (Index, Ixed (..), IxValue)
import Data.Bits                  (Bits (..), FiniteBits (..))
import Data.Data                  (Data)
import Data.Default.Class         (Default (..))
import Data.Either                (isLeft)
import Data.Proxy                 (Proxy (..))
import Data.Typeable              (Typeable, typeOf)
import GHC.Generics               (Generic)
import Data.Maybe                 (fromMaybe)
import GHC.Integer                (smallInteger)
import GHC.Prim                   (dataToTag#)
import GHC.Stack                  (HasCallStack, withFrozenCallStack)
import GHC.TypeLits               (KnownNat, Nat, type (+), type (-), natVal)
import GHC.TypeLits.Extra         (Max)
import Language.Haskell.TH        (Q, TExp, TypeQ, appT, conT, litT, numTyLit, sigE, Lit(..), litE, Pat, litP)
import Language.Haskell.TH.Syntax (Lift(..))
import Test.QuickCheck.Arbitrary  (Arbitrary (..), CoArbitrary (..),
                                   arbitraryBoundedIntegral,
                                   coarbitraryIntegral, shrinkIntegral)

import Clash.Class.Num            (ExtendingNum (..), SaturatingNum (..),
                                   SaturationMode (..))
import Clash.Class.Resize         (Resize (..))
import Clash.Promoted.Nat
  (SNat (..), SNatLE (..), compareSNat, snatToInteger, snatToNum)
import Clash.XException
  (ShowX (..), NFDataX (..), errorX, isX, showsPrecXWith, rwhnfX)

import {-# SOURCE #-} qualified Clash.Sized.Vector         as V
import {-# SOURCE #-} qualified Clash.Sized.Internal.Index as I
import                qualified Data.List                  as L

{- $setup
>>> :set -XTemplateHaskell
>>> :set -XBinaryLiterals
-}

-- * Type definitions

-- | A vector of bits.
--
-- * Bit indices are descending
-- * 'Num' instance performs /unsigned/ arithmetic.
data BitVector (n :: Nat) =
    -- | The constructor, 'BV', and  the field, 'unsafeToInteger', are not
    -- synthesizable.
    BV { BitVector n -> Integer
unsafeMask      :: !Integer
       , BitVector n -> Integer
unsafeToInteger :: !Integer
       }
  deriving (Typeable (BitVector n)
DataType
Constr
Typeable (BitVector n) =>
(forall (c :: Type -> Type).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> BitVector n -> c (BitVector n))
-> (forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (BitVector n))
-> (BitVector n -> Constr)
-> (BitVector n -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (BitVector n)))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (BitVector n)))
-> ((forall b. Data b => b -> b) -> BitVector n -> BitVector n)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> BitVector n -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> BitVector n -> r)
-> (forall u. (forall d. Data d => d -> u) -> BitVector n -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> BitVector n -> u)
-> (forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d) -> BitVector n -> m (BitVector n))
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BitVector n -> m (BitVector n))
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BitVector n -> m (BitVector n))
-> Data (BitVector n)
BitVector n -> DataType
BitVector n -> Constr
(forall b. Data b => b -> b) -> BitVector n -> BitVector n
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BitVector n -> c (BitVector n)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BitVector n)
forall a.
Typeable a =>
(forall (c :: Type -> Type).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> BitVector n -> u
forall u. (forall d. Data d => d -> u) -> BitVector n -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BitVector n -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BitVector n -> r
forall (n :: Nat). KnownNat n => Typeable (BitVector n)
forall (n :: Nat). KnownNat n => BitVector n -> DataType
forall (n :: Nat). KnownNat n => BitVector n -> Constr
forall (n :: Nat).
KnownNat n =>
(forall b. Data b => b -> b) -> BitVector n -> BitVector n
forall (n :: Nat) u.
KnownNat n =>
Int -> (forall d. Data d => d -> u) -> BitVector n -> u
forall (n :: Nat) u.
KnownNat n =>
(forall d. Data d => d -> u) -> BitVector n -> [u]
forall (n :: Nat) r r'.
KnownNat n =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BitVector n -> r
forall (n :: Nat) r r'.
KnownNat n =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BitVector n -> r
forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, Monad m) =>
(forall d. Data d => d -> m d) -> BitVector n -> m (BitVector n)
forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> BitVector n -> m (BitVector n)
forall (n :: Nat) (c :: Type -> Type).
KnownNat n =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BitVector n)
forall (n :: Nat) (c :: Type -> Type).
KnownNat n =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BitVector n -> c (BitVector n)
forall (n :: Nat) (t :: Type -> Type) (c :: Type -> Type).
(KnownNat n, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (BitVector n))
forall (n :: Nat) (t :: Type -> Type -> Type) (c :: Type -> Type).
(KnownNat n, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BitVector n))
forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> BitVector n -> m (BitVector n)
forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BitVector n -> m (BitVector n)
forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BitVector n)
forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BitVector n -> c (BitVector n)
forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (BitVector n))
forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BitVector n))
$cBV :: Constr
$tBitVector :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> BitVector n -> m (BitVector n)
$cgmapMo :: forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> BitVector n -> m (BitVector n)
gmapMp :: (forall d. Data d => d -> m d) -> BitVector n -> m (BitVector n)
$cgmapMp :: forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, MonadPlus m) =>
(forall d. Data d => d -> m d) -> BitVector n -> m (BitVector n)
gmapM :: (forall d. Data d => d -> m d) -> BitVector n -> m (BitVector n)
$cgmapM :: forall (n :: Nat) (m :: Type -> Type).
(KnownNat n, Monad m) =>
(forall d. Data d => d -> m d) -> BitVector n -> m (BitVector n)
gmapQi :: Int -> (forall d. Data d => d -> u) -> BitVector n -> u
$cgmapQi :: forall (n :: Nat) u.
KnownNat n =>
Int -> (forall d. Data d => d -> u) -> BitVector n -> u
gmapQ :: (forall d. Data d => d -> u) -> BitVector n -> [u]
$cgmapQ :: forall (n :: Nat) u.
KnownNat n =>
(forall d. Data d => d -> u) -> BitVector n -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BitVector n -> r
$cgmapQr :: forall (n :: Nat) r r'.
KnownNat n =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BitVector n -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BitVector n -> r
$cgmapQl :: forall (n :: Nat) r r'.
KnownNat n =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BitVector n -> r
gmapT :: (forall b. Data b => b -> b) -> BitVector n -> BitVector n
$cgmapT :: forall (n :: Nat).
KnownNat n =>
(forall b. Data b => b -> b) -> BitVector n -> BitVector n
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BitVector n))
$cdataCast2 :: forall (n :: Nat) (t :: Type -> Type -> Type) (c :: Type -> Type).
(KnownNat n, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BitVector n))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (BitVector n))
$cdataCast1 :: forall (n :: Nat) (t :: Type -> Type) (c :: Type -> Type).
(KnownNat n, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (BitVector n))
dataTypeOf :: BitVector n -> DataType
$cdataTypeOf :: forall (n :: Nat). KnownNat n => BitVector n -> DataType
toConstr :: BitVector n -> Constr
$ctoConstr :: forall (n :: Nat). KnownNat n => BitVector n -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BitVector n)
$cgunfold :: forall (n :: Nat) (c :: Type -> Type).
KnownNat n =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BitVector n)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BitVector n -> c (BitVector n)
$cgfoldl :: forall (n :: Nat) (c :: Type -> Type).
KnownNat n =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BitVector n -> c (BitVector n)
$cp1Data :: forall (n :: Nat). KnownNat n => Typeable (BitVector n)
Data, (forall x. BitVector n -> Rep (BitVector n) x)
-> (forall x. Rep (BitVector n) x -> BitVector n)
-> Generic (BitVector n)
forall x. Rep (BitVector n) x -> BitVector n
forall x. BitVector n -> Rep (BitVector n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (n :: Nat) x. Rep (BitVector n) x -> BitVector n
forall (n :: Nat) x. BitVector n -> Rep (BitVector n) x
$cto :: forall (n :: Nat) x. Rep (BitVector n) x -> BitVector n
$cfrom :: forall (n :: Nat) x. BitVector n -> Rep (BitVector n) x
Generic)

-- * Bit

-- | Bit
data Bit =
  -- | The constructor, 'Bit', and  the field, 'unsafeToInteger#', are not
  -- synthesizable.
  Bit { Bit -> Integer
unsafeMask#      :: !Integer
      , Bit -> Integer
unsafeToInteger# :: !Integer
      }
  deriving (Typeable Bit
DataType
Constr
Typeable Bit =>
(forall (c :: Type -> Type).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Bit -> c Bit)
-> (forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Bit)
-> (Bit -> Constr)
-> (Bit -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Bit))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Bit))
-> ((forall b. Data b => b -> b) -> Bit -> Bit)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bit -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bit -> r)
-> (forall u. (forall d. Data d => d -> u) -> Bit -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Bit -> u)
-> (forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d) -> Bit -> m Bit)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Bit -> m Bit)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Bit -> m Bit)
-> Data Bit
Bit -> DataType
Bit -> Constr
(forall b. Data b => b -> b) -> Bit -> Bit
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bit -> c Bit
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Bit
forall a.
Typeable a =>
(forall (c :: Type -> Type).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Bit -> u
forall u. (forall d. Data d => d -> u) -> Bit -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bit -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bit -> r
forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> Bit -> m Bit
forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bit -> m Bit
forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Bit
forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bit -> c Bit
forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Bit)
forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Bit)
$cBit :: Constr
$tBit :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Bit -> m Bit
$cgmapMo :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bit -> m Bit
gmapMp :: (forall d. Data d => d -> m d) -> Bit -> m Bit
$cgmapMp :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bit -> m Bit
gmapM :: (forall d. Data d => d -> m d) -> Bit -> m Bit
$cgmapM :: forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> Bit -> m Bit
gmapQi :: Int -> (forall d. Data d => d -> u) -> Bit -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Bit -> u
gmapQ :: (forall d. Data d => d -> u) -> Bit -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Bit -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bit -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bit -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bit -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bit -> r
gmapT :: (forall b. Data b => b -> b) -> Bit -> Bit
$cgmapT :: (forall b. Data b => b -> b) -> Bit -> Bit
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Bit)
$cdataCast2 :: forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Bit)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Bit)
$cdataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Bit)
dataTypeOf :: Bit -> DataType
$cdataTypeOf :: Bit -> DataType
toConstr :: Bit -> Constr
$ctoConstr :: Bit -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Bit
$cgunfold :: forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Bit
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bit -> c Bit
$cgfoldl :: forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bit -> c Bit
$cp1Data :: Typeable Bit
Data, (forall x. Bit -> Rep Bit x)
-> (forall x. Rep Bit x -> Bit) -> Generic Bit
forall x. Rep Bit x -> Bit
forall x. Bit -> Rep Bit x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Bit x -> Bit
$cfrom :: forall x. Bit -> Rep Bit x
Generic)

-- * Constructions
-- ** Initialisation
{-# NOINLINE high #-}
-- | logic '1'
high :: Bit
high :: Bit
high = Integer -> Integer -> Bit
Bit 0 1

{-# NOINLINE low #-}
-- | logic '0'
low :: Bit
low :: Bit
low = Integer -> Integer -> Bit
Bit 0 0

-- ** Instances
instance NFData Bit where
  rnf :: Bit -> ()
rnf (Bit m :: Integer
m i :: Integer
i) = Integer -> ()
forall a. NFData a => a -> ()
rnf Integer
m () -> () -> ()
forall a b. a -> b -> b
`seq` Integer -> ()
forall a. NFData a => a -> ()
rnf Integer
i () -> () -> ()
forall a b. a -> b -> b
`seq` ()
  {-# NOINLINE rnf #-}

instance Show Bit where
  show :: Bit -> String
show (Bit 0 b :: Integer
b) =
    case Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
b 0 of
      True  -> "1"
      False -> "0"
  show (Bit _ _) = "."

instance ShowX Bit where
  showsPrecX :: Int -> Bit -> ShowS
showsPrecX = (Int -> Bit -> ShowS) -> Int -> Bit -> ShowS
forall a. (Int -> a -> ShowS) -> Int -> a -> ShowS
showsPrecXWith Int -> Bit -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

instance NFDataX Bit where
  deepErrorX :: String -> Bit
deepErrorX = String -> Bit
forall a. HasCallStack => String -> a
errorX
  rnfX :: Bit -> ()
rnfX = Bit -> ()
forall a. a -> ()
rwhnfX
  hasUndefined :: Bit -> Bool
hasUndefined bv :: Bit
bv = Either String Bit -> Bool
forall a b. Either a b -> Bool
isLeft (Bit -> Either String Bit
forall a. a -> Either String a
isX Bit
bv) Bool -> Bool -> Bool
|| Bit -> Integer
unsafeMask# Bit
bv Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= 0

instance Lift Bit where
  lift :: Bit -> Q Exp
lift (Bit m :: Integer
m i :: Integer
i) = [| fromInteger## m i |]
  {-# NOINLINE lift #-}

instance Eq Bit where
  == :: Bit -> Bit -> Bool
(==) = Bit -> Bit -> Bool
eq##
  /= :: Bit -> Bit -> Bool
(/=) = Bit -> Bit -> Bool
neq##

eq## :: Bit -> Bit -> Bool
eq## :: Bit -> Bit -> Bool
eq## b1 :: Bit
b1 b2 :: Bit
b2 = BitVector 1 -> BitVector 1 -> Bool
forall (n :: Nat). KnownNat n => BitVector n -> BitVector n -> Bool
eq# (Bit -> BitVector 1
pack# Bit
b1) (Bit -> BitVector 1
pack# Bit
b2)
{-# NOINLINE eq## #-}

neq## :: Bit -> Bit -> Bool
neq## :: Bit -> Bit -> Bool
neq## b1 :: Bit
b1 b2 :: Bit
b2 = BitVector 1 -> BitVector 1 -> Bool
forall (n :: Nat). KnownNat n => BitVector n -> BitVector n -> Bool
neq# (Bit -> BitVector 1
pack# Bit
b1) (Bit -> BitVector 1
pack# Bit
b2)
{-# NOINLINE neq## #-}

instance Ord Bit where
  < :: Bit -> Bit -> Bool
(<)  = Bit -> Bit -> Bool
lt##
  <= :: Bit -> Bit -> Bool
(<=) = Bit -> Bit -> Bool
le##
  > :: Bit -> Bit -> Bool
(>)  = Bit -> Bit -> Bool
gt##
  >= :: Bit -> Bit -> Bool
(>=) = Bit -> Bit -> Bool
ge##

lt##,ge##,gt##,le## :: Bit -> Bit -> Bool
lt## :: Bit -> Bit -> Bool
lt## b1 :: Bit
b1 b2 :: Bit
b2 = BitVector 1 -> BitVector 1 -> Bool
forall (n :: Nat). KnownNat n => BitVector n -> BitVector n -> Bool
lt# (Bit -> BitVector 1
pack# Bit
b1) (Bit -> BitVector 1
pack# Bit
b2)
{-# NOINLINE lt## #-}
ge## :: Bit -> Bit -> Bool
ge## b1 :: Bit
b1 b2 :: Bit
b2 = BitVector 1 -> BitVector 1 -> Bool
forall (n :: Nat). KnownNat n => BitVector n -> BitVector n -> Bool
ge# (Bit -> BitVector 1
pack# Bit
b1) (Bit -> BitVector 1
pack# Bit
b2)
{-# NOINLINE ge## #-}
gt## :: Bit -> Bit -> Bool
gt## b1 :: Bit
b1 b2 :: Bit
b2 = BitVector 1 -> BitVector 1 -> Bool
forall (n :: Nat). KnownNat n => BitVector n -> BitVector n -> Bool
gt# (Bit -> BitVector 1
pack# Bit
b1) (Bit -> BitVector 1
pack# Bit
b2)
{-# NOINLINE gt## #-}
le## :: Bit -> Bit -> Bool
le## b1 :: Bit
b1 b2 :: Bit
b2 = BitVector 1 -> BitVector 1 -> Bool
forall (n :: Nat). KnownNat n => BitVector n -> BitVector n -> Bool
le# (Bit -> BitVector 1
pack# Bit
b1) (Bit -> BitVector 1
pack# Bit
b2)
{-# NOINLINE le## #-}

instance Enum Bit where
  toEnum :: Int -> Bit
toEnum     = Integer -> Integer -> Bit
fromInteger## 0 (Integer -> Bit) -> (Int -> Integer) -> Int -> Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger
  fromEnum :: Bit -> Int
fromEnum b :: Bit
b = if Bit -> Bit -> Bool
eq## Bit
b Bit
low then 0 else 1

instance Bounded Bit where
  minBound :: Bit
minBound = Bit
low
  maxBound :: Bit
maxBound = Bit
high

instance Default Bit where
  def :: Bit
def = Bit
low

instance Num Bit where
  + :: Bit -> Bit -> Bit
(+)         = Bit -> Bit -> Bit
xor##
  (-)         = Bit -> Bit -> Bit
xor##
  * :: Bit -> Bit -> Bit
(*)         = Bit -> Bit -> Bit
and##
  negate :: Bit -> Bit
negate      = Bit -> Bit
complement##
  abs :: Bit -> Bit
abs         = Bit -> Bit
forall a. a -> a
id
  signum :: Bit -> Bit
signum b :: Bit
b    = Bit
b
  fromInteger :: Integer -> Bit
fromInteger = Integer -> Integer -> Bit
fromInteger## 0

fromInteger## :: Integer -> Integer -> Bit
fromInteger## :: Integer -> Integer -> Bit
fromInteger## m :: Integer
m i :: Integer
i = Integer -> Integer -> Bit
Bit (Integer
m Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` 2) (Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` 2)
{-# NOINLINE fromInteger## #-}

instance Real Bit where
  toRational :: Bit -> Rational
toRational b :: Bit
b = if Bit -> Bit -> Bool
eq## Bit
b Bit
low then 0 else 1

instance Integral Bit where
  quot :: Bit -> Bit -> Bit
quot    a :: Bit
a _ = Bit
a
  rem :: Bit -> Bit -> Bit
rem     _ _ = Bit
low
  div :: Bit -> Bit -> Bit
div     a :: Bit
a _ = Bit
a
  mod :: Bit -> Bit -> Bit
mod     _ _ = Bit
low
  quotRem :: Bit -> Bit -> (Bit, Bit)
quotRem n :: Bit
n _ = (Bit
n,Bit
low)
  divMod :: Bit -> Bit -> (Bit, Bit)
divMod  n :: Bit
n _ = (Bit
n,Bit
low)
  toInteger :: Bit -> Integer
toInteger b :: Bit
b = if Bit -> Bit -> Bool
eq## Bit
b Bit
low then 0 else 1

instance Bits Bit where
  .&. :: Bit -> Bit -> Bit
(.&.)             = Bit -> Bit -> Bit
and##
  .|. :: Bit -> Bit -> Bit
(.|.)             = Bit -> Bit -> Bit
or##
  xor :: Bit -> Bit -> Bit
xor               = Bit -> Bit -> Bit
xor##
  complement :: Bit -> Bit
complement        = Bit -> Bit
complement##
  zeroBits :: Bit
zeroBits          = Bit
low
  bit :: Int -> Bit
bit i :: Int
i             = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then Bit
high else Bit
low
  setBit :: Bit -> Int -> Bit
setBit b :: Bit
b i :: Int
i        = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then Bit
high else Bit
b
  clearBit :: Bit -> Int -> Bit
clearBit b :: Bit
b i :: Int
i      = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then Bit
low  else Bit
b
  complementBit :: Bit -> Int -> Bit
complementBit b :: Bit
b i :: Int
i = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then Bit -> Bit
complement## Bit
b else Bit
b
  testBit :: Bit -> Int -> Bool
testBit b :: Bit
b i :: Int
i       = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then Bit -> Bit -> Bool
eq## Bit
b Bit
high else Bool
False
  bitSizeMaybe :: Bit -> Maybe Int
bitSizeMaybe _    = Int -> Maybe Int
forall a. a -> Maybe a
Just 1
  bitSize :: Bit -> Int
bitSize _         = 1
  isSigned :: Bit -> Bool
isSigned _        = Bool
False
  shiftL :: Bit -> Int -> Bit
shiftL b :: Bit
b i :: Int
i        = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then Bit
b else Bit
low
  shiftR :: Bit -> Int -> Bit
shiftR b :: Bit
b i :: Int
i        = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then Bit
b else Bit
low
  rotateL :: Bit -> Int -> Bit
rotateL b :: Bit
b _       = Bit
b
  rotateR :: Bit -> Int -> Bit
rotateR b :: Bit
b _       = Bit
b
  popCount :: Bit -> Int
popCount b :: Bit
b        = if Bit -> Bit -> Bool
eq## Bit
b Bit
low then 0 else 1

instance FiniteBits Bit where
  finiteBitSize :: Bit -> Int
finiteBitSize _      = 1
  countLeadingZeros :: Bit -> Int
countLeadingZeros b :: Bit
b  = if Bit -> Bit -> Bool
eq## Bit
b Bit
low then 1 else 0
  countTrailingZeros :: Bit -> Int
countTrailingZeros b :: Bit
b = if Bit -> Bit -> Bool
eq## Bit
b Bit
low then 1 else 0

and##, or##, xor## :: Bit -> Bit -> Bit
and## :: Bit -> Bit -> Bit
and## b1 :: Bit
b1 b2 :: Bit
b2 = BitVector 1 -> Bit
unpack# (BitVector 1 -> Bit) -> BitVector 1 -> Bit
forall a b. (a -> b) -> a -> b
$ BitVector 1 -> BitVector 1 -> BitVector 1
forall (n :: Nat). BitVector n -> BitVector n -> BitVector n
and# (Bit -> BitVector 1
pack# Bit
b1) (Bit -> BitVector 1
pack# Bit
b2)
{-# NOINLINE and## #-}

or## :: Bit -> Bit -> Bit
or## b1 :: Bit
b1 b2 :: Bit
b2 = BitVector 1 -> Bit
unpack# (BitVector 1 -> Bit) -> BitVector 1 -> Bit
forall a b. (a -> b) -> a -> b
$ BitVector 1 -> BitVector 1 -> BitVector 1
forall (n :: Nat). BitVector n -> BitVector n -> BitVector n
or# (Bit -> BitVector 1
pack# Bit
b1) (Bit -> BitVector 1
pack# Bit
b2)
{-# NOINLINE or## #-}

xor## :: Bit -> Bit -> Bit
xor## b1 :: Bit
b1 b2 :: Bit
b2 = BitVector 1 -> Bit
unpack# (BitVector 1 -> Bit) -> BitVector 1 -> Bit
forall a b. (a -> b) -> a -> b
$ BitVector 1 -> BitVector 1 -> BitVector 1
forall (n :: Nat). BitVector n -> BitVector n -> BitVector n
xor# (Bit -> BitVector 1
pack# Bit
b1) (Bit -> BitVector 1
pack# Bit
b2)
{-# NOINLINE xor## #-}

complement## :: Bit -> Bit
complement## :: Bit -> Bit
complement## = BitVector 1 -> Bit
unpack# (BitVector 1 -> Bit) -> (Bit -> BitVector 1) -> Bit -> Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector 1 -> BitVector 1
forall (n :: Nat). KnownNat n => BitVector n -> BitVector n
complement# (BitVector 1 -> BitVector 1)
-> (Bit -> BitVector 1) -> Bit -> BitVector 1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bit -> BitVector 1
pack#
{-# NOINLINE complement## #-}

-- *** BitPack
pack# :: Bit -> BitVector 1
pack# :: Bit -> BitVector 1
pack# (Bit m :: Integer
m b :: Integer
b) = Integer -> Integer -> BitVector 1
forall (n :: Nat). Integer -> Integer -> BitVector n
BV Integer
m Integer
b
{-# NOINLINE pack# #-}

unpack# :: BitVector 1 -> Bit
unpack# :: BitVector 1 -> Bit
unpack# (BV m :: Integer
m b :: Integer
b) = Integer -> Integer -> Bit
Bit Integer
m Integer
b
{-# NOINLINE unpack# #-}

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

instance KnownNat n => Show (BitVector n) where
  show :: BitVector n -> String
show bv :: BitVector n
bv@(BV msk :: Integer
msk i :: Integer
i) = ShowS
forall a. [a] -> [a]
reverse ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
underScore ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
forall a. [a] -> [a]
reverse ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer -> ShowS
forall a t a.
(Integral a, Integral t, Num a, Eq a) =>
a -> a -> t -> ShowS
showBV (BitVector n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal BitVector n
bv) Integer
msk Integer
i []
    where
      showBV :: a -> a -> t -> ShowS
showBV 0 _ _ s :: String
s = String
s
      showBV n :: a
n m :: a
m v :: t
v s :: String
s = let (v' :: t
v',vBit :: t
vBit) = t -> t -> (t, t)
forall a. Integral a => a -> a -> (a, a)
divMod t
v 2
                           (m' :: a
m',mBit :: a
mBit) = a -> a -> (a, a)
forall a. Integral a => a -> a -> (a, a)
divMod a
m 2
                       in  case (a
mBit,t
vBit) of
                           (0,0) -> a -> a -> t -> ShowS
showBV (a
n a -> a -> a
forall a. Num a => a -> a -> a
- 1) a
m' t
v' ('0'Char -> ShowS
forall a. a -> [a] -> [a]
:String
s)
                           (0,_) -> a -> a -> t -> ShowS
showBV (a
n a -> a -> a
forall a. Num a => a -> a -> a
- 1) a
m' t
v' ('1'Char -> ShowS
forall a. a -> [a] -> [a]
:String
s)
                           _     -> a -> a -> t -> ShowS
showBV (a
n a -> a -> a
forall a. Num a => a -> a -> a
- 1) a
m' t
v' ('.'Char -> ShowS
forall a. a -> [a] -> [a]
:String
s)

      underScore :: ShowS
underScore xs :: String
xs = case Int -> String -> (String, String)
forall a. Int -> [a] -> ([a], [a])
splitAt 5 String
xs of
                        ([a :: Char
a,b :: Char
b,c :: Char
c,d :: Char
d,e :: Char
e],rest :: String
rest) -> [Char
a,Char
b,Char
c,Char
d,'_'] String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
underScore (Char
eChar -> ShowS
forall a. a -> [a] -> [a]
:String
rest)
                        (rest :: String
rest,_)               -> String
rest
  {-# NOINLINE show #-}

instance KnownNat n => ShowX (BitVector n) where
  showsPrecX :: Int -> BitVector n -> ShowS
showsPrecX = (Int -> BitVector n -> ShowS) -> Int -> BitVector n -> ShowS
forall a. (Int -> a -> ShowS) -> Int -> a -> ShowS
showsPrecXWith Int -> BitVector n -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

instance NFDataX (BitVector n) where
  deepErrorX :: String -> BitVector n
deepErrorX = String -> BitVector n
forall a. HasCallStack => String -> a
errorX
  rnfX :: BitVector n -> ()
rnfX = BitVector n -> ()
forall a. a -> ()
rwhnfX
  hasUndefined :: BitVector n -> Bool
hasUndefined bv :: BitVector n
bv = Either String (BitVector n) -> Bool
forall a b. Either a b -> Bool
isLeft (BitVector n -> Either String (BitVector n)
forall a. a -> Either String a
isX BitVector n
bv) Bool -> Bool -> Bool
|| BitVector n -> Integer
forall (n :: Nat). BitVector n -> Integer
unsafeMask BitVector n
bv Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= 0

-- | Create a binary literal
--
-- >>> $$(bLit "1001") :: BitVector 4
-- 1001
-- >>> $$(bLit "1001") :: BitVector 3
-- 001
--
-- __NB__: You can also just write:
--
-- >>> 0b1001 :: BitVector 4
-- 1001
--
-- The advantage of 'bLit' is that you can use computations to create the
-- string literal:
--
-- >>> import qualified Data.List as List
-- >>> $$(bLit (List.replicate 4 '1')) :: BitVector 4
-- 1111
--
-- Also 'bLit' can handle don't care bits:
--
-- >>> $$(bLit "1.0.") :: BitVector 4
-- 1.0.
bLit :: forall n. KnownNat n => String -> Q (TExp (BitVector n))
bLit :: String -> Q (TExp (BitVector n))
bLit s :: String
s = [|| fromInteger# m i ||]
  where
    bv :: BitVector n
    bv :: BitVector n
bv = String -> BitVector n
forall (n :: Nat). KnownNat n => String -> BitVector n
read# String
s

    m,i :: Integer
    BV m :: Integer
m i :: Integer
i = BitVector n
bv

read# :: KnownNat n => String -> BitVector n
read# :: String -> BitVector n
read# cs :: String
cs = Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV Integer
m Integer
v
  where
    (vs :: [Integer]
vs,ms :: [Integer]
ms) = [(Integer, Integer)] -> ([Integer], [Integer])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Integer, Integer)] -> ([Integer], [Integer]))
-> (String -> [(Integer, Integer)])
-> String
-> ([Integer], [Integer])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> (Integer, Integer)) -> String -> [(Integer, Integer)]
forall a b. (a -> b) -> [a] -> [b]
map Char -> (Integer, Integer)
readBit (String -> [(Integer, Integer)])
-> ShowS -> String -> [(Integer, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '_') (String -> ([Integer], [Integer]))
-> String -> ([Integer], [Integer])
forall a b. (a -> b) -> a -> b
$ String
cs
    combineBits :: [Integer] -> Integer
combineBits = (Integer -> Integer -> Integer) -> Integer -> [Integer] -> Integer
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\b :: Integer
b a :: Integer
a -> Integer
bInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
*2Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
a) 0
    v :: Integer
v = [Integer] -> Integer
combineBits [Integer]
vs
    m :: Integer
m = [Integer] -> Integer
combineBits [Integer]
ms
    readBit :: Char -> (Integer, Integer)
readBit c :: Char
c = case Char
c of
      '0' -> (0,0)
      '1' -> (1,0)
      '.' -> (0,1)
      _   -> String -> (Integer, Integer)
forall a. HasCallStack => String -> a
error (String -> (Integer, Integer)) -> String -> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ "Clash.Sized.Internal.bLit: unknown character: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. Show a => a -> String
show Char
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ " in input: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
cs


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

{-# NOINLINE eq# #-}
eq# :: KnownNat n => BitVector n -> BitVector n -> Bool
eq# :: BitVector n -> BitVector n -> Bool
eq# (BV 0 v1 :: Integer
v1) (BV 0 v2 :: Integer
v2 ) = Integer
v1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
v2
eq# bv1 :: BitVector n
bv1 bv2 :: BitVector n
bv2 = String -> BitVector n -> BitVector n -> Bool
forall (m :: Nat) (n :: Nat) a.
(HasCallStack, KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorI "==" BitVector n
bv1 BitVector n
bv2

{-# NOINLINE neq# #-}
neq# :: KnownNat n => BitVector n -> BitVector n -> Bool
neq# :: BitVector n -> BitVector n -> Bool
neq# (BV 0 v1 :: Integer
v1) (BV 0 v2 :: Integer
v2) = Integer
v1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
v2
neq# bv1 :: BitVector n
bv1 bv2 :: BitVector n
bv2 = String -> BitVector n -> BitVector n -> Bool
forall (m :: Nat) (n :: Nat) a.
(HasCallStack, KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorI "/=" BitVector n
bv1 BitVector n
bv2

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

lt#,ge#,gt#,le# :: KnownNat n => BitVector n -> BitVector n -> Bool
{-# NOINLINE lt# #-}
lt# :: BitVector n -> BitVector n -> Bool
lt# (BV 0 n :: Integer
n) (BV 0 m :: Integer
m) = Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
m
lt# bv1 :: BitVector n
bv1 bv2 :: BitVector n
bv2 = String -> BitVector n -> BitVector n -> Bool
forall (m :: Nat) (n :: Nat) a.
(HasCallStack, KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorI "<" BitVector n
bv1 BitVector n
bv2
{-# NOINLINE ge# #-}
ge# :: BitVector n -> BitVector n -> Bool
ge# (BV 0 n :: Integer
n) (BV 0 m :: Integer
m) = Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
m
ge# bv1 :: BitVector n
bv1 bv2 :: BitVector n
bv2 = String -> BitVector n -> BitVector n -> Bool
forall (m :: Nat) (n :: Nat) a.
(HasCallStack, KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorI ">=" BitVector n
bv1 BitVector n
bv2
{-# NOINLINE gt# #-}
gt# :: BitVector n -> BitVector n -> Bool
gt# (BV 0 n :: Integer
n) (BV 0 m :: Integer
m) = Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
m
gt# bv1 :: BitVector n
bv1 bv2 :: BitVector n
bv2 = String -> BitVector n -> BitVector n -> Bool
forall (m :: Nat) (n :: Nat) a.
(HasCallStack, KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorI ">" BitVector n
bv1 BitVector n
bv2
{-# NOINLINE le# #-}
le# :: BitVector n -> BitVector n -> Bool
le# (BV 0 n :: Integer
n) (BV 0 m :: Integer
m) = Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
m
le#  bv1 :: BitVector n
bv1 bv2 :: BitVector n
bv2 = String -> BitVector n -> BitVector n -> Bool
forall (m :: Nat) (n :: Nat) a.
(HasCallStack, KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorI "<=" BitVector n
bv1 BitVector n
bv2

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

{-# NOINLINE enumFrom# #-}
{-# NOINLINE enumFromThen# #-}
{-# NOINLINE enumFromTo# #-}
{-# NOINLINE enumFromThenTo# #-}
enumFrom#       :: forall n. KnownNat n => BitVector n -> [BitVector n]
enumFromThen#   :: forall n. KnownNat n => BitVector n -> BitVector n -> [BitVector n]
enumFromTo#     :: KnownNat n => BitVector n -> BitVector n -> [BitVector n]
enumFromThenTo# :: KnownNat n => BitVector n -> BitVector n -> BitVector n -> [BitVector n]

enumFrom# :: BitVector n -> [BitVector n]
enumFrom# (BV 0 x :: Integer
x)                           = (Integer -> BitVector n) -> [Integer] -> [BitVector n]
forall a b. (a -> b) -> [a] -> [b]
map (Integer -> Integer -> BitVector n
forall (n :: Nat). KnownNat n => Integer -> Integer -> BitVector n
fromInteger_INLINE 0) [Integer
x .. BitVector n -> Integer
forall (n :: Nat). BitVector n -> Integer
unsafeToInteger (BitVector n
forall a. Bounded a => a
maxBound :: BitVector n)]
enumFrom# bv :: BitVector n
bv
  = String -> BitVector n -> [BitVector n]
forall (n :: Nat) a.
(HasCallStack, KnownNat n) =>
String -> BitVector n -> a
undefErrorU "enumFrom" BitVector n
bv

enumFromThen# :: BitVector n -> BitVector n -> [BitVector n]
enumFromThen# (BV 0 x :: Integer
x) (BV 0 y :: Integer
y)              = (Integer -> BitVector n) -> [Integer] -> [BitVector n]
forall a b. (a -> b) -> [a] -> [b]
map (Integer -> Integer -> BitVector n
forall (n :: Nat). KnownNat n => Integer -> Integer -> BitVector n
fromInteger_INLINE 0) [Integer
x, Integer
y .. BitVector n -> Integer
forall (n :: Nat). BitVector n -> Integer
unsafeToInteger (BitVector n
forall a. Bounded a => a
maxBound :: BitVector n)]
enumFromThen# bv1 :: BitVector n
bv1 bv2 :: BitVector n
bv2
  = String -> BitVector n -> BitVector n -> [BitVector n]
forall (m :: Nat) (n :: Nat) a.
(HasCallStack, KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorP "enumFromThen" BitVector n
bv1 BitVector n
bv2

enumFromTo# :: BitVector n -> BitVector n -> [BitVector n]
enumFromTo# (BV 0 x :: Integer
x) (BV 0 y :: Integer
y)                = (Integer -> BitVector n) -> [Integer] -> [BitVector n]
forall a b. (a -> b) -> [a] -> [b]
map (Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV 0) [Integer
x .. Integer
y]
enumFromTo# bv1 :: BitVector n
bv1 bv2 :: BitVector n
bv2
  = String -> BitVector n -> BitVector n -> [BitVector n]
forall (m :: Nat) (n :: Nat) a.
(HasCallStack, KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorP "enumFromTo" BitVector n
bv1 BitVector n
bv2

enumFromThenTo# :: BitVector n -> BitVector n -> BitVector n -> [BitVector n]
enumFromThenTo# (BV 0 x1 :: Integer
x1) (BV 0 x2 :: Integer
x2) (BV 0 y :: Integer
y) = (Integer -> BitVector n) -> [Integer] -> [BitVector n]
forall a b. (a -> b) -> [a] -> [b]
map (Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV 0) [Integer
x1, Integer
x2 .. Integer
y]
enumFromThenTo# bv1 :: BitVector n
bv1 bv2 :: BitVector n
bv2 bv3 :: BitVector n
bv3
  = String
-> BitVector n -> BitVector n -> BitVector n -> [BitVector n]
forall (m :: Nat) (n :: Nat) (o :: Nat) a.
(HasCallStack, KnownNat m, KnownNat n, KnownNat o) =>
String -> BitVector m -> BitVector n -> BitVector o -> a
undefErrorP3 "enumFromTo" BitVector n
bv1 BitVector n
bv2 BitVector n
bv3


instance KnownNat n => Bounded (BitVector n) where
  minBound :: BitVector n
minBound = BitVector n
forall (n :: Nat). BitVector n
minBound#
  maxBound :: BitVector n
maxBound = BitVector n
forall (n :: Nat). KnownNat n => BitVector n
maxBound#

{-# NOINLINE minBound# #-}
minBound# :: BitVector n
minBound# :: BitVector n
minBound# = Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV 0 0

{-# NOINLINE maxBound# #-}
maxBound# :: forall n . KnownNat n => BitVector n
maxBound# :: BitVector n
maxBound# = let m :: Integer
m = 1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
            in  Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV 0 (Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-1)

instance KnownNat n => Num (BitVector n) where
  + :: BitVector n -> BitVector n -> BitVector n
(+)         = BitVector n -> BitVector n -> BitVector n
forall (n :: Nat).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
(+#)
  (-)         = BitVector n -> BitVector n -> BitVector n
forall (n :: Nat).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
(-#)
  * :: BitVector n -> BitVector n -> BitVector n
(*)         = BitVector n -> BitVector n -> BitVector n
forall (n :: Nat).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
(*#)
  negate :: BitVector n -> BitVector n
negate      = BitVector n -> BitVector n
forall (n :: Nat). KnownNat n => BitVector n -> BitVector n
negate#
  abs :: BitVector n -> BitVector n
abs         = BitVector n -> BitVector n
forall a. a -> a
id
  signum :: BitVector n -> BitVector n
signum bv :: BitVector n
bv   = BitVector 1 -> BitVector n
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
BitVector n -> BitVector m
resizeBV (Bit -> BitVector 1
pack# (BitVector n -> Bit
forall (n :: Nat). KnownNat n => BitVector n -> Bit
reduceOr# BitVector n
bv))
  fromInteger :: Integer -> BitVector n
fromInteger = Integer -> Integer -> BitVector n
forall (n :: Nat). KnownNat n => Integer -> Integer -> BitVector n
fromInteger# 0

(+#),(-#),(*#) :: forall n . KnownNat n => BitVector n -> BitVector n -> BitVector n
{-# NOINLINE (+#) #-}
+# :: BitVector n -> BitVector n -> BitVector n
(+#) (BV 0 i :: Integer
i) (BV 0 j :: Integer
j) =
  let m :: Integer
m = 1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
      z :: Integer
z = Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j
  in  if Integer
z Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
m then Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV 0 (Integer
z Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
m) else Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV 0 Integer
z
(+#) bv1 :: BitVector n
bv1 bv2 :: BitVector n
bv2 = String -> BitVector n -> BitVector n -> BitVector n
forall (m :: Nat) (n :: Nat) a.
(HasCallStack, KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorI "+" BitVector n
bv1 BitVector n
bv2

{-# NOINLINE (-#) #-}
-# :: BitVector n -> BitVector n -> BitVector n
(-#) (BV 0 i :: Integer
i) (BV 0 j :: Integer
j) =
  let m :: Integer
m = 1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
      z :: Integer
z = Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j
  in  if Integer
z Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0 then Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV 0 (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
z) else Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV 0 Integer
z
(-#) bv1 :: BitVector n
bv1 bv2 :: BitVector n
bv2 = String -> BitVector n -> BitVector n -> BitVector n
forall (m :: Nat) (n :: Nat) a.
(HasCallStack, KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorI "-" BitVector n
bv1 BitVector n
bv2

{-# NOINLINE (*#) #-}
*# :: BitVector n -> BitVector n -> BitVector n
(*#) (BV 0 i :: Integer
i) (BV 0 j :: Integer
j) = Integer -> Integer -> BitVector n
forall (n :: Nat). KnownNat n => Integer -> Integer -> BitVector n
fromInteger_INLINE 0 (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
j)
(*#) bv1 :: BitVector n
bv1 bv2 :: BitVector n
bv2 = String -> BitVector n -> BitVector n -> BitVector n
forall (m :: Nat) (n :: Nat) a.
(HasCallStack, KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorI "*" BitVector n
bv1 BitVector n
bv2

{-# NOINLINE negate# #-}
negate# :: forall n . KnownNat n => BitVector n -> BitVector n
negate# :: BitVector n -> BitVector n
negate# (BV 0 0) = Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV 0 0
negate# (BV 0 i :: Integer
i) = Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV 0 (Integer
sz Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
i)
  where
    sz :: Integer
sz = 1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
negate# bv :: BitVector n
bv = String -> BitVector n -> BitVector n
forall (n :: Nat) a.
(HasCallStack, KnownNat n) =>
String -> BitVector n -> a
undefErrorU "negate" BitVector n
bv

{-# NOINLINE fromInteger# #-}
fromInteger# :: KnownNat n => Integer -> Integer -> BitVector n
fromInteger# :: Integer -> Integer -> BitVector n
fromInteger# = Integer -> Integer -> BitVector n
forall (n :: Nat). KnownNat n => Integer -> Integer -> BitVector n
fromInteger_INLINE

{-# INLINE fromInteger_INLINE #-}
fromInteger_INLINE :: forall n . KnownNat n => Integer -> Integer -> BitVector n
fromInteger_INLINE :: Integer -> Integer -> BitVector n
fromInteger_INLINE m :: Integer
m i :: Integer
i = Integer
sz Integer -> BitVector n -> BitVector n
forall a b. a -> b -> b
`seq` Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV (Integer
m Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
sz) (Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
sz)
  where
    sz :: Integer
sz = 1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))

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

{-# NOINLINE plus# #-}
plus# :: (KnownNat m, KnownNat n) => BitVector m -> BitVector n -> BitVector (Max m n + 1)
plus# :: BitVector m -> BitVector n -> BitVector (Max m n + 1)
plus# (BV 0 a :: Integer
a) (BV 0 b :: Integer
b) = Integer -> Integer -> BitVector (Max m n + 1)
forall (n :: Nat). Integer -> Integer -> BitVector n
BV 0 (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
b)
plus# bv1 :: BitVector m
bv1 bv2 :: BitVector n
bv2 = String -> BitVector m -> BitVector n -> BitVector (Max m n + 1)
forall (m :: Nat) (n :: Nat) a.
(HasCallStack, KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorP "plus" BitVector m
bv1 BitVector n
bv2

{-# NOINLINE minus# #-}
minus# :: forall m n . (KnownNat m, KnownNat n) => BitVector m -> BitVector n
                                                -> BitVector (Max m n + 1)
minus# :: BitVector m -> BitVector n -> BitVector (Max m n + 1)
minus# (BV 0 a :: Integer
a) (BV 0 b :: Integer
b) =
  let sz :: Int
sz   = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy (Max m n + 1) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Max m n + 1)
forall k (t :: k). Proxy t
Proxy @(Max m n + 1)))
      mask :: Integer
mask = 1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
sz
      z :: Integer
z    = Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b
  in  if Integer
z Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0 then Integer -> Integer -> BitVector (Max m n + 1)
forall (n :: Nat). Integer -> Integer -> BitVector n
BV 0 (Integer
mask Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
z) else Integer -> Integer -> BitVector (Max m n + 1)
forall (n :: Nat). Integer -> Integer -> BitVector n
BV 0 Integer
z
minus# bv1 :: BitVector m
bv1 bv2 :: BitVector n
bv2 = String -> BitVector m -> BitVector n -> BitVector (Max m n + 1)
forall (m :: Nat) (n :: Nat) a.
(HasCallStack, KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorP "minus" BitVector m
bv1 BitVector n
bv2

{-# NOINLINE times# #-}
times# :: (KnownNat m, KnownNat n) => BitVector m -> BitVector n -> BitVector (m + n)
times# :: BitVector m -> BitVector n -> BitVector (m + n)
times# (BV 0 a :: Integer
a) (BV 0 b :: Integer
b) = Integer -> Integer -> BitVector (m + n)
forall (n :: Nat). Integer -> Integer -> BitVector n
BV 0 (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
b)
times# bv1 :: BitVector m
bv1 bv2 :: BitVector n
bv2 = String -> BitVector m -> BitVector n -> BitVector (m + n)
forall (m :: Nat) (n :: Nat) a.
(HasCallStack, KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorP "times" BitVector m
bv1 BitVector n
bv2

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

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

quot#,rem# :: KnownNat n => BitVector n -> BitVector n -> BitVector n
{-# NOINLINE quot# #-}
quot# :: BitVector n -> BitVector n -> BitVector n
quot# (BV 0 i :: Integer
i) (BV 0 j :: Integer
j) = Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV 0 (Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
j)
quot# bv1 :: BitVector n
bv1 bv2 :: BitVector n
bv2 = String -> BitVector n -> BitVector n -> BitVector n
forall (m :: Nat) (n :: Nat) a.
(HasCallStack, KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorP "quot" BitVector n
bv1 BitVector n
bv2
{-# NOINLINE rem# #-}
rem# :: BitVector n -> BitVector n -> BitVector n
rem# (BV 0 i :: Integer
i) (BV 0 j :: Integer
j) = Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV 0 (Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` Integer
j)
rem# bv1 :: BitVector n
bv1 bv2 :: BitVector n
bv2 = String -> BitVector n -> BitVector n -> BitVector n
forall (m :: Nat) (n :: Nat) a.
(HasCallStack, KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorP "rem" BitVector n
bv1 BitVector n
bv2

{-# NOINLINE toInteger# #-}
toInteger# :: KnownNat n => BitVector n -> Integer
toInteger# :: BitVector n -> Integer
toInteger# (BV 0 i :: Integer
i) = Integer
i
toInteger# bv :: BitVector n
bv = String -> BitVector n -> Integer
forall (n :: Nat) a.
(HasCallStack, KnownNat n) =>
String -> BitVector n -> a
undefErrorU "toInteger" BitVector n
bv

instance KnownNat n => Bits (BitVector n) where
  .&. :: BitVector n -> BitVector n -> BitVector n
(.&.)             = BitVector n -> BitVector n -> BitVector n
forall (n :: Nat). BitVector n -> BitVector n -> BitVector n
and#
  .|. :: BitVector n -> BitVector n -> BitVector n
(.|.)             = BitVector n -> BitVector n -> BitVector n
forall (n :: Nat). BitVector n -> BitVector n -> BitVector n
or#
  xor :: BitVector n -> BitVector n -> BitVector n
xor               = BitVector n -> BitVector n -> BitVector n
forall (n :: Nat). BitVector n -> BitVector n -> BitVector n
xor#
  complement :: BitVector n -> BitVector n
complement        = BitVector n -> BitVector n
forall (n :: Nat). KnownNat n => BitVector n -> BitVector n
complement#
  zeroBits :: BitVector n
zeroBits          = 0
  bit :: Int -> BitVector n
bit i :: Int
i             = BitVector n -> Int -> Bit -> BitVector n
forall (n :: Nat).
KnownNat n =>
BitVector n -> Int -> Bit -> BitVector n
replaceBit# 0 Int
i Bit
high
  setBit :: BitVector n -> Int -> BitVector n
setBit v :: BitVector n
v i :: Int
i        = BitVector n -> Int -> Bit -> BitVector n
forall (n :: Nat).
KnownNat n =>
BitVector n -> Int -> Bit -> BitVector n
replaceBit# BitVector n
v Int
i Bit
high
  clearBit :: BitVector n -> Int -> BitVector n
clearBit v :: BitVector n
v i :: Int
i      = BitVector n -> Int -> Bit -> BitVector n
forall (n :: Nat).
KnownNat n =>
BitVector n -> Int -> Bit -> BitVector n
replaceBit# BitVector n
v Int
i Bit
low
  complementBit :: BitVector n -> Int -> BitVector n
complementBit v :: BitVector n
v i :: Int
i = BitVector n -> Int -> Bit -> BitVector n
forall (n :: Nat).
KnownNat n =>
BitVector n -> Int -> Bit -> BitVector n
replaceBit# BitVector n
v Int
i (Bit -> Bit
complement## (BitVector n -> Int -> Bit
forall (n :: Nat). KnownNat n => BitVector n -> Int -> Bit
index# BitVector n
v Int
i))
  testBit :: BitVector n -> Int -> Bool
testBit v :: BitVector n
v i :: Int
i       = Bit -> Bit -> Bool
eq## (BitVector n -> Int -> Bit
forall (n :: Nat). KnownNat n => BitVector n -> Int -> Bit
index# BitVector n
v Int
i) Bit
high
  bitSizeMaybe :: BitVector n -> Maybe Int
bitSizeMaybe v :: BitVector n
v    = Int -> Maybe Int
forall a. a -> Maybe a
Just (BitVector n -> Int
forall (n :: Nat). KnownNat n => BitVector n -> Int
size# BitVector n
v)
  bitSize :: BitVector n -> Int
bitSize           = BitVector n -> Int
forall (n :: Nat). KnownNat n => BitVector n -> Int
size#
  isSigned :: BitVector n -> Bool
isSigned _        = Bool
False
  shiftL :: BitVector n -> Int -> BitVector n
shiftL v :: BitVector n
v i :: Int
i        = BitVector n -> Int -> BitVector n
forall (n :: Nat). KnownNat n => BitVector n -> Int -> BitVector n
shiftL# BitVector n
v Int
i
  shiftR :: BitVector n -> Int -> BitVector n
shiftR v :: BitVector n
v i :: Int
i        = BitVector n -> Int -> BitVector n
forall (n :: Nat). KnownNat n => BitVector n -> Int -> BitVector n
shiftR# BitVector n
v Int
i
  rotateL :: BitVector n -> Int -> BitVector n
rotateL v :: BitVector n
v i :: Int
i       = BitVector n -> Int -> BitVector n
forall (n :: Nat). KnownNat n => BitVector n -> Int -> BitVector n
rotateL# BitVector n
v Int
i
  rotateR :: BitVector n -> Int -> BitVector n
rotateR v :: BitVector n
v i :: Int
i       = BitVector n -> Int -> BitVector n
forall (n :: Nat). KnownNat n => BitVector n -> Int -> BitVector n
rotateR# BitVector n
v Int
i
  popCount :: BitVector n -> Int
popCount bv :: BitVector n
bv       = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Index (n + 2) -> Integer
forall (n :: Nat). Index n -> Integer
I.toInteger# (BitVector (n + 1) -> Index (n + 2)
forall (n :: Nat). KnownNat n => BitVector (n + 1) -> Index (n + 2)
popCountBV (BitVector n
bv BitVector n -> BitVector 1 -> BitVector (n + 1)
forall (m :: Nat) (n :: Nat).
KnownNat m =>
BitVector n -> BitVector m -> BitVector (n + m)
++# (0 :: BitVector 1))))

instance KnownNat n => FiniteBits (BitVector n) where
  finiteBitSize :: BitVector n -> Int
finiteBitSize       = BitVector n -> Int
forall (n :: Nat). KnownNat n => BitVector n -> Int
size#
  countLeadingZeros :: BitVector n -> Int
countLeadingZeros   = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> (BitVector n -> Integer) -> BitVector n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (n + 1) -> Integer
forall (n :: Nat). Index n -> Integer
I.toInteger# (Index (n + 1) -> Integer)
-> (BitVector n -> Index (n + 1)) -> BitVector n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector n -> Index (n + 1)
forall (n :: Nat). KnownNat n => BitVector n -> Index (n + 1)
countLeadingZerosBV
  countTrailingZeros :: BitVector n -> Int
countTrailingZeros  = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> (BitVector n -> Integer) -> BitVector n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (n + 1) -> Integer
forall (n :: Nat). Index n -> Integer
I.toInteger# (Index (n + 1) -> Integer)
-> (BitVector n -> Index (n + 1)) -> BitVector n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector n -> Index (n + 1)
forall (n :: Nat). KnownNat n => BitVector n -> Index (n + 1)
countTrailingZerosBV

countLeadingZerosBV :: KnownNat n => BitVector n -> I.Index (n+1)
countLeadingZerosBV :: BitVector n -> Index (n + 1)
countLeadingZerosBV = (Bit -> Index (n + 1) -> Index (n + 1))
-> Index (n + 1) -> Vec n Bit -> Index (n + 1)
forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
V.foldr (\l :: Bit
l r :: Index (n + 1)
r -> if Bit -> Bit -> Bool
eq## Bit
l Bit
low then 1 Index (n + 1) -> Index (n + 1) -> Index (n + 1)
forall a. Num a => a -> a -> a
+ Index (n + 1)
r else 0) 0 (Vec n Bit -> Index (n + 1))
-> (BitVector n -> Vec n Bit) -> BitVector n -> Index (n + 1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector n -> Vec n Bit
forall (n :: Nat). KnownNat n => BitVector n -> Vec n Bit
V.bv2v
{-# INLINE countLeadingZerosBV #-}

countTrailingZerosBV :: KnownNat n => BitVector n -> I.Index (n+1)
countTrailingZerosBV :: BitVector n -> Index (n + 1)
countTrailingZerosBV = (Index (n + 1) -> Bit -> Index (n + 1))
-> Index (n + 1) -> Vec n Bit -> Index (n + 1)
forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
V.foldl (\l :: Index (n + 1)
l r :: Bit
r -> if Bit -> Bit -> Bool
eq## Bit
r Bit
low then 1 Index (n + 1) -> Index (n + 1) -> Index (n + 1)
forall a. Num a => a -> a -> a
+ Index (n + 1)
l else 0) 0 (Vec n Bit -> Index (n + 1))
-> (BitVector n -> Vec n Bit) -> BitVector n -> Index (n + 1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector n -> Vec n Bit
forall (n :: Nat). KnownNat n => BitVector n -> Vec n Bit
V.bv2v
{-# INLINE countTrailingZerosBV #-}

{-# NOINLINE reduceAnd# #-}
reduceAnd# :: KnownNat n => BitVector n -> Bit
reduceAnd# :: BitVector n -> Bit
reduceAnd# bv :: BitVector n
bv@(BV 0 i :: Integer
i) = Integer -> Integer -> Bit
Bit 0 (Int# -> Integer
smallInteger (Bool -> Int#
forall a. a -> Int#
dataToTag# Bool
check))
  where
    check :: Bool
check = Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
maxI

    sz :: Integer
sz    = BitVector n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal BitVector n
bv
    maxI :: Integer
maxI  = (2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
sz) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1
reduceAnd# bv :: BitVector n
bv = (Bit -> Bit -> Bit) -> Bit -> Vec n Bit -> Bit
forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
V.foldl Bit -> Bit -> Bit
forall a. Bits a => a -> a -> a
(.&.) 1 (BitVector n -> Vec n Bit
forall (n :: Nat). KnownNat n => BitVector n -> Vec n Bit
V.bv2v BitVector n
bv)

{-# NOINLINE reduceOr# #-}
reduceOr# :: KnownNat n => BitVector n -> Bit
reduceOr# :: BitVector n -> Bit
reduceOr# (BV 0 i :: Integer
i) = Integer -> Integer -> Bit
Bit 0 (Int# -> Integer
smallInteger (Bool -> Int#
forall a. a -> Int#
dataToTag# Bool
check))
  where
    check :: Bool
check = Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= 0
reduceOr# bv :: BitVector n
bv = (Bit -> Bit -> Bit) -> Bit -> Vec n Bit -> Bit
forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
V.foldl Bit -> Bit -> Bit
forall a. Bits a => a -> a -> a
(.|.) 0 (BitVector n -> Vec n Bit
forall (n :: Nat). KnownNat n => BitVector n -> Vec n Bit
V.bv2v BitVector n
bv)

{-# NOINLINE reduceXor# #-}
reduceXor# :: KnownNat n => BitVector n -> Bit
reduceXor# :: BitVector n -> Bit
reduceXor# (BV 0 i :: Integer
i) = Integer -> Integer -> Bit
Bit 0 (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Integer -> Int
forall a. Bits a => a -> Int
popCount Integer
i Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` 2))
reduceXor# bv :: BitVector n
bv = String -> BitVector n -> Bit
forall (n :: Nat) a.
(HasCallStack, KnownNat n) =>
String -> BitVector n -> a
undefErrorU "reduceXor" BitVector n
bv

instance Default (BitVector n) where
  def :: BitVector n
def = BitVector n
forall (n :: Nat). BitVector n
minBound#

-- * Accessors
-- ** Length information
{-# NOINLINE size# #-}
size# :: KnownNat n => BitVector n -> Int
size# :: BitVector n -> Int
size# bv :: BitVector n
bv = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (BitVector n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal BitVector n
bv)

{-# NOINLINE maxIndex# #-}
maxIndex# :: KnownNat n => BitVector n -> Int
maxIndex# :: BitVector n -> Int
maxIndex# bv :: BitVector n
bv = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (BitVector n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal BitVector n
bv) Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1

-- ** Indexing
{-# NOINLINE index# #-}
index# :: KnownNat n => BitVector n -> Int -> Bit
index# :: BitVector n -> Int -> Bit
index# bv :: BitVector n
bv@(BV m :: Integer
m v :: Integer
v) i :: Int
i
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
sz = Integer -> Integer -> Bit
Bit (Int# -> Integer
smallInteger (Bool -> Int#
forall a. a -> Int#
dataToTag# (Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
m Int
i)))
                             (Int# -> Integer
smallInteger (Bool -> Int#
forall a. a -> Int#
dataToTag# (Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
v Int
i)))
    | Bool
otherwise        = Bit
err
  where
    sz :: Int
sz  = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (BitVector n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal BitVector n
bv)
    err :: Bit
err = String -> Bit
forall a. HasCallStack => String -> a
error (String -> Bit) -> String -> Bit
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [ "(!): "
                         , Int -> String
forall a. Show a => a -> String
show Int
i
                         , " is out of range ["
                         , Int -> String
forall a. Show a => a -> String
show (Int
sz Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1)
                         , "..0]"
                         ]

{-# NOINLINE msb# #-}
-- | MSB
msb# :: forall n . KnownNat n => BitVector n -> Bit
msb# :: BitVector n -> Bit
msb# (BV m :: Integer
m v :: Integer
v)
  = let i :: Int
i = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1)
    in  Integer -> Integer -> Bit
Bit (Int# -> Integer
smallInteger (Bool -> Int#
forall a. a -> Int#
dataToTag# (Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
m Int
i)))
            (Int# -> Integer
smallInteger (Bool -> Int#
forall a. a -> Int#
dataToTag# (Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
v Int
i)))

{-# NOINLINE lsb# #-}
-- | LSB
lsb# :: BitVector n -> Bit
lsb# :: BitVector n -> Bit
lsb# (BV m :: Integer
m v :: Integer
v) = Integer -> Integer -> Bit
Bit (Int# -> Integer
smallInteger (Bool -> Int#
forall a. a -> Int#
dataToTag# (Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
m 0)))
                    (Int# -> Integer
smallInteger (Bool -> Int#
forall a. a -> Int#
dataToTag# (Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
v 0)))

{-# NOINLINE slice# #-}
slice# :: BitVector (m + 1 + i) -> SNat m -> SNat n -> BitVector (m + 1 - n)
slice# :: BitVector ((m + 1) + i)
-> SNat m -> SNat n -> BitVector ((m + 1) - n)
slice# (BV msk :: Integer
msk i :: Integer
i) m :: SNat m
m n :: SNat n
n = Integer -> Integer -> BitVector ((m + 1) - n)
forall (n :: Nat). Integer -> Integer -> BitVector n
BV (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftR (Integer
msk Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask) Int
n')
                           (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftR (Integer
i   Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask) Int
n')
  where
    m' :: Integer
m' = SNat m -> Integer
forall (n :: Nat). SNat n -> Integer
snatToInteger SNat m
m
    n' :: Int
n' = SNat n -> Int
forall a (n :: Nat). Num a => SNat n -> a
snatToNum SNat n
n

    mask :: Integer
mask = 2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
m' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1

-- * Constructions

-- ** Concatenation
{-# NOINLINE (++#) #-}
-- | Concatenate two 'BitVector's
(++#) :: KnownNat m => BitVector n -> BitVector m -> BitVector (n + m)
(BV m1 :: Integer
m1 v1 :: Integer
v1) ++# :: BitVector n -> BitVector m -> BitVector (n + m)
++# bv2 :: BitVector m
bv2@(BV m2 :: Integer
m2 v2 :: Integer
v2) = Integer -> Integer -> BitVector (n + m)
forall (n :: Nat). Integer -> Integer -> BitVector n
BV (Integer
m1' Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
m2) (Integer
v1' Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
v2)
  where
    size2 :: Int
size2 = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (BitVector m -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal BitVector m
bv2)
    v1' :: Integer
v1' = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
v1 Int
size2
    m1' :: Integer
m1' = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
m1 Int
size2

-- * Modifying BitVectors
{-# NOINLINE replaceBit# #-}
replaceBit# :: KnownNat n => BitVector n -> Int -> Bit -> BitVector n
replaceBit# :: BitVector n -> Int -> Bit -> BitVector n
replaceBit# bv :: BitVector n
bv@(BV m :: Integer
m v :: Integer
v) i :: Int
i (Bit mb :: Integer
mb b :: Integer
b)
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
sz = Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
clearBit Integer
m Int
i  Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. (Integer
mb Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
i))
                            (if Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
b 0 Bool -> Bool -> Bool
&& Integer
mb Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
setBit Integer
v Int
i else Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
clearBit Integer
v Int
i)
    | Bool
otherwise        = BitVector n
err
  where
    sz :: Int
sz   = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (BitVector n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal BitVector n
bv)
    err :: BitVector n
err  = String -> BitVector n
forall a. HasCallStack => String -> a
error (String -> BitVector n) -> String -> BitVector n
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [ "replaceBit: "
                          , Int -> String
forall a. Show a => a -> String
show Int
i
                          , " is out of range ["
                          , Int -> String
forall a. Show a => a -> String
show (Int
sz Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1)
                          , "..0]"
                          ]

{-# NOINLINE setSlice# #-}
setSlice#
  :: BitVector (m + 1 + i)
  -> SNat m
  -> SNat n
  -> BitVector (m + 1 - n)
  -> BitVector (m + 1 + i)
setSlice# :: BitVector ((m + 1) + i)
-> SNat m
-> SNat n
-> BitVector ((m + 1) - n)
-> BitVector ((m + 1) + i)
setSlice# (BV iMask :: Integer
iMask i :: Integer
i) m :: SNat m
m n :: SNat n
n (BV jMask :: Integer
jMask j :: Integer
j) = Integer -> Integer -> BitVector ((m + 1) + i)
forall (n :: Nat). Integer -> Integer -> BitVector n
BV ((Integer
iMask Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
jMask')
                                             ((Integer
i     Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
j')
  where
    m' :: Integer
m' = SNat m -> Integer
forall (n :: Nat). SNat n -> Integer
snatToInteger SNat m
m
    n' :: Integer
n' = SNat n -> Integer
forall (n :: Nat). SNat n -> Integer
snatToInteger SNat n
n

    j' :: Integer
j'     = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
j     (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n')
    jMask' :: Integer
jMask' = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
jMask (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n')
    mask :: Integer
mask = Integer -> Integer
forall a. Bits a => a -> a
complement ((2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
m' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` (2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
n' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1))

{-# NOINLINE split# #-}
split#
  :: forall n m
   . KnownNat n
  => BitVector (m + n)
  -> (BitVector m, BitVector n)
split# :: BitVector (m + n) -> (BitVector m, BitVector n)
split# (BV m :: Integer
m i :: Integer
i) = (Integer -> Integer -> BitVector m
forall (n :: Nat). Integer -> Integer -> BitVector n
BV Integer
lMask Integer
l, Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV Integer
rMask Integer
r)
  where
    n :: Int
n     = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
    mask :: Integer
mask  = 1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
n
    -- The code below is faster than:
    -- > (l,r) = i `divMod` mask
    r :: Integer
r     = Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
mask
    rMask :: Integer
rMask = Integer
m Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
mask
    l :: Integer
l     = Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
n
    lMask :: Integer
lMask = Integer
m Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
n


and#, or#, xor# :: BitVector n -> BitVector n -> BitVector n
{-# NOINLINE and# #-}
and# :: BitVector n -> BitVector n -> BitVector n
and# (BV m1 :: Integer
m1 v1 :: Integer
v1) (BV m2 :: Integer
m2 v2 :: Integer
v2) = Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV Integer
mask (Integer
v1 Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
v2  Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
mask)
  where
    mask :: Integer
mask = (Integer
m1Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&.Integer
v2 Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
m1Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&.Integer
m2 Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
m2Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&.Integer
v1)

{-# NOINLINE or# #-}
or# :: BitVector n -> BitVector n -> BitVector n
or# (BV m1 :: Integer
m1 v1 :: Integer
v1) (BV m2 :: Integer
m2 v2 :: Integer
v2) = Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV Integer
mask ((Integer
v1Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|.Integer
v2) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
mask)
  where
    mask :: Integer
mask = Integer
m1 Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
v2  Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|.  Integer
m1Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&.Integer
m2  Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|.  Integer
m2 Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
v1

{-# NOINLINE xor# #-}
xor# :: BitVector n -> BitVector n -> BitVector n
xor# (BV m1 :: Integer
m1 v1 :: Integer
v1) (BV m2 :: Integer
m2 v2 :: Integer
v2) = Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV Integer
mask ((Integer
v1 Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer
v2) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
mask)
  where
    mask :: Integer
mask = Integer
m1 Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
m2


{-# NOINLINE complement# #-}
complement# :: KnownNat n => BitVector n -> BitVector n
complement# :: BitVector n -> BitVector n
complement# (BV m :: Integer
m v :: Integer
v) = Integer -> Integer -> BitVector n
forall (n :: Nat). KnownNat n => Integer -> Integer -> BitVector n
fromInteger_INLINE Integer
m (Integer -> Integer
forall a. Bits a => a -> a
complement Integer
v Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
m)

shiftL#, shiftR#, rotateL#, rotateR#
  :: KnownNat n => BitVector n -> Int -> BitVector n

{-# NOINLINE shiftL# #-}
shiftL# :: BitVector n -> Int -> BitVector n
shiftL# (BV m :: Integer
m v :: Integer
v) i :: Int
i
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0     = String -> BitVector n
forall a. HasCallStack => String -> a
error
              (String -> BitVector n) -> String -> BitVector n
forall a b. (a -> b) -> a -> b
$ "'shiftL undefined for negative number: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
  | Bool
otherwise = Integer -> Integer -> BitVector n
forall (n :: Nat). KnownNat n => Integer -> Integer -> BitVector n
fromInteger_INLINE (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
m Int
i) (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
v Int
i)

{-# NOINLINE shiftR# #-}
shiftR# :: BitVector n -> Int -> BitVector n
shiftR# (BV m :: Integer
m v :: Integer
v) i :: Int
i
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0     = String -> BitVector n
forall a. HasCallStack => String -> a
error
              (String -> BitVector n) -> String -> BitVector n
forall a b. (a -> b) -> a -> b
$ "'shiftR undefined for negative number: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
  | Bool
otherwise = Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftR Integer
m Int
i) (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftR Integer
v Int
i)

{-# NOINLINE rotateL# #-}
rotateL# :: BitVector n -> Int -> BitVector n
rotateL# _ b :: Int
b | Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0   = String -> BitVector n
forall a. HasCallStack => String -> a
error "'shiftL undefined for negative numbers"
rotateL# bv :: BitVector n
bv@(BV m :: Integer
m v :: Integer
v) b :: Int
b = Integer -> Integer -> BitVector n
forall (n :: Nat). KnownNat n => Integer -> Integer -> BitVector n
fromInteger_INLINE (Integer
ml Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
mr) (Integer
vl Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
vr)
  where
    vl :: Integer
vl    = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
v Int
b'
    vr :: Integer
vr    = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftR Integer
v Int
b''

    ml :: Integer
ml    = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
m Int
b'
    mr :: Integer
mr    = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftR Integer
m Int
b''

    b' :: Int
b'   = Int
b Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
sz
    b'' :: Int
b''  = Int
sz Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
b'
    sz :: Int
sz   = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (BitVector n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal BitVector n
bv)

{-# NOINLINE rotateR# #-}
rotateR# :: BitVector n -> Int -> BitVector n
rotateR# _ b :: Int
b | Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0   = String -> BitVector n
forall a. HasCallStack => String -> a
error "'shiftR undefined for negative numbers"
rotateR# bv :: BitVector n
bv@(BV m :: Integer
m v :: Integer
v) b :: Int
b = Integer -> Integer -> BitVector n
forall (n :: Nat). KnownNat n => Integer -> Integer -> BitVector n
fromInteger_INLINE (Integer
ml Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
mr) (Integer
vl Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
vr)
  where
    vl :: Integer
vl   = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftR Integer
v Int
b'
    vr :: Integer
vr   = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
v Int
b''
    ml :: Integer
ml   = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftR Integer
m Int
b'
    mr :: Integer
mr   = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
m Int
b''

    b' :: Int
b'  = Int
b Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
sz
    b'' :: Int
b'' = Int
sz Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
b'
    sz :: Int
sz  = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (BitVector n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal BitVector n
bv)

popCountBV :: forall n . KnownNat n => BitVector (n+1) -> I.Index (n+2)
popCountBV :: BitVector (n + 1) -> Index (n + 2)
popCountBV bv :: BitVector (n + 1)
bv =
  let v :: Vec (n + 1) Bit
v = BitVector (n + 1) -> Vec (n + 1) Bit
forall (n :: Nat). KnownNat n => BitVector n -> Vec n Bit
V.bv2v BitVector (n + 1)
bv
  in  Vec (n + 1) (Index (n + 2)) -> Index (n + 2)
forall (t :: Type -> Type) a. (Foldable t, Num a) => t a -> a
sum ((Bit -> Index (n + 2))
-> Vec (n + 1) Bit -> Vec (n + 1) (Index (n + 2))
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
V.map (BitVector 1 -> Index (n + 2)
forall a b. (Integral a, Num b) => a -> b
fromIntegral (BitVector 1 -> Index (n + 2))
-> (Bit -> BitVector 1) -> Bit -> Index (n + 2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bit -> BitVector 1
pack#) Vec (n + 1) Bit
v)
{-# INLINE popCountBV #-}

instance Resize BitVector where
  resize :: BitVector a -> BitVector b
resize     = BitVector a -> BitVector b
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
BitVector n -> BitVector m
resizeBV
  zeroExtend :: BitVector a -> BitVector (b + a)
zeroExtend = (0 BitVector b -> BitVector a -> BitVector (b + a)
forall (m :: Nat) (n :: Nat).
KnownNat m =>
BitVector n -> BitVector m -> BitVector (n + m)
++#)
  signExtend :: BitVector a -> BitVector (b + a)
signExtend = \bv :: BitVector a
bv -> (if BitVector a -> Bit
forall (n :: Nat). KnownNat n => BitVector n -> Bit
msb# BitVector a
bv Bit -> Bit -> Bool
forall a. Eq a => a -> a -> Bool
== Bit
low then BitVector b -> BitVector b
forall a. a -> a
id else BitVector b -> BitVector b
forall a. Bits a => a -> a
complement) 0 BitVector b -> BitVector a -> BitVector (b + a)
forall (m :: Nat) (n :: Nat).
KnownNat m =>
BitVector n -> BitVector m -> BitVector (n + m)
++# BitVector a
bv
  truncateB :: BitVector (a + b) -> BitVector a
truncateB  = BitVector (a + b) -> BitVector a
forall (a :: Nat) (b :: Nat).
KnownNat a =>
BitVector (a + b) -> BitVector a
truncateB#

resizeBV :: forall n m . (KnownNat n, KnownNat m) => BitVector n -> BitVector m
resizeBV :: BitVector n -> BitVector m
resizeBV = case SNat n -> SNat m -> SNatLE n m
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
compareSNat @n @m (KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat @n) (KnownNat m => SNat m
forall (n :: Nat). KnownNat n => SNat n
SNat @m) of
  SNatLE -> BitVector (m - n) -> BitVector n -> BitVector ((m - n) + n)
forall (m :: Nat) (n :: Nat).
KnownNat m =>
BitVector n -> BitVector m -> BitVector (n + m)
(++#) @n @(m-n) 0
  SNatGT -> KnownNat m => BitVector (m + (n - m)) -> BitVector m
forall (a :: Nat) (b :: Nat).
KnownNat a =>
BitVector (a + b) -> BitVector a
truncateB# @m @(n - m)
{-# INLINE resizeBV #-}

truncateB# :: forall a b . KnownNat a => BitVector (a + b) -> BitVector a
truncateB# :: BitVector (a + b) -> BitVector a
truncateB# (BV msk :: Integer
msk i :: Integer
i) = Integer -> Integer -> BitVector a
forall (n :: Nat). KnownNat n => Integer -> Integer -> BitVector n
fromInteger_INLINE Integer
msk Integer
i
{-# NOINLINE truncateB# #-}

instance KnownNat n => Lift (BitVector n) where
  lift :: BitVector n -> Q Exp
lift bv :: BitVector n
bv@(BV m :: Integer
m i :: Integer
i) = Q Exp -> TypeQ -> Q Exp
sigE [| fromInteger# m i |] (Integer -> TypeQ
decBitVector (BitVector n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal BitVector n
bv))
  {-# NOINLINE lift #-}

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

instance KnownNat n => SaturatingNum (BitVector n) where
  satAdd :: SaturationMode -> BitVector n -> BitVector n -> BitVector n
satAdd SatWrap a :: BitVector n
a b :: BitVector n
b = BitVector n
a BitVector n -> BitVector n -> BitVector n
forall (n :: Nat).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
+# BitVector n
b
  satAdd SatZero a :: BitVector n
a b :: BitVector n
b =
    let r :: BitVector (Max n n + 1)
r = BitVector n -> BitVector n -> BitVector (Max n n + 1)
forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
BitVector m -> BitVector n -> BitVector (Max m n + 1)
plus# BitVector n
a BitVector n
b
    in  if BitVector (n + 1) -> Bit
forall (n :: Nat). KnownNat n => BitVector n -> Bit
msb# BitVector (n + 1)
BitVector (Max n n + 1)
r Bit -> Bit -> Bool
forall a. Eq a => a -> a -> Bool
== Bit
low
           then BitVector (n + 1) -> BitVector n
forall (a :: Nat) (b :: Nat).
KnownNat a =>
BitVector (a + b) -> BitVector a
truncateB# BitVector (n + 1)
BitVector (Max n n + 1)
r
           else BitVector n
forall (n :: Nat). BitVector n
minBound#
  satAdd _ a :: BitVector n
a b :: BitVector n
b =
    let r :: BitVector (Max n n + 1)
r  = BitVector n -> BitVector n -> BitVector (Max n n + 1)
forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
BitVector m -> BitVector n -> BitVector (Max m n + 1)
plus# BitVector n
a BitVector n
b
    in  if BitVector (n + 1) -> Bit
forall (n :: Nat). KnownNat n => BitVector n -> Bit
msb# BitVector (n + 1)
BitVector (Max n n + 1)
r Bit -> Bit -> Bool
forall a. Eq a => a -> a -> Bool
== Bit
low
           then BitVector (n + 1) -> BitVector n
forall (a :: Nat) (b :: Nat).
KnownNat a =>
BitVector (a + b) -> BitVector a
truncateB# BitVector (n + 1)
BitVector (Max n n + 1)
r
           else BitVector n
forall (n :: Nat). KnownNat n => BitVector n
maxBound#

  satSub :: SaturationMode -> BitVector n -> BitVector n -> BitVector n
satSub SatWrap a :: BitVector n
a b :: BitVector n
b = BitVector n
a BitVector n -> BitVector n -> BitVector n
forall (n :: Nat).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
-# BitVector n
b
  satSub _ a :: BitVector n
a b :: BitVector n
b =
    let r :: BitVector (Max n n + 1)
r = BitVector n -> BitVector n -> BitVector (Max n n + 1)
forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
BitVector m -> BitVector n -> BitVector (Max m n + 1)
minus# BitVector n
a BitVector n
b
    in  if BitVector (n + 1) -> Bit
forall (n :: Nat). KnownNat n => BitVector n -> Bit
msb# BitVector (n + 1)
BitVector (Max n n + 1)
r Bit -> Bit -> Bool
forall a. Eq a => a -> a -> Bool
== Bit
low
           then BitVector (n + 1) -> BitVector n
forall (a :: Nat) (b :: Nat).
KnownNat a =>
BitVector (a + b) -> BitVector a
truncateB# BitVector (n + 1)
BitVector (Max n n + 1)
r
           else BitVector n
forall (n :: Nat). BitVector n
minBound#

  satMul :: SaturationMode -> BitVector n -> BitVector n -> BitVector n
satMul SatWrap a :: BitVector n
a b :: BitVector n
b = BitVector n
a BitVector n -> BitVector n -> BitVector n
forall (n :: Nat).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
*# BitVector n
b
  satMul SatZero a :: BitVector n
a b :: BitVector n
b =
    let r :: BitVector (n + n)
r       = BitVector n -> BitVector n -> BitVector (n + n)
forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
BitVector m -> BitVector n -> BitVector (m + n)
times# BitVector n
a BitVector n
b
        (rL :: BitVector n
rL,rR :: BitVector n
rR) = BitVector (n + n) -> (BitVector n, BitVector n)
forall (n :: Nat) (m :: Nat).
KnownNat n =>
BitVector (m + n) -> (BitVector m, BitVector n)
split# BitVector (n + n)
r
    in  case BitVector n
rL of
          0 -> BitVector n
rR
          _ -> BitVector n
forall (n :: Nat). BitVector n
minBound#
  satMul _ a :: BitVector n
a b :: BitVector n
b =
    let r :: BitVector (n + n)
r       = BitVector n -> BitVector n -> BitVector (n + n)
forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
BitVector m -> BitVector n -> BitVector (m + n)
times# BitVector n
a BitVector n
b
        (rL :: BitVector n
rL,rR :: BitVector n
rR) = BitVector (n + n) -> (BitVector n, BitVector n)
forall (n :: Nat) (m :: Nat).
KnownNat n =>
BitVector (m + n) -> (BitVector m, BitVector n)
split# BitVector (n + n)
r
    in  case BitVector n
rL of
          0 -> BitVector n
rR
          _ -> BitVector n
forall (n :: Nat). KnownNat n => BitVector n
maxBound#

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

-- | 'shrink' for sized unsigned types
shrinkSizedUnsigned :: (KnownNat n, Integral (p n)) => p n -> [p n]
shrinkSizedUnsigned :: p n -> [p n]
shrinkSizedUnsigned x :: p n
x | p n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal p n
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 2 = case p n -> Integer
forall a. Integral a => a -> Integer
toInteger p n
x of
                                         1 -> [0]
                                         _ -> []
                      -- 'shrinkIntegral' uses "`quot` 2", which for sized types
                      -- less than 2 bits wide results in a division by zero.
                      --
                      -- See: https://github.com/clash-lang/clash-compiler/issues/153
                      | Bool
otherwise    = p n -> [p n]
forall a. Integral a => a -> [a]
shrinkIntegral p n
x
{-# INLINE shrinkSizedUnsigned #-}

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

type instance Index   (BitVector n) = Int
type instance IxValue (BitVector n) = Bit
instance KnownNat n => Ixed (BitVector n) where
  ix :: Index (BitVector n)
-> Traversal' (BitVector n) (IxValue (BitVector n))
ix i :: Index (BitVector n)
i f :: IxValue (BitVector n) -> f (IxValue (BitVector n))
f bv :: BitVector n
bv = BitVector n -> Int -> Bit -> BitVector n
forall (n :: Nat).
KnownNat n =>
BitVector n -> Int -> Bit -> BitVector n
replaceBit# BitVector n
bv Int
Index (BitVector n)
i (Bit -> BitVector n) -> f Bit -> f (BitVector n)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IxValue (BitVector n) -> f (IxValue (BitVector n))
f (BitVector n -> Int -> Bit
forall (n :: Nat). KnownNat n => BitVector n -> Int -> Bit
index# BitVector n
bv Int
Index (BitVector n)
i)


-- error for infix operator
undefErrorI :: (HasCallStack, KnownNat m, KnownNat n) => String -> BitVector m -> BitVector n -> a
undefErrorI :: String -> BitVector m -> BitVector n -> a
undefErrorI op :: String
op bv1 :: BitVector m
bv1 bv2 :: BitVector n
bv2 = (HasCallStack => a) -> a
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => a) -> a) -> (HasCallStack => a) -> a
forall a b. (a -> b) -> a -> b
$
  String -> a
forall a. HasCallStack => String -> a
errorX (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ "Clash.Sized.BitVector." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
op
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ " called with (partially) undefined arguments: "
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ BitVector m -> String
forall a. Show a => a -> String
show BitVector m
bv1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
op String -> ShowS
forall a. [a] -> [a] -> [a]
++" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ BitVector n -> String
forall a. Show a => a -> String
show BitVector n
bv2

-- error for prefix operator/function
undefErrorP :: (HasCallStack, KnownNat m, KnownNat n) => String -> BitVector m -> BitVector n -> a
undefErrorP :: String -> BitVector m -> BitVector n -> a
undefErrorP op :: String
op bv1 :: BitVector m
bv1 bv2 :: BitVector n
bv2 = (HasCallStack => a) -> a
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => a) -> a) -> (HasCallStack => a) -> a
forall a b. (a -> b) -> a -> b
$
  String -> a
forall a. HasCallStack => String -> a
errorX (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ "Clash.Sized.BitVector." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
op
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ " called with (partially) undefined arguments: "
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ BitVector m -> String
forall a. Show a => a -> String
show BitVector m
bv1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ BitVector n -> String
forall a. Show a => a -> String
show BitVector n
bv2

-- error for prefix operator/function
undefErrorP3 :: (HasCallStack, KnownNat m, KnownNat n, KnownNat o) => String -> BitVector m -> BitVector n -> BitVector o -> a
undefErrorP3 :: String -> BitVector m -> BitVector n -> BitVector o -> a
undefErrorP3 op :: String
op bv1 :: BitVector m
bv1 bv2 :: BitVector n
bv2 bv3 :: BitVector o
bv3 = (HasCallStack => a) -> a
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => a) -> a) -> (HasCallStack => a) -> a
forall a b. (a -> b) -> a -> b
$
  String -> a
forall a. HasCallStack => String -> a
errorX (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ "Clash.Sized.BitVector." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
op
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ " called with (partially) undefined arguments: "
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ BitVector m -> String
forall a. Show a => a -> String
show BitVector m
bv1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ BitVector n -> String
forall a. Show a => a -> String
show BitVector n
bv2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ BitVector o -> String
forall a. Show a => a -> String
show BitVector o
bv3

-- error for unary operator/function
undefErrorU :: (HasCallStack, KnownNat n) => String -> BitVector n -> a
-- undefErrorU op bv1 = undefError ("Clash.Sized.BitVector." ++ op) [bv1]
undefErrorU :: String -> BitVector n -> a
undefErrorU op :: String
op bv1 :: BitVector n
bv1 = (HasCallStack => a) -> a
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => a) -> a) -> (HasCallStack => a) -> a
forall a b. (a -> b) -> a -> b
$
  String -> a
forall a. HasCallStack => String -> a
errorX (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ "Clash.Sized.BitVector." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
op
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ " called with (partially) undefined argument: "
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ BitVector n -> String
forall a. Show a => a -> String
show BitVector n
bv1

undefError :: (HasCallStack, KnownNat n) => String -> [BitVector n] -> a
undefError :: String -> [BitVector n] -> a
undefError op :: String
op bvs :: [BitVector n]
bvs = (HasCallStack => a) -> a
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => a) -> a) -> (HasCallStack => a) -> a
forall a b. (a -> b) -> a -> b
$
  String -> a
forall a. HasCallStack => String -> a
errorX (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
op
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ " called with (partially) undefined arguments: "
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((BitVector n -> String) -> [BitVector n] -> [String]
forall a b. (a -> b) -> [a] -> [b]
L.map BitVector n -> String
forall a. Show a => a -> String
show [BitVector n]
bvs)


-- | Implement BitVector undefinedness checking for unpack funtions
checkUnpackUndef :: (KnownNat n, Typeable a)
                 => (BitVector n -> a) -- ^ unpack function
                 -> BitVector n -> a
checkUnpackUndef :: (BitVector n -> a) -> BitVector n -> a
checkUnpackUndef f :: BitVector n -> a
f bv :: BitVector n
bv@(BV 0 _) = BitVector n -> a
f BitVector n
bv
checkUnpackUndef _ bv :: BitVector n
bv = a
res
  where
    ty :: TypeRep
ty = a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf a
res
    res :: a
res = String -> [BitVector n] -> a
forall (n :: Nat) a.
(HasCallStack, KnownNat n) =>
String -> [BitVector n] -> a
undefError (TypeRep -> String
forall a. Show a => a -> String
show TypeRep
ty String -> ShowS
forall a. [a] -> [a] -> [a]
++ ".unpack") [BitVector n
bv]
{-# NOINLINE checkUnpackUndef #-}

-- | Create a BitVector with all its bits undefined
undefined# :: forall n . KnownNat n => BitVector n
undefined# :: BitVector n
undefined# =
  let m :: Integer
m = 1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
  in  Integer -> Integer -> BitVector n
forall (n :: Nat). Integer -> Integer -> BitVector n
BV (Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-1) 0
{-# NOINLINE undefined# #-}

-- | Check if one BitVector is like another.
-- NFDataX bits in the second argument are interpreted as don't care bits.
--
-- >>> let expected = $$(bLit "1.") :: BitVector 2
-- >>> let checked  = $$(bLit "11") :: BitVector 2
-- >>> checked  `isLike` expected
-- True
-- >>> expected `isLike` checked
-- False
--
-- __NB__: Not synthesizable
isLike :: BitVector n -> BitVector n -> Bool
isLike :: BitVector n -> BitVector n -> Bool
isLike (BV cMask :: Integer
cMask c :: Integer
c) (BV eMask :: Integer
eMask e :: Integer
e) = Integer
e' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
c' Bool -> Bool -> Bool
&& Integer
e' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
c''
  where
    -- | set don't care bits to 0
    e' :: Integer
e' = Integer
e Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
eMask

    -- | checked with undefined bits set to 0
    c' :: Integer
c' = (Integer
c Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
cMask) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
eMask
    -- | checked with undefined bits set to 1
    c'' :: Integer
c'' = (Integer
c Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
cMask) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer -> Integer
forall a. Bits a => a -> a
complement Integer
eMask
{-# NOINLINE isLike #-}

fromBits :: [Bit] -> Integer
fromBits :: [Bit] -> Integer
fromBits = (Integer -> Bit -> Integer) -> Integer -> [Bit] -> Integer
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl (\v :: Integer
v b :: Bit
b -> Integer
v Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` 1 Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Bit -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Bit
b) 0

-- | Template Haskell macro for generating a pattern matching on some
-- bits of a value.
--
-- This macro compiles to an efficient view pattern that matches the
-- bits of a given value against the bits specified in the
-- pattern. The scrutinee can be any type that is an instance of the
-- 'Num', 'Bits' and 'Eq' typeclasses.
--
-- The bit pattern is specified by a string which contains @\'0\'@ or
-- @\'1\'@ for matching a bit, or @\'.\'@ for bits which are not matched.
--
-- The following example matches a byte against two bit patterns where
-- some bits are relevant and others are not:
--
-- @
--   decode :: Unsigned 8 -> Maybe Bool
--   decode $(bitPattern "00...110") = Just True
--   decode $(bitPattern "10..0001") = Just False
--   decode _ = Nothing
-- @
bitPattern :: String -> Q Pat
bitPattern :: String -> Q Pat
bitPattern s :: String
s = [p| (($mask .&.) -> $target) |]
  where
    bs :: [Maybe Bit]
bs = Char -> Maybe Bit
forall a. Num a => Char -> Maybe a
parse (Char -> Maybe Bit) -> String -> [Maybe Bit]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> String
s

    mask :: Q Exp
mask = Lit -> Q Exp
litE (Lit -> Q Exp) -> ([Bit] -> Lit) -> [Bit] -> Q Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Lit
IntegerL (Integer -> Lit) -> ([Bit] -> Integer) -> [Bit] -> Lit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Bit] -> Integer
fromBits ([Bit] -> Q Exp) -> [Bit] -> Q Exp
forall a b. (a -> b) -> a -> b
$ Bit -> (Bit -> Bit) -> Maybe Bit -> Bit
forall b a. b -> (a -> b) -> Maybe a -> b
maybe 0 (Bit -> Bit -> Bit
forall a b. a -> b -> a
const 1) (Maybe Bit -> Bit) -> [Maybe Bit] -> [Bit]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Maybe Bit]
bs
    target :: Q Pat
target = Lit -> Q Pat
litP (Lit -> Q Pat) -> ([Bit] -> Lit) -> [Bit] -> Q Pat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Lit
IntegerL (Integer -> Lit) -> ([Bit] -> Integer) -> [Bit] -> Lit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Bit] -> Integer
fromBits ([Bit] -> Q Pat) -> [Bit] -> Q Pat
forall a b. (a -> b) -> a -> b
$ Bit -> Maybe Bit -> Bit
forall a. a -> Maybe a -> a
fromMaybe 0 (Maybe Bit -> Bit) -> [Maybe Bit] -> [Bit]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Maybe Bit]
bs

    parse :: Char -> Maybe a
parse '.' = Maybe a
forall a. Maybe a
Nothing
    parse '0' = a -> Maybe a
forall a. a -> Maybe a
Just 0
    parse '1' = a -> Maybe a
forall a. a -> Maybe a
Just 1
    parse c :: Char
c = String -> Maybe a
forall a. HasCallStack => String -> a
error (String -> Maybe a) -> String -> Maybe a
forall a b. (a -> b) -> a -> b
$ "Invalid bit pattern: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. Show a => a -> String
show Char
c