| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Lang.Crucible.Vector
Contents
Synopsis
- module Data.Parameterized.Vector
- fromBV :: forall f w n. (1 <= w, 1 <= n, IsExpr f) => Endian -> NatRepr n -> NatRepr w -> f (BVType (n * w)) -> Vector n (f (BVType w))
- toBV :: forall f n w. (1 <= w, IsExpr f) => Endian -> NatRepr w -> Vector n (f (BVType w)) -> f (BVType (n * w))
- joinVecBV :: (IsExpr f, 1 <= i, 1 <= w, 1 <= n) => Endian -> NatRepr w -> NatRepr i -> Vector (n * i) (f (BVType w)) -> Vector n (f (BVType (i * w)))
- splitVecBV :: (IsExpr f, 1 <= i, 1 <= w) => Endian -> NatRepr i -> NatRepr w -> Vector n (f (BVType (i * w))) -> Vector (n * i) (f (BVType w))
Documentation
module Data.Parameterized.Vector
Bit-vectors
fromBV :: forall f w n. (1 <= w, 1 <= n, IsExpr f) => Endian -> NatRepr n -> NatRepr w -> f (BVType (n * w)) -> Vector n (f (BVType w)) Source #
Split a bit-vector into a vector of bit-vectors.
toBV :: forall f n w. (1 <= w, IsExpr f) => Endian -> NatRepr w -> Vector n (f (BVType w)) -> f (BVType (n * w)) Source #
Join the bit-vectors in a vector into a single large bit-vector. The Endian parameter indicates which way to join the elemnts: LittleEndian indicates that low vector indexes are less significant.
Arguments
| :: (IsExpr f, 1 <= i, 1 <= w, 1 <= n) | |
| => Endian | How to append bit-vectors |
| -> NatRepr w | Width of bit-vectors in input |
| -> NatRepr i | Number of bit-vectors to join togeter |
| -> Vector (n * i) (f (BVType w)) | |
| -> Vector n (f (BVType (i * w))) |
Turn a vector of bit-vectors, into a shorter vector of longer bit-vectors.