{-|
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 CPP #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleContexts #-}
{-# 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.Exts
  (Word#, Word (W#), eqWord#, int2Word#, uncheckedShiftRL#)
import qualified GHC.Exts
import GHC.Integer.GMP.Internals  (Integer (..), bigNatToWord, shiftRBigNat)
import GHC.Natural
  (Natural (..), naturalFromInteger, wordToNatural)
#if MIN_VERSION_base(4,12,0)
import GHC.Natural                (naturalToInteger)
#endif
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(..))
#if MIN_VERSION_template_haskell(2,16,0)
import Language.Haskell.TH.Compat
#endif
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, natToNum)
import Clash.XException
  (ShowX (..), NFDataX (..), errorX, isX, showsPrecXWith, rwhnfX)

import Clash.Sized.Internal.Mod

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
>>> import Clash.Sized.Internal.BitVector
-}

-- * 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 -> Natural
unsafeMask      :: !Natural
       , BitVector n -> Natural
unsafeToNatural :: !Natural
       }
  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 -> Word
unsafeMask#      :: {-# unpack #-} !Word
      , Bit -> Word
unsafeToInteger# :: {-# unpack #-} !Word
      }
  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 = Word -> Word -> Bit
Bit Word
0 Word
1

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

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

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

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 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 -> Word
unsafeMask# Bit
bv Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
/= Word
0

instance Lift Bit where
  lift :: Bit -> Q Exp
lift (Bit Word
m Word
i) = [| fromInteger## $(litE (WordPrimL (toInteger m))) i |]
  {-# NOINLINE lift #-}
#if MIN_VERSION_template_haskell(2,16,0)
  liftTyped :: Bit -> Q (TExp Bit)
liftTyped = Bit -> Q (TExp Bit)
forall a. Lift a => a -> Q (TExp a)
liftTypedFromUntyped
#endif

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## Bit
b1 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## Bit
b1 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## Bit
b1 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## Bit
b1 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## Bit
b1 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## Bit
b1 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     = Word# -> Integer -> Bit
fromInteger## Word#
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 Bit
b = if Bit -> Bit -> Bool
eq## Bit
b Bit
low then Int
0 else Int
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 Bit
b    = Bit
b
  fromInteger :: Integer -> Bit
fromInteger = Word# -> Integer -> Bit
fromInteger## Word#
0##

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

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

instance Integral Bit where
  quot :: Bit -> Bit -> Bit
quot    Bit
a Bit
_ = Bit
a
  rem :: Bit -> Bit -> Bit
rem     Bit
_ Bit
_ = Bit
low
  div :: Bit -> Bit -> Bit
div     Bit
a Bit
_ = Bit
a
  mod :: Bit -> Bit -> Bit
mod     Bit
_ Bit
_ = Bit
low
  quotRem :: Bit -> Bit -> (Bit, Bit)
quotRem Bit
n Bit
_ = (Bit
n,Bit
low)
  divMod :: Bit -> Bit -> (Bit, Bit)
divMod  Bit
n Bit
_ = (Bit
n,Bit
low)
  toInteger :: Bit -> Integer
toInteger Bit
b = if Bit -> Bit -> Bool
eq## Bit
b Bit
low then Integer
0 else Integer
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 Int
i             = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Bit
high else Bit
low
  setBit :: Bit -> Int -> Bit
setBit Bit
b Int
i        = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Bit
high else Bit
b
  clearBit :: Bit -> Int -> Bit
clearBit Bit
b Int
i      = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Bit
low  else Bit
b
  complementBit :: Bit -> Int -> Bit
complementBit Bit
b Int
i = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Bit -> Bit
complement## Bit
b else Bit
b
  testBit :: Bit -> Int -> Bool
testBit Bit
b Int
i       = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Bit -> Bit -> Bool
eq## Bit
b Bit
high else Bool
False
  bitSizeMaybe :: Bit -> Maybe Int
bitSizeMaybe Bit
_    = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1
  bitSize :: Bit -> Int
bitSize Bit
_         = Int
1
  isSigned :: Bit -> Bool
isSigned Bit
_        = Bool
False
  shiftL :: Bit -> Int -> Bit
shiftL Bit
b Int
i        = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Bit
b else Bit
low
  shiftR :: Bit -> Int -> Bit
shiftR Bit
b Int
i        = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Bit
b else Bit
low
  rotateL :: Bit -> Int -> Bit
rotateL Bit
b Int
_       = Bit
b
  rotateR :: Bit -> Int -> Bit
rotateR Bit
b Int
_       = Bit
b
  popCount :: Bit -> Int
popCount Bit
b        = if Bit -> Bit -> Bool
eq## Bit
b Bit
low then Int
0 else Int
1

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

and##, or##, xor## :: Bit -> Bit -> Bit
and## :: Bit -> Bit -> Bit
and## (Bit Word
m1 Word
v1) (Bit Word
m2 Word
v2) = Word -> Word -> Bit
Bit Word
mask (Word
v1 Word -> Word -> Word
forall a. Bits a => a -> a -> a
.&. Word
v2 Word -> Word -> Word
forall a. Bits a => a -> a -> a
.&. Word -> Word
forall a. Bits a => a -> a
complement Word
mask)
  where mask :: Word
mask = (Word
m1Word -> Word -> Word
forall a. Bits a => a -> a -> a
.&.Word
v2 Word -> Word -> Word
forall a. Bits a => a -> a -> a
.|. Word
m1Word -> Word -> Word
forall a. Bits a => a -> a -> a
.&.Word
m2 Word -> Word -> Word
forall a. Bits a => a -> a -> a
.|. Word
m2Word -> Word -> Word
forall a. Bits a => a -> a -> a
.&.Word
v1)
{-# NOINLINE and## #-}

or## :: Bit -> Bit -> Bit
or## (Bit Word
m1 Word
v1) (Bit Word
m2 Word
v2) = Word -> Word -> Bit
Bit Word
mask ((Word
v1 Word -> Word -> Word
forall a. Bits a => a -> a -> a
.|. Word
v2) Word -> Word -> Word
forall a. Bits a => a -> a -> a
.&. Word -> Word
forall a. Bits a => a -> a
complement Word
mask)
  where mask :: Word
mask = Word
m1 Word -> Word -> Word
forall a. Bits a => a -> a -> a
.&. Word -> Word
forall a. Bits a => a -> a
complement Word
v2 Word -> Word -> Word
forall a. Bits a => a -> a -> a
.|.  Word
m1Word -> Word -> Word
forall a. Bits a => a -> a -> a
.&.Word
m2  Word -> Word -> Word
forall a. Bits a => a -> a -> a
.|.  Word
m2 Word -> Word -> Word
forall a. Bits a => a -> a -> a
.&. Word -> Word
forall a. Bits a => a -> a
complement Word
v1
{-# NOINLINE or## #-}

xor## :: Bit -> Bit -> Bit
xor## (Bit Word
m1 Word
v1) (Bit Word
m2 Word
v2) = Word -> Word -> Bit
Bit Word
mask ((Word
v1 Word -> Word -> Word
forall a. Bits a => a -> a -> a
`xor` Word
v2) Word -> Word -> Word
forall a. Bits a => a -> a -> a
.&. Word -> Word
forall a. Bits a => a -> a
complement Word
mask)
  where mask :: Word
mask = Word
m1 Word -> Word -> Word
forall a. Bits a => a -> a -> a
.|. Word
m2
{-# NOINLINE xor## #-}

complement## :: Bit -> Bit
complement## :: Bit -> Bit
complement## (Bit Word
m Word
v) = Word -> Word -> Bit
Bit Word
m (Word -> Word
complementB Word
v Word -> Word -> Word
forall a. Bits a => a -> a -> a
.&. Word -> Word
complementB Word
m)
  where complementB :: Word -> Word
complementB (W# Word#
b#) = Word# -> Word
W# (Int# -> Word#
int2Word# (Word# -> Word# -> Int#
eqWord# Word#
b# Word#
0##))
{-# NOINLINE complement## #-}

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

unpack# :: BitVector 1 -> Bit
unpack# :: BitVector 1 -> Bit
unpack# (BV Natural
m Natural
b) = Word -> Word -> Bit
Bit (Natural -> Word
go Natural
m) (Natural -> Word
go Natural
b)
 where
  go :: Natural -> Word
go (NatS# Word#
w) = Word# -> Word
W# Word#
w
  go (NatJ# BigNat
w) = Word# -> Word
W# (BigNat -> Word#
bigNatToWord BigNat
w)
{-# NOINLINE unpack# #-}

-- * Instances
instance NFData (BitVector n) where
  rnf :: BitVector n -> ()
rnf (BV Natural
i Natural
m) = Natural -> ()
forall a. NFData a => a -> ()
rnf Natural
i () -> () -> ()
`seq` Natural -> ()
forall a. NFData a => a -> ()
rnf Natural
m () -> () -> ()
`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 Natural
msk Natural
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 -> Natural -> Natural -> 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) Natural
msk Natural
i []
    where
      showBV :: a -> a -> t -> ShowS
showBV a
0 a
_ t
_ String
s = String
s
      showBV a
n a
m t
v String
s = let (t
v',t
vBit) = t -> t -> (t, t)
forall a. Integral a => a -> a -> (a, a)
divMod t
v t
2
                           (a
m',a
mBit) = a -> a -> (a, a)
forall a. Integral a => a -> a -> (a, a)
divMod a
m a
2
                       in  case (a
mBit,t
vBit) of
                           (a
0,t
0) -> a -> a -> t -> ShowS
showBV (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1) a
m' t
v' (Char
'0'Char -> ShowS
forall a. a -> [a] -> [a]
:String
s)
                           (a
0,t
_) -> a -> a -> t -> ShowS
showBV (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1) a
m' t
v' (Char
'1'Char -> ShowS
forall a. a -> [a] -> [a]
:String
s)
                           (a, t)
_     -> a -> a -> t -> ShowS
showBV (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1) a
m' t
v' (Char
'.'Char -> ShowS
forall a. a -> [a] -> [a]
:String
s)

      underScore :: ShowS
underScore String
xs = case Int -> String -> (String, String)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
5 String
xs of
                        ([Char
a,Char
b,Char
c,Char
d,Char
e],String
rest) -> [Char
a,Char
b,Char
c,Char
d,Char
'_'] String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
underScore (Char
eChar -> ShowS
forall a. a -> [a] -> [a]
:String
rest)
                        (String
rest,String
_)               -> 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 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 -> Natural
forall (n :: Nat). BitVector n -> Natural
unsafeMask BitVector n
bv Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
/= Natural
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 String
s = [|| fromInteger# m i1 ||]
  where
    bv :: BitVector n
    bv :: BitVector n
bv = String -> BitVector n
forall (n :: Nat). KnownNat n => String -> BitVector n
read# String
s

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

    i1 :: Integer
    i1 :: Integer
i1 = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i

read# :: KnownNat n => String -> BitVector n
read# :: String -> BitVector n
read# String
cs = Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
m Natural
v
  where
    ([Natural]
vs,[Natural]
ms) = [(Natural, Natural)] -> ([Natural], [Natural])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Natural, Natural)] -> ([Natural], [Natural]))
-> (String -> [(Natural, Natural)])
-> String
-> ([Natural], [Natural])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> (Natural, Natural)) -> String -> [(Natural, Natural)]
forall a b. (a -> b) -> [a] -> [b]
map Char -> (Natural, Natural)
readBit (String -> [(Natural, Natural)])
-> ShowS -> String -> [(Natural, Natural)]
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
/= Char
'_') (String -> ([Natural], [Natural]))
-> String -> ([Natural], [Natural])
forall a b. (a -> b) -> a -> b
$ String
cs
    combineBits :: [Natural] -> Natural
combineBits = (Natural -> Natural -> Natural) -> Natural -> [Natural] -> Natural
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Natural
b Natural
a -> Natural
bNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
*Natural
2Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+Natural
a) Natural
0
    v :: Natural
v = [Natural] -> Natural
combineBits [Natural]
vs
    m :: Natural
m = [Natural] -> Natural
combineBits [Natural]
ms
    readBit :: Char -> (Natural, Natural)
readBit Char
c = case Char
c of
      Char
'0' -> (Natural
0,Natural
0)
      Char
'1' -> (Natural
1,Natural
0)
      Char
'.' -> (Natural
0,Natural
1)
      Char
_   -> String -> (Natural, Natural)
forall a. HasCallStack => String -> a
error (String -> (Natural, Natural)) -> String -> (Natural, Natural)
forall a b. (a -> b) -> a -> b
$ String
"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]
++ String
" 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 Natural
0 Natural
v1) (BV Natural
0 Natural
v2 ) = Natural
v1 Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
v2
eq# BitVector n
bv1 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 String
"==" BitVector n
bv1 BitVector n
bv2

{-# NOINLINE neq# #-}
neq# :: KnownNat n => BitVector n -> BitVector n -> Bool
neq# :: BitVector n -> BitVector n -> Bool
neq# (BV Natural
0 Natural
v1) (BV Natural
0 Natural
v2) = Natural
v1 Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
/= Natural
v2
neq# BitVector n
bv1 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 String
"/=" 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 Natural
0 Natural
n) (BV Natural
0 Natural
m) = Natural
n Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
m
lt# BitVector n
bv1 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 String
"<" BitVector n
bv1 BitVector n
bv2
{-# NOINLINE ge# #-}
ge# :: BitVector n -> BitVector n -> Bool
ge# (BV Natural
0 Natural
n) (BV Natural
0 Natural
m) = Natural
n Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= Natural
m
ge# BitVector n
bv1 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 String
">=" BitVector n
bv1 BitVector n
bv2
{-# NOINLINE gt# #-}
gt# :: BitVector n -> BitVector n -> Bool
gt# (BV Natural
0 Natural
n) (BV Natural
0 Natural
m) = Natural
n Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
m
gt# BitVector n
bv1 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 String
">" BitVector n
bv1 BitVector n
bv2
{-# NOINLINE le# #-}
le# :: BitVector n -> BitVector n -> Bool
le# (BV Natural
0 Natural
n) (BV Natural
0 Natural
m) = Natural
n Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
m
le#  BitVector n
bv1 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 String
"<=" 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
+# Natural -> Integer -> BitVector n
forall (n :: Nat). KnownNat n => Natural -> Integer -> BitVector n
fromInteger# Natural
0 Integer
1)
  pred :: BitVector n -> BitVector n
pred           = (BitVector n -> BitVector n -> BitVector n
forall (n :: Nat).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
-# Natural -> Integer -> BitVector n
forall (n :: Nat). KnownNat n => Natural -> Integer -> BitVector n
fromInteger# Natural
0 Integer
1)
  toEnum :: Int -> BitVector n
toEnum         = Natural -> Integer -> BitVector n
forall (n :: Nat). KnownNat n => Natural -> Integer -> BitVector n
fromInteger# Natural
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#

enumFrom# :: forall n. KnownNat n => BitVector n -> [BitVector n]
enumFrom# :: BitVector n -> [BitVector n]
enumFrom# (BV Natural
0 Natural
x) = (Natural -> BitVector n) -> [Natural] -> [BitVector n]
forall a b. (a -> b) -> [a] -> [b]
map (Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
0 (Natural -> BitVector n)
-> (Natural -> Natural) -> Natural -> BitVector n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m)) [Natural
x .. BitVector n -> Natural
forall (n :: Nat). BitVector n -> Natural
unsafeToNatural (BitVector n
forall a. Bounded a => a
maxBound :: BitVector n)]
  where m :: Natural
m = Natural
1 Natural -> Int -> Natural
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))
enumFrom# BitVector n
bv = String -> BitVector n -> [BitVector n]
forall (n :: Nat) a.
(HasCallStack, KnownNat n) =>
String -> BitVector n -> a
undefErrorU String
"enumFrom" BitVector n
bv
{-# NOINLINE enumFrom# #-}

enumFromThen#
  :: forall n
   . KnownNat n
  => BitVector n
  -> BitVector n
  -> [BitVector n]
enumFromThen# :: BitVector n -> BitVector n -> [BitVector n]
enumFromThen# (BV Natural
0 Natural
x) (BV Natural
0 Natural
y) =
  [Natural] -> [BitVector n]
toBvs [Natural
x, Natural
y .. BitVector n -> Natural
forall (n :: Nat). BitVector n -> Natural
unsafeToNatural BitVector n
bound]
 where
  bound :: BitVector n
bound = if Natural
x Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
y then BitVector n
forall a. Bounded a => a
maxBound else BitVector n
forall a. Bounded a => a
minBound :: BitVector n
  toBvs :: [Natural] -> [BitVector n]
toBvs = (Natural -> BitVector n) -> [Natural] -> [BitVector n]
forall a b. (a -> b) -> [a] -> [b]
map (Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
0 (Natural -> BitVector n)
-> (Natural -> Natural) -> Natural -> BitVector n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m))
  m :: Natural
m = Natural
1 Natural -> Int -> Natural
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))
enumFromThen# BitVector n
bv1 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 String
"enumFromThen" BitVector n
bv1 BitVector n
bv2
{-# NOINLINE enumFromThen# #-}

enumFromTo#
  :: forall n
   . KnownNat n
  => BitVector n
  -> BitVector n
  -> [BitVector n]
enumFromTo# :: BitVector n -> BitVector n -> [BitVector n]
enumFromTo# (BV Natural
0 Natural
x) (BV Natural
0 Natural
y) = (Natural -> BitVector n) -> [Natural] -> [BitVector n]
forall a b. (a -> b) -> [a] -> [b]
map (Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
0 (Natural -> BitVector n)
-> (Natural -> Natural) -> Natural -> BitVector n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m)) [Natural
x .. Natural
y]
  where m :: Natural
m = Natural
1 Natural -> Int -> Natural
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))
enumFromTo# BitVector n
bv1 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 String
"enumFromTo" BitVector n
bv1 BitVector n
bv2
{-# NOINLINE enumFromTo# #-}

enumFromThenTo#
  :: forall n
   . KnownNat n
  => BitVector n
  -> BitVector n
  -> BitVector n
  -> [BitVector n]
enumFromThenTo# :: BitVector n -> BitVector n -> BitVector n -> [BitVector n]
enumFromThenTo# (BV Natural
0 Natural
x1) (BV Natural
0 Natural
x2) (BV Natural
0 Natural
y) = (Natural -> BitVector n) -> [Natural] -> [BitVector n]
forall a b. (a -> b) -> [a] -> [b]
map (Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
0 (Natural -> BitVector n)
-> (Natural -> Natural) -> Natural -> BitVector n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m)) [Natural
x1, Natural
x2 .. Natural
y]
  where m :: Natural
m = Natural
1 Natural -> Int -> Natural
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))
enumFromThenTo# BitVector n
bv1 BitVector n
bv2 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 String
"enumFromTo" BitVector n
bv1 BitVector n
bv2 BitVector n
bv3
{-# NOINLINE enumFromThenTo# #-}


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#

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

maxBound# :: forall n. KnownNat n => BitVector n
maxBound# :: BitVector n
maxBound# = let m :: Natural
m = Natural
1 Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftL` forall a. (Num a, KnownNat n) => a
forall (n :: Nat) a. (Num a, KnownNat n) => a
natToNum @n in Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
0 (Natural
mNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
-Natural
1)
{-# NOINLINE maxBound# #-}

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 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 = Natural -> Integer -> BitVector n
forall (n :: Nat). KnownNat n => Natural -> Integer -> BitVector n
fromInteger# Natural
0

(+#),(-#),(*#) :: forall n . KnownNat n => BitVector n -> BitVector n -> BitVector n
{-# NOINLINE (+#) #-}
+# :: BitVector n -> BitVector n -> BitVector n
(+#) = BitVector n -> BitVector n -> BitVector n
go
  where
    go :: BitVector n -> BitVector n -> BitVector n
go (BV Natural
0 Natural
i) (BV Natural
0 Natural
j) = Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
0 (Natural -> Natural -> Natural -> Natural
addMod Natural
m Natural
i Natural
j)
    go BitVector n
bv1 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 String
"+" BitVector n
bv1 BitVector n
bv2

    m :: Natural
m = Natural
1 Natural -> Int -> Natural
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))

{-# NOINLINE (-#) #-}
-# :: BitVector n -> BitVector n -> BitVector n
(-#) = BitVector n -> BitVector n -> BitVector n
go
  where
    go :: BitVector n -> BitVector n -> BitVector n
go (BV Natural
0 Natural
i) (BV Natural
0 Natural
j) = Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
0 (Natural -> Natural -> Natural -> Natural
subMod Natural
m Natural
i Natural
j)
    go BitVector n
bv1 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 String
"-" BitVector n
bv1 BitVector n
bv2

    m :: Natural
m = Natural
1 Natural -> Int -> Natural
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))

{-# NOINLINE (*#) #-}
*# :: BitVector n -> BitVector n -> BitVector n
(*#) = BitVector n -> BitVector n -> BitVector n
go
 where
  go :: BitVector n -> BitVector n -> BitVector n
go (BV Natural
0 Natural
i) (BV Natural
0 Natural
j) = Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
0 (Natural -> Natural -> Natural -> Natural
mulMod2 Natural
m Natural
i Natural
j)
  go BitVector n
bv1 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 String
"*" BitVector n
bv1 BitVector n
bv2

  m :: Natural
m = (Natural
1 Natural -> Int -> Natural
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))) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1

{-# NOINLINE negate# #-}
negate# :: forall n . KnownNat n => BitVector n -> BitVector n
negate# :: BitVector n -> BitVector n
negate# = BitVector n -> BitVector n
go
 where
  go :: BitVector n -> BitVector n
go (BV Natural
0 Natural
i) = Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
0 (Natural -> Natural -> Natural
negateMod Natural
m Natural
i)
  go BitVector n
bv = String -> BitVector n -> BitVector n
forall (n :: Nat) a.
(HasCallStack, KnownNat n) =>
String -> BitVector n -> a
undefErrorU String
"negate" BitVector n
bv

  m :: Natural
m = Natural
1 Natural -> Int -> Natural
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))

{-# NOINLINE fromInteger# #-}
fromInteger# :: KnownNat n => Natural -> Integer -> BitVector n
fromInteger# :: Natural -> Integer -> BitVector n
fromInteger# Natural
m Integer
i = Integer
sz Integer -> BitVector n -> BitVector n
`seq` BitVector n
mx
  where
    mx :: BitVector n
mx = Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV (Natural
m Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Integer -> Natural
naturalFromInteger Integer
sz)
            (Integer -> Natural
naturalFromInteger (Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
sz))
    sz :: Integer
sz  = Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` 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
mx) :: Integer

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 Natural
0 Natural
a) (BV Natural
0 Natural
b) = Natural -> Natural -> BitVector (Max m n + 1)
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
0 (Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
b)
plus# BitVector m
bv1 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 String
"add" 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# = BitVector m -> BitVector n -> BitVector (Max m n + 1)
go
 where
  go :: BitVector m -> BitVector n -> BitVector (Max m n + 1)
go (BV Natural
0 Natural
a) (BV Natural
0 Natural
b) = Natural -> Natural -> BitVector (Max m n + 1)
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
0 (Natural -> Natural -> Natural -> Natural
subMod Natural
m Natural
a Natural
b)
  go BitVector m
bv1 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 String
"sub" BitVector m
bv1 BitVector n
bv2

  m :: Natural
m = Natural
1 Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftL` 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)))

{-# NOINLINE times# #-}
times# :: (KnownNat m, KnownNat n) => BitVector m -> BitVector n -> BitVector (m + n)
times# :: BitVector m -> BitVector n -> BitVector (m + n)
times# (BV Natural
0 Natural
a) (BV Natural
0 Natural
b) = Natural -> Natural -> BitVector (m + n)
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
0 (Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
b)
times# BitVector m
bv1 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 String
"mul" 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 BitVector n
n 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  BitVector n
n 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 Natural
0 Natural
i) (BV Natural
0 Natural
j) = Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
0 (Natural
i Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`quot` Natural
j)
quot# BitVector n
bv1 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 String
"quot" BitVector n
bv1 BitVector n
bv2
{-# NOINLINE rem# #-}
rem# :: BitVector n -> BitVector n -> BitVector n
rem# (BV Natural
0 Natural
i) (BV Natural
0 Natural
j) = Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
0 (Natural
i Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`rem` Natural
j)
rem# BitVector n
bv1 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 String
"rem" BitVector n
bv1 BitVector n
bv2

{-# NOINLINE toInteger# #-}
toInteger# :: KnownNat n => BitVector n -> Integer
toInteger# :: BitVector n -> Integer
toInteger# (BV Natural
0 Natural
i) = Natural -> Integer
naturalToInteger Natural
i
toInteger# BitVector n
bv = String -> BitVector n -> Integer
forall (n :: Nat) a.
(HasCallStack, KnownNat n) =>
String -> BitVector n -> a
undefErrorU String
"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).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
and#
  .|. :: BitVector n -> BitVector n -> BitVector n
(.|.)             = BitVector n -> BitVector n -> BitVector n
forall (n :: Nat).
KnownNat n =>
BitVector n -> BitVector n -> BitVector n
or#
  xor :: BitVector n -> BitVector n -> BitVector n
xor               = BitVector n -> BitVector n -> BitVector n
forall (n :: Nat).
KnownNat n =>
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          = BitVector n
0
  bit :: Int -> BitVector n
bit Int
i             = BitVector n -> Int -> Bit -> BitVector n
forall (n :: Nat).
KnownNat n =>
BitVector n -> Int -> Bit -> BitVector n
replaceBit# BitVector n
0 Int
i Bit
high
  setBit :: BitVector n -> Int -> BitVector n
setBit BitVector n
v 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 BitVector n
v 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 BitVector n
v 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 BitVector n
v 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 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 BitVector n
_        = Bool
False
  shiftL :: BitVector n -> Int -> BitVector n
shiftL BitVector n
v 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 BitVector n
v 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 BitVector n
v 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 BitVector n
v 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 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)
++# (BitVector 1
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 (\Bit
l Index (n + 1)
r -> if Bit -> Bit -> Bool
eq## Bit
l Bit
low then Index (n + 1)
1 Index (n + 1) -> Index (n + 1) -> Index (n + 1)
forall a. Num a => a -> a -> a
+ Index (n + 1)
r else Index (n + 1)
0) Index (n + 1)
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 (\Index (n + 1)
l Bit
r -> if Bit -> Bit -> Bool
eq## Bit
r Bit
low then Index (n + 1)
1 Index (n + 1) -> Index (n + 1) -> Index (n + 1)
forall a. Num a => a -> a -> a
+ Index (n + 1)
l else Index (n + 1)
0) Index (n + 1)
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 Natural
0 Natural
i) = Word -> Word -> Bit
Bit Word
0 (Word# -> Word
W# (Int# -> Word#
int2Word# (Bool -> Int#
forall a. a -> Int#
dataToTag# Bool
check)))
  where
    check :: Bool
check = Natural
i Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
maxI

    sz :: Integer
sz    = BitVector n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal BitVector n
bv
    maxI :: Natural
maxI  = (Natural
2 Natural -> Integer -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
sz) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1
reduceAnd# 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
(.&.) Bit
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 Natural
0 Natural
i) = Word -> Word -> Bit
Bit Word
0 (Word# -> Word
W# (Int# -> Word#
int2Word# (Bool -> Int#
forall a. a -> Int#
dataToTag# Bool
check)))
  where
    check :: Bool
check = Natural
i Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
/= Natural
0
reduceOr# 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
(.|.) Bit
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 Natural
0 Natural
i) = Word -> Word -> Bit
Bit Word
0 (Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int
forall a. Bits a => a -> Int
popCount Natural
i Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
2))
reduceXor# BitVector n
bv = String -> BitVector n -> Bit
forall (n :: Nat) a.
(HasCallStack, KnownNat n) =>
String -> BitVector n -> a
undefErrorU String
"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# 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# 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
- Int
1

-- ** Indexing
{-# NOINLINE index# #-}
index# :: KnownNat n => BitVector n -> Int -> Bit
index# :: BitVector n -> Int -> Bit
index# bv :: BitVector n
bv@(BV Natural
m Natural
v) Int
i
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
sz = Word -> Word -> Bit
Bit (Word# -> Word
W# (Int# -> Word#
int2Word# (Bool -> Int#
forall a. a -> Int#
dataToTag# (Natural -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Natural
m Int
i))))
                             (Word# -> Word
W# (Int# -> Word#
int2Word# (Bool -> Int#
forall a. a -> Int#
dataToTag# (Natural -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Natural
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 [ String
"(!): "
                         , Int -> String
forall a. Show a => a -> String
show Int
i
                         , String
" 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
- Int
1)
                         , String
"..0]"
                         ]

{-# NOINLINE msb# #-}
-- | MSB
msb# :: forall n . KnownNat n => BitVector n -> Bit
msb# :: BitVector n -> Bit
msb# (BV Natural
m Natural
v)
  = Word -> Word -> Bit
Bit (Natural -> Word
msbN Natural
m)
        (Natural -> Word
msbN Natural
v)
 where
  !(S# Int#
i#) = 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)
  msbN :: Natural -> Word
msbN (NatS# Word#
w)  = Word# -> Word
W# (Word#
w Word# -> Int# -> Word#
`uncheckedShiftRL#` (Int#
i# Int# -> Int# -> Int#
GHC.Exts.-# Int#
1#))
  msbN (NatJ# BigNat
bn) = Word# -> Word
W# (BigNat -> Word#
bigNatToWord (BigNat -> Int# -> BigNat
shiftRBigNat BigNat
bn (Int#
i# Int# -> Int# -> Int#
GHC.Exts.-# Int#
1#)))

{-# NOINLINE lsb# #-}
-- | LSB
lsb# :: BitVector n -> Bit
lsb# :: BitVector n -> Bit
lsb# (BV Natural
m Natural
v) = Word -> Word -> Bit
Bit (Word# -> Word
W# (Int# -> Word#
int2Word# (Bool -> Int#
forall a. a -> Int#
dataToTag# (Natural -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Natural
m Int
0))))
                    (Word# -> Word
W# (Int# -> Word#
int2Word# (Bool -> Int#
forall a. a -> Int#
dataToTag# (Natural -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Natural
v Int
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 Natural
msk Natural
i) SNat m
m SNat n
n = Natural -> Natural -> BitVector ((m + 1) - n)
forall (n :: Nat). Natural -> Natural -> BitVector n
BV (Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftR (Natural
msk Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. Natural
mask) Int
n')
                           (Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftR (Natural
i   Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. Natural
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 :: Natural
mask = Natural
2 Natural -> Integer -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
m' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1

-- * Constructions

-- ** Concatenation
{-# NOINLINE (++#) #-}
-- | Concatenate two 'BitVector's
(++#) :: KnownNat m => BitVector n -> BitVector m -> BitVector (n + m)
(BV Natural
m1 Natural
v1) ++# :: BitVector n -> BitVector m -> BitVector (n + m)
++# bv2 :: BitVector m
bv2@(BV Natural
m2 Natural
v2) = Natural -> Natural -> BitVector (n + m)
forall (n :: Nat). Natural -> Natural -> BitVector n
BV (Natural
m1' Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|. Natural
m2) (Natural
v1' Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|. Natural
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' :: Natural
v1' = Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftL Natural
v1 Int
size2
    m1' :: Natural
m1' = Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftL Natural
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 Natural
m Natural
v) Int
i (Bit Word
mb Word
b)
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
sz = Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV (Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
clearBit Natural
m Int
i  Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|. (Word -> Natural
wordToNatural Word
mb Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftL` Int
i))
                            (if Word -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Word
b Int
0 Bool -> Bool -> Bool
&& Word
mb Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0 then Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
setBit Natural
v Int
i else Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
clearBit Natural
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 [ String
"replaceBit: "
                          , Int -> String
forall a. Show a => a -> String
show Int
i
                          , String
" 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
- Int
1)
                          , String
"..0]"
                          ]

{-# NOINLINE setSlice# #-}
setSlice#
  :: forall m i n
   . SNat (m + 1 + i)
  -> BitVector (m + 1 + i)
  -> SNat m
  -> SNat n
  -> BitVector (m + 1 - n)
  -> BitVector (m + 1 + i)
setSlice# :: SNat ((m + 1) + i)
-> BitVector ((m + 1) + i)
-> SNat m
-> SNat n
-> BitVector ((m + 1) - n)
-> BitVector ((m + 1) + i)
setSlice# SNat ((m + 1) + i)
SNat =
  \(BV Natural
iMask Natural
i) m :: SNat m
m@SNat m
SNat SNat n
n (BV Natural
jMask Natural
j) ->
    let 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' :: Natural
j'     = Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftL Natural
j     (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n')
        jMask' :: Natural
jMask' = Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftL Natural
jMask (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n')
        mask :: Natural
mask   = Natural -> Natural
complementN ((Natural
2 Natural -> Integer -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
m' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1) Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
`xor` (Natural
2 Natural -> Integer -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
n' Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1))
    in  Natural -> Natural -> BitVector ((m + 1) + i)
forall (n :: Nat). Natural -> Natural -> BitVector n
BV ((Natural
iMask Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. Natural
mask) Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|. Natural
jMask') ((Natural
i Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. Natural
mask) Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|. Natural
j')
 where
  complementN :: Natural -> Natural
complementN = Integer -> Natural -> Natural
complementMod (Proxy ((m + 1) + i) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy ((m + 1) + i)
forall k (t :: k). Proxy t
Proxy @(m + 1 + i)))

{-# 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 Natural
m Natural
i) =
  let 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 :: Natural -> Natural
mask  = Integer -> Natural -> Natural
maskMod (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))
      r :: Natural
r     = Natural -> Natural
mask Natural
i
      rMask :: Natural
rMask = Natural -> Natural
mask Natural
m
      l :: Natural
l     = Natural
i Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftR` Int
n
      lMask :: Natural
lMask = Natural
m Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftR` Int
n
  in  (Natural -> Natural -> BitVector m
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
lMask Natural
l, Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
rMask Natural
r)

and#, or#, xor# :: forall n . KnownNat n => BitVector n -> BitVector n -> BitVector n
{-# NOINLINE and# #-}
and# :: BitVector n -> BitVector n -> BitVector n
and# =
  \(BV Natural
m1 Natural
v1) (BV Natural
m2 Natural
v2) ->
    let mask :: Natural
mask = (Natural
m1Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&.Natural
v2 Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|. Natural
m1Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&.Natural
m2 Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|. Natural
m2Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&.Natural
v1)
    in  Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
mask (Natural
v1 Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. Natural
v2  Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. Natural -> Natural
complementN Natural
mask)
  where
    complementN :: Natural -> Natural
complementN = Integer -> Natural -> Natural
complementMod (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))

{-# NOINLINE or# #-}
or# :: BitVector n -> BitVector n -> BitVector n
or# =
  \(BV Natural
m1 Natural
v1) (BV Natural
m2 Natural
v2) ->
    let mask :: Natural
mask = Natural
m1 Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. Natural -> Natural
complementN Natural
v2  Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|.  Natural
m1Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&.Natural
m2  Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|.  Natural
m2 Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. Natural -> Natural
complementN Natural
v1
    in  Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
mask ((Natural
v1Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|.Natural
v2) Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. Natural -> Natural
complementN Natural
mask)
  where
    complementN :: Natural -> Natural
complementN = Integer -> Natural -> Natural
complementMod (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))

{-# NOINLINE xor# #-}
xor# :: BitVector n -> BitVector n -> BitVector n
xor# =
  \(BV Natural
m1 Natural
v1) (BV Natural
m2 Natural
v2) ->
    let mask :: Natural
mask  = Natural
m1 Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|. Natural
m2
    in  Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
mask ((Natural
v1 Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
`xor` Natural
v2) Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. Natural -> Natural
complementN Natural
mask)
  where
    complementN :: Natural -> Natural
complementN = Integer -> Natural -> Natural
complementMod (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))

{-# NOINLINE complement# #-}
complement# :: forall n . KnownNat n => BitVector n -> BitVector n
complement# :: BitVector n -> BitVector n
complement# = \(BV Natural
m Natural
v) -> Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
m (Natural -> Natural
complementN Natural
v Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. Natural -> Natural
complementN Natural
m)
  where complementN :: Natural -> Natural
complementN = Integer -> Natural -> Natural
complementMod (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))

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

{-# NOINLINE shiftL# #-}
shiftL# :: BitVector n -> Int -> BitVector n
shiftL# =
  \(BV Natural
msk Natural
v) Int
i ->
    if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 then
      Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV ((Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftL Natural
msk Int
i) Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m) ((Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftL Natural
v Int
i) Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m)
    else
      String -> BitVector n
forall a. HasCallStack => String -> a
error (String
"'shiftL' undefined for negative number: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)
 where
  m :: Natural
m = Natural
1 Natural -> Int -> Natural
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))

{-# NOINLINE shiftR# #-}
shiftR# :: BitVector n -> Int -> BitVector n
shiftR# (BV Natural
m Natural
v) Int
i
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0     = String -> BitVector n
forall a. HasCallStack => String -> a
error
              (String -> BitVector n) -> String -> BitVector n
forall a b. (a -> b) -> a -> b
$ String
"'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 = Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV (Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftR Natural
m Int
i) (Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftR Natural
v Int
i)

{-# NOINLINE rotateL# #-}
rotateL# :: BitVector n -> Int -> BitVector n
rotateL# =
  \(BV Natural
msk Natural
v) Int
b ->
    if Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 then
      let vl :: Natural
vl    = Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftL Natural
v Int
b'
          vr :: Natural
vr    = Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftR Natural
v Int
b''

          ml :: Natural
ml    = Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftL Natural
msk Int
b'
          mr :: Natural
mr    = Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftR Natural
msk 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'
      in  Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV ((Natural
ml Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|. Natural
mr) Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m) ((Natural
vl Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|. Natural
vr) Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m)
    else
      String -> BitVector n
forall a. HasCallStack => String -> a
error String
"'rotateL' undefined for negative numbers"
 where
  sz :: Int
sz = 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)) :: Int
  m :: Natural
m  = Natural
1 Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftL` Int
sz

{-# NOINLINE rotateR# #-}
rotateR# :: BitVector n -> Int -> BitVector n
rotateR# =
  \(BV Natural
msk Natural
v) Int
b ->
    if Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 then
      let vl :: Natural
vl   = Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftR Natural
v Int
b'
          vr :: Natural
vr   = Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftL Natural
v Int
b''
          ml :: Natural
ml   = Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftR Natural
msk Int
b'
          mr :: Natural
mr   = Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftL Natural
msk 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'
      in  Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV ((Natural
ml Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|. Natural
mr) Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m) ((Natural
vl Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|. Natural
vr) Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m)
    else
      String -> BitVector n
forall a. HasCallStack => String -> a
error String
"'rotateR' undefined for negative numbers"
 where
  sz :: Int
sz = 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)) :: Int
  m :: Natural
m  = Natural
1 Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftL` Int
sz

popCountBV :: forall n . KnownNat n => BitVector (n+1) -> I.Index (n+2)
popCountBV :: BitVector (n + 1) -> Index (n + 2)
popCountBV 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 = (BitVector b
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 = \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) BitVector b
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 n m
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) BitVector (m - n)
0
  SNatLE n m
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 Natural
msk Natural
i) -> Natural -> Natural -> BitVector a
forall (n :: Nat). Natural -> Natural -> BitVector n
BV (Natural
msk Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m) (Natural
i Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
m)
  where m :: Natural
m = Natural
1 Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy a -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy a
forall k (t :: k). Proxy t
Proxy @a))
{-# NOINLINE truncateB# #-}

instance KnownNat n => Lift (BitVector n) where
  lift :: BitVector n -> Q Exp
lift bv :: BitVector n
bv@(BV Natural
m Natural
i) = Q Exp -> TypeQ -> Q Exp
sigE [| fromInteger# m $(litE (IntegerL (toInteger i))) |] (Integer -> TypeQ
decBitVector (BitVector n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal BitVector n
bv))
  {-# NOINLINE lift #-}
#if MIN_VERSION_template_haskell(2,16,0)
  liftTyped :: BitVector n -> Q (TExp (BitVector n))
liftTyped = BitVector n -> Q (TExp (BitVector n))
forall a. Lift a => a -> Q (TExp a)
liftTypedFromUntyped
#endif

decBitVector :: Integer -> TypeQ
decBitVector :: Integer -> TypeQ
decBitVector 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 SaturationMode
SatWrap BitVector n
a 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 SaturationMode
SatZero BitVector n
a 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 SaturationMode
_ BitVector n
a 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 SaturationMode
SatWrap BitVector n
a 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 SaturationMode
_ BitVector n
a 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 SaturationMode
SatWrap BitVector n
a 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 SaturationMode
SatZero BitVector n
a 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
        (BitVector n
rL,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
          BitVector n
0 -> BitVector n
rR
          BitVector n
_ -> BitVector n
forall (n :: Nat). BitVector n
minBound#
  satMul SaturationMode
_ BitVector n
a 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
        (BitVector n
rL,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
          BitVector n
0 -> BitVector n
rR
          BitVector n
_ -> 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 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
< Integer
2 = case p n -> Integer
forall a. Integral a => a -> Integer
toInteger p n
x of
                                         Integer
1 -> [p n
0]
                                         Integer
_ -> []
                      -- '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 Index (BitVector n)
i IxValue (BitVector n) -> f (IxValue (BitVector n))
f 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 String
op BitVector m
bv1 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
$ String
"Clash.Sized.BitVector." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
op
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" 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
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
op String -> ShowS
forall a. [a] -> [a] -> [a]
++String
" " 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 String
op BitVector m
bv1 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
$ String
"Clash.Sized.BitVector." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
op
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" 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
" " 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 String
op BitVector m
bv1 BitVector n
bv2 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
$ String
"Clash.Sized.BitVector." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
op
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" 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
" " 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
" " 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 String
op 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
$ String
"Clash.Sized.BitVector." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
op
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" 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 String
op [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]
++ String
" 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 BitVector n -> a
f bv :: BitVector n
bv@(BV Natural
0 Natural
_) = BitVector n -> a
f BitVector n
bv
checkUnpackUndef BitVector n -> a
_ 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]
++ String
".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 :: Natural
m = Natural
1 Natural -> Int -> Natural
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  Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV (Natural
mNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
-Natural
1) Natural
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 :: forall n . KnownNat n => BitVector n -> BitVector n -> Bool
isLike :: BitVector n -> BitVector n -> Bool
isLike =
  \(BV Natural
cMask Natural
c) (BV Natural
eMask Natural
e) ->
        -- set don't care bits to 0
    let e' :: Natural
e' = Natural
e Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. Natural -> Natural
complementN Natural
eMask
        -- checked with undefined bits set to 0
        c' :: Natural
c' = (Natural
c Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. Natural -> Natural
complementN Natural
cMask) Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. Natural -> Natural
complementN Natural
eMask
        -- checked with undefined bits set to 1
        c'' :: Natural
c'' = (Natural
c Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|. Natural
cMask) Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. Natural -> Natural
complementN Natural
eMask
    in  Natural
e' Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
c' Bool -> Bool -> Bool
&& Natural
e' Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
c''
 where
  complementN :: Natural -> Natural
complementN = Integer -> Natural -> Natural
complementMod (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))
{-# 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 (\Integer
v Bit
b -> Integer
v Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
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) Integer
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 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 Bit
0 (Bit -> Bit -> Bit
forall a b. a -> b -> a
const Bit
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 Bit
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 Char
'.' = Maybe a
forall a. Maybe a
Nothing
    parse Char
'0' = a -> Maybe a
forall a. a -> Maybe a
Just a
0
    parse Char
'1' = a -> Maybe a
forall a. a -> Maybe a
Just a
1
    parse Char
c = String -> Maybe a
forall a. HasCallStack => String -> a
error (String -> Maybe a) -> String -> Maybe a
forall a b. (a -> b) -> a -> b
$ String
"Invalid bit pattern: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. Show a => a -> String
show Char
c