1{-# LANGUAGE DataKinds #-} 2{-# LANGUAGE GADTs #-} 3{-# LANGUAGE KindSignatures #-} 4{-# LANGUAGE PatternSynonyms #-} 5{-# LANGUAGE ScopedTypeVariables #-} 6{-# LANGUAGE TypeOperators #-} 7 8{-| 9Module : Data.BitVector.Sized 10Copyright : (c) Galois Inc. 2018 11License : BSD-3 12Maintainer : Ben Selfridge <benselfridge@galois.com> 13Stability : experimental 14Portability : portable 15 16This module defines a width-parameterized 'BV' type and various 17associated operations. A @'BV' w@ is a newtype around an 'Integer', so 18operations that require the width take an explicit @'NatRepr' w@ 19argument. We explicitly do not allow widths that cannot be represented 20as an 'Prelude.Int', as we appeal to the underlying 'Prelude.Num' and 21'Data.Bits.Bits' instances on 'Integer' for the implementation of many 22of the same operations (which, in turn, require those widths to be 23'Prelude.Int's). 24 25We omit all typeclass instances that require compile-time knowledge of 26bitvector width, or force a signed or unsigned intepretation. Those 27instances can be recovered via the use of 28'Data.BitVector.Sized.Signed.SignedBV' or 29'Data.BitVector.Sized.Unsigned.UnsignedBV'. 30 31This module should be imported qualified, as many of the names clash 32with those in Prelude or other base packages. 33-} 34 35module Data.BitVector.Sized 36 ( -- * 'BV.BV' type 37 BV.BV, pattern BV 38 -- * 'NatRepr's (from parameterized-utils) 39 , NatRepr 40 , knownNat 41 -- * Constructors 42 , mkBV, mkBVUnsigned, mkBVSigned 43 , unsignedClamp, signedClamp 44 , minUnsigned, maxUnsigned 45 , minSigned, maxSigned 46 , zero, one, width 47 -- * Construction from fixed-width data types 48 , bool 49 , word8, word16, word32, word64 50 , int8, int16, int32, int64 51 , bitsBE, bitsLE 52 , bytesBE, bytesLE 53 , bytestringBE, bytestringLE 54 -- * Conversions to primitive types 55 , asSigned 56 , asUnsigned 57 , asNatural 58 , asBitsBE, asBitsLE 59 , asBytesBE, asBytesLE 60 , asBytestringBE, asBytestringLE 61 -- * Bits operations (width-preserving) 62 -- | 'BV' versions of the functions in @Data.Bits@. 63 , and, or, xor 64 , complement 65 , shl, lshr, ashr, rotateL, rotateR 66 , bit, bit' 67 , setBit, setBit' 68 , clearBit, clearBit' 69 , complementBit, complementBit' 70 , testBit, testBit' 71 , popCount 72 , ctz, clz 73 , truncBits 74 -- * Arithmetic operations (width-preserving) 75 , add, sub, mul 76 , uquot, squot, sdiv 77 , urem, srem, smod 78 , uquotRem, squotRem, sdivMod 79 , abs, negate 80 , signBit 81 , signum 82 , slt, sle, ult, ule 83 , umin, umax 84 , smin, smax 85 -- * Variable-width operations 86 -- | These are functions that involve bit vectors of different lengths. 87 , concat 88 , select, select' 89 , zext 90 , sext 91 , trunc, trunc' 92 , mulWide 93 -- * Enum operations 94 , succUnsigned, succSigned 95 , predUnsigned, predSigned 96 , enumFromToUnsigned, enumFromToSigned 97 -- * Pretty printing 98 , ppHex 99 , ppBin 100 , ppOct 101 , ppDec 102 ) where 103 104import Data.BitVector.Sized.Internal hiding (BV(..)) 105import qualified Data.BitVector.Sized.Internal as BV 106 107import Data.Parameterized.NatRepr (knownNat, NatRepr) 108import Prelude (Integer) 109 110-- | Get the underlying 'Integer' representation from a 'BV'. We 111-- guarantee that @(\\(BV.BV x) -> x) == BV.asUnsigned@. 112pattern BV :: Integer -> BV.BV w 113pattern BV x <- BV.BV x 114{-# COMPLETE BV #-} 115