{-|
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 { forall (n :: Nat). BitVector n -> Natural
unsafeMask      :: !Natural
       , forall (n :: Nat). BitVector n -> Natural
unsafeToNatural :: !Natural
       }
  deriving (Typeable (BitVector n)
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 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))
gmapMo :: forall (m :: Type -> Type).
MonadPlus m =>
(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 (m :: Type -> Type).
MonadPlus m =>
(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 (m :: Type -> Type).
Monad m =>
(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 :: forall u. 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 u. (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 :: forall r r'.
(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 :: forall r r'.
(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 (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(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 (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(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 (c :: Type -> Type).
(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 (c :: Type -> Type).
(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)
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
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 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)
gmapMo :: forall (m :: Type -> Type).
MonadPlus m =>
(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 (m :: Type -> Type).
MonadPlus m =>
(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 (m :: Type -> Type).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Bit -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Bit -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Bit -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Bit -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(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 (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(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 (c :: Type -> Type).
(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 (c :: Type -> Type).
(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
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 :: HasCallStack => 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 :: forall (m :: Type -> Type). Quote m => Bit -> m Exp
lift (Bit Word
m Word
i) = [| fromInteger## $(litE (WordPrimL (toInteger m))) i |]
  {-# NOINLINE lift #-}
#if MIN_VERSION_template_haskell(2,16,0)
  liftTyped :: forall (m :: Type -> Type). Quote m => Bit -> Code m Bit
liftTyped = Bit -> Code m Bit
forall a (m :: Type -> Type). (Lift a, Quote m) => a -> Code m 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 -> BitVector 1
pack# (Bit (W# Word#
m) (W# Word#
b)) = Natural -> Natural -> BitVector 1
forall (n :: Nat). Natural -> Natural -> BitVector n
BV (Word# -> Natural
NS Word#
m) (Word# -> Natural
NS Word#
b)
#else
pack# (Bit (W# m) (W# b)) = BV (NatS# m) (NatS# 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 :: Natural -> Word
go (NS Word#
w) = Word# -> Word
W# Word#
w
  go (NB ByteArray#
w) = ByteArray# -> Word
bigNatToWord ByteArray#
w
#else
  go (NatS# w) = W# w
  go (NatJ# w) = W# (bigNatToWord 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 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 (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 :: HasCallStack => 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 -> ExpQ
bLit String
s = Exp -> ExpQ
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# :: forall (n :: Nat). 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# :: forall (n :: Nat). KnownNat n => 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# :: forall (n :: Nat). KnownNat n => 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# :: forall (n :: Nat). KnownNat n => 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# :: forall (n :: Nat). KnownNat n => 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# :: forall (n :: Nat). KnownNat n => 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# :: forall (n :: Nat). KnownNat n => 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# :: forall (n :: Nat). KnownNat n => 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# :: forall (n :: Nat). KnownNat n => 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# :: forall (n :: Nat). KnownNat n => 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 :: Natural
m = Natural
1 Natural -> Word -> Natural
`naturalShiftL` Natural -> Word
naturalToWord (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))
#else
  where m = 1 `shiftL` fromInteger (natVal (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# :: forall (n :: Nat).
KnownNat n =>
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 :: Natural
m = Natural
1 Natural -> Word -> Natural
`naturalShiftL` Natural -> Word
naturalToWord (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))
#else
  m = 1 `shiftL` fromInteger (natVal (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# :: forall (n :: Nat).
KnownNat n =>
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 :: Natural
m = Natural
1 Natural -> Word -> Natural
`naturalShiftL` Natural -> Word
naturalToWord (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))
#else
  where m = 1 `shiftL` fromInteger (natVal (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# :: forall (n :: Nat).
KnownNat n =>
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 :: Natural
m = Natural
1 Natural -> Word -> Natural
`naturalShiftL` Natural -> Word
naturalToWord (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))
#else
  where m = 1 `shiftL` fromInteger (natVal (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# :: forall (n :: Nat). 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# :: forall (n :: Nat). KnownNat n => BitVector n
maxBound# = let m :: Natural
m = Natural
1 Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftL` 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 #-}
+# :: forall (n :: Nat).
KnownNat n =>
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 :: Natural
m = Natural
1 Natural -> Word -> Natural
`naturalShiftL` Natural -> Word
naturalToWord (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))
#else
    m = 1 `shiftL` fromInteger (natVal (Proxy @n))
#endif

{-# NOINLINE (-#) #-}
{-# ANN (-#) hasBlackBox #-}
-# :: forall (n :: Nat).
KnownNat n =>
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 :: Natural
m = Natural
1 Natural -> Word -> Natural
`naturalShiftL` Natural -> Word
naturalToWord (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))
#else
    m = 1 `shiftL` fromInteger (natVal (Proxy @n))
#endif

{-# NOINLINE (*#) #-}
{-# ANN (*#) hasBlackBox #-}
*# :: forall (n :: Nat).
KnownNat n =>
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 :: Natural
m = (Natural
1 Natural -> Word -> Natural
`naturalShiftL` Natural -> Word
naturalToWord (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1
#else
  m = (1 `shiftL` fromInteger (natVal (Proxy @n))) - 1
#endif

{-# NOINLINE negate# #-}
{-# ANN negate# hasBlackBox #-}
negate# :: forall n . KnownNat n => BitVector n -> BitVector n
negate# :: forall (n :: Nat). KnownNat n => 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 :: Natural
m = Natural
1 Natural -> Word -> Natural
`naturalShiftL` Natural -> Word
naturalToWord (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))
#else
  m = 1 `shiftL` fromInteger (natVal (Proxy @n))
#endif

{-# NOINLINE fromInteger# #-}
{-# ANN fromInteger# hasBlackBox #-}
fromInteger# :: KnownNat n => Natural -> Integer -> BitVector n
fromInteger# :: forall (n :: Nat). KnownNat n => Natural -> Integer -> BitVector n
fromInteger# Natural
m Integer
i = Natural
sz Natural -> BitVector n -> BitVector n
`seq` BitVector n
mx
  where
#if MIN_VERSION_base(4,15,0)
    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` Natural
sz)
            (Integer -> Natural
integerToNatural (Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Natural -> Integer
integerFromNatural Natural
sz))
    sz :: Natural
sz  = Natural
1 Natural -> Word -> Natural
`naturalShiftL` Natural -> Word
naturalToWord (BitVector n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal BitVector n
mx)
#else
    mx = BV (m `mod` naturalFromInteger sz)
            (naturalFromInteger (i `mod` sz))
    sz  = 1 `shiftL` fromInteger (natVal 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# :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
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# :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
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 :: Natural
m = Natural
1 Natural -> Word -> Natural
`naturalShiftL` Natural -> Word
naturalToWord (Proxy (Max m n + 1) -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @(Max m n + 1)))
#else
  m = 1 `shiftL` fromInteger (natVal (Proxy @(Max m n + 1)))
#endif

{-# NOINLINE times# #-}
{-# ANN times# hasBlackBox #-}
times# :: (KnownNat m, KnownNat n) => BitVector m -> BitVector n -> BitVector (m + n)
times# :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
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# :: forall (n :: Nat).
KnownNat n =>
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# :: forall (n :: Nat).
KnownNat n =>
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# :: forall (n :: Nat). KnownNat n => 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 :: forall (n :: Nat). KnownNat n => 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 :: forall (n :: Nat). KnownNat n => 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# :: forall (n :: Nat). KnownNat n => 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 :: Natural
sz    = BitVector n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal BitVector n
bv
    maxI :: Natural
maxI  = (Natural
2 Natural -> Natural -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ Natural
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# :: forall (n :: Nat). KnownNat n => 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# :: forall (n :: Nat). KnownNat n => 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# :: forall (n :: Nat). KnownNat n => BitVector n -> Int
size# BitVector n
bv = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (BitVector n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal BitVector n
bv)
#else
size# bv = fromInteger (natVal bv)
#endif

{-# NOINLINE maxIndex# #-}
{-# ANN maxIndex# hasBlackBox #-}
maxIndex# :: KnownNat n => BitVector n -> Int
#if MIN_VERSION_base(4,15,0)
maxIndex# :: forall (n :: Nat). KnownNat n => BitVector n -> Int
maxIndex# BitVector n
bv = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (BitVector n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal BitVector n
bv) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
#else
maxIndex# bv = fromInteger (natVal bv) - 1
#endif

-- ** Indexing
{-# NOINLINE index# #-}
{-# ANN index# hasBlackBox #-}
index# :: KnownNat n => BitVector n -> Int -> Bit
index# :: forall (n :: Nat). KnownNat n => 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 :: Int
sz  = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (BitVector n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal BitVector n
bv)
#else
    sz  = fromInteger (natVal 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# :: forall (n :: Nat). KnownNat n => 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 Word#
i#) = Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n)

  msbN :: Natural -> Word
msbN (NS Word#
w) =
    if Int# -> Bool
isTrue# (Word#
i# Word# -> Word# -> Int#
`gtWord#` WORD_SIZE_IN_BITS##)
    then Word# -> Word
W# Word#
0##
    else Word# -> Word
W# (Word#
w Word# -> Int# -> Word#
`uncheckedShiftRL#` (Word# -> Int#
word2Int# (Word#
i# Word# -> Word# -> Word#
`minusWord#` Word#
1##)))
  msbN (NB ByteArray#
bn) = ByteArray# -> Word
bigNatToWord (ByteArray# -> Word# -> ByteArray#
bigNatShiftR# ByteArray#
bn (Word#
i# Word# -> Word# -> Word#
`minusWord#` Word#
1##))
#else
  !(S# i#) = natVal (Proxy @n)

  msbN (NatS# w) =
    if isTrue# (i# ># WORD_SIZE_IN_BITS#)
    then W# 0##
    else W# (w `uncheckedShiftRL#` (i# GHC.Exts.-# 1#))
  msbN (NatJ# bn) = W# (bigNatToWord (shiftRBigNat bn (i# GHC.Exts.-# 1#)))
#endif

{-# NOINLINE lsb# #-}
{-# ANN lsb# hasBlackBox #-}
-- | LSB
lsb# :: BitVector n -> Bit
lsb# :: forall (n :: Nat). 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# :: forall (m :: Nat) (i :: Nat) (n :: Nat).
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) ++# :: forall (m :: Nat) (n :: Nat).
KnownNat m =>
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 :: Word
size2 = Natural -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral (BitVector m -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal BitVector m
bv2)
    v1' :: Natural
v1' = Natural -> Word -> Natural
naturalShiftL Natural
v1 Word
size2
    m1' :: Natural
m1' = Natural -> Word -> Natural
naturalShiftL Natural
m1 Word
size2
#else
    size2 = fromInteger (natVal bv2)
    v1' = shiftL v1 size2
    m1' = shiftL m1 size2
#endif

-- * Modifying BitVectors
{-# NOINLINE replaceBit# #-}
{-# ANN replaceBit# hasBlackBox #-}
replaceBit# :: KnownNat n => BitVector n -> Int -> Bit -> BitVector n
replaceBit# :: forall (n :: Nat).
KnownNat n =>
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)
    | 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
naturalFromWord Word
mb Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftL` Int
i))
#else
    | i >= 0 && i < sz = BV (clearBit m i .|. (wordToNatural mb `shiftL` 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 :: Int
sz   = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (BitVector n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal BitVector n
bv)
#else
    sz   = fromInteger (natVal 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# :: forall (m :: Nat) (i :: Nat) (n :: Nat).
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 = Natural -> Natural -> Natural
complementMod (Proxy ((m + 1) + i) -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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# :: forall (n :: Nat) (m :: Nat).
KnownNat n =>
BitVector (m + n) -> (BitVector m, BitVector n)
split# (BV Natural
m Natural
i) =
#if MIN_VERSION_base(4,15,0)
  let n :: Word
n     = Natural -> Word
naturalToWord (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))
      mask :: Natural -> Natural
mask  = Natural -> Natural -> Natural
maskMod (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 -> Word -> Natural
`naturalShiftR` Word
n
      lMask :: Natural
lMask = Natural
m Natural -> Word -> Natural
`naturalShiftR` Word
n
#else
  let n     = fromInteger (natVal (Proxy @n))
      mask  = maskMod (natVal (Proxy @n))
      r     = mask i
      rMask = mask m
      l     = i `shiftR` n
      lMask = m `shiftR` 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# :: forall (n :: Nat).
KnownNat n =>
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 = Natural -> Natural -> Natural
complementMod (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))

{-# NOINLINE or# #-}
{-# ANN or# hasBlackBox #-}
or# :: forall (n :: Nat).
KnownNat n =>
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 = Natural -> Natural -> Natural
complementMod (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))

{-# NOINLINE xor# #-}
{-# ANN xor# hasBlackBox #-}
xor# :: forall (n :: Nat).
KnownNat n =>
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 = Natural -> Natural -> Natural
complementMod (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))

{-# NOINLINE complement# #-}
{-# ANN complement# hasBlackBox #-}
complement# :: forall n . KnownNat n => BitVector n -> BitVector n
complement# :: forall (n :: Nat). KnownNat n => 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 = Natural -> Natural -> Natural
complementMod (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))

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

{-# NOINLINE shiftL# #-}
{-# ANN shiftL# hasBlackBox #-}
shiftL# :: forall (n :: Nat). KnownNat n => 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 -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
>= Word
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 :: Word
sz = Natural -> Word
naturalToWord (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))
  m :: Natural
m = Natural
1 Natural -> Word -> Natural
`naturalShiftL` Word
sz
#else
  sz = fromInteger (natVal (Proxy @n))
  m = 1 `shiftL` sz
#endif

{-# NOINLINE shiftR# #-}
{-# ANN shiftR# hasBlackBox #-}
shiftR# :: forall (n :: Nat). KnownNat n => 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# :: forall (n :: Nat). KnownNat n => 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 :: Natural
vl    = Natural -> Word -> Natural
naturalShiftL Natural
v Word
b'
          vr :: Natural
vr    = Natural -> Word -> Natural
naturalShiftR Natural
v Word
b''

          ml :: Natural
ml    = Natural -> Word -> Natural
naturalShiftL Natural
msk Word
b'
          mr :: Natural
mr    = Natural -> Word -> Natural
naturalShiftR Natural
msk Word
b''

          b' :: Word
b'   = Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
b Word -> Word -> Word
forall a. Integral a => a -> a -> a
`mod` Word
sz
#else
      let vl    = shiftL v b'
          vr    = shiftR v b''

          ml    = shiftL msk b'
          mr    = shiftR msk b''

          b'   = b `mod` sz
#endif
          b'' :: Word
b''  = Word
sz Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
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 :: Word
sz = Natural -> Word
naturalToWord (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))
  m :: Natural
m  = Natural
1 Natural -> Word -> Natural
`naturalShiftL` Word
sz
#else
  sz = fromInteger (natVal (Proxy @n)) :: Int
  m  = 1 `shiftL` sz
#endif

{-# NOINLINE rotateR# #-}
{-# ANN rotateR# hasBlackBox #-}
rotateR# :: forall (n :: Nat). KnownNat n => 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 :: Natural
vl   = Natural -> Word -> Natural
naturalShiftR Natural
v Word
b'
          vr :: Natural
vr   = Natural -> Word -> Natural
naturalShiftL Natural
v Word
b''
          ml :: Natural
ml   = Natural -> Word -> Natural
naturalShiftR Natural
msk Word
b'
          mr :: Natural
mr   = Natural -> Word -> Natural
naturalShiftL Natural
msk Word
b''
          b' :: Word
b'   = Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
b Word -> Word -> Word
forall a. Integral a => a -> a -> a
`mod` Word
sz
#else
      let vl   = shiftR v b'
          vr   = shiftL v b''
          ml   = shiftR msk b'
          mr   = shiftL msk b''
          b'   = b `mod` sz
#endif
          b'' :: Word
b''  = Word
sz Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
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 :: Word
sz = Natural -> Word
naturalToWord (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))
  m :: Natural
m  = Natural
1 Natural -> Word -> Natural
`naturalShiftL` Word
sz
#else
  sz = fromInteger (natVal (Proxy @n)) :: Int
  m  = 1 `shiftL` sz
#endif

popCountBV :: forall n . KnownNat n => BitVector (n+1) -> I.Index (n+2)
popCountBV :: forall (n :: Nat). KnownNat n => 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 :: forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
BitVector n -> BitVector m
resize     = BitVector a -> BitVector b
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
BitVector n -> BitVector m
resizeBV
  zeroExtend :: forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
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 :: forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b) =>
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 :: forall (a :: Nat) (b :: Nat).
KnownNat a =>
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 :: forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
BitVector n -> BitVector m
resizeBV = case forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> SNatLE a b
compareSNat @n @m (forall (n :: Nat). KnownNat n => SNat n
SNat @n) (forall (n :: Nat). KnownNat n => SNat n
SNat @m) of
  SNatLE n m
SNatLE -> 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 -> 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# :: forall (a :: Nat) (b :: Nat).
KnownNat a =>
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 :: Natural
m = Natural
1 Natural -> Word -> Natural
`naturalShiftL` Natural -> Word
naturalToWord (Proxy a -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @a))
#else
  where m = 1 `shiftL` fromInteger (natVal (Proxy @a))
#endif
{-# NOINLINE truncateB# #-}
{-# ANN truncateB# hasBlackBox #-}

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

#if MIN_VERSION_template_haskell(2,17,0)
decBitVector :: Quote m => Natural -> m Type
decBitVector :: forall (m :: Type -> Type). Quote m => Natural -> m Type
decBitVector Natural
n = m Type -> m Type -> m Type
forall (m :: Type -> Type). Quote m => m Type -> m Type -> m Type
appT (Name -> m Type
forall (m :: Type -> Type). Quote m => Name -> m Type
conT ''BitVector) (m TyLit -> m Type
forall (m :: Type -> Type). Quote m => m TyLit -> m Type
litT (m TyLit -> m Type) -> m TyLit -> m Type
forall a b. (a -> b) -> a -> b
$ Integer -> m TyLit
forall (m :: Type -> Type). Quote m => Integer -> m TyLit
numTyLit (Natural -> Integer
integerFromNatural Natural
n))
#else
decBitVector :: Integer -> TypeQ
decBitVector n = appT (conT ''BitVector) (litT $ numTyLit 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 :: forall (n :: Nat) (p :: Nat -> Type).
(KnownNat n, Integral (p n)) =>
p n -> [p n]
shrinkSizedUnsigned p n
x | p n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal p n
x Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
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 :: forall b. 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 :: forall (m :: Nat) (n :: Nat) a.
(KnownNat m, KnownNat n) =>
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 :: forall (m :: Nat) (n :: Nat) a.
(KnownNat m, KnownNat n) =>
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 :: forall (m :: Nat) (n :: Nat) (o :: Nat) a.
(KnownNat m, KnownNat n, KnownNat o) =>
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 :: forall (n :: Nat) a. KnownNat n => 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 :: forall (n :: Nat) a. KnownNat n => 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 :: forall (n :: Nat) a.
(KnownNat n, Typeable a) =>
(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# :: forall (n :: Nat). KnownNat n => BitVector n
undefined# =
#if MIN_VERSION_base(4,15,0)
  let m :: Natural
m = Natural
1 Natural -> Word -> Natural
`naturalShiftL` Natural -> Word
naturalToWord (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @n))
#else
  let m = 1 `shiftL` fromInteger (natVal (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# :: forall (n :: Nat). KnownNat n => 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 = Natural -> Natural -> Natural
complementMod (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 -> m Pat
var Char
c t a
is = Name -> m Pat
forall (m :: Type -> Type). Quote m => Name -> m Pat
varP (Name -> m Pat) -> (String -> Name) -> String -> m Pat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name
mkName (String -> m Pat) -> String -> m 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 -> m Exp
bitSelect Integer
i = [e| if testBit _x $(litE $ IntegerL i) then pack# high else pack# low |]
    varSelect :: t Integer -> m Exp
varSelect t Integer
is = (m Exp -> m Exp -> m Exp) -> t (m Exp) -> m Exp
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
L.foldr1 (\m Exp
a m Exp
b -> [e| $a ++# $b |]) (Integer -> m Exp
forall {m :: Type -> Type}. Quote m => Integer -> m Exp
bitSelect (Integer -> m Exp) -> t Integer -> t (m Exp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> t Integer
is)

    mask :: ExpQ
mask = Lit -> ExpQ
forall (m :: Type -> Type). Quote m => Lit -> m Exp
litE (Lit -> ExpQ) -> ([Bit] -> Lit) -> [Bit] -> ExpQ
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] -> ExpQ) -> [Bit] -> ExpQ
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 :: ExpQ
maskE = [e| $mask .&. _x |]
    target :: Q Pat
target = Lit -> Q Pat
forall (m :: Type -> Type). Quote m => Lit -> m 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 :: ExpQ
preprocess = [ExpQ] -> ExpQ
forall (m :: Type -> Type). Quote m => [m Exp] -> m Exp
tupE ([ExpQ] -> ExpQ) -> [ExpQ] -> ExpQ
forall a b. (a -> b) -> a -> b
$ ExpQ
maskE ExpQ -> [ExpQ] -> [ExpQ]
forall a. a -> [a] -> [a]
: ([Integer] -> ExpQ
forall {t :: Type -> Type} {m :: Type -> Type}.
(Foldable t, Quote m, Functor t) =>
t Integer -> m Exp
varSelect ([Integer] -> ExpQ)
-> ((Char, [Integer]) -> [Integer]) -> (Char, [Integer]) -> ExpQ
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char, [Integer]) -> [Integer]
forall a b. (a, b) -> b
snd ((Char, [Integer]) -> ExpQ) -> [(Char, [Integer])] -> [ExpQ]
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
forall (m :: Type -> Type). Quote m => [m Pat] -> m 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 {m :: Type -> Type} {t :: Type -> Type} {a}.
(Quote m, Foldable t) =>
Char -> t a -> m 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"