| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Lang.Crucible.Vector
Contents
Synopsis
- module Data.Parameterized.Vector
- fromBV :: forall f (w :: Natural) (n :: Natural). (1 <= w, 1 <= n, IsExpr f) => Endian -> NatRepr n -> NatRepr w -> f (BVType (n * w)) -> Vector n (f (BVType w))
- toBV :: forall f (n :: Natural) (w :: Natural). (1 <= w, IsExpr f) => Endian -> NatRepr w -> Vector n (f (BVType w)) -> f (BVType (n * w))
- joinVecBV :: forall f (i :: Natural) (w :: Natural) (n :: Natural). (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 :: forall f (i :: Natural) (w :: Natural) (n :: Natural). (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 :: Natural) (n :: Natural). (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 :: Natural) (w :: Natural). (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
| :: forall f (i :: Natural) (w :: Natural) (n :: Natural). (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.
Arguments
| :: forall f (i :: Natural) (w :: Natural) (n :: Natural). (IsExpr f, 1 <= i, 1 <= w) | |
| => Endian | |
| -> NatRepr i | Split bit-vectors in this many parts |
| -> NatRepr w | Length of bit-vectors in the result |
| -> Vector n (f (BVType (i * w))) | |
| -> Vector (n * i) (f (BVType w)) |
Turn a vector of large bit-vectors, into a longer vector of shorter bit-vectors.