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