Lang.Crucible.Vector

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))

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))

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.

joinVecBV

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.

splitVecBV

Arguments

:: (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.