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

{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

{-# LANGUAGE Unsafe #-}

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

module Clash.Sized.Internal.BitVector
  ( -- * Bit
    Bit (..)
    -- ** Construction
  , high
  , low
    -- ** Type classes
    -- *** Eq
  , eq##
  , neq##
    -- *** Ord
  , lt##
  , ge##
  , gt##
  , le##
    -- *** Enum
  , toEnum##
    -- *** 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
  , toEnum#
  , fromEnum#
    -- *** 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#, isTrue#, uncheckedShiftRL#)
#if MIN_VERSION_base(4,15,0)
import GHC.Exts (minusWord#, gtWord#, word2Int#)
import GHC.Num.BigNat (bigNatShiftR#, bigNatToWord)
import GHC.Num.Integer (integerFromNatural, integerToNatural)
import GHC.Num.Natural
  (Natural (..), naturalFromWord, naturalShiftL, naturalShiftR, naturalToWord)
#else
import GHC.Exts ((>#))
import qualified GHC.Exts
import GHC.Integer.GMP.Internals  (Integer (..), bigNatToWord, shiftRBigNat)
import GHC.Natural
  (Natural (..), naturalFromInteger, wordToNatural)
#endif
import GHC.Natural                (naturalToInteger)
import GHC.Prim                   (dataToTag#)
import GHC.Stack                  (withFrozenCallStack)
import GHC.TypeLits               (KnownNat, Nat, type (+), type (-))
#if MIN_VERSION_base(4,15,0)
import GHC.TypeNats               (natVal)
#else
import GHC.TypeLits               (natVal)
#endif
import GHC.TypeLits.Extra         (Max)
import Language.Haskell.TH
  (Lit (..), ExpQ, Type(ConT, AppT, LitT), Exp(VarE, AppE, SigE, LitE),
   TyLit(NumTyLit), Pat, Q, appT, conT, litE, litP, litT, mkName, numTyLit,
   sigE, tupE, tupP, varP)
import Language.Haskell.TH.Syntax (Lift(..))
#if MIN_VERSION_template_haskell(2,16,0)
import Language.Haskell.TH.Compat
#endif
#if MIN_VERSION_template_haskell(2,17,0)
import Language.Haskell.TH        (Quote)
#else
import Language.Haskell.TH        (TypeQ)
#endif
import Test.QuickCheck.Arbitrary  (Arbitrary (..), CoArbitrary (..),
                                   arbitraryBoundedIntegral,
                                   coarbitraryIntegral, shrinkIntegral)

import Clash.Annotations.Primitive (hasBlackBox)
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.Char                  as C
import                qualified Data.List                  as L
import                qualified Data.Map.Strict            as M

#include "MachDeps.h"

{- $setup
>>> :set -XTemplateHaskell
>>> :set -XBinaryLiterals
>>> import Clash.Sized.Internal.BitVector
-}

type role BitVector nominal

-- * Type definitions

-- | A vector of bits.
--
-- * Bit indices are descending
-- * 'Num' instance performs /unsigned/ arithmetic.
--
-- BitVector has the <https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/roles.html type role>
--
-- >>> :i BitVector
-- type role BitVector nominal
-- ...
--
-- as it is not safe to coerce between different size BitVector. To change the
-- size, use the functions in the 'Clash.Class.Resize.Resize' class.
data BitVector (n :: Nat) =
    -- | The constructor, 'BV', and  the field, 'unsafeToNatural', 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)

{-# ANN BV hasBlackBox #-}

-- * 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)

{-# ANN Bit hasBlackBox #-}

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

{-# NOINLINE low #-}
{-# ANN low hasBlackBox #-}
-- | 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## #-}
{-# ANN eq## hasBlackBox #-}

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## #-}
{-# ANN neq## hasBlackBox #-}

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## #-}
{-# ANN lt## hasBlackBox #-}
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## #-}
{-# ANN ge## hasBlackBox #-}
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## #-}
{-# ANN gt## hasBlackBox #-}
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## #-}
{-# ANN le## hasBlackBox #-}

instance Enum Bit where
  toEnum :: Int -> Bit
toEnum     = Int -> Bit
toEnum##
  fromEnum :: Bit -> Int
fromEnum Bit
b = if Bit -> Bit -> Bool
eq## Bit
b Bit
low then Int
0 else Int
1

toEnum## :: Int -> Bit
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
{-# NOINLINE toEnum## #-}
{-# ANN toEnum## hasBlackBox #-}

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## #-}
{-# ANN fromInteger## hasBlackBox #-}

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
  shift :: Bit -> Int -> Bit
shift 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
  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
  rotate :: Bit -> Int -> Bit
rotate Bit
b Int
_        = Bit
b
  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## #-}
{-# ANN and## hasBlackBox #-}

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## #-}
{-# ANN or## hasBlackBox #-}

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## #-}
{-# ANN xor## hasBlackBox #-}

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## #-}
{-# ANN complement## hasBlackBox #-}

-- *** BitPack
pack# :: Bit -> BitVector 1
#if MIN_VERSION_base(4,15,0)
pack# (Bit (W# m) (W# b)) = BV (NS m) (NS b)
#else
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)
#endif
{-# NOINLINE pack# #-}
{-# ANN pack# hasBlackBox #-}

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
#if MIN_VERSION_base(4,15,0)
  go (NS w) = W# w
  go (NB w) = bigNatToWord w
#else
  go :: Natural -> Word
go (NatS# Word#
w) = Word# -> Word
W# Word#
w
  go (NatJ# BigNat
w) = Word# -> Word
W# (BigNat -> Word#
bigNatToWord BigNat
w)
#endif
{-# NOINLINE unpack# #-}
{-# ANN unpack# hasBlackBox #-}

-- * 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 Natural
m Natural
i) =
    case (Num Int, KnownNat n) => Int
forall (n :: Nat) a. (Num a, KnownNat n) => a
natToNum @n @Int of
      Int
0 -> String
"0"
      Int
_ -> Char
'0' Char -> ShowS
forall a. a -> [a] -> [a]
: Char
'b' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> Int -> Natural -> Natural -> ShowS
forall t t a.
(Integral t, Integral t, Num a, Eq a) =>
Int -> a -> t -> t -> ShowS
go Int
groupSize ((Num Int, KnownNat n) => Int
forall (n :: Nat) a. (Num a, KnownNat n) => a
natToNum @n @Int) Natural
m Natural
i []
   where
    go :: Int -> a -> t -> t -> ShowS
go Int
_ a
0 t
_ t
_ String
s = String
s
    go Int
c a
n t
m0 t
v0 String
s =
      let
        (!t
v1, !t
vBit) = t -> t -> (t, t)
forall a. Integral a => a -> a -> (a, a)
quotRem t
v0 t
2
        (!t
m1, !t
mBit) = t -> t -> (t, t)
forall a. Integral a => a -> a -> (a, a)
quotRem t
m0 t
2
        !renderedBit :: Char
renderedBit = t -> t -> Char
forall a a. (Eq a, Eq a, Num a, Num a) => a -> a -> Char
showBit t
mBit t
vBit
      in
        case Int
c of
          Int
0 -> Int -> a -> t -> t -> ShowS
go (Int
groupSize Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1) t
m1 t
v1 (Char
renderedBit Char -> ShowS
forall a. a -> [a] -> [a]
: Char
'_' Char -> ShowS
forall a. a -> [a] -> [a]
: String
s)
          Int
_ -> Int -> a -> t -> t -> ShowS
go (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)         (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1) t
m1 t
v1 (Char
renderedBit Char -> ShowS
forall a. a -> [a] -> [a]
:       String
s)

    showBit :: a -> a -> Char
showBit a
0 a
0 = Char
'0'
    showBit a
0 a
1 = Char
'1'
    showBit a
_ a
_ = Char
'.'

    groupSize :: Int
    groupSize :: Int
groupSize = Int
4
  {-# 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 KnownNat n => NFDataX (BitVector n) where
  deepErrorX :: String -> BitVector n
deepErrorX String
_ = BitVector n
forall (n :: Nat). KnownNat n => BitVector n
undefined#
  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")
-- 0b1001
--
-- __NB__: You can also just write:
--
-- >>> 0b1001 :: BitVector 4
-- 0b1001
--
-- 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'))
-- 0b1111
--
-- Also 'bLit' can handle don't care bits:
--
-- >>> $(bLit "1.0.")
-- 0b1.0.
--
-- __N.B.__: From Clash 1.6 an onwards 'bLit' will deduce the size of the
--           BitVector from the given string and annotate the splice it
--           produces accordingly.
bLit :: String -> ExpQ
bLit :: String -> Q Exp
bLit String
s = Exp -> Q Exp
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Exp -> Type -> Exp
SigE Exp
body Type
typ)
 where
  typ :: Type
typ = Name -> Type
ConT ''BitVector Type -> Type -> Type
`AppT` TyLit -> Type
LitT (Integer -> TyLit
NumTyLit (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
n))
  body :: Exp
body = Name -> Exp
VarE 'fromInteger# Exp -> Exp -> Exp
`AppE` Natural -> Exp
iLit Natural
mask Exp -> Exp -> Exp
`AppE` Natural -> Exp
iLit Natural
value

  iLit :: Natural -> Exp
iLit = Lit -> Exp
LitE (Lit -> Exp) -> (Natural -> Lit) -> Natural -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Lit
IntegerL (Integer -> Lit) -> (Natural -> Integer) -> Natural -> Lit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Integer
forall a. Integral a => a -> Integer
toInteger
  (Natural
n, BV Natural
mask Natural
value) = String -> (Natural, BitVector n)
forall (n :: Nat). String -> (Natural, BitVector n)
read# String
s :: (Natural, BitVector n)

read# :: String -> (Natural, BitVector n)
read# :: String -> (Natural, BitVector n)
read# String
cs0 = (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (String -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length String
cs1), Natural -> Natural -> BitVector n
forall (n :: Nat). Natural -> Natural -> BitVector n
BV Natural
m Natural
v)
  where
    cs1 :: String
cs1 = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'_') String
cs0
    ([Natural]
vs, [Natural]
ms) = [(Natural, Natural)] -> ([Natural], [Natural])
forall a b. [(a, b)] -> ([a], [b])
unzip ((Char -> (Natural, Natural)) -> String -> [(Natural, Natural)]
forall a b. (a -> b) -> [a] -> [b]
map Char -> (Natural, Natural)
readBit String
cs1)
    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
cs0


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# #-}
{-# ANN eq# hasBlackBox #-}
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.
(KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorI String
"==" BitVector n
bv1 BitVector n
bv2

{-# NOINLINE neq# #-}
{-# ANN neq# hasBlackBox #-}
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.
(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# #-}
{-# ANN lt# hasBlackBox #-}
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.
(KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorI String
"<" BitVector n
bv1 BitVector n
bv2
{-# NOINLINE ge# #-}
{-# ANN ge# hasBlackBox #-}
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.
(KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorI String
">=" BitVector n
bv1 BitVector n
bv2
{-# NOINLINE gt# #-}
{-# ANN gt# hasBlackBox #-}
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.
(KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorI String
">" BitVector n
bv1 BitVector n
bv2
{-# NOINLINE le# #-}
{-# ANN le# hasBlackBox #-}
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.
(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         = Int -> BitVector n
forall (n :: Nat). KnownNat n => Int -> BitVector n
toEnum#
  fromEnum :: BitVector n -> Int
fromEnum       = BitVector n -> Int
forall (n :: Nat). KnownNat n => BitVector n -> Int
fromEnum#
  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#

toEnum# :: forall n. KnownNat n => Int -> BitVector n
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
{-# NOINLINE toEnum# #-}
{-# ANN toEnum# hasBlackBox #-}

fromEnum# :: forall n. KnownNat n => BitVector n -> Int
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#
{-# NOINLINE fromEnum# #-}
{-# ANN fromEnum# hasBlackBox #-}

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)]
#if MIN_VERSION_base(4,15,0)
  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
#else
  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))
#endif
enumFrom# BitVector n
bv = String -> BitVector n -> [BitVector n]
forall (n :: Nat) a. 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))
#if MIN_VERSION_base(4,15,0)
  m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
#else
  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))
#endif
enumFromThen# BitVector n
bv1 BitVector n
bv2 = String -> BitVector n -> BitVector n -> [BitVector n]
forall (m :: Nat) (n :: Nat) a.
(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]
#if MIN_VERSION_base(4,15,0)
  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
#else
  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))
#endif
enumFromTo# BitVector n
bv1 BitVector n
bv2 = String -> BitVector n -> BitVector n -> [BitVector n]
forall (m :: Nat) (n :: Nat) a.
(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]
#if MIN_VERSION_base(4,15,0)
  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
#else
  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))
#endif
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.
(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# #-}
{-# ANN minBound# hasBlackBox #-}

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# #-}
{-# ANN maxBound# hasBlackBox #-}

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 (+#) #-}
{-# ANN (+#) hasBlackBox #-}
+# :: 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.
(KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorI String
"+" BitVector n
bv1 BitVector n
bv2

#if MIN_VERSION_base(4,15,0)
    m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
#else
    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))
#endif

{-# NOINLINE (-#) #-}
{-# ANN (-#) hasBlackBox #-}
-# :: 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.
(KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorI String
"-" BitVector n
bv1 BitVector n
bv2

#if MIN_VERSION_base(4,15,0)
    m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
#else
    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))
#endif

{-# NOINLINE (*#) #-}
{-# ANN (*#) hasBlackBox #-}
*# :: 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.
(KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorI String
"*" BitVector n
bv1 BitVector n
bv2

#if MIN_VERSION_base(4,15,0)
  m = (1 `naturalShiftL` naturalToWord (natVal (Proxy @n))) - 1
#else
  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
#endif

{-# NOINLINE negate# #-}
{-# ANN negate# hasBlackBox #-}
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. KnownNat n => String -> BitVector n -> a
undefErrorU String
"negate" BitVector n
bv

#if MIN_VERSION_base(4,15,0)
  m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
#else
  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))
#endif

{-# NOINLINE fromInteger# #-}
{-# ANN fromInteger# hasBlackBox #-}
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
#if MIN_VERSION_base(4,15,0)
    mx = BV (m `mod` sz)
            (integerToNatural (i `mod` integerFromNatural sz))
    sz  = 1 `naturalShiftL` naturalToWord (natVal mx)
#else
    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
#endif

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# #-}
{-# ANN plus# hasBlackBox #-}
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.
(KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorP String
"add" BitVector m
bv1 BitVector n
bv2

{-# NOINLINE minus# #-}
{-# ANN minus# hasBlackBox #-}
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.
(KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorP String
"sub" BitVector m
bv1 BitVector n
bv2

#if MIN_VERSION_base(4,15,0)
  m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @(Max m n + 1)))
#else
  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)))
#endif

{-# NOINLINE times# #-}
{-# ANN times# hasBlackBox #-}
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.
(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# #-}
{-# ANN quot# hasBlackBox #-}
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.
(KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorP String
"quot" BitVector n
bv1 BitVector n
bv2
{-# NOINLINE rem# #-}
{-# ANN rem# hasBlackBox #-}
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.
(KnownNat m, KnownNat n) =>
String -> BitVector m -> BitVector n -> a
undefErrorP String
"rem" BitVector n
bv1 BitVector n
bv2

{-# NOINLINE toInteger# #-}
{-# ANN toInteger# hasBlackBox #-}
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. 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# #-}
{-# ANN reduceAnd# hasBlackBox #-}
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# #-}
{-# ANN reduceOr# hasBlackBox #-}
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# #-}
{-# ANN reduceXor# hasBlackBox #-}
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. 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# #-}
{-# ANN size# hasBlackBox #-}
size# :: KnownNat n => BitVector n -> Int
#if MIN_VERSION_base(4,15,0)
size# bv = fromIntegral (natVal bv)
#else
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)
#endif

{-# NOINLINE maxIndex# #-}
{-# ANN maxIndex# hasBlackBox #-}
maxIndex# :: KnownNat n => BitVector n -> Int
#if MIN_VERSION_base(4,15,0)
maxIndex# bv = fromIntegral (natVal bv) - 1
#else
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
#endif

-- ** Indexing
{-# NOINLINE index# #-}
{-# ANN index# hasBlackBox #-}
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
#if MIN_VERSION_base(4,15,0)
    sz  = fromIntegral (natVal bv)
#else
    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)
#endif
    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# #-}
{-# ANN msb# hasBlackBox #-}
-- | 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
#if MIN_VERSION_base(4,15,0)
  !(NS i#) = natVal (Proxy @n)

  msbN (NS w) =
    if isTrue# (i# `gtWord#` WORD_SIZE_IN_BITS##)
    then W# 0##
    else W# (w `uncheckedShiftRL#` (word2Int# (i# `minusWord#` 1##)))
  msbN (NB bn) = bigNatToWord (bigNatShiftR# bn (i# `minusWord#` 1##))
#else
  !(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) =
    if Int# -> Bool
isTrue# (Int#
i# Int# -> Int# -> Int#
># WORD_SIZE_IN_BITS#)
    then Word# -> Word
W# Word#
0##
    else 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#)))
#endif

{-# NOINLINE lsb# #-}
{-# ANN lsb# hasBlackBox #-}
-- | 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# #-}
{-# ANN slice# hasBlackBox #-}
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 (++#) #-}
{-# ANN (++#) hasBlackBox #-}
-- | 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
#if MIN_VERSION_base(4,15,0)
    size2 = fromIntegral (natVal bv2)
    v1' = naturalShiftL v1 size2
    m1' = naturalShiftL m1 size2
#else
    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
#endif

-- * Modifying BitVectors
{-# NOINLINE replaceBit# #-}
{-# ANN replaceBit# hasBlackBox #-}
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)
#if MIN_VERSION_base(4,15,0)
    | i >= 0 && i < sz = BV (clearBit m i .|. (naturalFromWord mb `shiftL` i))
#else
    | 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))
#endif
                            (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
#if MIN_VERSION_base(4,15,0)
    sz   = fromIntegral (natVal bv)
#else
    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)
#endif
    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# #-}
{-# ANN setSlice# hasBlackBox #-}
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# #-}
{-# ANN split# hasBlackBox #-}
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) =
#if MIN_VERSION_base(4,15,0)
  let n     = naturalToWord (natVal (Proxy @n))
      mask  = maskMod (natVal (Proxy @n))
      r     = mask i
      rMask = mask m
      l     = i `naturalShiftR` n
      lMask = m `naturalShiftR` n
#else
  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
#endif
  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# #-}
{-# ANN and# hasBlackBox #-}
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# #-}
{-# ANN or# hasBlackBox #-}
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# #-}
{-# ANN xor# hasBlackBox #-}
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# #-}
{-# ANN complement# hasBlackBox #-}
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# #-}
{-# ANN shiftL# hasBlackBox #-}
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
     -> String -> BitVector n
forall a. HasCallStack => String -> a
error (String -> BitVector n) -> String -> BitVector n
forall a b. (a -> b) -> a -> b
$ String
"'shiftL' undefined for negative number: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
     | Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral 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
0 Natural
0
     | Bool
otherwise
     -> 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)
 where
#if MIN_VERSION_base(4,15,0)
  sz = naturalToWord (natVal (Proxy @n))
  m = 1 `naturalShiftL` sz
#else
  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))
  m :: Natural
m = Natural
1 Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftL` Int
sz
#endif

{-# NOINLINE shiftR# #-}
{-# ANN shiftR# hasBlackBox #-}
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# #-}
{-# ANN rotateL# hasBlackBox #-}
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
#if MIN_VERSION_base(4,15,0)
      let vl    = naturalShiftL v b'
          vr    = naturalShiftR v b''

          ml    = naturalShiftL msk b'
          mr    = naturalShiftR msk b''

          b'   = fromIntegral b `mod` sz
#else
      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
#endif
          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 -> BitVector n) -> String -> BitVector n
forall a b. (a -> b) -> a -> b
$ String
"'rotateL' undefined for negative number: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
 where
#if MIN_VERSION_base(4,15,0)
  sz = naturalToWord (natVal (Proxy @n))
  m  = 1 `naturalShiftL` sz
#else
  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
#endif

{-# NOINLINE rotateR# #-}
{-# ANN rotateR# hasBlackBox #-}
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
#if MIN_VERSION_base(4,15,0)
      let vl   = naturalShiftR v b'
          vr   = naturalShiftL v b''
          ml   = naturalShiftR msk b'
          mr   = naturalShiftL msk b''
          b'   = fromIntegral b `mod` sz
#else
      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
#endif
          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 -> BitVector n) -> String -> BitVector n
forall a b. (a -> b) -> a -> b
$ String
"'rotateR' undefined for negative number: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
 where
#if MIN_VERSION_base(4,15,0)
  sz = naturalToWord (natVal (Proxy @n))
  m  = 1 `naturalShiftL` sz
#else
  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
#endif

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)
#if MIN_VERSION_base(4,15,0)
  where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @a))
#else
  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))
#endif
{-# NOINLINE truncateB# #-}
{-# ANN truncateB# hasBlackBox #-}

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

#if MIN_VERSION_template_haskell(2,17,0)
decBitVector :: Quote m => Natural -> m Type
decBitVector n = appT (conT ''BitVector) (litT $ numTyLit (integerFromNatural n))
#else
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)
#endif

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
SatError 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
undefined#
  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
SatError 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). KnownNat n => BitVector n
undefined#
  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
SatError 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
undefined#
  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 :: (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 :: (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 :: (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 :: 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 :: 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 functions
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. 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 #-}
{-# ANN checkUnpackUndef hasBlackBox #-}

-- | Create a BitVector with all its bits undefined
undefined# :: forall n . KnownNat n => BitVector n
undefined# :: BitVector n
undefined# =
#if MIN_VERSION_base(4,15,0)
  let m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
#else
  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))
#endif
  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# #-}
{-# ANN undefined# hasBlackBox #-}

-- | Check if one BitVector is similar to another, interpreting undefined bits
-- in the second argument as being "don't care" bits. This is a more lenient
-- version of '(==)', similar to @std_match@ in VHDL or @casez@ in Verilog.
--
-- >>> let expected = $(bLit "1.")
-- >>> let checked  = $(bLit "11")
--
-- >>> 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
--
--   * @\'.\'@ for bits which are not matched (wildcard)
--
--   * @\'_\'@ can be used as a separator similar to the NumericUnderscores
--   language extension
--
--   * lowercase alphabetical characters can be used to bind some bits to variables.
--   For example @"0aab11bb"@ will bind two variables @aa :: BitVector 2@ and
--   @bbb :: BitVector 3@ with their values set by the corresponding bits
--
-- The following example matches a byte against two bit patterns where
-- some bits are relevant and others are not while binding two variables @aa@
-- and @bb@:
--
-- @
--   decode :: Unsigned 8 -> Maybe Bool
--   decode $(bitPattern "00.._.110") = Just True
--   decode $(bitPattern "10.._0001") = Just False
--   decode $(bitPattern "aa.._b0b1") = Just (aa + bb > 1)
--   decode _ = Nothing
-- @
bitPattern :: String -> Q Pat
bitPattern :: String -> Q Pat
bitPattern String
s = [p| ((\_x -> $preprocess) -> $tuple) |]
  where
    (Integer
_, [Maybe Bit]
bs, Map Char [Integer] -> [(Char, [Integer])]
forall k a. Map k a -> [(k, a)]
M.toList -> [(Char, [Integer])]
ns) = (Char
 -> (Integer, [Maybe Bit], Map Char [Integer])
 -> (Integer, [Maybe Bit], Map Char [Integer]))
-> (Integer, [Maybe Bit], Map Char [Integer])
-> String
-> (Integer, [Maybe Bit], Map Char [Integer])
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
L.foldr Char
-> (Integer, [Maybe Bit], Map Char [Integer])
-> (Integer, [Maybe Bit], Map Char [Integer])
forall a a.
(Enum a, Num a) =>
Char
-> (a, [Maybe a], Map Char [a]) -> (a, [Maybe a], Map Char [a])
parse (Integer
0, [], Map Char [Integer]
forall k a. Map k a
M.empty) (String -> (Integer, [Maybe Bit], Map Char [Integer]))
-> String -> (Integer, [Maybe Bit], Map Char [Integer])
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'_') String
s

    var :: Char -> t a -> Q Pat
var Char
c t a
is = Name -> Q Pat
varP (Name -> Q Pat) -> (String -> Name) -> String -> Q Pat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name
mkName (String -> Q Pat) -> String -> Q Pat
forall a b. (a -> b) -> a -> b
$ Int -> Char -> String
forall a. Int -> a -> [a]
L.replicate (t a -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length t a
is) Char
c
    bitSelect :: Integer -> Q Exp
bitSelect Integer
i = [e| if testBit _x $(litE $ IntegerL i) then pack# high else pack# low |]
    varSelect :: t Integer -> Q Exp
varSelect t Integer
is = (Q Exp -> Q Exp -> Q Exp) -> t (Q Exp) -> Q Exp
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
L.foldr1 (\Q Exp
a Q Exp
b -> [e| $a ++# $b |]) (Integer -> Q Exp
bitSelect (Integer -> Q Exp) -> t Integer -> t (Q Exp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> t Integer
is)

    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
    maskE :: Q Exp
maskE = [e| $mask .&. _x |]
    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

    preprocess :: Q Exp
preprocess = [Q Exp] -> Q Exp
tupE ([Q Exp] -> Q Exp) -> [Q Exp] -> Q Exp
forall a b. (a -> b) -> a -> b
$ Q Exp
maskE Q Exp -> [Q Exp] -> [Q Exp]
forall a. a -> [a] -> [a]
: ([Integer] -> Q Exp
forall (t :: Type -> Type).
(Foldable t, Functor t) =>
t Integer -> Q Exp
varSelect ([Integer] -> Q Exp)
-> ((Char, [Integer]) -> [Integer]) -> (Char, [Integer]) -> Q Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char, [Integer]) -> [Integer]
forall a b. (a, b) -> b
snd ((Char, [Integer]) -> Q Exp) -> [(Char, [Integer])] -> [Q Exp]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Char, [Integer])]
ns)
    tuple :: Q Pat
tuple = [Q Pat] -> Q Pat
tupP ([Q Pat] -> Q Pat) -> [Q Pat] -> Q Pat
forall a b. (a -> b) -> a -> b
$ Q Pat
target Q Pat -> [Q Pat] -> [Q Pat]
forall a. a -> [a] -> [a]
: ((Char -> [Integer] -> Q Pat) -> (Char, [Integer]) -> Q Pat
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Char -> [Integer] -> Q Pat
forall (t :: Type -> Type) a. Foldable t => Char -> t a -> Q Pat
var ((Char, [Integer]) -> Q Pat) -> [(Char, [Integer])] -> [Q Pat]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Char, [Integer])]
ns)

    parse :: Char
-> (a, [Maybe a], Map Char [a]) -> (a, [Maybe a], Map Char [a])
parse Char
'.' (a
i, [Maybe a]
b, Map Char [a]
n) = (a -> a
forall a. Enum a => a -> a
succ a
i, Maybe a
forall a. Maybe a
NothingMaybe a -> [Maybe a] -> [Maybe a]
forall a. a -> [a] -> [a]
:[Maybe a]
b, Map Char [a]
n)
    parse Char
'0' (a
i, [Maybe a]
b, Map Char [a]
n) = (a -> a
forall a. Enum a => a -> a
succ a
i, a -> Maybe a
forall a. a -> Maybe a
Just a
0Maybe a -> [Maybe a] -> [Maybe a]
forall a. a -> [a] -> [a]
:[Maybe a]
b, Map Char [a]
n)
    parse Char
'1' (a
i, [Maybe a]
b, Map Char [a]
n) = (a -> a
forall a. Enum a => a -> a
succ a
i, a -> Maybe a
forall a. a -> Maybe a
Just a
1Maybe a -> [Maybe a] -> [Maybe a]
forall a. a -> [a] -> [a]
:[Maybe a]
b, Map Char [a]
n)
    parse Char
c (a
i, [Maybe a]
b, Map Char [a]
n)
      | Char -> Bool
C.isAlpha Char
c Bool -> Bool -> Bool
&& Char -> Bool
C.isLower Char
c =
        ( a -> a
forall a. Enum a => a -> a
succ a
i
        , Maybe a
forall a. Maybe a
NothingMaybe a -> [Maybe a] -> [Maybe a]
forall a. a -> [a] -> [a]
:[Maybe a]
b
        , (Maybe [a] -> Maybe [a]) -> Char -> Map Char [a] -> Map Char [a]
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
M.alter ([a] -> Maybe [a]
forall a. a -> Maybe a
Just ([a] -> Maybe [a]) -> (Maybe [a] -> [a]) -> Maybe [a] -> Maybe [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
ia -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ([a] -> [a]) -> (Maybe [a] -> [a]) -> Maybe [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Maybe [a] -> [a]
forall a. a -> Maybe a -> a
fromMaybe []) Char
c Map Char [a]
n
        )
      | Bool
otherwise = String -> (a, [Maybe a], Map Char [a])
forall a. HasCallStack => String -> a
error (String -> (a, [Maybe a], Map Char [a]))
-> String -> (a, [Maybe a], Map Char [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 String -> ShowS
forall a. [a] -> [a] -> [a]
++
        String
", expecting one of '0', '1', '.', '_', or a lowercase alphabetic character"