clash-prelude-1.10.0: src/Clash/Sized/Internal/BitVector.hs
{-|
Copyright : (C) 2013-2016, University of Twente,
2019 , Gergő Érdi
2016-2019, Myrtle Software Ltd,
2021-2025, QBayLogic B.V.
2023 , Nadia Chambers
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
, hLit
, oLit
, 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
, xToBV
)
where
import Control.DeepSeq (NFData (..))
import Control.Exception (catch, evaluate)
import Control.Lens (Index, Ixed (..), IxValue)
import Data.Bits (Bits (..), FiniteBits (..))
import Data.Data (Data)
import Data.Default (Default (..))
import Data.Either (isLeft)
import Data.Proxy (Proxy (..))
import Data.Typeable (Typeable, typeOf)
import GHC.Generics (Generic)
import Data.Maybe (fromMaybe)
import Numeric (readOct, readHex)
import GHC.Exts
(Word#, Word (W#), eqWord#, int2Word#, isTrue#, uncheckedShiftRL#)
import GHC.Exts (minusWord#, gtWord#, word2Int#, dataToTag#)
import GHC.Num.BigNat (bigNatShiftR#, bigNatToWord)
import GHC.Num.Integer (integerFromNatural, integerToNatural)
import GHC.Num.Natural
(Natural (..), naturalFromWord, naturalShiftL, naturalShiftR, naturalToWord)
import GHC.Natural (naturalToInteger)
import GHC.Stack (withFrozenCallStack)
import GHC.TypeLits (KnownNat, Nat, type (+), type (-))
import GHC.TypeNats (natVal)
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(..))
import Language.Haskell.TH.Compat
import Language.Haskell.TH (Quote)
import System.IO.Unsafe (unsafeDupablePerformIO)
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.Sized.Internal (formatRange)
import Clash.XException
(ShowX (..), NFDataX (..), errorX, isX, showsPrecXWith, rwhnfX, XException(..))
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.
--
-- __NB__: The usual Haskell method of converting an integral numeric type to
-- another, 'fromIntegral', is not well suited for Clash as it will go through
-- 'Integer' which is arbitrarily bounded in HDL. Instead use
-- 'Clash.Class.BitPack.bitCoerce' and the 'Resize' class.
--
-- 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 sizes of BitVector. To change
-- the size, use the functions in the 'Resize' class.
data BitVector (n :: Nat) =
-- | The constructor, 'BV', and the fields, 'unsafeMask' and 'unsafeToNatural', are not
-- synthesizable.
BV { unsafeMask :: !Natural
, unsafeToNatural :: !Natural
}
deriving (Data, Generic)
{-# ANN BV hasBlackBox #-}
-- * Bit
-- | A single bit
--
-- __NB__: The usual Haskell method of converting an integral numeric type to
-- another, 'fromIntegral', is not well suited for Clash as it will go through
-- 'Integer' which is arbitrarily bounded in HDL. Instead use
-- 'Clash.Class.BitPack.bitCoerce' and the 'Resize' class.
data Bit =
-- | The constructor, 'Bit', and the fields, 'unsafeMask#' and 'unsafeToInteger#', are not
-- synthesizable.
Bit { unsafeMask# :: {-# unpack #-} !Word
, unsafeToInteger# :: {-# unpack #-} !Word
}
deriving (Data, Generic)
{-# ANN Bit hasBlackBox #-}
-- * Constructions
-- ** Initialisation
{-# OPAQUE high #-}
{-# ANN high hasBlackBox #-}
-- | logic '1'
high :: Bit
high = Bit 0 1
{-# OPAQUE low #-}
{-# ANN low hasBlackBox #-}
-- | logic '0'
low :: Bit
low = Bit 0 0
-- ** Instances
instance NFData Bit where
rnf (Bit m i) = rnf m `seq` rnf i `seq` ()
{-# NOINLINE rnf #-}
instance Show Bit where
show (Bit 0 b) =
case testBit b 0 of
True -> "1"
False -> "0"
show (Bit _ _) = "."
instance ShowX Bit where
showsPrecX = showsPrecXWith showsPrec
instance NFDataX Bit where
deepErrorX = errorX
ensureSpine = unpack# . xToBV . pack#
rnfX = rwhnfX
hasUndefined bv = isLeft (isX bv) || unsafeMask# bv /= 0
instance Lift Bit where
lift (Bit m i) = [| fromInteger## $(litE (WordPrimL (toInteger m))) i |]
{-# NOINLINE lift #-}
liftTyped = liftTypedFromUntyped
instance Eq Bit where
(==) = eq##
(/=) = neq##
eq## :: Bit -> Bit -> Bool
eq## b1 b2 = eq# (pack# b1) (pack# b2)
{-# OPAQUE eq## #-}
{-# ANN eq## hasBlackBox #-}
neq## :: Bit -> Bit -> Bool
neq## b1 b2 = neq# (pack# b1) (pack# b2)
{-# OPAQUE neq## #-}
{-# ANN neq## hasBlackBox #-}
instance Ord Bit where
(<) = lt##
(<=) = le##
(>) = gt##
(>=) = ge##
lt##,ge##,gt##,le## :: Bit -> Bit -> Bool
lt## b1 b2 = lt# (pack# b1) (pack# b2)
{-# OPAQUE lt## #-}
{-# ANN lt## hasBlackBox #-}
ge## b1 b2 = ge# (pack# b1) (pack# b2)
{-# OPAQUE ge## #-}
{-# ANN ge## hasBlackBox #-}
gt## b1 b2 = gt# (pack# b1) (pack# b2)
{-# OPAQUE gt## #-}
{-# ANN gt## hasBlackBox #-}
le## b1 b2 = le# (pack# b1) (pack# b2)
{-# OPAQUE le## #-}
{-# ANN le## hasBlackBox #-}
instance Enum Bit where
toEnum = toEnum##
fromEnum b = if eq## b low then 0 else 1
toEnum## :: Int -> Bit
toEnum## = fromInteger## 0## . toInteger
{-# OPAQUE toEnum## #-}
{-# ANN toEnum## hasBlackBox #-}
instance Bounded Bit where
minBound = low
maxBound = high
instance Default Bit where
def = low
instance Num Bit where
(+) = xor##
(-) = xor##
(*) = and##
negate = id
abs = id
signum b = b
fromInteger = fromInteger## 0##
fromInteger## :: Word# -> Integer -> Bit
fromInteger## m# i = Bit ((W# m#) `mod` 2) (fromInteger i `mod` 2)
{-# OPAQUE fromInteger## #-}
{-# ANN fromInteger## hasBlackBox #-}
instance Real Bit where
toRational b = if eq## b low then 0 else 1
instance Integral Bit where
quot a _ = a
rem _ _ = low
div a _ = a
mod _ _ = low
quotRem n _ = (n,low)
divMod n _ = (n,low)
toInteger b = if eq## b low then 0 else 1
instance Bits Bit where
(.&.) = and##
(.|.) = or##
xor = xor##
complement = complement##
zeroBits = low
bit i = if i == 0 then high else low
setBit b i = if i == 0 then high else b
clearBit b i = if i == 0 then low else b
complementBit b i = if i == 0 then complement## b else b
testBit b i = if i == 0 then eq## b high else False
bitSizeMaybe _ = Just 1
bitSize _ = 1
isSigned _ = False
shift b i = if i == 0 then b else low
shiftL b i = if i == 0 then b else low
shiftR b i = if i == 0 then b else low
rotate b _ = b
rotateL b _ = b
rotateR b _ = b
popCount b = if eq## b low then 0 else 1
instance FiniteBits Bit where
finiteBitSize _ = 1
countLeadingZeros b = if eq## b low then 1 else 0
countTrailingZeros b = if eq## b low then 1 else 0
and##, or##, xor## :: Bit -> Bit -> Bit
and## (Bit m1 v1) (Bit m2 v2) = Bit mask (v1 .&. v2 .&. complement mask)
where mask = (m1.&.v2 .|. m1.&.m2 .|. m2.&.v1)
{-# OPAQUE and## #-}
{-# ANN and## hasBlackBox #-}
or## (Bit m1 v1) (Bit m2 v2) = Bit mask ((v1 .|. v2) .&. complement mask)
where mask = m1 .&. complement v2 .|. m1.&.m2 .|. m2 .&. complement v1
{-# OPAQUE or## #-}
{-# ANN or## hasBlackBox #-}
xor## (Bit m1 v1) (Bit m2 v2) = Bit mask ((v1 `xor` v2) .&. complement mask)
where mask = m1 .|. m2
{-# OPAQUE xor## #-}
{-# ANN xor## hasBlackBox #-}
complement## :: Bit -> Bit
complement## (Bit m v) = Bit m (complementB v .&. complementB m)
where complementB (W# b#) = W# (int2Word# (eqWord# b# 0##))
{-# OPAQUE complement## #-}
{-# ANN complement## hasBlackBox #-}
-- *** BitPack
pack# :: Bit -> BitVector 1
pack# (Bit (W# m) (W# b)) = BV (NS m) (NS b)
{-# OPAQUE pack# #-}
{-# ANN pack# hasBlackBox #-}
unpack# :: BitVector 1 -> Bit
unpack# (BV m b) = Bit (go m) (go b)
where
go (NS w) = W# w
go (NB w) = bigNatToWord w
{-# OPAQUE unpack# #-}
{-# ANN unpack# hasBlackBox #-}
-- * Instances
instance NFData (BitVector n) where
rnf (BV i m) = rnf i `seq` rnf 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 (BV m i) =
case natToNum @n @Int of
0 -> "0"
_ -> '0' : 'b' : go groupSize (natToNum @n @Int) m i []
where
go _ 0 _ _ s = s
go c n m0 v0 s =
let
(!v1, !vBit) = quotRem v0 2
(!m1, !mBit) = quotRem m0 2
!renderedBit = showBit mBit vBit
in
case c of
0 -> go (groupSize - 1) (n - 1) m1 v1 (renderedBit : '_' : s)
_ -> go (c - 1) (n - 1) m1 v1 (renderedBit : s)
showBit 0 0 = '0'
showBit 0 1 = '1'
showBit _ _ = '.'
groupSize :: Int
groupSize = 4
{-# NOINLINE show #-}
instance KnownNat n => ShowX (BitVector n) where
showsPrecX = showsPrecXWith showsPrec
instance KnownNat n => NFDataX (BitVector n) where
deepErrorX _ = undefined#
rnfX = rwhnfX
hasUndefined bv = isLeft (isX bv) || unsafeMask bv /= 0
ensureSpine = xToBV -- Converts `XException` to 'undefined#'
-- | 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.
--
-- __NB__: 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 s = pure (SigE body typ)
where
typ = ConT ''BitVector `AppT` LitT (NumTyLit (toInteger n))
body = VarE 'fromInteger# `AppE` iLit mask `AppE` iLit value
iLit = LitE . IntegerL . toInteger
(n, BV mask value) = read# s :: (Natural, BitVector n)
read# :: String -> (Natural, BitVector n)
read# cs0 = (fromIntegral (length cs1), BV m v)
where
cs1 = filter (/= '_') cs0
(vs, ms) = unzip (map readBit cs1)
combineBits = foldl (\b a -> b*2+a) 0
v = combineBits vs
m = combineBits ms
readBit c = case c of
'0' -> (0,0)
'1' -> (1,0)
'.' -> (0,1)
_ -> error $
"Clash.Sized.Internal.bLit: unknown character: "
++ show c ++ " in input: " ++ cs0
-- | Create a hexadecimal literal
--
-- >>> $(hLit "dead")
-- 0b1101_1110_1010_1101
--
-- Don't care digits set 4 bits:
--
-- >>> $(hLit "de..")
-- 0b1101_1110_...._....
hLit :: String -> ExpQ
hLit s = pure (SigE body typ)
where
typ = ConT ''BitVector `AppT` LitT (NumTyLit (toInteger n))
body = VarE 'fromInteger# `AppE` iLit mask `AppE` iLit value
iLit = LitE . IntegerL . toInteger
(n, BV mask value) = read16# s :: (Natural, BitVector n)
read16# :: String -> (Natural, BitVector n)
read16# cs0 = (fromIntegral $ 4 * length cs1, BV m v)
where
cs1 = filter (/= '_') cs0
(vs, ms) = unzip $ map readHexDigit cs1
combineHexDigits = foldl (\b a -> 16*b+a) 0
v = combineHexDigits vs
m = combineHexDigits ms
-- The dot is a don't care, which applies to a whole digit.
readHexDigit '.' = (0, 0xf)
readHexDigit c = case readHex [c] of
[(n, "")] -> (n, 0)
_ -> error $
"Clash.Sized.Internal.hLit: unknown character: "
++ show c ++ " in input: " ++ cs0
-- | Create an octal literal
--
-- >>> $(oLit "5234")
-- 0b1010_1001_1100
--
-- Don't care digits set 3 bits:
--
-- >>> $(oLit "52..")
-- 0b1010_10.._....
oLit :: String -> ExpQ
oLit s = pure (SigE body typ)
where
typ = ConT ''BitVector `AppT` LitT (NumTyLit (toInteger n))
body = VarE 'fromInteger# `AppE` iLit mask `AppE` iLit value
iLit = LitE . IntegerL . toInteger
(n, BV mask value) = read8# s :: (Natural, BitVector n)
read8# :: String -> (Natural, BitVector n)
read8# cs0 = (fromIntegral $ 3 * length cs1, BV m v)
where
cs1 = filter (/= '_') cs0
(vs, ms) = unzip $ map readOctDigit cs1
combineOctDigits = foldl (\b a -> 8*b+a) 0
v = combineOctDigits vs
m = combineOctDigits ms
-- The dot is a don't care, which applies to a whole digit.
readOctDigit '.' = (0, 0o7)
readOctDigit c = case readOct [c] of
[(n, "")] -> (n, 0)
_ -> error $
"Clash.Sized.Internal.oLit: unknown character: "
++ show c ++ " in input: " ++ cs0
instance KnownNat n => Eq (BitVector n) where
(==) = eq#
(/=) = neq#
{-# OPAQUE eq# #-}
{-# ANN eq# hasBlackBox #-}
eq# :: KnownNat n => BitVector n -> BitVector n -> Bool
eq# (BV 0 v1) (BV 0 v2 ) = v1 == v2
eq# bv1 bv2 = undefErrorI "==" bv1 bv2
{-# OPAQUE neq# #-}
{-# ANN neq# hasBlackBox #-}
neq# :: KnownNat n => BitVector n -> BitVector n -> Bool
neq# (BV 0 v1) (BV 0 v2) = v1 /= v2
neq# bv1 bv2 = undefErrorI "/=" bv1 bv2
instance KnownNat n => Ord (BitVector n) where
(<) = lt#
(>=) = ge#
(>) = gt#
(<=) = le#
lt#,ge#,gt#,le# :: KnownNat n => BitVector n -> BitVector n -> Bool
{-# OPAQUE lt# #-}
{-# ANN lt# hasBlackBox #-}
lt# (BV 0 n) (BV 0 m) = n < m
lt# bv1 bv2 = undefErrorI "<" bv1 bv2
{-# OPAQUE ge# #-}
{-# ANN ge# hasBlackBox #-}
ge# (BV 0 n) (BV 0 m) = n >= m
ge# bv1 bv2 = undefErrorI ">=" bv1 bv2
{-# OPAQUE gt# #-}
{-# ANN gt# hasBlackBox #-}
gt# (BV 0 n) (BV 0 m) = n > m
gt# bv1 bv2 = undefErrorI ">" bv1 bv2
{-# OPAQUE le# #-}
{-# ANN le# hasBlackBox #-}
le# (BV 0 n) (BV 0 m) = n <= m
le# bv1 bv2 = undefErrorI "<=" bv1 bv2
-- | The functions: 'enumFrom', 'enumFromThen', 'enumFromTo', and
-- 'enumFromThenTo', are not synthesizable.
instance KnownNat n => Enum (BitVector n) where
succ = (+# fromInteger# 0 1)
pred = (-# fromInteger# 0 1)
toEnum = toEnum#
fromEnum = fromEnum#
enumFrom = enumFrom#
enumFromThen = enumFromThen#
enumFromTo = enumFromTo#
enumFromThenTo = enumFromThenTo#
toEnum# :: forall n. KnownNat n => Int -> BitVector n
toEnum# = fromInteger# 0 . toInteger
{-# OPAQUE toEnum# #-}
{-# ANN toEnum# hasBlackBox #-}
fromEnum# :: forall n. KnownNat n => BitVector n -> Int
fromEnum# = fromEnum . toInteger#
{-# OPAQUE fromEnum# #-}
{-# ANN fromEnum# hasBlackBox #-}
enumFrom# :: forall n. KnownNat n => BitVector n -> [BitVector n]
enumFrom# (BV 0 x) = map (BV 0 . (`mod` m)) [x .. unsafeToNatural (maxBound :: BitVector n)]
where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
enumFrom# bv = undefErrorU "enumFrom" bv
{-# OPAQUE enumFrom# #-}
enumFromThen#
:: forall n
. KnownNat n
=> BitVector n
-> BitVector n
-> [BitVector n]
enumFromThen# (BV 0 x) (BV 0 y) =
toBvs [x, y .. unsafeToNatural bound]
where
bound = if x <= y then maxBound else minBound :: BitVector n
toBvs = map (BV 0 . (`mod` m))
m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
enumFromThen# bv1 bv2 = undefErrorP "enumFromThen" bv1 bv2
{-# OPAQUE enumFromThen# #-}
enumFromTo#
:: forall n
. KnownNat n
=> BitVector n
-> BitVector n
-> [BitVector n]
enumFromTo# (BV 0 x) (BV 0 y) = map (BV 0 . (`mod` m)) [x .. y]
where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
enumFromTo# bv1 bv2 = undefErrorP "enumFromTo" bv1 bv2
{-# OPAQUE enumFromTo# #-}
enumFromThenTo#
:: forall n
. KnownNat n
=> BitVector n
-> BitVector n
-> BitVector n
-> [BitVector n]
enumFromThenTo# (BV 0 x1) (BV 0 x2) (BV 0 y) = map (BV 0 . (`mod` m)) [x1, x2 .. y]
where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
enumFromThenTo# bv1 bv2 bv3 = undefErrorP3 "enumFromTo" bv1 bv2 bv3
{-# OPAQUE enumFromThenTo# #-}
instance KnownNat n => Bounded (BitVector n) where
minBound = minBound#
maxBound = maxBound#
minBound# :: BitVector n
minBound# = BV 0 0
{-# OPAQUE minBound# #-}
{-# ANN minBound# hasBlackBox #-}
maxBound# :: forall n. KnownNat n => BitVector n
maxBound# = let m = 1 `shiftL` natToNum @n in BV 0 (m-1)
{-# OPAQUE maxBound# #-}
{-# ANN maxBound# hasBlackBox #-}
-- | __NB__: 'fromInteger'/'fromIntegral' can cause unexpected truncation, as
-- 'Integer' is arbitrarily bounded during synthesis. Prefer
-- 'Clash.Class.BitPack.bitCoerce' and the 'Resize' class.
instance KnownNat n => Num (BitVector n) where
(+) = (+#)
(-) = (-#)
(*) = (*#)
negate = negate#
abs = id
signum bv = resizeBV (pack# (reduceOr# bv))
fromInteger = fromInteger# 0
(+#),(-#),(*#) :: forall n . KnownNat n => BitVector n -> BitVector n -> BitVector n
{-# OPAQUE (+#) #-}
{-# ANN (+#) hasBlackBox #-}
(+#) = go
where
go (BV 0 i) (BV 0 j) = BV 0 (addMod m i j)
go bv1 bv2 = undefErrorI "+" bv1 bv2
m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
{-# OPAQUE (-#) #-}
{-# ANN (-#) hasBlackBox #-}
(-#) = go
where
go (BV 0 i) (BV 0 j) = BV 0 (subMod m i j)
go bv1 bv2 = undefErrorI "-" bv1 bv2
m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
{-# OPAQUE (*#) #-}
{-# ANN (*#) hasBlackBox #-}
(*#) = go
where
go (BV 0 i) (BV 0 j) = BV 0 (mulMod2 m i j)
go bv1 bv2 = undefErrorI "*" bv1 bv2
m = (1 `naturalShiftL` naturalToWord (natVal (Proxy @n))) - 1
{-# OPAQUE negate# #-}
{-# ANN negate# hasBlackBox #-}
negate# :: forall n . KnownNat n => BitVector n -> BitVector n
negate# = go
where
go (BV 0 i) = BV 0 (negateMod m i)
go bv = undefErrorU "negate" bv
m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
{-# OPAQUE fromInteger# #-}
{-# ANN fromInteger# hasBlackBox #-}
fromInteger# :: KnownNat n => Natural -> Integer -> BitVector n
fromInteger# m i = sz `seq` mx
where
mx = BV (m `mod` sz)
(integerToNatural (i `mod` integerFromNatural sz))
sz = 1 `naturalShiftL` naturalToWord (natVal mx)
instance (KnownNat m, KnownNat n) => ExtendingNum (BitVector m) (BitVector n) where
type AResult (BitVector m) (BitVector n) = BitVector (Max m n + 1)
add = plus#
sub = minus#
type MResult (BitVector m) (BitVector n) = BitVector (m + n)
mul = times#
{-# OPAQUE plus# #-}
{-# ANN plus# hasBlackBox #-}
plus# :: (KnownNat m, KnownNat n) => BitVector m -> BitVector n -> BitVector (Max m n + 1)
plus# (BV 0 a) (BV 0 b) = BV 0 (a + b)
plus# bv1 bv2 = undefErrorP "add" bv1 bv2
{-# OPAQUE minus# #-}
{-# ANN minus# hasBlackBox #-}
minus# :: forall m n . (KnownNat m, KnownNat n) => BitVector m -> BitVector n
-> BitVector (Max m n + 1)
minus# = go
where
go (BV 0 a) (BV 0 b) = BV 0 (subMod m a b)
go bv1 bv2 = undefErrorP "sub" bv1 bv2
m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @(Max m n + 1)))
{-# OPAQUE times# #-}
{-# ANN times# hasBlackBox #-}
times# :: (KnownNat m, KnownNat n) => BitVector m -> BitVector n -> BitVector (m + n)
times# (BV 0 a) (BV 0 b) = BV 0 (a * b)
times# bv1 bv2 = undefErrorP "mul" bv1 bv2
instance KnownNat n => Real (BitVector n) where
toRational = toRational . toInteger#
-- | __NB__: 'toInteger'/'fromIntegral' can cause unexpected truncation, as
-- 'Integer' is arbitrarily bounded during synthesis. Prefer
-- 'Clash.Class.BitPack.bitCoerce' and the 'Resize' class.
instance KnownNat n => Integral (BitVector n) where
quot = quot#
rem = rem#
div = quot#
mod = rem#
quotRem n d = (n `quot#` d,n `rem#` d)
divMod n d = (n `quot#` d,n `rem#` d)
toInteger = toInteger#
quot#,rem# :: KnownNat n => BitVector n -> BitVector n -> BitVector n
{-# OPAQUE quot# #-}
{-# ANN quot# hasBlackBox #-}
quot# (BV 0 i) (BV 0 j) = BV 0 (i `quot` j)
quot# bv1 bv2 = undefErrorP "quot" bv1 bv2
{-# OPAQUE rem# #-}
{-# ANN rem# hasBlackBox #-}
rem# (BV 0 i) (BV 0 j) = BV 0 (i `rem` j)
rem# bv1 bv2 = undefErrorP "rem" bv1 bv2
{-# OPAQUE toInteger# #-}
{-# ANN toInteger# hasBlackBox #-}
toInteger# :: KnownNat n => BitVector n -> Integer
toInteger# (BV 0 i) = naturalToInteger i
toInteger# bv = undefErrorU "toInteger" bv
-- | @'shiftR' a n@:
--
-- * Returns 0 if @n >= 'bitSize' a@
-- * 'Clash.XException.XException' if @n < 0@
instance KnownNat n => Bits (BitVector n) where
(.&.) = and#
(.|.) = or#
xor = xor#
complement = complement#
zeroBits = 0
bit i = replaceBit# 0 i high
setBit v i = replaceBit# v i high
clearBit v i = replaceBit# v i low
complementBit v i = replaceBit# v i (complement## (index# v i))
testBit v i = eq## (index# v i) high
bitSizeMaybe v = Just (size# v)
bitSize = size#
isSigned _ = False
shiftL v i = shiftL# v i
shiftR v i = shiftR# v i
rotateL v i = rotateL# v i
rotateR v i = rotateR# v i
popCount bv = fromInteger (I.toInteger# (popCountBV (bv ++# (0 :: BitVector 1))))
instance KnownNat n => FiniteBits (BitVector n) where
finiteBitSize = size#
countLeadingZeros = fromInteger . I.toInteger# . countLeadingZerosBV
countTrailingZeros = fromInteger . I.toInteger# . countTrailingZerosBV
countLeadingZerosBV :: KnownNat n => BitVector n -> I.Index (n+1)
countLeadingZerosBV = V.foldr (\l r -> if eq## l low then 1 + r else 0) 0 . V.bv2v
{-# INLINE countLeadingZerosBV #-}
countTrailingZerosBV :: KnownNat n => BitVector n -> I.Index (n+1)
countTrailingZerosBV = V.foldl (\l r -> if eq## r low then 1 + l else 0) 0 . V.bv2v
{-# INLINE countTrailingZerosBV #-}
{-# OPAQUE reduceAnd# #-}
{-# ANN reduceAnd# hasBlackBox #-}
reduceAnd# :: KnownNat n => BitVector n -> Bit
reduceAnd# bv@(BV 0 i) = Bit 0 (W# (int2Word# (dataToTag# check)))
where
check = i == maxI
sz = natVal bv
maxI = (2 ^ sz) - 1
reduceAnd# bv@(BV m i) =
-- If any defined bit is 0, i.e., 'm .|. i /= maxI', then the result is
-- '0' (Bit 0 0), otherwise the result is '.' (Bit 1 0).
Bit (W# (int2Word# (dataToTag# check))) 0
where
check = m .|. i == maxI
sz = natVal bv
maxI = (2 ^ sz) - 1
{-# OPAQUE reduceOr# #-}
{-# ANN reduceOr# hasBlackBox #-}
reduceOr# :: KnownNat n => BitVector n -> Bit
reduceOr# (BV 0 i) = Bit 0 (W# (int2Word# (dataToTag# check)))
where
check = i /= 0
reduceOr# bv@(BV m i) | defI /= 0 = Bit 0 1
| otherwise = Bit 1 0
where
complementN = complementMod $ natVal bv
defI = i .&. (complementN m)
{-# OPAQUE reduceXor# #-}
{-# ANN reduceXor# hasBlackBox #-}
reduceXor# :: KnownNat n => BitVector n -> Bit
reduceXor# (BV 0 i) = Bit 0 (fromIntegral (popCount i `mod` 2))
reduceXor# _ = Bit 1 0
instance Default (BitVector n) where
def = minBound#
-- * Accessors
-- ** Length information
{-# OPAQUE size# #-}
{-# ANN size# hasBlackBox #-}
size# :: KnownNat n => BitVector n -> Int
size# bv = fromIntegral (natVal bv)
{-# OPAQUE maxIndex# #-}
{-# ANN maxIndex# hasBlackBox #-}
maxIndex# :: KnownNat n => BitVector n -> Int
maxIndex# bv = fromIntegral (natVal bv) - 1
-- ** Indexing
{-# OPAQUE index# #-}
{-# ANN index# hasBlackBox #-}
index# :: KnownNat n => BitVector n -> Int -> Bit
index# bv@(BV m v) i
| i >= 0 && i < sz = Bit (W# (int2Word# (dataToTag# (testBit m i))))
(W# (int2Word# (dataToTag# (testBit v i))))
| otherwise = err
where
sz = fromIntegral (natVal bv)
err = error $ concat [ "(!): "
, show i
, " is out of range "
, formatRange 0 (sz - 1)
]
{-# OPAQUE msb# #-}
{-# ANN msb# hasBlackBox #-}
-- | MSB
msb# :: forall n . KnownNat n => BitVector n -> Bit
msb# (BV m v)
= Bit (msbN m)
(msbN v)
where
!(NS i#) = natVal (Proxy @n)
msbN (NS w) =
if isTrue# (i# `gtWord#` WORD_SIZE_IN_BITS##)
then W# 0##
else W# (w `uncheckedShiftRL#` (word2Int# (i# `minusWord#` 1##)))
msbN (NB bn) = bigNatToWord (bigNatShiftR# bn (i# `minusWord#` 1##))
{-# OPAQUE lsb# #-}
{-# ANN lsb# hasBlackBox #-}
-- | LSB
lsb# :: BitVector n -> Bit
lsb# (BV m v) = Bit (W# (int2Word# (dataToTag# (testBit m 0))))
(W# (int2Word# (dataToTag# (testBit v 0))))
{-# OPAQUE slice# #-}
{-# ANN slice# hasBlackBox #-}
slice# :: BitVector (m + 1 + i) -> SNat m -> SNat n -> BitVector (m + 1 - n)
slice# (BV msk i) m n = BV (shiftR (msk .&. mask) n')
(shiftR (i .&. mask) n')
where
m' = snatToInteger m
n' = snatToNum n
mask = 2 ^ (m' + 1) - 1
-- * Constructions
-- ** Concatenation
{-# OPAQUE (++#) #-}
{-# ANN (++#) hasBlackBox #-}
-- | Concatenate two 'BitVector's
(++#) :: KnownNat m => BitVector n -> BitVector m -> BitVector (n + m)
(BV m1 v1) ++# bv2@(BV m2 v2) = BV (m1' .|. m2) (v1' .|. v2)
where
size2 = fromIntegral (natVal bv2)
v1' = naturalShiftL v1 size2
m1' = naturalShiftL m1 size2
-- * Modifying BitVectors
{-# OPAQUE replaceBit# #-}
{-# ANN replaceBit# hasBlackBox #-}
replaceBit# :: KnownNat n => BitVector n -> Int -> Bit -> BitVector n
replaceBit# bv@(BV m v) i (Bit mb b)
| i >= 0 && i < sz = BV (clearBit m i .|. (naturalFromWord mb `shiftL` i))
(if testBit b 0 && mb == 0 then setBit v i else clearBit v i)
| otherwise = err
where
sz = fromIntegral (natVal bv)
err = error $ concat [ "replaceBit: "
, show i
, " is out of range "
, formatRange 0 (sz - 1)
]
{-# OPAQUE setSlice# #-}
{-# ANN setSlice# hasBlackBox #-}
setSlice#
:: forall m i n
. SNat (m + 1 + i)
-> BitVector (m + 1 + i)
-> SNat m
-> SNat n
-> BitVector (m + 1 - n)
-> BitVector (m + 1 + i)
setSlice# SNat =
\(BV iMask i) m@SNat n (BV jMask j) ->
let m' = snatToInteger m
n' = snatToInteger n
j' = shiftL j (fromInteger n')
jMask' = shiftL jMask (fromInteger n')
mask = complementN ((2 ^ (m' + 1) - 1) `xor` (2 ^ n' - 1))
in BV ((iMask .&. mask) .|. jMask') ((i .&. mask) .|. j')
where
complementN = complementMod (natVal (Proxy @(m + 1 + i)))
{-# OPAQUE split# #-}
{-# ANN split# hasBlackBox #-}
split#
:: forall n m
. KnownNat n
=> BitVector (m + n)
-> (BitVector m, BitVector n)
split# (BV m i) =
let n = naturalToWord (natVal (Proxy @n))
mask = maskMod (natVal (Proxy @n))
r = mask i
rMask = mask m
l = i `naturalShiftR` n
lMask = m `naturalShiftR` n
in (BV lMask l, BV rMask r)
and#, or#, xor# :: forall n . KnownNat n => BitVector n -> BitVector n -> BitVector n
{-# OPAQUE and# #-}
{-# ANN and# hasBlackBox #-}
and# =
\(BV m1 v1) (BV m2 v2) ->
let mask = (m1.&.v2 .|. m1.&.m2 .|. m2.&.v1)
in BV mask (v1 .&. v2 .&. complementN mask)
where
complementN = complementMod (natVal (Proxy @n))
{-# OPAQUE or# #-}
{-# ANN or# hasBlackBox #-}
or# =
\(BV m1 v1) (BV m2 v2) ->
let mask = m1 .&. complementN v2 .|. m1.&.m2 .|. m2 .&. complementN v1
in BV mask ((v1.|.v2) .&. complementN mask)
where
complementN = complementMod (natVal (Proxy @n))
{-# OPAQUE xor# #-}
{-# ANN xor# hasBlackBox #-}
xor# =
\(BV m1 v1) (BV m2 v2) ->
let mask = m1 .|. m2
in BV mask ((v1 `xor` v2) .&. complementN mask)
where
complementN = complementMod (natVal (Proxy @n))
{-# OPAQUE complement# #-}
{-# ANN complement# hasBlackBox #-}
complement# :: forall n . KnownNat n => BitVector n -> BitVector n
complement# = \(BV m v) -> BV m (complementN v .&. complementN m)
where complementN = complementMod (natVal (Proxy @n))
shiftL#, shiftR#, rotateL#, rotateR#
:: forall n . KnownNat n => BitVector n -> Int -> BitVector n
{-# OPAQUE shiftL# #-}
{-# ANN shiftL# hasBlackBox #-}
shiftL# = \(BV msk v) i ->
if | i < 0
-> error $ "'shiftL' undefined for negative number: " ++ show i
| fromIntegral i >= sz
-> BV 0 0
| otherwise
-> BV ((shiftL msk i) `mod` m) ((shiftL v i) `mod` m)
where
sz = naturalToWord (natVal (Proxy @n))
m = 1 `naturalShiftL` sz
{-# OPAQUE shiftR# #-}
{-# ANN shiftR# hasBlackBox #-}
shiftR# (BV m v) i
| i < 0 = error
$ "'shiftR' undefined for negative number: " ++ show i
| otherwise = BV (shiftR m i) (shiftR v i)
{-# OPAQUE rotateL# #-}
{-# ANN rotateL# hasBlackBox #-}
rotateL# =
\(BV msk v) b ->
if sz == 0 then
BV msk v
else if b >= 0 then
let vl = naturalShiftL v b'
vr = naturalShiftR v b''
ml = naturalShiftL msk b'
mr = naturalShiftR msk b''
b' = fromIntegral b `mod` sz
b'' = sz - b'
in BV ((ml .|. mr) `mod` m) ((vl .|. vr) `mod` m)
else
error $ "'rotateL' undefined for negative number: " ++ show b
where
sz = naturalToWord (natVal (Proxy @n))
m = 1 `naturalShiftL` sz
{-# OPAQUE rotateR# #-}
{-# ANN rotateR# hasBlackBox #-}
rotateR# =
\(BV msk v) b ->
if sz == 0 then
BV msk v
else if b >= 0 then
let vl = naturalShiftR v b'
vr = naturalShiftL v b''
ml = naturalShiftR msk b'
mr = naturalShiftL msk b''
b' = fromIntegral b `mod` sz
b'' = sz - b'
in BV ((ml .|. mr) `mod` m) ((vl .|. vr) `mod` m)
else
error $ "'rotateR' undefined for negative number: " ++ show b
where
sz = naturalToWord (natVal (Proxy @n))
m = 1 `naturalShiftL` sz
popCountBV :: forall n . KnownNat n => BitVector (n+1) -> I.Index (n+2)
popCountBV bv =
let v = V.bv2v bv
in sum (V.map (fromIntegral . pack#) v)
{-# INLINE popCountBV #-}
instance Resize BitVector where
resize = resizeBV
zeroExtend = (0 ++#)
signExtend = \bv -> (if msb# bv == low then id else complement) 0 ++# bv
truncateB = truncateB#
resizeBV :: forall n m . (KnownNat n, KnownNat m) => BitVector n -> BitVector m
resizeBV = case compareSNat @n @m (SNat @n) (SNat @m) of
SNatLE -> (++#) @n @(m-n) 0
SNatGT -> truncateB# @m @(n - m)
{-# INLINE resizeBV #-}
truncateB# :: forall a b . KnownNat a => BitVector (a + b) -> BitVector a
truncateB# = \(BV msk i) -> BV (msk `mod` m) (i `mod` m)
where m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @a))
{-# OPAQUE truncateB# #-}
{-# ANN truncateB# hasBlackBox #-}
instance KnownNat n => Lift (BitVector n) where
lift bv@(BV m i) = sigE [| fromInteger# m $(litE (IntegerL (toInteger i))) |] (decBitVector (natVal bv))
{-# NOINLINE lift #-}
liftTyped = liftTypedFromUntyped
decBitVector :: Quote m => Natural -> m Type
decBitVector n = appT (conT ''BitVector) (litT $ numTyLit (integerFromNatural n))
instance KnownNat n => SaturatingNum (BitVector n) where
satAdd SatWrap a b = a +# b
satAdd SatZero a b =
let r = plus# a b
in if msb# r == low
then truncateB# r
else minBound#
satAdd SatError a b =
let r = plus# a b
in if msb# r == low
then truncateB# r
else undefined#
satAdd _ a b =
let r = plus# a b
in if msb# r == low
then truncateB# r
else maxBound#
satSub SatWrap a b = a -# b
satSub SatError a b =
let r = minus# a b
in if msb# r == low
then truncateB# r
else undefined#
satSub _ a b =
let r = minus# a b
in if msb# r == low
then truncateB# r
else minBound#
satMul SatWrap a b = a *# b
satMul SatZero a b =
let r = times# a b
(rL,rR) = split# r
in case rL of
0 -> rR
_ -> minBound#
satMul SatError a b =
let r = times# a b
(rL,rR) = split# r
in case rL of
0 -> rR
_ -> undefined#
satMul _ a b =
let r = times# a b
(rL,rR) = split# r
in case rL of
0 -> rR
_ -> maxBound#
instance KnownNat n => Arbitrary (BitVector n) where
arbitrary = arbitraryBoundedIntegral
shrink = shrinkSizedUnsigned
-- | 'shrink' for sized unsigned types
shrinkSizedUnsigned :: (KnownNat n, Integral (p n)) => p n -> [p n]
shrinkSizedUnsigned x | natVal x < 2 = case toInteger x of
1 -> [0]
_ -> []
-- 'shrinkIntegral' uses "`quot` 2", which for sized types
-- less than 2 bits wide results in a division by zero.
--
-- See: https://github.com/clash-lang/clash-compiler/issues/153
| otherwise = shrinkIntegral x
{-# INLINE shrinkSizedUnsigned #-}
instance KnownNat n => CoArbitrary (BitVector n) where
coarbitrary = coarbitraryIntegral
type instance Index (BitVector n) = Int
type instance IxValue (BitVector n) = Bit
instance KnownNat n => Ixed (BitVector n) where
ix i f bv = replaceBit# bv i <$> f (index# bv i)
-- error for infix operator
undefErrorI :: (KnownNat m, KnownNat n) => String -> BitVector m -> BitVector n -> a
undefErrorI op bv1 bv2 = withFrozenCallStack $
errorX $ "Clash.Sized.BitVector." ++ op
++ " called with (partially) undefined arguments: "
++ show bv1 ++ " " ++ op ++" " ++ show bv2
-- error for prefix operator/function
undefErrorP :: (KnownNat m, KnownNat n) => String -> BitVector m -> BitVector n -> a
undefErrorP op bv1 bv2 = withFrozenCallStack $
errorX $ "Clash.Sized.BitVector." ++ op
++ " called with (partially) undefined arguments: "
++ show bv1 ++ " " ++ show bv2
-- error for prefix operator/function
undefErrorP3 :: (KnownNat m, KnownNat n, KnownNat o) => String -> BitVector m -> BitVector n -> BitVector o -> a
undefErrorP3 op bv1 bv2 bv3 = withFrozenCallStack $
errorX $ "Clash.Sized.BitVector." ++ op
++ " called with (partially) undefined arguments: "
++ show bv1 ++ " " ++ show bv2 ++ " " ++ show bv3
-- error for unary operator/function
undefErrorU :: KnownNat n => String -> BitVector n -> a
-- undefErrorU op bv1 = undefError ("Clash.Sized.BitVector." ++ op) [bv1]
undefErrorU op bv1 = withFrozenCallStack $
errorX $ "Clash.Sized.BitVector." ++ op
++ " called with (partially) undefined argument: "
++ show bv1
undefError :: KnownNat n => String -> [BitVector n] -> a
undefError op bvs = withFrozenCallStack $
errorX $ op
++ " called with (partially) undefined arguments: "
++ unwords (L.map show bvs)
-- | Implement BitVector undefinedness checking for unpack functions
checkUnpackUndef :: (KnownNat n, Typeable a)
=> (BitVector n -> a) -- ^ unpack function
-> BitVector n -> a
checkUnpackUndef f bv@(BV 0 _) = f bv
checkUnpackUndef _ bv = res
where
ty = typeOf res
res = undefError (show ty ++ ".unpack") [bv]
{-# OPAQUE checkUnpackUndef #-}
{-# ANN checkUnpackUndef hasBlackBox #-}
-- | Create a BitVector with all its bits undefined
undefined# :: forall n . KnownNat n => BitVector n
undefined# =
let m = 1 `naturalShiftL` naturalToWord (natVal (Proxy @n))
in BV (m-1) 0
{-# OPAQUE 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# =
\(BV cMask c) (BV eMask e) ->
-- set don't care bits to 0
let e' = e .&. complementN eMask
-- checked with undefined bits set to 0
c' = (c .&. complementN cMask) .&. complementN eMask
-- checked with undefined bits set to 1
c'' = (c .|. cMask) .&. complementN eMask
in e' == c' && e' == c''
where
complementN = complementMod (natVal (Proxy @n))
{-# OPAQUE isLike# #-}
fromBits :: [Bit] -> Integer
fromBits = L.foldl (\v b -> v `shiftL` 1 .|. fromIntegral b) 0
-- | Template Haskell macro for generating a pattern matching on some
-- bits of a value.
--
-- This macro compiles to an efficient view pattern that matches the
-- bits of a given value against the bits specified in the
-- pattern. The scrutinee can be any type that is an instance of the
-- 'Num', 'Bits' and 'Eq' typeclasses.
--
-- The bit pattern is specified by a string which contains:
--
-- * @\'0\'@ or @\'1\'@ for matching a bit
--
-- * @\'.\'@ 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 s = [p| ((\_x -> $preprocess) -> $tuple) |]
where
(_, bs, M.toList -> ns) = L.foldr parse (0, [], M.empty) $ filter (/= '_') s
var c is = varP . mkName $ L.replicate (length is) c
bitSelect i = [e| if testBit _x $(litE $ IntegerL i) then pack# high else pack# low |]
varSelect is = L.foldr1 (\a b -> [e| $a ++# $b |]) (bitSelect <$> is)
mask = litE . IntegerL . fromBits $ maybe 0 (const 1) <$> bs
maskE = [e| $mask .&. _x |]
target = litP . IntegerL . fromBits $ fromMaybe 0 <$> bs
preprocess = tupE $ maskE : (varSelect . snd <$> ns)
tuple = tupP $ target : (uncurry var <$> ns)
parse '.' (i, b, n) = (succ i, Nothing:b, n)
parse '0' (i, b, n) = (succ i, Just 0:b, n)
parse '1' (i, b, n) = (succ i, Just 1:b, n)
parse c (i, b, n)
| C.isAlpha c && C.isLower c =
( succ i
, Nothing:b
, M.alter (Just . (i:) . fromMaybe []) c n
)
| otherwise = error $
"Invalid bit pattern: " ++ show c ++
", expecting one of '0', '1', '.', '_', or a lowercase alphabetic character"
xToBV :: KnownNat n => BitVector n -> BitVector n
xToBV x =
unsafeDupablePerformIO (catch (evaluate x)
(\(XException _) -> return undefined#))
{-# OPAQUE xToBV #-}
{-# ANN xToBV hasBlackBox #-}